Skip to content

Refactoring usage of forall_symbols macro into c++11 loops and replacement of asserts. #1839

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 4, 2018
Merged

Refactoring usage of forall_symbols macro into c++11 loops and replacement of asserts. #1839

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
a8319a3
Remove unused macro `forall_symbol_module_map`
thomasspriggs Feb 14, 2018
f1670b2
Refactor `forall_symbols` usage into c++11 loop.
thomasspriggs Feb 9, 2018
ecbbc73
Remove unused `forall_symbols` macro.
thomasspriggs Feb 14, 2018
f8c2b09
Replace asserts with new equivalents.
thomasspriggs Feb 14, 2018
357bbe4
Fix formatting in assert replacements.
thomasspriggs Feb 14, 2018
4d33a91
Add missing brackets to multiline if statements.
thomasspriggs Feb 23, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions src/analyses/invariant_propagation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,10 +178,13 @@ void invariant_propagationt::get_globals(
object_listt &dest)
{
// static ones
forall_symbols(it, ns.get_symbol_table().symbols)
if(it->second.is_lvalue &&
it->second.is_static_lifetime)
get_objects(it->second, dest);
for(const auto &symbol_pair : ns.get_symbol_table().symbols)
{
if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
{
get_objects(symbol_pair.second, dest);
}
}
}

