Merge pull request #3737 from tautschnig/remove-follow-in-util

Remove unnecessary uses of ns.follow in util/

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1173,7 +1173,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
     if(flags.is_unknown() || flags.is_dynamic_heap())
     {
       const or_exprt dynamic_bounds_violation(
-        dynamic_object_lower_bound(address, ns, nil_exprt()),
+        dynamic_object_lower_bound(address, nil_exprt()),
         dynamic_object_upper_bound(address, ns, size));
 
       conditions.push_back(conditiont(
@@ -1189,8 +1189,8 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
       flags.is_static_lifetime())
     {
       const or_exprt object_bounds_violation(
-        object_lower_bound(address, ns, nil_exprt()),
-        object_upper_bound(address, ns, size));
+        object_lower_bound(address, nil_exprt()),
+        object_upper_bound(address, size));
 
       conditions.push_back(conditiont(
         or_exprt(

src/util/allocate_objects.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include "fresh_symbol.h"
 #include "pointer_offset_size.h"
 #include "string_constant.h"
+#include "type_eq.h"
 
 /// Allocates a new object, either by creating a local variable with automatic
 /// lifetime, a global variable with static lifetime, or by dynamically
@@ -183,7 +184,7 @@ exprt allocate_objectst::allocate_dynamic_object(
   output_code.add(assign);
 
   exprt malloc_symbol_expr =
-    ns.follow(malloc_sym.symbol_expr().type()) != ns.follow(target_expr.type())
+    !type_eq(malloc_sym.symbol_expr().type(), target_expr.type(), ns)
       ? (exprt)typecast_exprt(malloc_sym.symbol_expr(), target_expr.type())
       : malloc_sym.symbol_expr();
 

src/util/expr_initializer.cpp

@@ -263,7 +263,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result = expr_initializer_rec(ns.follow(type), source_location);
     // we might have mangled the type for arrays, so keep that
-    if(ns.follow(type).id()!=ID_array)
+    if(type.id() != ID_array)
       result.type()=type;
 
     return result;

src/util/expr_util.cpp

@@ -104,10 +104,9 @@ exprt is_not_zero(
   // Note that this returns a proper bool_typet(), not a C/C++ boolean.
   // To get a C/C++ boolean, add a further typecast.
 
-  const typet &src_type=
-    src.type().id()==ID_c_enum_tag?
-    ns.follow_tag(to_c_enum_tag_type(src.type())):
-    ns.follow(src.type());
+  const typet &src_type = src.type().id() == ID_c_enum_tag
+                            ? ns.follow_tag(to_c_enum_tag_type(src.type()))
+                            : src.type();
 
   if(src_type.id()==ID_bool) // already there
     return src; // do nothing

src/util/pointer_predicates.cpp

@@ -84,16 +84,15 @@ exprt good_pointer_def(
   const exprt &pointer,
   const namespacet &ns)
 {
-  const pointer_typet &pointer_type=to_pointer_type(ns.follow(pointer.type()));
+  const pointer_typet &pointer_type = to_pointer_type(pointer.type());
   const typet &dereference_type=pointer_type.subtype();
 
   const or_exprt good_dynamic_tmp1(
     not_exprt(malloc_object(pointer, ns)),
     and_exprt(
-      not_exprt(dynamic_object_lower_bound(pointer, ns, nil_exprt())),
-      not_exprt(
-        dynamic_object_upper_bound(
-          pointer, ns, size_of_expr(dereference_type, ns)))));
+      not_exprt(dynamic_object_lower_bound(pointer, nil_exprt())),
+      not_exprt(dynamic_object_upper_bound(
+        pointer, ns, size_of_expr(dereference_type, ns)))));
 
   const and_exprt good_dynamic_tmp2(
     not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1);
@@ -106,9 +105,8 @@ exprt good_pointer_def(
   const not_exprt not_invalid(invalid_pointer(pointer));
 
   const or_exprt bad_other(
-    object_lower_bound(pointer, ns, nil_exprt()),
-    object_upper_bound(
-      pointer, ns, size_of_expr(dereference_type, ns)));
+    object_lower_bound(pointer, nil_exprt()),
+    object_upper_bound(pointer, size_of_expr(dereference_type, ns)));
 
   const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other));
 
@@ -145,10 +143,9 @@ exprt invalid_pointer(const exprt &pointer)
 
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &offset)
 {
-  return object_lower_bound(pointer, ns, offset);
+  return object_lower_bound(pointer, offset);
 }
 
 exprt dynamic_object_upper_bound(
@@ -171,22 +168,17 @@ exprt dynamic_object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, access_size.type()),
+      access_size);
   }
 
-  if(ns.follow(sum.type())!=
-     ns.follow(malloc_size.type()))
-    sum.make_typecast(malloc_size.type());
-
-  return binary_relation_exprt(sum, op, malloc_size);
+  return binary_relation_exprt(
+    typecast_exprt::conditional_cast(sum, malloc_size.type()), op, malloc_size);
 }
 
 exprt object_upper_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &access_size)
 {
   // this is
@@ -204,23 +196,19 @@ exprt object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, access_size.type()),
+      access_size);
   }
 
