memory: assume blocks are always live if free() isn't used
also simplify block kind constraints if malloc and/or free aren't used
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -16,5 +16,7 @@ bool little_endian;
bool nullptr_is_used;
bool has_int2ptr;
bool has_ptr2int;
+bool has_malloc;
+bool has_free;
}

MODIFY
ir/globals.h
ir/globals.h
@@ -28,11 +28,15 @@ extern unsigned bits_byte;
extern bool little_endian;
-/// Wether the null pointer is used in either function
+/// Whether the null pointer is used in either function
extern bool nullptr_is_used;
-/// Wether int2ptr or ptr2int are used in either function
+/// Whether int2ptr or ptr2int are used in either function
extern bool has_int2ptr;
extern bool has_ptr2int;
+/// Whether malloc or free/delete is used in either function
+extern bool has_malloc;
+extern bool has_free;
+
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -430,12 +430,31 @@ void Pointer::is_disjoint(const expr &len1, const Pointer &ptr2,
}
expr Pointer::is_block_alive() const {
+ // If programs have no free(), we assume all blocks are always live.
+ // For non-local blocks, there's enough non-determinism through block size,
+ // that can be 0 or non-0
+ if (!has_free)
+ return true;
+
auto bid = get_short_bid();
return expr::mkIf(is_local(), m.local_block_liveness.load(bid),
m.non_local_block_liveness.load(bid));
}
expr Pointer::get_alloc_type() const {
+ // If programs have no malloc & free, we don't need to store this information
+ // since it is only used to check if free/delete is ok and
+ // for memory refinement of local malloc'ed blocks
+ if (!has_malloc && !has_free)
+ return expr::mkUInt(NON_HEAP, 2);
+
+ // if malloc is used, but no free, we can still ignore info for non-locals
+ if (!has_free) {
+ FunctionExpr non_local;
+ non_local.add(get_short_bid(), expr::mkUInt(NON_HEAP, 2));
+ return get_value("blk_kind", m.local_blk_kind, non_local, expr());
+
+ }
return get_value("blk_kind", m.local_blk_kind, m.non_local_blk_kind,
expr::mkUInt(0, 2));
}
@@ -819,7 +838,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
}
void Memory::free(const expr &ptr) {
- assert(!memory_unused());
+ assert(!memory_unused() && has_free);
Pointer p(*this, ptr);
state->addUB(p.isNull() || (p.get_offset() == 0 &&
p.is_block_alive() &&

MODIFY
tests/alive-tv/memory/storeptr-fail.src.ll
tests/alive-tv/memory/storeptr-fail.src.ll
+; TEST-ARGS: -disable-undef-input
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
define i16 @f(i16** %pptr) {

MODIFY
tests/alive-tv/memory/storeptr.src.ll
tests/alive-tv/memory/storeptr.src.ll
+; TEST-ARGS: -disable-undef-input
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
define i16 @f(i16** %pptr) {

MODIFY
tests/alive-tv/memory/zeroinit-memset.src.ll
tests/alive-tv/memory/zeroinit-memset.src.ll
; From Transforms/MemCpyOpt/fca2memcpy.ll
-; TEST-ARGS: -smt-to=15000 -disable-undef-input -disable-poison-input
+; TEST-ARGS: -smt-to=15000 -disable-poison-input
target datalayout = "e-i64:64-f80:128-n8:16:32:64"
%S = type { i8*, i8, i32 }

MODIFY
tests/alive-tv/refinement/zero-null.src.ll
tests/alive-tv/refinement/zero-null.src.ll
+; TEST-ARGS: -disable-poison-input
+
define void @f(i64* %p) {
store i64 0, i64* %p
ret void

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -466,6 +466,9 @@ static void calculateAndInitConstants(Transform &t) {
nullptr_is_used = false;
has_int2ptr = false;
has_ptr2int = false;
+ has_malloc = false;
+ has_free = false;
+
// Mininum access size (in bytes)
uint64_t min_access_size = 16;
bool does_mem_access = false;
@@ -476,11 +479,15 @@ static void calculateAndInitConstants(Transform &t) {
for (auto op : I.operands()) {
nullptr_is_used |= has_nullptr(op);
}
+
if (auto conv = dynamic_cast<const ConversionOp*>(&I)) {
has_int2ptr |= conv->getOp() == ConversionOp::Int2Ptr;
has_ptr2int |= conv->getOp() == ConversionOp::Ptr2Int;
}
+ has_malloc |= dynamic_cast<const Malloc*>(&I) != nullptr;
+ has_free |= dynamic_cast<const Free *>(&I) != nullptr;
+
auto accsz = get_access_size(I);
if (accsz != NO_ACCESS) {
min_access_size = gcd(min_access_size, accsz);
@@ -515,7 +522,9 @@ static void calculateAndInitConstants(Transform &t) {
"little_endian: " << little_endian << "\n"
"nullptr_is_used: " << nullptr_is_used << "\n"
"has_int2ptr: " << has_int2ptr << "\n"
- "has_ptr2int: " << has_ptr2int << "\n";
+ "has_ptr2int: " << has_ptr2int << "\n"
+ "has_malloc: " << has_malloc << "\n"
+ "has_free: " << has_free << "\n";
}

memory: assume blocks are always live if free() isn't used
also simplify block kind constraints if malloc and/or free aren't used