fix alignment of null block when null_is_dereferenceable is enabled
MODIFY
BugList.md
BugList.md
@@ -78,7 +78,6 @@ Please contact us or submit a PR if something is missing or inaccurate.
71. InstSimplify: xor pattern miscompiles undef lane (https://llvm.org/PR58977)
72. llvm.canonicalize() folding incorrect for denormals (https://llvm.org/PR59245)
73. InstCombine: incorrect fabs formation (https://llvm.org/PR59279)
-74. InstCombine: incorrect increase of alignment of load with null_pointer_is_valid (https://llvm.org/PR59281)
### Bugs found in Z3

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1161,7 +1161,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
return;
auto skip_bid = [&](unsigned bid) {
- if (bid == 0 && has_null_block && !null_is_dereferenceable)
+ if (bid == 0 && has_null_block)
return true;
if (is_globalvar(bid, true))
return false;
@@ -1173,6 +1173,11 @@ void Memory::mkAxioms(const Memory &tgt) const {
// transformation can increase alignment
expr align = expr::mkUInt(ilog2(heap_block_alignment), 6);
+ if (null_is_dereferenceable && has_null_block) {
+ state->addAxiom(Pointer::mkNullPointer(*this).blockAlignment() == -1u);
+ state->addAxiom(Pointer::mkNullPointer(tgt).blockAlignment() == -1u);
+ }
+
for (unsigned bid = 0; bid < num_nonlocals_src; ++bid) {
if (skip_bid(bid))
continue;

ADD
tests/alive-tv/memory/nullptr-align.srctgt.ll
+define i8 @src() null_pointer_is_valid {
+ %v = load i8, ptr null, align 4
+ ret i8 %v
+}
+
+define i8 @tgt() null_pointer_is_valid {
+ %v = load i8, ptr null, align 8
+ ret i8 %v
+}

fix alignment of null block when null_is_dereferenceable is enabled