fix #930: disable stores to byval nowrite function args

ir/memory.cpp

@@ -281,8 +281,9 @@ expr Byte::nonptrValue() const {
 
 expr Byte::isPoison() const {
   expr np = nonptrNonpoison();
-  if (byte_has_ptr_bit() && bits_poison_per_byte == 1) {
-    assert(!np.isValid() || ptrNonpoison().eq(np == 1));
+  if (!does_int_mem_access ||
+      (byte_has_ptr_bit() && bits_poison_per_byte == 1)) {
+    assert(!np.isValid() || !does_int_mem_access || ptrNonpoison().eq(np == 1));
     return np == 0;
   }
   return expr::mkIf(isPtr(), !ptrNonpoison(), np != expr::mkInt(-1, np));
@@ -1251,9 +1252,9 @@ void Memory::syncWithSrc(const Memory &src) {
   // TODO: copy alias info for fn return ptrs from src?
 }
 
-void Memory::markByVal(unsigned bid) {
+void Memory::markByVal(unsigned bid, bool is_const) {
   assert(is_globalvar(bid, false));
-  byval_blks.emplace_back(bid);
+  byval_blks.emplace_back(bid, is_const);
 }
 
 expr Memory::mkInput(const char *name, const ParamAttrs &attrs) {
@@ -1267,7 +1268,7 @@ expr Memory::mkInput(const char *name, const ParamAttrs &attrs) {
   AliasSet alias(*this);
   alias.setMayAliasUpTo(false, max_bid);
 
-  for (auto byval_bid : byval_blks) {
+  for (auto [byval_bid, is_const] : byval_blks) {
     state->addAxiom(bid != byval_bid);
     alias.setNoAlias(false, byval_bid);
   }
@@ -1378,7 +1379,7 @@ Memory::mkFnRet(const char *name0, const vector<PtrInput> &ptr_inputs,
   auto alias = escaped_local_blks;
   alias.setMayAliasUpTo(false, max_nonlocal_bid);
 
-  for (auto byval_bid : byval_blks) {
+  for (auto [byval_bid, is_const] : byval_blks) {
     nonlocal &= bid != byval_bid;
     alias.setNoAlias(false, byval_bid);
   }
@@ -2072,8 +2073,6 @@ expr Memory::blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid,
           blockValRefined(tgt.getMemory(), bid, false, ptr_offset, undef));
   }
 
-  assert(src.isWritable().eq(tgt.isWritable()));
-
   expr aligned(true);
   expr src_align = src.blockAlignment();
   expr tgt_align = tgt.blockAlignment();
@@ -2238,7 +2237,6 @@ Memory Memory::mkIf(const expr &cond, Memory &&then, Memory &&els) {
   ret.non_local_blk_size.add(els.non_local_blk_size);
   ret.non_local_blk_align.add(els.non_local_blk_align);
   ret.non_local_blk_kind.add(els.non_local_blk_kind);
-  assert(then.byval_blks == els.byval_blks);
   ret.escaped_local_blks.unionWith(els.escaped_local_blks);
 
   for (const auto &[expr, alias] : els.ptr_alias) {

ir/memory.h

@@ -146,7 +146,7 @@ class Memory {
   smt::FunctionExpr non_local_blk_align;
   smt::FunctionExpr non_local_blk_kind;
 
-  std::vector<unsigned> byval_blks;
+  std::vector<std::pair<unsigned, bool>> byval_blks; /// <bid, is_const>
   AliasSet escaped_local_blks;
 
   bool hasEscapedLocals() const {
@@ -241,7 +241,7 @@ class Memory {
   static void resetGlobals();
   void syncWithSrc(const Memory &src);
 
-  void markByVal(unsigned bid);
+  void markByVal(unsigned bid, bool is_const);
   smt::expr mkInput(const char *name, const ParamAttrs &attrs);
   std::pair<smt::expr, smt::expr> mkUndefInput(const ParamAttrs &attrs) const;
 

ir/pointer.cpp

@@ -552,13 +552,20 @@ expr Pointer::isWritable() const {
     non_local &= bid.ult(num_nonlocals_src);
   if (has_null_block && null_is_dereferenceable)
     non_local |= bid == 0;
+
+  // check for non-writable byval blocks (which are non-local)
+  for (auto [byval, is_const] : m.byval_blks) {
+    if (is_const)
+      non_local &= bid != byval;
+  }
+
   return isLocal() || non_local;
 }
 
 expr Pointer::isByval() const {
   auto this_bid = getShortBid();
   expr non_local(false);
-  for (auto bid : m.byval_blks) {
+  for (auto [bid, is_const] : m.byval_blks) {
     non_local |= this_bid == bid;
   }
   return !isLocal() && non_local;

ir/value.cpp

@@ -1,9 +1,10 @@
 // Copyright (c) 2018-present The Alive2 Authors.
 // Distributed under the MIT license that can be found in the LICENSE file.
 
+#include "ir/value.h"
+#include "ir/function.h"
 #include "ir/instr.h"
 #include "ir/globals.h"
-#include "ir/value.h"
 #include "smt/expr.h"
 #include "util/compiler.h"
 #include "util/config.h"
@@ -210,7 +211,9 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
     unsigned bid;
     expr size = expr::mkUInt(attrs.blockSize, bits_size_t);
     val = get_global(s, smt_name, size, attrs.align, false, bid);
-    s.getMemory().markByVal(bid);
+    bool is_const = hasAttribute(ParamAttrs::NoWrite) ||
+                    !s.getFn().getFnAttrs().mem.canWrite(MemoryAccess::Args);
+    s.getMemory().markByVal(bid, is_const);
   } else {
     auto name = getSMTName(child);
     val = ty.mkInput(s, name.c_str(), attrs);

tests/alive-tv/attrs/byval-readonly-param.srctgt.ll

@@ -0,0 +1,8 @@
+define void @src(ptr readonly byval(i8) %p) {
+  store i8 0, ptr %p
+  ret void
+}
+
+define void @tgt(ptr readonly byval(i8) %p) {
+  unreachable
+}