Skip to content

Split the rename function according to the level and pass expression by copy instead of reference #3996

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
Feb 27, 2019
Merged

Split the rename function according to the level and pass expression by copy instead of reference #3996

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cf26fd0
Extract a rename_level0_ssa function
romainbrenguier Jan 23, 2019
137b635
Make level argument of rename a template argument
romainbrenguier Jan 22, 2019
7553ca7
Extract a rename_level1_ssa function
romainbrenguier Feb 19, 2019
9d18229
Use rename_level1_ssa where possible
romainbrenguier Feb 19, 2019
3726631
Make rename take a copy instead of reference
romainbrenguier Feb 19, 2019
7da918f
Merge the two rename_ssa functions
romainbrenguier Feb 27, 2019
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
6 changes: 1 addition & 5 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 @@ -69,11 +69,7 @@ bool scratch_programt::check_sat(bool do_slice)

exprt scratch_programt::eval(const exprt &e)
{
exprt ssa=e;

symex_state->rename(ssa, ns);

return checker->get(ssa);
return checker->get(symex_state->rename<goto_symex_statet::L2>(e, ns));
}

void scratch_programt::append(goto_programt::instructionst &new_instructions)
Expand Down
105 changes: 55 additions & 50 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 @@ -163,11 +163,11 @@ void goto_symex_statet::assignment(
bool allow_pointer_unsoundness)
{
// identifier should be l0 or l1, make sure it's l1
rename(lhs, ns, L1);
lhs = rename_level1_ssa(std::move(lhs), ns);
irep_idt l1_identifier=lhs.get_identifier();

// the type might need renaming
rename(lhs.type(), l1_identifier, ns);
rename<L2>(lhs.type(), l1_identifier, ns);
lhs.update_type();
if(run_validation_checks)
{
Expand Down Expand Up @@ -263,10 +263,26 @@ void goto_symex_statet::set_l2_indices(
ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
}

void goto_symex_statet::rename(
exprt &expr,
const namespacet &ns,
levelt level)
ssa_exprt
goto_symex_statet::rename_level0_ssa(ssa_exprt ssa, const namespacet &ns)
{
set_l0_indices(ssa, ns);
rename<L0>(ssa.type(), ssa.get_identifier(), ns);
ssa.update_type();
return ssa;
}

ssa_exprt
goto_symex_statet::rename_level1_ssa(ssa_exprt ssa, const namespacet &ns)
{
set_l1_indices(ssa, ns);
rename<L1>(ssa.type(), ssa.get_identifier(), ns);
ssa.update_type();
return ssa;
}

template <goto_symex_statet::levelt level>
exprt goto_symex_statet::rename(exprt expr, const namespacet &ns)
{
// rename all the symbols with their last known value

Expand All @@ -277,20 +293,16 @@ void goto_symex_statet::rename(

if(level == L0)
{
set_l0_indices(ssa, ns);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
ssa = rename_level0_ssa(std::move(ssa), ns);
}
else if(level == L1)
{
set_l1_indices(ssa, ns);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
ssa = rename_level1_ssa(std::move(ssa), ns);
}
else if(level==L2)
{
set_l1_indices(ssa, ns);
rename(expr.type(), ssa.get_identifier(), ns, level);
rename<level>(expr.type(), ssa.get_identifier(), ns);
ssa.update_type();

if(l2_thread_read_encoding(ssa, ns))
Expand Down Expand Up @@ -318,33 +330,24 @@ void goto_symex_statet::rename(
{
// we never rename function symbols
if(as_const(expr).type().id() == ID_code)
{
rename(
expr.type(),
to_symbol_expr(expr).get_identifier(),
ns,
level);

return;
}

expr=ssa_exprt(expr);
rename(expr, ns, level);
rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
else
expr = rename<level>(ssa_exprt(expr), ns);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: you otherwise aim to use {...} in constructor calls, so do ssa_exprt{expr} here as well.

}
else if(expr.id()==ID_address_of)
{
auto &address_of_expr = to_address_of_expr(expr);
rename_address(address_of_expr.object(), ns, level);
rename_address<level>(address_of_expr.object(), ns);
to_pointer_type(expr.type()).subtype() =
as_const(address_of_expr).object().type();
}
else
{
rename(expr.type(), irep_idt(), ns, level);
rename<level>(expr.type(), irep_idt(), ns);

// do this recursively
Forall_operands(it, expr)
rename(*it, ns, level);
*it = rename<level>(std::move(*it), ns);

const exprt &c_expr = as_const(expr);
INVARIANT(
Expand All @@ -356,6 +359,7 @@ void goto_symex_statet::rename(
"Type of renamed expr should be the same as operands for with_exprt and "
"if_exprt");
}
return expr;
}

/// thread encoding
Expand Down Expand Up @@ -535,10 +539,8 @@ bool goto_symex_statet::l2_thread_write_encoding(
return threads.size()>1;
}

void goto_symex_statet::rename_address(
exprt &expr,
const namespacet &ns,
levelt level)
template <goto_symex_statet::levelt level>
void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
{
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
Expand All @@ -548,42 +550,42 @@ void goto_symex_statet::rename_address(
// only do L1!
set_l1_indices(ssa, ns);

rename(expr.type(), ssa.get_identifier(), ns, level);
rename<level>(expr.type(), ssa.get_identifier(), ns);
ssa.update_type();
}
else if(expr.id()==ID_symbol)
{
expr=ssa_exprt(expr);
rename_address(expr, ns, level);
rename_address<level>(expr, ns);
}
else
{
if(expr.id()==ID_index)
{
index_exprt &index_expr=to_index_expr(expr);

rename_address(index_expr.array(), ns, level);
rename_address<level>(index_expr.array(), ns);
PRECONDITION(index_expr.array().type().id() == ID_array);
expr.type() = to_array_type(index_expr.array().type()).subtype();

// the index is not an address
rename(index_expr.index(), ns, level);
index_expr.index() = rename<level>(std::move(index_expr.index()), ns);
}
else if(expr.id()==ID_if)
{
// the condition is not an address
if_exprt &if_expr=to_if_expr(expr);
rename(if_expr.cond(), ns, level);
rename_address(if_expr.true_case(), ns, level);
rename_address(if_expr.false_case(), ns, level);
if_expr.cond() = rename<level>(std::move(if_expr.cond()), ns);
rename_address<level>(if_expr.true_case(), ns);
rename_address<level>(if_expr.false_case(), ns);

if_expr.type()=if_expr.true_case().type();
}
else if(expr.id()==ID_member)
{
member_exprt &member_expr=to_member_expr(expr);

rename_address(member_expr.struct_op(), ns, level);
rename_address<level>(member_expr.struct_op(), ns);

// type might not have been renamed in case of nesting of
// structs and pointers/arrays
Expand All @@ -600,17 +602,17 @@ void goto_symex_statet::rename_address(
expr.type()=comp.type();
}
else
rename(expr.type(), irep_idt(), ns, level);
rename<level>(expr.type(), irep_idt(), ns);
}
else
{
// this could go wrong, but we would have to re-typecheck ...
rename(expr.type(), irep_idt(), ns, level);
rename<level>(expr.type(), irep_idt(), ns);

// do this recursively; we assume here
// that all the operands are addresses
Forall_operands(it, expr)
rename_address(*it, ns, level);
rename_address<level>(*it, ns);
}
}
}
Expand Down Expand Up @@ -668,11 +670,11 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
return false;
}

template <goto_symex_statet::levelt level>
void goto_symex_statet::rename(
typet &type,
const irep_idt &l1_identifier,
const namespacet &ns,
levelt level)
const namespacet &ns)
{
// check whether there are symbol expressions in the type; if not, there
// is no need to expand the struct/union tags in the type
Expand Down Expand Up @@ -711,8 +713,8 @@ void goto_symex_statet::rename(
if(type.id()==ID_array)
{
auto &array_type = to_array_type(type);
rename(array_type.subtype(), irep_idt(), ns, level);
rename(array_type.size(), ns, level);
rename<level>(array_type.subtype(), irep_idt(), ns);
array_type.size() = rename<level>(std::move(array_type.size()), ns);
}
else if(type.id() == ID_struct || type.id() == ID_union)
{
Expand All @@ -723,14 +725,17 @@ void goto_symex_statet::rename(
{
// be careful, or it might get cyclic
if(component.type().id() == ID_array)
rename(to_array_type(component.type()).size(), ns, level);
{
auto &array_type = to_array_type(component.type());
array_type.size() = rename<level>(std::move(array_type.size()), ns);
}
else if(component.type().id() != ID_pointer)
rename(component.type(), irep_idt(), ns, level);
rename<level>(component.type(), irep_idt(), ns);
}
}
else if(type.id()==ID_pointer)
{
rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
}

if(level==L2 &&
Expand Down
18 changes: 11 additions & 7 deletions src/goto-symex/goto_symex_state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,12 +179,15 @@ class goto_symex_statet final : public goto_statet
///
/// A full explanation of SSA (which is why we do this renaming) is in
/// the SSA section of background-concepts.md.
void rename(exprt &expr, const namespacet &ns, levelt level=L2);
void rename(
typet &type,
const irep_idt &l1_identifier,
const namespacet &ns,
levelt level=L2);
template <levelt level = L2>
exprt rename(exprt expr, const namespacet &ns);

ssa_exprt rename_level0_ssa(ssa_exprt ssa, const namespacet &ns);

ssa_exprt rename_level1_ssa(ssa_exprt ssa, const namespacet &ns);

template <levelt level = L2>
void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);

void assignment(
ssa_exprt &lhs, // L0/L1
Expand All @@ -195,7 +198,8 @@ class goto_symex_statet final : public goto_statet
bool allow_pointer_unsoundness=false);

protected:
void rename_address(exprt &expr, const namespacet &ns, levelt level);
template <levelt>
void rename_address(exprt &expr, const namespacet &ns);

/// Update level 0 values.
void set_l0_indices(ssa_exprt &expr, const namespacet &ns);
Expand Down
16 changes: 8 additions & 8 deletions src/goto-symex/symex_assign.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -212,13 +212,13 @@ void goto_symext::symex_assign_symbol(
tmp_ssa_rhs.swap(ssa_rhs);
}

state.rename(ssa_rhs, ns);
do_simplify(ssa_rhs);
exprt l2_rhs = state.rename(std::move(ssa_rhs), ns);
do_simplify(l2_rhs);

ssa_exprt ssa_lhs=lhs;
state.assignment(
ssa_lhs,
ssa_rhs,
l2_rhs,
ns,
symex_config.simplify_opt,
symex_config.constant_propagation,
Expand All @@ -228,7 +228,7 @@ void goto_symext::symex_assign_symbol(
ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
const bool record_events=state.record_events;
state.record_events=false;
state.rename(ssa_full_lhs, ns);
exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns);
state.record_events=record_events;

guardt tmp_guard(state.guard);
Expand All @@ -254,8 +254,9 @@ void goto_symext::symex_assign_symbol(
target.assignment(
tmp_guard.as_expr(),
ssa_lhs,
ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
ssa_rhs,
l2_full_lhs,
add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
l2_rhs,
state.source,
assignment_type);
}
Expand Down Expand Up @@ -406,8 +407,7 @@ void goto_symext::symex_assign_if(

guardt old_guard=guard;

exprt renamed_guard=lhs.cond();
state.rename(renamed_guard, ns);
exprt renamed_guard = state.rename(lhs.cond(), ns);
do_simplify(renamed_guard);

if(!renamed_guard.is_false())
Expand Down
Loading