From 4e1ca5a859aae8314cbc294bb884233072d909e6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Oct 2026 18:09:19 +0000
Subject: [PATCH] Fix integer-pointer cast extension to match GCC semantics

The SAT and SMT2 back ends disagreed on how to extend integer-to-pointer
and pointer-to-integer casts when the types have different widths:
- SAT: zero-extended in both directions
- SMT2: sign-extended in both directions

GCC documents that integer-to-pointer conversion extends according to
the signedness of the source integer type, and pointer-to-integer
conversion sign-extends. Neither back end matched GCC on all cases.

Fix SAT back end (bv_pointers.cpp):
- Integer to pointer: sign-extend for signed sources, zero-extend for
  unsigned sources (was: always zero-extend).
- Pointer to integer: sign-extend (was: zero-extend).

Fix SMT2 back end (smt2_conv.cpp):
- Integer to pointer: extend according to source signedness (was:
  always sign-extend).
- Pointer to integer: already correct (sign-extend), no change.

Fixes #9212

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 regression/cbmc/Pointer_cast_extend/main.c    | 23 ++++++++++++++++++
 regression/cbmc/Pointer_cast_extend/test.desc |  8 +++++++
 src/solvers/flattening/bv_pointers.cpp        | 24 ++++++++++++++-----
 src/solvers/smt2/smt2_conv.cpp                | 14 +++++++----
 4 files changed, 59 insertions(+), 10 deletions(-)
 create mode 100644 regression/cbmc/Pointer_cast_extend/main.c
 create mode 100644 regression/cbmc/Pointer_cast_extend/test.desc

diff --git a/regression/cbmc/Pointer_cast_extend/main.c b/regression/cbmc/Pointer_cast_extend/main.c
new file mode 100644
index 000000000000..f2302e074404
--- /dev/null
+++ b/regression/cbmc/Pointer_cast_extend/main.c
@@ -0,0 +1,23 @@
+int nondet_int(void);
+unsigned nondet_unsigned(void);
+
+int main(void)
+{
+  // signed int to wider pointer: sign-extends
+  int i = nondet_int();
+  __CPROVER_assume(i < 0 && i > -5);
+  char *p1 = (char *)i;
+  unsigned long u1 = (unsigned long)p1;
+  __CPROVER_assert(
+    u1 > 0xFFFFFFFFul, "signed int to wider pointer sign-extends");
+
+  // unsigned int to wider pointer: zero-extends
+  unsigned v = nondet_unsigned();
+  __CPROVER_assume(v > 0x80000000u && v < 0x80001000u);
+  char *p2 = (char *)v;
+  unsigned long u2 = (unsigned long)p2;
+  __CPROVER_assert(
+    u2 < 0x100000000ul, "unsigned to wider pointer zero-extends");
+
+  return 0;
+}
diff --git a/regression/cbmc/Pointer_cast_extend/test.desc b/regression/cbmc/Pointer_cast_extend/test.desc
new file mode 100644
index 000000000000..a5790e40f019
--- /dev/null
+++ b/regression/cbmc/Pointer_cast_extend/test.desc
@@ -0,0 +1,8 @@
+CORE broken-cprover-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 52482e8b060a..750116b44587 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -403,11 +403,23 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
     {
       // Cast from a bitvector type to pointer.
-      // We just do a zero extension.
+      // Extend according to the signedness of the source type (GCC
+      // semantics for implementation-defined integer-to-pointer
+      // conversion).
 
-      const bvt &op_bv=convert_bv(op);
+      const bvt &op_bv = convert_bv(op);
 
-      return bv_utils.zero_extension(op_bv, bits);
+      if(
+        op_type.id() == ID_signedbv ||
+        (op_type.id() == ID_c_enum &&
+         to_c_enum_type(op_type).underlying_type().id() == ID_signedbv))
+      {
+        return bv_utils.sign_extension(op_bv, bits);
+      }
+      else
+      {
+        return bv_utils.zero_extension(op_bv, bits);
+      }
     }
   }
   else if(expr.id()==ID_if)
@@ -719,10 +731,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     // pointer to int
     bvt op0 = convert_bv(to_typecast_expr(expr).op());
 
-    // squeeze it in!
-    std::size_t width=boolbv_width(expr.type());
+    // GCC sign-extends pointers converted to wider integer types.
+    std::size_t width = boolbv_width(expr.type());
 
-    return bv_utils.zero_extension(op0, width);
+    return bv_utils.sign_extension(op0, width);
   }
 
   return SUB::convert_bitvector(expr);
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 752fe9fab3ca..f8f0c1511198 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -3425,11 +3425,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         convert_expr(src);
       else if(from_width<to_width)
       {
-        out << "((_ sign_extend "
-            << (to_width-from_width)
-            << ") ";
+        // Extend according to the signedness of the source type (GCC
+        // semantics for implementation-defined integer-to-pointer
+        // conversion).
+        if(src_type.id() == ID_signedbv)
+          out << "((_ sign_extend ";
+        else
+          out << "((_ zero_extend ";
+
+        out << (to_width - from_width) << ") ";
         convert_expr(src);
-        out << ")"; // sign_extend
+        out << ")";
       }
       else // from_width>to_width
       {