Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[CN-Test-Gen] Add sanitize-trap #824

Closed
wants to merge 1 commit into from
Closed

[CN-Test-Gen] Add sanitize-trap #824

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci-cn-spec-testing.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 13 additions & 3 deletions backend/cn/bin/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -964,18 +964,26 @@ 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)


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)
& 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.(
Expand Down Expand Up @@ -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
Expand Down
9 changes: 6 additions & 3 deletions backend/cn/lib/testGeneration/buildScript.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions backend/cn/lib/testGeneration/testGenConfig.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions backend/cn/lib/testGeneration/testGenConfig.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion tests/run-cn-test-gen.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading