strongly type the lookup() methods in namespacet

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -1469,7 +1469,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)
   exprt &op0=expr.op0();
   typet type=op0.type();
 
-  follow_symbol(type);
+  type = follow(type);
 
   if(type.id()==ID_incomplete_struct)
   {

src/cpp/cpp_constructor.cpp

@@ -33,8 +33,7 @@ codet cpp_typecheckt::cpp_constructor(
 
   elaborate_class_template(object_tc.type());
 
-  typet tmp_type(object_tc.type());
-  follow_symbol(tmp_type);
+  typet tmp_type(follow(object_tc.type()));
 
   assert(!is_reference(tmp_type));
 

src/cpp/cpp_destructor.cpp

@@ -26,8 +26,7 @@ codet cpp_typecheckt::cpp_destructor(
 
   elaborate_class_template(object.type());
 
-  typet tmp_type(object.type());
-  follow_symbol(tmp_type);
+  typet tmp_type(follow(object.type()));
 
   assert(!is_reference(tmp_type));
 

src/cpp/cpp_instantiate_template.cpp

@@ -189,7 +189,7 @@ void cpp_typecheckt::elaborate_class_template(
   if(type.id()!=ID_symbol)
     return;
 
-  const symbolt &symbol=lookup(type);
+  const symbolt &symbol = lookup(to_symbol_type(type));
 
   // Make a copy, as instantiate will destroy the symbol type!
   const typet t_type=symbol.type;

src/cpp/cpp_typecheck_bases.cpp

@@ -51,8 +51,8 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type)
       throw 0;
     }
 
-    const symbolt &base_symbol=
-      lookup(base_symbol_expr.type());
+    const symbolt &base_symbol =
+      lookup(to_symbol_type(base_symbol_expr.type()));
 
     if(base_symbol.type.id()==ID_incomplete_struct)
     {

src/cpp/cpp_typecheck_expr.cpp

@@ -100,8 +100,8 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr)
     typecheck_type(base);
     typecheck_type(deriv);
 
-    follow_symbol(base);
-    follow_symbol(deriv);
+    base = follow(base);
+    deriv = follow(deriv);
 
     if(base.id()!=ID_struct || deriv.id()!=ID_struct)
       expr=false_exprt();
@@ -1991,7 +1991,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
 
   // look at type of function
 
-  follow_symbol(expr.function().type());
+  expr.function().type() = follow(expr.function().type());
 
   if(expr.function().type().id()==ID_pointer)
   {

src/cpp/cpp_typecheck_resolve.cpp

@@ -352,8 +352,8 @@ exprt cpp_typecheck_resolvet::convert_identifier(
 
       while(followed_type.id()==ID_symbol)
       {
-        typet tmp=cpp_typecheck.lookup(followed_type).type;
-        followed_type=tmp;
+        followed_type =
+          cpp_typecheck.follow(to_symbol_type(followed_type));
         constant |= followed_type.get_bool(ID_C_constant);
       }
 
@@ -1899,8 +1899,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args(
   const exprt &expr,
   const cpp_typecheck_fargst &fargs)
 {
-  typet tmp=expr.type();
-  cpp_typecheck.follow_symbol(tmp);
+  typet tmp = cpp_typecheck.follow(expr.type());
 
   if(!tmp.get_bool(ID_is_template))
     return nil_exprt(); // not a template

src/goto-instrument/wmm/fence.cpp

@@ -19,25 +19,33 @@ bool is_fence(
   const goto_programt::instructiont &instruction,
   const namespacet &ns)
 {
-  return (instruction.is_function_call() && ns.lookup(
-    to_code_function_call(instruction.code).function()).base_name == "fence")
-    /* if assembly-sensitive algorithms are not available */
-    || (instruction.is_other() && instruction.code.get_statement()==ID_fence
-      && instruction.code.get_bool(ID_WWfence)
-      && instruction.code.get_bool(ID_WRfence)
-      && instruction.code.get_bool(ID_RWfence)
-      && instruction.code.get_bool(ID_RRfence));
+  return (instruction.is_function_call() &&
+          ns.lookup(
+              to_symbol_expr(
+                to_code_function_call(instruction.code).function()))
+              .base_name == "fence")
+         /* if assembly-sensitive algorithms are not available */
+         || (instruction.is_other() &&
+             instruction.code.get_statement() == ID_fence &&
+             instruction.code.get_bool(ID_WWfence) &&
+             instruction.code.get_bool(ID_WRfence) &&
+             instruction.code.get_bool(ID_RWfence) &&
+             instruction.code.get_bool(ID_RRfence));
 }
 
 bool is_lwfence(
   const goto_programt::instructiont &instruction,
   const namespacet &ns)
 {
-  return (instruction.is_function_call() && ns.lookup(
-    to_code_function_call(instruction.code).function()).base_name == "lwfence")
-    /* if assembly-sensitive algorithms are not available */
-  || (instruction.is_other() && instruction.code.get_statement()==ID_fence
-      && instruction.code.get_bool(ID_WWfence)
-      && instruction.code.get_bool(ID_RWfence)
-      && instruction.code.get_bool(ID_RRfence));
+  return (instruction.is_function_call() &&
+          ns.lookup(
+              to_symbol_expr(
+                to_code_function_call(instruction.code).function()))
+              .base_name == "lwfence")
+         /* if assembly-sensitive algorithms are not available */
+         || (instruction.is_other() &&
+             instruction.code.get_statement() == ID_fence &&
+             instruction.code.get_bool(ID_WWfence) &&
+             instruction.code.get_bool(ID_RWfence) &&
+             instruction.code.get_bool(ID_RRfence));
 }

src/goto-symex/symex_assign.cpp

@@ -245,7 +245,9 @@ void goto_symext::symex_assign_symbol(
   tmp_guard.append(guard);
 
   // do the assignment
-  const symbolt &symbol=ns.lookup(ssa_lhs.get_original_expr());
+  const symbolt &symbol =
+    ns.lookup(to_symbol_expr(ssa_lhs.get_original_expr()));
+
   if(symbol.is_auxiliary)
     assignment_type=symex_targett::assignment_typet::HIDDEN;
 

src/pointer-analysis/goto_program_dereference.cpp

@@ -28,7 +28,7 @@ bool goto_program_dereferencet::has_failed_symbol(
     if(expr.get_bool("#invalid_object"))
       return false;
 
-    const symbolt &ptr_symbol=ns.lookup(expr);
+    const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr));
 
     const irep_idt &failed_symbol=
       ptr_symbol.type.get("#failed_symbol");

src/util/array_name.cpp

@@ -35,7 +35,7 @@ std::string array_name(
   }
   else if(expr.id()==ID_symbol)
   {
-    const symbolt &symbol=ns.lookup(expr);
+    const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
     return "array `"+id2string(symbol.base_name)+"'";
   }
   else if(expr.id()==ID_string_constant)

src/util/namespace.cpp

@@ -15,10 +15,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
-#include "string2int.h"
-#include "symbol_table.h"
 #include "prefix.h"
+#include "std_expr.h"
 #include "std_types.h"
+#include "string2int.h"
+#include "symbol_table.h"
 
 unsigned get_max(
   const std::string &prefix,
@@ -44,43 +45,37 @@ namespace_baset::~namespace_baset()
 {
 }
 
-void namespace_baset::follow_symbol(irept &irep) const
+const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
 {
-  while(irep.id()==ID_symbol)
-  {
-    const symbolt &symbol=lookup(irep);
+  return lookup(expr.get_identifier());
+}
 
-    if(symbol.is_type)
-    {
-      if(symbol.type.is_nil())
-        return;
-      else
-        irep=symbol.type;
-    }
-    else
-    {
-      if(symbol.value.is_nil())
-        return;
-      else
-        irep=symbol.value;
-    }
-  }
+const symbolt &namespace_baset::lookup(const symbol_typet &type) const
+{
+  return lookup(type.get_identifier());
+}
+
+const symbolt &namespace_baset::lookup(const tag_typet &type) const
+{
+  return lookup(type.get_identifier());
 }
 
 const typet &namespace_baset::follow(const typet &src) const
 {
   if(src.id()!=ID_symbol)
     return src;
 
-  const symbolt *symbol=&lookup(src);
+  const symbolt *symbol = &lookup(to_symbol_type(src));
 
   // let's hope it's not cyclic...
   while(true)
   {
-    assert(symbol->is_type);
-    if(symbol->type.id()!=ID_symbol)
+    DATA_INVARIANT(symbol->is_type, "symbol type points to type");
+
+    if(symbol->type.id() == ID_symbol)
+      symbol = &lookup(to_symbol_type(symbol->type));
+    else
       return symbol->type;
-    symbol=&lookup(symbol->type);
   }
 }
 
@@ -112,7 +107,7 @@ void namespace_baset::follow_macros(exprt &expr) const
 {
   if(expr.id()==ID_symbol)
   {
-    const symbolt &symbol=lookup(expr);
+    const symbolt &symbol = lookup(to_symbol_expr(expr));
 
     if(symbol.is_macro && !symbol.value.is_nil())
     {

src/util/namespace.h

@@ -16,11 +16,14 @@ class symbol_tablet;
 class exprt;
 class symbolt;
 class typet;
-class union_tag_typet;
+class symbol_exprt;
+class symbol_typet;
+class tag_typet;
 class union_typet;
-class struct_tag_typet;
 class struct_typet;
 class c_enum_typet;
+class union_tag_typet;
+class struct_tag_typet;
 class c_enum_tag_typet;
 
 class namespace_baset
@@ -35,22 +38,20 @@ class namespace_baset
     return *symbol;
   }
 
-  const symbolt &lookup(const irept &irep) const
-  {
-    return lookup(irep.get(ID_identifier));
-  }
+  const symbolt &lookup(const symbol_exprt &) const;
+  const symbolt &lookup(const symbol_typet &) const;
+  const symbolt &lookup(const tag_typet &) const;
 
   virtual ~namespace_baset();
 
-  void follow_symbol(irept &irep) const;
-  void follow_macros(exprt &expr) const;
-  const typet &follow(const typet &src) const;
+  void follow_macros(exprt &) const;
+  const typet &follow(const typet &) const;
 
   // These produce union_typet, struct_typet, c_enum_typet or
   // the incomplete version.
-  const typet &follow_tag(const union_tag_typet &src) const;
-  const typet &follow_tag(const struct_tag_typet &src) const;
-  const typet &follow_tag(const c_enum_tag_typet &src) const;
+  const typet &follow_tag(const union_tag_typet &) const;
+  const typet &follow_tag(const struct_tag_typet &) const;
+  const typet &follow_tag(const c_enum_tag_typet &) const;
 
   /// Returns the maximum integer n such that there is a symbol (in some of the
   /// symbol tables) whose name is of the form "AB" where A is \p prefix and B

src/util/simplify_expr_int.cpp

@@ -1347,8 +1347,8 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
      (expr.id()==ID_equal || expr.id()==ID_notequal))
     return simplify_inequality_pointer_object(expr);
 
-  ns.follow_symbol(tmp0.type());
-  ns.follow_symbol(tmp1.type());
+  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()));

src/util/type_eq.cpp

@@ -11,11 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "type_eq.h"
 
-#include <cassert>
-
-#include "type.h"
-#include "symbol.h"
 #include "namespace.h"
+#include "std_types.h"
+#include "symbol.h"
 
 bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
 {
@@ -24,7 +22,7 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
 
   if(type1.id()==ID_symbol)
   {
-    const symbolt &symbol=ns.lookup(type1);
+    const symbolt &symbol = ns.lookup(to_symbol_type(type1));
     if(!symbol.is_type)
       throw "symbol "+id2string(symbol.name)+" is not a type";
 
@@ -33,7 +31,7 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
 
   if(type2.id()==ID_symbol)
   {
-    const symbolt &symbol=ns.lookup(type2);
+    const symbolt &symbol = ns.lookup(to_symbol_type(type2));
     if(!symbol.is_type)
       throw "symbol "+id2string(symbol.name)+" is not a type";