[sledge] Convert memset, memcpy, and memmov to intrinsics

Reviewed By: jvillard

Differential Revision: D25146165

fbshipit-source-id: bd188096a

sledge/cli/domain_itv.ml

@@ -193,9 +193,7 @@ let exec_inst i q =
     | None -> Some q )
   | Load {reg; ptr; len= _; loc= _} -> Some (assign reg ptr q)
   | Nondet {reg= Some reg; msg= _; loc= _} -> Some (exec_kill reg q)
-  | Nondet {reg= None; msg= _; loc= _}
-   |Alloc _ | Memset _ | Memcpy _ | Memmov _ | Free _ ->
-      Some q
+  | Nondet {reg= None; msg= _; loc= _} | Alloc _ | Free _ -> Some q
   | Abort _ -> None
   | Intrinsic {reg= Some reg; _} -> Some (exec_kill reg q)
   | Intrinsic {reg= None; _} -> Some q

sledge/cli/frontend.ml

@@ -995,27 +995,6 @@ let xlate_intrinsic_inst emit_inst x name_segs instr num_actuals loc =
    |["free" (* void free(void* ptr) *)] ->
       let prefix, ptr = xlate_value x (Llvm.operand instr 0) in
       emit_inst ~prefix (Inst.free ~ptr ~loc)
-  | "llvm" :: "memset" :: _ ->
-      let pre_0, dst = xlate_value x (Llvm.operand instr 0) in
-      let pre_1, byt = xlate_value x (Llvm.operand instr 1) in
-      let pre_2, len = xlate_value x (Llvm.operand instr 2) in
-      emit_inst
-        ~prefix:(pre_0 @ pre_1 @ pre_2)
-        (Inst.memset ~dst ~byt ~len ~loc)
-  | "llvm" :: "memcpy" :: _ ->
-      let pre_0, dst = xlate_value x (Llvm.operand instr 0) in
-      let pre_1, src = xlate_value x (Llvm.operand instr 1) in
-      let pre_2, len = xlate_value x (Llvm.operand instr 2) in
-      emit_inst
-        ~prefix:(pre_0 @ pre_1 @ pre_2)
-        (Inst.memcpy ~dst ~src ~len ~loc)
-  | "llvm" :: "memmove" :: _ ->
-      let pre_0, dst = xlate_value x (Llvm.operand instr 0) in
-      let pre_1, src = xlate_value x (Llvm.operand instr 1) in
-      let pre_2, len = xlate_value x (Llvm.operand instr 2) in
-      emit_inst
-        ~prefix:(pre_0 @ pre_1 @ pre_2)
-        (Inst.memmov ~dst ~src ~len ~loc)
   | ["abort"] | ["llvm"; "trap"] -> emit_inst (Inst.abort ~loc)
   | [iname] | "llvm" :: iname :: _ -> (
     match Intrinsic.of_name iname with

sledge/src/domain_sh.ml

@@ -60,12 +60,6 @@ let exec_inst inst pre =
       Exec.load pre ~reg:(X.reg reg) ~ptr:(X.term ptr) ~len:(X.term len)
   | Store {ptr; exp; len; _} ->
       Exec.store pre ~ptr:(X.term ptr) ~exp:(X.term exp) ~len:(X.term len)
-  | Memset {dst; byt; len; _} ->
-      Exec.memset pre ~dst:(X.term dst) ~byt:(X.term byt) ~len:(X.term len)
-  | Memcpy {dst; src; len; _} ->
-      Exec.memcpy pre ~dst:(X.term dst) ~src:(X.term src) ~len:(X.term len)
-  | Memmov {dst; src; len; _} ->
-      Exec.memmov pre ~dst:(X.term dst) ~src:(X.term src) ~len:(X.term len)
   | Alloc {reg; num; len; _} ->
       Exec.alloc pre ~reg:(X.reg reg) ~num:(X.term num) ~len
   | Free {ptr; _} -> Exec.free pre ~ptr:(X.term ptr)

sledge/src/exec.ml

@@ -729,9 +729,6 @@ let move pre reg_exps =
 
 let load pre ~reg ~ptr ~len = exec_spec pre (load_spec reg ptr len)
 let store pre ~ptr ~exp ~len = exec_spec pre (store_spec ptr exp len)
-let memset pre ~dst ~byt ~len = exec_spec pre (memset_spec dst byt len)
-let memcpy pre ~dst ~src ~len = exec_specs pre (memcpy_specs dst src len)
-let memmov pre ~dst ~src ~len = exec_specs pre (memmov_specs dst src len)
 let alloc pre ~reg ~num ~len = exec_spec pre (alloc_spec reg num len)
 let free pre ~ptr = exec_spec pre (free_spec ptr)
 let nondet pre = function Some reg -> kill pre reg | None -> pre
@@ -745,6 +742,15 @@ let intrinsic ~skip_throw :
     -> Sh.t option =
  fun pre areturn intrinsic actuals ->
   match (areturn, intrinsic, IArray.to_array actuals) with
+  (*
+   * llvm intrinsics
+   *)
+  | None, `memset, [|dst; byt; len; _isvolatile|] ->
+      exec_spec pre (memset_spec dst byt len)
+  | None, `memcpy, [|dst; src; len; _isvolatile|] ->
+      exec_specs pre (memcpy_specs dst src len)
+  | None, `memmove, [|dst; src; len; _isvolatile|] ->
+      exec_specs pre (memmov_specs dst src len)
   (*
    * cstdlib - memory management
    *)
@@ -817,11 +823,11 @@ let intrinsic ~skip_throw :
    * signature mismatch
    *)
   | ( _
-    , ( `malloc | `aligned_alloc | `calloc | `posix_memalign | `realloc
-      | `mallocx | `rallocx | `xallocx | `sallocx | `dallocx | `sdallocx
-      | `nallocx | `malloc_usable_size | `mallctl | `mallctlnametomib
-      | `mallctlbymib | `strlen | `__cxa_allocate_exception
-      | `_ZN5folly13usingJEMallocEv )
+    , ( `memset | `memcpy | `memmove | `malloc | `aligned_alloc | `calloc
+      | `posix_memalign | `realloc | `mallocx | `rallocx | `xallocx
+      | `sallocx | `dallocx | `sdallocx | `nallocx | `malloc_usable_size
+      | `mallctl | `mallctlnametomib | `mallctlbymib | `strlen
+      | `__cxa_allocate_exception | `_ZN5folly13usingJEMallocEv )
     , _ ) ->
       fail "%aintrinsic %a%a;"
         (Option.pp "%a := " Var.pp)

