memory: handle alignment
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -33,6 +33,10 @@ expr Pointer::get_offset() const {
return p.extract(bits_for_bids() + m.bits_for_offset - 1, bits_for_bids());
}
+expr Pointer::get_address() const {
+ return m.block_addr(get_bid());
+}
+
void Pointer::operator++(void) {
*this += expr::mkUInt(1, m.bits_for_offset);
}
@@ -63,7 +67,13 @@ expr Pointer::inbounds() const {
return offset.zextOrTrunc(m.bits_size_t).ule(block_sz);
}
-void Pointer::is_dereferenceable(const expr &bytes) {
+expr Pointer::is_aligned(unsigned align) const {
+ if (auto bits = ilog2(align))
+ return get_address().extract(bits-1, 0) == 0;
+ return true;
+}
+
+void Pointer::is_dereferenceable(const expr &bytes, unsigned align) {
expr block_sz = m.blocks_size.load(get_bid());
expr offset = get_offset();
@@ -71,22 +81,37 @@ void Pointer::is_dereferenceable(const expr &bytes) {
m.state->addUB((offset + bytes).zextOrTrunc(m.bits_size_t).ule(block_sz));
m.state->addUB(offset.add_no_uoverflow(bytes));
- // 2) check block is alive
+ // 2) check block's address is aligned
+ m.state->addUB(is_aligned(align));
+
+ // 3) check block is alive
// TODO
}
-void Pointer::is_dereferenceable(unsigned bytes) {
- is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset));
+void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
+ is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
}
+string Memory::mkName(const char *str) const {
+ return string(str) + (state->isSource() ? "_src" : "_tgt");
+}
+
+expr Memory::block_addr(const expr &bid) const {
+ auto name = mkName("blks_addr");
+ return expr::mkUF(name.c_str(), { bid }, expr::mkUInt(0, bits_size_t));
+}
+
Memory::Memory(State &state) : state(&state) {
unsigned bits_bids = bits_for_local_bid + bits_for_nonlocal_bid;
- blocks_size = expr::mkArray("blks_size",
+
+ auto size_name = mkName("blks_size");
+ blocks_size = expr::mkArray(size_name.c_str(),
expr::mkUInt(0, bits_bids),
expr::mkUInt(0, bits_size_t));
- blocks_val = expr::mkArray("blks_val",
+ auto val_name = mkName("blks_val");
+ blocks_val = expr::mkArray(val_name.c_str(),
expr::mkUInt(0, bits_bids + bits_for_offset),
expr::mkUInt(0, 8 + 1)); // val+poison bit
@@ -105,7 +130,8 @@ pair<expr, vector<expr>> Memory::mkInput(const char *name) {
expr Memory::alloc(const expr &bytes, unsigned align, bool local) {
Pointer p(*this, last_bid++, local);
- // TODO: handle alignment
+ state->addPre(p.is_aligned(align));
+
expr size = bytes.zextOrTrunc(bits_size_t);
blocks_size = blocks_size.store(p.get_bid(), size);
memset(p(), { expr::mkUInt(0, 8), false }, size, align);
@@ -121,8 +147,7 @@ void Memory::store(const expr &p, const StateValue &v, unsigned align) {
unsigned bytes = divide_up(bits, 8);
Pointer ptr(*this, p);
- // TODO: handle alignment
- ptr.is_dereferenceable(bytes);
+ ptr.is_dereferenceable(bytes, align);
expr poison = v.non_poison.toBVBool();
expr val = v.value.zext(bytes * 8 - bits);
@@ -137,8 +162,7 @@ void Memory::store(const expr &p, const StateValue &v, unsigned align) {
StateValue Memory::load(const expr &p, unsigned bits, unsigned align) {
unsigned bytes = divide_up(bits, 8);
Pointer ptr(*this, p);
- // TODO: handle alignment
- ptr.is_dereferenceable(bytes);
+ ptr.is_dereferenceable(bytes, align);
expr val, non_poison;
bool first = true;
@@ -164,8 +188,7 @@ StateValue Memory::load(const expr &p, unsigned bits, unsigned align) {
void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,
unsigned align) {
Pointer ptr(*this, p);
- // TODO: handle alignment
- ptr.is_dereferenceable(bytes);
+ ptr.is_dereferenceable(bytes, align);
expr store_val = val.non_poison.toBVBool().concat(val.value);
uint64_t n;
@@ -187,9 +210,8 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,
void Memory::memcpy(const expr &d, const expr &s, const expr &bytes,
unsigned align_dst, unsigned align_src) {
Pointer dst(*this, d), src(*this, s);
- // TODO: handle alignment
- dst.is_dereferenceable(bytes);
- src.is_dereferenceable(bytes);
+ dst.is_dereferenceable(bytes, align_dst);
+ src.is_dereferenceable(bytes, align_src);
// TODO
}

MODIFY
ir/memory.h
ir/memory.h
#include "ir/state_value.h"
#include "smt/expr.h"
+#include <string>
#include <utility>
#include <vector>
@@ -26,6 +27,7 @@ public:
smt::expr get_bid() const;
smt::expr get_offset() const;
+ smt::expr get_address() const;
const smt::expr& operator()() const { return p; }
smt::expr&& release() { return std::move(p); }
@@ -40,8 +42,9 @@ public:
smt::expr uge(const Pointer &rhs) const;
smt::expr inbounds() const;
- void is_dereferenceable(unsigned bytes);
- void is_dereferenceable(const smt::expr &bytes);
+ smt::expr is_aligned(unsigned align) const;
+ void is_dereferenceable(unsigned bytes, unsigned align);
+ void is_dereferenceable(const smt::expr &bytes, unsigned align);
};
@@ -59,6 +62,9 @@ class Memory {
unsigned last_bid = 0;
unsigned last_idx_ptr = 0;
+ std::string mkName(const char *str) const;
+ smt::expr block_addr(const smt::expr &bid) const;
+
public:
Memory(State &state);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -11,7 +11,8 @@ using namespace std;
namespace IR {
-State::State(const Function &f) : f(f), memory(*this) {
+State::State(const Function &f, bool source)
+ : f(f), source(source), memory(*this) {
predecessor_data[&f.getFirstBB()].try_emplace(nullptr,
DomainTy(true, set<expr>()),
*this);

MODIFY
ir/state.h
ir/state.h
@@ -30,6 +30,9 @@ public:
private:
const Function &f;
+ bool source;
+ smt::expr precondition;
+
const BasicBlock *current_bb;
std::set<smt::expr> quantified_vars;
@@ -57,7 +60,7 @@ private:
bool returned = false;
public:
- State(const Function &f);
+ State(const Function &f, bool source);
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
@@ -72,14 +75,18 @@ public:
void addCondJump(const StateValue &cond, const BasicBlock &dst_true,
const BasicBlock &dst_false);
void addReturn(const StateValue &val);
+
+ void addPre(smt::expr &&cond) { precondition &= std::move(cond); }
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
+
void addQuantVar(const smt::expr &var);
void addUndefVar(const smt::expr &var);
void resetUndefVars();
- auto& getMemory() { return memory; }
auto& getFn() const { return f; }
+ auto& getMemory() { return memory; }
+ auto& getPre() const { return precondition; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }
@@ -87,6 +94,9 @@ public:
auto& returnDomain() const { return return_domain; }
auto& returnVal() const { return return_val; }
+ // whether this is source or target program
+ bool isSource() const { return source; }
+
private:
void addJump(const BasicBlock &dst, smt::expr &&domain);
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -215,18 +215,20 @@ static void check_refinement(Errors &errs, Transform &t,
check_each_var);
};
+ expr pre = src_state.getPre() && tgt_state.getPre();
+
Solver::check({
- { preprocess(t, qvars, ap.second, dom_a.notImplies(dom_b)),
+ { preprocess(t, qvars, ap.second, pre && dom_a.notImplies(dom_b)),
[&](const Result &r) {
err(r, false, "Source is more defined than target");
}},
{ preprocess(t, qvars, ap.second,
- dom_a && a.non_poison.notImplies(b.non_poison)),
+ pre && dom_a && a.non_poison.notImplies(b.non_poison)),
[&](const Result &r) {
err(r, true, "Target is more poisonous than source");
}},
{ preprocess(t, qvars, ap.second,
- dom_a && a.non_poison && a.value != b.value),
+ pre && dom_a && a.non_poison && a.value != b.value),
[&](const Result &r) {
err(r, true, "Value mismatch");
}}
@@ -247,7 +249,7 @@ TransformVerify::TransformVerify(Transform &t, bool check_each_var) :
Errors TransformVerify::verify() const {
Value::reset_gbl_id();
- State src_state(t.src), tgt_state(t.tgt);
+ State src_state(t.src, true), tgt_state(t.tgt, false);
try {
sym_exec(src_state);

memory: handle alignment