From 0f61a97feb8f99e9ec7411accd185bdf4b231fb6 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Wed, 12 Jun 2019 08:47:06 -0700 Subject: [PATCH] [sledge] Add non-failling alloc intrinsic Summary: This diff adds a `__llair_alloc` intrinsic which is modeled as a non-failing malloc. Using it instead of `malloc` increases the readbility of symbolic heaps, because it removes all the cases where malloc failed. Note that `assert(malloc())` does not have the desired effect. Reviewed By: ngorogiannis Differential Revision: D15778817 fbshipit-source-id: d02784077 --- sledge/model/llair_intrinsics.h | 3 +++ sledge/src/llair/frontend.ml | 8 +++++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/sledge/model/llair_intrinsics.h b/sledge/model/llair_intrinsics.h index 967a1d07e..fdcb6cd18 100644 --- a/sledge/model/llair_intrinsics.h +++ b/sledge/model/llair_intrinsics.h @@ -13,6 +13,9 @@ extern "C" { __attribute__((noreturn)) void __llair_throw(void* thrown_exception); +/* This models allocation that cannot fail. */ +void* __llair_alloc(unsigned size); + #ifdef __cplusplus } #endif diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 34cd84baf..009a66f89 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -940,10 +940,16 @@ let xlate_instr : let exc = xlate_value x (Llvm.operand instr 0) in emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc) | ["_Znwm" (* operator new(size_t num) *)] + |["__llair_alloc" (* void* __llair_alloc(unsigned size) *)] |[ "_ZnwmSt11align_val_t" (* operator new(unsigned long, std::align_val_t) *) ] -> let reg = xlate_name instr in - let num = xlate_value x (Llvm.operand instr 0) in + let num_operand = Llvm.operand instr 0 in + let num = + Exp.convert ~dst:Typ.siz + (xlate_value x num_operand) + ~src:(xlate_type x (Llvm.type_of num_operand)) + in let llt = Llvm.type_of instr in let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)