LLVM semantics: alignment can be a non-power-of-2 if ptr == null

AliveToolkit · Nov 29, 2023 · ff9d8e8 · ff9d8e8
1 parent cdf792b
commit ff9d8e8
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 8 deletions.
diff --git a/ir/pointer.cpp b/ir/pointer.cpp
@@ -355,12 +355,10 @@ expr Pointer::isBlockAligned(uint64_t align, bool exact) const {
 }
 
 expr Pointer::isAligned(uint64_t align) {
-  if (align == 0)
+  if (align == 0 || !is_power2(align))
     return isNull();
   if (align == 1)
     return true;
-  if (!is_power2(align))
-    return false;
 
   auto offset = getOffset();
   if (isUndef(offset))
@@ -395,10 +393,9 @@ expr Pointer::isAligned(const expr &align) {
     return isAligned(n);
 
   return
-    expr::mkIf(align == 0,
+    expr::mkIf(align == 0 || !align.isPowerOf2(),
                isNull(),
-               align.isPowerOf2() &&
-                 getAddress().urem(align.zextOrTrunc(bits_ptr_address)) == 0);
+               getAddress().urem(align.zextOrTrunc(bits_ptr_address)) == 0);
 }
 
 static pair<expr, expr> is_dereferenceable(Pointer &p,

diff --git a/smt/expr.cpp b/smt/expr.cpp
@@ -743,7 +743,7 @@ expr expr::udiv(const expr &rhs) const {
 }
 
 expr expr::srem(const expr &rhs) const {
-  if (eq(rhs) || (isSMin() && rhs.isAllOnes()))
+  if (eq(rhs) || isZero() || (isSMin() && rhs.isAllOnes()))
     return mkUInt(0, sort());
 
   if (rhs.isZero())
@@ -757,7 +757,7 @@ expr expr::srem(const expr &rhs) const {
 
 expr expr::urem(const expr &rhs) const {
   C();
-  if (eq(rhs))
+  if (eq(rhs) || isZero())
     return mkUInt(0, sort());
 
   uint64_t n, log;

diff --git a/tests/alive-tv/assume/align-nonpow2.srctgt.ll b/tests/alive-tv/assume/align-nonpow2.srctgt.ll
@@ -0,0 +1,13 @@
+; ERROR: Source is more defined than target
+
+define void @src(i32 %align) {
+  call void @llvm.assume(i1 true) ["align"(ptr null, i32 5)]
+  call void @llvm.assume(i1 true) ["align"(ptr null, i32 %align)]
+  ret void
+}
+
+define void @tgt(i32 %align) {
+  unreachable
+}
+
+declare void @llvm.assume(i1)