Skip to content

Introduce range class and use it to optimize symex #3454

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 4 commits into from
Nov 26, 2018
Merged

Introduce range class and use it to optimize symex #3454

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b6239d0
Add a class for ranges
romainbrenguier Nov 20, 2018
b0ec79a
Use range in symex instead of merging sets of expressions
romainbrenguier Nov 20, 2018
96b0ff4
Use ranged-for instead of iterators
romainbrenguier Nov 21, 2018
cfb1203
Unit tests for range
romainbrenguier Nov 26, 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
43 changes: 27 additions & 16 deletions src/goto-symex/symex_goto.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/exception_utils.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/range.h>
#include <util/std_expr.h>

#include <analyses/dirty.h>
Expand Down Expand Up @@ -357,29 +358,38 @@ void goto_symext::phi_function(
const statet::goto_statet &goto_state,
statet &dest_state)
{
// go over all variables to see what changed
std::unordered_set<ssa_exprt, irep_hash> variables;
auto ssa_of_current_name =
[&](const std::pair<irep_idt, std::pair<ssa_exprt, unsigned>> &pair) {
Copy link
Contributor

Choose a reason for hiding this comment

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

🌊

return pair.second.first;
};

auto dest_state_names_range =
make_range(dest_state.level2.current_names)
.filter(
[&](const std::pair<irep_idt, std::pair<ssa_exprt, unsigned>> &pair) {
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏ I'd consider const statet::value_type & here. 🌊

Copy link
Contributor Author

Choose a reason for hiding this comment

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

That's actually statet::renaming_levelt::current_namest::value_type so not really better I think

// We ignore the identifiers that are already in goto_state names
return goto_state.level2_current_names.count(pair.first) == 0;
})
.map<const ssa_exprt>(ssa_of_current_name);

goto_state.level2_get_variables(variables);
dest_state.level2.get_variables(variables);
// go over all variables to see what changed
auto all_current_names_range = make_range(goto_state.level2_current_names)
.map<const ssa_exprt>(ssa_of_current_name)
.concat(dest_state_names_range);

guardt diff_guard;

if(!variables.empty())
if(!all_current_names_range.empty())
{
diff_guard=goto_state.guard;

// this gets the diff between the guards
diff_guard-=dest_state.guard;
}

for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator
it=variables.begin();
it!=variables.end();
it++)
for(const auto &ssa : all_current_names_range)
{
const irep_idt l1_identifier=it->get_identifier();
const irep_idt &obj_identifier=it->get_object_name();
const irep_idt l1_identifier = ssa.get_identifier();
const irep_idt &obj_identifier = ssa.get_object_name();

if(obj_identifier==guard_identifier)
continue; // just a guard, don't bother
Expand All @@ -404,11 +414,12 @@ void goto_symext::phi_function(
// may have been introduced by symex_start_thread (and will
// only later be removed from level2.current_names by pop_frame
// once the thread is executed)
if(!it->get_level_0().empty() &&
it->get_level_0()!=std::to_string(dest_state.source.thread_nr))
if(
!ssa.get_level_0().empty() &&
ssa.get_level_0() != std::to_string(dest_state.source.thread_nr))
continue;

exprt goto_state_rhs=*it, dest_state_rhs=*it;
exprt goto_state_rhs = ssa, dest_state_rhs = ssa;

{
const auto p_it = goto_state.propagation.find(l1_identifier);
Expand Down Expand Up @@ -454,7 +465,7 @@ void goto_symext::phi_function(
do_simplify(rhs);
}

ssa_exprt new_lhs=*it;
ssa_exprt new_lhs = ssa;
const bool record_events=dest_state.record_events;
dest_state.record_events=false;
dest_state.assignment(new_lhs, rhs, ns, true, true);
Expand Down
Loading