summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/jib/jib_smt.ml56
-rw-r--r--src/jib/jib_ssa.ml27
-rw-r--r--src/jib/jib_ssa.mli2
-rw-r--r--src/smtlib.ml10
4 files changed, 48 insertions, 47 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index de5feca1..3b42e749 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -93,7 +93,7 @@ type ctx = {
(* When generating SMT for an instruction pathcond will contain
the global path conditional of the containing block in the
control flow graph *)
- pathcond : smt_exp;
+ pathcond : smt_exp Lazy.t;
(* Set if we need to use strings *)
use_string : bool ref;
use_real : bool ref
@@ -118,7 +118,7 @@ let initial_ctx () = {
arg_stack = Stack.create ();
ast = Defs [];
events = ref EventMap.empty;
- pathcond = Bool_lit true;
+ pathcond = lazy (Bool_lit true);
use_string = ref false;
use_real = ref false;
}
@@ -281,9 +281,9 @@ let rec smt_cval ctx cval =
| V_call (Bnot, [cval]) ->
Fn ("not", [smt_cval ctx cval])
| V_call (Band, cvals) ->
- Fn ("and", List.map (smt_cval ctx) cvals)
+ smt_conj (List.map (smt_cval ctx) cvals)
| V_call (Bor, cvals) ->
- Fn ("or", List.map (smt_cval ctx) cvals)
+ smt_disj (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, _) ->
@@ -326,10 +326,10 @@ let rec smt_cval ctx cval =
let add_event ctx ev smt =
let stack = event_stack ctx ev in
- Stack.push (Fn ("=>", [ctx.pathcond; smt])) stack
+ Stack.push (Fn ("=>", [Lazy.force ctx.pathcond; smt])) stack
let add_pathcond_event ctx ev =
- Stack.push ctx.pathcond (event_stack ctx ev)
+ Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)
let overflow_check ctx smt =
if not !opt_ignore_overflow then (
@@ -1269,11 +1269,7 @@ let smt_ssanode ctx cfg preds =
let pis = List.map get_pi (IntSet.elements preds) in
let mux =
List.fold_right2 (fun pi id chain ->
- let pathcond =
- match pi with
- | [cval] -> smt_cval ctx cval
- | _ -> Fn ("and", List.map (smt_cval ctx) pi)
- in
+ let pathcond = smt_conj (List.map (smt_cval ctx) pi) in
match chain with
| Some smt ->
Some (Ite (pathcond, Var (zencode_name id), smt))
@@ -1286,12 +1282,28 @@ let smt_ssanode ctx cfg preds =
| Some mux ->
[Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
-let rec get_pathcond ctx fns =
+let rec get_pathcond n cfg ctx =
let open Jib_ssa in
- match fns with
- | [] | Pi [] :: _ -> Bool_lit true
- | Pi cvals :: _ -> Fn ("and", List.map (smt_cval ctx) cvals)
- | Phi _ :: fns -> get_pathcond ctx fns
+ match get_vertex cfg n with
+ | Some ((_, CF_guard cond), _, _) ->
+ smt_cval ctx (get_cond cfg cond)
+ | Some (_, preds, succs) ->
+ if IntSet.cardinal preds = 0 then
+ Bool_lit true
+ else if IntSet.cardinal preds = 1 then
+ get_pathcond (IntSet.min_elt preds) cfg ctx
+ else
+ let get_pi m =
+ match get_vertex cfg m with
+ | Some ((ssanodes, _), _, _) ->
+ V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes))
+ | None -> failwith "Predecessor node does not exist"
+ in
+ let pis = List.map get_pi (IntSet.elements preds) in
+ prerr_endline (string_of_int n ^ string_of_cval (V_call (Bor, pis)));
+ smt_cval ctx (V_call (Bor, pis))
+
+ | None -> assert false (* Should never be called for a non-existent node *)
(* For any complex l-expression we need to turn it into a
read-modify-write in the SMT solver. The SSA transform turns CL_id
@@ -1455,7 +1467,6 @@ let smt_cfnode all_cdefs ctx ssanodes =
in
smt_reg_decs @ List.map smt_start (NameMap.bindings inits)
| CF_block (instrs, terminator) ->
- let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in
let smt_instrs = List.map (smt_instr ctx) instrs in
let smt_term = smt_terminator ctx terminator in
List.concat (smt_instrs @ [smt_term])
@@ -1607,16 +1618,6 @@ let expand_reg_deref ctx = function
end
| instr -> instr
-let smt_conj = function
- | [] -> Bool_lit true
- | [x] -> x
- | xs -> Fn ("and", xs)
-
-let smt_disj = function
- | [] -> Bool_lit false
- | [x] -> x
- | xs -> Fn ("or", xs)
-
let rec smt_query ctx = function
| Q_all ev ->
let stack = event_stack ctx ev in
@@ -1687,6 +1688,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
let muxers =
ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
in
+ let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in
let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in
push_smt_defs stack muxers;
push_smt_defs stack basic_block;
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index dfacf90a..0f0f582e 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -73,6 +73,12 @@ let make ~initial_size () = {
conds = IntMap.empty
}
+let get_cond graph n =
+ if n >= 0 then
+ IntMap.find n graph.conds
+ else
+ V_call (Bnot, [IntMap.find (abs n) graph.conds])
+
let get_vertex graph n = graph.nodes.(n)
let iter_graph f graph =
@@ -662,34 +668,15 @@ 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 (bd @ args) :: ssa, cfnode), preds, succs)
+ graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs)
| None -> assert false
end
| None -> assert false
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 72cf1a1e..dadb20fd 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -60,6 +60,8 @@ val make : initial_size:int -> unit -> 'a array_graph
module IntSet : Set.S with type elt = int
+val get_cond : 'a array_graph -> int -> Jib.cval
+
val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 7f485447..1665419c 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -100,6 +100,16 @@ type smt_exp =
| Extract of int * int * smt_exp
| Tester of string * smt_exp
+let smt_conj = function
+ | [] -> Bool_lit true
+ | [x] -> x
+ | xs -> Fn ("and", xs)
+
+let smt_disj = function
+ | [] -> Bool_lit false
+ | [x] -> x
+ | xs -> Fn ("or", xs)
+
let extract i j x = Extract (i, j, x)
let bvnot x = Fn ("bvnot", [x])
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:57:13 +0000