Move is_null_pointer to constant_exprt

Removes one of the functions from the expr_util translation unit that is
supposed to be deprecated.

src/analyses/custom_bitvector_analysis.cpp

@@ -349,7 +349,7 @@ void custom_bitvector_domaint::transform(
             {
               if(
                 lhs.is_constant() &&
-                is_null_pointer(to_constant_expr(lhs))) // NULL means all
+                to_constant_expr(lhs).is_null_pointer()) // NULL means all
               {
                 if(mode==modet::CLEAR_MAY)
                 {
@@ -478,7 +478,7 @@ void custom_bitvector_domaint::transform(
         {
           if(
             lhs.is_constant() &&
-            is_null_pointer(to_constant_expr(lhs))) // NULL means all
+            to_constant_expr(lhs).is_null_pointer()) // NULL means all
           {
             if(mode==modet::CLEAR_MAY)
             {
@@ -716,7 +716,7 @@ exprt custom_bitvector_domaint::eval(
 
       if(
         pointer.is_constant() &&
-        is_null_pointer(to_constant_expr(pointer))) // NULL means all
+        to_constant_expr(pointer).is_null_pointer()) // NULL means all
       {
         if(src.id() == ID_get_may)
         {

src/analyses/invariant_set.cpp

@@ -121,7 +121,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   if(expr.is_constant())
   {
     // NULL?
-    if(is_null_pointer(to_constant_expr(expr)))
+    if(to_constant_expr(expr).is_null_pointer())
       return "0";
 
     const auto i = numeric_cast<mp_integer>(expr);

src/ansi-c/c_typecheck_expr.cpp

@@ -1672,13 +1672,13 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
     // (at least that's how GCC behaves)
     if(
       to_pointer_type(operands[1].type()).base_type().id() == ID_empty &&
-      tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1)))
+      tmp1.is_constant() && to_constant_expr(tmp1).is_null_pointer())
     {
       implicit_typecast(operands[1], operands[2].type());
     }
     else if(
       to_pointer_type(operands[2].type()).base_type().id() == ID_empty &&
-      tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2)))
+      tmp2.is_constant() && to_constant_expr(tmp2).is_null_pointer())
     {
       implicit_typecast(operands[2], operands[1].type());
     }

src/ansi-c/expr2c.cpp

@@ -1983,7 +1983,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_pointer)
   {
-    if(is_null_pointer(src))
+    if(src.is_null_pointer())
     {
       if(configuration.use_library_macros)
         dest = "NULL";

src/cpp/cpp_typecheck_conversions.cpp

@@ -603,7 +603,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
   if(expr.get_bool(ID_C_lvalue))
     return false;
 
-  if(expr.is_constant() && is_null_pointer(to_constant_expr(expr)))
+  if(expr.is_constant() && to_constant_expr(expr).is_null_pointer())
   {
     new_expr = typecast_exprt::conditional_cast(expr, type);
     return true;

src/cprover/bv_pointers_wide.cpp

@@ -387,7 +387,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
   {
     const constant_exprt &c = to_constant_expr(expr);
 
-    if(is_null_pointer(c))
+    if(c.is_null_pointer())
       return encode(pointer_logic.get_null_object(), type);
     else
     {

src/goto-instrument/dump_c.cpp

@@ -1399,7 +1399,7 @@ void dump_ct::cleanup_expr(exprt &expr)
     }
     // add a typecast for NULL
     else if(
-      u.op().is_constant() && is_null_pointer(to_constant_expr(u.op())) &&
+      u.op().is_constant() && to_constant_expr(u.op()).is_null_pointer() &&
       to_pointer_type(u.op().type()).base_type().id() == ID_empty)
     {
       const struct_union_typet::componentt &comp=
@@ -1459,7 +1459,7 @@ void dump_ct::cleanup_expr(exprt &expr)
             // add a typecast for NULL or 0
             if(
               argument.is_constant() &&
-              is_null_pointer(to_constant_expr(argument)))
+              to_constant_expr(argument).is_null_pointer())
             {
               const typet &comp_type=
                 to_union_type(type).components().front().type();

src/goto-instrument/goto_program2code.cpp

@@ -311,7 +311,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
   const exprt this_va_list_expr = target->assign_lhs();
   const exprt &r = skip_typecast(target->assign_rhs());
 
-  if(r.is_constant() && is_null_pointer(to_constant_expr(r)))
+  if(r.is_constant() && to_constant_expr(r).is_null_pointer())
   {
     code_function_callt f(
       symbol_exprt("va_end", code_typet({}, empty_typet())),

src/goto-programs/xml_expr.cpp

@@ -221,7 +221,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       result.name = "pointer";
       result.set_attribute(
         "binary", integer2binary(bvrep2integer(value, width, false), width));
-      if(is_null_pointer(constant_expr))
+      if(constant_expr.is_null_pointer())
         result.data = "NULL";
     }
     else if(type.id() == ID_bool)

src/goto-symex/shadow_memory_util.cpp

@@ -319,9 +319,7 @@ bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,
   const exprt &address)
 {
-  if(
-    address.id() == ID_constant && address.type().id() == ID_pointer &&
-    to_constant_expr(address).is_zero())
+  if(address.is_constant() && to_constant_expr(address).is_null_pointer())
   {
     for(const auto &e : value_set)
     {

src/goto-symex/symex_goto.cpp

@@ -91,7 +91,7 @@ static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 
   if(
     skip_typecast(other_operand).id() != ID_address_of &&
-    (!constant_expr || !is_null_pointer(*constant_expr)))
+    (!constant_expr || !constant_expr->is_null_pointer()))
   {
     return {};
   }

src/goto-synthesizer/cegis_verifier.cpp

@@ -71,7 +71,7 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation)
   // NULL == ptr
   if(
     can_cast_expr<constant_exprt>(lhs_pointer) &&
-    is_null_pointer(*expr_try_dynamic_cast<constant_exprt>(lhs_pointer)))
+    expr_try_dynamic_cast<constant_exprt>(lhs_pointer)->is_null_pointer())
   {
     return rhs_pointer;
   }

src/pointer-analysis/value_set.cpp

@@ -621,7 +621,7 @@ void value_sett::get_value_set_rec(
   else if(expr.is_constant())
   {
     // check if NULL
-    if(is_null_pointer(to_constant_expr(expr)))
+    if(to_constant_expr(expr).is_null_pointer())
     {
       insert(
         dest,

src/pointer-analysis/value_set_fi.cpp

@@ -532,7 +532,7 @@ void value_set_fit::get_value_set_rec(
   else if(expr.is_constant())
   {
     // check if NULL
-    if(is_null_pointer(to_constant_expr(expr)))
+    if(to_constant_expr(expr).is_null_pointer())
     {
       insert(
         dest,

src/solvers/flattening/bv_pointers.cpp

@@ -443,7 +443,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     const constant_exprt &c = to_constant_expr(expr);
 
-    if(is_null_pointer(c))
+    if(c.is_null_pointer())
       return encode(pointer_logic.get_null_object(), type);
     else
     {

src/solvers/smt2/smt2_conv.cpp

@@ -3379,7 +3379,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
   }
   else if(expr_type.id()==ID_pointer)
   {
-    if(is_null_pointer(expr))
+    if(expr.is_null_pointer())
     {
       out << "(_ bv0 " << boolbv_width(expr_type)
           << ")";

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -329,7 +329,7 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
 
 static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
 {
-  if(is_null_pointer(constant_literal))
+  if(constant_literal.is_null_pointer())
   {
     const size_t bit_width =
       type_checked_cast<pointer_typet>(constant_literal.type()).get_width();

src/util/arith_tools.cpp

@@ -25,7 +25,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
 
   if(type_id==ID_pointer)
   {
-    if(is_null_pointer(expr))
+    if(expr.is_null_pointer())
     {
       int_value=0;
       return false;

src/util/expr_util.cpp

@@ -369,20 +369,5 @@ exprt make_and(exprt a, exprt b)
 
 bool is_null_pointer(const constant_exprt &expr)
 {
-  if(expr.type().id() != ID_pointer)
-    return false;
-
-  if(expr.get_value() == ID_NULL)
-    return true;
-
-    // We used to support "0" (when NULL_is_zero), but really front-ends should
-    // resolve this and generate ID_NULL instead.
-#if 0
-  return config.ansi_c.NULL_is_zero && expr.value_is_zero_string();
-#else
-  INVARIANT(
-    !expr.value_is_zero_string() || !config.ansi_c.NULL_is_zero,
-    "front-end should use ID_NULL");
-  return false;
-#endif
+  return expr.is_null_pointer();
 }

src/util/expr_util.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
  * \date   Sun Jul 31 21:54:44 BST 2011
 */
 
+#include "deprecate.h"
 #include "irep.h"
 
 #include <functional>
@@ -116,6 +117,7 @@ exprt make_and(exprt a, exprt b);
 /// Returns true if \p expr has a pointer type and a value NULL; it also returns
 /// true when \p expr has value zero and NULL_is_zero is true; returns false in
 /// all other cases.
+DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead"))
 bool is_null_pointer(const constant_exprt &expr);
 
 #endif // CPROVER_UTIL_EXPR_UTIL_H

src/util/format_expr.cpp

@@ -194,7 +194,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
     return os << ieee_floatt(src);
   else if(type == ID_pointer)
   {
-    if(is_null_pointer(src))
+    if(src.is_null_pointer())
       return os << ID_NULL;
     else if(
       src.get_value() == "INVALID" || src.get_value().starts_with("INVALID-"))

src/util/simplify_expr.cpp

@@ -906,7 +906,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       (op_plus_expr.op0().id() == ID_typecast &&
        to_typecast_expr(op_plus_expr.op0()).op().is_zero()) ||
       (op_plus_expr.op0().is_constant() &&
-       is_null_pointer(to_constant_expr(op_plus_expr.op0()))))
+       to_constant_expr(op_plus_expr.op0()).is_null_pointer()))
     {
       auto sub_size =
         pointer_offset_size(to_pointer_type(op_type).base_type(), ns);

src/util/simplify_expr_int.cpp

@@ -1538,8 +1538,8 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1)
   // we can't eliminate zeros
   if(
     op0.is_zero() || op1.is_zero() ||
-    (op0.is_constant() && is_null_pointer(to_constant_expr(op0))) ||
-    (op1.is_constant() && is_null_pointer(to_constant_expr(op1))))
+    (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) ||
+    (op1.is_constant() && to_constant_expr(op1).is_null_pointer()))
   {
     return true;
   }
@@ -1736,7 +1736,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
 
     const constant_exprt &op1_constant = to_constant_expr(expr.op1());
 
-    if(is_null_pointer(op1_constant))
+    if(op1_constant.is_null_pointer())
     {
       // the address of an object is never NULL
 
@@ -1799,7 +1799,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
 
         exprt ptr = simplify_object(expr.op0()).expr;
         // NULL + N == NULL is N == 0
-        if(ptr.is_constant() && is_null_pointer(to_constant_expr(ptr)))
+        if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer())
           return make_boolean_expr(offset.is_zero());
         // &x + N == NULL is false when the offset is in bounds
         else if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(ptr))

src/util/simplify_expr_pointer.cpp

@@ -38,7 +38,7 @@ static bool is_dereference_integer_object(
     {
       const constant_exprt &constant = to_constant_expr(pointer);
 
-      if(is_null_pointer(constant))
+      if(constant.is_null_pointer())
       {
         address=0;
         return true;
@@ -398,7 +398,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
   {
     const constant_exprt &c_ptr = to_constant_expr(ptr);
 
-    if(is_null_pointer(c_ptr))
+    if(c_ptr.is_null_pointer())
     {
       return from_integer(0, expr.type());
     }
@@ -571,7 +571,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
   }
 
   // NULL is not dynamic
-  if(op.is_constant() && is_null_pointer(to_constant_expr(op)))
+  if(op.is_constant() && to_constant_expr(op).is_null_pointer())
     return false_exprt();
 
   // &something depends on the something
@@ -619,7 +619,7 @@ simplify_exprt::simplify_is_invalid_pointer(const unary_exprt &expr)
   }
 
   // NULL is not invalid
-  if(op.is_constant() && is_null_pointer(to_constant_expr(op)))
+  if(op.is_constant() && to_constant_expr(op).is_null_pointer())
   {
     return false_exprt();
   }

src/util/simplify_utils.cpp

@@ -439,7 +439,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
     }
     else if(type.id() == ID_pointer)
     {
-      if(config.ansi_c.NULL_is_zero && is_null_pointer(to_constant_expr(expr)))
+      if(config.ansi_c.NULL_is_zero && to_constant_expr(expr).is_null_pointer())
         return std::string(to_bitvector_type(type).get_width(), '0');
       else
         return {};

src/util/std_expr.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "std_expr.h"
 
+#include "config.h"
 #include "namespace.h"
 #include "pointer_expr.h"
 #include "range.h"
@@ -21,6 +22,26 @@ bool constant_exprt::value_is_zero_string() const
   return val.find_first_not_of('0')==std::string::npos;
 }
 
+bool constant_exprt::is_null_pointer() const
+{
+  if(type().id() != ID_pointer)
+    return false;
+
+  if(get_value() == ID_NULL)
+    return true;
+
+    // We used to support "0" (when NULL_is_zero), but really front-ends should
+    // resolve this and generate ID_NULL instead.
+#if 0
+  return config.ansi_c.NULL_is_zero && value_is_zero_string();
+#else
+  INVARIANT(
+    !value_is_zero_string() || !config.ansi_c.NULL_is_zero,
+    "front-end should use ID_NULL");
+  return false;
+#endif
+}
+
 void constant_exprt::check(const exprt &expr, const validation_modet vm)
 {
   nullary_exprt::check(expr, vm);

src/util/std_expr.h

@@ -3004,6 +3004,11 @@ class constant_exprt : public nullary_exprt
 
   bool value_is_zero_string() const;
 
+  /// Returns true if \p expr has a pointer type and a value NULL; it also
+  /// returns true when \p expr has value zero and NULL_is_zero is true; returns
+  /// false in all other cases.
+  bool is_null_pointer() const;
+
   static void check(
     const exprt &expr,
     const validation_modet vm = validation_modet::INVARIANT);