diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 49dda8bb3..9d3513a34 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -344,7 +344,7 @@ module Make (Dom : Domain_sig.Dom) = struct let exit_state = match (freturn, exp) with | Some freturn, Some return_val -> - Dom.exec_move pre_state freturn return_val + Dom.exec_move pre_state (Vector.of_ (freturn, return_val)) | None, None -> pre_state | _ -> violates Llair.Func.invariant block.parent in @@ -376,7 +376,9 @@ module Make (Dom : Domain_sig.Dom) = struct ( match Stack.pop_throw stk ~unwind ~init:pre_state with | Some (from_call, retn_site, stk, unwind_state) -> let fthrow = func.fthrow in - let exit_state = Dom.exec_move unwind_state fthrow exc in + let exit_state = + Dom.exec_move unwind_state (Vector.of_ (fthrow, exc)) + in let post_state = Dom.post func.locals from_call exit_state in let retn_state = Dom.retn func.params func.freturn from_call post_state diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index 428767610..186522ab1 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -16,7 +16,7 @@ module type Dom = sig val is_false : t -> bool val exec_assume : t -> Exp.t -> t option val exec_kill : t -> Reg.t -> t - val exec_move : t -> Reg.t -> Exp.t -> t + val exec_move : t -> (Reg.t * Exp.t) vector -> t val exec_inst : t -> Llair.inst -> (t, unit) result val exec_intrinsic : diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index 990fa66ea..57a15b1d5 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -47,8 +47,8 @@ module Make (State_domain : State_domain_sig) = struct let exec_kill (entry, current) reg = (entry, State_domain.exec_kill current reg) - let exec_move (entry, current) formal actual = - (entry, State_domain.exec_move current formal actual) + let exec_move (entry, current) reg_exps = + (entry, State_domain.exec_move current reg_exps) let exec_inst (entry, current) inst = match State_domain.exec_inst current inst with diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index 5978bcc15..e4a45a6c6 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -16,7 +16,7 @@ let join () () = Some () let is_false _ = false let exec_assume () _ = Some () let exec_kill () _ = () -let exec_move () _ _ = () +let exec_move () _ = () let exec_inst () _ = Ok () let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index f2af11554..3b6c4d997 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -30,7 +30,10 @@ let used_globals ?(init = empty) exp = let exec_assume st exp = Some (used_globals ~init:st exp) let exec_kill st _ = st -let exec_move st _ rhs = used_globals ~init:st rhs + +let exec_move st reg_exps = + Vector.fold reg_exps ~init:st ~f:(fun st (_, rhs) -> + used_globals ~init:st rhs ) let exec_inst st inst = [%Trace.call fun {pf} -> pf "pre:{%a} %a" pp st Llair.Inst.pp inst] diff --git a/sledge/src/import/vector.ml b/sledge/src/import/vector.ml index eb2f92d36..6908f7e86 100644 --- a/sledge/src/import/vector.ml +++ b/sledge/src/import/vector.ml @@ -78,6 +78,7 @@ let fold_map x ~init ~f = let concat xs = v (Array.concat (al xs)) let copy x = v (Array.copy (a x)) +let of_ x = v [|x|] let of_array = v let of_list x = v (Array.of_list x) let of_list_rev x = v (Array.of_list_rev x) diff --git a/sledge/src/import/vector.mli b/sledge/src/import/vector.mli index 5b37018cd..53faa66eb 100644 --- a/sledge/src/import/vector.mli +++ b/sledge/src/import/vector.mli @@ -91,6 +91,8 @@ val copy : 'a t -> 'a t (* val sub : ('a t, 'a t) Base__Blit_intf.sub *) (* val subo : ('a t, 'a t) Base__Blit_intf.subo *) +val of_ : 'a -> 'a t + val of_array : 'a array -> 'a t (** [of_array a] is a vector that shares its representation with array [a], therefore mutating [a] changes [of_array a]. The intended use for diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 656844ee3..f18e2066c 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -695,8 +695,8 @@ let rec exec_specs pre = function exec_specs pre specs >>| fun posts -> Sh.or_ post posts | [] -> Ok (Sh.false_ pre.us) -let move pre reg exp = - exec_spec pre (move_spec pre.us (Vector.of_array [|(reg, exp)|])) +let move pre reg_exps = + exec_spec pre (move_spec pre.us reg_exps) |> function Ok post -> post | _ -> assert false let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result = diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli index f91ce13c8..39b0e4603 100644 --- a/sledge/src/symbheap/exec.mli +++ b/sledge/src/symbheap/exec.mli @@ -9,7 +9,7 @@ val assume : Sh.t -> Term.t -> Sh.t option val kill : Sh.t -> Var.t -> Sh.t -val move : Sh.t -> Var.t -> Term.t -> Sh.t +val move : Sh.t -> (Var.t * Term.t) vector -> Sh.t val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result val intrinsic : diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index a0025f924..a1b8a0f78 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -30,7 +30,10 @@ let join l r = Some (Sh.or_ l r) let is_false = Sh.is_false let exec_assume q b = Exec.assume q (Exp.term b) let exec_kill q r = Exec.kill q (Reg.var r) -let exec_move q r e = Exec.move q (Reg.var r) (Exp.term e) + +let exec_move q res = + Exec.move q (Vector.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e))) + let exec_inst = Exec.inst let exec_intrinsic ~skip_throw q r i es = @@ -156,7 +159,8 @@ let retn formals freturn {areturn; subst; frame} q = let freturn = Option.map ~f:Reg.var freturn in let q = match (areturn, freturn) with - | Some areturn, Some freturn -> Exec.move q areturn (Term.var freturn) + | Some areturn, Some freturn -> + Exec.move q (Vector.of_ (areturn, Term.var freturn)) | Some areturn, None -> Exec.kill q areturn | _ -> q in