Skip to content

Move symex state levels to a new file #3434

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 16 commits into from
Nov 22, 2018
Merged

Move symex state levels to a new file #3434

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
5666c71
Remove unused typedef
romainbrenguier Nov 15, 2018
bbadc52
Remove typedef used only once
romainbrenguier Nov 15, 2018
c6bc894
Use auto for iterator type
romainbrenguier Nov 15, 2018
75355f5
Use ranged-for instead of iterators
romainbrenguier Nov 16, 2018
9362457
Use default for trivial constructors/destructors
romainbrenguier Nov 15, 2018
141c998
Use ranged-for instead of iterator
romainbrenguier Nov 15, 2018
2d12c6b
Use ranged-for instead of iterators
romainbrenguier Nov 15, 2018
b08fad7
Move renaming_level classes to a new file
romainbrenguier Nov 15, 2018
1b2eca6
Remove unused propagation operator
romainbrenguier Nov 15, 2018
91f7830
Remove unused propogationt::valuest variable
romainbrenguier Nov 20, 2018
dd3dcc1
Remove definition of propagationt
romainbrenguier Nov 15, 2018
de3aa2d
Split set_ssa_indices function
romainbrenguier Nov 15, 2018
96332d6
Replace iterator types by auto
romainbrenguier Nov 19, 2018
ada420d
Move restore_from definition to cpp file
romainbrenguier Nov 19, 2018
9d231f7
Document renaming_level struct
romainbrenguier Nov 19, 2018
b265f7f
Rename renaming_levelt to symex_renaming_levelt
romainbrenguier Nov 20, 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
2 changes: 0 additions & 2 deletions src/goto-instrument/accelerate/scratch_program.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,6 @@ bool scratch_programt::check_sat(bool do_slice)
output(ns, "scratch", std::cout);
#endif

goto_symex_statet::propagationt::valuest constants;
Copy link
Contributor

Choose a reason for hiding this comment

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

❓ This doesn't actually seem to be used anywhere, can it be removed?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

👍 good catch


symex.symex_with_state(symex_state, functions, symex_symbol_table);

if(do_slice)
Expand Down
1 change: 1 addition & 0 deletions src/goto-symex/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ SRC = auto_objects.cpp \
path_storage.cpp \
postcondition.cpp \
precondition.cpp \
renaming_level.cpp \
show_program.cpp \
show_vcc.cpp \
slice.cpp \
Expand Down
147 changes: 42 additions & 105 deletions src/goto-symex/goto_symex_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,50 +38,6 @@ goto_symex_statet::goto_symex_statet()

goto_symex_statet::~goto_symex_statet()=default;

void goto_symex_statet::level0t::operator()(
ssa_exprt &ssa_expr,
const namespacet &ns,
unsigned thread_nr)
{
// already renamed?
if(!ssa_expr.get_level_0().empty())
return;

const irep_idt &obj_identifier=ssa_expr.get_object_name();

// guards are not L0-renamed
if(obj_identifier=="goto_symex::\\guard")
return;

const symbolt *s;
const bool found_l0 = !ns.lookup(obj_identifier, s);
INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));

// don't rename shared variables or functions
if(s->type.id()==ID_code ||
s->is_shared())
return;

// rename!
ssa_expr.set_level_0(thread_nr);
}

void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr)
{
// already renamed?
if(!ssa_expr.get_level_1().empty())
return;

const irep_idt l0_name=ssa_expr.get_l1_object_identifier();

current_namest::const_iterator it=current_names.find(l0_name);
if(it==current_names.end())
return;

// rename!
ssa_expr.set_level_1(it->second.second);
}

/// write to a variable
static bool check_renaming(const exprt &expr);

