diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/jib_smt.ml | 39 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 20 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 4 |
3 files changed, 55 insertions, 8 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 086d4d11..350f50d9 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -67,6 +67,8 @@ let opt_ignore_overflow = ref false let opt_auto = ref false +let opt_debug_graphs = ref false + module EventMap = Map.Make(Event) (* Note that we have to use x : ty ref rather than mutable x : ty, to @@ -278,6 +280,10 @@ let rec smt_cval ctx cval = Fn ("=", [smt_cval ctx cval; Bin "1"]) | V_call (Bnot, [cval]) -> Fn ("not", [smt_cval ctx cval]) + | V_call (Band, cvals) -> + Fn ("and", List.map (smt_cval ctx) cvals) + | V_call (Bor, cvals) -> + Fn ("or", List.map (smt_cval ctx) cvals) | V_ctor_kind (union, ctor_id, unifiers, _) -> Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)]) | V_ctor_unwrap (ctor_id, union, unifiers, _) -> @@ -322,6 +328,9 @@ let add_event ctx ev smt = let stack = event_stack ctx ev in Stack.push (Fn ("=>", [ctx.pathcond; smt])) stack +let add_pathcond_event ctx ev = + Stack.push ctx.pathcond (event_stack ctx ev) + let overflow_check ctx smt = if not !opt_ignore_overflow then ( Util.warn "Adding overflow check in generated SMT"; @@ -903,6 +912,16 @@ let builtin_compare_bits fn ctx v1 v2 ret_ctyp = | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp) +(* ***** String operations: lib/real.sail ***** *) + +let builtin_decimal_string_of_bits ctx v = + begin match cval_ctyp v with + | CT_fbits (n, _) -> + Fn ("int.to.str", [Fn ("bv2nat", [smt_cval ctx v])]) + + | _ -> builtin_type_error ctx "decimal_string_of_bits" [v] None + end + (* ***** Real number operations: lib/real.sail ***** *) let builtin_sqrt_real ctx root v = @@ -986,6 +1005,7 @@ let smt_builtin ctx name args 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]) + | "decimal_string_of_bits", [v], CT_string -> ctx.use_string := true; builtin_decimal_string_of_bits ctx v (* lib/real.sail *) (* Note that sqrt_real is special and is handled by smt_instr. *) @@ -1408,7 +1428,7 @@ let smt_instr ctx = | I_aux (I_clear _, _) -> [] | I_aux (I_match_failure, _) -> - add_event ctx Match (Bool_lit false); + add_pathcond_event ctx Match; [] | I_aux (I_undefined ctyp, _) -> [] @@ -1606,6 +1626,12 @@ let rec smt_query ctx = function | Q_or qs -> Fn ("or", List.map (smt_query ctx) qs) +let dump_graph function_id cfg = + let gv_file = string_of_id function_id ^ ".gv" in + let out_chan = open_out gv_file in + Jib_ssa.make_dot out_chan cfg; + close_out out_chan + let smt_cdef props lets name_file ctx all_cdefs = function | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props -> begin match find_function [] function_id all_cdefs with @@ -1641,14 +1667,13 @@ let smt_cdef props lets name_file ctx all_cdefs = function let visit_order = try topsort cfg with | Not_a_DAG n -> - let gv_file = string_of_id function_id ^ ".gv" in - let out_chan = open_out gv_file in - make_dot out_chan cfg; - close_out out_chan; + dump_graph function_id cfg; raise (Reporting.err_general pragma_l - (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s" - prop_type (string_of_id function_id) n gv_file)) + (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv" + prop_type (string_of_id function_id) n (string_of_id function_id))) in + if !opt_debug_graphs then + dump_graph function_id cfg; List.iter (fun n -> begin match get_vertex cfg n with diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index 9a9a3361..a4a77f9d 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -619,15 +619,33 @@ let place_pi_functions graph start idom children = List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes) in + let rec between_dom p n = + if n = p then + [] + else + match graph.nodes.(n) with + | Some ((_, cfnode), preds, _) -> + let preds = List.concat (List.map (between_dom p) (IntSet.elements preds)) in + begin match get_guard cfnode, preds with + | [guard], [pred] -> [V_call (Band, [guard; pred])] + | [guard], [] -> [guard] + | [guard], _ -> [V_call (Band, [guard; V_call (Bor, preds)])] + | _, (_ :: _ :: _ as preds) -> [V_call (Bor, preds)] + | _, pred -> pred + end + | None -> assert false + in + let rec go n = begin match graph.nodes.(n) with | Some ((ssa, cfnode), preds, succs) -> let p = idom.(n) in + let bd = between_dom p n in if p <> -1 then begin match graph.nodes.(p) with | Some ((dom_ssa, _), _, _) -> let args = get_guard cfnode @ get_pi_contents dom_ssa in - graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs) + graph.nodes.(n) <- Some ((Pi (bd @ args) :: ssa, cfnode), preds, succs) | None -> assert false end | None -> assert false diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 378f5fae..3326d4ad 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -278,6 +278,8 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) = let string_of_op = function | Bnot -> "@not" + | Band -> "@and" + | Bor -> "@or" | List_hd -> "@hd" | List_tl -> "@tl" | Bit_to_bool -> "@bit_to_bool" @@ -896,6 +898,8 @@ let rec infer_call op vs = match op, vs with | Bit_to_bool, _ -> CT_bool | Bnot, _ -> CT_bool + | Band, _ -> CT_bool + | Bor, _ -> CT_bool | List_hd, [v] -> begin match cval_ctyp v with | CT_list ctyp -> ctyp |