CONTRACTS: havoc all statics by default #6829
Conversation
remi-delmas-3000
requested review from
chris-ryder,
martin-cs and
peterschrammel
as code owners
remi-delmas-3000
force-pushed
the
contracts-havoc-statics
branch
from
16debbc to
38b0c73
Compare
remi-delmas-3000
requested review from
SaswatPadhi,
feliperodri and
tautschnig
as code owners
remi-delmas-3000
force-pushed
the
contracts-havoc-statics
branch
from
38b0c73 to
4c509aa
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6829 +/- ##
===========================================
+ Coverage 77.04% 77.79% +0.74%
===========================================
Files 1594 1567 -27
Lines 185287 179719 -5568
===========================================
- Hits 142763 139809 -2954
+ Misses 42524 39910 -2614
Continue to review full report at Codecov.
|
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
Approving except for the one debug left-over.
remi-delmas-3000
force-pushed
the
contracts-havoc-statics
branch
from
4c509aa to
d3b4899
Compare
remi-delmas-3000
force-pushed
the
contracts-havoc-statics
branch
2 times, most recently
from
0bc5526 to
cbe9326
Compare
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
LGTM apart from some debug leftovers.
feliperodri
added
bugfix
aws
Now calling nondet_static from enforce_contracts and apply_loop_contracts. Reordered some imports to match the new clang-format rules.
remi-delmas-3000
force-pushed
the
contracts-havoc-statics
branch
from
cbe9326 to
f2935a3
Compare
|
Hi, I answered @feliperodri 's questions and fixed the missing newline, this should be good to go now. |
tautschnig
assigned
peterschrammel,
martin-cs and
chris-ryder and unassigned
remi-delmas-3000
|
@chris-ryder @martin-cs @peterschrammel could you take a look at this PR? It's missing a code owner review. |
| : ns(goto_model.symbol_table), | ||
| goto_model(goto_model), | ||
| symbol_table(goto_model.symbol_table), | ||
| goto_functions(goto_model.goto_functions), |
There was a problem hiding this comment.
Having goto_model, symbol_table and goto_functions is redundant.
Either have goto_model or symbol_table+goto_functions. I'd prefer the former.
There was a problem hiding this comment.
Ah, ok, I see. You are just using them as shortcuts for the goto_model members. That's fine.
There was a problem hiding this comment.
But then I wonder: is it really useful to have these at class level?
There was a problem hiding this comment.
Yes, might still be confusing that changing one thing has side effects on the other.
There was a problem hiding this comment.
Hi! I had to add the goto_model as a class member because the nondet static call I needed to add requires a goto_model. I also think that exploding the goto_model into shortcuts to its members is confusing as it could make you think these members are disconnected in some way. But it also seems like this style of having shortcuts to the symbol table, namespace of function maps like this occurs in several places in the codebase.
Do you want me to do a cleanup pass and remove shortcuts ?
There was a problem hiding this comment.
Yes, I would suggest that we clean out these particular short cuts. Note that the situation is a bit different from the widespread use of a namespace member for there is no risk of confusion as to whether a namespace is different or the same as the member of another class member. (In other words: the current code raises the question whether .symbol_table is the same as .goto_model.symbol_table or not.)
6 participants
For soundness, automatically havoc all statics as soon as loop or function contracts are checked (same effect as
--nondet-static). Variables can still be manually excluded using--nondet-static-exclude.Havocing is not activated if only
--replace-call-with-contractis used in an otherwise classic harness-based proof (we already automatically detect static variables modified by a function and havoc them during replacement).