disambiguate two exprts with same ID

regression/goto-instrument/slice19/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$

src/analyses/goto_check.cpp

@@ -1129,18 +1129,16 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
     if(flags.is_unknown())
     {
-      conditions.push_back(conditiont(
-        not_exprt(invalid_pointer(address)),
-        "pointer invalid"));
+      conditions.push_back(conditiont{
+        not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
     }
 
     if(flags.is_uninitialized())
     {
-      conditions.push_back(conditiont(
-        or_exprt(
-          in_bounds_of_some_explicit_allocation,
-          not_exprt(invalid_pointer(address))),
-        "pointer uninitialized"));
+      conditions.push_back(
+        conditiont{or_exprt{in_bounds_of_some_explicit_allocation,
+                            not_exprt{is_invalid_pointer_exprt{address}}},
+                   "pointer uninitialized"});
     }
 
     if(flags.is_unknown() || flags.is_dynamic_heap())

src/ansi-c/c_typecheck_expr.cpp

@@ -2095,16 +2095,16 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(get_may_expr);
   }
-  else if(identifier==CPROVER_PREFIX "invalid_pointer")
+  else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
   {
     if(expr.arguments().size()!=1)
     {
       error().source_location = f_op.source_location();
-      error() << "invalid_pointer expects one operand" << eom;
+      error() << "is_invalid_pointer expects one operand" << eom;
       throw 0;
     }
 
-    exprt same_object_expr = invalid_pointer(expr.arguments().front());
+    exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
     same_object_expr.add_source_location()=source_location;
 
     return same_object_expr;
@@ -2165,11 +2165,10 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
-    dynamic_object_expr.operands()=expr.arguments();
-    dynamic_object_expr.add_source_location()=source_location;
+    exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
+    is_dynamic_object_expr.add_source_location() = source_location;
 
-    return dynamic_object_expr;
+    return is_dynamic_object_expr;
   }
   else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
   {

src/ansi-c/cprover_builtin_headers.h

@@ -5,7 +5,7 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description
 void __CPROVER_havoc_object(void *);
 __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
-__CPROVER_bool __CPROVER_invalid_pointer(const void *);
+__CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);

src/ansi-c/expr2c.cpp

@@ -3426,8 +3426,8 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id() == ID_w_ok)
     return convert_function(src, "W_OK", precedence = 16);
 
-  else if(src.id()==ID_invalid_pointer)
-    return convert_function(src, "INVALID-POINTER", precedence=16);
+  else if(src.id() == ID_is_invalid_pointer)
+    return convert_function(src, "IS_INVALID_POINTER", precedence = 16);
 
   else if(src.id()==ID_good_pointer)
     return convert_function(src, "GOOD_POINTER", precedence=16);
@@ -3482,12 +3482,12 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()=="pointer_cons")
     return convert_function(src, "POINTER_CONS", precedence=16);
 
-  else if(src.id()==ID_invalid_pointer)
+  else if(src.id() == ID_is_invalid_pointer)
     return convert_function(
-      src, CPROVER_PREFIX "invalid_pointer", precedence = 16);
+      src, CPROVER_PREFIX "is_invalid_pointer", precedence = 16);
 
-  else if(src.id()==ID_dynamic_object)
-    return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
+  else if(src.id() == ID_is_dynamic_object)
+    return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16);
 
   else if(src.id()=="is_zero_string")
     return convert_function(src, "IS_ZERO_STRING", precedence=16);

src/solvers/flattening/bv_pointers.cpp

@@ -20,7 +20,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
 
   const exprt::operandst &operands=expr.operands();
 
