Merge pull request #4314 from tautschnig/base_type-object-types

Do not use base_type_eq with non-code types [blocks: #4056]

Author: tautschnig

jbmc/unit/java-testing-utils/require_type.cpp

@@ -9,7 +9,6 @@ Author: Diffblue Ltd.
 #include "require_type.h"
 
 #include <testing-utils/use_catch.h>
-#include <util/base_type.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
@@ -26,10 +25,8 @@ pointer_typet require_type::require_pointer(
   const pointer_typet &pointer = to_pointer_type(type);
 
   if(subtype)
-  {
-    namespacet ns{symbol_tablet{}};
-    base_type_eq(pointer.subtype(), subtype.value(), ns);
-  }
+    REQUIRE(pointer.subtype() == subtype.value());
+
   return pointer;
 }
 

src/analyses/constant_propagator.cpp

@@ -17,7 +17,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
@@ -103,7 +102,7 @@ void constant_propagator_domaint::assign_rec(
     if(dest_values.is_constant(tmp))
     {
       DATA_INVARIANT(
-        base_type_eq(ns.lookup(s).type, tmp.type(), ns),
+        ns.lookup(s).type == tmp.type(),
         "type of constant to be replaced should match");
       dest_values.set_to(s, tmp);
     }
@@ -624,7 +623,7 @@ bool constant_propagator_domaint::valuest::meet(
     {
       const typet &m_id_type = ns.lookup(m.first).type;
       DATA_INVARIANT(
-        base_type_eq(m_id_type, m.second.type(), ns),
+        m_id_type == m.second.type(),
         "type of constant to be stored should match");
       set_to(symbol_exprt(m.first, m_id_type), m.second);
       changed=true;

src/goto-instrument/dump_c.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "dump_c.h"
 
-#include <util/base_type.h>
 #include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -1277,9 +1276,9 @@ void dump_ct::cleanup_expr(exprt &expr)
       expr.swap(tmp);
     }
   }
-  else if(expr.id()==ID_typecast &&
-      expr.op0().id()==ID_typecast &&
-      base_type_eq(expr.type(), expr.op0().type(), ns))
+  else if(
+    expr.id() == ID_typecast && expr.op0().id() == ID_typecast &&
+    expr.type() == expr.op0().type())
   {
     exprt tmp=expr.op0();
     expr.swap(tmp);
@@ -1309,8 +1308,7 @@ void dump_ct::cleanup_expr(exprt &expr)
           if(type.id()==ID_union &&
              type.get_bool(ID_C_transparent_union))
           {
-            if(it2->id()==ID_typecast &&
-               base_type_eq(it2->type(), type, ns))
+            if(it2->id() == ID_typecast && it2->type() == type)
               *it2=to_typecast_expr(*it2).op();
 
             // add a typecast for NULL or 0

src/goto-programs/goto_inline_class.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
-#include <util/base_type.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -83,7 +82,7 @@ void goto_inlinet::parameter_assignments(
     {
       // it should be the same exact type as the parameter,
       // subject to some exceptions
-      if(!base_type_eq(parameter_type, actual.type(), ns))
+      if(parameter_type != actual.type())
       {
         const typet &f_partype = parameter_type;
         const typet &f_acttype = actual.type();

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>
 
+#include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -715,10 +716,9 @@ void goto_programt::instructiont::validate(
             // Return removal sets the return type of a function symbol table
             // entry to 'void', but some callsites still expect the original
             // type (e.g. if a function is passed as a parameter)
-            symbol_expr_type_matches_symbol_table = base_type_eq(
-              goto_symbol_expr.type(),
-              original_return_type(ns.get_symbol_table(), goto_id),
-              ns);
+            symbol_expr_type_matches_symbol_table =
+              goto_symbol_expr.type() ==
+              original_return_type(ns.get_symbol_table(), goto_id);
 
             if(
               !symbol_expr_type_matches_symbol_table &&
@@ -760,8 +760,8 @@ void goto_programt::instructiont::validate(
               auto symbol_table_array_type = to_array_type(table_symbol->type);
               symbol_table_array_type.size() = nil_exprt();
 
-              symbol_expr_type_matches_symbol_table = base_type_eq(
-                goto_symbol_expr.type(), symbol_table_array_type, ns);
+              symbol_expr_type_matches_symbol_table =
+                goto_symbol_expr.type() == symbol_table_array_type;
             }
           }
 

src/goto-programs/graphml_witness.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening
 
 #include "graphml_witness.h"
 
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/arith_tools.h>
@@ -75,8 +74,9 @@ std::string graphml_witnesst::convert_assign_rec(
   {
     // dereferencing may have resulted in an lhs that is the first
     // struct member; undo this
-    if(assign.lhs().id()==ID_member &&
-       !base_type_eq(assign.lhs().type(), assign.rhs().type(), ns))
+    if(
+      assign.lhs().id() == ID_member &&
+      assign.lhs().type() != assign.rhs().type())
     {
       code_assignt tmp=assign;
       tmp.lhs()=to_member_expr(assign.lhs()).struct_op();

src/goto-programs/wp.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/base_type.h>
 
 #include <util/invariant.h>
 
@@ -79,7 +78,7 @@ aliasingt aliasing(
     return aliasing(e1, e2.op0().op0(), ns);
 
   // fairly radical. Ignores struct prefixes and the like.
-  if(!base_type_eq(e1.type(), e2.type(), ns))
+  if(e1.type() != e2.type())
     return aliasingt::A_MUSTNOT;
 
   // syntactically the same?

src/goto-symex/symex_assign.cpp

@@ -27,8 +27,7 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
   exprt rhs=code.rhs();
 
   DATA_INVARIANT(
-    base_type_eq(lhs.type(), rhs.type(), ns),
-    "assignments must be type consistent");
+    lhs.type() == rhs.type(), "assignments must be type consistent");
 
   clean_expr(lhs, state, true);
   clean_expr(rhs, state, false);

src/goto-symex/symex_clean_expr.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
@@ -37,7 +36,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     process_array_expr(if_expr.true_case(), do_simplify, ns);
     process_array_expr(if_expr.false_case(), do_simplify, ns);
 
-    if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
+    if(if_expr.true_case() != if_expr.false_case())
     {
       byte_extract_exprt be(
         byte_extract_id(),

src/goto-symex/symex_dereference.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
@@ -61,7 +60,7 @@ exprt goto_symext::address_arithmetic(
 
       // turn &a of type T[i][j] into &(a[0][0])
       for(const typet *t = &(a.type().subtype());
-          t->id() == ID_array && !base_type_eq(expr.type(), *t, ns);
+          t->id() == ID_array && expr.type() != *t;
           t = &(t->subtype()))
         a.object()=index_exprt(a.object(), from_integer(0, index_type()));
     }
@@ -184,9 +183,10 @@ exprt goto_symext::address_arithmetic(
       "goto_symext::address_arithmetic does not handle " + expr.id_string());
 
   const typet &expr_type = expr.type();
-  INVARIANT((expr_type.id()==ID_array && !keep_array) ||
-            base_type_eq(pointer_type(expr_type), result.type(), ns),
-            "either non-persistent array or pointer to result");
+  INVARIANT(
+    (expr_type.id() == ID_array && !keep_array) ||
+      pointer_type(expr_type) == result.type(),
+    "either non-persistent array or pointer to result");
 
   return result;
 }
@@ -286,12 +286,11 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
     exprt &tc_op=to_typecast_expr(expr).op();
 
     // turn &array into &array[0] when casting to pointer-to-element-type
-    if(tc_op.id()==ID_address_of &&
-       to_address_of_expr(tc_op).object().type().id()==ID_array &&
-       base_type_eq(
-         expr.type(),
-         pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
-         ns))
+    if(
+      tc_op.id() == ID_address_of &&
+      to_address_of_expr(tc_op).object().type().id() == ID_array &&
+      expr.type() ==
+        pointer_type(to_address_of_expr(tc_op).object().type().subtype()))
     {
       expr=
         address_of_exprt(