Merge branch 'master' into issue#813-support-default-in-executable-specs

backend/cn/bin/main.ml

@@ -461,6 +461,7 @@ let run_tests
   max_unfolds
   max_array_length
   with_static_hack
+  sanitizers
   input_timeout
   null_in_every
   seed
@@ -506,6 +507,7 @@ let run_tests
           max_unfolds;
           max_array_length;
           with_static_hack;
+          sanitizers;
           input_timeout;
           null_in_every;
           seed;
@@ -958,6 +960,22 @@ module Testing_flags = struct
     Arg.(value & flag & info [ "with-static-hack" ] ~doc)
 
 
+  let sanitize =
+    let doc = "Forwarded to the '-fsanitize' argument of the C compiler" in
+    Arg.(
+      value
+      & opt (some string) (fst TestGeneration.default_cfg.sanitizers)
+      & info [ "sanitize" ] ~doc)
+
+
+  let no_sanitize =
+    let doc = "Forwarded to the '-fno-sanitize' argument of the C compiler" in
+    Arg.(
+      value
+      & opt (some string) (snd TestGeneration.default_cfg.sanitizers)
+      & info [ "no-sanitize" ] ~doc)
+
+
   let input_timeout =
     let doc = "Timeout for discarding a generation attempt (ms)" in
     Arg.(
@@ -1114,6 +1132,7 @@ let testing_cmd =
     $ Testing_flags.gen_max_unfolds
     $ Testing_flags.max_array_length
     $ Testing_flags.with_static_hack
+    $ Term.product Testing_flags.sanitize Testing_flags.no_sanitize
     $ Testing_flags.input_timeout
     $ Testing_flags.null_in_every
     $ Testing_flags.seed

backend/cn/lib/check.ml

@@ -2285,19 +2285,27 @@ let record_and_check_logical_functions funs =
       recursive
   in
   (* Now check all functions in order. *)
-  ListM.iteriM
-    (fun i (name, def) ->
-      debug
-        2
-        (lazy
-          (headline
-             ("checking welltypedness of function"
-              ^ Pp.of_total i n_funs
-              ^ ": "
-              ^ Sym.pp_string name)));
-      let@ def = WellTyped.function_ def in
-      Global.add_logical_function name def)
-    funs
+  let@ () =
+    ListM.iteriM
+      (fun i (name, def) ->
+        debug
+          2
+          (lazy
+            (headline
+               ("checking welltypedness of function"
+                ^ Pp.of_total i n_funs
+                ^ ": "
+                ^ Sym.pp_string name)));
+        let@ def = WellTyped.function_ def in
+        Global.add_logical_function name def)
+      funs
+  in
+  let@ global = get_global () in
+  let@ () =
+    Global.set_logical_function_order
+      (Some (WellTyped.logical_function_order global.logical_functions))
+  in
+  return ()
 
 
 let record_and_check_resource_predicates preds =
@@ -2309,20 +2317,28 @@ let record_and_check_resource_predicates preds =
         Global.add_resource_predicate name simple_def)
       preds
   in
-  ListM.iteriM
-    (fun i (name, def) ->
-      debug
-        2
-        (lazy
-          (headline
-             ("checking welltypedness of resource pred"
-              ^ Pp.of_total i (List.length preds)
-              ^ ": "
-              ^ Sym.pp_string name)));
-      let@ def = WellTyped.predicate def in
-      (* add simplified def to the context *)
-      Global.add_resource_predicate name def)
-    preds
+  let@ () =
+    ListM.iteriM
+      (fun i (name, def) ->
+        debug
+          2
+          (lazy
+            (headline
+               ("checking welltypedness of resource pred"
+                ^ Pp.of_total i (List.length preds)
+                ^ ": "
+                ^ Sym.pp_string name)));
+        let@ def = WellTyped.predicate def in
+        (* add simplified def to the context *)
+        Global.add_resource_predicate name def)
+      preds
+  in
+  let@ global = get_global () in
+  let@ () =
+    Global.set_resource_predicate_order
+      (Some (WellTyped.resource_predicate_order global.resource_predicates))
+  in
+  return ()
 
 
 let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> LC.t list m =

backend/cn/lib/global.ml

@@ -10,7 +10,9 @@ type t =
     datatype_order : Sym.t list list option;
     fun_decls : (Locations.t * AT.ft option * Sctypes.c_concrete_sig) Sym.Map.t;
     resource_predicates : Definition.Predicate.t Sym.Map.t;
+    resource_predicate_order : Sym.t list list option;
     logical_functions : Definition.Function.t Sym.Map.t;
+    logical_function_order : Sym.t list list option;
     lemmata : (Locations.t * AT.lemmat) Sym.Map.t
   }
 
@@ -21,7 +23,9 @@ let empty =
     datatype_order = None;
     fun_decls = Sym.Map.empty;
     resource_predicates = Sym.Map.(empty |> add Alloc.Predicate.sym Definition.alloc);
+    resource_predicate_order = None;
     logical_functions = Sym.Map.empty;
+    logical_function_order = None;
     lemmata = Sym.Map.empty
   }
 

backend/cn/lib/testGeneration/buildScript.ml

@@ -41,25 +41,34 @@ let attempt cmd success failure =
   ^^ string "fi"
 
 
