Move exprt::bounded_size to complexity_limitert #5988
Conversation
tautschnig
requested review from
kroening,
peterschrammel,
romainbrenguier and
smowton
as code owners
There was a problem hiding this comment.
Minor tweaks on text matching new names noted.
Outside of this, there were many experiments with CSE (some info #5964) that used the expression size and these showed that this could be a useful parameter to manipulate. I note this because if we want to have a bounded size for expressions later this would involve a refactor to return this to expr and not be in complexity_limiter.
| #include <goto-symex/complexity_limiter.h> | ||
|
|
||
| TEST_CASE( | ||
| "Bounded size is computed correctly", |
There was a problem hiding this comment.
"Bounded size" -> "Bounded expr[ession] size"
| } | ||
|
|
||
| TEST_CASE( | ||
| "Bounded size versus pathological example", |
There was a problem hiding this comment.
"Bounded size" -> "Bounded expr[ession] size"
| exprt pathology = plus_exprt(from_integer(1, type), from_integer(1, type)); | ||
| // Create an infinite exprt by self reference! | ||
| pathology.add_to_operands(pathology); | ||
| // If bounded size is not checking the bound this will never terminate. |
There was a problem hiding this comment.
"Bounded size" -> "Bounded expr[ession] size"
| { | ||
| return count; | ||
| } | ||
| count = bounded_expr_size(op, count, limit); |
There was a problem hiding this comment.
If we aren't going to fix this, can we at least have a comment saying this is potentially risky?
There was a problem hiding this comment.
Comment now added to the public member function.
tautschnig
force-pushed
the
bounded-size-cleanup
branch
2 times, most recently
from
a1dd075 to
bad8e11
Compare
Thanks a lot for the comments, text changes implemented. As far as re-use is concerned: if it turns out to be useful, then we could certainly consider moving this elsewhere. If we do, however, then IMHO it should be somewhere around |
complexity_limitert is really the only user of this method, and may be fine with its implementation details (cf. discussion in diffblue#5914). For other potential users such assumptions might not be safe.
tautschnig
force-pushed
the
bounded-size-cleanup
branch
from
bad8e11 to
8f61a22
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5988 +/- ##
===========================================
+ Coverage 75.12% 75.13% +0.01%
===========================================
Files 1435 1445 +10
Lines 156301 157261 +960
===========================================
+ Hits 117416 118165 +749
- Misses 38885 39096 +211
Continue to review full report at Codecov.
|
complexity_limitert is really the only user of this method, and may be
fine with its implementation details (cf. discussion in #5914). For
other potential users such assumptions might not be safe.