From 673046692bac0d7880cd5f632eebf2d44e399119 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 4 Sep 2024 16:06:30 +0100 Subject: [PATCH] SMT/SV: Add more simplifications for union types Add simplification for pure matches in Sail->SMT Make counterexample checking stricter --- lib/sv/sail_modules.sv | 8 ++ src/lib/jib_compile.ml | 109 ++++++++++++++++++++++---- src/lib/jib_compile.mli | 26 ++++-- src/lib/smt_exp.ml | 20 ++++- src/lib/smt_gen.ml | 2 +- src/lib/value.ml | 1 + src/sail_c_backend/c_backend.ml | 1 + src/sail_smt_backend/jib_smt.ml | 12 +-- src/sail_sv_backend/sail_plugin_sv.ml | 1 + test/c/spc_mappings.sail | 23 +++--- 10 files changed, 156 insertions(+), 47 deletions(-) diff --git a/lib/sv/sail_modules.sv b/lib/sv/sail_modules.sv index dbffa2be4..7b0bde866 100644 --- a/lib/sv/sail_modules.sv +++ b/lib/sv/sail_modules.sv @@ -72,4 +72,12 @@ function automatic string string_take(string str, int n); return str.substr(0, n - 1); endfunction // string_take +function automatic string string_drop(string str, int n); + return str.substr(n, str.len() - 1); +endfunction // string_drop + +function automatic logic [127:0] string_length(string str); + return {96'h0, str.len()}; +endfunction // string_length + `endif diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 6d1d19c60..90179fe00 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -178,6 +178,19 @@ let ctx_get_extern id ctx = let ctx_has_val_spec id ctx = Bindings.mem id ctx.valspecs || Bindings.mem id (Env.get_val_specs ctx.tc_env) +let rec is_pure_aexp ctx (AE_aux (aexp, { uannot; _ })) = + match get_attribute "anf_pure" uannot with + | Some _ -> true + | None -> ( + match aexp with + | AE_app (f, _, _) -> Effects.function_is_pure f ctx.effect_info + | AE_let (Immutable, _, _, aexp1, aexp2, _) -> is_pure_aexp ctx aexp1 && is_pure_aexp ctx aexp2 + | AE_val _ -> true + | _ -> false + ) + +let is_pure_case ctx (_, guard, body) = is_pure_aexp ctx guard && is_pure_aexp ctx body + let initial_ctx ?for_target env effect_info = let initial_valspecs = [ @@ -274,6 +287,7 @@ module type CONFIG = sig val branch_coverage : out_channel option val track_throw : bool val use_void : bool + val eager_control_flow : bool end module IdGraph = Graph.Make (Id) @@ -642,7 +656,7 @@ module Make (C : CONFIG) = struct | AP_as (_, _, typ) -> ctyp_of_typ ctx typ | AP_struct (_, typ) -> ctyp_of_typ ctx typ - let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = + let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval on_failure = let ctx = { ctx with local_env = env } in let ctyp = cval_ctyp cval in match apat_aux with @@ -652,7 +666,7 @@ module Make (C : CONFIG) = struct | AP_id (pid, _) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with | Unbound _ -> ([], [idecl l ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx) - | _ -> ([ijump l (V_call (Neq, [V_member (pid, ctyp); cval])) case_label], [], [], ctx) + | _ -> ([on_failure l (V_call (Neq, [V_member (pid, ctyp); cval]))], [], [], ctx) end | AP_id (pid, typ) -> let id_ctyp = ctyp_of_typ ctx typ in @@ -660,7 +674,7 @@ module Make (C : CONFIG) = struct ([], [idecl l id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx) | AP_as (apat, id, typ) -> let id_ctyp = ctyp_of_typ ctx typ in - let pre, instrs, cleanup, ctx = compile_match ctx apat cval case_label in + let pre, instrs, cleanup, ctx = compile_match ctx apat cval on_failure in let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in ( pre, instrs @ [idecl l id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], @@ -669,7 +683,7 @@ module Make (C : CONFIG) = struct ) | AP_struct (afpats, _) -> begin let fold (pre, instrs, cleanup, ctx) (field, apat) = - let pre', instrs', cleanup', ctx = compile_match ctx apat (V_field (cval, field)) case_label in + let pre', instrs', cleanup', ctx = compile_match ctx apat (V_field (cval, field)) on_failure in (pre @ pre', instrs @ instrs', cleanup' @ cleanup, ctx) in let pre, instrs, cleanup, ctx = List.fold_left fold ([], [], [], ctx) afpats in @@ -678,7 +692,7 @@ module Make (C : CONFIG) = struct | AP_tuple apats -> begin let get_tup n = V_tuple_member (cval, List.length apats, n) in let fold (pre, instrs, cleanup, n, ctx) apat ctyp = - let pre', instrs', cleanup', ctx = compile_match ctx apat (get_tup n) case_label in + let pre', instrs', cleanup', ctx = compile_match ctx apat (get_tup n) on_failure in (pre @ pre', instrs @ instrs', cleanup' @ cleanup, n + 1, ctx) in match ctyp with @@ -718,9 +732,9 @@ module Make (C : CONFIG) = struct end in let pre, instrs, cleanup, ctx = - compile_match ctx apat (V_ctor_unwrap (cval, (ctor, unifiers), ctor_ctyp)) case_label + compile_match ctx apat (V_ctor_unwrap (cval, (ctor, unifiers), ctor_ctyp)) on_failure in - ([ijump l (V_ctor_kind (cval, (ctor, unifiers), pat_ctyp)) case_label] @ pre, instrs, cleanup, ctx) + ([on_failure l (V_ctor_kind (cval, (ctor, unifiers), pat_ctyp))] @ pre, instrs, cleanup, ctx) | ctyp -> raise (Reporting.err_general l @@ -733,16 +747,16 @@ module Make (C : CONFIG) = struct | AP_cons (hd_apat, tl_apat) -> begin match ctyp with | CT_list ctyp -> - let hd_pre, hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in - let tl_pre, tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in - ( [ijump l (V_call (List_is_empty, [cval])) case_label] @ hd_pre @ tl_pre, + let hd_pre, hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) on_failure in + let tl_pre, tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) on_failure in + ( [on_failure l (V_call (List_is_empty, [cval]))] @ hd_pre @ tl_pre, hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx ) | _ -> raise (Reporting.err_general l "Tried to pattern match cons on non list type") end - | AP_nil _ -> ([ijump l (V_call (Bnot, [V_call (List_is_empty, [cval])])) case_label], [], [], ctx) + | AP_nil _ -> ([on_failure l (V_call (Bnot, [V_call (List_is_empty, [cval])]))], [], [], ctx) let unit_cval = V_lit (VL_unit, CT_unit) @@ -775,6 +789,63 @@ module Make (C : CONFIG) = struct let setup, cval, cleanup = compile_aval l ctx aval in (setup, (fun clexp -> icopy l clexp cval), cleanup) (* Compile case statements *) + | AE_match (aval, cases, typ) + when C.eager_control_flow + && Option.is_some (get_attribute "complete" uannot) + && List.for_all (is_pure_case ctx) cases -> + let ctyp = ctyp_of_typ ctx typ in + let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + let compile_case case_match_id case_return_id (apat, guard, body) = + let trivial_guard = + match guard with + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _) + | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _) -> + true + | _ -> false + in + let pre_destructure, destructure, destructure_cleanup, ctx = + compile_match ctx apat cval (fun l b -> icopy l (CL_id (case_match_id, CT_bool)) (V_call (Bnot, [b]))) + in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + [iinit l CT_bool case_match_id (V_lit (VL_bool true, CT_bool)); idecl l ctyp case_return_id] + @ pre_destructure @ destructure + @ ( if not trivial_guard then ( + let gs = ngensym () in + guard_setup + @ [idecl l CT_bool gs; guard_call (CL_id (gs, CT_bool))] + @ guard_cleanup + @ [ + iif l + (V_call (Bnot, [V_id (gs, CT_bool)])) + (destructure_cleanup @ [icopy l (CL_id (case_match_id, CT_bool)) (V_lit (VL_bool false, CT_bool))]) + [] CT_unit; + ] + ) + else [] + ) + @ body_setup + @ [body_call (CL_id (case_return_id, ctyp))] + @ body_cleanup @ destructure_cleanup + in + let case_ids, cases = + List.map + (fun case -> + let case_match_id = ngensym () in + let case_return_id = ngensym () in + ( (V_id (case_match_id, CT_bool), V_id (case_return_id, ctyp)), + compile_case case_match_id case_return_id case + ) + ) + cases + |> List.split + in + let rec build_ite = function + | [(_, ret)] -> ret + | (b, ret) :: rest -> V_call (Ite, [b; ret; build_ite rest]) + | [] -> Reporting.unreachable l __POS__ "Empty match found" + in + (aval_setup @ List.concat cases, (fun clexp -> icopy l clexp (build_ite case_ids)), aval_cleanup) | AE_match (aval, cases, typ) -> let ctx = update_coverage_override uannot ctx in let ctyp = ctyp_of_typ ctx typ in @@ -796,7 +867,9 @@ module Make (C : CONFIG) = struct true | _ -> false in - let pre_destructure, destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in + let pre_destructure, destructure, destructure_cleanup, ctx = + compile_match ctx apat cval (fun l b -> ijump l b case_label) + in let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = ngensym () in @@ -846,7 +919,9 @@ module Make (C : CONFIG) = struct in let try_label = label "try_" in let exn_cval = V_id (current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in - let pre_destructure, destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in + let pre_destructure, destructure, destructure_cleanup, ctx = + compile_match ctx apat exn_cval (fun l b -> ijump l b try_label) + in let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = ngensym () in @@ -1487,7 +1562,9 @@ module Make (C : CONFIG) = struct let ret_ctyp = ctyp_of_typ ctx ret_typ in (* Compile the function arguments as patterns. *) - let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in + let arg_setup, compiled_args, arg_cleanup = + compile_arg_pats ctx (fun l b -> ijump l b fundef_label) pat arg_ctyps + in let ctx = (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) List.fold_left2 @@ -1634,7 +1711,9 @@ module Make (C : CONFIG) = struct let apat = anf_pat ~global:true pat in let gs = ngensym () in let end_label = label "let_end_" in - let pre_destructure, destructure, destructure_cleanup, _ = compile_match ctx apat (V_id (gs, ctyp)) end_label in + let pre_destructure, destructure, destructure_cleanup, _ = + compile_match ctx apat (V_id (gs, ctyp)) (fun l b -> ijump l b end_label) + in let gs_setup, gs_cleanup = ([idecl (exp_loc exp) ctyp gs], [iclear ctyp gs]) in let bindings = List.map (fun (id, typ) -> (id, ctyp_of_typ ctx typ)) (apat_globals apat) in let n = !letdef_count in diff --git a/src/lib/jib_compile.mli b/src/lib/jib_compile.mli index ca6282858..08eb19235 100644 --- a/src/lib/jib_compile.mli +++ b/src/lib/jib_compile.mli @@ -116,6 +116,8 @@ val ctx_get_extern : id -> ctx -> string val ctx_has_val_spec : id -> ctx -> bool +val is_pure_aexp : ctx -> 'a aexp -> bool + (** Create an inital Jib compilation context. The target is the name that would appear in a valspec extern section, i.e. @@ -139,7 +141,7 @@ module type CONFIG = sig val optimize_anf : ctx -> typ aexp -> typ aexp (** Unroll all for loops a bounded number of times. Used for SMT - generation. *) + generation. *) val unroll_loops : int option (** A call is precise if the function arguments match the function @@ -148,8 +150,8 @@ module type CONFIG = sig val make_call_precise : ctx -> id -> ctyp list -> ctyp -> bool (** If false, will ensure that fixed size bitvectors are - specifically less that 64-bits. If true this restriction will - be ignored. *) + specifically less that 64-bits. If true this restriction will + be ignored. *) val ignore_64 : bool (** If false we won't generate any V_struct values *) @@ -165,11 +167,25 @@ module type CONFIG = sig val branch_coverage : out_channel option (** If true track the location of the last exception thrown, useful - for debugging C but we want to turn it off for SMT generation - where we can't use strings *) + for debugging C but we want to turn it off for SMT generation + where we can't use strings *) val track_throw : bool val use_void : bool + + (** Convert control flow where all branches are pure into, into eager variants, i.e. + + let x = if b else y then z + + becomes + + let x = eager_if(b, y, z) + + so `y` and `z` are eagerly evaluated before the if-statement + which just becomes like a function call. Reducing the + control-flow like this is useful for the Sail->SV and Sail->SMT + backends. *) + val eager_control_flow : bool end module IdGraph : sig diff --git a/src/lib/smt_exp.ml b/src/lib/smt_exp.ml index 2e748eb3a..5db6f4a29 100644 --- a/src/lib/smt_exp.ml +++ b/src/lib/smt_exp.ml @@ -329,6 +329,7 @@ let rec identical x y = | Var x, Var y -> Name.compare x y = 0 | Fn (f1, args1), Fn (f2, args2) -> String.compare f1 f2 = 0 && List.compare_lengths args1 args2 = 0 && List.for_all2 identical args1 args2 + | Tester (sx, x), Tester (sy, y) -> String.compare sx sy = 0 && identical x y | _ -> false let simp_eq x y = @@ -733,6 +734,12 @@ module Simplifier = struct match SimpSet.find_opt v simpset with Some exp -> change exp | None -> NoChange ) | _ -> NoChange + let rule_tester = + mk_rule __LOC__ @@ fun simpset -> function + | Tester (ctor, Var v) -> ( + match SimpSet.is_ctor v ctor simpset with Some b -> change (Bool_lit b) | _ -> NoChange + ) | _ -> NoChange + let rule_access_ite = mk_simple_rule __LOC__ @@ function | Field (struct_id, field, Ite (i, t, e)) -> @@ -928,7 +935,7 @@ let simp simpset exp = | Extract _ -> run_strategy simpset exp rule_extract | Field _ -> run_strategy simpset exp rule_access_ite | Unwrap _ -> run_strategy simpset exp rule_access_ite - | Tester _ -> run_strategy simpset exp rule_access_ite + | Tester _ -> run_strategy simpset exp (Then [rule_tester; rule_access_ite]) | exp -> NoChange in let rec go exp = @@ -1116,10 +1123,10 @@ module Counterexample (Config : COUNTEREXAMPLE_CONFIG) = struct let rec run frame = match frame with - | Interpreter.Done (state, v) -> Some v + | Interpreter.Done (state, v) -> Result.Ok v | Interpreter.Step (lazy_str, _, _, _) -> run (Interpreter.eval_frame frame) | Interpreter.Break frame -> run (Interpreter.eval_frame frame) - | Interpreter.Fail (_, _, _, _, msg) -> None + | Interpreter.Fail (_, _, _, _, msg) -> Result.Error msg | Interpreter.Effect_request (out, state, stack, eff) -> run (Interpreter.default_effect_interp state eff) let check ~env ~ast ~solver ~file_name ~function_id ~args ~arg_ctyps ~arg_smt_names = @@ -1160,8 +1167,13 @@ module Counterexample (Config : COUNTEREXAMPLE_CONFIG) = struct let result = run (Step (lazy "", istate, return call, [])) in begin match result with - | Some (V_bool false) | None -> + | Result.Ok (V_bool false) | Result.Ok V_unit -> ksprintf print_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear) + | Result.Ok (V_bool true) -> + ksprintf print_endline "Failed to replay counterexample: %s\n Function returned true" + Util.("error" |> red |> clear) + | Result.Error msg -> + ksprintf print_endline "Failed to replay counterexample: %s\n %s" Util.("error" |> red |> clear) msg | _ -> () end | Some (Atom "unsat" :: _) -> diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml index 7fb960a3b..45a0a3de2 100644 --- a/src/lib/smt_gen.ml +++ b/src/lib/smt_gen.ml @@ -349,7 +349,7 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct | Bvadd, args -> Fn ("bvadd", args) | Bvsub, args -> Fn ("bvsub", args) | Concat, args -> Fn ("concat", args) - | Ite, args -> Fn ("ite", args) + | Ite, [i; t; e] -> Ite (i, t, e) | Zero_extend _, _ -> failwith "ZE" | Sign_extend _, _ -> failwith "SE" | Slice _, _ -> failwith "slice" diff --git a/src/lib/value.ml b/src/lib/value.ml index 767b03277..fef41b488 100644 --- a/src/lib/value.ml +++ b/src/lib/value.ml @@ -792,6 +792,7 @@ let primops = ("trace_memory_read", fun _ -> V_unit); ("trace_memory_write", fun _ -> V_unit); ("get_time_ns", fun _ -> V_int (Sail_lib.get_time_ns ())); + ("sail_assume", fun _ -> V_unit); ("load_raw", value_load_raw); ("to_real", value_to_real); ("eq_real", value_eq_real); diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 6cc18ff27..179f3e00e 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -594,6 +594,7 @@ end) : CONFIG = struct let branch_coverage = Opts.branch_coverage let track_throw = true let use_void = false + let eager_control_flow = false end (** Functions that have heap-allocated return types are implemented by diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 2f038646a..904454e0b 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -1202,17 +1202,6 @@ end) : Jib_compile.CONFIG = struct end | aexp -> aexp - let rec is_pure_aexp ctx (AE_aux (aexp, { uannot; _ })) = - match get_attribute "anf_pure" uannot with - | Some _ -> true - | None -> ( - match aexp with - | AE_app (f, _, _) -> Effects.function_is_pure f ctx.effect_info - | AE_let (Immutable, _, _, aexp1, aexp2, _) -> is_pure_aexp ctx aexp1 && is_pure_aexp ctx aexp2 - | AE_val _ -> true - | _ -> false - ) - (* Map over all the functions in an aexp. *) let rec analyze ctx (AE_aux (aexp, ({ env; uannot; loc } as annot))) = let ctx = { ctx with local_env = env } in @@ -1290,6 +1279,7 @@ end) : Jib_compile.CONFIG = struct let branch_coverage = None let track_throw = false let use_void = false + let eager_control_flow = true end (* In order to support register references, we need to build a map diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index c138addc6..7f6ccc901 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -326,6 +326,7 @@ module Verilog_config (C : JIB_CONFIG) : Jib_compile.CONFIG = struct let branch_coverage = None let use_real = false let use_void = false + let eager_control_flow = false end let register_types cdefs = diff --git a/test/c/spc_mappings.sail b/test/c/spc_mappings.sail index febaf77e2..65bac5ac3 100644 --- a/test/c/spc_mappings.sail +++ b/test/c/spc_mappings.sail @@ -7,48 +7,49 @@ infixl 5 ++ overload operator ++ = concat_str +$[jib_debug] function main() -> unit = { match " " { spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 1"), }; match "" { - spc() => print_endline("fail"), + spc() => print_endline("fail 2"), _ => print_endline("ok"), }; match " not spaces" { - spc() => print_endline("fail"), + spc() => print_endline("fail 3"), _ => print_endline("ok"), }; match " " { spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 4"), }; match " " { opt_spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 5"), }; match "" { opt_spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 6"), }; match " " { opt_spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 7"), }; match " " { def_spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 8"), }; match "" { def_spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 9"), }; match " " { def_spc() => print_endline("ok"), - _ => print_endline("fail"), + _ => print_endline("fail 10"), }; match ((), (), ()) { @@ -57,6 +58,6 @@ function main() -> unit = { print_endline(">" ++ s2 ++ "<"); print_endline(">" ++ s3 ++ "<"); }, - _ => print_endline("fail"), + _ => print_endline("fail 11"), } }