Remove base_type_eq

We consistently use tag types, and two expressions are now base_type_eq if, and
only if, they have types that compare equal.

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -92,10 +92,10 @@ warning: Included by graph for 'expr_util.h' not generated, too many nodes (60),
 warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'namespace.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'namespace.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_types.h' not generated, too many nodes (123), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/does_remove_const.cpp

@@ -15,7 +15,6 @@ Author: Diffblue Ltd.
 #include <util/type.h>
 #include <util/expr.h>
 #include <util/std_code.h>
-#include <util/base_type.h>
 
 /// A naive analysis to look for casts that remove const-ness from pointers.
 /// \param goto_program: the goto program to check
@@ -74,7 +73,7 @@ bool does_remove_constt::does_expr_lose_const(const exprt &expr) const
   for(const exprt &op : expr.operands())
   {
     const typet &op_type=op.type();
-    if(base_type_eq(op_type, root_type, ns))
+    if(op_type == root_type)
     {
       // Is this child more const-qualified than the root
       if(!does_type_preserve_const_correctness(&root_type, &op_type))

src/goto-instrument/replace_calls.cpp

@@ -15,7 +15,6 @@ Author: Daniel Poetzl
 
 #include <goto-programs/remove_returns.h>
 
-#include <util/base_type.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/irep.h>
@@ -165,12 +164,13 @@ void replace_callst::check_replacement_map(
     auto it1 = goto_functions.function_map.find(p.first);
     if(it1 != goto_functions.function_map.end())
     {
-      if(!base_type_eq(
-           ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns))
+      if(ns.lookup(it1->first).type != ns.lookup(it2->first).type)
+      {
         throw invalid_command_line_argument_exceptiont(
           "functions " + id2string(p.first) + " and " + id2string(p.second) +
             " are not type-compatible",
           "--replace-calls");
+      }
     }
   }
 }

src/goto-instrument/value_set_fi_fp_removal.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <pointer-analysis/value_set_analysis_fi.h>
 
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/expanding_vector.h>
 #include <util/fresh_symbol.h>

src/goto-programs/goto_program.cpp

@@ -14,7 +14,6 @@ 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>
@@ -740,7 +739,7 @@ void goto_programt::instructiont::validate(
         if(!ns.lookup(goto_id, table_symbol))
         {
           bool symbol_expr_type_matches_symbol_table =
-            base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
+            goto_symbol_expr.type() == table_symbol->type;
 
           if(
             !symbol_expr_type_matches_symbol_table &&
@@ -763,7 +762,7 @@ void goto_programt::instructiont::validate(
                 table_symbol_type.return_type();
 
               symbol_expr_type_matches_symbol_table =
-                base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
+                goto_symbol_expr_type == table_symbol_type;
             }
           }
 

src/goto-programs/link_goto_model.cpp

@@ -13,7 +13,6 @@ Author: Michael Tautschnig, Daniel Kroening
 
 #include <unordered_set>
 
-#include <util/base_type.h>
 #include <util/symbol.h>
 #include <util/rename_symbol.h>
 
@@ -123,15 +122,14 @@ static bool link_functions(
       INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
       const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
 
-      #if 0
-      if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
+#if 0
+      if(symbol.type != ns.lookup(id).type)
       {
         std::cerr << symbol << '\n';
         std::cerr << ns.lookup(id) << '\n';
       }
-      INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
-                "type matches");
-      #endif
+      INVARIANT(symbol.type == ns.lookup(id).type, "type matches");
+#endif
 
       macro_application.insert_expr(symbol.name, id);
     }

src/linking/linking.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <deque>
 #include <unordered_set>
 
-#include <util/base_type.h>
 #include <util/find_symbols.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
@@ -139,8 +138,7 @@ void linkingt::detailed_conflict_report_rec(
   else if(t1.id()==ID_pointer ||
           t1.id()==ID_array)
   {
-    if(depth>0 &&
-       !base_type_eq(t1.subtype(), t2.subtype(), ns))
+    if(depth > 0 && t1.subtype() != t2.subtype())
     {
       if(conflict_path.type().id() == ID_pointer)
         conflict_path = dereference_exprt(conflict_path);
@@ -189,7 +187,7 @@ void linkingt::detailed_conflict_report_rec(
           msg+=id2string(components2[i].get_name())+')';
           break;
         }
-        else if(!base_type_eq(subtype1, subtype2, ns))
+        else if(subtype1 != subtype2)
         {
           typedef std::unordered_set<typet, irep_hash> type_sett;
           type_sett parent_types;
@@ -313,7 +311,7 @@ void linkingt::detailed_conflict_report_rec(
       msg+=std::to_string(parameters1.size())+'/';
       msg+=std::to_string(parameters2.size())+')';
     }
-    else if(!base_type_eq(return_type1, return_type2, ns))
+    else if(return_type1 != return_type2)
     {
       conflict_path=
         index_exprt(conflict_path,
@@ -337,7 +335,7 @@ void linkingt::detailed_conflict_report_rec(
         const typet &subtype1=parameters1[i].type();
         const typet &subtype2=parameters2[i].type();
 
-        if(!base_type_eq(subtype1, subtype2, ns))
+        if(subtype1 != subtype2)
         {
           conflict_path=
             index_exprt(conflict_path,
@@ -456,7 +454,7 @@ void linkingt::duplicate_code_symbol(
   symbolt &new_symbol)
 {
   // Both are functions.
-  if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
+  if(old_symbol.type != new_symbol.type)
   {
     const code_typet &old_t=to_code_type(old_symbol.type);
     const code_typet &new_t=to_code_type(new_symbol.type);
@@ -467,11 +465,8 @@ void linkingt::duplicate_code_symbol(
     // casts we need to fail hard
     if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil())
     {
-      if(base_type_eq(old_t.return_type(), new_t.return_type(), ns))
-         link_warning(
-           old_symbol,
-           new_symbol,
-           "implicit function declaration");
+      if(old_t.return_type() == new_t.return_type())
+        link_warning(old_symbol, new_symbol, "implicit function declaration");
       else
         link_error(
           old_symbol,
@@ -485,7 +480,7 @@ void linkingt::duplicate_code_symbol(
     else if(
       new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil())
     {
-      if(base_type_eq(old_t.return_type(), new_t.return_type(), ns))
+      if(old_t.return_type() == new_t.return_type())
         link_warning(
           old_symbol,
           new_symbol,
@@ -497,13 +492,12 @@ void linkingt::duplicate_code_symbol(
           "implicit function declaration");
     }
     // handle (incomplete) function prototypes
-    else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
-            ((old_t.parameters().empty() &&
-              old_t.has_ellipsis() &&
-              old_symbol.value.is_nil()) ||
-             (new_t.parameters().empty() &&
-              new_t.has_ellipsis() &&
-              new_symbol.value.is_nil())))
+    else if(
+      old_t.return_type() == new_t.return_type() &&
+      ((old_t.parameters().empty() && old_t.has_ellipsis() &&
+        old_symbol.value.is_nil()) ||
+       (new_t.parameters().empty() && new_t.has_ellipsis() &&
+        new_symbol.value.is_nil())))
     {
       if(old_t.parameters().empty() &&
          old_t.has_ellipsis() &&
@@ -553,9 +547,9 @@ void linkingt::duplicate_code_symbol(
     }
     // conflicting declarations without a definition, matching return
     // types
-    else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
-            old_symbol.value.is_nil() &&
-            new_symbol.value.is_nil())
+    else if(
+      old_t.return_type() == new_t.return_type() && old_symbol.value.is_nil() &&
+      new_symbol.value.is_nil())
     {
       link_warning(
         old_symbol,
@@ -594,7 +588,7 @@ void linkingt::duplicate_code_symbol(
       typedef std::deque<std::pair<typet, typet> > conflictst;
       conflictst conflicts;
 
-      if(!base_type_eq(old_t.return_type(), new_t.return_type(), ns))
+      if(old_t.return_type() != new_t.return_type())
         conflicts.push_back(
           std::make_pair(old_t.return_type(), new_t.return_type()));
 
@@ -606,7 +600,7 @@ void linkingt::duplicate_code_symbol(
           n_it!=new_t.parameters().end();
           ++o_it, ++n_it)
       {
-        if(!base_type_eq(o_it->type(), n_it->type(), ns))
+        if(o_it->type() != n_it->type())
           conflicts.push_back(
             std::make_pair(o_it->type(), n_it->type()));
       }
@@ -699,7 +693,7 @@ void linkingt::duplicate_code_symbol(
 
           bool found=false;
           for(const auto &c : union_type.components())
-            if(base_type_eq(c.type(), src_type, ns))
+            if(c.type() == src_type)
             {
               found=true;
               if(warn_msg.empty())
@@ -774,7 +768,7 @@ void linkingt::duplicate_code_symbol(
     {
       // ok, silently ignore
     }
-    else if(base_type_eq(old_symbol.type, new_symbol.type, ns))
+    else if(old_symbol.type == new_symbol.type)
     {
       // keep the one in old_symbol -- libraries come last!
       warning().source_location=new_symbol.location;
@@ -797,7 +791,7 @@ bool linkingt::adjust_object_type_rec(
   const typet &t2,
   adjust_type_infot &info)
 {
-  if(base_type_eq(t1, t2, ns))
+  if(t1 == t2)
     return false;
 
   if(
@@ -993,7 +987,7 @@ void linkingt::duplicate_object_symbol(
   // both are variables
   bool set_to_new = false;
 
-  if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
+  if(old_symbol.type != new_symbol.type)
   {
     bool failed=
       adjust_object_type(old_symbol, new_symbol, set_to_new);
@@ -1051,7 +1045,7 @@ void linkingt::duplicate_object_symbol(
       simplify(tmp_old, ns);
       simplify(tmp_new, ns);
 
-      if(base_type_eq(tmp_old, tmp_new, ns))
+      if(tmp_old == tmp_new)
       {
         // ok, the same
       }
@@ -1176,9 +1170,9 @@ void linkingt::duplicate_type_symbol(
     return;
   }
 
-  if(old_symbol.type.id()==ID_array &&
-     new_symbol.type.id()==ID_array &&
-     base_type_eq(old_symbol.type.subtype(), new_symbol.type.subtype(), ns))
+  if(
+    old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
+    old_symbol.type.subtype() == new_symbol.type.subtype())
   {
     if(to_array_type(old_symbol.type).size().is_nil() &&
        to_array_type(new_symbol.type).size().is_not_nil())
@@ -1248,9 +1242,9 @@ bool linkingt::needs_renaming_type(
     to_union_type(new_symbol.type).is_incomplete())
     return false; // not different
 
-  if(old_symbol.type.id()==ID_array &&
-     new_symbol.type.id()==ID_array &&
-     base_type_eq(old_symbol.type.subtype(), new_symbol.type.subtype(), ns))
+  if(
+    old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
+    old_symbol.type.subtype() == new_symbol.type.subtype())
   {
     if(to_array_type(old_symbol.type).size().is_nil() &&
        to_array_type(new_symbol.type).size().is_not_nil())

src/util/Makefile

@@ -2,7 +2,6 @@ SRC = allocate_objects.cpp \
       arith_tools.cpp \
       array_element_from_pointer.cpp \
       array_name.cpp \
-      base_type.cpp \
       bv_arithmetic.cpp \
       byte_operators.cpp \
       c_types.cpp \