Skip to content

Value-set dereference: use cond_exprt to avoid quadratic guards #4555

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

Closed
wants to merge 12 commits into from
Closed

Value-set dereference: use cond_exprt to avoid quadratic guards #4555

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
93e4622
Add exclusive flag to cond_exprt
smowton Apr 18, 2019
1a553e0
Add accessors to cond_exprt
smowton Apr 18, 2019
e860099
value-set-dereference: return a cond_exprt
smowton Apr 18, 2019
ae870f1
goto-symex: handle cond_exprt on the LHS
smowton Apr 18, 2019
f57ebf2
Use lift-if more consistently
smowton Apr 18, 2019
739e11d
Add lift_cond
smowton Apr 18, 2019
3629f2a
Simplify cond_exprt
smowton Apr 18, 2019
3645437
Add missing case to bv_pointerst
smowton Apr 18, 2019
59145f1
Value-set: handle cond_exprt on the RHS
smowton Apr 18, 2019
b56063b
Lower cond_expr on the RHS
smowton Apr 18, 2019
2fc837c
process_array_expr: handle ID_cond
smowton Apr 18, 2019
2e48edd
Add cases handling cond_exprt wherever symex or value-set currently h…
smowton Apr 19, 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
7 changes: 7 additions & 0 deletions src/goto-symex/goto_symex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -534,6 +534,13 @@ class goto_symext
const exprt &rhs,
exprt::operandst &,
assignment_typet);
void symex_assign_cond(
statet &,
const cond_exprt &lhs,
const exprt &full_lhs,
const exprt &rhs,
exprt::operandst &,
assignment_typet);
void symex_assign_byte_extract(
statet &,
const byte_extract_exprt &lhs,
Expand Down
41 changes: 41 additions & 0 deletions src/goto-symex/symex_assign.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,9 @@ void goto_symext::symex_assign_rec(
else if(lhs.id()==ID_if)
symex_assign_if(
state, to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
else if(lhs.id() == ID_cond)
symex_assign_cond(
state, to_cond_expr(lhs), full_lhs, rhs, guard, assignment_type);
else if(lhs.id()==ID_typecast)
symex_assign_typecast(
state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type);
Expand Down Expand Up @@ -613,6 +616,44 @@ void goto_symext::symex_assign_if(
}
}

void goto_symext::symex_assign_cond(
statet &state,
const cond_exprt &lhs,
const exprt &full_lhs,
const exprt &rhs,
exprt::operandst &guard,
assignment_typet assignment_type)
{
std::size_t old_guard_size = guard.size();

for(std::size_t i = 0; i < lhs.get_n_cases(); ++i)
{
exprt renamed_guard = state.rename(lhs.condition(i), ns).get();
Copy link
Contributor

Choose a reason for hiding this comment

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

💡 It's confusing that the variable names don't distinguish between the incoming guard and the extra bit coming from the current case we're considering. Maybe renamed_case_guard?

do_simplify(renamed_guard);
if(!renamed_guard.is_false())
{
guard.push_back(renamed_guard);
symex_assign_rec(
state, lhs.value(i), full_lhs, rhs, guard, assignment_type);
guard.pop_back();
}

// If this one is a certainty the remaining cases are irrelevant:
if(renamed_guard.is_true())
break;

// If the conditions are non-exclusive, further cases can only happen if
// this one did not. If they are exclusive then they can be tested
// independently.
if(!lhs.is_exclusive())
guard.push_back(not_exprt(renamed_guard));
}

// Restore the guard to its state before entering this function:
INVARIANT(guard.size() >= old_guard_size, "must not shrink the guard!");
Copy link
Collaborator

Choose a reason for hiding this comment

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

s/shrink/grow/?

guard.resize(old_guard_size);
}

void goto_symext::symex_assign_byte_extract(
statet &state,
const byte_extract_exprt &lhs,
Expand Down