print memory with SE verbose mode
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -11,6 +11,8 @@ using namespace smt;
using namespace std;
using namespace util;
+static bool did_pointer_store = false;
+
namespace IR {
Byte::Byte(const Memory &m, expr &&byterepr) : m(m), p(move(byterepr)) {
@@ -471,8 +473,7 @@ expr Pointer::block_val_refined(const Pointer &other) const {
expr is_ptr = val.is_ptr();
expr is_ptr2 = val2.is_ptr();
expr ptr_cnstr;
- if ((!m.did_pointer_store && !other.m.did_pointer_store) ||
- is_ptr.isFalse() || is_ptr2.isFalse()) {
+ if (!did_pointer_store || is_ptr.isFalse() || is_ptr2.isFalse()) {
ptr_cnstr = val == val2;
} else {
Pointer load_ptr(m, val.ptr_value());
@@ -690,6 +691,7 @@ void Memory::mkAxioms() const {
void Memory::resetGlobalData() {
resetLocalBids();
last_nonlocal_bid = 1;
+ did_pointer_store = false;
}
void Memory::resetLocalBids() {
@@ -1030,19 +1032,18 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
ret.non_local_blk_size.add(els.non_local_blk_size);
ret.non_local_blk_align.add(els.non_local_blk_align);
ret.non_local_blk_kind.add(els.non_local_blk_kind);
- ret.did_pointer_store |= els.did_pointer_store;
return ret;
}
bool Memory::operator<(const Memory &rhs) const {
// FIXME: remove this once we move to C++20
return
- tie(did_pointer_store, non_local_block_val, local_block_val,
+ tie(non_local_block_val, local_block_val,
non_local_block_liveness, local_block_liveness, local_blk_addr,
local_blk_size, local_blk_align, local_blk_kind, local_avail_space,
non_local_blk_writable, non_local_blk_size, non_local_blk_align,
non_local_blk_kind) <
- tie(rhs.did_pointer_store, rhs.non_local_block_val, rhs.local_block_val,
+ tie(rhs.non_local_block_val, rhs.local_block_val,
rhs.non_local_block_liveness, rhs.local_block_liveness,
rhs.local_blk_addr, rhs.local_blk_size, rhs.local_blk_align,
rhs.local_blk_kind,
@@ -1051,4 +1052,23 @@ bool Memory::operator<(const Memory &rhs) const {
rhs.non_local_blk_kind);
}
+#define P(msg, local, nonlocal) \
+ os << msg "\nLocal: " << m.local.simplify() \
+ << "\nNon-local: " << m.nonlocal.simplify() << "\n\n"
+
+ostream& operator<<(ostream &os, const Memory &m) {
+ if (memory_unused())
+ return os;
+ os << "\n\nMEMORY\n======\n";
+ P("BLOCK VALUE:", local_block_val, non_local_block_val);
+ P("BLOCK LIVENESS:", local_block_liveness, non_local_block_liveness);
+ 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
+ << "\nNON-LOCAL BLOCK WRITABLE: " << m.non_local_blk_writable
+ << "\nLOCAL AVAIL SPACE: " << m.local_avail_space
+ << "\nDid pointer store: " << did_pointer_store << '\n';
+}
+
}

MODIFY
ir/memory.h
ir/memory.h
@@ -162,8 +162,6 @@ public:
class Memory {
State *state;
- bool did_pointer_store = false;
-
smt::expr non_local_block_val; // array: (bid, offset) -> Byte
smt::expr local_block_val;
@@ -244,6 +242,8 @@ public:
// for container use only
bool operator<(const Memory &rhs) const;
+ friend std::ostream &operator<<(std::ostream &os, const Memory &m);
+
friend class Pointer;
};

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -89,8 +89,29 @@ const expr* FunctionExpr::lookup(const expr &key) const {
return I != fn.end() ? &I->second : nullptr;
}
+FunctionExpr FunctionExpr::simplify() const {
+ FunctionExpr newfn;
+ if (default_val)
+ newfn.default_val = default_val->simplify();
+
+ for (auto &[k, v] : fn) {
+ newfn.add(k.simplify(), v.simplify());
+ }
+ return newfn;
+}
+
bool FunctionExpr::operator<(const FunctionExpr &rhs) const {
return tie(fn, default_val) < tie(rhs.fn, rhs.default_val);
}
+ostream& operator<<(ostream &os, const FunctionExpr &f) {
+ os << "{\n";
+ for (auto &[k, v] : f) {
+ os << k << ": " << v << '\n';
+ }
+ if (f.default_val)
+ os << "default: " << *f.default_val << '\n';
+ return os << '}';
+}
+
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -92,11 +92,15 @@ public:
std::optional<expr> operator()(const expr &key) const;
const expr* lookup(const expr &key) const;
+ FunctionExpr simplify() const;
+
auto begin() const { return fn.begin(); }
auto end() const { return fn.end(); }
// for container use only
bool operator<(const FunctionExpr &rhs) const;
+
+ friend std::ostream& operator<<(std::ostream &os, const FunctionExpr &e);
};
}

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -50,7 +50,8 @@ void sym_exec(State &s) {
if (config::symexec_print_each_value) {
cout << "domain = " << s.returnDomain()
- << "\nreturn = " << s.returnVal().first << "\n\n";
+ << "\nreturn = " << s.returnVal().first
+ << s.returnMemory() << "\n\n";
}
}

print memory with SE verbose mode