Do not escape local block ids if ptr is loaded from initial mem
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1707,14 +1707,22 @@ expr Memory::checkNocapture() const {
void Memory::escapeLocalPtr(const expr &ptr) {
uint64_t bid;
+ unsigned hi, lo;
+ expr sel, blk, idx;
+
for (const auto &bid_expr : extract_possible_local_bids(*this, ptr)) {
if (bid_expr.isUInt(bid)) {
if (bid < numLocals())
escaped_local_blks[bid] = true;
+ } else if (bid_expr.isExtract(sel, hi, lo) &&
+ sel.isSelect(blk, idx) && blk.eq(mk_block_val_array())) {
+ // initial non local block bytes don't contain local pointers.
+ continue;
} else {
// may escape a local ptr, but we don't know which one
escaped_local_blks.clear();
escaped_local_blks.resize(numLocals(), true);
+ break;
}
}
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -448,6 +448,15 @@ bool expr::isStore(expr &array, expr &idx, expr &val) const {
return false;
}
+bool expr::isSelect(expr &array, expr &idx) const {
+ if (auto app = isAppOf(Z3_OP_SELECT)) {
+ array = Z3_get_app_arg(ctx(), app, 0);
+ idx = Z3_get_app_arg(ctx(), app, 1);
+ return true;
+ }
+ return false;
+}
+
bool expr::isNaNCheck(expr &fp) const {
if (auto app = isAppOf(Z3_OP_FPA_IS_NAN)) {
fp = Z3_get_app_arg(ctx(), app, 0);

MODIFY
smt/expr.h
smt/expr.h
@@ -134,6 +134,7 @@ public:
bool isBasePlusOffset(expr &base, uint64_t &offset) const;
bool isConstArray(expr &val) const;
bool isStore(expr &array, expr &idx, expr &val) const;
+ bool isSelect(expr &array, expr &idx) const;
bool isNaNCheck(expr &fp) const;
bool isfloat2BV(expr &fp) const;

ADD
tests/alive-tv/calls/escape2.srctgt.ll
+@glb = global i8* null
+declare i8* @f(i8* %p)
+
+define i8 @src() {
+ %p = alloca i8
+ store i8 1, i8* %p
+
+ %q = load i8*, i8** @glb
+ %q2 = call i8* @f(i8* %q) ; cannot be %p
+ store i8 2, i8* %q2
+
+ %v = load i8, i8* %p
+ ret i8 %v
+}
+
+define i8 @tgt() {
+ %p = alloca i8
+ store i8 1, i8* %p
+
+ %q = load i8*, i8** @glb
+ %q2 = call i8* @f(i8* %q) ; cannot be %p
+ store i8 2, i8* %q2
+
+ ret i8 1
+}

Do not escape local block ids if ptr is loaded from initial mem (#426)