From 5d87cf0f31cc418360eb130b4e3b8f9ab72f2c1f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 22 Feb 2023 12:12:01 +0000
Subject: [PATCH] Simplify tests of is-null that use integer types

Injecting casts to integer types should not hamper our ability to
simplify tests for null-ness. Such expressions emerge from Rust code,
see https://github.com/model-checking/kani/issues/2191.
---
 regression/cbmc/null8/main.c    | 12 +++++++++++
 regression/cbmc/null8/test.desc |  9 ++++++++
 src/util/simplify_expr_int.cpp  | 37 +++++++++++++++++++++++++++++++++
 3 files changed, 58 insertions(+)
 create mode 100644 regression/cbmc/null8/main.c
 create mode 100644 regression/cbmc/null8/test.desc

diff --git a/regression/cbmc/null8/main.c b/regression/cbmc/null8/main.c
new file mode 100644
index 00000000000..23bf5a67b31
--- /dev/null
+++ b/regression/cbmc/null8/main.c
@@ -0,0 +1,12 @@
+union U
+{
+  void *ptr;
+  __CPROVER_size_t n;
+};
+
+int main()
+{
+  int *p = __CPROVER_allocate(sizeof(int), 0);
+  union U u = {.ptr = p};
+  __CPROVER_assert(u.n != 0, "is not null");
+}
diff --git a/regression/cbmc/null8/test.desc b/regression/cbmc/null8/test.desc
new file mode 100644
index 00000000000..33b97c40e57
--- /dev/null
+++ b/regression/cbmc/null8/test.desc
@@ -0,0 +1,9 @@
+CORE new-smt-backend
+main.c
+
+Generated 1 VCC\(s\), 0 remaining after simplification
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 1bfa8a7d6e7..e2e7d6388f1 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1897,6 +1897,43 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
         }
       }
     }
+
+    if(config.ansi_c.NULL_is_zero)
+    {
+      const exprt &maybe_tc_op = skip_typecast(expr.op0());
+      if(maybe_tc_op.type().id() == ID_pointer)
+      {
+        // make sure none of the type casts lose information
+        const pointer_typet &p_type = to_pointer_type(maybe_tc_op.type());
+        bool bitwidth_unchanged = true;
+        const exprt *ep = &(expr.op0());
+        while(bitwidth_unchanged && ep->id() == ID_typecast)
+        {
+          if(auto t = type_try_dynamic_cast<bitvector_typet>(ep->type()))
+          {
+            bitwidth_unchanged = t->get_width() == p_type.get_width();
+          }
+          else
+            bitwidth_unchanged = false;
+
+          ep = &to_typecast_expr(*ep).op();
+        }
+
+        if(bitwidth_unchanged)
+        {
+          if(expr.id() == ID_equal || expr.id() == ID_ge || expr.id() == ID_le)
+          {
+            return changed(simplify_rec(
+              equal_exprt{maybe_tc_op, null_pointer_exprt{p_type}}));
+          }
+          else
+          {
+            return changed(simplify_rec(
+              notequal_exprt{maybe_tc_op, null_pointer_exprt{p_type}}));
+          }
+        }
+      }
+    }
   }
 
   // are we comparing with a typecast from bool?