+let cc_flags () =
+  [ "-g"; "\"-I${RUNTIME_PREFIX}/include/\"" ]
+  @ (let sanitize, no_sanitize = Config.has_sanitizers () in
+     (match sanitize with Some sanitize -> [ "-fsanitize=" ^ sanitize ] | None -> [])
+     @
+     match no_sanitize with
+     | Some no_sanitize -> [ "-fno-sanitize=" ^ no_sanitize ]
+     | None -> [])
+  @
+  if Config.is_coverage () then
+    [ "--coverage" ]
+  else
+    []
+
+
 let compile ~filename_base =
   string "# Compile"
   ^^ hardline
   ^^ attempt
        (String.concat
           " "
           ([ "cc";
-             "-g";
              "-c";
-             "\"-I${RUNTIME_PREFIX}/include/\"";
              "-o";
              "\"./" ^ filename_base ^ "_test.o\"";
              "\"./" ^ filename_base ^ "_test.c\""
            ]
-           @
-           if Config.is_coverage () then
-             [ "--coverage" ]
-           else
-             []))
+           @ cc_flags ()))
        ("Compiled '" ^ filename_base ^ "_test.c'.")
        ("Failed to compile '" ^ filename_base ^ "_test.c' in ${TEST_DIR}.")
   ^^ (if Config.with_static_hack () then
@@ -70,37 +79,19 @@ let compile ~filename_base =
              (String.concat
                 " "
                 ([ "cc";
-                   "-g";
                    "-c";
-                   "\"-I${RUNTIME_PREFIX}/include/\"";
                    "-o";
                    "\"./" ^ filename_base ^ "-exec.o\"";
                    "\"./" ^ filename_base ^ "-exec.c\""
                  ]
-                 @
-                 if Config.is_coverage () then
-                   [ "--coverage" ]
-                 else
-                   []))
+                 @ cc_flags ()))
              ("Compiled '" ^ filename_base ^ "-exec.c'.")
              ("Failed to compile '" ^ filename_base ^ "-exec.c' in ${TEST_DIR}.")
         ^^ twice hardline
         ^^ attempt
              (String.concat
                 " "
-                ([ "cc";
-                   "-g";
-                   "-c";
-                   "\"-I${RUNTIME_PREFIX}/include/\"";
-                   "-o";
-                   "\"./cn.o\"";
-                   "\"./cn.c\""
-                 ]
-                 @
-                 if Config.is_coverage () then
-                   [ "--coverage" ]
-                 else
-                   []))
+                ([ "cc"; "-c"; "-o"; "\"./cn.o\""; "\"./cn.c\"" ] @ cc_flags ()))
              "Compiled 'cn.c'."
              "Failed to compile 'cn.c' in ${TEST_DIR}.")
   ^^ hardline
@@ -115,8 +106,6 @@ let link ~filename_base =
        (String.concat
           " "
           ([ "cc";
-             "-g";
-             "\"-I${RUNTIME_PREFIX}/include\"";
              "-o";
              "\"./tests.out\"";
              (filename_base
@@ -128,11 +117,7 @@ let link ~filename_base =
                 " " ^ filename_base ^ "-exec.o cn.o");
              "\"${RUNTIME_PREFIX}/libcn.a\""
            ]
-           @
-           if Config.is_coverage () then
-             [ "--coverage" ]
-           else
-             []))
+           @ cc_flags ()))
        "Linked C *.o files."
        "Failed to link *.o files in ${TEST_DIR}."
   ^^ hardline

backend/cn/lib/testGeneration/testGenConfig.ml

@@ -5,6 +5,7 @@ type t =
     max_unfolds : int option;
     max_array_length : int;
     with_static_hack : bool;
+    sanitizers : string option * string option;
     (* Run time *)
     input_timeout : int option;
     null_in_every : int option;
@@ -30,6 +31,7 @@ let default =
     max_unfolds = None;
     max_array_length = 50;
     with_static_hack = false;
+    sanitizers = (None, None);
     input_timeout = None;
     null_in_every = None;
     seed = None;
@@ -63,6 +65,8 @@ let get_max_array_length () = !instance.max_array_length
 
 let with_static_hack () = !instance.with_static_hack
 
+let has_sanitizers () = !instance.sanitizers
+
 let has_input_timeout () = !instance.input_timeout
 
 let has_null_in_every () = !instance.null_in_every

backend/cn/lib/testGeneration/testGenConfig.mli

@@ -5,6 +5,7 @@ type t =
     max_unfolds : int option;
     max_array_length : int;
     with_static_hack : bool;
+    sanitizers : string option * string option;
     (* Run time *)
     input_timeout : int option;
     null_in_every : int option;
@@ -38,6 +39,8 @@ val get_max_array_length : unit -> int
 
 val with_static_hack : unit -> bool
 
+val has_sanitizers : unit -> string option * string option
+
 val has_input_timeout : unit -> int option
 
 val has_null_in_every : unit -> int option

backend/cn/lib/typing.ml

@@ -286,6 +286,26 @@ module Global = struct
   let get_datatype_order () =
     let@ g = get_global () in
     return g.datatype_order
+
+
+  let set_resource_predicate_order resource_predicate_order =
+    let@ g = get_global () in
+    set_global { g with resource_predicate_order }
+
+
+  let get_resource_predicate_order () =
+    let@ g = get_global () in
+    return g.resource_predicate_order
+
+
+  let set_logical_function_order logical_function_order =
+    let@ g = get_global () in
+    set_global { g with logical_function_order }
+
+
+  let get_logical_function_order () =
+    let@ g = get_global () in
+    return g.logical_function_order
 end
 
 (* end: convenient functions for global typing context *)

backend/cn/lib/typing.mli

@@ -128,6 +128,14 @@ module Global : sig
 
   val get_datatype_order : unit -> Sym.t list list option m
 
+  val set_resource_predicate_order : Sym.t list list option -> unit m
+
+  val get_resource_predicate_order : unit -> Sym.t list list option m
+
+  val set_logical_function_order : Sym.t list list option -> unit m
+
+  val get_logical_function_order : unit -> Sym.t list list option m
+
   val add_resource_predicate : Sym.t -> Definition.Predicate.t -> unit m
 
   val add_logical_function : Sym.t -> Definition.Function.t -> unit m