Skip to content

Field sensitivity: using apply is now always safe #7259

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 1 commit into from
Nov 3, 2022
Merged

Field sensitivity: using apply is now always safe #7259

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
16 changes: 5 additions & 11 deletions src/goto-symex/field_sensitivity.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ exprt field_sensitivityt::apply(
ssa_exprt ssa_expr,
bool write) const
{
if(!run_apply || write)
if(write)
return std::move(ssa_expr);
else
return get_fields(ns, state, ssa_expr);
Expand All @@ -35,9 +35,6 @@ exprt field_sensitivityt::apply(
exprt expr,
bool write) const
{
if(!run_apply)
return expr;

if(expr.id() != ID_address_of)
{
Forall_operands(it, expr)
Expand All @@ -46,7 +43,7 @@ exprt field_sensitivityt::apply(

if(!write && is_ssa_expr(expr))
{
return apply(ns, state, to_ssa_expr(expr), write);
return get_fields(ns, state, to_ssa_expr(expr));
}
else if(
!write && expr.id() == ID_member &&
Expand Down Expand Up @@ -231,17 +228,14 @@ void field_sensitivityt::field_assignments(
const ssa_exprt &lhs,
const exprt &rhs,
symex_targett &target,
bool allow_pointer_unsoundness)
bool allow_pointer_unsoundness) const
{
const exprt lhs_fs = apply(ns, state, lhs, false);
const exprt lhs_fs = get_fields(ns, state, lhs);

if(lhs != lhs_fs)
{
bool run_apply_bak = run_apply;
run_apply = false;
field_assignments_rec(
ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);
run_apply = run_apply_bak;
}
}

Expand All @@ -261,7 +255,7 @@ void field_sensitivityt::field_assignments_rec(
const exprt &lhs_fs,
const exprt &ssa_rhs,
symex_targett &target,
bool allow_pointer_unsoundness)
bool allow_pointer_unsoundness) const
{
if(is_ssa_expr(lhs_fs))
{
Expand Down
8 changes: 3 additions & 5 deletions src/goto-symex/field_sensitivity.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ class field_sensitivityt
const ssa_exprt &lhs,
const exprt &rhs,
symex_targett &target,
bool allow_pointer_unsoundness);
bool allow_pointer_unsoundness) const;

/// Turn an expression \p expr into a field-sensitive SSA expression.
/// Field-sensitive SSA expressions have individual symbols for each
Expand Down Expand Up @@ -154,12 +154,10 @@ class field_sensitivityt
/// \param expr: the expression to evaluate
/// \return False, if and only if, \p expr would be a single field-sensitive
/// SSA expression.
NODISCARD
bool is_divisible(const ssa_exprt &expr) const;

private:
/// whether or not to invoke \ref field_sensitivityt::apply
bool run_apply = true;

const std::size_t max_field_sensitivity_array_size;

const bool should_simplify;
Expand All @@ -170,7 +168,7 @@ class field_sensitivityt
const exprt &lhs_fs,
const exprt &ssa_rhs,
symex_targett &target,
bool allow_pointer_unsoundness);
bool allow_pointer_unsoundness) const;

exprt simplify_opt(exprt e, const namespacet &ns) const;
};
Expand Down