strongly type the lookup() methods in namespacet

Daniel Kroening · Daniel Kroening · commit d77dea3c238b · 2018-05-19T09:01:18.000+01:00
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/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)
   {
diff --git a/src/cpp/cpp_constructor.cpp b/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));
 
diff --git a/src/cpp/cpp_destructor.cpp b/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));
 
diff --git a/src/cpp/cpp_instantiate_template.cpp b/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;
diff --git a/src/cpp/cpp_typecheck_bases.cpp b/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)
     {
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/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)
   {
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/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
diff --git a/src/goto-instrument/wmm/fence.cpp b/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));
 }
diff --git a/src/goto-symex/symex_assign.cpp b/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;
 
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/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");
diff --git a/src/util/array_name.cpp b/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)
diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp
@@ -15,10 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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())
     {
diff --git a/src/util/namespace.h b/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
diff --git a/src/util/simplify_expr_int.cpp 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()));
diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp
@@ -11,11 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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";
 

Original file line number	Diff line number	Diff line change
`@@ -1469,7 +1469,7 @@ void c_typecheck_baset::typecheck_expr_member(exprt &expr)`
`1469`	`1469`	`exprt &op0=expr.op0();`
`1470`	`1470`	`typet type=op0.type();`
`1471`	`1471`
`1472`		`- follow_symbol(type);`
	`1472`	`+ type = follow(type);`
`1473`	`1473`
`1474`	`1474`	`if(type.id()==ID_incomplete_struct)`
`1475`	`1475`	`{`
Original file line number	Diff line number	Diff line change
`@@ -51,8 +51,8 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type)`
`51`	`51`	`throw 0;`
`52`	`52`	`}`
`53`	`53`
`54`		`- const symbolt &base_symbol=`
`55`		`- lookup(base_symbol_expr.type());`
	`54`	`+ const symbolt &base_symbol =`
	`55`	`+ lookup(to_symbol_type(base_symbol_expr.type()));`
`56`	`56`
`57`	`57`	`if(base_symbol.type.id()==ID_incomplete_struct)`
`58`	`58`	`{`
Original file line number	Diff line number	Diff line change
`@@ -352,8 +352,8 @@ exprt cpp_typecheck_resolvet::convert_identifier(`
`352`	`352`
`353`	`353`	`while(followed_type.id()==ID_symbol)`
`354`	`354`	`{`
`355`		`- typet tmp=cpp_typecheck.lookup(followed_type).type;`
`356`		`- followed_type=tmp;`
	`355`	`+ followed_type =`
	`356`	`+ cpp_typecheck.follow(to_symbol_type(followed_type));`
`357`	`357`	`constant \|= followed_type.get_bool(ID_C_constant);`
`358`	`358`	`}`
`359`	`359`
`@@ -1899,8 +1899,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args(`
`1899`	`1899`	`const exprt &expr,`
`1900`	`1900`	`const cpp_typecheck_fargst &fargs)`
`1901`	`1901`	`{`
`1902`		`- typet tmp=expr.type();`
`1903`		`- cpp_typecheck.follow_symbol(tmp);`
	`1902`	`+ typet tmp = cpp_typecheck.follow(expr.type());`
`1904`	`1903`
`1905`	`1904`	`if(!tmp.get_bool(ID_is_template))`
`1906`	`1905`	`return nil_exprt(); // not a template`