[sledge] Refactor dispatch on instruction from Exec to Sh_domain

Summary:
This puts the mediation between Exp and Term together in Sh_domain
rather than being spread across the two.

Reviewed By: bennostein

Differential Revision: D17665235

fbshipit-source-id: edf277d45

sledge/src/symbheap/exec.ml

@@ -48,12 +48,6 @@ let assign ~ws ~rs ~us =
  * Instruction small axioms
  *)
 
-let assume pre cnd =
-  let post = Sh.and_ cnd pre in
-  if Sh.is_false post then None else Some post
-
-let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
-
 (* { emp }
  *   rs := es
  * { *ᵢ rᵢ=eᵢΘ }
@@ -695,45 +689,36 @@ let rec exec_specs pre = function
       exec_specs pre specs >>| fun posts -> Sh.or_ post posts
   | [] -> Ok (Sh.false_ pre.us)
 
+(*
+ * Exposed interface
+ *)
+
+let assume pre cnd =
+  let post = Sh.and_ cnd pre in
+  if Sh.is_false post then None else Some post
+
+let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
+
 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 =
+let load pre ~reg ~ptr ~len = exec_spec pre (load_spec pre.us reg ptr len)
- fun pre inst ->
+let store pre ~ptr ~exp ~len = exec_spec pre (store_spec pre.us ptr exp len)
-  [%Trace.info
+
-    "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ;
+let memset pre ~dst ~byt ~len =
-  assert (Set.disjoint (Sh.fv pre) (Reg.Set.vars (Llair.Inst.locals inst))) ;
+  exec_spec pre (memset_spec pre.us dst byt len)
-  let us = pre.us in
+
-  match inst with
+let memcpy pre ~dst ~src ~len =
-  | Move {reg_exps; _} ->
+  exec_specs pre (memcpy_specs pre.us dst src len)
-      exec_spec pre
+
-        (move_spec us
+let memmov pre ~dst ~src ~len =
-           (Vector.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e))))
+  exec_specs pre (memmov_specs pre.us dst src len)
-  | Load {reg; ptr; len; _} ->
+
-      exec_spec pre
+let alloc pre ~reg ~num ~len = exec_spec pre (alloc_spec pre.us reg num len)
-        (load_spec us (Reg.var reg) (Exp.term ptr) (Exp.term len))
+let free pre ~ptr = exec_spec pre (free_spec pre.us ptr)
-  | Store {ptr; exp; len; _} ->
+let nondet pre = function Some reg -> kill pre reg | None -> pre
-      exec_spec pre
+let abort _ = Error ()
-        (store_spec us (Exp.term ptr) (Exp.term exp) (Exp.term len))
-  | Memset {dst; byt; len; _} ->
-      exec_spec pre
-        (memset_spec us (Exp.term dst) (Exp.term byt) (Exp.term len))
-  | Memcpy {dst; src; len; _} ->
-      exec_specs pre
-        (memcpy_specs us (Exp.term dst) (Exp.term src) (Exp.term len))
-  | Memmov {dst; src; len; _} ->
-      exec_specs pre
-        (memmov_specs us (Exp.term dst) (Exp.term src) (Exp.term len))
-  | Alloc {reg; num; len; _} ->
-      exec_spec pre
-        (alloc_spec us (Reg.var reg) (Exp.term num) (Exp.term len))
-  | Free {ptr; _} -> exec_spec pre (free_spec us (Exp.term ptr))
-  | Nondet {reg= Some reg; _} -> Ok (kill pre (Reg.var reg))
-  | Nondet {reg= None; _} -> Ok pre
-  | Abort _ -> Error ()
-
-let skip : Sh.t -> (Sh.t, _) result option = fun pre -> Some (Ok pre)
 
 let intrinsic ~skip_throw :
        Sh.t
@@ -752,6 +737,7 @@ let intrinsic ~skip_throw :
     let n = Var.name intrinsic in
     match String.index n '.' with None -> n | Some i -> String.prefix n i
   in
+  let skip pre = Some (Ok pre) in
   match (areturn, name, actuals) with
   (*
    * cstdlib - memory management

sledge/src/symbheap/exec.mli

@@ -10,7 +10,28 @@
 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) vector -> Sh.t
-val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result
+
+val load :
+  Sh.t -> reg:Var.var -> ptr:Term.t -> len:Term.t -> (Sh.t, unit) result
+
+val store :
+  Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> (Sh.t, unit) result
+
+val memset :
+  Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> (Sh.t, unit) result
+
+val memcpy :
+  Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> (Sh.t, unit) result
+
+val memmov :
+  Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> (Sh.t, unit) result
+
+val alloc :
+  Sh.t -> reg:Var.var -> num:Term.t -> len:Term.t -> (Sh.t, unit) result
+
+val free : Sh.t -> ptr:Term.t -> (Sh.t, unit) result
+val nondet : Sh.t -> Var.var sexp_option -> Sh.t
+val abort : Sh.t -> (Sh.t, unit) result
 
 val intrinsic :
      skip_throw:bool

sledge/src/symbheap/sh_domain.ml

@@ -34,7 +34,36 @@ let exec_kill q r = Exec.kill q (Reg.var r)
 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_inst pre inst =
+  [%Trace.info
+    "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ;
+  assert (Set.disjoint (Sh.fv pre) (Reg.Set.vars (Llair.Inst.locals inst))) ;
+  match inst with
+  | Move {reg_exps; _} ->
+      Ok
+        (Exec.move pre
+           (Vector.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e))))
+  | Load {reg; ptr; len; _} ->
+      Exec.load pre ~reg:(Reg.var reg) ~ptr:(Exp.term ptr)
+        ~len:(Exp.term len)
+  | Store {ptr; exp; len; _} ->
+      Exec.store pre ~ptr:(Exp.term ptr) ~exp:(Exp.term exp)
+        ~len:(Exp.term len)
+  | Memset {dst; byt; len; _} ->
+      Exec.memset pre ~dst:(Exp.term dst) ~byt:(Exp.term byt)
+        ~len:(Exp.term len)
+  | Memcpy {dst; src; len; _} ->
+      Exec.memcpy pre ~dst:(Exp.term dst) ~src:(Exp.term src)
+        ~len:(Exp.term len)
+  | Memmov {dst; src; len; _} ->
+      Exec.memmov pre ~dst:(Exp.term dst) ~src:(Exp.term src)
+        ~len:(Exp.term len)
+  | Alloc {reg; num; len; _} ->
+      Exec.alloc pre ~reg:(Reg.var reg) ~num:(Exp.term num)
+        ~len:(Exp.term len)
+  | Free {ptr; _} -> Exec.free pre ~ptr:(Exp.term ptr)
+  | Nondet {reg; _} -> Ok (Exec.nondet pre (Option.map ~f:Reg.var reg))
+  | Abort _ -> Exec.abort pre
 
 let exec_intrinsic ~skip_throw q r i es =
   Exec.intrinsic ~skip_throw q (Option.map ~f:Reg.var r) (Reg.var i)