From a356435a1368cfd8449bd215ba66fe9af070b43a Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 8 Jan 2025 18:45:49 +0000 Subject: [PATCH 1/3] Predicate and function order (#819) * compute strongly connected components for resource predicate definitions and specification function definitions, and record in global typing context * ocamlformat --- backend/cn/lib/check.ml | 70 +++++++++++++++++++------------ backend/cn/lib/global.ml | 4 ++ backend/cn/lib/typing.ml | 20 +++++++++ backend/cn/lib/typing.mli | 8 ++++ backend/cn/lib/wellTyped.ml | 72 ++++++++++++++++++++++++++++++++ backend/cn/lib/wellTyped_intf.ml | 4 ++ 6 files changed, 151 insertions(+), 27 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index bfa0383c9..14336d694 100644 --- a/backend/cn/lib/check.ml +++ b/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 = diff --git a/backend/cn/lib/global.ml b/backend/cn/lib/global.ml index 3b18160c2..8b2e18aee 100644 --- a/backend/cn/lib/global.ml +++ b/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 } diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml index 74e58a84b..99faa7088 100644 --- a/backend/cn/lib/typing.ml +++ b/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 *) diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli index 881e89b9a..026673003 100644 --- a/backend/cn/lib/typing.mli +++ b/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 diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index da7ad671f..f2d49a33b 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -2288,6 +2288,45 @@ module WRPD = struct return (Some clauses) in return Def.Predicate.{ loc; pointer; iargs; oarg_bt; clauses }) + + + module G = Graph.Persistent.Digraph.Concrete (Sym) + module Components = Graph.Components.Make (G) + + let resource_predicate_order predicates = + let graph = G.empty in + let graph = Sym.Map.fold (fun p _ graph -> G.add_vertex graph p) predicates graph in + let graph = + Sym.Map.fold + (fun p pdef graph -> + match pdef.Definition.Predicate.clauses with + | None -> graph + | Some clauses -> + List.fold_left + (fun graph clause -> + let rec aux graph packing_ft = + let open LogicalArgumentTypes in + match packing_ft with + | Define (_, _, packing_ft) -> aux graph packing_ft + | Resource ((_, (req, _)), _, packing_ft) -> + let graph = + match req with + | P { name = Owned _; _ } | Q { name = Owned _; _ } -> graph + | P { name = PName p'; _ } | Q { name = PName p'; _ } -> + G.add_edge graph p p' + in + aux graph packing_ft + | Constraint (_, _, packing_ft) -> aux graph packing_ft + | I _return_value -> graph + in + aux graph clause.Definition.Clause.packing_ft) + graph + clauses) + predicates + graph + in + let sccs = Components.scc_list graph in + sccs end module WLFD = struct @@ -2316,6 +2355,31 @@ module WLFD = struct | Uninterp -> return Uninterp in return { loc; args; return_bt; emit_coq; body }) + + + module G = Graph.Persistent.Digraph.Concrete (Sym) + module Components = Graph.Components.Make (G) + + let logical_function_order functions = + let graph = G.empty in + let graph = + Sym.Map.fold (fun fname _ graph -> G.add_vertex graph fname) functions graph + in + let graph = + Sym.Map.fold + (fun fname fdef graph -> + let calls = + match fdef.body with + | Def body -> IT.preds_of body + | Rec_Def body -> IT.preds_of body + | Uninterp -> Sym.Set.empty + in + Sym.Set.fold (fun fname' graph -> G.add_edge graph fname fname') calls graph) + functions + graph + in + let sccs = Components.scc_list graph in + sccs end module WLemma = struct @@ -2437,6 +2501,10 @@ let datatype = WDT.welltyped let datatype_recursion = WDT.check_recursion_ok +let logical_function_order = WLFD.logical_function_order + +let resource_predicate_order = WRPD.resource_predicate_order + let lemma = WLemma.welltyped let function_ = WLFD.welltyped @@ -2508,6 +2576,10 @@ module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = stru let datatype_recursion = lift1 datatype_recursion + let logical_function_order = (* lift1 *) logical_function_order + + let resource_predicate_order = (* lift1 *) resource_predicate_order + let lemma x y z = lift3 lemma x y z let function_ = lift1 function_ diff --git a/backend/cn/lib/wellTyped_intf.ml b/backend/cn/lib/wellTyped_intf.ml index d3e179f32..2c8ed06bc 100644 --- a/backend/cn/lib/wellTyped_intf.ml +++ b/backend/cn/lib/wellTyped_intf.ml @@ -70,4 +70,8 @@ module type S = sig val datatype : 'a * Mucore.datatype -> ('a * Mucore.datatype) t val datatype_recursion : (Sym.t * Mucore.datatype) list -> Sym.t list list t + + val logical_function_order : Definition.Function.t Sym.Map.t -> Sym.t list list + + val resource_predicate_order : Definition.Predicate.t Sym.Map.t -> Sym.t list list end From 6c3ad3fc0b1bba55aaab625eda2c900923f95359 Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Wed, 8 Jan 2025 15:05:29 -0500 Subject: [PATCH 2/3] [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 --- backend/cn/bin/main.ml | 19 +++++++ backend/cn/lib/testGeneration/buildScript.ml | 53 +++++++------------ .../cn/lib/testGeneration/testGenConfig.ml | 4 ++ .../cn/lib/testGeneration/testGenConfig.mli | 3 ++ tests/run-cn-test-gen.sh | 2 +- 5 files changed, 46 insertions(+), 35 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 816fe8743..3756b8e24 100644 --- 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 index 97685cc43..33dcd92c9 100644 --- a/backend/cn/lib/testGeneration/buildScript.ml +++ b/backend/cn/lib/testGeneration/buildScript.ml @@ -41,6 +41,21 @@ 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 @@ -48,18 +63,12 @@ let compile ~filename_base = (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 index 8a43a1223..77c0f74dc 100644 --- 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 index e1c9acbce..2ac4b0a66 100644 --- 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 index bfb477a1e..2ab15f444 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" "--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 From 8b22b2b144b26ddc116445740ad28835379b6d53 Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Thu, 9 Jan 2025 12:41:25 -0500 Subject: [PATCH 3/3] [CN-Exec] Add UBSan (w/o alignment) to CI (#825) --- runtime/libcn/libexec/cn-runtime-single-file.sh | 14 ++++++++++---- tests/run-cn-exec.sh | 2 +- tests/run-cn-test-gen.sh | 3 +++ 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/runtime/libcn/libexec/cn-runtime-single-file.sh b/runtime/libcn/libexec/cn-runtime-single-file.sh index cdf35555c..e43642757 100755 --- a/runtime/libcn/libexec/cn-runtime-single-file.sh +++ b/runtime/libcn/libexec/cn-runtime-single-file.sh @@ -1,7 +1,7 @@ #!/bin/bash set -euo pipefail -o noclobber -USAGE="USAGE: $0 -h\n $0 [-nvq] FILE.c" +USAGE="USAGE: $0 -h\n $0 [-nqu] FILE.c" function echo_and_err() { printf "$1\n" @@ -9,9 +9,10 @@ function echo_and_err() { } QUIET="" +UBSAN="" NO_CHECK_OWNERSHIP="" -while getopts "hnq" flag; do +while getopts "hnqu" flag; do case "$flag" in h) printf "${USAGE}" @@ -23,6 +24,11 @@ while getopts "hnq" flag; do q) QUIET=1 ;; + u) + export UBSAN_OPTIONS=halt_on_error=1 + # FIXME: https://github.com/rems-project/cerberus/issues/821 + UBSAN="-fsanitize=undefined -fno-sanitize=alignment" + ;; \?) echo_and_err "${USAGE}" ;; @@ -65,14 +71,14 @@ fi # Compile cd "${EXEC_DIR}" -if cc -g -c "-I${RUNTIME_PREFIX}"/include/ ./"${INPUT_BASENAME}-exec.c" cn.c; then +if cc -g -c ${UBSAN} "-I${RUNTIME_PREFIX}"/include/ ./"${INPUT_BASENAME}-exec.c" cn.c; then [ "${QUIET}" ] || echo "Compiled C files." else echo_and_err "Failed to compile C files in ${EXEC_DIR}." fi # Link -if cc "-I${RUNTIME_PREFIX}/include" -o "${INPUT_BASENAME}-exec-output.bin" ./*.o "${RUNTIME_PREFIX}/libcn.a"; then +if cc ${UBSAN} "-I${RUNTIME_PREFIX}/include" -o "${INPUT_BASENAME}-exec-output.bin" ./*.o "${RUNTIME_PREFIX}/libcn.a"; then [ "${QUIET}" ] || echo "Linked C .o files." else echo_and_err "Failed to link .o files in ${EXEC_DIR}." diff --git a/tests/run-cn-exec.sh b/tests/run-cn-exec.sh index 1f7319fd6..903da7a57 100755 --- a/tests/run-cn-exec.sh +++ b/tests/run-cn-exec.sh @@ -17,7 +17,7 @@ CHECK_SCRIPT="${RUNTIME_PREFIX}/libexec/cn-runtime-single-file.sh" [ -f "${CHECK_SCRIPT}" ] || echo_and_err "Could not find single file helper script: ${CHECK_SCRIPT}" -SCRIPT_OPT="-q" +SCRIPT_OPT="-qu" function exits_with_code() { local file=$1 diff --git a/tests/run-cn-test-gen.sh b/tests/run-cn-test-gen.sh index 2ab15f444..a7753b316 100755 --- a/tests/run-cn-test-gen.sh +++ b/tests/run-cn-test-gen.sh @@ -12,6 +12,9 @@ cd "$DIRNAME"/cn-test-gen || exit rm -rf build decorated test mkdir build decorated test +# For UBSan +export UBSAN_OPTIONS=halt_on_error=1 + # Get `*.c` files FILES=$(find "$DIRNAME"/src -name '*.c')