From 080c843856d6c7a207116122357ed32a53e937f7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 17 Oct 2018 02:24:29 -0700 Subject: [PATCH] [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 | 7 +++++++ sledge/src/llair/llair.ml | 11 ++++++++++- sledge/src/llair/llair.mli | 4 ++++ sledge/src/symbheap/exec.ml | 12 ++++++++++++ 4 files changed, 33 insertions(+), 1 deletion(-) diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 0f80064fb..370d19fb1 100644 --- a/sledge/src/llair/frontend.ml +++ b/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 diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index e5034768e..2b541bf8f 100644 --- a/sledge/src/llair/llair.ml +++ b/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} -> diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 62b26c1e7..40bf0804b 100644 --- a/sledge/src/llair/llair.mli +++ b/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 diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 641051819..78c6e891b 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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)