-  if(expr.id()==ID_invalid_pointer)
+  if(expr.id() == ID_is_invalid_pointer)
   {
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
@@ -45,7 +45,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       }
     }
   }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id() == ID_is_dynamic_object)
   {
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
@@ -728,7 +728,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 void bv_pointerst::do_postponed(
   const postponedt &postponed)
 {
-  if(postponed.expr.id() == ID_dynamic_object)
+  if(postponed.expr.id() == ID_is_dynamic_object)
   {
     const pointer_logict::objectst &objects=
       pointer_logic.objects;

src/solvers/smt2/smt2_conv.cpp

@@ -1316,11 +1316,11 @@ void smt2_convt::convert_expr(const exprt &expr)
     if(ext>0)
       out << ")"; // zero_extend
   }
-  else if(expr.id() == ID_dynamic_object)
+  else if(expr.id() == ID_is_dynamic_object)
   {
     convert_is_dynamic_object(expr);
   }
-  else if(expr.id()==ID_invalid_pointer)
+  else if(expr.id() == ID_is_invalid_pointer)
   {
     DATA_INVARIANT(
       expr.operands().size() == 1,

src/util/irep_ids.def

@@ -217,7 +217,7 @@ IREP_ID_ONE(invalid)
 IREP_ID_TWO(C_invalid_object, #invalid_object)
 IREP_ID_ONE(pointer_offset)
 IREP_ID_ONE(pointer_object)
-IREP_ID_TWO(invalid_pointer, invalid-pointer)
+IREP_ID_ONE(is_invalid_pointer)
 IREP_ID_ONE(ieee_float_equal)
 IREP_ID_ONE(ieee_float_notequal)
 IREP_ID_ONE(isnan)
@@ -446,6 +446,7 @@ IREP_ID_TWO(overflow_minus, overflow--)
 IREP_ID_TWO(overflow_mult, overflow-*)
 IREP_ID_TWO(overflow_unary_minus, overflow-unary-)
 IREP_ID_ONE(object_descriptor)
+IREP_ID_ONE(is_dynamic_object)
 IREP_ID_ONE(dynamic_object)
 IREP_ID_TWO(C_dynamic, #dynamic)
 IREP_ID_ONE(object_size)

src/util/pointer_predicates.cpp

@@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns)
 
 exprt dynamic_object(const exprt &pointer)
 {
-  exprt dynamic_expr(ID_dynamic_object, bool_typet());
+  exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
   dynamic_expr.copy_to_operands(pointer);
   return dynamic_expr;
 }
@@ -105,7 +105,7 @@ exprt good_pointer_def(
 
   const not_exprt not_null(null_pointer(pointer));
 
-  const not_exprt not_invalid(invalid_pointer(pointer));
+  const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
 
   const or_exprt bad_other(
     object_lower_bound(pointer, nil_exprt()),
@@ -139,11 +139,6 @@ exprt null_pointer(const exprt &pointer)
   return same_object(pointer, null_pointer);
 }
 
-exprt invalid_pointer(const exprt &pointer)
-{
-  return unary_exprt(ID_invalid_pointer, pointer, bool_typet());
-}
-
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
   const exprt &offset)

src/util/pointer_predicates.h

@@ -12,11 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
 #define CPROVER_UTIL_POINTER_PREDICATES_H
 
-#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
+#include "std_expr.h"
 
-class exprt;
-class namespacet;
-class typet;
+#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
 
 exprt same_object(const exprt &p1, const exprt &p2);
 exprt deallocated(const exprt &pointer, const namespacet &);
@@ -32,7 +30,6 @@ exprt good_pointer_def(const exprt &pointer, const namespacet &);
 exprt null_object(const exprt &pointer);
 exprt null_pointer(const exprt &pointer);
 exprt integer_address(const exprt &pointer);
-exprt invalid_pointer(const exprt &pointer);
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
   const exprt &offset);
@@ -47,4 +44,13 @@ exprt object_upper_bound(
   const exprt &pointer,
   const exprt &access_size);
 
+class is_invalid_pointer_exprt : public unary_predicate_exprt
+{
+public:
+  explicit is_invalid_pointer_exprt(exprt pointer)
+    : unary_predicate_exprt{ID_is_invalid_pointer, std::move(pointer)}
+  {
+  }
+};
+
 #endif // CPROVER_UTIL_POINTER_PREDICATES_H

src/util/simplify_expr.cpp

@@ -2403,12 +2403,12 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
   else if(expr.id()==ID_pointer_object)
     result=simplify_pointer_object(expr) && result;
-  else if(expr.id() == ID_dynamic_object)
+  else if(expr.id() == ID_is_dynamic_object)
   {
-    result = simplify_dynamic_object(expr) && result;
+    result = simplify_is_dynamic_object(expr) && result;
   }
-  else if(expr.id()==ID_invalid_pointer)
-    result=simplify_invalid_pointer(expr) && result;
+  else if(expr.id() == ID_is_invalid_pointer)
+    result = simplify_is_invalid_pointer(expr) && result;
   else if(expr.id()==ID_object_size)
     result=simplify_object_size(expr) && result;
   else if(expr.id()==ID_good_pointer)

src/util/simplify_expr_class.h

@@ -96,8 +96,8 @@ class simplify_exprt
   bool simplify_pointer_object(exprt &expr);
   bool simplify_object_size(exprt &expr);
   bool simplify_dynamic_size(exprt &expr);
-  bool simplify_dynamic_object(exprt &expr);
-  bool simplify_invalid_pointer(exprt &expr);
+  bool simplify_is_dynamic_object(exprt &expr);
+  bool simplify_is_invalid_pointer(exprt &expr);
   bool simplify_same_object(exprt &expr);
   bool simplify_good_pointer(exprt &expr);
   bool simplify_object(exprt &expr);

src/util/simplify_expr_int.cpp

@@ -1686,7 +1686,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       {
         if(
           expr.op0().op0().id() == ID_symbol ||
-          expr.op0().op0().id() == ID_dynamic_object ||
+          expr.op0().op0().id() == ID_is_dynamic_object ||
           expr.op0().op0().id() == ID_member ||
           expr.op0().op0().id() == ID_index ||
           expr.op0().op0().id() == ID_string_constant)
@@ -1701,11 +1701,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
               expr.op0().op0().id()==ID_address_of &&
               expr.op0().op0().operands().size()==1)
       {
-        if(expr.op0().op0().op0().id()==ID_symbol ||
-           expr.op0().op0().op0().id()==ID_dynamic_object ||
-           expr.op0().op0().op0().id()==ID_member ||
-           expr.op0().op0().op0().id()==ID_index ||
-           expr.op0().op0().op0().id()==ID_string_constant)
+        if(
+          expr.op0().op0().op0().id() == ID_symbol ||
+          expr.op0().op0().op0().id() == ID_is_dynamic_object ||
+          expr.op0().op0().op0().id() == ID_member ||
+          expr.op0().op0().op0().id() == ID_index ||
+          expr.op0().op0().op0().id() == ID_string_constant)
         {
           expr=false_exprt();
           return false;

src/util/simplify_expr_pointer.cpp

@@ -468,7 +468,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
     {
       if(
         op.operands().size() != 1 ||
-        (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object &&
+        (op.op0().id() != ID_symbol && op.op0().id() != ID_is_dynamic_object &&
          op.op0().id() != ID_string_constant))
       {
         return true;
@@ -515,18 +515,18 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
   return result;
 }
 
-bool simplify_exprt::simplify_dynamic_object(exprt &expr)
+bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return true;
+  // This should hold as a result of the expr ID being is_dynamic_object.
+  PRECONDITION(expr.operands().size() == 1);
 
   exprt &op=expr.op0();
 
   if(op.id()==ID_if && op.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    simplify_dynamic_object(if_expr.true_case());
-    simplify_dynamic_object(if_expr.false_case());
+    simplify_is_dynamic_object(if_expr.true_case());
+    simplify_is_dynamic_object(if_expr.false_case());
     simplify_if(if_expr);
     expr.swap(if_expr);
 
@@ -571,7 +571,7 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr)
   return result;
 }
 
-bool simplify_exprt::simplify_invalid_pointer(exprt &expr)
+bool simplify_exprt::simplify_is_invalid_pointer(exprt &expr)
 {
   if(expr.operands().size()!=1)
     return true;

src/util/std_expr.h

@@ -2103,6 +2103,38 @@ inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr)
   return ret;
 }
 
+/// Evaluates to true if the operand is a pointer to a dynamic object.
+class is_dynamic_object_exprt : public unary_predicate_exprt
+{
+public:
+  is_dynamic_object_exprt() : unary_predicate_exprt(ID_is_dynamic_object)
+  {
+  }
+
+  explicit is_dynamic_object_exprt(const exprt &op)
+    : unary_predicate_exprt(ID_is_dynamic_object, op)
+  {
+  }
+};
+
+inline const is_dynamic_object_exprt &
+to_is_dynamic_object_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_is_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size() == 1, "is_dynamic_object must have one operand");
+  return static_cast<const is_dynamic_object_exprt &>(expr);
+}
+
+/// \copydoc to_is_dynamic_object_expr(const exprt &)
+/// \ingroup gr_std_expr
+inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_is_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size() == 1, "is_dynamic_object must have one operand");
+  return static_cast<is_dynamic_object_exprt &>(expr);
+}
 
 /// \brief Semantic type conversion
 class typecast_exprt:public unary_exprt