memory: increase precision of escaped local blocks
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -783,13 +783,27 @@ ostream& operator<<(ostream &os, const Pointer &p) {
}
+static vector<expr> extract_possible_local_bids(Memory &m, const Byte &b) {
+ vector<expr> ret;
+ expr zero = expr::mkUInt(0, bits_for_offset);
+ for (auto ptr_val : expr::allLeafs(b.ptr_value())) {
+ for (auto bid : expr::allLeafs(Pointer(m, move(ptr_val)).get_bid())) {
+ Pointer ptr(m, bid, zero);
+ if (!ptr.is_local().isFalse())
+ ret.emplace_back(ptr.get_short_bid());
+ }
+ }
+ return ret;
+}
+
void Memory::store(const Pointer &p, const expr &val, expr &local,
expr &non_local, bool index_bid) {
- if (!index_bid) {
- Byte b(*this, expr(val));
- if (!b.is_ptr().isFalse() && !b.ptr().is_local().isFalse()) {
+ if (!index_bid && num_locals > 0) {
+ Byte byte(*this, expr(val));
+ if (byte.is_ptr().isTrue()) {
uint64_t bid;
- if (b.ptr().get_short_bid().isUInt(bid)) {
+ for (const auto &bid_expr : extract_possible_local_bids(*this, byte)) {
+ if (bid_expr.isUInt(bid)) {
if (bid < num_locals)
escaped_local_blks[bid] = true;
} else {
@@ -799,6 +813,7 @@ void Memory::store(const Pointer &p, const expr &val, expr &local,
}
}
}
+ }
auto is_local = p.is_local();
auto idx = index_bid ? p.get_short_bid() : p.short_ptr();
local = expr::mkIf(is_local, local.store(idx, val), local);
@@ -1525,8 +1540,9 @@ bool Memory::operator<(const Memory &rhs) const {
}
#define P(msg, local, nonlocal) \
- os << msg "\nLocal: " << m.local.simplify() \
- << "\nNon-local: " << m.nonlocal.simplify() << "\n\n"
+ os << msg "\n"; \
+ if (num_locals > 0) os << "Local: " << m.local.simplify() << '\n'; \
+ if (num_locals > 0) os << "Non-local: " << m.nonlocal.simplify() << "\n\n"
ostream& operator<<(ostream &os, const Memory &m) {
if (memory_unused())
@@ -1537,7 +1553,14 @@ ostream& operator<<(ostream &os, const Memory &m) {
P("BLOCK SIZE:", local_blk_size, non_local_blk_size);
P("BLOCK ALIGN:", local_blk_align, non_local_blk_align);
P("BLOCK KIND:", local_blk_kind, non_local_blk_kind);
- return os << "LOCAL BLOCK ADDR: " << m.local_blk_addr << '\n';
+ if (num_locals > 0) {
+ os << "ESCAPED LOCAL BLOCKS: ";
+ for (unsigned i = 0; i < num_locals; ++i) {
+ os << m.escaped_local_blks[i];
+ }
+ os << "\nLOCAL BLOCK ADDR: " << m.local_blk_addr << '\n';
+ }
+ return os;
}
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1541,6 +1541,27 @@ set<expr> expr::vars() const {
return result;
}
+vector<expr> expr::allLeafs(const expr &e) {
+ vector<expr> ret;
+ vector<expr> worklist = { e };
+ unordered_set<Z3_ast> seen;
+ do {
+ expr v = worklist.back();
+ worklist.pop_back();
+ if (!seen.insert(v()).second)
+ continue;
+
+ expr cond, then, els;
+ if (v.isIf(cond, then, els)) {
+ worklist.emplace_back(move(then));
+ worklist.emplace_back(move(els));
+ } else {
+ ret.emplace_back(move(v));
+ }
+ } while (!worklist.empty());
+ return ret;
+}
+
void expr::printUnsigned(ostream &os) const {
os << numeral_string();
}

MODIFY
smt/expr.h
smt/expr.h
@@ -285,6 +285,9 @@ public:
std::set<expr> vars() const;
+ // returns set of all possible leaf expressions (best-effort simplification)
+ static std::vector<expr> allLeafs(const expr &e);
+
void printUnsigned(std::ostream &os) const;
void printSigned(std::ostream &os) const;
void printHexadecimal(std::ostream &os) const;

ADD
tests/alive-tv/memory/fncall-local-escaped.src.ll
+; TEST-ARGS: -smt-to=10000
+
+@glb = global i8* null
+
+define i8 @foo(i1 %cmp) {
+ %a = alloca i8
+ %b = alloca i8
+ %c = alloca i8
+ store i8 42, i8* %c
+ br i1 %cmp, label %t, label %f
+
+t:
+ store i8* %a, i8** @glb
+ br label %end
+
+f:
+ store i8* %b, i8** @glb
+ br label %end
+
+end:
+ call void @fn()
+ %load = load i8, i8* %c
+ ret i8 %load
+}
+
+declare void @fn()

ADD
tests/alive-tv/memory/fncall-local-escaped.tgt.ll
+@glb = global i8* null
+
+define i8 @foo(i1 %cmp) {
+ %a = alloca i8
+ %b = alloca i8
+ %c = alloca i8
+ %a.b = select i1 %cmp, i8* %a, i8* %b
+ store i8* %a.b, i8** @glb
+ call void @fn()
+ ret i8 42
+}
+
+declare void @fn()

MODIFY
tests/alive-tv/memory/storeptr.src.ll
tests/alive-tv/memory/storeptr.src.ll
-; TEST-ARGS: -smt-to=10000 -disable-undef-input
+; TEST-ARGS: -smt-to=20000 -disable-undef-input
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"

memory: increase precision of escaped local blocks