replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #4264 from diffblue/cleanout-symbol_type 

remove symbol_typet [blocks: #4056]
This commit is contained in:
Michael Tautschnig 2019-02-28 16:33:02 +00:00 committed by GitHub
parent be4cee2fa9 44858f2464
commit ca54005a12
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
36 changed files with 96 additions and 344 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/analyses/invariant_propagation.cpp
View File

@ -191,8 +191,6 @@ bool invariant_propagationt::check_type(const typet &type) const
return false;
else if(type.id()==ID_array)
return false;
else if(type.id() == ID_symbol_type)
return check_type(ns.follow(type));
else if(type.id()==ID_unsignedbv ||
type.id()==ID_signedbv)
return true;

2
src/ansi-c/c_typecheck_base.cpp
View File

@ -415,8 +415,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
to_array_type(final_new).size().is_not_nil() &&
final_old.subtype()==final_new.subtype())
{
// we don't do symbol types for arrays anymore
PRECONDITION(old_symbol.type.id() != ID_symbol_type);
old_symbol.type=new_symbol.type;
}
else if(

1
src/ansi-c/c_typecheck_initializer.cpp
View File

@ -504,7 +504,6 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
const typet &type=designator.back().subtype;
const typet &full_type=follow(type);
CHECK_RETURN(full_type.id() != ID_symbol_type);
// do we initialize a scalar?
if(full_type.id()!=ID_struct &&

37
src/ansi-c/expr2c.cpp
View File

@ -440,43 +440,6 @@ std::string expr2ct::convert_rec(
{
return convert_array_type(src, qualifiers, declarator);
}
else if(src.id() == ID_symbol_type)
{
symbol_typet symbolic_type=to_symbol_type(src);
const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
// Providing we have a valid identifer, we can just use that rather than
// trying to find the concrete type
if(typedef_identifer!="")
{
return q+id2string(typedef_identifer)+d;
}
else
{
const typet &followed=ns.follow(src);
if(followed.id()==ID_struct)
{
std::string dest=q+"struct";
const irep_idt &tag=to_struct_type(followed).get_tag();
if(tag!="")
dest+=" "+id2string(tag);
dest+=d;
return dest;
}
else if(followed.id()==ID_union)
{
std::string dest=q+"union";
const irep_idt &tag=to_union_type(followed).get_tag();
if(tag!="")
dest+=" "+id2string(tag);
dest+=d;
return dest;
}
else
return convert_rec(followed, new_qualifiers, declarator);
}
}
else if(src.id()==ID_struct_tag)
{
const struct_tag_typet &struct_tag_type=

1
src/cpp/cpp_typecheck_compound_type.cpp
View File

@ -894,7 +894,6 @@ void cpp_typecheckt::typecheck_friend_declaration(
// TODO
// typecheck_type(ftype);
// assert(ftype.id()==ID_symbol_type);
// symbol.type.add("ID_C_friends").move_to_sub(ftype);
return;

15
src/cpp/cpp_typecheck_constructor.cpp
View File

@ -442,8 +442,8 @@ void cpp_typecheckt::check_member_initializers(
for(const auto &b : bases)
{
if(
to_symbol_type(member_type).get_identifier() ==
to_symbol_type(b.type()).get_identifier())
to_struct_tag_type(member_type).get_identifier() ==
to_struct_tag_type(b.type()).get_identifier())
{
ok=true;
break;
@ -483,14 +483,15 @@ void cpp_typecheckt::check_member_initializers(
if(c.type().id() != ID_struct_tag)
continue;
const symbolt &symb = lookup(to_symbol_type(c.type()).get_identifier());
const symbolt &symb =
lookup(to_struct_tag_type(c.type()).get_identifier());
if(symb.type.id()!=ID_struct)
break;
// check for a direct parent
for(const auto &b : bases)
{
if(symb.name == to_symbol_type(b.type()).get_identifier())
if(symb.name == to_struct_tag_type(b.type()).get_identifier())
{
ok=true;
break;
@ -513,7 +514,7 @@ void cpp_typecheckt::check_member_initializers(
{
if(
member_type.get(ID_identifier) ==
to_symbol_type(b.type()).get_identifier())
to_struct_tag_type(b.type()).get_identifier())
{
ok=true;
break;
@ -638,8 +639,8 @@ void cpp_typecheckt::full_member_initialization(
break;
if(
to_symbol_type(b.type()).get_identifier() ==
to_symbol_type(member_type).get_identifier())
to_struct_tag_type(b.type()).get_identifier() ==
to_struct_tag_type(member_type).get_identifier())
{
final_initializers.move_to_sub(initializer);
found=true;

2
src/cpp/cpp_typecheck_template.cpp
View File

@ -808,7 +808,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
if(cpp_declarator_converter.is_typedef)
{
parameter = exprt(ID_type, symbol_typet(symbol.name));
parameter = exprt(ID_type, struct_tag_typet(symbol.name));
parameter.type().add_source_location()=declaration.find_location();
}
else

62
src/goto-instrument/dump_c.cpp
View File

@ -61,10 +61,10 @@ void dump_ct::operator()(std::ostream &os)
{
typet &type=it2->type();
if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union))
if(type.id() == ID_union_tag && type.get_bool(ID_C_transparent_union))
{
symbolt new_type_sym=
ns.lookup(to_symbol_type(type).get_identifier());
symbolt new_type_sym =
ns.lookup(to_union_tag_type(type).get_identifier());
new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
new_type_sym.type.set(ID_C_transparent_union, true);
@ -72,7 +72,7 @@ void dump_ct::operator()(std::ostream &os)
// we might have it already, in which case this has no effect
symbols_transparent.add(new_type_sym);
to_symbol_type(type).set_identifier(new_type_sym.name);
to_union_tag_type(type).set_identifier(new_type_sym.name);
type.remove(ID_C_transparent_union);
}
}
@ -181,9 +181,16 @@ void dump_ct::operator()(std::ostream &os)
if(type_id==ID_c_enum)
convert_compound_enum(symbol.type, global_decl_stream);
else
global_decl_stream << type_to_string(symbol_typet(symbol.name))
else if(type_id == ID_struct)
{
global_decl_stream << type_to_string(struct_tag_typet{symbol.name})
<< ";\n\n";
}
else
{
global_decl_stream << type_to_string(union_tag_typet{symbol.name})
<< ";\n\n";
}
}
}
else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
@ -297,10 +304,12 @@ void dump_ct::convert_compound_declaration(
return;
// do compound type body
if(symbol.type.id()==ID_struct ||
symbol.type.id()==ID_union ||
symbol.type.id()==ID_c_enum)
convert_compound(symbol.type, symbol_typet(symbol.name), true, os_body);
if(symbol.type.id() == ID_struct)
convert_compound(symbol.type, struct_tag_typet(symbol.name), true, os_body);
else if(symbol.type.id() == ID_union)
convert_compound(symbol.type, union_tag_typet(symbol.name), true, os_body);
else if(symbol.type.id() == ID_c_enum)
convert_compound(symbol.type, c_enum_tag_typet(symbol.name), true, os_body);
}
void dump_ct::convert_compound(
@ -309,16 +318,7 @@ void dump_ct::convert_compound(
bool recursive,
std::ostream &os)
{
if(type.id() == ID_symbol_type)
{
const symbolt &symbol=
ns.lookup(to_symbol_type(type).get_identifier());
DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
convert_compound(symbol.type, unresolved, recursive, os);
}
else if(
if(
type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
type.id() == ID_union_tag)
{
@ -346,7 +346,13 @@ void dump_ct::convert_compound(
it!=syms.end();
++it)
{
symbol_typet s_type(*it);
const symbolt &type_symbol = ns.lookup(*it);
irep_idt tag_kind =
type_symbol.type.id() == ID_c_enum
? ID_c_enum_tag
: (type_symbol.type.id() == ID_union ? ID_union_tag
: ID_struct_tag);
tag_typet s_type(tag_kind, *it);
convert_compound(s_type, s_type, recursive, os);
}
}
@ -378,7 +384,7 @@ void dump_ct::convert_compound(
UNREACHABLE;
/*
assert(parent_it->id() == ID_base);
assert(parent_it->get(ID_type) == ID_symbol_type);
assert(parent_it->get(ID_type) == ID_struct_tag);
const irep_idt &base_id=
parent_it->find(ID_type).get(ID_identifier);
@ -657,12 +663,6 @@ void dump_ct::collect_typedefs_rec(
{
collect_typedefs_rec(type.subtype(), early, local_deps);
}
else if(type.id() == ID_symbol_type)
{
const symbolt &symbol=
ns.lookup(to_symbol_type(type).get_identifier());
collect_typedefs_rec(symbol.type, early, local_deps);
}
else if(
type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
type.id() == ID_union_tag)
@ -1183,7 +1183,11 @@ void dump_ct::insert_local_type_decls(
// a comment block ...
std::ostringstream os_body;
os_body << *it << " */\n";
convert_compound(type, symbol_typet(*it), false, os_body);
irep_idt tag_kind =
type.id() == ID_c_enum
? ID_c_enum_tag
: (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
os_body << "/*";
code_skipt skip;

38
src/goto-instrument/goto_program2code.cpp
View File

@ -1410,31 +1410,22 @@ goto_programt::const_targett goto_program2codet::convert_catch(
void goto_program2codet::add_local_types(const typet &type)
{
if(type.id() == ID_symbol_type)
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const typet &full_type=ns.follow(type);
if(full_type.id()==ID_pointer ||
full_type.id()==ID_array)
{
add_local_types(full_type.subtype());
}
else if(full_type.id()==ID_struct ||
full_type.id()==ID_union)
{
const irep_idt &identifier=to_symbol_type(type).get_identifier();
const symbolt &symbol=ns.lookup(identifier);
const irep_idt &identifier = to_tag_type(type).get_identifier();
const symbolt &symbol = ns.lookup(identifier);
if(symbol.location.get_function().empty() ||
!type_names_set.insert(identifier).second)
return;
if(
symbol.location.get_function().empty() ||
!type_names_set.insert(identifier).second)
return;
for(const auto &c : to_struct_union_type(full_type).components())
add_local_types(c.type());
for(const auto &c : to_struct_union_type(full_type).components())
add_local_types(c.type());
assert(!identifier.empty());
type_names.push_back(identifier);
}
type_names.push_back(identifier);
}
else if(type.id()==ID_c_enum_tag)
{
@ -1633,9 +1624,9 @@ void goto_program2codet::remove_const(typet &type)
if(type.get_bool(ID_C_constant))
type.remove(ID_C_constant);
if(type.id() == ID_symbol_type)
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const irep_idt &identifier=to_symbol_type(type).get_identifier();
const irep_idt &identifier = to_tag_type(type).get_identifier();
if(!const_removed.insert(identifier).second)
return;
@ -1833,8 +1824,9 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
if(no_typecast)
return;
DATA_INVARIANT(expr.type().id() == ID_symbol_type,
"type of union/struct expressions");
DATA_INVARIANT(
expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag,
"union/struct expressions should have a tag type");
const typet &t=expr.type();

16
src/goto-instrument/nondet_volatile.cpp
View File

@ -16,19 +16,16 @@ Date: September 2011
#include <util/std_expr.h>
#include <util/symbol_table.h>
bool is_volatile(
const symbol_tablet &symbol_table,
const typet &src)
static bool is_volatile(const namespacet &ns, const typet &src)
{
if(src.get_bool(ID_C_volatile))
return true;
if(src.id()==ID_symbol)
if(
src.id() == ID_struct_tag || src.id() == ID_union_tag ||
src.id() == ID_c_enum_tag)
{
symbol_tablet::symbolst::const_iterator s_it=
symbol_table.symbols.find(to_symbol_type(src).get_identifier());
assert(s_it!=symbol_table.symbols.end());
return is_volatile(symbol_table, s_it->second.type);
return is_volatile(ns, ns.follow(src));
}
return false;
@ -42,7 +39,8 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
if(expr.id()==ID_symbol ||
expr.id()==ID_dereference)
{
if(is_volatile(symbol_table, expr.type()))
const namespacet ns(symbol_table);
if(is_volatile(ns, expr.type()))
{
typet t=expr.type();
t.remove(ID_C_volatile);

4
src/goto-programs/destructor.cpp
View File

@ -19,9 +19,9 @@ code_function_callt get_destructor(
const namespacet &ns,
const typet &type)
{
if(type.id() == ID_symbol_type)
if(type.id() == ID_struct_tag)
{
return get_destructor(ns, ns.follow(type));
return get_destructor(ns, ns.follow_tag(to_struct_tag_type(type)));
}
else if(type.id()==ID_struct)
{

4
src/goto-programs/interpreter.cpp
View File

@ -1030,9 +1030,9 @@ mp_integer interpretert::get_size(const typet &type)
}
return subtype_size;
}
else if(type.id() == ID_symbol_type || type.id() == ID_struct_tag)
else if(type.id() == ID_struct_tag)
{
return get_size(ns.follow(type));
return get_size(ns.follow_tag(to_struct_tag_type(type)));
}
return 1;

3
src/goto-programs/json_expr.cpp
View File

@ -97,9 +97,6 @@ static exprt simplify_json_expr(const exprt &src)
/// \return a json object
json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
{
if(type.id() == ID_symbol_type)
return json(ns.follow(type), ns, mode);
json_objectt result;
if(type.id() == ID_unsignedbv)

3
src/goto-programs/xml_expr.cpp
View File

@ -25,9 +25,6 @@ Author: Daniel Kroening
xmlt xml(const typet &type, const namespacet &ns)
{
if(type.id() == ID_symbol_type)
return xml(ns.follow(type), ns);
xmlt result;
if(type.id() == ID_unsignedbv)

6
src/goto-symex/goto_symex_state.cpp
View File

@ -595,7 +595,6 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
// type might not have been renamed in case of nesting of
// structs and pointers/arrays
if(
member_expr.struct_op().type().id() != ID_symbol_type &&
member_expr.struct_op().type().id() != ID_struct_tag &&
member_expr.struct_op().type().id() != ID_union_tag)
{
@ -656,11 +655,6 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
{
return requires_renaming(to_pointer_type(type).subtype(), ns);
}
else if(type.id() == ID_symbol_type)
{
const symbolt &symbol = ns.lookup(to_symbol_type(type));
return requires_renaming(symbol.type, ns);
}
else if(type.id() == ID_union_tag)
{
const symbolt &symbol = ns.lookup(to_union_tag_type(type));

16
src/linking/linking.cpp
View File

@ -58,9 +58,7 @@ static const typet &follow_tags_symbols(
const namespacet &ns,
const typet &type)
{
if(type.id() == ID_symbol_type)
return ns.follow(type);
else if(type.id()==ID_c_enum_tag)
if(type.id() == ID_c_enum_tag)
return ns.follow_tag(to_c_enum_tag_type(type));
else if(type.id()==ID_struct_tag)
return ns.follow_tag(to_struct_tag_type(type));
@ -796,10 +794,10 @@ bool linkingt::adjust_object_type_rec(
return false;
if(
t1.id() == ID_symbol_type || t1.id() == ID_struct_tag ||
t1.id() == ID_union_tag || t1.id() == ID_c_enum_tag)
t1.id() == ID_struct_tag || t1.id() == ID_union_tag ||
t1.id() == ID_c_enum_tag)
{
const irep_idt &identifier=t1.get(ID_identifier);
const irep_idt &identifier = to_tag_type(t1).get_identifier();
if(info.o_symbols.insert(identifier).second)
{
@ -813,10 +811,10 @@ bool linkingt::adjust_object_type_rec(
return false;
}
else if(
t2.id() == ID_symbol_type || t2.id() == ID_struct_tag ||
t2.id() == ID_union_tag || t2.id() == ID_c_enum_tag)
t2.id() == ID_struct_tag || t2.id() == ID_union_tag ||
t2.id() == ID_c_enum_tag)
{
const irep_idt &identifier=t2.get(ID_identifier);
const irep_idt &identifier = to_tag_type(t2).get_identifier();
if(info.n_symbols.insert(identifier).second)
{

2
src/pointer-analysis/value_set_analysis_fi.cpp
View File

@ -190,7 +190,7 @@ bool value_set_analysis_fit::check_type(const typet &type)
}
else if(type.id()==ID_array)
return check_type(type.subtype());
else if(type.id() == ID_symbol_type)
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
return check_type(ns.follow(type));
return false;

2
src/pointer-analysis/value_set_analysis_fivr.cpp
View File

@ -178,7 +178,7 @@ bool value_set_analysis_fivrt::check_type(const typet &type)
}
else if(type.id()==ID_array)
return check_type(type.subtype());
else if(type.id() == ID_symbol_type)
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
return check_type(ns.follow(type));
return false;

2
src/pointer-analysis/value_set_analysis_fivrns.cpp
View File

@ -178,8 +178,6 @@ bool value_set_analysis_fivrnst::check_type(const typet &type)
}
else if(type.id()==ID_array)
return check_type(type.subtype());
else if(type.id() == ID_symbol_type)
return check_type(ns.follow(type));
return false;
}

2
src/solvers/flattening/boolbv_width.cpp
View File

@ -180,8 +180,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
}
else if(type_id==ID_pointer)
entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
else if(type_id == ID_symbol_type)
entry=get_entry(ns.follow(type));
else if(type_id==ID_struct_tag)
entry=get_entry(ns.follow_tag(to_struct_tag_type(type)));
else if(type_id==ID_union_tag)

2
src/solvers/flattening/boolbv_with.cpp
View File

@ -100,8 +100,6 @@ void boolbvt::convert_with(
else if(type.id() == ID_union_tag)
return convert_with(
ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
else if(type.id() == ID_symbol_type)
return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
error().source_location=type.source_location();
error() << "unexpected with type: " << type.id() << eom;

16
src/solvers/smt2/smt2_conv.cpp
View File

@ -3916,9 +3916,6 @@ void smt2_convt::unflatten(
const typet &type,
unsigned nesting)
{
if(type.id() == ID_symbol_type)
return unflatten(where, ns.follow(type));
if(type.id()==ID_bool)
{
if(where==wheret::BEGIN)
@ -4444,8 +4441,6 @@ void smt2_convt::convert_type(const typet &type)
out << "Real";
else if(type.id()==ID_integer)
out << "Int";
else if(type.id() == ID_symbol_type)
convert_type(ns.follow(type));
else if(type.id()==ID_complex)
{
if(use_datatypes)
@ -4657,17 +4652,6 @@ void smt2_convt::find_symbols_rec(
{
find_symbols_rec(type.subtype(), recstack);
}
else if(type.id() == ID_symbol_type)
{
const symbol_typet &st=to_symbol_type(type);
const irep_idt &id=st.get_identifier();
if(recstack.find(id)==recstack.end())
{
recstack.insert(id);
find_symbols_rec(ns.follow(type), recstack);
}
}
else if(type.id() == ID_struct_tag)
{
const auto &struct_tag = to_struct_tag_type(type);

12
src/util/README.md
View File

@ -104,10 +104,10 @@ stored in two [sub](\ref irept::dt::sub)s named “subtype” (a single type) an
“subtypes” (a vector of types). For pre-defined types see `std_types.h` and
`mathematical_types.h`.
\subsubsection symbol_typet_section symbol_typet
\subsubsection tag_typet_section tag_typet
\ref symbol_typet is a type used to store a reference to the symbol table. The
full \ref symbolt can be retrieved using the identifier of \ref symbol_typet.
\ref tag_typet is a type used to store a reference to the symbol table. The
full \ref symbolt can be retrieved using the identifier of \ref tag_typet.
\subsection exprt_section exprt
@ -174,7 +174,7 @@ Local variables' symbol values are always ignored;
any initialiser must be explicitly assigned after they are instantiated by a
declaration (\ref code_declt).
Symbol expressions (\ref symbol_exprt) and types (\ref symbol_typet) refer to
Symbol expressions (\ref symbol_exprt) and types (\ref tag_typet) refer to
symbols stored in a symbol table. Symbol expressions can be thought of as
referring to the table for more detail about a symbol (for example, is it a
local or a global variable, or perhaps a function?), and have a type which must
@ -198,8 +198,8 @@ found. Note class \ref multi_namespacet can layer arbitrary numbers of symbol
tables, while for historical reasons \ref namespacet can layer up to two.
The namespace wrapper class also provides the \ref namespacet::follow
operation, which dereferences a `symbol_typet` to retrieve the type it refers
to, including following a symbol_typet which refers to another symbol which
operation, which dereferences a `tag_typet` to retrieve the type it refers
to, including following a type tag which refers to another symbol which
eventually refers to a 'real' type.
\subsubsection symbolt_lifetime Symbol lifetimes

47
src/util/base_type.cpp
View File

@ -53,20 +53,7 @@ protected:
void base_type_rec(
typet &type, const namespacet &ns, std::set<irep_idt> &symb)
{
if(type.id() == ID_symbol_type)
{
const symbolt *symbol;
if(
!ns.lookup(to_symbol_type(type).get_identifier(), symbol) &&
symbol->is_type && !symbol->type.is_nil())
{
type = symbol->type;
base_type_rec(type, ns, symb); // recursive call
return;
}
}
else if(
if(
type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
type.id() == ID_union_tag)
{
@ -99,20 +86,7 @@ void base_type_rec(
typet &subtype=to_pointer_type(type).subtype();
// we need to avoid running into an infinite loop
if(subtype.id() == ID_symbol_type)
{
const irep_idt &id = to_symbol_type(subtype).get_identifier();
if(symb.find(id) != symb.end())
return;
symb.insert(id);
base_type_rec(subtype, ns, symb);
symb.erase(id);
}
else if(
if(
subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
subtype.id() == ID_union_tag)
{
@ -160,8 +134,8 @@ bool base_type_eqt::base_type_eq_rec(
// loop avoidance
if(
(type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
type1.id() == ID_struct_tag || type1.id() == ID_union_tag) &&
(type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
type1.id() == ID_union_tag) &&
type2.id() == type1.id())
{
// already in same set?
@ -172,8 +146,8 @@ bool base_type_eqt::base_type_eq_rec(
}
if(
type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
type1.id() == ID_struct_tag || type1.id() == ID_union_tag)
type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
type1.id() == ID_union_tag)
{
const symbolt &symbol=
ns.lookup(type1.get(ID_identifier));
@ -185,8 +159,8 @@ bool base_type_eqt::base_type_eq_rec(
}
if(
type2.id() == ID_symbol_type || type2.id() == ID_c_enum_tag ||
type2.id() == ID_struct_tag || type2.id() == ID_union_tag)
type2.id() == ID_c_enum_tag || type2.id() == ID_struct_tag ||
type2.id() == ID_union_tag)
{
const symbolt &symbol=
ns.lookup(type2.get(ID_identifier));
@ -309,9 +283,8 @@ bool base_type_eqt::base_type_eq_rec(
/// Check types for equality across all levels of hierarchy. For equality
/// in the top level of the hierarchy only use \ref type_eq.
/// Example:
/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal,
/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a")
/// .type}` will also compare equal.
/// - `struct_typet {union_tag_typet("a")}` and `struct_typet {ns.lookup("a")
/// .type}` will compare equal.
/// \param type1: The first type to compare.
/// \param type2: The second type to compare.
/// \param ns: The namespace, needed for resolution of symbols.

4
src/util/endianness_map.cpp
View File

@ -51,9 +51,7 @@ void endianness_mapt::build_little_endian(const typet &src)
void endianness_mapt::build_big_endian(const typet &src)
{
if(src.id() == ID_symbol_type)
build_big_endian(ns.follow(src));
else if(src.id()==ID_c_enum_tag)
if(src.id() == ID_c_enum_tag)
build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
else if(src.id()==ID_unsignedbv ||
src.id()==ID_signedbv ||

13
src/util/expr_initializer.cpp
View File

@ -261,19 +261,6 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
return std::move(value);
}
}
else if(type_id == ID_symbol_type)
{
auto result = expr_initializer_rec(ns.follow(type), source_location);
if(!result.has_value())
return {};
// we might have mangled the type for arrays, so keep that
if(type.id() != ID_array)
result->type() = type;
return *result;
}
else if(type_id==ID_c_enum_tag)
{
auto result = expr_initializer_rec(

2
src/util/find_symbols.cpp
View File

@ -156,8 +156,6 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
// dest.insert(identifier);
}
}
else if(src.id() == ID_symbol_type)
dest.insert(to_symbol_type(src).get_identifier());
else if(src.id()==ID_array)
{
// do the size -- the subtype is already done

2
src/util/format_type.cpp
View File

@ -79,8 +79,6 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
return os << "struct " << to_struct_tag_type(type).get_identifier();
else if(id == ID_c_enum_tag)
return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
else if(id == ID_symbol_type)
return os << "symbol_type " << to_symbol_type(type).get_identifier();
else if(id == ID_signedbv)
return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
else if(id == ID_unsignedbv)

1
src/util/irep_ids.def
View File

@ -57,7 +57,6 @@ IREP_ID_ONE(bitxnor)
IREP_ID_ONE(notequal)
IREP_ID_ONE(if)
IREP_ID_ONE(symbol)
IREP_ID_ONE(symbol_type)
IREP_ID_ONE(next_symbol)
IREP_ID_ONE(nondet_symbol)
IREP_ID_ONE(predicate_symbol)

27
src/util/namespace.cpp
View File

@ -34,17 +34,6 @@ const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
return lookup(expr.get_identifier());
}
/// Generic lookup function for a symbol type in a symbol table.
/// \param type: The symbol type to lookup.
/// \return The symbol found in the namespace.
/// \remarks The lookup function called assumes that the type symbol we are
/// looking for exists in the symbol table. If it doesn't, it hits an
/// INVARIANT.
const symbolt &namespace_baset::lookup(const symbol_typet &type) const
{
return lookup(type.get_identifier());
}
/// Generic lookup function for a tag type in a symbol table.
/// \param type: The tag type to lookup.
/// \return The symbol found in the namespace.
@ -67,21 +56,7 @@ const typet &namespace_baset::follow(const typet &src) const
if(src.id() == ID_struct_tag)
return follow_tag(to_struct_tag_type(src));
if(src.id() != ID_symbol_type)
return src;
const symbolt *symbol = &lookup(to_symbol_type(src));
// let's hope it's not cyclic...
while(true)
{
DATA_INVARIANT(symbol->is_type, "symbol type points to type");
if(symbol->type.id() == ID_symbol_type)
symbol = &lookup(to_symbol_type(symbol->type));
else
return symbol->type;
}
return src;
}
/// Follow type tag of union type.

2
src/util/namespace.h
View File

@ -18,7 +18,6 @@ class exprt;
class symbolt;
class typet;
class symbol_exprt;
class symbol_typet;
class tag_typet;
class union_typet;
class struct_typet;
@ -55,7 +54,6 @@ public:
}
const symbolt &lookup(const symbol_exprt &) const;
const symbolt &lookup(const symbol_typet &) const;
const symbolt &lookup(const tag_typet &) const;
virtual ~namespace_baset();

8
src/util/pointer_offset_size.cpp
View File

@ -203,10 +203,6 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
return mp_integer(to_bitvector_type(type).get_width());
}
else if(type.id() == ID_symbol_type)
{
return pointer_offset_bits(ns.follow(type), ns);
}
else if(type.id() == ID_union_tag)
{
return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
@ -503,10 +499,6 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
bytes++;
return from_integer(bytes, size_type());
}
else if(type.id() == ID_symbol_type)
{
return size_of_expr(ns.follow(type), ns);
}
else if(type.id() == ID_union_tag)
{
return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);

16
src/util/rename_symbol.cpp
View File

@ -161,17 +161,6 @@ bool rename_symbolt::rename(typet &dest) const
}
}
}
else if(dest.id() == ID_symbol_type)
{
type_mapt::const_iterator it=
type_map.find(to_symbol_type(dest).get_identifier());
if(it!=type_map.end())
{
to_symbol_type(dest).set_identifier(it->second);
result=false;
}
}
else if(dest.id()==ID_c_enum_tag ||
dest.id()==ID_struct_tag ||
dest.id()==ID_union_tag)
@ -233,11 +222,6 @@ bool rename_symbolt::have_to_rename(const typet &dest) const
return true;
}
}
else if(dest.id() == ID_symbol_type)
{
const irep_idt &identifier = to_symbol_type(dest).get_identifier();
return type_map.find(identifier) != type_map.end();
}
else if(dest.id()==ID_c_enum_tag ||
dest.id()==ID_struct_tag ||
dest.id()==ID_union_tag)

4
src/util/std_types.cpp
View File

@ -262,9 +262,7 @@ bool is_constant_or_has_constant_components(
// we have to use the namespace to resolve to its definition:
// struct t { const int a; };
// struct t t1;
if(type.id() == ID_symbol_type ||
type.id() == ID_struct_tag ||
type.id() == ID_union_tag)
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const auto &resolved_type = ns.follow(type);
return has_constant_components(resolved_type);

50
src/util/std_types.h
View File

@ -54,56 +54,6 @@ public:
}
};
/// A reference into the symbol table
class symbol_typet:public typet
{
public:
explicit symbol_typet(const irep_idt &identifier) : typet(ID_symbol_type)
{
set_identifier(identifier);
}
void set_identifier(const irep_idt &identifier)
{
set(ID_identifier, identifier);
}
const irep_idt &get_identifier() const
{
return get(ID_identifier);
}
};
/// Check whether a reference to a typet is a \ref symbol_typet.
/// \param type: Source type.
/// \return True if \p type is a \ref symbol_typet.
template <>
inline bool can_cast_type<symbol_typet>(const typet &type)
{
return type.id() == ID_symbol_type;
}
/// \brief Cast a typet to a \ref symbol_typet.
///
/// This is an unchecked conversion. \a type must be known to be
/// \ref symbol_typet. Will fail with a precondition violation if type
/// doesn't match.
///
/// \param type: Source type.
/// \return Object of type \ref symbol_typet.
inline const symbol_typet &to_symbol_type(const typet &type)
{
PRECONDITION(can_cast_type<symbol_typet>(type));
return static_cast<const symbol_typet &>(type);
}
/// \copydoc to_symbol_type(const typet &)
inline symbol_typet &to_symbol_type(typet &type)
{
PRECONDITION(can_cast_type<symbol_typet>(type));
return static_cast<symbol_typet &>(type);
}
/// Base type for structs and unions
///
/// For example C structs, C unions, C++ classes, Java classes.

14
src/util/type_eq.cpp
View File

@ -33,19 +33,5 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
if(type1==type2)
return true;
if(const auto symbol_type1 = type_try_dynamic_cast<symbol_typet>(type1))
{
const symbolt &symbol = ns.lookup(*symbol_type1);
CHECK_RETURN(symbol.is_type);
return type_eq(symbol.type, type2, ns);
}
if(const auto symbol_type2 = type_try_dynamic_cast<symbol_typet>(type2))
{
const symbolt &symbol = ns.lookup(*symbol_type2);
CHECK_RETURN(symbol.is_type);
return type_eq(type1, symbol.type, ns);
}
return false;
}