Merge pull request #6532 from tautschnig/is-null-pointer

tautschnig · web-flow · commit db47f0732bd9 · 2022-02-26T18:12:31.000+01:00
Wrap NULL/0 is-a-null-pointer in a utility function
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
@@ -345,8 +345,9 @@ void custom_bitvector_domaint::transform(
 
             if(lhs.type().id()==ID_pointer)
             {
-              if(lhs.is_constant() &&
-                 to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
+              if(
+                lhs.is_constant() &&
+                is_null_pointer(to_constant_expr(lhs))) // NULL means all
               {
                 if(mode==modet::CLEAR_MAY)
                 {
@@ -473,8 +474,9 @@ void custom_bitvector_domaint::transform(
 
         if(lhs.type().id()==ID_pointer)
         {
-          if(lhs.is_constant() &&
-             to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
+          if(
+            lhs.is_constant() &&
+            is_null_pointer(to_constant_expr(lhs))) // NULL means all
           {
             if(mode==modet::CLEAR_MAY)
             {
@@ -708,8 +710,9 @@ exprt custom_bitvector_domaint::eval(
       if(pointer.type().id()!=ID_pointer)
         return src;
 
-      if(pointer.is_constant() &&
-         to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
+      if(
+        pointer.is_constant() &&
+        is_null_pointer(to_constant_expr(pointer))) // NULL means all
       {
         if(src.id() == ID_get_may)
         {
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
@@ -121,9 +121,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   if(expr.is_constant())
   {
     // NULL?
-    if(expr.type().id()==ID_pointer)
-      if(expr.get(ID_value)==ID_NULL)
-        return "0";
+    if(is_null_pointer(to_constant_expr(expr)))
+      return "0";
 
     const auto i = numeric_cast<mp_integer>(expr);
     if(i.has_value())
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -1602,14 +1602,18 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
 
     // is one of them void * AND null? Convert that to the other.
     // (at least that's how GCC behaves)
-    if(operands[1].type().subtype().id()==ID_empty &&
-       tmp1.is_constant() &&
-       to_constant_expr(tmp1).get_value()==ID_NULL)
+    if(
+      operands[1].type().subtype().id() == ID_empty && tmp1.is_constant() &&
+      is_null_pointer(to_constant_expr(tmp1)))
+    {
       implicit_typecast(operands[1], operands[2].type());
-    else if(operands[2].type().subtype().id()==ID_empty &&
-            tmp2.is_constant() &&
-            to_constant_expr(tmp2).get_value()==ID_NULL)
+    }
+    else if(
+      operands[2].type().subtype().id() == ID_empty && tmp2.is_constant() &&
+      is_null_pointer(to_constant_expr(tmp2)))
+    {
       implicit_typecast(operands[2], operands[1].type());
+    }
     else if(operands[1].type().subtype().id()!=ID_code ||
             operands[2].type().subtype().id()!=ID_code)
     {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -7,16 +7,13 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "expr2c.h"
-
-#include <algorithm>
-#include <sstream>
-
-#include <map>
+#include "expr2c_class.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/find_symbols.h>
 #include <util/fixedbv.h>
 #include <util/floatbv_expr.h>
@@ -33,7 +30,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "c_misc.h"
 #include "c_qualifiers.h"
-#include "expr2c_class.h"
+
+#include <algorithm>
+#include <map>
+#include <sstream>
 
 // clang-format off
 
@@ -1983,9 +1983,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_pointer)
   {
-    if(
-      value == ID_NULL ||
-      (value == std::string(value.size(), '0') && config.ansi_c.NULL_is_zero))
+    if(is_null_pointer(src))
     {
       if(configuration.use_library_macros)
         dest = "NULL";
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
@@ -601,8 +601,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
   if(expr.get_bool(ID_C_lvalue))
     return false;
 
-  if(expr.id()==ID_constant &&
-     expr.get(ID_value)==ID_NULL)
+  if(expr.id() == ID_constant && is_null_pointer(to_constant_expr(expr)))
   {
     new_expr = typecast_exprt::conditional_cast(expr, type);
     return true;
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
@@ -10,25 +10,23 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Dump Goto-Program as C/C++ Source
 
 #include "dump_c.h"
+#include "dump_c_class.h"
 
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
+#include <util/expr_util.h>
 #include <util/find_symbols.h>
 #include <util/get_base_name.h>
 #include <util/invariant.h>
-#include <util/namespace.h>
 #include <util/replace_symbol.h>
-#include <util/std_code.h>
 #include <util/string_utils.h>
 
 #include <ansi-c/expr2c.h>
 #include <cpp/expr2cpp.h>
-
 #include <linking/static_lifetime_init.h>
 
-#include "dump_c_class.h"
 #include "goto_program2code.h"
 
 dump_c_configurationt dump_c_configurationt::default_configuration =
@@ -1325,11 +1323,9 @@ void dump_ct::cleanup_expr(exprt &expr)
         expr = struct_exprt({}, struct_typet());
     }
     // add a typecast for NULL
-    else if(u.op().id()==ID_constant &&
-            u.op().type().id()==ID_pointer &&
-            u.op().type().subtype().id()==ID_empty &&
-            (u.op().is_zero() ||
-             to_constant_expr(u.op()).get_value()==ID_NULL))
+    else if(
+      u.op().id() == ID_constant && is_null_pointer(to_constant_expr(u.op())) &&
+      u.op().type().subtype().id() == ID_empty)
     {
       const struct_union_typet::componentt &comp=
         u_type_f.get_component(u.get_component_name());
@@ -1385,8 +1381,7 @@ void dump_ct::cleanup_expr(exprt &expr)
             // add a typecast for NULL or 0
             if(
               argument.id() == ID_constant &&
-              (argument.is_zero() ||
-               to_constant_expr(argument).get_value() == ID_NULL))
+              is_null_pointer(to_constant_expr(argument)))
             {
               const typet &comp_type=
                 to_union_type(type).components().front().type();
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
@@ -12,13 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
 #define CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
 
-#include <set>
-#include <string>
-
+#include <util/namespace.h>
+#include <util/std_code.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/system_library_symbols.h>
 
+#include <set>
+#include <string>
+#include <unordered_set>
+
 /// Used for configuring the behaviour of dump_c
 struct dump_c_configurationt final
 {
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -309,8 +309,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.id()==ID_constant &&
-     (r.is_zero() || to_constant_expr(r).get_value()==ID_NULL))
+  if(r.id() == ID_constant && is_null_pointer(to_constant_expr(r)))
   {
     code_function_callt f(
       symbol_exprt("va_end", code_typet({}, empty_typet())),
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_util.h>
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
@@ -220,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(constant_expr.get(ID_value) == ID_NULL)
+      if(is_null_pointer(constant_expr))
         result.data = "NULL";
     }
     else if(type.id() == ID_bool)
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
@@ -91,7 +91,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 
   if(
     skip_typecast(other_operand).id() != ID_address_of &&
-    (!constant_expr || constant_expr->get_value() != ID_NULL))
+    (!constant_expr || !is_null_pointer(*constant_expr)))
   {
     return {};
   }
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
@@ -11,11 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set.h"
 
-#include <ostream>
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/format_expr.h>
 #include <util/format_type.h>
 #include <util/pointer_expr.h>
@@ -26,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+#include <ostream>
+
 #ifdef DEBUG
 #include <iostream>
 #include <util/format_expr.h>
@@ -560,8 +561,7 @@ void value_sett::get_value_set_rec(
   else if(expr.is_constant())
   {
     // check if NULL
-    if(expr.get(ID_value)==ID_NULL &&
-       expr_type.id()==ID_pointer)
+    if(is_null_pointer(to_constant_expr(expr)))
     {
       insert(
         dest, exprt(ID_null_object, to_pointer_type(expr_type).base_type()), 0);
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
@@ -11,22 +11,23 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set_fi.h"
 
-#include <ostream>
-
-#include <goto-programs/goto_instruction_code.h>
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_code.h>
 #include <util/symbol.h>
 
+#include <goto-programs/goto_instruction_code.h>
+
 #include <langapi/language_util.h>
 
+#include <ostream>
+
 const value_set_fit::object_map_dt value_set_fit::object_map_dt::blank{};
 
 object_numberingt value_set_fit::object_numbering;
@@ -517,8 +518,7 @@ void value_set_fit::get_value_set_rec(
   else if(expr.is_constant())
   {
     // check if NULL
-    if(expr.get(ID_value)==ID_NULL &&
-       expr.type().id()==ID_pointer)
+    if(is_null_pointer(to_constant_expr(expr)))
     {
       insert(dest, exprt(ID_null_object, expr.type().subtype()), 0);
       return;
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -409,13 +410,13 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_constant)
   {
-    irep_idt value=to_constant_expr(expr).get_value();
+    const constant_exprt &c = to_constant_expr(expr);
 
-    if(value==ID_NULL)
+    if(is_null_pointer(c))
       return encode(pointer_logic.get_null_object(), type);
     else
     {
-      mp_integer i = bvrep2integer(value, bits, false);
+      mp_integer i = bvrep2integer(c.get_value(), bits, false);
       return bv_utils.build_constant(i, bits);
     }
   }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -3035,15 +3035,14 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
   }
   else if(expr_type.id()==ID_pointer)
   {
-    const irep_idt &value = expr.get_value();
-
-    if(value==ID_NULL)
+    if(is_null_pointer(expr))
     {
       out << "(_ bv0 " << boolbv_width(expr_type)
           << ")";
     }
     else
-      UNEXPECTEDCASE("unknown pointer constant: "+id2string(value));
+      UNEXPECTEDCASE(
+        "unknown pointer constant: " + id2string(expr.get_value()));
   }
   else if(expr_type.id()==ID_bool)
   {
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 
 #include "c_types.h"
+#include "expr_util.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
@@ -24,7 +25,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
 
   if(type_id==ID_pointer)
   {
-    if(value==ID_NULL)
+    if(is_null_pointer(expr))
     {
       int_value=0;
       return false;
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 #include "bitvector_types.h"
 #include "expr_iterator.h"
+#include "expr_util.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "rational.h"
@@ -97,8 +98,7 @@ bool exprt::is_zero() const
     }
     else if(type_id==ID_pointer)
     {
-      return constant.value_is_zero_string() ||
-             constant.get_value()==ID_NULL;
+      return is_null_pointer(constant);
     }
   }
 
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
diff --git a/src/util/expr_util.h b/src/util/expr_util.h
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp

Original file line number	Diff line number	Diff line change
`@@ -345,8 +345,9 @@ void custom_bitvector_domaint::transform(`
`345`	`345`
`346`	`346`	`if(lhs.type().id()==ID_pointer)`
`347`	`347`	`{`
`348`		`- if(lhs.is_constant() &&`
`349`		`- to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all`
	`348`	`+ if(`
	`349`	`+ lhs.is_constant() &&`
	`350`	`+ is_null_pointer(to_constant_expr(lhs))) // NULL means all`
`350`	`351`	`{`
`351`	`352`	`if(mode==modet::CLEAR_MAY)`
`352`	`353`	`{`
`@@ -473,8 +474,9 @@ void custom_bitvector_domaint::transform(`
`473`	`474`
`474`	`475`	`if(lhs.type().id()==ID_pointer)`
`475`	`476`	`{`
`476`		`- if(lhs.is_constant() &&`
`477`		`- to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all`
	`477`	`+ if(`
	`478`	`+ lhs.is_constant() &&`
	`479`	`+ is_null_pointer(to_constant_expr(lhs))) // NULL means all`
`478`	`480`	`{`
`479`	`481`	`if(mode==modet::CLEAR_MAY)`
`480`	`482`	`{`
`@@ -708,8 +710,9 @@ exprt custom_bitvector_domaint::eval(`
`708`	`710`	`if(pointer.type().id()!=ID_pointer)`
`709`	`711`	`return src;`
`710`	`712`
`711`		`- if(pointer.is_constant() &&`
`712`		`- to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all`
	`713`	`+ if(`
	`714`	`+ pointer.is_constant() &&`
	`715`	`+ is_null_pointer(to_constant_expr(pointer))) // NULL means all`
`713`	`716`	`{`
`714`	`717`	`if(src.id() == ID_get_may)`
`715`	`718`	`{`
Original file line number	Diff line number	Diff line change
`@@ -601,8 +601,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(`
`601`	`601`	`if(expr.get_bool(ID_C_lvalue))`
`602`	`602`	`return false;`
`603`	`603`
`604`		`- if(expr.id()==ID_constant &&`
`605`		`- expr.get(ID_value)==ID_NULL)`
	`604`	`+ if(expr.id() == ID_constant && is_null_pointer(to_constant_expr(expr)))`
`606`	`605`	`{`
`607`	`606`	`new_expr = typecast_exprt::conditional_cast(expr, type);`
`608`	`607`	`return true;`
Original file line number	Diff line number	Diff line change
`@@ -309,8 +309,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(`
`309`	`309`	`const exprt this_va_list_expr = target->assign_lhs();`
`310`	`310`	`const exprt &r = skip_typecast(target->assign_rhs());`
`311`	`311`
`312`		`- if(r.id()==ID_constant &&`
`313`		`- (r.is_zero() \|\| to_constant_expr(r).get_value()==ID_NULL))`
	`312`	`+ if(r.id() == ID_constant && is_null_pointer(to_constant_expr(r)))`
`314`	`313`	`{`
`315`	`314`	`code_function_callt f(`
`316`	`315`	`symbol_exprt("va_end", code_typet({}, empty_typet())),`
Original file line number	Diff line number	Diff line change
`@@ -91,7 +91,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(`
`91`	`91`
`92`	`92`	`if(`
`93`	`93`	`skip_typecast(other_operand).id() != ID_address_of &&`
`94`		`- (!constant_expr \|\| constant_expr->get_value() != ID_NULL))`
	`94`	`+ (!constant_expr \|\| !is_null_pointer(*constant_expr)))`
`95`	`95`	`{`
`96`	`96`	`return {};`
`97`	`97`	`}`