minor optimization to Memory::mkAxioms
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1093,14 +1093,19 @@ void Memory::mkAxioms(const Memory &tgt) const {
if (memory_unused())
return;
- auto nonlocal_used = [&](unsigned bid) {
- return bid < tgt.next_nonlocal_bid || is_globalvar(bid, true);
+ auto skip_bid = [&](unsigned bid) {
+ if (is_globalvar(bid, true))
+ return false;
+ if (is_fncall_mem(bid))
+ return true;
+ return bid >= tgt.next_nonlocal_bid;
};
// transformation can increase alignment
- unsigned align = ilog2(heap_block_alignment);
- for (unsigned bid = has_null_block; bid < num_nonlocals; ++bid) {
- if (!nonlocal_used(bid))
+ expr align = expr::mkUInt(ilog2(heap_block_alignment), 6);
+
+ for (unsigned bid = has_null_block; bid < num_nonlocals_src; ++bid) {
+ if (skip_bid(bid))
continue;
Pointer p(*this, bid, false);
Pointer q(tgt, bid, false);
@@ -1111,6 +1116,12 @@ void Memory::mkAxioms(const Memory &tgt) const {
if (!p_align.isConst() || !q_align.isConst())
state->addAxiom(p_align.ule(q_align));
}
+ for (unsigned bid = num_nonlocals_src; bid < num_nonlocals; ++bid) {
+ if (skip_bid(bid))
+ continue;
+ Pointer q(tgt, bid, false);
+ state->addAxiom(q.isHeapAllocated().implies(q.blockAlignment() == align));
+ }
if (!observesAddresses())
return;
@@ -1121,7 +1132,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
// Non-local blocks are disjoint.
// Ignore null pointer block
for (unsigned bid = has_null_block; bid < num_nonlocals; ++bid) {
- if (!nonlocal_used(bid) || is_fncall_mem(bid))
+ if (skip_bid(bid))
continue;
Pointer p1(*this, bid, false);
@@ -1136,7 +1147,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
// disjointness constraint
for (unsigned bid2 = bid + 1; bid2 < num_nonlocals; ++bid2) {
- if (!nonlocal_used(bid2) || is_fncall_mem(bid2))
+ if (skip_bid(bid2))
continue;
Pointer p2(*this, bid2, false);
disj &= p2.isBlockAlive()

minor optimization to Memory::mkAxioms