diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_compile.ml | 17 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 4 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 77 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 17 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 1 | ||||
| -rw-r--r-- | src/smtlib.ml | 10 | ||||
| -rw-r--r-- | src/value2.lem | 1 |
7 files changed, 98 insertions, 29 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index ad60d224..f8cb3bcd 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -160,7 +160,8 @@ type ctx = optimize_anf : ctx -> typ aexp -> typ aexp; specialize_calls : bool; ignore_64 : bool; - struct_value : bool + struct_value : bool; + use_real : bool; } let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env = @@ -176,7 +177,8 @@ let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env = optimize_anf = optimize_anf; specialize_calls = false; ignore_64 = false; - struct_value = false + struct_value = false; + use_real = false; } let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ @@ -232,10 +234,13 @@ let rec compile_aval l ctx = function | AV_lit (L_aux (L_false, _), _) -> [], V_lit (VL_bool false, CT_bool), [] | AV_lit (L_aux (L_real str, _), _) -> - let gs = ngensym () in - [iinit CT_real gs (V_lit (VL_string str, CT_string))], - V_id (gs, CT_real), - [iclear CT_real gs] + if ctx.use_real then + [], V_lit (VL_real str, CT_real), [] + else + let gs = ngensym () in + [iinit CT_real gs (V_lit (VL_string str, CT_string))], + V_id (gs, CT_real), + [iclear CT_real gs] | AV_lit (L_aux (L_unit, _), _) -> [], V_lit (VL_unit, CT_unit), [] diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index b882f2f9..70a0b322 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -96,7 +96,9 @@ type ctx = be ignored. *) ignore_64 : bool; (** If false (default) we won't generate any V_struct values *) - struct_value : bool + struct_value : bool; + (** Allow real literals *) + use_real : bool; } val initial_ctx : diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 99938365..c03b8934 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -92,6 +92,9 @@ type ctx = { the global path conditional of the containing block in the control flow graph *) pathcond : smt_exp; + (* Set if we need to use strings *) + use_string : bool ref; + use_real : bool ref } (* These give the default bounds for various SMT types, stored in the @@ -114,6 +117,8 @@ let initial_ctx () = { ast = Defs []; events = ref EventMap.empty; pathcond = Bool_lit true; + use_string = ref false; + use_real = ref false; } let event_stack ctx ev = @@ -162,7 +167,12 @@ let rec smt_ctyp ctx = function ctx.tuple_sizes := IntSet.add (List.length ctyps) !(ctx.tuple_sizes); Tuple (List.map (smt_ctyp ctx) ctyps) | CT_vector (_, ctyp) -> Array (Bitvec !vector_index, smt_ctyp ctx ctyp) - | CT_string -> Bitvec 64 + | CT_string -> + ctx.use_string := true; + String + | CT_real -> + ctx.use_real := true; + Real | CT_ref ctyp -> begin match CTMap.find_opt ctyp ctx.register_map with | Some regs -> Bitvec (required_width (Big_int.of_int (List.length regs))) @@ -231,8 +241,16 @@ let smt_value ctx vl ctyp = | VL_bit Sail2_values.B0, CT_bit -> Bin "0" | VL_bit Sail2_values.B1, CT_bit -> Bin "1" | VL_unit, _ -> Var "unit" - | VL_string _, _ -> Var "unit" (* FIXME: String support *) - | vl, _ -> failwith ("Cannot translate literal to SMT " ^ string_of_value vl) + | VL_string str, _ -> + ctx.use_string := true; + String_lit (String.escaped str) + | VL_real str, _ -> + ctx.use_real := true; + if str.[0] = '-' then + Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))]) + else + Real_lit str + | vl, _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl) let zencode_ctor ctor_id unifiers = match unifiers with @@ -883,9 +901,18 @@ let builtin_compare_bits fn ctx v1 v2 ret_ctyp = | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp) +(* ***** Real number operations: lib/real.sail ***** *) + +let builtin_sqrt_real ctx root v = + ctx.use_real := true; + let smt = smt_cval ctx v in + [Declare_const (root, Real); + Assert (Fn ("and", [Fn ("=", [smt; Fn ("*", [Var root; Var root])]); + Fn (">=", [Var root; Real_lit "0.0"])]))] + let smt_builtin ctx name args ret_ctyp = match name, args, ret_ctyp with - | "eq_bits", [v1; v2], _ -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) + | "eq_bits", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) | "eq_anything", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) (* lib/flow.sail *) @@ -954,6 +981,23 @@ let smt_builtin ctx name args ret_ctyp = | "get_slice_int", [v1; v2; v3], ret_ctyp -> builtin_get_slice_int ctx v1 v2 v3 ret_ctyp | "set_slice", [v1; v2; v3; v4; v5], ret_ctyp -> builtin_set_slice_bits ctx v1 v2 v3 v4 v5 ret_ctyp + (* string builtins *) + | "concat_str", [v1; v2], CT_string -> ctx.use_string := true; Fn ("str.++", [smt_cval ctx v1; smt_cval ctx v2]) + | "eq_string", [v1; v2], CT_bool -> ctx.use_string := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) + + (* lib/real.sail *) + (* Note that sqrt_real is special and is handled by smt_instr. *) + | "eq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2]) + | "neg_real", [v], CT_real -> ctx.use_real := true; Fn ("-", [smt_cval ctx v]) + | "add_real", [v1; v2], CT_real -> ctx.use_real := true; Fn ("+", [smt_cval ctx v1; smt_cval ctx v2]) + | "sub_real", [v1; v2], CT_real -> ctx.use_real := true; Fn ("-", [smt_cval ctx v1; smt_cval ctx v2]) + | "mult_real", [v1; v2], CT_real -> ctx.use_real := true; Fn ("*", [smt_cval ctx v1; smt_cval ctx v2]) + | "div_real", [v1; v2], CT_real -> ctx.use_real := true; Fn ("/", [smt_cval ctx v1; smt_cval ctx v2]) + | "lt_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<", [smt_cval ctx v1; smt_cval ctx v2]) + | "gt_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn (">", [smt_cval ctx v1; smt_cval ctx v2]) + | "lteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<=", [smt_cval ctx v1; smt_cval ctx v2]) + | "gteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn (">=", [smt_cval ctx v1; smt_cval ctx v2]) + | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp) let rec smt_conversion ctx from_ctyp to_ctyp x = @@ -1288,8 +1332,15 @@ let smt_instr ctx = | I_aux (I_funcall (CL_id (id, ret_ctyp), extern, function_id, args), (_, l)) -> if Env.is_extern function_id ctx.tc_env "c" && not extern then let name = Env.get_extern function_id ctx.tc_env "c" in - let value = smt_builtin ctx name args ret_ctyp in - [define_const ctx id ret_ctyp value] + if name = "sqrt_real" then + begin match args with + | [v] -> builtin_sqrt_real ctx (zencode_name id) v + | _ -> + Reporting.unreachable l __POS__ "Bad arguments for sqrt_real" + end + else + let value = smt_builtin ctx name args ret_ctyp in + [define_const ctx id ret_ctyp value] else if extern && string_of_id function_id = "internal_vector_init" then [declare_const ctx id ret_ctyp] else if extern && string_of_id function_id = "internal_vector_update" then @@ -1360,6 +1411,10 @@ let smt_instr ctx = | I_aux (I_undefined ctyp, _) -> [] + (* I_jump and I_goto will only appear as terminators for basic blocks. *) + | I_aux ((I_jump _ | I_goto _), _) -> [] + + | instr -> failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr)) @@ -1404,7 +1459,7 @@ let optimize_smt stack = | Some n -> Hashtbl.replace uses var (n + 1) | None -> Hashtbl.add uses var 1 end - | Hex _ | Bin _ | Bool_lit _ -> () + | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () | Fn (f, exps) -> List.iter uses_in_exp exps | Ite (cond, t, e) -> @@ -1613,7 +1668,11 @@ let smt_cdef props lets name_file ctx all_cdefs = function let out_chan = open_out fname in if prop_type = "counterexample" then output_string out_chan "(set-option :produce-models true)\n"; - output_string out_chan "(set-logic QF_AUFBVDT)\n"; + + if !(ctx.use_string) || !(ctx.use_real) then + output_string out_chan "(set-logic ALL)\n" + else + output_string out_chan "(set-logic QF_AUFBVDT)\n"; List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") (smt_header ctx all_cdefs); @@ -1679,7 +1738,7 @@ let generate_smt props name_file env ast = env in let t = Profile.start () in - let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true } ast in + let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true; use_real = true } ast in Profile.finish "Compiling to Jib IR" t; cdefs in diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index c8027ee5..9a9a3361 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -125,7 +125,7 @@ let reachable roots graph = IntSet.iter reachable' roots; !visited exception Not_a_DAG of int;; - + let topsort graph = let marked = ref IntSet.empty in let temp_marked = ref IntSet.empty in @@ -193,6 +193,7 @@ type cf_node = | CF_guard of cval | CF_start of ctyp NameMap.t +(* For now we only generate CFGs for flat lists of instructions *) let control_flow_graph instrs = let module StringMap = Map.Make(String) in let labels = ref StringMap.empty in @@ -215,7 +216,7 @@ let control_flow_graph instrs = let rec cfg preds instrs = let before, after = instr_split_at cf_split instrs in let last = match after with - | I_aux ((I_label _ | I_goto _ | I_jump _), _) :: _ -> [] + | I_aux (I_label _, _) :: _ -> [] | instr :: _ -> [instr] | _ -> [] in @@ -227,11 +228,6 @@ let control_flow_graph instrs = [n] in match after with - | I_aux (I_if (cond, then_instrs, else_instrs, _), _) :: after -> - let t = cfg preds then_instrs in - let e = cfg preds else_instrs in - cfg (t @ e) after - | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after -> cfg [] after @@ -249,11 +245,8 @@ let control_flow_graph instrs = | I_aux (I_label label, _) :: after -> cfg (StringMap.find label !labels :: preds) after - | I_aux (I_block instrs, _) :: after -> - let m = cfg preds instrs in - cfg m after - - | _ :: after -> assert false + | I_aux (_, (_, l)) :: after -> + Reporting.unreachable l __POS__ "Could not add instruction to control-flow graph" | [] -> preds in diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index c98c325c..378f5fae 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -259,6 +259,7 @@ let string_of_value = function | VL_bit Sail2_values.B0 -> "UINT64_C(0)" | VL_bit Sail2_values.B1 -> "UINT64_C(1)" | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value" + | VL_real str -> str | VL_string str -> "\"" ^ str ^ "\"" let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) = diff --git a/src/smtlib.ml b/src/smtlib.ml index 72421b8a..7f485447 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -54,6 +54,8 @@ open Ast_util type smt_typ = | Bitvec of int | Bool + | String + | Real | Datatype of string * (string * (string * smt_typ) list) list | Tuple of smt_typ list | Array of smt_typ * smt_typ @@ -89,6 +91,8 @@ type smt_exp = | Bool_lit of bool | Hex of string | Bin of string + | Real_lit of string + | String_lit of string | Var of string | Fn of string * smt_exp list | Ite of smt_exp * smt_exp * smt_exp @@ -145,7 +149,7 @@ let rec simp_smt_exp vars = function | Some exp -> simp_smt_exp vars exp | None -> Var v end - | (Hex _ | Bin _ | Bool_lit _ as exp) -> exp + | (Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp | Fn (f, exps) -> let exps = List.map (simp_smt_exp vars) exps in simp_fn (Fn (f, exps)) @@ -184,6 +188,8 @@ let rec pp_smt_exp = let open PPrint in function | Bool_lit b -> string (string_of_bool b) + | Real_lit str -> string str + | String_lit str -> string ("\"" ^ str ^ "\"") | Hex str -> string ("#x" ^ str) | Bin str -> string ("#b" ^ str) | Var str -> string str @@ -201,6 +207,8 @@ let rec pp_smt_typ = let open PPrint in function | Bool -> string "Bool" + | String -> string "String" + | Real -> string "Real" | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n) | Datatype (name, _) -> string name | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys) diff --git a/src/value2.lem b/src/value2.lem index 0e65e91f..0afaa2d1 100644 --- a/src/value2.lem +++ b/src/value2.lem @@ -59,4 +59,5 @@ type vl = | VL_unit | VL_int of integer | VL_string of string + | VL_real of string | VL_null (* Used for unitialized values and null pointers in C compilation *) |