Cleaning flags

case_studies/clift/demo/demo_no_verif.ml

@@ -1,8 +1,10 @@
+(* Deprecated *)
+
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := false;
+  (* Flags.check_validity := false; *)
   Flags.detailed_resources_in_trace := false;
   Flags.pretty_matrix_notation := true
 

case_studies/clift/demo/demo_verif.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := true;
+  (* Flags.check_validity := true; *)
   (* Flags.detailed_resources_in_trace := true; *)
   Flags.save_ast_for_steps := Some Steps_important
 

case_studies/clift/demo/loop_swap.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := true;
+  (* Flags.check_validity := true; *)
   Flags.detailed_resources_in_trace := true;
   Flags.save_ast_for_steps := Some Steps_all
 

case_studies/clift/quantization/access_scale.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.check_validity := true *)
+(* let _ = Flags.recompute_resources_between_steps := true *)
 
 let insert_max_tab_on (tab : typed_var) (size : trm) (i : int) (t : trm) : trm =
   let v, typ = tab in

case_studies/clift/quantization/matvec_to_quantize.ml

@@ -1,10 +1,11 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
   Flags.pretty_matrix_notation := true;
   Flags.print_optitrust_syntax := true;
-  Flags.check_validity := false
+  (* Flags.check_validity := false *)
 
 let reconstruct_seq (lbefore : trm mlist) (t : trm) (lafter : trm mlist) : trm =
   let new_lbefore = Mlist.push_back t lbefore in

case_studies/clift/verif/kernels.ml

@@ -1,7 +1,8 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := true;Flags.detailed_resources_in_trace := true;
+ (*  Flags.check_validity := true; *)Flags.detailed_resources_in_trace := true;
 Flags.save_ast_for_steps := Some Steps_all
 let _  = Run.script_cpp ( fun x -> !!!());

case_studies/dot_product/dot.ml

