optimize checkNoCapture() to not check constant data as it cannot have escaped pointers
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1681,7 +1681,8 @@ expr Memory::checkNocapture() const {
auto ofs = expr::mkVar(name.c_str(), bits_for_offset);
expr res(true);
- for (unsigned bid = has_null_block; bid < numNonlocals(); ++bid) {
+ for (unsigned bid = has_null_block + num_consts_src; bid < numNonlocals();
+ ++bid) {
Pointer p(*this, expr::mkUInt(bid, bits_for_bid), ofs);
Byte b(*this, non_local_block_val.load(p.shortPtr()));
Pointer loadp(*this, b.ptrValue());
@@ -1703,7 +1704,7 @@ void Memory::escapeLocalPtr(const expr &ptr) {
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())) {
+ sel.isLoad(blk, idx) && blk.eq(mk_block_val_array())) {
// initial non local block bytes don't contain local pointers.
continue;
} else {

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -448,7 +448,7 @@ bool expr::isStore(expr &array, expr &idx, expr &val) const {
return false;
}
-bool expr::isSelect(expr &array, expr &idx) const {
+bool expr::isLoad(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);

MODIFY
smt/expr.h
smt/expr.h
@@ -134,7 +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 isLoad(expr &array, expr &idx) const;
bool isNaNCheck(expr &fp) const;
bool isfloat2BV(expr &fp) const;

optimize checkNoCapture() to not check constant data as it cannot have escaped pointers