Fixing issue #205#684
Conversation
mschwerhoff
left a comment
mschwerhoff
left a comment
There was a problem hiding this comment.
LGTM, I just left one "out of curiosity" comment.
Also out of curiosity, and related to my other comment: An alternative might be to store the ternary as the chunk's snapshot. This might reduce the number of decider checks — in particular, if the ternary snapshot is introduced early, while consumption happens later on many branches — at the cost of pushing work to Z3.
Anyway, just ideas, no reason to not accept this PR.
| if (v1.decider.check(Greater(perms, NoPerm()), Verifier.config.checkTimeout())) { | ||
| Some(ch.snap) | ||
| } else { | ||
| Some(Ite(Greater(perms, NoPerm()), ch.snap.convert(sorts.Snap), Unit)) |
There was a problem hiding this comment.
Out of curiosity: does it affect performance if the snapshot is always the ternary term? I.e. if you remove the decider check and the if-branch?
There was a problem hiding this comment.
I'll check; the reason I added it in the first place was that I got some "invalid pattern contains If expression" Z3 warnings (that didn't prevent it from verifying anything though IIRC).
There was a problem hiding this comment.
Good point! With heap-dependent triggers, snapshots can end up in Z3 patterns, where ternary terms are obviously not allowed. Could probably be abstracted away with uninterpreted functions, but that seems like quite a bit of overhead (maybe for Z3, definitely on Silicon's side).
By the way, I remember seeing these warnings anyway, when running the regular test suite. Maybe you fixed that in the meantime; if not, there seems to be a problem already.
There was a problem hiding this comment.
No, I haven't fixed that; we have quite a few tests that produce these warnings, yes.
I never really know what to think of those. Apart from warnings being ugly, my impression is that Z3 usually finds a way to handle the situation and the quantifiers do get instantiated correctly in the end, so I haven't put that super high on the list. Would be great to have a general solution for that though, I agree.
There was a problem hiding this comment.
"Popular" lore has it that Z3 can be configured to list quantifier patterns effectively used — maybe by some config option, or --verbosity a-gazillion. I never tried to find out if that's actually the case, though. But seeing these would help with deciding how relevant the warnings are.
There was a problem hiding this comment.
Yes, that would be interesting.
I benchmarked a version that always uses the ternary term; performance seems basically the same, but I get an additional test failure (for a test where I get lots of warnings about If in patterns when using the ternary term).
2 participants
When consuming a chunk, this PR adds a check whether the consumed permission amount is definitely non-zero. If so, nothing changes, otherwise it makes the returned snapshot a ternary expression that is unit in case the permission amount is zero.
The purpose of this change is to tighten the footprint of functions whose preconditions contain access predicates with conditional permission amounts, which fixes issue #205.
A previous PR tried to achieve the same fix by branching on the value of the permission expression; I think this solution is better, since it does not introduce additional branching (otherwise, the parameter
--conditionalizePermissions, which pushes conditions into permission expressions, would be completely useless, for example).I've also added shortcuts for evaluating comparisons between permission literals, which should mean that no additional SMT solver queries have to be made in 99% of cases. I haven't observed any noticable permormance difference as a result of this branch on a mix of test suite and frontend benchmarks or on a larger SCION example.