From 834ce61226ec0f5f1ebf154de44606938aa0d28f Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Mon, 18 Sep 2023 11:47:45 +0100
Subject: [PATCH] support indirect calls with ptr attributes

---
 ir/instr.cpp                                  | 10 ++++----
 ir/pointer.cpp                                | 11 +++++++--
 ir/pointer.h                                  |  3 +++
 ir/state.cpp                                  |  8 ++++---
 .../indirect-call-ptr-attrbiutes.srctgt.ll    | 23 +++++++++++++++++++
 5 files changed, 45 insertions(+), 10 deletions(-)
 create mode 100644 tests/alive-tv/calls/indirect-call-ptr-attrbiutes.srctgt.ll

diff --git a/ir/instr.cpp b/ir/instr.cpp
index 98557a3ca..8cd40549f 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -2359,18 +2359,18 @@ StateValue FnCall::toSMT(State &s) const {
   ostringstream fnName_mangled;
   if (ptr) {
     fnName_mangled << "#indirect_call";
-    inputs.emplace_back(s.getAndAddPoisonUB(*ptr, true));
 
-    Pointer ptr(s.getMemory(), inputs.back().value);
-    s.addUB(ptr.isDereferenceable(1, 1, false));
+    Pointer p(s.getMemory(), s.getAndAddPoisonUB(*ptr, true).value);
+    inputs.emplace_back(p.reprWithoutAttrs(), true);
+    s.addUB(p.isDereferenceable(1, 1, false));
 
     Function::FnDecl decl;
     decl.output = &getType();
     for (auto &[arg, params] : args) {
       decl.inputs.emplace_back(&arg->getType(), params);
     }
-    s.addUB(expr::mkUF("#fndeclty", { std::move(ptr).release() },
-                       expr::mkUInt(0, 32)) == decl.hash());
+    s.addUB(expr::mkUF("#fndeclty", { inputs[0].value }, expr::mkUInt(0, 32)) ==
+            decl.hash());
   } else {
     fnName_mangled << fnName;
   }
diff --git a/ir/pointer.cpp b/ir/pointer.cpp
index b8b0813fa..faf6027ed 100644
--- a/ir/pointer.cpp
+++ b/ir/pointer.cpp
@@ -268,6 +268,14 @@ expr Pointer::blockSizeOffsetT() const {
   return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
 }
 
+expr Pointer::reprWithoutAttrs() const {
+  return p.extract(totalBits() - 1, bits_for_ptrattrs);
+}
+
+Pointer Pointer::mkPointerFromNoAttrs(const Memory &m, const expr &e) {
+  return { m, e.concat_zeros(bits_for_ptrattrs) };
+}
+
 Pointer Pointer::operator+(const expr &bytes) const {
   return { m, getBid(), getOffset() + bytes.zextOrTrunc(bits_for_offset),
            getAttrs() };
@@ -293,8 +301,7 @@ expr Pointer::addNoOverflow(const expr &offset) const {
 }
 
 expr Pointer::operator==(const Pointer &rhs) const {
-  return p.extract(totalBits() - 1, bits_for_ptrattrs) ==
-         rhs.p.extract(totalBits() - 1, bits_for_ptrattrs);
+  return reprWithoutAttrs() == rhs.reprWithoutAttrs();
 }
 
 expr Pointer::operator!=(const Pointer &rhs) const {
diff --git a/ir/pointer.h b/ir/pointer.h
index 6c9bccbbc..42ce7afb6 100644
--- a/ir/pointer.h
+++ b/ir/pointer.h
@@ -75,6 +75,9 @@ class Pointer {
   smt::expr release() && { return std::move(p); }
   unsigned bits() const { return p.bits(); }
 
+  smt::expr reprWithoutAttrs() const;
+  static Pointer mkPointerFromNoAttrs(const Memory &m, const smt::expr &e);
+
   Pointer operator+(unsigned) const;
   Pointer operator+(const smt::expr &bytes) const;
   void operator+=(const smt::expr &bytes);
diff --git a/ir/state.cpp b/ir/state.cpp
index 405f18ea7..3bed233d9 100644
--- a/ir/state.cpp
+++ b/ir/state.cpp
@@ -977,7 +977,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
 
   auto isgvar = [&](const auto &decl) {
     if (auto gv = getFn().getConstant(string_view(decl.name).substr(1)))
-      return Pointer(memory, fn_ptr).getAddress() ==
+      return Pointer::mkPointerFromNoAttrs(memory, fn_ptr).getAddress() ==
              Pointer(memory, (*this)[*gv].value).getAddress();
     return expr();
   };
@@ -1303,8 +1303,10 @@ void State::mkAxioms(State &tgt) {
   if (has_indirect_fncalls) {
     for (auto &decl : f.getFnDecls()) {
       if (auto gv = f.getConstant(string_view(decl.name).substr(1)))
-        addAxiom(expr::mkUF("#fndeclty", { (*this)[*gv].value },
-                            expr::mkUInt(0, 32)) == decl.hash());
+        addAxiom(
+          expr::mkUF("#fndeclty",
+                     { Pointer(memory, (*this)[*gv].value).reprWithoutAttrs() },
+                     expr::mkUInt(0, 32)) == decl.hash());
     }
   }
 }
diff --git a/tests/alive-tv/calls/indirect-call-ptr-attrbiutes.srctgt.ll b/tests/alive-tv/calls/indirect-call-ptr-attrbiutes.srctgt.ll
new file mode 100644
index 000000000..205b29841
--- /dev/null
+++ b/tests/alive-tv/calls/indirect-call-ptr-attrbiutes.srctgt.ll
@@ -0,0 +1,23 @@
+define i8 @src(ptr nocapture %0) {
+  %2 = call i8 %0(ptr null)
+  ret i8 %2
+}
+
+define i8 @tgt(ptr nocapture %0) {
+  %2 = icmp eq ptr %0, @_Z3fooPi
+  br i1 %2, label %then, label %else
+
+else:
+  %3 = call i8 %0(ptr null)
+  br label %ret
+
+then:
+  %4 = call i8 @_Z3fooPi(ptr null)
+  br label %ret
+
+ret:
+  %5 = phi i8 [ %3, %else ], [ %4, %then ]
+  ret i8 %5
+}
+
+declare i8 @_Z3fooPi(ptr)