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(

src/goto-symex/symex_function_call.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>
@@ -80,7 +79,7 @@ void goto_symext::parameter_assignments(
     else
     {
       // It should be the same exact type.
-      if(!base_type_eq(parameter_type, rhs.type(), ns))
+      if(parameter_type != rhs.type())
       {
         const typet &rhs_type = rhs.type();
 

src/goto-symex/symex_other.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>
@@ -149,7 +148,7 @@ void goto_symext::symex_other(
     process_array_expr(state, src_array);
 
     // check for size (or type) mismatch and adjust
-    if(!base_type_eq(dest_array.type(), src_array.type(), ns))
+    if(dest_array.type() != src_array.type())
     {
       if(statement==ID_array_copy)
       {
@@ -217,7 +216,7 @@ void goto_symext::symex_other(
 
     const array_typet &array_type = to_array_type(array_expr.type());
 
-    if(!base_type_eq(array_type.subtype(), value.type(), ns))
+    if(array_type.subtype() != value.type())
       value = typecast_exprt(value, array_type.subtype());
 
     code_assignt assignment(array_expr, array_of_exprt(value, array_type));
@@ -250,7 +249,7 @@ void goto_symext::symex_other(
     code_assignt assignment(code.op2(), equal_exprt(array1, array2));
 
     // check for size (or type) mismatch
-    if(!base_type_eq(array1.type(), array2.type(), ns))
+    if(array1.type() != array2.type())
       assignment.lhs() = false_exprt();
 
     symex_assign(state, assignment);

src/goto-symex/symex_target_equation.cpp

@@ -940,7 +940,7 @@ void symex_target_equationt::SSA_stept::validate(
     validate_full_expr(ssa_rhs, ns, vm);
     DATA_CHECK(
       vm,
-      base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
+      ssa_lhs.get_original_expr().type() == ssa_rhs.type(),
       "Type inequality in SSA assignment\nlhs-type: " +
         ssa_lhs.get_original_expr().type().id_string() +
         "\nrhs-type: " + ssa_rhs.type().id_string());

src/pointer-analysis/value_set.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
@@ -1155,10 +1154,10 @@ void value_sett::assign(
       }
       else
       {
-        if(!base_type_eq(rhs.type(), type, ns))
+        if(rhs.type() != lhs.type())
           throw "value_sett::assign type mismatch: "
                 "rhs.type():\n"+rhs.type().pretty()+"\n"+
-                "type:\n"+type.pretty();
+                "lhs.type():\n"+lhs.type().pretty();
 
         rhs_member=make_member(rhs, name, ns);
 
@@ -1183,7 +1182,7 @@ void value_sett::assign(
     }
     else
     {
-      if(!base_type_eq(rhs.type(), type, ns))
+      if(rhs.type() != type)
         throw "value_sett::assign type mismatch: "
           "rhs.type():\n"+rhs.type().pretty()+"\n"+
           "type:\n"+type.pretty();

src/pointer-analysis/value_set_dereference.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/array_name.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/config.h>
@@ -208,7 +207,7 @@ bool value_set_dereferencet::dereference_type_compare(
 #endif
   }
 
-  if(base_type_eq(object_type, dereference_type, ns))
+  if(object_type == dereference_type)
     return true; // ok, they just match
 
   // check for struct prefixes
@@ -314,7 +313,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
     const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
 
-    if(base_type_eq(memory_symbol.type.subtype(), dereference_type, ns))
+    if(memory_symbol.type.subtype() == dereference_type)
     {
       // Types match already, what a coincidence!
       // We can use an index expression.

src/pointer-analysis/value_set_fi.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
 #include <util/std_expr.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
@@ -990,10 +989,10 @@ void value_set_fit::assign(
       }
       else
       {
-        if(!base_type_eq(rhs.type(), type, ns))
+        if(rhs.type() != lhs.type())
           throw "value_set_fit::assign type mismatch: "
                 "rhs.type():\n"+rhs.type().pretty()+"\n"+
-                "type:\n"+type.pretty();
+                "type:\n"+lhs.type().pretty();
 
         if(rhs.id()==ID_struct ||
            rhs.id()==ID_constant)
@@ -1051,7 +1050,7 @@ void value_set_fit::assign(
     }
     else
     {
-      if(!base_type_eq(rhs.type(), type, ns))
+      if(rhs.type() != type)
         throw "value_set_fit::assign type mismatch: "
               "rhs.type():\n"+rhs.type().pretty()+"\n"+
               "type:\n"+type.pretty();