35 const exprt &const_dest(dest);
45 if(dest.
id() == ID_side_effect)
47 if(
auto call = expr_try_dynamic_cast<side_effect_expr_function_callt>(dest))
58 for(
auto &arg : call->arguments())
73 else if(dest.
id() == ID_address_of)
101 const exprt &e = it->second;
105 previous_source_location.is_not_nil(),
106 "front-ends should construct symbol expressions with source locations",
108 if(e.
type().
id() != ID_array && e.
type().
id() != ID_code)
114 static_cast<exprt &
>(s) = e;
122 const exprt &expr)
const
129 const typet &type)
const
138 if(type.
id() == ID_c_enum_tag)
140 else if(type.
id()==ID_struct_tag)
142 else if(type.
id()==ID_union_tag)
150 const typet &type)
const
154 if(followed.
id()==ID_struct || followed.
id()==ID_union)
158 const std::string &tag=followed.
get_string(ID_tag);
164 result +=
" (incomplete)";
172 const typet &subtype = c.type();
177 if(!c.get_base_name().empty())
190 else if(followed.
id()==ID_pointer)
206 exprt &conflict_path)
208 bool conclusive =
false;
222 msg=
"type classes differ";
225 else if(t1.
id()==ID_pointer ||
232 if(conflict_path.
type().
id() == ID_pointer)
243 else if(t1.
id()==ID_pointer)
244 msg=
"pointer types differ";
246 msg=
"array types differ";
248 else if(t1.
id()==ID_struct ||
257 exprt conflict_path_before=conflict_path;
259 if(components1.size()!=components2.size())
261 msg=
"number of members is different (";
268 for(std::size_t i=0; i<components1.size(); ++i)
270 const typet &subtype1=components1[i].type();
271 const typet &subtype2=components2[i].type();
273 if(components1[i].get_name()!=components2[i].get_name())
276 msg+=
id2string(components1[i].get_name())+
'/';
277 msg+=
id2string(components2[i].get_name())+
')';
280 else if(subtype1 != subtype2)
282 typedef std::unordered_set<typet, irep_hash> type_sett;
283 type_sett parent_types;
285 exprt e=conflict_path_before;
286 while(e.
id()==ID_dereference ||
290 parent_types.insert(e.
type());
292 if(e.
id() == ID_dereference)
294 else if(e.
id() == ID_member)
296 else if(e.
id() == ID_index)
302 if(parent_types.find(subtype1) == parent_types.end())
304 conflict_path = conflict_path_before;
305 conflict_path.
type() = t1;
306 conflict_path =
member_exprt(conflict_path, components1[i]);
321 msg =
"type of member " +
id2string(components1[i].get_name()) +
322 " differs (recursive)";
331 else if(t1.
id()==ID_c_enum)
343 msg=
"enum value types are different (";
352 else if(members1.size()!=members2.size())
354 msg=
"number of enum members is different (";
361 for(std::size_t i=0; i<members1.size(); ++i)
370 else if(members1[i].get_value()!=members2[i].get_value())
373 msg+=
id2string(members1[i].get_value())+
'/';
374 msg+=
id2string(members2[i].get_value())+
')';
383 msg+=
"\nenum declarations at\n";
387 else if(t1.
id()==ID_code)
398 if(parameters1.size()!=parameters2.size())
400 msg=
"parameter counts differ (";
405 else if(return_type1 != return_type2)
423 msg=
"return types differ";
427 for(std::size_t i=0; i<parameters1.size(); i++)
429 const typet &subtype1=parameters1[i].type();
430 const typet &subtype2=parameters2[i].type();
432 if(subtype1 != subtype2)
450 msg=
"parameter types differ";
460 msg=
"conflict on POD";
464 if(conclusive && !msg.empty())
470 log.error() <<
"reason for conflict at "
490 const std::string &msg)
495 log.error() << msg <<
" '" << old_symbol.
display_name() <<
"'" <<
'\n';
496 log.error() <<
"old definition in module '" << old_symbol.
module <<
"' "
499 log.error() <<
"new definition in module '" << new_symbol.
module <<
"' "
507 const std::string &msg)
510 log.warning().source_location = new_symbol.
location;
513 log.warning() <<
"old definition in module " << old_symbol.
module <<
" "
516 log.warning() <<
"new definition in module " << new_symbol.
module <<
" "
538 if(src_symbol_table.
symbols.find(new_identifier)!=
539 src_symbol_table.
symbols.end())
542 return new_identifier;
554 return renamingt::RENAME_NEW;
556 return renamingt::RENAME_OLD;
558 return renamingt::NO_RENAMING;
566 if(old_symbol.
type != new_symbol.
type)
573 link_warning(old_symbol, new_symbol,
"implicit function declaration");
585 "ignoring conflicting implicit function declaration");
609 "function declaration conflicts with with weak definition");
623 "ignoring conflicting weak function declaration");
637 "ignoring conflicting function alias declaration");
646 "ignoring conflicting function declarations");
666 "conflicting parameter counts of function declarations");
675 std::string warn_msg;
677 typedef std::deque<std::pair<typet, typet> > conflictst;
678 conflictst conflicts;
682 link_warning(old_symbol, new_symbol,
"conflicting return types");
687 code_typet::parameterst::const_iterator
695 if(o_it->type() != n_it->type())
697 std::make_pair(o_it->type(), n_it->type()));
706 "conflicting parameter counts of function declarations");
721 "conflicting parameter counts of function declarations");
730 while(!conflicts.empty())
737 (t1.
id() == ID_pointer || t2.
id() == ID_pointer) &&
742 warn_msg=
"different pointer types in extern function";
747 else if((t1.
id()==ID_pointer || t2.
id()==ID_pointer) &&
753 warn_msg=
"pointer parameter types differ between "
754 "declaration and definition";
762 else if((t1.
id()==ID_union &&
763 (t1.
get_bool(ID_C_transparent_union) ||
764 conflicts.front().first.get_bool(ID_C_transparent_union))) ||
765 (t2.
id()==ID_union &&
766 (t2.
get_bool(ID_C_transparent_union) ||
767 conflicts.front().second.get_bool(ID_C_transparent_union))))
771 (t1.
get_bool(ID_C_transparent_union) ||
772 conflicts.front().first.get_bool(ID_C_transparent_union)) &&
777 const typet &src_type=t1.
id()==ID_union?t2:t1;
781 if(c.type() == src_type)
785 warn_msg=
"conflict on transparent union parameter in function";
799 warn_msg=
"non-pointer parameter types differ between "
800 "declaration and definition";
806 conflicts.pop_front();
809 if(!conflicts.empty())
814 conflicts.front().first,
815 conflicts.front().second);
820 "conflicting function declarations");
864 else if(old_symbol.
type == new_symbol.
type)
869 log.debug() <<
"function '" << old_symbol.
name <<
"' in module '"
871 <<
"' is shadowed by a definition in module '"
878 "duplicate definition of function");
891 t1.
id() == ID_struct_tag || t1.
id() == ID_union_tag ||
892 t1.
id() == ID_c_enum_tag)
896 if(info.
o_symbols.insert(identifier).second)
908 t2.
id() == ID_struct_tag || t2.
id() == ID_union_tag ||
909 t2.
id() == ID_c_enum_tag)
913 if(info.
n_symbols.insert(identifier).second)
924 else if(t1.
id()==ID_pointer && t2.
id()==ID_array)
930 else if(t1.
id()==ID_array && t2.
id()==ID_pointer)
965 else if(t1.
id()!=t2.
id())
971 if(t1.
id()==ID_pointer)
980 "conflicting pointer types for variable");
987 "conflicting pointer types for variable");
998 t1.
id() == ID_array &&
1012 else if(new_size.
is_nil() ||
1020 if(new_size.
type() != old_size.
type())
1025 "conflicting array sizes for variable");
1038 "conflicting array sizes for variable");
1047 else if(t1.
id()==ID_struct || t1.
id()==ID_union)
1055 struct_union_typet::componentst::const_iterator
1056 it1=components1.begin(), it2=components2.begin();
1058 it1!=components1.end() && it2!=components2.end();
1061 if(it1->get_name()!=it2->get_name() ||
1065 if(it1!=components1.end() || it2!=components2.end())
1094 bool set_to_new =
false;
1096 if(old_symbol.
type != new_symbol.
type)
1107 if(old_type.
id()==ID_struct ||
1108 old_type.
id()==ID_union ||
1109 old_type.
id()==ID_array ||
1110 old_type.
id()==ID_c_enum)
1120 "conflicting types for variable");
1147 tmp_new=new_symbol.
value;
1152 if(tmp_old == tmp_new)
1159 log.warning().source_location = new_symbol.
location;
1161 log.warning() <<
"conflicting initializers for"
1162 <<
" variable '" << old_symbol.
name <<
"'\n";
1163 log.warning() <<
"using old value in module " << old_symbol.
module
1166 log.warning() <<
"ignoring new value in module " << new_symbol.
module
1190 old_symbol.
type != new_symbol.
type))
1192 link_error(old_symbol, new_symbol,
"conflict on code contract");
1197 bool is_code_old_symbol=old_symbol.
type.
id()==ID_code;
1198 bool is_code_new_symbol=new_symbol.
type.
id()==ID_code;
1200 if(is_code_old_symbol!=is_code_new_symbol)
1205 "conflicting definition for symbol");
1211 if(is_code_old_symbol)
1236 "conflicting definition for symbol");
1242 if(old_symbol.
type==new_symbol.
type)
1246 old_symbol.
type.
id() == ID_struct &&
1248 new_symbol.
type.
id() == ID_struct &&
1257 old_symbol.
type.
id() == ID_struct &&
1259 new_symbol.
type.
id() == ID_struct &&
1267 old_symbol.
type.
id() == ID_union &&
1269 new_symbol.
type.
id() == ID_union &&
1278 old_symbol.
type.
id() == ID_union &&
1280 new_symbol.
type.
id() == ID_union &&
1288 old_symbol.
type.
id() == ID_array && new_symbol.
type.
id() == ID_array &&
1317 "unexpected difference between type symbols");
1327 return renamingt::RENAME_NEW;
1329 if(old_symbol.
type==new_symbol.
type)
1330 return renamingt::NO_RENAMING;
1333 old_symbol.
type.
id() == ID_struct &&
1335 new_symbol.
type.
id() == ID_struct &&
1338 return renamingt::NO_RENAMING;
1342 old_symbol.
type.
id() == ID_struct &&
1344 new_symbol.
type.
id() == ID_struct &&
1347 return renamingt::NO_RENAMING;
1351 old_symbol.
type.
id() == ID_union &&
1353 new_symbol.
type.
id() == ID_union &&
1356 return renamingt::NO_RENAMING;
1360 old_symbol.
type.
id() == ID_union &&
1362 new_symbol.
type.
id() == ID_union &&
1365 return renamingt::NO_RENAMING;
1369 old_symbol.
type.
id() == ID_array && new_symbol.
type.
id() == ID_array &&
1376 return renamingt::NO_RENAMING;
1382 return renamingt::NO_RENAMING;
1386 return renamingt::RENAME_NEW;
1391 std::unordered_set<irep_idt> &needs_to_be_renamed,
1398 std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_by;
1400 for(
const auto &symbol_pair : src_symbol_table.
symbols)
1402 if(symbol_pair.second.is_type)
1408 for(
const auto &symbol_used : symbols_used)
1410 used_by[symbol_used].insert(symbol_pair.first);
1415 std::deque<irep_idt> queue(
1416 needs_to_be_renamed.begin(), needs_to_be_renamed.end());
1418 while(!queue.empty())
1423 const std::unordered_set<irep_idt> &u = used_by[id];
1425 for(
const auto &dep : u)
1426 if(needs_to_be_renamed.insert(dep).second)
1428 queue.push_back(dep);
1431 log.debug() <<
"LINKING: needs to be renamed (dependency): " << dep
1440 const std::unordered_set<irep_idt> &needs_to_be_renamed)
1442 std::unordered_map<irep_idt, irep_idt> new_identifiers;
1445 for(
const irep_idt &
id : needs_to_be_renamed)
1454 new_identifier =
rename(src_symbol_table,
id);
1456 new_identifiers.emplace(
id, new_identifier);
1460 log.debug() <<
"LINKING: renaming " <<
id <<
" to " << new_identifier
1470 return new_identifiers;
1475 const std::unordered_map<irep_idt, irep_idt> &new_identifiers)
1477 std::map<irep_idt, symbolt> src_symbols;
1479 for(
const auto &named_symbol : src_symbol_table.
symbols)
1481 symbolt symbol=named_symbol.second;
1485 auto it = new_identifiers.find(named_symbol.first);
1486 if(it != new_identifiers.end())
1487 symbol.
name = it->second;
1489 src_symbols.emplace(named_symbol.first, std::move(symbol));
1493 std::unordered_set<irep_idt> collisions;
1495 for(
const auto &named_symbol : src_symbols)
1498 if(named_symbol.first!=named_symbol.second.name)
1511 collisions.insert(named_symbol.first);
1516 for(
const irep_idt &collision : collisions)
1519 symbolt &new_symbol=src_symbols.at(collision);
1531 !it->second.is_type && !it->second.is_macro &&
1532 it->second.value.is_not_nil())
1541 const unsigned errors_before =
1550 std::unordered_set<irep_idt> needs_to_be_renamed;
1552 for(
const auto &symbol_pair : src_symbol_table.
symbols)
1554 symbol_table_baset::symbolst::const_iterator m_it =
1562 case renamingt::NO_RENAMING:
1564 case renamingt::RENAME_OLD:
1566 symbolt renamed_symbol = m_it->second;
1567 renamed_symbol.
name =
rename(src_symbol_table, symbol_pair.first);
1568 if(m_it->second.is_type)
1576 case renamingt::RENAME_NEW:
1578 needs_to_be_renamed.insert(symbol_pair.first);
1581 log.debug() <<
"LINKING: needs to be renamed: " << symbol_pair.first
1593 symbolt tmp = symbol_pair.second;
1600 *sym_ptr = std::move(tmp);
1608 auto new_identifiers =
rename_symbols(src_symbol_table, needs_to_be_renamed);
1623 return linking.link(new_symbol_table);
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
std::vector< c_enum_membert > memberst
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
std::vector< parametert > parameterst
const typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() const
A constant literal expression.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
source_locationt & add_source_location()
const source_locationt & source_location() const
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
Unbounded, signed integers (mathematical integers, not bitvectors)
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const std::string & id_string() const
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
std::unordered_map< irep_idt, irep_idt > rename_symbols(const symbol_table_baset &, const std::unordered_set< irep_idt > &needs_to_be_renamed)
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
bool link(const symbol_table_baset &src_symbol_table)
Merges the symbol table src_symbol_table into main_symbol_table, renaming symbols from src_symbol_tab...
renamingt needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
rename_symbolt rename_main_symbol
void copy_symbols(const symbol_table_baset &, const std::unordered_map< irep_idt, irep_idt > &)
irep_idt rename(const symbol_table_baset &, const irep_idt &)
renamingt needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
symbol_table_baset & main_symbol_table
std::string expr_to_string(const irep_idt &identifier, const exprt &expr) const
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
renamingt needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
casting_replace_symbolt object_type_updates
std::string type_to_string(const irep_idt &identifier, const typet &type) const
std::unordered_set< irep_idt > renamed_ids
bool detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
Returns true iff the conflict report on a particular branch of the tree of types was a definitive res...
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
rename_symbolt rename_new_symbol
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
message_handlert & message_handler
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Extract member of struct or union.
const exprt & compound() const
std::size_t get_message_count(unsigned level) const
Class that provides messages with a built-in verbosity 'level'.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
virtual bool replace(exprt &dest) const
std::size_t erase(const irep_idt &id)
bool have_to_replace(const exprt &dest) const
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
std::string as_string() const
bool is_incomplete() const
A struct/union may be incomplete.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
virtual iteratort begin()=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const irep_idt & display_name() const
Return language specific display name if present.
irep_idt module
Name of module the symbol belongs to.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
const irep_idt & get_identifier() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const source_locationt & source_location() const
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables,...
std::unordered_set< irep_idt > find_symbols_sett
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
static void do_type_dependencies(const symbol_table_baset &src_symbol_table, std::unordered_set< irep_idt > &needs_to_be_renamed, message_handlert &message_handler)
static const typet & follow_tags_symbols(const namespacet &ns, const typet &type)
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
bool is_true(const literalt &l)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const symbolt & old_symbol
std::unordered_set< irep_idt > o_symbols
std::unordered_set< irep_idt > n_symbols
const symbolt & new_symbol
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)