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,7 +2141,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
+    exprt dynamic_object_expr=exprt(ID_is_dynamic_object, expr.type());
     dynamic_object_expr.operands()=expr.arguments();
     dynamic_object_expr.add_source_location()=source_location;
 

src/ansi-c/expr2c.cpp

@@ -3574,7 +3574,7 @@ 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)
+  else if(src.id()==ID_is_dynamic_object)
     return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
 
   else if(src.id()=="is_zero_string")

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

@@ -447,6 +447,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);