From 8d9b8962c74fbe1c7a436d64d45a5f72303cc08b Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 23 Aug 2019 07:19:41 -0700
Subject: [PATCH] [sledge] Add Move instruction

Reviewed By: jvillard

Differential Revision: D16905896

fbshipit-source-id: 3d8b9a88a
---
 sledge/src/llair/llair.ml   | 11 ++++++++++-
 sledge/src/llair/llair.mli  |  4 ++++
 sledge/src/symbheap/exec.ml | 20 ++++++++++++++++++++
 3 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 62bddc49f..a0aadf903 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -8,6 +8,7 @@
 (** Translation units *)
 
 type inst =
+  | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t}
   | Load of {reg: Var.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
   | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t}
   | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
@@ -119,6 +120,10 @@ type t = {globals: Global.t vector; functions: functions}
 let pp_inst fs inst =
   let pf pp = Format.fprintf fs pp in
   match inst with
+  | Move {reg_exps; loc} ->
+      let regs, exps = Vector.unzip reg_exps in
+      pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Var.pp) regs
+        (Vector.pp ",@ " Exp.pp) exps Loc.pp loc
   | Load {reg; ptr; len; loc} ->
       pf "@[<2>load %a@ %a@ %a;@]\t%a" Exp.pp len Var.pp reg Exp.pp ptr
         Loc.pp loc
@@ -218,6 +223,7 @@ module Inst = struct
   type t = inst [@@deriving sexp]
 
   let pp = pp_inst
+  let move ~reg_exps ~loc = Move {reg_exps; loc}
   let load ~reg ~ptr ~len ~loc = Load {reg; ptr; len; loc}
   let store ~ptr ~exp ~len ~loc = Store {ptr; exp; len; loc}
   let memset ~dst ~byt ~len ~loc = Memset {dst; byt; len; loc}
@@ -229,7 +235,8 @@ module Inst = struct
   let abort ~loc = Abort {loc}
 
   let loc = function
-    | Load {loc}
+    | Move {loc}
+     |Load {loc}
      |Store {loc}
      |Memset {loc}
      |Memcpy {loc}
@@ -242,6 +249,8 @@ module Inst = struct
 
   let union_locals inst vs =
     match inst with
+    | Move {reg_exps} ->
+        Vector.fold ~f:(fun vs (reg, _) -> Set.add vs reg) ~init:vs reg_exps
     | Load {reg} | Alloc {reg} | Nondet {reg= Some reg} -> Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
      |Nondet {reg= None}
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index b19cf7fef..715ec4543 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -30,6 +30,9 @@
 
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
+  | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t}
+      (** Move each value [exp] into corresponding register [reg]. All of
+          the moves take effect simultaneously. *)
   | Load of {reg: Var.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
       (** Read a [len]-byte value from the contents of memory at address
           [ptr] into [reg]. *)
@@ -130,6 +133,7 @@ module Inst : sig
   type t = inst
 
   val pp : t pp
+  val move : reg_exps:(Var.t * Exp.t) vector -> loc:Loc.t -> inst
   val load : reg:Var.t -> ptr:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val store : ptr:Exp.t -> exp:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memset : dst:Exp.t -> byt:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index e55059e76..a83cca4bf 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -54,6 +54,25 @@ let assume pre cnd =
 let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
 let return pre formal exp = Sh.and_ (Exp.eq (Exp.var formal) exp) pre
 
+(* { emp }
+ *   rs := es
+ * { *ᵢ rᵢ=eᵢΘ }
+ *)
+let move_spec us reg_exps =
+  let xs = Var.Set.empty in
+  let foot = Sh.emp in
+  let ws, rs =
+    Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty)
+      ~f:(fun (ws, rs) (reg, exp) ->
+        (Set.add ws reg, Set.union rs (Exp.fv exp)) )
+  in
+  let sub, ms, _ = assign ~ws ~rs ~us in
+  let post =
+    Vector.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) ->
+        Sh.and_ (Exp.eq (Exp.var reg) (Exp.rename sub exp)) post )
+  in
+  {xs; foot; sub; ms; post}
+
 (* { p-[b;m)->⟨l,α⟩ }
  *   load l r p
  * { r=αΘ * (p-[b;m)->⟨l,α⟩)Θ }
@@ -686,6 +705,7 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
   assert (Set.disjoint (Sh.fv pre) (Llair.Inst.locals inst)) ;
   let us = pre.us in
   match inst with
+  | Move {reg_exps; _} -> exec_spec pre (move_spec us reg_exps)
   | Load {reg; ptr; len; _} -> exec_spec pre (load_spec us reg ptr len)
   | Store {ptr; exp; len; _} -> exec_spec pre (store_spec us ptr exp len)
   | Memset {dst; byt; len; _} -> exec_spec pre (memset_spec us dst byt len)