[sledge] Refactor to clean up instruction ordering

Summary: No functional change diff in prep for modeling changes.

Reviewed By: ngorogiannis

Differential Revision: D14403655

fbshipit-source-id: 22b6a87d8

sledge/src/llair/frontend.ml

@@ -917,6 +917,12 @@ let xlate_instr :
             (Llair.Inst.nondet ~reg ~msg ~loc :: insts, term, []) )
       in
       match String.split fname ~on:'.' with
+      | "llvm" :: "memset" :: _ ->
+          let dst = xlate_value x (Llvm.operand instr 0) in
+          let byt = xlate_value x (Llvm.operand instr 1) in
+          let len = xlate_value x (Llvm.operand instr 2) in
+          continue (fun (insts, term) ->
+              (Llair.Inst.memset ~dst ~byt ~len ~loc :: insts, term, []) )
       | "llvm" :: "memcpy" :: _ ->
           let dst = xlate_value x (Llvm.operand instr 0) in
           let src = xlate_value x (Llvm.operand instr 1) in
@@ -929,12 +935,6 @@ let xlate_instr :
           let len = xlate_value x (Llvm.operand instr 2) in
           continue (fun (insts, term) ->
               (Llair.Inst.memmov ~dst ~src ~len ~loc :: insts, term, []) )
-      | "llvm" :: "memset" :: _ ->
-          let dst = xlate_value x (Llvm.operand instr 0) in
-          let byt = xlate_value x (Llvm.operand instr 1) in
-          let len = xlate_value x (Llvm.operand instr 2) in
-          continue (fun (insts, term) ->
-              (Llair.Inst.memset ~dst ~byt ~len ~loc :: insts, term, []) )
       | _ when Option.is_some (xlate_intrinsic_exp fname) ->
           continue (fun (insts, term) -> (insts, term, []))
       | ["llvm"; "dbg"; ("declare" | "value")]

sledge/src/llair/llair.ml

@@ -10,14 +10,14 @@
 type inst =
   | 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}
   | Memcpy of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
   | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
-  | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
   | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t}
-  | Malloc of {reg: Var.t; siz: Exp.t; loc: Loc.t}
   | Free of {ptr: Exp.t; loc: Loc.t}
-  | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
+  | Malloc of {reg: Var.t; siz: Exp.t; loc: Loc.t}
   | Strlen of {reg: Var.t; ptr: Exp.t; loc: Loc.t}
+  | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
 [@@deriving sexp]
 
 type cmnd = inst vector [@@deriving sexp]
@@ -94,26 +94,26 @@ let pp_inst fs inst =
   | Store {ptr; exp; len; loc} ->
       pf "@[<2>store %a@ %a@ %a;@]\t%a" Exp.pp len Exp.pp ptr Exp.pp exp
         Loc.pp loc
+  | Memset {dst; byt; len; loc} ->
+      pf "@[<2>memset %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp byt
+        Loc.pp loc
   | Memcpy {dst; src; len; loc} ->
       pf "@[<2>memcpy %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src
         Loc.pp loc
   | Memmov {dst; src; len; loc} ->
       pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src
         Loc.pp loc
-  | Memset {dst; byt; len; loc} ->
-      pf "@[<2>memset %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp byt
-        Loc.pp loc
   | Alloc {reg; num; len; loc} ->
       pf "@[<2>alloc %a@ [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp len
         Loc.pp loc
+  | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
   | Malloc {reg; siz; loc} ->
       pf "@[<2>malloc %a@ %a;@]\t%a" Var.pp reg Exp.pp siz Loc.pp loc
-  | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
+  | Strlen {reg; ptr; loc} ->
+      pf "@[<2>strlen %a@ %a;@]\t%a" Var.pp reg Exp.pp ptr Loc.pp loc
   | Nondet {reg; msg; loc} ->
       pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg
         Loc.pp loc
-  | Strlen {reg; ptr; loc} ->
-      pf "@[<2>strlen %a@ %a;@]\t%a" Var.pp reg Exp.pp ptr Loc.pp loc
 
 let pp_args pp_arg fs args =
   Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_arg) (List.rev args)
@@ -189,26 +189,26 @@ module Inst = struct
   let pp = pp_inst
   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}
   let memcpy ~dst ~src ~len ~loc = Memcpy {dst; src; len; loc}
   let memmov ~dst ~src ~len ~loc = Memmov {dst; src; len; loc}