sledge/src/exec.mli

@@ -14,9 +14,6 @@ val kill : Sh.t -> Var.t -> Sh.t
 val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t
 val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option
 val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option
-val memset : Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> Sh.t option
-val memcpy : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
-val memmov : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
 val alloc : Sh.t -> reg:Var.t -> num:Term.t -> len:int -> Sh.t option
 val free : Sh.t -> ptr:Term.t -> Sh.t option
 val nondet : Sh.t -> Var.t option -> Sh.t

sledge/src/llair/intrinsics.ml

@@ -8,7 +8,11 @@
 (** Intrinsic instruction opcodes *)
 
 type t =
-  [ (* cstdlib - memory management *)
+  [ (* llvm intrinsics *)
+    `memset
+  | `memcpy
+  | `memmove
+  | (* cstdlib - memory management *)
     `malloc
   | `aligned_alloc
   | `calloc

sledge/src/llair/llair.ml

@@ -39,9 +39,6 @@ type inst =
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
   | Load of {reg: Reg.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}
   | Alloc of {reg: Reg.t; num: Exp.t; len: int; loc: Loc.t}
   | Free of {ptr: Exp.t; loc: Loc.t}
   | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t}
@@ -260,15 +257,6 @@ 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
   | Alloc {reg; num; len; loc} ->
       pf "@[<2>%a@ := alloc [%a x %i];@]\t%a" Reg.pp reg Exp.pp num len
         Loc.pp loc
@@ -369,9 +357,6 @@ module Inst = struct
   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}
-  let memcpy ~dst ~src ~len ~loc = Memcpy {dst; src; len; loc}
-  let memmov ~dst ~src ~len ~loc = Memmov {dst; src; len; loc}
   let alloc ~reg ~num ~len ~loc = Alloc {reg; num; len; loc}
   let free ~ptr ~loc = Free {ptr; loc}
   let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
@@ -382,9 +367,6 @@ module Inst = struct
     | Move {loc; _}
      |Load {loc; _}
      |Store {loc; _}
-     |Memset {loc; _}
-     |Memcpy {loc; _}
-     |Memmov {loc; _}
      |Alloc {loc; _}
      |Free {loc; _}
      |Nondet {loc; _}
@@ -401,7 +383,7 @@ module Inst = struct
      |Nondet {reg= Some reg; _}
      |Intrinsic {reg= Some reg; _} ->
         Reg.Set.add reg vs
-    | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
+    | Store _ | Free _
      |Nondet {reg= None; _}
      |Abort _
      |Intrinsic {reg= None; _} ->
@@ -415,9 +397,6 @@ module Inst = struct
         IArray.fold ~f:(fun (_reg, exp) -> f exp) reg_exps s
     | Load {reg= _; ptr; len; loc= _} -> f len (f ptr s)
     | Store {ptr; exp; len; loc= _} -> f len (f exp (f ptr s))
-    | Memset {dst; byt; len; loc= _} -> f len (f byt (f dst s))
-    | Memcpy {dst; src; len; loc= _} | Memmov {dst; src; len; loc= _} ->
-        f len (f src (f dst s))
     | Alloc {reg= _; num; len= _; loc= _} -> f num s
     | Free {ptr; loc= _} -> f ptr s
     | Nondet {reg= _; msg= _; loc= _} -> s

sledge/src/llair/llair.mli

@@ -34,13 +34,6 @@ 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]. *)
   | Alloc of {reg: Reg.t; num: Exp.t; len: int; 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. *)
@@ -126,9 +119,6 @@ module Inst : sig
   val move : reg_exps:(Reg.t * Exp.t) iarray -> loc:Loc.t -> inst
   val load : reg:Reg.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 alloc : reg:Reg.t -> num:Exp.t -> len:int -> loc:Loc.t -> inst
   val free : ptr:Exp.t -> loc:Loc.t -> inst
   val nondet : reg:Reg.t option -> msg:string -> loc:Loc.t -> inst