diff options
Diffstat (limited to 'src/jib/jib_smt.ml')
| -rw-r--r-- | src/jib/jib_smt.ml | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 310a38a5..26509a69 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -345,7 +345,7 @@ let rec smt_cval ctx cval = | _ -> match cval with | V_lit (vl, ctyp) -> smt_value ctx vl ctyp - | V_id (Name (id, _) as ssa_id, _) -> + | V_id ((Name (id, _) | Global (id, _)) as ssa_id, _) -> begin match Type_check.Env.lookup_id id ctx.tc_env with | Enum _ -> Enum (zencode_id id) | _ when Bindings.mem id ctx.shared -> Shared (zencode_id id) @@ -1405,8 +1405,8 @@ let rec generate_ctype_defs ctx = function | [] -> [] let rec generate_reg_decs ctx inits = function - | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits)-> - Declare_const (zencode_name (Name (id, 0)), smt_ctyp ctx ctyp) + | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Global (id, 0)) inits)-> + Declare_const (zencode_name (Global (id, 0)), smt_ctyp ctx ctyp) :: generate_reg_decs ctx inits cdefs | _ :: cdefs -> generate_reg_decs ctx inits cdefs | [] -> [] @@ -1418,7 +1418,7 @@ let rec generate_reg_decs ctx inits = function let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) -module SMT_config : Jib_compile.Config = struct +module SMT_config(Opts : sig val unroll_limit : int end) : Jib_compile.Config = struct open Jib_compile (** Convert a sail type into a C-type. This function can be quite @@ -1581,9 +1581,11 @@ let unroll_static_foreach ctx = function let specialize_calls = true let ignore_64 = true - let unroll_loops () = Some !opt_unroll_limit + let unroll_loops = Some Opts.unroll_limit let struct_value = true let use_real = true + let branch_coverage = false + let track_throw = false end @@ -1897,7 +1899,7 @@ let smt_instr ctx = | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> begin match id, cval with - | Name (id, _), _ when IdSet.mem id ctx.preserved -> + | (Name (id, _) | Global (id, _)), _ when IdSet.mem id ctx.preserved -> [preserve_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] | _, V_lit (VL_undefined, _) -> @@ -1959,7 +1961,7 @@ let rec find_function lets id = function | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 -> lets, Some (heap_return, args, body) | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in find_function (lets @ vars @ setup) id cdefs; | _ :: cdefs -> find_function lets id cdefs @@ -2145,7 +2147,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_write_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - ifuncall (CL_id (name r, reg_ctyp)) function_id args; + ifuncall (CL_id (global r, reg_ctyp)) function_id args; igoto end_label; ilabel next_label] in @@ -2169,7 +2171,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_deref_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label; - icopy l clexp (V_id (name r, reg_ctyp)); + icopy l clexp (V_id (global r, reg_ctyp)); igoto end_label; ilabel next_label] in @@ -2191,7 +2193,7 @@ let expand_reg_deref env register_map = function let try_reg r = let next_label = label "next_reg_write_" in [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label; - icopy l (CL_id (name r, reg_ctyp)) cval; + icopy l (CL_id (global r, reg_ctyp)) cval; igoto end_label; ilabel next_label] in @@ -2325,7 +2327,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function let rec smt_cdefs props lets name_file ctx ast = function | CDEF_let (_, vars, setup) :: cdefs -> - let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in + let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs; | cdef :: cdefs -> smt_cdef props lets name_file ctx ast cdef; @@ -2351,7 +2353,7 @@ let rec build_register_map rmap = function let compile env ast = let cdefs, jib_ctx = - let module Jibc = Jib_compile.Make(SMT_config) in + let module Jibc = Jib_compile.Make(SMT_config(struct let unroll_limit = !opt_unroll_limit end)) in let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in let t = Profile.start () in let cdefs, ctx = Jibc.compile_ast ctx ast in |