memory: move local blk data to the Memory class
this gets rid of the annoying globals and allows shrinking constraint size since info is carried per path
MODIFY
ir/memory.cpp
ir/memory.cpp
#include "ir/memory.h"
#include "ir/state.h"
-#include "smt/exprs.h"
#include "util/compiler.h"
using namespace IR;
@@ -160,10 +159,6 @@ StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
}
-static FunctionExpr local_blk_addr, local_blk_size, local_blk_kind;
-static bool globals_initialized = false;
-
-
namespace IR {
Pointer::Pointer(const Memory &m, const char *var_name)
@@ -213,7 +208,7 @@ expr Pointer::get_address(bool simplify) const {
if (simplify && (get_bid() == 0).isTrue())
return offset;
- return offset + get_value("blk_addr", local_blk_addr, offset);
+ return offset + get_value("blk_addr", m.local_blk_addr, offset);
}
expr Pointer::block_size(bool simplify) const {
@@ -227,7 +222,7 @@ expr Pointer::block_size(bool simplify) const {
expr range = expr::mkUInt(0, m.bits_size_t - 1);
return expr::mkUInt(0, 1)
- .concat(get_value("blk_size", local_blk_size, range));
+ .concat(get_value("blk_size", m.local_blk_size, range));
}
expr Pointer::short_ptr() const {
@@ -335,7 +330,7 @@ expr Pointer::is_block_alive() const {
}
expr Pointer::get_alloc_type() const {
- return get_value("blk_kind", local_blk_kind, expr::mkUInt(0, 2));
+ return get_value("blk_kind", m.local_blk_kind, expr::mkUInt(0, 2));
}
expr Pointer::is_readonly() const {
@@ -408,12 +403,9 @@ static unsigned last_nonlocal_bid = 1;
Memory::Memory(State &state, bool little_endian)
: state(&state), little_endian(little_endian) {
- if (!globals_initialized) {
local_blk_addr.reset(expr::mkUInt(0, bits_size_t));
local_blk_size.reset(expr::mkUInt(0, bits_size_t - 1));
local_blk_kind.reset(expr::mkUInt(0, 2));
- globals_initialized = true;
- }
non_local_block_val = mk_val_array();
non_local_block_liveness = mk_liveness_array();
@@ -453,17 +445,10 @@ Memory::Memory(State &state, bool little_endian)
void Memory::resetGlobalData() {
resetLocalBids();
last_nonlocal_bid = 1;
- local_blk_addr.reset(expr());
- local_blk_size.reset(expr());
- local_blk_kind.reset(expr());
- globals_initialized = false;
}
void Memory::resetLocalBids() {
last_local_bid = 0;
- local_blk_addr.clear();
- local_blk_size.clear();
- local_blk_kind.clear();
}
pair<expr, vector<expr>> Memory::mkInput(const char *name) {
@@ -648,6 +633,9 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
els.non_local_block_liveness);
ret.local_block_liveness = expr::mkIf(cond, then.local_block_liveness,
els.local_block_liveness);
+ ret.local_blk_addr.add(els.local_blk_addr);
+ ret.local_blk_size.add(els.local_blk_size);
+ ret.local_blk_kind.add(els.local_blk_kind);
return ret;
}

MODIFY
ir/memory.h
ir/memory.h
#include "ir/state_value.h"
#include "ir/type.h"
#include "smt/expr.h"
+#include "smt/exprs.h"
#include <optional>
#include <ostream>
#include <string>
@@ -118,6 +119,10 @@ class Memory {
smt::expr non_local_block_liveness; // array: bid -> bool
smt::expr local_block_liveness;
+ smt::FunctionExpr local_blk_addr;
+ smt::FunctionExpr local_blk_size;
+ smt::FunctionExpr local_blk_kind;
+
smt::expr mk_val_array() const;
smt::expr mk_liveness_array() const;
@@ -128,8 +133,8 @@ public:
Memory(State &state, bool little_endian);
- void resetGlobalData();
- void resetLocalBids();
+ static void resetGlobalData();
+ static void resetLocalBids();
std::pair<smt::expr, std::vector<smt::expr>> mkInput(const char *name);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -19,6 +19,10 @@ State::State(const Function &f, bool source)
return_val.first = f.getType().getDummyValue(false);
}
+void State::resetGlobals() {
+ Memory::resetGlobalData();
+}
+
const StateValue& State::exec(const Value &v) {
assert(undef_vars.empty());
auto val = v.toSMT(*this);
@@ -200,12 +204,7 @@ void State::copyGlobalVarBidsFromSrc(const State &src) {
assert(src.isSource());
glbvar_bids = src.glbvar_bids;
- memory.resetLocalBids();
-}
-
-
-global_state_destroy::~global_state_destroy() {
- s.getMemory().resetGlobalData();
+ Memory::resetLocalBids();
}
}

MODIFY
ir/state.h
ir/state.h
@@ -66,6 +66,8 @@ private:
public:
State(const Function &f, bool source);
+ static void resetGlobals();
+
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
const ValTy& at(const Value &val) const;
@@ -114,12 +116,4 @@ private:
void addJump(const BasicBlock &dst, smt::expr &&domain);
};
-
-class global_state_destroy {
- State &s;
-public:
- global_state_destroy(State &s) : s(s) {}
- ~global_state_destroy();
-};
-
}

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -39,16 +39,16 @@ void FunctionExpr::add(expr &&key, expr &&val) {
ENSURE(fn.emplace(move(key), move(val)).second);
}
-void FunctionExpr::del(const expr &key) {
- fn.erase(key);
+void FunctionExpr::add(const FunctionExpr &other) {
+ fn.insert(other.fn.begin(), other.fn.end());
}
-void FunctionExpr::clear() {
- fn.clear();
+void FunctionExpr::del(const expr &key) {
+ fn.erase(key);
}
void FunctionExpr::reset(expr &&val) {
- clear();
+ fn.clear();
default_val = move(val);
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -29,8 +29,8 @@ class FunctionExpr {
public:
void add(expr &&key, expr &&val);
+ void add(const FunctionExpr &other);
void del(const expr &key);
- void clear();
void reset(smt::expr &&default_val);
expr operator()(expr &key) const;
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -348,8 +348,8 @@ Errors TransformVerify::verify() const {
}
}
+ State::resetGlobals();
State src_state(t.src, true), tgt_state(t.tgt, false);
- global_state_destroy gbl_destroy(src_state);
try {
sym_exec(src_state);

memory: move local blk data to the Memory class
this gets rid of the annoying globals and allows shrinking constraint size since info is carried per path