[CN-Test-Gen] CLI args for using sanitizers (#822)

* [CN-Test-Gen] Allow passing sanitizers * [CN-Test-Gen] Add UBSan (w/o alignment) to CI
rems-project · Jan 8, 2025 · 6c3ad3f · 6c3ad3f
1 parent a356435
commit 6c3ad3f
Show file tree

Hide file tree

Showing 5 changed files with 46 additions and 35 deletions.
diff --git a/backend/cn/bin/main.ml b/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

diff --git a/backend/cn/lib/testGeneration/buildScript.ml b/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

diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/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

diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/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

diff --git a/tests/run-cn-test-gen.sh b/tests/run-cn-test-gen.sh
@@ -27,7 +27,7 @@ function separator() {
   printf '\n\n'
 }
 
-CONFIGS=("--coverage" "--with-static-hack --coverage" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10")
+CONFIGS=("--coverage" "--with-static-hack --coverage --sanitize=undefined --no-sanitize=alignment" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10")
 
 # For each configuration
 for CONFIG in "${CONFIGS[@]}"; do