fix #941: supporting local allocations in tgt in asm mode

ir/memory.cpp

@@ -2051,7 +2051,7 @@ expr Memory::ptr2int(const expr &ptr) const {
 expr Memory::int2ptr(const expr &val0) const {
   assert(!memory_unused() && observesAddresses());
   if (state->getFn().getFnAttrs().has(FnAttrs::Asm)) {
-    DisjointExpr<expr> ret(expr{});
+    DisjointExpr<expr> ret(Pointer::mkNullPointer(*this).release());
     expr val = val0;
     OrExpr domain;
     bool processed_all = true;
@@ -2062,16 +2062,31 @@ expr Memory::int2ptr(const expr &val0) const {
     // Also, these pointers must have originated from ptr->int type punning
     // so they must have a (blk_addr bid) expression in them (+ some offset)
     for (auto [e, cond] : DisjointExpr<expr>(val, 5)) {
-      auto blks = e.get_apps_of("blk_addr");
+      auto blks = e.get_apps_of("blk_addr", "local_addr!");
       if (blks.empty()) {
         expr subst = false;
         if (cond.isNot(cond))
           subst = true;
         val = val.subst(cond, subst);
         continue;
       }
+      // There's only only possible bid in this expression
       if (blks.size() == 1) {
-        expr bid = blks.begin()->getFnArg(0);
+        auto &fn = *blks.begin();
+        expr bid;
+        if (fn.fn_name().starts_with("local_addr!")) {
+          for (auto &[bid0, addr] : local_blk_addr) {
+            auto blks = addr.get_apps_of("blk_addr", "local_addr!");
+            assert(blks.size() == 1);
+            if (blks.begin()->eq(fn)) {
+              bid = Pointer::mkLongBid(bid0, true);
+              break;
+            }
+          }
+        } else {
+          bid = fn.getFnArg(0);
+        }
+        assert(bid.isValid());
         Pointer base(*this, bid, expr::mkUInt(0, bits_for_offset));
         expr offset = (e - base.getAddress()).sextOrTrunc(bits_for_offset);
         ret.add(Pointer(*this, bid, offset).release(), cond);

smt/expr.cpp

@@ -812,8 +812,8 @@ expr expr::add_no_soverflow(const expr &rhs) const {
 
   if (rhs.isConst()) {
     auto v = IntSMin(bits()) - rhs;
-    return
-      rhs.isNegative().isTrue() ? sge(v) : sle(v - expr::mkUInt(1, sort()));
+    return rhs.isNegative().isTrue() ? sge(v)
+                                     : sle(v - expr::mkUInt(1, rhs.sort()));
   }
   if (isConst())
     return rhs.add_no_soverflow(*this);
@@ -2240,22 +2240,23 @@ set<expr> expr::leafs(unsigned max) const {
   return ret;
 }
 
-set<expr> expr::get_apps_of(const char *fn_name) const {
+set<expr> expr::get_apps_of(const char *fn_name, const char *prefix) const {
   C();
   vector<expr> worklist = { *this };
   unordered_set<Z3_ast> seen;
   set<expr> ret;
   do {
     auto val = std::move(worklist.back());
     worklist.pop_back();
-    if (!seen.emplace(val()).second || !val.isApp())
-      continue;
 
     for (unsigned i = 0, e = val.getFnNumArgs(); i < e; ++i) {
-      worklist.emplace_back(val.getFnArg(i));
+      expr arg = val.getFnArg(i);
+      if (arg.isApp() && seen.emplace(arg()).second)
+        worklist.emplace_back(std::move(arg));
     }
 
-    if (val.fn_name() == fn_name) {
+    auto str = val.fn_name();
+    if (str == fn_name || str.starts_with(prefix)) {
       ret.emplace(std::move(val));
     }
   } while (!worklist.empty());

smt/expr.h

@@ -360,7 +360,7 @@ class expr {
 
   std::set<expr> leafs(unsigned max = 64) const;
 
-  std::set<expr> get_apps_of(const char *fn_name) const;
+  std::set<expr> get_apps_of(const char *fn_name, const char *prefix) const;
 
   void printUnsigned(std::ostream &os) const;
   void printSigned(std::ostream &os) const;

tests/alive-tv/asm/malloc-in-tgt.srctgt.ll

@@ -0,0 +1,22 @@
+; TEST-ARGS: -tgt-is-asm
+; SKIP-IDENTITY
+
+define i32 @src() {
+  %1 = alloca i8, i32 0, align 1
+  store i8 0, ptr %1, align 1
+  ret i32 0
+}
+
+define i32 @tgt() {
+f:
+  %stack = tail call dereferenceable(64) ptr @myalloc(i32 64)
+  %0 = getelementptr inbounds i8, ptr %stack, i64 48
+  %1 = ptrtoint ptr %0 to i64
+  %a0_38 = add i64 %1, -16
+  %2 = inttoptr i64 %a0_38 to ptr
+  %3 = getelementptr i8, ptr %2, i64 15
+  store i8 0, ptr %3, align 1
+  ret i32 0
+}
+
+declare ptr @myalloc(i32) local_unnamed_addr allockind("alloc") allocsize(0)