tweaks to semantics of aligned malloc

ensure return is null if align is not power of 2 or size is not a multiple of align
AliveToolkit · Oct 22, 2023 · 8771c44 · 8771c44
1 parent e1ca0c0
commit 8771c44
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 7 deletions.
diff --git a/ir/attrs.cpp b/ir/attrs.cpp
@@ -332,7 +332,7 @@ static expr merge(pair<AndExpr, expr> e) {
 static expr
 encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
                uint64_t derefOrNullBytes, uint64_t align, bool nonnull,
-               bool nocapture, const expr &deref_expr, Value *allocalign) {
+               bool nocapture, const expr &allocsize, Value *allocalign) {
   auto &m = s.getMemory();
   Pointer p(m, ptrvalue);
   expr non_poison(true);
@@ -342,7 +342,7 @@ encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
 
   non_poison &= p.isNocapture().implies(nocapture);
 
-  if (derefBytes || derefOrNullBytes || deref_expr.isValid()) {
+  if (derefBytes || derefOrNullBytes || allocsize.isValid()) {
     // dereferenceable, byval (ParamAttrs), dereferenceable_or_null
     if (derefBytes)
       s.addUB(merge(Pointer(m, ptrvalue)
@@ -351,17 +351,23 @@ encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
       s.addUB(p.isNull() ||
               merge(Pointer(m, ptrvalue)
                       .isDereferenceable(derefOrNullBytes, align, false,true)));
-    if (deref_expr.isValid())
+    if (allocsize.isValid())
       s.addUB(p.isNull() ||
               merge(Pointer(m, ptrvalue)
-                      .isDereferenceable(deref_expr, align, false, true)));
+                      .isDereferenceable(allocsize, align, false, true)));
   } else if (align != 1)
     non_poison &= Pointer(m, ptrvalue).isAligned(align);
 
   if (allocalign) {
+    Pointer p(m, ptrvalue);
     auto &align = s[*allocalign];
+    auto bw = max(align.bits(), allocsize.bits());
     non_poison &= align.non_poison;
-    non_poison &= Pointer(m, ptrvalue).isAligned(align.value);
+    // pointer must be null if alignment is not a power of 2
+    // or size is not a multiple of alignment
+    non_poison &= p.isNull() ||
+      (p.isAligned(align.value) &&
+       allocsize.zextOrTrunc(bw).urem(align.value.zextOrTrunc(bw)) == 0);
   }
   return non_poison;
 }

diff --git a/ir/instr.cpp b/ir/instr.cpp
@@ -2074,7 +2074,7 @@ pair<uint64_t, uint64_t> FnCall::getMaxAllocSize() const {
   return { UINT64_MAX, getAlign() };
 }
 
-static Value* get_align_arg(const vector<pair<Value*, ParamAttrs>> args) {
+static Value* get_align_arg(const vector<pair<Value*, ParamAttrs>> &args) {
   for (auto &[arg, attrs] : args) {
     if (attrs.has(ParamAttrs::AllocAlign))
       return arg;
@@ -2420,11 +2420,23 @@ StateValue FnCall::toSMT(State &s) const {
     expr nonnull = attrs.isNonNull() ? expr(true)
                                      : expr::mkBoolVar("malloc_never_fails");
     // FIXME: alloc-family below
+    // FIXME: take allocalign into account
     auto [p_new, allocated]
       = m.alloc(&size, getAlign(), Memory::MALLOC, np_size, nonnull);
 
+    // pointer must be null if:
+    // 1) alignment is not a power of 2
+    // 2) size is not a multiple of alignment
+    expr is_not_null = true;
+    if (auto *allocalign = getAlignArg()) {
+      auto &align = s[*allocalign].value;
+      auto bw = max(align.bits(), size.bits());
+      is_not_null &= align.isPowerOf2();
+      is_not_null &= size.zextOrTrunc(bw).urem(align.zextOrTrunc(bw)) == 0;
+    }
+
     expr nullp = Pointer::mkNullPointer(m)();
-    expr ret = expr::mkIf(allocated, p_new, nullp);
+    expr ret = expr::mkIf(allocated && is_not_null, p_new, nullp);
 
     // TODO: In C++ we need to throw an exception if the allocation fails.