From 1352eaa056182efe712ae56e93bc676758b75889 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Tue, 5 Dec 2023 17:26:21 +0000
Subject: [PATCH] asm mode: allow refinement of a memory byte with a ptr with
 an integer Type punning through memory is perfectly fine in asm

---
 ir/memory.cpp                          | 36 +++++++++++++++++++-------
 ir/memory.h                            |  1 +
 tests/alive-tv/asm/store-ptr.srctgt.ll | 15 +++++++++++
 3 files changed, 43 insertions(+), 9 deletions(-)
 create mode 100644 tests/alive-tv/asm/store-ptr.srctgt.ll

diff --git a/ir/memory.cpp b/ir/memory.cpp
index 3c4b85aa5..205a1f4f6 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -274,6 +274,11 @@ expr Byte::nonptrNonpoison() const {
   return p.extract(start + bits_poison_per_byte - 1, start);
 }
 
+expr Byte::boolNonptrNonpoison() const {
+  expr np = nonptrNonpoison();
+  return np == expr::mkInt(-1, np);
+}
+
 expr Byte::nonptrValue() const {
   if (!does_int_mem_access)
     return expr::mkUInt(0, bits_byte);
@@ -317,9 +322,6 @@ expr Byte::forceCastToInt() const {
 }
 
 expr Byte::refined(const Byte &other) const {
-  if (eq(other))
-    return true;
-
   // refinement if offset had non-ptr value
   expr v1 = nonptrValue();
   expr v2 = other.nonptrValue();
@@ -348,20 +350,36 @@ expr Byte::refined(const Byte &other) const {
     }
   }
 
-  // fast path: if we didn't do any ptr store, then all ptrs in memory were
-  // already there and don't need checking
   expr is_ptr = isPtr();
   expr is_ptr2 = other.isPtr();
+  bool asm_mode = other.m.getState().getFn().has(FnAttrs::Asm);
   expr ptr_cnstr;
-  if (!does_ptr_store || is_ptr.isFalse() || is_ptr2.isFalse()) {
+
+  // fast path: if we didn't do any ptr store, then all ptrs in memory were
+  // already there and don't need checking
+  if (!does_ptr_store || is_ptr.isFalse() || (!asm_mode && is_ptr2.isFalse())) {
     ptr_cnstr = *this == other;
   } else {
-    ptr_cnstr = !ptrNonpoison() ||
+    // allow ptr -> int type punning in asm mode
+    expr extra = false;
+    if (asm_mode) {
+      extra = !is_ptr2 &&
+              other.boolNonptrNonpoison() &&
+              forceCastToInt() == v2;
+    }
+    ptr_cnstr = ptrNonpoison().implies(
                   (other.ptrNonpoison() &&
                    ptrByteoffset() == other.ptrByteoffset() &&
-                   ptr().refined(other.ptr()));
+                   ptr().refined(other.ptr())) ||
+                  extra);
   }
-  return expr::mkIf(is_ptr == is_ptr2,
+
+  expr same_type = is_ptr == is_ptr2;
+  // allow ptr -> int type punning in asm mode
+  if (asm_mode)
+    same_type = is_ptr || !is_ptr2;
+
+  return expr::mkIf(same_type,
                     expr::mkIf(is_ptr, ptr_cnstr, int_cnstr),
                     // allow null ptr <-> zero
                     isPoison() ||
diff --git a/ir/memory.h b/ir/memory.h
index 58e777e56..697f19619 100644
--- a/ir/memory.h
+++ b/ir/memory.h
@@ -61,6 +61,7 @@ class Byte {
   smt::expr ptrValue() const;
   smt::expr ptrByteoffset() const;
   smt::expr nonptrNonpoison() const;
+  smt::expr boolNonptrNonpoison() const;
   smt::expr nonptrValue() const;
   smt::expr isPoison() const;
   smt::expr nonPoison() const;
diff --git a/tests/alive-tv/asm/store-ptr.srctgt.ll b/tests/alive-tv/asm/store-ptr.srctgt.ll
new file mode 100644
index 000000000..e70a235a0
--- /dev/null
+++ b/tests/alive-tv/asm/store-ptr.srctgt.ll
@@ -0,0 +1,15 @@
+; TEST-ARGS: -tgt-is-asm
+; SKIP-IDENTITY
+
+@dst = external global i64
+@ptr = external global ptr
+
+define void @src() {
+   store ptr @dst, ptr @ptr, align 8
+   ret void
+}
+
+define void @tgt() {
+   store i64 ptrtoint (ptr @dst to i64), ptr @ptr, align 8
+   ret void
+}