@@ -1,9 +1,10 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true (* FIXME: false *)
+(* let _ = Flags.check_validity := true (* FIXME: false *) *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.use_resources_with_models := true
-let _ = Flags.preserve_specs_only := true
+(* let _ = Flags.preserve_specs_only := true *)
 let _ = Flags.pretty_matrix_notation := false
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true

case_studies/floyd_warshall/floyd_warshall.ml

@@ -1,3 +1,4 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 

case_studies/gpu/histogram/hist.ml

@@ -1,7 +1,8 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.pretty_matrix_notation := true
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true

case_studies/gpu/matmul/matmul.ml

@@ -1,7 +1,8 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true (* FIXME: this flag behaviour needs to be cleaned up *)
+(* let _ = Flags.check_validity := true  *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.pretty_matrix_notation := false
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true

case_studies/gpu/reduction/reduce.ml

@@ -1,9 +1,10 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
 let _ = Flags.use_resources_with_models := true
-let _ = Flags.preserve_specs_only := true
+(* let _ = Flags.preserve_specs_only := true *)
+let _ = Flags.typechecking_mode := Flags.Annotated
 let _ = Flags.pretty_matrix_notation := false
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true
@@ -115,7 +116,7 @@ let _ = Run.script_cpp_stage stage_ok (fun () ->
   let sum_tg = [cFunDef "reduce"; cFor "bi"; cFor "ti"; cArrayWrite "d_partial_sums"] in
   !! Ghost.flatten_expr_rewrites (sum_tg @ [dRHS]);
   !! replace_with_tree_reduce (trm_int log_tpb) sum_tg;
-  !! Flags.with_flag Flags.check_validity false (fun () -> Function.inline_def [cFunDef "tree_reduce"]);
+  !! Flags.with_flag (* Flags.check_validity false *) Flags.typechecking_mode Flags.Unverified (fun () -> Function.inline_def [cFunDef "tree_reduce"]);
 
   (* Mask writing of final result to only 1 thread *)
   !! Loop_basic.intro_loop_single_on ~index:"ti_f" (trm_int tpb) [tAfter; cFor "i" ~body:[cFor "t"]] [tAfter; occLast; cArrayWrite "d_partial_sums"];

case_studies/gpu/transpose/transpose.ml

@@ -1,7 +1,8 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true
 let _ = Flags.save_ast_for_steps := Some Flags.Steps_important

case_studies/gpu/transpose/transpose_gpu.ml

@@ -1,7 +1,8 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.pretty_matrix_notation := true
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true

case_studies/gpu/vector_add/vector_add.ml

@@ -2,7 +2,8 @@ open Optitrust
 open Prelude
 open Cuda_lowering
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.pretty_matrix_notation := true
 let _ = Flags.recompute_resources_between_steps := false
 let _ = Flags.disable_stringreprs := true
@@ -24,7 +25,7 @@ let _ = Run.script_cpp (fun () ->
   !! Resources.ensure_computed ();
 
   (* Stage 2: create thread hierarchy *)
-  !! Gpu.convert_tail_thread_for [cFor "i"];
+  !! Gpu.convert_tail_thread_for [] [cFor "i"];
   !! Resources.ensure_computed ();
 
   (* Stage 3: convert memories *)

case_studies/matmul/matmul.ml

@@ -1,8 +1,8 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ = Flags.pretty_matrix_notation := true
-let _ = Flags.disable_resource_typing ()
 
 (* Reproducing a TVM schedule for matrix multiplication:
    1. improve data locality by blocking the computation of C and preloading B with a packed memory layout

case_studies/matmul/matmul_check.ml

@@ -1,9 +1,10 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
 let _ = Flags.pretty_matrix_notation := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.recompute_resources_between_steps := true *)
 let _ = Flags.disable_stringreprs := true
 
 (* let _ = Flags.report_exectime := true *)

case_studies/matmul/matmul_models.ml

@@ -1,7 +1,8 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.pretty_matrix_notation := true
 let _ = Flags.recompute_resources_between_steps := true
 let _ = Flags.disable_stringreprs := true

case_studies/minipic/fixed_tmp_micropic.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.check_validity := true
+let _ = Flags.recompute_resources_between_steps := true *)
 
 (** Reproducing a subset of the PIC case study *)
 

case_studies/minipic/micropic.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.check_validity := true
+let _ = Flags.recompute_resources_between_steps := true *)
 let _ = Flags.disable_stringreprs := true
 let _ = Flags.save_steps := Some Steps_script
 let _ = Flags.save_ast_for_steps := Some Steps_all

case_studies/opencv/box_filter_rowsum.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.check_validity := true
+let _ = Flags.recompute_resources_between_steps := true *)
 let _ = Flags.disable_stringreprs := true
 
 (* Generated trace is too heavy. Keep only the steps of the transformation script *)

case_studies/opencv/box_filter_rowsum_before_cleanup.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.check_validity := true
+let _ = Flags.recompute_resources_between_steps := true *)
 let _ = Flags.disable_stringreprs := true
 
 let _ = Run.script_cpp (fun () ->

case_studies/opencv/box_filter_rowsum_models.ml

@@ -1,8 +1,9 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
 let _ = Flags.recompute_resources_between_steps := true
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.disable_stringreprs := true
 
 (* Generated trace is too heavy. Keep only the steps of the transformation script *)

case_studies/opencv/box_filter_rowsum_models_end.ml

@@ -1,7 +1,8 @@
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
+(* let _ = Flags.check_validity := true *)
+let _ = Flags.typechecking_mode := Flags.AnnotatedAndVerified
 let _ = Flags.disable_stringreprs := true
 
 (* Generated trace is too heavy. Keep only the steps of the transformation script *)

case_studies/tuto/reduction_reinit/reduction_reinit.ml

@@ -1,6 +1,7 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
-let _ = Flags.check_validity := false
+(* let _ = Flags.check_validity := false *)
 let delocalize_sum = Local_arith (Lit_float (typ_f64,0.)  , Binop_add)
 let _ = Run.script_cpp (fun _ ->
 

case_studies/tuto/skewing/skewing.ml

@@ -1,7 +1,8 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := false
+(* let _ = Flags.check_validity := false *)
 let _ =
   Run.script_cpp (fun _ ->
 

case_studies/tuto/stencil/stencil1D.ml

@@ -1,6 +1,7 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
-let _ = Flags.check_validity := false
+(* let _ = Flags.check_validity := false *)
 
 let _ = Run.script_cpp (fun _ ->
   !! Loop.fission [cForBody "i"; tBefore; dSeqNth 1];)

lib/framework/flags.ml

@@ -21,7 +21,7 @@ let analyse_stats_details : bool ref = ref false
 (** [dump_ast_details]: flag to dump OptiTrust AST, both in the form of a '.ast' and '_enc.cpp' files. *)
 let dump_ast_details : bool ref = ref false
 
-(* TODO : deprecate once optilambda surface display works *)
+(* TODO Yanni : deprecate once optilambda surface display works *)
 (** [pretty_matrix_notation]: flag to display matrix macros with syntactic sugar:
   MALLOC2(n, m, sizeof(T)) --> malloc(sizeof(T[n][m]))
   x[MINDEX2(n, m, i, j)] --> x[i;j]
@@ -78,7 +78,7 @@ let reparse_at_big_steps : bool ref = ref false
 let report_big_steps : bool ref = ref false
 
 (** [use_clang_format]: flag to use clang-format or not in output CPP files. *)
-let use_clang_format : bool ref = ref true
+let use_clang_format : bool ref = ref false
 
 (** [keep_file_before_clang_format]: flag to save the file before cleaning up with clang format
    "foo_out.cpp" is saved as "foo_out_notfmt.cpp". Used by the tester for faster correctness checks. *)
@@ -90,9 +90,9 @@ let clang_format_nb_columns : int ref = ref 80
 (** [code_print_width]: flag to choose the width of the printed code on stdout. *)
 let code_print_width = ref 80
 
+(* TODO: could it be true by default? *)
 (** [use_light_diff]: flag to enable "light diffs", whereby we hide the function body of all the
    toplevel functions that are not affected by the transformation. *)
-   (* TODO: could it be true by default? *)
 let use_light_diff : bool ref = ref false
 
 (** [bypass_cfeatures]: flag used for debugging the [decode_from_c/intro] functions, by bypassing them.
@@ -131,18 +131,20 @@ let resource_typing_enabled = ref true
 
 (* TODO Yanni : reevaluate *)
 (** [check_validity]: perform validation of transformations *)
-let check_validity = ref false
+(* let check_validity = ref false *)
 
 (* TODO Yanni : reevaluate *)
 (** [preserve_specs_only]: allow code transformation that preserve the specification without necessarily preserving the semantics
     TODO: update code which was also using check_validity for this purpose *)
-let preserve_specs_only = ref false
+(* Deprecated *)
+(* let preserve_specs_only = ref false *)
 
 (* TODO Yanni : reevaluate *)
 (** [disable_resource_typing ()] should be called when using OptiTrust without resources. *)
-let disable_resource_typing () =
+(* Deprecated *)
+(* let disable_resource_typing () =
   resource_typing_enabled := false;
-  check_validity := false
+  check_validity := false *)
 
 (** [reparse_between_step]: always reparse between two steps *)
 let reparse_between_steps = ref false
@@ -162,8 +164,32 @@ let clang_use_libstdcxx = ref false
 
 let aux_file_compare = ref (fun (f1: string) (f2: string) -> true)
 
-(** Possible [execution_mode] of the script *)
+(* Start of new flags *)
+
+type typechecking_mode =
+  | Unverified (* equivalent to `resource_typing_enabled = false && check_validity = false` *)
+  | Annotated (* equivalent to `check_validity = false` *)
+  | AnnotatedAndVerified (* equivalent to `check_validity := true && preserve_specs_only = false` *)
+
+(** [typechecking_mode]: Defines the verification guarantee of the input code for transformations and typechecking. *)
+let typechecking_mode : typechecking_mode ref = ref Annotated (* Should later on be changed to AnnotatedAndVerified *)
+
+let unverified () : bool = !typechecking_mode = Unverified
+let annotated () : bool = (!typechecking_mode = Annotated) || (!typechecking_mode = AnnotatedAndVerified)
+let only_annotated () : bool = (!typechecking_mode = Annotated)
+let annotated_and_verified () : bool = !typechecking_mode = AnnotatedAndVerified
 
+(* Expected to be a temporary function, to be used in [trace.ml] where there is a [flag_check_validity] flag *)
+let match_typechecking_mode (flag_check_validity : bool) = if flag_check_validity then AnnotatedAndVerified else Unverified
+
+let typechecking_mode_to_string = function
+  | Unverified -> "Unverivied"
+  | Annotated -> "Annotated"
+  | AnnotatedAndVerified -> "AnnotatedAndVerified"
+
+(* End of new flags *)
+
+(** Possible [execution_mode] of the script *)
 type execution_mode =
   | Execution_mode_step_diff (* produce a diff for a small-step, assumes [target_line] is provided *)
   | Execution_mode_step_trace (* produce a trace for a small-step, assumes [target_line] is provided *)
@@ -403,8 +429,8 @@ let reset_flags_to_default () : unit =
   display_includes := false;
   stop_on_first_resource_error := true;
   resource_typing_enabled := true;
-  check_validity := false;
-  preserve_specs_only := false;
+  (* TO be modified when the code is clean: *)
+  typechecking_mode := Annotated;
   reparse_between_steps := false;
   recompute_resources_between_steps := false;
   save_steps := None;