Merge pull request #7556 from tautschnig/features/simp-is_null

Simplify tests of is-null that use integer types

Author: tautschnig

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");
+}

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

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?