Skip to content

Commit 461fcd9

Browse files
committed
Overload field_sensitivityt::apply for ssa_exprt
For two of the eight call sites of field_sensitivityt::apply we know at compile time that an ssa_exprt is being passed in. We can thus avoid redundant is-it-an-SSA-expression tests for those cases, and also know that we do not need to look at any operands.
1 parent 2fbbd09 commit 461fcd9

File tree

2 files changed

+20
-2
lines changed

2 files changed

+20
-2
lines changed

src/goto-symex/field_sensitivity.cpp

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,18 @@ Author: Michael Tautschnig
1818

1919
#define ENABLE_ARRAY_FIELD_SENSITIVITY
2020

21+
exprt field_sensitivityt::apply(
22+
const namespacet &ns,
23+
goto_symex_statet &state,
24+
ssa_exprt ssa_expr,
25+
bool write) const
26+
{
27+
if(!run_apply || write)
28+
return std::move(ssa_expr);
29+
else
30+
return get_fields(ns, state, ssa_expr);
31+
}
32+
2133
exprt field_sensitivityt::apply(
2234
const namespacet &ns,
2335
goto_symex_statet &state,
@@ -33,9 +45,9 @@ exprt field_sensitivityt::apply(
3345
*it = apply(ns, state, std::move(*it), write);
3446
}
3547

36-
if(is_ssa_expr(expr) && !write)
48+
if(!write && is_ssa_expr(expr))
3749
{
38-
return get_fields(ns, state, to_ssa_expr(expr));
50+
return apply(ns, state, to_ssa_expr(expr), write);
3951
}
4052
else if(
4153
!write && expr.id() == ID_member &&

src/goto-symex/field_sensitivity.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,12 @@ class field_sensitivityt
119119
exprt
120120
apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
121121
const;
122+
/// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
123+
exprt apply(
124+
const namespacet &ns,
125+
goto_symex_statet &state,
126+
ssa_exprt expr,
127+
bool write) const;
122128

123129
/// Compute an expression representing the individual components of a
124130
/// field-sensitive SSA representation of \p ssa_expr.

0 commit comments

Comments
 (0)