diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b3d7389f995..7c3e914ddfa 100644 --- 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 index 4639103e47e..252a9cb935e 100644 --- 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 index 273c59fbde4..82d796b18aa 100644 --- 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 index 50da8557d3b..44790ed2a42 100644 --- 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 index 26d2efb210e..a9cabf3c112 100644 --- 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 index 45d7c872759..3a5ac9cd9c0 100644 --- 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 index 647e1e14e46..3eca6b3bc12 100644 --- 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 index 82e9308278d..0e0fe44f37c 100644 --- 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 index 2c95736ed42..9642d148e56 100644 --- 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 index efc0dd510fd..71496fabece 100644 --- 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 index a4bfa42c8df..450b95b3713 100644 --- 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 index 5329755d0cc..5c98d53019e 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -15,10 +15,11 @@ Author: Daniel Kroening, kroening@kroening.com #include -#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,27 +45,19 @@ 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 @@ -72,15 +65,17 @@ 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 index a72a3ba8a19..43acc8a80dd 100644 --- 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 index da3c03da448..e8346901bd7 100644 --- 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 index 0f78c20880f..5fc587f58e3 100644 --- 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 - -#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";