[sledge] Make type of exec_move consistent with move instruction

Summary:
The move instruction takes a vector of assignments to perform in
parallel, so generalize exec_move from one to a vector.

Reviewed By: bennostein

Differential Revision: D17665248

fbshipit-source-id: 52aae5ff9

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

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 :

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 =
+  let exec_move (entry, current) reg_exps =
-    (entry, State_domain.exec_move current formal actual)
+    (entry, State_domain.exec_move current reg_exps)
 
   let exec_inst (entry, current) inst =
     match State_domain.exec_inst current inst with

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
 

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]

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)

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

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 =
+let move pre reg_exps =
-  exec_spec pre (move_spec pre.us (Vector.of_array [|(reg, exp)|]))
+  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 =

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 :

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