Disambiguates two exprts with the same ID.

This commit resolves an issue where ID_dynamic_object was used to
label two semantically distinct exprts.

One, with a single operand, was a boolean expression meaning that
the operand is a pointer to a dynamic object. This has been renamed
to ID_is_dynamic_object.

The second, with two operands, is an exprt representing a dynamic
object itself. This has stayed ID_dynamic_object.

Disambiguating which meaning was intended in each case was relatively
easy, as uses of these exprts frequently come with assertions
about the number of operands, and so this was used to inform which
instances of ID_dynamic_object should be changed and which should
be left the same.

Author: klaas

regression/goto-instrument/slice19/test.desc

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

src/ansi-c/c_typecheck_expr.cpp

@@ -2141,11 +2141,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/expr2c.cpp

@@ -3580,8 +3580,8 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_invalid_pointer)
     return convert_function(src, "__CPROVER_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

@@ -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)
@@ -735,7 +735,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

@@ -1367,7 +1367,7 @@ 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);
   }

src/util/irep_ids.def

@@ -448,6 +448,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;
 }

src/util/simplify_expr.cpp

@@ -2266,8 +2266,8 @@ 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)
-    result=simplify_dynamic_object(expr) && result;
+  else if(expr.id()==ID_is_dynamic_object)
+    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_object_size)

src/util/simplify_expr_class.h

@@ -96,7 +96,7 @@ 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_is_dynamic_object(exprt &expr);
   bool simplify_invalid_pointer(exprt &expr);
   bool simplify_same_object(exprt &expr);
   bool simplify_good_pointer(exprt &expr);

src/util/simplify_expr_int.cpp

@@ -1699,7 +1699,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
          expr.op0().operands().size()==1)
       {
         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)
@@ -1715,7 +1715,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
               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_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)

src/util/simplify_expr_pointer.cpp

@@ -464,7 +464,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_is_dynamic_object &&
           op.op0().id()!=ID_string_constant))
         return true;
     }
@@ -508,18 +508,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);
 

src/util/std_expr.h

@@ -2106,6 +2106,54 @@ inline void validate_expr(const dynamic_object_exprt &value)
 }
 
 
+/*! \brief 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)
+  {
+  }
+};
+
+/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt
+ *
+ * This is an unchecked conversion. \a expr must be known to be \ref
+ * is_dynamic_object_exprt.
+ *
+ * \param expr Source expression
+ * \return Object of type \ref is_dynamic_object_exprt
+ *
+ * \ingroup gr_std_expr
+*/
+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