diff --git a/.github/workflows/ci-cn-spec-testing.yml b/.github/workflows/ci-cn-spec-testing.yml index 0bcdb4d74..8ff76b2ab 100644 --- a/.github/workflows/ci-cn-spec-testing.yml +++ b/.github/workflows/ci-cn-spec-testing.yml @@ -31,7 +31,7 @@ jobs: - name: System dependencies (ubuntu) run: | - sudo apt-get install build-essential libgmp-dev z3 opam cmake lcov + sudo apt-get install build-essential libgmp-dev z3 opam cmake lcov gcc-13 - name: Restore cached opam id: cache-opam-restore diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 3756b8e24..fc4a90696 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -964,7 +964,7 @@ module Testing_flags = struct let doc = "Forwarded to the '-fsanitize' argument of the C compiler" in Arg.( value - & opt (some string) (fst TestGeneration.default_cfg.sanitizers) + & opt (some string) (fst (fst TestGeneration.default_cfg.sanitizers)) & info [ "sanitize" ] ~doc) @@ -972,10 +972,18 @@ module Testing_flags = struct let doc = "Forwarded to the '-fno-sanitize' argument of the C compiler" in Arg.( value - & opt (some string) (snd TestGeneration.default_cfg.sanitizers) + & opt (some string) (snd (fst TestGeneration.default_cfg.sanitizers)) & info [ "no-sanitize" ] ~doc) + let sanitize_trap = + let doc = "Forwarded to the '-fsanitize-trap' argument of the C compiler" in + Arg.( + value + & opt (some string) (snd TestGeneration.default_cfg.sanitizers) + & info [ "sanitize-trap" ] ~doc) + + let input_timeout = let doc = "Timeout for discarding a generation attempt (ms)" in Arg.( @@ -1132,7 +1140,9 @@ 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 + $ Term.product + (Term.product Testing_flags.sanitize Testing_flags.no_sanitize) + Testing_flags.sanitize_trap $ 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 index 33dcd92c9..759cbac58 100644 --- a/backend/cn/lib/testGeneration/buildScript.ml +++ b/backend/cn/lib/testGeneration/buildScript.ml @@ -43,11 +43,14 @@ let attempt cmd success failure = let cc_flags () = [ "-g"; "\"-I${RUNTIME_PREFIX}/include/\"" ] - @ (let sanitize, no_sanitize = Config.has_sanitizers () in + @ (let (sanitize, no_sanitize), sanitize_trap = Config.has_sanitizers () in (match sanitize with Some sanitize -> [ "-fsanitize=" ^ sanitize ] | None -> []) + @ (match no_sanitize with + | Some no_sanitize -> [ "-fno-sanitize=" ^ no_sanitize ] + | None -> []) @ - match no_sanitize with - | Some no_sanitize -> [ "-fno-sanitize=" ^ no_sanitize ] + match sanitize_trap with + | Some sanitize_trap -> [ "-fsanitize-trap=" ^ sanitize_trap ] | None -> []) @ if Config.is_coverage () then diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/backend/cn/lib/testGeneration/testGenConfig.ml index 77c0f74dc..3ad9bf9fd 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.ml +++ b/backend/cn/lib/testGeneration/testGenConfig.ml @@ -5,7 +5,7 @@ type t = max_unfolds : int option; max_array_length : int; with_static_hack : bool; - sanitizers : string option * string option; + sanitizers : (string option * string option) * string option; (* Run time *) input_timeout : int option; null_in_every : int option; @@ -31,7 +31,7 @@ let default = max_unfolds = None; max_array_length = 50; with_static_hack = false; - sanitizers = (None, None); + sanitizers = ((None, None), None); input_timeout = None; null_in_every = None; seed = None; diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/backend/cn/lib/testGeneration/testGenConfig.mli index 2ac4b0a66..d53a33626 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.mli +++ b/backend/cn/lib/testGeneration/testGenConfig.mli @@ -5,7 +5,7 @@ type t = max_unfolds : int option; max_array_length : int; with_static_hack : bool; - sanitizers : string option * string option; + sanitizers : (string option * string option) * string option; (* Run time *) input_timeout : int option; null_in_every : int option; @@ -39,7 +39,7 @@ val get_max_array_length : unit -> int val with_static_hack : unit -> bool -val has_sanitizers : unit -> string option * string option +val has_sanitizers : unit -> (string option * string option) * string option val has_input_timeout : unit -> int option diff --git a/tests/run-cn-test-gen.sh b/tests/run-cn-test-gen.sh index 2ab15f444..ce7a73bcf 100755 --- 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 --sanitize=undefined --no-sanitize=alignment" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") +CONFIGS=("--coverage" "--with-static-hack --coverage --sanitize=undefined --no-sanitize=alignment --sanitize-trap=all" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") # For each configuration for CONFIG in "${CONFIGS[@]}"; do