Expand Down Expand Up @@ -255,7 +211,7 @@ void goto_symex_statet::assignment(
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
level2.current_names[l1_identifier]=std::make_pair(lhs, 0);
level2.increase_counter(l1_identifier);
set_ssa_indices(lhs, ns, L2);
set_l2_indices(lhs, ns);

// in case we happen to be multi-threaded, record the memory access
bool is_shared=l2_thread_write_encoding(lhs, ns);
Expand All @@ -271,9 +227,9 @@ void goto_symex_statet::assignment(
// for value propagation -- the RHS is L2

if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
propagation.values[l1_identifier]=rhs;
propagation[l1_identifier] = rhs;
else
propagation.remove(l1_identifier);
propagation.erase(l1_identifier);

{
// update value sets
Expand All @@ -297,58 +253,34 @@ void goto_symex_statet::assignment(
#endif
}

void goto_symex_statet::propagationt::operator()(exprt &expr)
void goto_symex_statet::set_l0_indices(
ssa_exprt &ssa_expr,
const namespacet &ns)
{
if(expr.id()==ID_symbol)
{
valuest::const_iterator it =
values.find(to_symbol_expr(expr).get_identifier());
if(it!=values.end())
expr=it->second;
}
else if(expr.id()==ID_address_of)
{
// ignore
}
else
{
// do this recursively
Forall_operands(it, expr)
operator()(*it);
}
level0(ssa_expr, ns, source.thread_nr);
}

void goto_symex_statet::set_ssa_indices(
void goto_symex_statet::set_l1_indices(
ssa_exprt &ssa_expr,
const namespacet &ns,
levelt level)
const namespacet &ns)
{
switch(level)
{
case L0:
level0(ssa_expr, ns, source.thread_nr);
break;

case L1:
if(!ssa_expr.get_level_2().empty())
return;
if(!ssa_expr.get_level_1().empty())
return;
level0(ssa_expr, ns, source.thread_nr);
level1(ssa_expr);
break;

case L2:
if(!ssa_expr.get_level_2().empty())
return;
level0(ssa_expr, ns, source.thread_nr);
level1(ssa_expr);
ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
break;
if(!ssa_expr.get_level_2().empty())
return;
if(!ssa_expr.get_level_1().empty())
return;
level0(ssa_expr, ns, source.thread_nr);
level1(ssa_expr);
}

default:
UNREACHABLE;
}
void goto_symex_statet::set_l2_indices(
ssa_exprt &ssa_expr,
const namespacet &ns)
{
if(!ssa_expr.get_level_2().empty())
return;
level0(ssa_expr, ns, source.thread_nr);
level1(ssa_expr);
ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
}

void goto_symex_statet::rename(
Expand All @@ -363,15 +295,21 @@ void goto_symex_statet::rename(
{
ssa_exprt &ssa=to_ssa_expr(expr);

if(level==L0 || level==L1)
if(level == L0)
{
set_l0_indices(ssa, ns);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
}
else if(level == L1)
{
set_ssa_indices(ssa, ns, level);
set_l1_indices(ssa, ns);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
}
else if(level==L2)
{
set_ssa_indices(ssa, ns, L1);
set_l1_indices(ssa, ns);
Copy link
Contributor

Choose a reason for hiding this comment

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

💡 "If L2 then use the L1 version" is quite confusing. I see that it was the same before your changes, but if you know the reason, could you explain it 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.

I agree it's a bit confusing and I don't know exactly how it works, but I think the idea is that doing the renaming for one level you should also take care of the lower levels (for level1 we also do level0 and for level2 we do level0 and level1)

Copy link
Collaborator

Choose a reason for hiding this comment

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

We do the L2 renaming below, but first need to make sure the expression has all L1 levels set correctly, in particular in the type.

rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();

Expand All @@ -387,13 +325,12 @@ void goto_symex_statet::rename(
{
// We also consider propagation if we go up to L2.
// L1 identifiers are used for propagation!
propagationt::valuest::const_iterator p_it=
propagation.values.find(ssa.get_identifier());
auto p_it = propagation.find(ssa.get_identifier());

if(p_it!=propagation.values.end())
if(p_it != propagation.end())
expr=p_it->second; // already L2
else
set_ssa_indices(ssa, ns, L2);
set_l2_indices(ssa, ns);
}
}
}
Expand Down Expand Up @@ -519,7 +456,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
cond=or_exprt(no_write.op(), cond);

if_exprt tmp(cond, ssa_l1, ssa_l1);
set_ssa_indices(to_ssa_expr(tmp.true_case()), ns, L2);
set_l2_indices(to_ssa_expr(tmp.true_case()), ns);

if(a_s_read.second.empty())
{
Expand Down Expand Up @@ -551,7 +488,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
source,
symex_targett::assignment_typet::PHI);

set_ssa_indices(ssa_l1, ns, L2);
set_l2_indices(ssa_l1, ns);
expr=ssa_l1;

a_s_read.second.push_back(guard);
Expand All @@ -567,14 +504,14 @@ bool goto_symex_statet::l2_thread_read_encoding(
// No event and no fresh index, but avoid constant propagation
if(!record_events)
{
set_ssa_indices(ssa_l1, ns, L2);
set_l2_indices(ssa_l1, ns);
expr=ssa_l1;
return true;
}

// produce a fresh L2 name
level2.increase_counter(l1_identifier);
set_ssa_indices(ssa_l1, ns, L2);
set_l2_indices(ssa_l1, ns);
expr=ssa_l1;

// and record that
Expand Down Expand Up @@ -636,7 +573,7 @@ void goto_symex_statet::rename_address(
ssa_exprt &ssa=to_ssa_expr(expr);

// only do L1!
set_ssa_indices(ssa, ns, L1);
set_l1_indices(ssa, ns);

rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
Expand Down
Loading