Fix side-effect check on loop invariants #5942
Conversation
SaswatPadhi
requested review from
chrisr-diffblue,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
peterschrammel,
smowton and
tautschnig
as code owners
SaswatPadhi
changed the title
feliperodri
added
aws
Codecov Report
@@ Coverage Diff @@
## develop #5942 +/- ##
===========================================
- Coverage 75.33% 75.09% -0.24%
===========================================
Files 1447 1447
Lines 157988 158066 +78
===========================================
- Hits 119013 118704 -309
- Misses 38975 39362 +387
Continue to review full report at Codecov.
|
SaswatPadhi
force-pushed
the
side_effects_fix
branch
3 times, most recently
from
3f1a56a to
d1532ea
Compare
src/goto-programs/goto_convert.cpp
Outdated
| // at multiple code points around a loop. | ||
| // Rather than performing `clean_expr` during compilation, | ||
| // we convert the invariant to logic at these various code points | ||
| // only when they are enforced (using goto-instrument). |
There was a problem hiding this comment.
So... this means that the output of goto_convert will no longer be side effect free? So I can now write code that has a different meaning if run with and without code contracts? That doesn't seem like a very safe design.
There was a problem hiding this comment.
Without having reviewed the details just yet: the short term idea is to move all invariant-related processing (as far as possible) to code_contracts.cpp, knowing that this will leave annotations in there that wouldn't satisfy side-effect freedom. Once this has been cleaned up (right now it's a mess with parts of the processing happening in all sorts of places), it should be fully integrated into goto-program conversion, possibly leaving little or (ideally) nothing left in goto-instrument.
SaswatPadhi
force-pushed
the
side_effects_fix
branch
from
d1532ea to
186a6cf
Compare
SaswatPadhi
requested review from
feliperodri and
martin-cs
and removed request for
hannes-steffenhagen-diffblue
|
After a lot of back and forth discussion and changes, it seemed like at least for the invariants that we currently write, it's sufficient to just check for |
SaswatPadhi
changed the title
SaswatPadhi
force-pushed
the
side_effects_fix
branch
2 times, most recently
from
7e1f9c1 to
f4b312a
Compare
| @@ -26,6 +28,8 @@ Date: February 2016 | |||
| #include <util/namespace.h> | |||
| #include <util/pointer_expr.h> | |||
|
|
|||
| #include "loop_utils.h" | |||
There was a problem hiding this comment.
Wouldn't forward declarations do the trick?
There was a problem hiding this comment.
Sorry, resolved this comment by mistake without addressing it.
I #included this header file for the loopt type, which is typedefed as:
typedef const natural_loops_mutablet::natural_loopt loopt;Could I forward declare it here somehow? I wasn't sure how to.
There was a problem hiding this comment.
I believe one of typename loopt; or class loopt; might still work, and likely the compiler will telly you if it doesn't :-) Not high priority, though.
We can maintain a `protected` `goto_convertt` field in our class, which would be reusable, rather than trying to instantiate an object for each codet -> goto_programt transformation.
SaswatPadhi
force-pushed
the
side_effects_fix
branch
from
f4b312a to
6a3414d
Compare
Loop invariants were rejected during compilation if any intermediate goto instructions were introduced during the cleaning process. However, this check is overly conservative -- it ends up rejecting some complex, but pure, Boolean expressions that are compiled to multiple goto instructions. We replace this logic with a call to `has_subexpr` with `ID_side_effect`.
SaswatPadhi
force-pushed
the
side_effects_fix
branch
from
6a3414d to
1debdc7
Compare
There was a problem hiding this comment.
My initial reason for objection, that we were changing a major post condition of goto-convert is gone so there is no reason for me to block this.
Some thoughts:
*. Are similar conditions checked for pre/post?
*. Are the restrictions documented in the manual?
Longer-term, do we want to ban function calls from these annotations? One thing I found nice about SPARK was being able to define predicates (like is_initialised and is_well_structured) using Ada functions. If there isn't a way of doing this you risk a lot of parallel maintenance when altering common invariants. I guess macros would be one option but these don't work for things like is_sorted_tree and having options of how much to expand them. This is well beyond the scope of this PR but is something worth thinking about IMHO and will touch this code.
| no_sideeffects.instructions.empty(), | ||
| "loop invariant is not side-effect free", | ||
| code.find_source_location()); | ||
| if(has_subexpr(invariant, ID_side_effect)) |
There was a problem hiding this comment.
As I recall, this was the really contentious part last time around. This seems much less disruptive.
I think throwing the exception is correct because the user can trigger this even if the tool is non-buggy. I wonder if it would be more user-friendly to check this earlier but ... I guess we need to check it here as well.
I wonder if this might still be a bit too conservative but, if it works for you then fine.
There was a problem hiding this comment.
Thank you, yes earlier I had removed this part entirely and was doing some checking in goto-instrument instead. Now this check is performed at goto-cc compilation.
I wonder if this might still be a bit too conservative but, if it works for you then fine.
I completely agree with you. And it's on our roadmap to allow function calls within contracts, if those functions have an empty assigns clause (so no side effects).
|
Thank you for taking a look, @martin-cs. I just wanted to mention that @feliperodri and I are actively working on the issues that you pointed out:
Not currently, but we are fix this during our refactoring pass over the code contracts module
Good call out! Nope, they are not. I would add it to our TODO list for documentation updates.
It's on our roadmap to allow function calls within contracts, if those functions have an empty assigns clause (so no side effects). |
Fixes #5915.
Invariant predicates were being cleaned (C -> logic via
clean_expr) withinconvert_loop_invariantand were rejected if any intermediate goto instructions were introduced during the cleaning process. However, this check is overly conservative -- it ends up rejecting some complex, but pure, Boolean expressions that are compiled to multiple goto instructions.We replace this logic with a call to
has_subexprwithID_side_effect.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).White-space or formatting changes outside the feature-related changed lines are in commits of their own.