Fix a bug regarding nonlocal ptr's align
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -320,7 +320,7 @@ expr Pointer::block_alignment() const {
expr::mkUInt(0, 8));
}
-expr Pointer::is_aligned(unsigned align, bool exact) const {
+expr Pointer::is_block_aligned(unsigned align, bool exact) const {
assert(align != 0);
if (!exact && align == 1)
return true;
@@ -330,6 +330,23 @@ expr Pointer::is_aligned(unsigned align, bool exact) const {
return exact ? blk_align == bits : blk_align.uge(bits);
}
+expr Pointer::is_aligned(unsigned align) const {
+ assert(align != 0);
+ if (align == 1)
+ return true;
+
+ auto bits = ilog2(align);
+
+ if (!observes_addresses())
+ // This is stricter than checking get_address(), but as addresses are not
+ // observed, program shouldn't be able to distinguish this from checking
+ // get_address()
+ return is_block_aligned(align, false) &&
+ get_offset().extract(bits - 1, 0) == 0;
+
+ return get_address().extract(bits - 1, 0) == 0;
+}
+
static pair<expr, expr> is_dereferenceable(const Pointer &p, const expr &bytes,
unsigned align, bool iswrite) {
expr block_sz = p.block_size();
@@ -767,7 +784,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
non_local_block_liveness
= non_local_block_liveness.store(short_bid, allocated);
state->addAxiom(p.block_size() == size_zext);
- state->addAxiom(p.is_aligned(align, true));
+ state->addAxiom(p.is_block_aligned(align, true));
state->addAxiom(p.get_alloc_type() == alloc_ty);
if (align_bits && observes_addresses())

MODIFY
ir/memory.h
ir/memory.h
@@ -127,7 +127,8 @@ public:
smt::expr inbounds() const;
smt::expr block_alignment() const;
- smt::expr is_aligned(unsigned align, bool exact = false) const;
+ smt::expr is_block_aligned(unsigned align, bool exact = false) const;
+ smt::expr is_aligned(unsigned align) const;
void is_dereferenceable(unsigned bytes, unsigned align, bool iswrite);
void is_dereferenceable(const smt::expr &bytes, unsigned align, bool iswrite);
void is_disjoint(const smt::expr &len1, const Pointer &ptr2,

ADD
tests/alive-tv/memory/align.src.ll
+define i32 @foo1(i32* %a) {
+ %v = load i32, i32* %a, align 4
+ %ptrint = ptrtoint i32* %a to i64
+ %maskedptr = and i64 %ptrint, 31
+ %maskcond = icmp eq i64 %maskedptr, 0
+ tail call void @llvm.assume(i1 %maskcond)
+ ret i32 %v
+}
+
+declare void @llvm.assume(i1)

ADD
tests/alive-tv/memory/align.tgt.ll
+define i32 @foo1(i32* %a) {
+ %v = load i32, i32* %a, align 32
+ %ptrint = ptrtoint i32* %a to i64
+ %maskedptr = and i64 %ptrint, 31
+ %maskcond = icmp eq i64 %maskedptr, 0
+ tail call void @llvm.assume(i1 %maskcond)
+ ret i32 %v
+}
+
+declare void @llvm.assume(i1)

Fix a bug regarding nonlocal ptr's align (#235)