[sledge] Add maybe-alloc instruction that may fail

Summary: Used to model C `malloc`.

Reviewed By: mbouaziz

Differential Revision: D10389481

fbshipit-source-id: 039937dda

sledge/src/llair/frontend.ml

@@ -942,6 +942,13 @@ let xlate_instr :
                 :: insts
               , term
               , [] ) )
+      | ["malloc"] ->
+          let siz = xlate_value x (Llvm.operand instr 0) in
+          continue (fun (insts, term) ->
+              ( Llair.Inst.malloc ~reg:(Option.value_exn reg) ~siz ~loc
+                :: insts
+              , term
+              , [] ) )
       | ["_Znwm"] ->
           let num = xlate_value x (Llvm.operand instr 0) in
           let llt = Llvm.type_of instr in

sledge/src/llair/llair.ml

@@ -14,6 +14,7 @@ type inst =
   | 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}
   | Strlen of {reg: Var.t; ptr: Exp.t; loc: Loc.t}
@@ -103,6 +104,8 @@ let pp_inst fs inst =
   | 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
+  | 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
   | Nondet {reg; msg; loc} ->
       pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg
@@ -188,6 +191,7 @@ module Inst = struct
   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 strlen ~reg ~ptr ~loc = Strlen {reg; ptr; loc}
@@ -199,6 +203,7 @@ module Inst = struct
      |Memmov {loc}
      |Memset {loc}
      |Alloc {loc}
+     |Malloc {loc}
      |Free {loc}
      |Nondet {loc}
      |Strlen {loc} ->
@@ -206,7 +211,11 @@ module Inst = struct
 
   let union_locals inst vs =
     match inst with
-    | Load {reg} | Alloc {reg} | Nondet {reg= Some reg} | Strlen {reg} ->
+    | Load {reg}
+     |Alloc {reg}
+     |Malloc {reg}
+     |Nondet {reg= Some reg}
+     |Strlen {reg} ->
         Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _ | Nondet {reg= None}
       ->

sledge/src/llair/llair.mli

@@ -45,6 +45,9 @@ type inst = private
   | 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. *)
+  | 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}
@@ -131,6 +134,7 @@ module Inst : sig
   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 strlen : reg:Var.t -> ptr:Exp.t -> loc:Loc.t -> inst

sledge/src/symbheap/exec.ml

@@ -45,6 +45,17 @@ let alloc_spec us reg num len =
   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 }
@@ -282,6 +293,7 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, _) result =
   ( 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)