From ccf528ee36f52022cffff6d30fde24cbd8c9c3c9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 9 Jan 2019 14:07:35 +0000
Subject: [PATCH 1/4] Remove unnecessary use of ns.follow from pointer
 predicates

This also makes the namespace unnecessary in three cases.
---
 src/analyses/goto_check.cpp     |  6 ++--
 src/util/pointer_predicates.cpp | 57 ++++++++++++---------------------
 src/util/pointer_predicates.h   |  3 --
 3 files changed, 24 insertions(+), 42 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 7c5b64133b5..319f1852739 100644
--- a/src/analyses/goto_check.cpp
+++ b/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(
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index 93fb6f45c34..89d1e4ddf3a 100644
--- a/src/util/pointer_predicates.cpp
+++ b/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);
diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h
index f83588df8fe..a0c88d1192e 100644
--- a/src/util/pointer_predicates.h
+++ b/src/util/pointer_predicates.h
@@ -33,7 +33,6 @@ 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,
@@ -41,11 +40,9 @@ exprt dynamic_object_upper_bound(
   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

From 1837ea7d3340240b5d93fc4a3a959ca8d707d7e0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 9 Jan 2019 14:08:20 +0000
Subject: [PATCH 2/4] Replace use of ns.follow by type_eq

Using ns.follow on both sides of an operator== is better encapsulated in
type_eq.
---
 src/util/allocate_objects.cpp     | 3 ++-
 src/util/simplify_expr_struct.cpp | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp
index 2da68a84dac..6c00c9ae808 100644
--- a/src/util/allocate_objects.cpp
+++ b/src/util/allocate_objects.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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();
 
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 1e162ce03cc..4c94ec00fc0 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -200,7 +200,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
   else if(op.id()==ID_union && op_type.id()==ID_union)
   {
     // trivial?
-    if(ns.follow(to_union_expr(op).op().type())==ns.follow(expr.type()))
+    if(type_eq(to_union_expr(op).op().type(), expr.type(), ns))
     {
       exprt tmp=to_union_expr(op).op();
       expr.swap(tmp);

From 01ede2d6ec31aef29b17f6ac1ad23c22d33b3093 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 9 Jan 2019 14:09:30 +0000
Subject: [PATCH 3/4] Remove ns.follow when types cannot be hidden behind tags

Neither arrays nor Booleans use tag types.
---
 src/util/expr_initializer.cpp | 2 +-
 src/util/expr_util.cpp        | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index cb981543d0a..994dc3c9ec4 100644
--- a/src/util/expr_initializer.cpp
+++ b/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;
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index e30d6f36f69..72d0a6d899f 100644
--- a/src/util/expr_util.cpp
+++ b/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

From d48e62b512475b4bb577de8b77c46ce6b266e1a8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 9 Jan 2019 14:27:23 +0000
Subject: [PATCH 4/4] Remove unnecessary uses of ns.follow from the simplifier

There is no need to use ns.follow when either 1) we only compare the result to
types that can never be hidden behind tags or 2) the tag case is handled
explicitly.
---
 src/util/simplify_expr.cpp         | 23 ++++++++++++-----------
 src/util/simplify_expr_floatbv.cpp | 20 ++++++++++----------
 src/util/simplify_expr_int.cpp     | 25 +++++++++++--------------
 src/util/simplify_expr_pointer.cpp | 18 ++++++------------
 4 files changed, 39 insertions(+), 47 deletions(-)

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 6c33946460a..8dc39db06da 100644
--- a/src/util/simplify_expr.cpp
+++ b/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)
   {
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index fbdfa283595..2ffda22887b 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/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.
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index b92549780e1..9b968201391 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -447,7 +447,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
   // floating-point addition is _NOT_ associative; thus,
   // there is special case for float
 
-  if(ns.follow(plus_expr.type()).id() == ID_floatbv)
+  if(plus_expr.type().id() == ID_floatbv)
   {
     // we only merge neighboring constants!
     Forall_expr(it, operands)
@@ -660,9 +660,9 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
     forall_operands(it, expr)
     {
-      if(it->id()==ID_typecast &&
-         it->operands().size()==1 &&
-         ns.follow(it->op0().type()).id()==ID_bool)
+      if(
+        it->id() == ID_typecast && it->operands().size() == 1 &&
+        it->op0().type().id() == ID_bool)
       {
       }
       else if(it->is_zero() || it->is_one())
@@ -1355,9 +1355,6 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
      (expr.id()==ID_equal || expr.id()==ID_notequal))
     return simplify_inequality_pointer_object(expr);
 
-  tmp0.type() = ns.follow(tmp0.type());
-  tmp1.type() = ns.follow(tmp1.type());
-
   if(tmp0.type().id()==ID_c_enum_tag)
     tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
 
@@ -1547,7 +1544,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
   // pretty much all of the simplifications below are unsound
   // for IEEE float because of NaN!
 
-  if(ns.follow(expr.op0().type()).id()==ID_floatbv)
+  if(expr.op0().type().id() == ID_floatbv)
     return true;
 
   // eliminate strict inequalities
@@ -1800,18 +1797,18 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
   // (double)value REL const ---> value rel const
   // if 'const' can be represented exactly.
 
-  if(expr.op0().id()==ID_typecast &&
-     expr.op0().operands().size()==1 &&
-     ns.follow(expr.op0().type()).id()==ID_floatbv &&
-     ns.follow(expr.op0().op0().type()).id()==ID_floatbv)
+  if(
+    expr.op0().id() == ID_typecast && expr.op0().operands().size() == 1 &&
+    expr.op0().type().id() == ID_floatbv &&
+    expr.op0().op0().type().id() == ID_floatbv)
   {
     ieee_floatt const_val(to_constant_expr(expr.op1()));
     ieee_floatt const_val_converted=const_val;
     const_val_converted.change_spec(
-      ieee_float_spect(to_floatbv_type(ns.follow(expr.op0().op0().type()))));
+      ieee_float_spect(to_floatbv_type(expr.op0().op0().type())));
     ieee_floatt const_val_converted_back=const_val_converted;
     const_val_converted_back.change_spec(
-      ieee_float_spect(to_floatbv_type(ns.follow(expr.op0().type()))));
+      ieee_float_spect(to_floatbv_type(expr.op0().type())));
     if(const_val_converted_back==const_val)
     {
       exprt result=expr;
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 671c555dc01..af27c2a89bd 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -177,7 +177,7 @@ bool simplify_exprt::simplify_address_of(exprt &expr)
   if(expr.operands().size()!=1)
     return true;
 
-  if(ns.follow(expr.type()).id()!=ID_pointer)
+  if(expr.type().id() != ID_pointer)
     return true;
 
   exprt &object=expr.op0();
@@ -249,7 +249,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     if(ptr.operands().size()!=1)
       return true;
 
-    const typet &op_type=ns.follow(ptr.op0().type());
+    const typet &op_type = ptr.op0().type();
 
     if(op_type.id()==ID_pointer)
     {
@@ -281,7 +281,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
         // We do a bit of special treatment for (TYPE *)(a+(int)&o),
         // which is re-written to 'a'.
 
-        typet type=ns.follow(expr.type());
+        typet type = expr.type();
         exprt tmp=ptr.op0();
         if(tmp.id()==ID_plus && tmp.operands().size()==2)
         {
@@ -289,9 +289,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
              tmp.op0().operands().size()==1 &&
              tmp.op0().op0().id()==ID_address_of)
           {
-            expr=tmp.op1();
-            if(type!=expr.type())
-              expr.make_typecast(type);
+            expr = typecast_exprt::conditional_cast(tmp.op1(), type);
 
             simplify_node(expr);
             return false;
@@ -300,9 +298,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
                   tmp.op1().operands().size()==1 &&
                   tmp.op1().op0().id()==ID_address_of)
           {
-            expr=tmp.op0();
-            if(type!=expr.type())
-              expr.make_typecast(type);
+            expr = typecast_exprt::conditional_cast(tmp.op0(), type);
 
             simplify_node(expr);
             return false;
@@ -664,9 +660,7 @@ bool simplify_exprt::simplify_object_size(exprt &expr)
     if(op.op0().id()==ID_symbol)
     {
       // just get the type
-      const typet &type=ns.follow(op.op0().type());
-
-      exprt size=size_of_expr(type, ns);
+      exprt size = size_of_expr(op.op0().type(), ns);
 
       if(size.is_not_nil())
       {