-  let memset ~dst ~byt ~len ~loc = Memset {dst; byt; len; loc}
   let alloc ~reg ~num ~len ~loc = Alloc {reg; num; len; loc}
-  let malloc ~reg ~siz ~loc = Malloc {reg; siz; loc}
   let free ~ptr ~loc = Free {ptr; loc}
-  let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
+  let malloc ~reg ~siz ~loc = Malloc {reg; siz; loc}
   let strlen ~reg ~ptr ~loc = Strlen {reg; ptr; loc}
+  let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
 
   let loc = function
     | Load {loc}
      |Store {loc}
+     |Memset {loc}
      |Memcpy {loc}
      |Memmov {loc}
-     |Memset {loc}
      |Alloc {loc}
-     |Malloc {loc}
      |Free {loc}
-     |Nondet {loc}
+     |Malloc {loc}
-     |Strlen {loc} ->
+     |Strlen {loc}
+     |Nondet {loc} ->
         loc
 
   let union_locals inst vs =
@@ -216,8 +216,8 @@ module Inst = struct
     | Load {reg}
      |Alloc {reg}
      |Malloc {reg}
-     |Nondet {reg= Some reg}
+     |Strlen {reg}
-     |Strlen {reg} ->
+     |Nondet {reg= Some reg} ->
         Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _ | Nondet {reg= None}
       ->

sledge/src/llair/llair.mli

@@ -35,27 +35,27 @@ type inst = private
           [ptr] into [reg]. *)
   | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t}
       (** Write [len]-byte value [exp] into memory at address [ptr]. *)
+  | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
+      (** Store byte [byt] into [len] memory addresses starting from [dst]. *)
   | Memcpy of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
       (** Copy [len] bytes starting from address [src] to [dst], undefined
           if ranges overlap. *)
   | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
       (** Copy [len] bytes starting from address [src] to [dst]. *)
-  | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
-      (** Store byte [byt] into [len] memory addresses starting from [dst]. *)
   | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t}
       (** Allocate a block of memory large enough to store [num] elements of
           [len] bytes each and bind [reg] to the first address. *)
+  | Free of {ptr: Exp.t; loc: Loc.t}
+      (** Deallocate the previously allocated block at address [ptr]. *)
   | Malloc of {reg: Var.t; siz: Exp.t; loc: Loc.t}
       (** Maybe allocate a block of memory of size [siz] bytes and bind
           [reg] to the first address, otherwise bind [reg] to [null]. *)
-  | Free of {ptr: Exp.t; loc: Loc.t}
-      (** Deallocate the previously allocated block at address [ptr]. *)
-  | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
-      (** Bind [reg] to an arbitrary value, representing non-deterministic
-          approximation of behavior described by [msg]. *)
   | Strlen of {reg: Var.t; ptr: Exp.t; loc: Loc.t}
       (** Bind [reg] to the length of the null-terminated string in memory
           starting from [ptr]. *)
+  | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
+      (** Bind [reg] to an arbitrary value, representing non-deterministic
+          approximation of behavior described by [msg]. *)
 
 (** A (straight-line) command is a sequence of instructions. *)
 type cmnd = inst vector
@@ -130,14 +130,14 @@ module Inst : sig
   val pp : t pp
   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
   val memcpy : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memmov : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
-  val memset : dst:Exp.t -> byt:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val alloc : reg:Var.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
-  val malloc : reg:Var.t -> siz:Exp.t -> loc:Loc.t -> inst
   val free : ptr:Exp.t -> loc:Loc.t -> inst
-  val nondet : reg:Var.t option -> msg:string -> loc:Loc.t -> inst
+  val malloc : reg:Var.t -> siz:Exp.t -> loc:Loc.t -> inst
   val strlen : reg:Var.t -> ptr:Exp.t -> loc:Loc.t -> inst
+  val nondet : reg:Var.t option -> msg:string -> loc:Loc.t -> inst
   val loc : inst -> Loc.t
   val locals : inst -> Var.Set.t
 end

sledge/src/symbheap/exec.ml

@@ -33,42 +33,6 @@ let assume cnd pre =
   let post = Sh.and_ cnd pre in
   if Sh.is_false post then None else Some post
 