bool invariant_propagationt::check_type(const typet &type) const
Expand Down
56 changes: 28 additions & 28 deletions src/goto-instrument/alignment_checks.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,21 +19,21 @@ void print_struct_alignment_problems(
const symbol_tablet &symbol_table,
std::ostream &out)
{
forall_symbols(it, symbol_table.symbols)
if(it->second.is_type && it->second.type.id()==ID_struct)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good riddance to this confusing indentation!

for(const auto &symbol_pair : symbol_table.symbols)
{
if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
{
const struct_typet &str=to_struct_type(it->second.type);
const struct_typet::componentst &components=str.components();
const struct_typet &str = to_struct_type(symbol_pair.second.type);
const struct_typet::componentst &components = str.components();

bool first_time_seen_in_struct=true;
bool first_time_seen_in_struct = true;

for(struct_typet::componentst::const_iterator
it_mem=components.begin();
it_mem!=components.end();
for(struct_typet::componentst::const_iterator it_mem = components.begin();
it_mem != components.end();
it_mem++)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why all these whitespace changes? Makes it harder to see what are actual code changes. If cleaning up the formatting is a good idea, can you do this in a separate commit?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because I ran my updates through clang-format before making each commit. I now realise these should have been kept in separate commits.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@hannes-steffenhagen-diffblue If you add "?w=1" to the end of the URL when viewing a diff on github then it ignores whitespace when making the diff.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add to that a later use of git blame also requires an additional -w. So, yes, there are workarounds, but maybe the pain can be avoided in the first place?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that running clang-format should be done in a separate commit in this instance, as it will make the PR much easier to review. Ignoring whitespace when viewing a diff is still useful in other situations, e.g. when a conditional is introduced which changes the indentation of a large section of code.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Though with that flag you can no longer add comments seemingly

{
mp_integer cumulated_length=0;
bool first_time_seen_from=true;
mp_integer cumulated_length = 0;
bool first_time_seen_from = true;

// if the instruction cannot be aligned to the address,
// try the next one
Expand All @@ -42,40 +42,39 @@ void print_struct_alignment_problems(
// || alignment(it_mem->type())%config.ansi_c.alignment!=0)
continue;

for(struct_typet::componentst::const_iterator
it_next=it_mem;
it_next!=components.end();
for(struct_typet::componentst::const_iterator it_next = it_mem;
it_next != components.end();
it_next++)
{
const typet &it_type=it_next->type();
const typet &it_type = it_next->type();
const namespacet ns(symbol_table);
mp_integer size=pointer_offset_size(it_type, ns);
mp_integer size = pointer_offset_size(it_type, ns);

if(size<0)
throw "type of unknown size:\n"+it_type.pretty();
if(size < 0)
throw "type of unknown size:\n" + it_type.pretty();

cumulated_length+=size;
cumulated_length += size;
// [it_mem;it_next] cannot be covered by an instruction
if(cumulated_length>config.ansi_c.memory_operand_size)
if(cumulated_length > config.ansi_c.memory_operand_size)
{
// if interferences have been found, no need to check with
// starting from an already covered member
if(!first_time_seen_from)
it_mem=it_next-1;
it_mem = it_next - 1;
break;
}

if(it_mem!=it_next && !it_next->get_is_padding())
if(it_mem != it_next && !it_next->get_is_padding())
{
if(first_time_seen_in_struct)
{
first_time_seen_in_struct=false;
first_time_seen_from=false;
first_time_seen_in_struct = false;
first_time_seen_from = false;

out << "\nWARNING: "
<< "declaration of structure "
<< str.find_type(ID_tag).pretty()
<< " at " << it->second.location << '\n';
<< str.find_type(ID_tag).pretty() << " at "
<< symbol_pair.second.location << '\n';
}

out << "members " << it_mem->get_pretty_name() << " and "
Expand All @@ -84,12 +83,12 @@ void print_struct_alignment_problems(
}
}
}
else if(it->second.type.id()==ID_array)
else if(symbol_pair.second.type.id() == ID_array)
{
// is this structure likely to introduce data races?
#if 0
const namespacet ns(symbol_table);
const array_typet array=to_array_type(it->second.type);
const array_typet array=to_array_type(symbol_pair.second.type);
const mp_integer size=
pointer_offset_size(array.subtype(), ns);

Expand All @@ -100,9 +99,10 @@ void print_struct_alignment_problems(
{
out << "\nWARNING: "
<< "declaration of an array at "
<< it->second.location <<
<< symbol_pair.second.location <<
<< "\nmight be concurrently accessed\n";
}
#endif
}
}
}
6 changes: 4 additions & 2 deletions src/goto-instrument/dump_c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,8 +82,10 @@ void dump_ct::operator()(std::ostream &os)
}
}
}
forall_symbols(it, symbols_transparent.symbols)
copied_symbol_table.add(it->second);
for(const auto &symbol_pair : symbols_transparent.symbols)
{
copied_symbol_table.add(symbol_pair.second);
}

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
unique_tagst unique_tags;
Expand Down
22 changes: 12 additions & 10 deletions src/goto-instrument/model_argc_argv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,25 +114,27 @@ bool model_argc_argv(
// locate the body of the newly built start function as well as any
// additional declarations we might need; the body will then be
// converted and inserted into the start function
forall_symbols(it, tmp_symbol_table.symbols)
for(const auto &symbol_pair : tmp_symbol_table.symbols)
{
// add __CPROVER_assume if necessary (it might exist already)
if(it->first==CPROVER_PREFIX "assume" ||
it->first==CPROVER_PREFIX "input")
goto_model.symbol_table.add(it->second);
else if(it->first==goto_model.goto_functions.entry_point())
if(
symbol_pair.first == CPROVER_PREFIX "assume" ||
symbol_pair.first == CPROVER_PREFIX "input")
goto_model.symbol_table.add(symbol_pair.second);
else if(symbol_pair.first == goto_model.goto_functions.entry_point())
{
value=it->second.value;
value = symbol_pair.second.value;

replace_symbolt replace;
replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
replace(value);
}
else if(has_prefix(
id2string(it->first),
id2string(goto_model.goto_functions.entry_point())+"::") &&
goto_model.symbol_table.add(it->second))
else if(
has_prefix(
id2string(symbol_pair.first),
id2string(goto_model.goto_functions.entry_point()) + "::") &&
goto_model.symbol_table.add(symbol_pair.second))
UNREACHABLE;
}
POSTCONDITION(value.is_not_nil());
Expand Down
30 changes: 16 additions & 14 deletions src/goto-programs/class_hierarchy.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,11 @@ Date: April 2016
/// \param symbol_table: The symbol table to analyze
void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
{
forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair : symbol_table.symbols)
{
if(it->second.is_type && it->second.type.id()==ID_struct)
if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
{
const struct_typet &struct_type=
to_struct_type(it->second.type);
const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);

const irept::subt &bases=
struct_type.find(ID_bases).get_sub();
Expand All @@ -40,8 +39,8 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
if(parent.empty())
continue;

class_map[parent].children.push_back(it->first);
class_map[it->first].parents.push_back(parent);
class_map[parent].children.push_back(symbol_pair.first);
class_map[symbol_pair.first].parents.push_back(parent);
}
}
}
Expand All @@ -55,28 +54,31 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
{
// Add nodes for all classes:
forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair : symbol_table.symbols)
{
if(it->second.is_type && it->second.type.id() == ID_struct)
if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
{
node_indext new_node_index = add_node();
nodes_by_name[it->first] = new_node_index;
(*this)[new_node_index].class_identifier = it->first;
nodes_by_name[symbol_pair.first] = new_node_index;
(*this)[new_node_index].class_identifier = symbol_pair.first;
}
}

// Add parent -> child edges:
forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair : symbol_table.symbols)
{
if(it->second.is_type && it->second.type.id() == ID_struct)
if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
{
const class_typet &class_type = to_class_type(it->second.type);
const class_typet &class_type = to_class_type(symbol_pair.second.type);

for(const auto &base : class_type.bases())
{
const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
if(!parent.empty())
add_edge(nodes_by_name.at(parent), nodes_by_name.at(it->first));
{
add_edge(
nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first));
}
}
}
}
Expand Down
30 changes: 16 additions & 14 deletions src/goto-programs/goto_convert_functions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,16 +38,16 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
typedef std::list<irep_idt> symbol_listt;
symbol_listt symbol_list;

forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair : symbol_table.symbols)
{
if(!it->second.is_type &&
!it->second.is_macro &&
it->second.type.id()==ID_code &&
(it->second.mode==ID_C ||
it->second.mode==ID_cpp ||
it->second.mode==ID_java ||
it->second.mode=="jsil"))
symbol_list.push_back(it->first);
if(
!symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
symbol_pair.second.type.id() == ID_code &&
(symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
symbol_pair.second.mode == ID_java || symbol_pair.second.mode == "jsil"))
{
symbol_list.push_back(symbol_pair.first);
}
}

for(const auto &id : symbol_list)
Expand All @@ -59,12 +59,14 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)

// this removes the parse tree of the bodies from memory
#if 0
Forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair, symbol_table.symbols)
{
if(!it->second.is_type &&
it->second.type.id()==ID_code &&
it->second.value.is_not_nil())
it->second.value=codet();
if(!symbol_pair.second.is_type &&
symbol_pair.second.type.id()==ID_code &&
symbol_pair.second.value.is_not_nil())
{
symbol_pair.second.value=codet();
}
}
#endif
}
Expand Down
20 changes: 12 additions & 8 deletions src/goto-programs/link_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,13 +110,14 @@ static bool link_functions(
// apply macros
rename_symbolt macro_application;

forall_symbols(it, dest_symbol_table.symbols)
if(it->second.is_macro && !it->second.is_type)
for(const auto &symbol_pair : dest_symbol_table.symbols)
{
if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
{
const symbolt &symbol=it->second;
const symbolt &symbol = symbol_pair.second;

INVARIANT(symbol.value.id()==ID_symbol, "must have symbol");
const irep_idt &id=to_symbol_expr(symbol.value).get_identifier();
INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();

#if 0
if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
Expand All @@ -130,6 +131,7 @@ static bool link_functions(

macro_application.insert_expr(symbol.name, id);
}
}

if(!macro_application.expr_map.empty())
Forall_goto_functions(dest_it, dest_functions)
Expand Down Expand Up @@ -159,9 +161,11 @@ void link_goto_model(
typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
id_sett weak_symbols;

forall_symbols(it, dest.symbol_table.symbols)
if(it->second.is_weak)
weak_symbols.insert(it->first);
for(const auto &symbol_pair : dest.symbol_table.symbols)
{
if(symbol_pair.second.is_weak)
weak_symbols.insert(symbol_pair.first);
}

linkingt linking(dest.symbol_table,
src.symbol_table,
Expand Down
12 changes: 8 additions & 4 deletions src/goto-programs/show_symbol_table.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,10 @@ void show_symbol_table_brief_plain(
// we want to sort alphabetically
std::set<std::string> symbols;

forall_symbols(it, symbol_table.symbols)
symbols.insert(id2string(it->first));
for(const auto &symbol_pair : symbol_table.symbols)
{
symbols.insert(id2string(symbol_pair.first));
}

const namespacet ns(symbol_table);

Expand Down Expand Up @@ -68,8 +70,10 @@ void show_symbol_table_plain(
// we want to sort alphabetically
std::set<std::string> symbols;

forall_symbols(it, symbol_table.symbols)
symbols.insert(id2string(it->first));
for(const auto &symbol_pair : symbol_table.symbols)
{
symbols.insert(id2string(symbol_pair.first));
}

const namespacet ns(symbol_table);

Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/write_goto_binary.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,12 @@ bool write_goto_binary_v3(

write_gb_word(out, symbol_table.symbols.size());

forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair : symbol_table.symbols)
{
// Since version 2, symbols are not converted to ireps,
// instead they are saved in a custom binary format

const symbolt &sym = it->second;
const symbolt &sym = symbol_pair.second;

irepconverter.reference_convert(sym.type, out);
irepconverter.reference_convert(sym.value, out);
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/symex_start_thread.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,9 @@ void goto_symext::symex_start_thread(statet &state)
// initialize all variables marked thread-local
const symbol_tablet &symbol_table=ns.get_symbol_table();

forall_symbols(it, symbol_table.symbols)
for(const auto &symbol_pair : symbol_table.symbols)
{
const symbolt &symbol=it->second;
const symbolt &symbol = symbol_pair.second;

if(!symbol.is_thread_local ||
!symbol.is_static_lifetime ||
Expand Down
Loading