-
-  if(ns.follow(sum.type())!=
-     ns.follow(object_size_expr.type()))
-    sum.make_typecast(object_size_expr.type());
-
-  return binary_relation_exprt(sum, op, object_size_expr);
+  return binary_relation_exprt(
+    typecast_exprt::conditional_cast(sum, object_size_expr.type()),
+    op,
+    object_size_expr);
 }
 
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
   const exprt &offset)
 {
   exprt p_offset=pointer_offset(pointer);
@@ -230,11 +218,8 @@ exprt object_lower_bound(
 
   if(offset.is_not_nil())
   {
-    if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
-      p_offset=
-        plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
-    else
-      p_offset=plus_exprt(p_offset, offset);
+    p_offset = plus_exprt(
+      p_offset, typecast_exprt::conditional_cast(offset, p_offset.type()));
   }
 
   return binary_relation_exprt(p_offset, ID_lt, zero);

src/util/pointer_predicates.h

@@ -33,19 +33,16 @@ exprt integer_address(const exprt &pointer);
 exprt invalid_pointer(const exprt &pointer);
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &offset);
 exprt dynamic_object_upper_bound(
   const exprt &pointer,
   const namespacet &,
   const exprt &access_size);
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &offset);
 exprt object_upper_bound(
   const exprt &pointer,
-  const namespacet &,
   const exprt &access_size);
 
 #endif // CPROVER_UTIL_POINTER_PREDICATES_H

src/util/simplify_expr.cpp

@@ -67,7 +67,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -107,7 +107,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -163,8 +163,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  const typet &expr_type=ns.follow(expr.type());
-  const typet &op_type=ns.follow(expr.op0().type());
+  const typet &expr_type = expr.type();
+  const typet &op_type = expr.op0().type();
 
   // eliminate casts of infinity
   if(expr.op0().id()==ID_infinity)
@@ -778,11 +778,12 @@ bool simplify_exprt::simplify_dereference(exprt &expr)
     if(address_of.object().id()==ID_index)
     {
       const index_exprt &old=to_index_expr(address_of.object());
-      if(ns.follow(old.array().type()).id()==ID_array)
+      if(old.array().type().id() == ID_array)
       {
-        index_exprt idx(old.array(),
-                        plus_exprt(old.index(), pointer.op1()),
-                        ns.follow(old.array().type()).subtype());
+        index_exprt idx(
+          old.array(),
+          plus_exprt(old.index(), pointer.op1()),
+          old.array().type().subtype());
         simplify_rec(idx);
         expr.swap(idx);
         return false;
@@ -1347,7 +1348,7 @@ bool simplify_exprt::simplify_object(exprt &expr)
     {
       // kill integers from sum
       Forall_operands(it, expr)
-        if(ns.follow(it->type()).id()==ID_pointer)
+        if(it->type().id() == ID_pointer)
         {
           exprt tmp=*it;
           expr.swap(tmp);
@@ -1359,7 +1360,7 @@ bool simplify_exprt::simplify_object(exprt &expr)
   else if(expr.id()==ID_typecast)
   {
     auto const &typecast_expr = to_typecast_expr(expr);
-    const typet &op_type = ns.follow(typecast_expr.op().type());
+    const typet &op_type = typecast_expr.op().type();
 
     if(op_type.id()==ID_pointer)
     {
@@ -1563,7 +1564,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
   bool little_endian)
 {
   // extract bits from lowest to highest memory address
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   if(expr.id()==ID_constant)
   {

src/util/simplify_expr_floatbv.cpp

@@ -21,7 +21,7 @@ bool simplify_exprt::simplify_isinf(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  if(ns.follow(expr.op0().type()).id()!=ID_floatbv)
+  if(expr.op0().type().id() != ID_floatbv)
     return true;
 
   if(expr.op0().is_constant())
@@ -72,7 +72,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -114,7 +114,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 
   if(expr.op0().is_constant())
   {
-    const typet &type=ns.follow(expr.op0().type());
+    const typet &type = expr.op0().type();
 
     if(type.id()==ID_floatbv)
     {
@@ -144,8 +144,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
 
   auto const &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
 
-  const typet &dest_type = ns.follow(floatbv_typecast_expr.type());
-  const typet &src_type = ns.follow(floatbv_typecast_expr.op().type());
+  const typet &dest_type = floatbv_typecast_expr.type();
+  const typet &src_type = floatbv_typecast_expr.op().type();
 
   // eliminate redundant casts
   if(dest_type==src_type)
@@ -171,8 +171,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
        casted_expr.op1().id()==ID_typecast &&
        casted_expr.op0().operands().size()==1 &&
        casted_expr.op1().operands().size()==1 &&
-       ns.follow(casted_expr.op0().type())==dest_type &&
-       ns.follow(casted_expr.op1().type())==dest_type)
+       casted_expr.op0().type()==dest_type &&
+       casted_expr.op1().type()==dest_type)
     {
       exprt result(casted_expr.id(), floatbv_typecast_expr.type());
       result.operands().resize(3);
@@ -282,7 +282,7 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
 
 bool simplify_exprt::simplify_floatbv_op(exprt &expr)
 {
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   PRECONDITION(type.id() == ID_floatbv);
   PRECONDITION(
@@ -298,10 +298,10 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
   exprt op2=expr.op2(); // rounding mode
 
   INVARIANT(
-    ns.follow(op0.type()) == type,
+    op0.type() == type,
     "expression type of operand must match type of expression");
   INVARIANT(
-    ns.follow(op1.type()) == type,
+    op1.type() == type,
     "expression type of operand must match type of expression");
 
   // Remember that floating-point addition is _NOT_ associative.