-(* { emp }
- *   alloc r [n × l]
- * { ∃α'. r-[r;n×l)->⟨n×l,α'⟩ }
- *)
-let alloc_spec us reg num len =
-  let loc = Exp.var reg in
-  let siz = Exp.mul Typ.siz num len in
-  let {xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
-  let post = Sh.seg seg in
-  let foot = Sh.extend_us xs Sh.emp in
-  {xs; foot; post}
-
-(* { emp }
- *   malloc r s
- * { r=0 ∨ ∃α'. r-[r;s)->⟨s,α'⟩ }
- *)
-let malloc_spec us reg siz =
-  let loc = Exp.var reg in
-  let {xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
-  let foot = Sh.extend_us xs Sh.emp in
-  let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in
-  {xs; foot; post}
-
-(* { p=0 ∨ p-[p;m)->⟨m,α⟩ }
- *   free p
- * { emp }
- *)
-let free_spec us ptr =
-  let len, us = Var.fresh "m" ~wrt:us in
-  let siz = Exp.var len in
-  let {xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len:siz ~siz us in
-  let xs = Set.add xs len in
-  let foot = Sh.or_ (null_eq ptr) (Sh.seg seg) in
-  let post = Sh.emp in
-  {xs; foot; post}
-
 (* { p-[b;m)->⟨l,α⟩ }
  *   load l r p
  * { r=α * p-[b;m)->⟨l,α⟩ }
@@ -242,6 +206,42 @@ let memmov_specs us dst src len =
   ; memmov_dn_spec us dst src len
   ; memmov_up_spec us dst src len ]
 
+(* { emp }
+ *   alloc r [n × l]
+ * { ∃α'. r-[r;n×l)->⟨n×l,α'⟩ }
+ *)
+let alloc_spec us reg num len =
+  let loc = Exp.var reg in
+  let siz = Exp.mul Typ.siz num len in
+  let {xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
+  let post = Sh.seg seg in
+  let foot = Sh.extend_us xs Sh.emp in
+  {xs; foot; post}
+
+(* { p=0 ∨ p-[p;m)->⟨m,α⟩ }
+ *   free p
+ * { emp }
+ *)
+let free_spec us ptr =
+  let len, us = Var.fresh "m" ~wrt:us in
+  let siz = Exp.var len in
+  let {xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len:siz ~siz us in
+  let xs = Set.add xs len in
+  let foot = Sh.or_ (null_eq ptr) (Sh.seg seg) in
+  let post = Sh.emp in
+  {xs; foot; post}
+
+(* { emp }
+ *   malloc r s
+ * { r=0 ∨ ∃α'. r-[r;s)->⟨s,α'⟩ }
+ *)
+let malloc_spec us reg siz =
+  let loc = Exp.var reg in
+  let {xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
+  let foot = Sh.extend_us xs Sh.emp in
+  let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in
+  {xs; foot; post}
+
 (* { p-[b;m)->⟨l,α⟩ }
  *   r = strlen p
  * { r=b+m-p-1 * p-[b;m)->⟨l,α⟩ }
@@ -296,14 +296,14 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, _) result =
   assert (Set.disjoint (Sh.fv pre) (Llair.Inst.locals inst)) ;
   let us = pre.us in
   ( match inst with
-  | Nondet _ -> Ok pre
-  | Alloc {reg; num; len} -> exec_spec pre (alloc_spec us reg num len)
-  | Malloc {reg; siz} -> exec_spec pre (malloc_spec us reg siz)
-  | Free {ptr} -> exec_spec pre (free_spec us ptr)
   | 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)
   | Memcpy {dst; src; len} -> exec_specs pre (memcpy_specs us dst src len)
   | Memmov {dst; src; len} -> exec_specs pre (memmov_specs us dst src len)
-  | Strlen {reg; ptr} -> exec_spec pre (strlen_spec us reg ptr) )
+  | Alloc {reg; num; len} -> exec_spec pre (alloc_spec us reg num len)
+  | Free {ptr} -> exec_spec pre (free_spec us ptr)
+  | Malloc {reg; siz} -> exec_spec pre (malloc_spec us reg siz)
+  | Strlen {reg; ptr} -> exec_spec pre (strlen_spec us reg ptr)
+  | Nondet _ -> Ok pre )
   |> Result.map_error ~f:(fun () -> (pre, inst))