memory: support increase of alignment
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -331,14 +331,18 @@ expr Pointer::get_offset() const {
expr Pointer::get_value(const char *name, const FunctionExpr &local_fn,
const FunctionExpr &nonlocal_fn,
- const expr &ret_type) const {
+ const expr &ret_type, bool src_name) const {
auto bid = get_short_bid();
expr non_local;
if (auto val = nonlocal_fn.lookup(bid))
non_local = *val;
- else
- non_local = expr::mkUF(name, { bid }, ret_type);
+ else {
+ string uf = name;
+ if (src_name)
+ uf += m.state->isSource() ? "_src" : "_tgt";
+ non_local = expr::mkUF(uf.c_str(), { bid }, ret_type);
+ }
if (auto local = local_fn(bid))
return expr::mkIf(is_local(), *local, non_local);
@@ -426,7 +430,7 @@ expr Pointer::inbounds() const {
expr Pointer::block_alignment() const {
return get_value("blk_align", m.local_blk_align, m.non_local_blk_align,
- expr::mkUInt(0, 8));
+ expr::mkUInt(0, 8), true);
}
expr Pointer::is_block_aligned(unsigned align, bool exact) const {
@@ -824,10 +828,17 @@ Memory::Memory(State &state) : state(&state) {
assert(bits_for_offset <= bits_size_t);
}
-void Memory::mkAxioms() const {
- if (memory_unused() || !state->isSource())
+void Memory::mkAxioms(const Memory &other) const {
+ assert(state->isSource() && !other.state->isSource());
+ if (memory_unused())
return;
+ // transformation can increase alignment
+ for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
+ state->addAxiom(Pointer(*this, bid, false).block_alignment().ule(
+ Pointer(other, bid, false).block_alignment()));
+ }
+
if (observes_addresses() && num_nonlocals > 0) {
state->addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);

MODIFY
ir/memory.h
ir/memory.h
@@ -88,7 +88,7 @@ class Pointer {
smt::expr get_value(const char *name, const smt::FunctionExpr &local_fn,
const smt::FunctionExpr &nonlocal_fn,
- const smt::expr &ret_type) const;
+ const smt::expr &ret_type, bool src_name = false) const;
public:
Pointer(const Memory &m, const char *var_name,
@@ -193,7 +193,7 @@ public:
Memory(State &state);
- void mkAxioms() const;
+ void mkAxioms(const Memory &other) const;
static void resetGlobalData();
static void resetLocalBids();

MODIFY
ir/state.cpp
ir/state.cpp
@@ -304,7 +304,7 @@ void State::syncSEdataWithSrc(const State &src) {
void State::mkAxioms(State &tgt) {
assert(isSource() && !tgt.isSource());
- memory.mkAxioms();
+ memory.mkAxioms(tgt.memory);
// axioms for function calls
for (auto &[fn, data] : fn_call_data) {

memory: support increase of alignment