viperproject
unregistered verification error: [application.precondition:insufficient.permission; 0]
The below program outputs a rather mysterious error:
pub struct A {
inner: [usize; 4],
}
impl A {
#[pure]
#[requires(index < self.inner.len())]
pub fn is_valid(&self, index: usize) -> bool {
self.inner[index] <= isize::MAX as usize
}
#[pure]
#[ensures(forall(|i: usize| (result && index < self.inner.len() && 0 <= i && i <= index) ==> (self.is_valid(i))) )]
pub fn test(&self, index: usize) -> bool {
match index {
index if 0 < index && index < self.inner.len() => self.is_valid(index) && self.test(index - 1),
index if index == 0 => self.is_valid(index),
_ => false,
}
}
}
The full error message is "unregistered verification error: [application.precondition:insufficient.permission; 0] Precondition of function snap$__$TY$__struct$m_A$Snap$struct$m_A might not hold. There might be insufficient permission to access struct$m_A(_old$pre$0)". The error message seems similar to the one in #25, however that example differs in using mutable borrows instead of immutable borrows in this new example.
The above example succeeds if the #[ensures] post-condition is removed. It looks like it is related to the universal quantifier forall. In the resulting Viper program for A::test, the relevant statements look like this (verification fails on the non-trivial assert statement):
--- SNIP ---
label l10
// ========== bb20 ==========
__t20 := true
// [mir] return
// ========== return ==========
// Target of any 'return' statement.
// Exhale postcondition
label l36
// Fold predicates for &mut args and transfer borrow permissions to old
fold acc(struct$m_A(_1.val_ref), read$())
// obtain acc(struct$m_A(_1.val_ref), write)
_old$pre$0 := _1.val_ref
// Fold the result
fold acc(bool(_0), write)
// obtain acc(bool(_0), write)
// Assert possible strengthening
// Assert functional specification of postcondition
unfold acc(bool(_0), write)
assert (unfolding acc(struct$m_A(_old$pre$0), read$()) in (let _LET_0 == (_0.val_bool) in (let _LET_2 == (old[pre](_2.val_int)) in (let _LET_1 == (old[pre](_2.val_int) < len$Snap$Slice$usize$__$TY$__Snap$Slice$usize$$int$(cons$Snap$Slice$usize$__$TY$__Seq$$int$$Snap$Slice$usize(Seq(read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 0), read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 1), read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 2), read$Snap$Array$4$usize$__$TY$__Snap$Array$4$usize$$int$$$int$(snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner), 3))))) in (forall _2_quant_a5335780e8534827844b904391c584f3_101: Int :: 0 <= _2_quant_a5335780e8534827844b904391c584f3_101 && _2_quant_a5335780e8534827844b904391c584f3_101 <= 18446744073709551615 ==> _LET_0 && (_LET_1 && (0 <= _2_quant_a5335780e8534827844b904391c584f3_101 && _2_quant_a5335780e8534827844b904391c584f3_101 <= _LET_2)) ==> m_is_valid__$TY$__Snap$struct$m_A$$int$$$bool$(snap$__$TY$__struct$m_A$Snap$struct$m_A(_old$pre$0), _2_quant_a5335780e8534827844b904391c584f3_101))))))
// Assert type invariants
fold acc(bool(_0), write)
assert true
// Exhale permissions of postcondition (1/3)
exhale acc(struct$m_A(_old$pre$0), read$())
// Exhale permissions of postcondition (2/3)
exhale acc(bool(_0), write)
// Exhale permissions of postcondition (3/3)
goto end_of_method
--- SNIP ---
Am I doing something wrong/unsupported, or could this be a bug? Thanks!
I believe this is an instance of #364: the postcondition requires _old$pre$0 to be folded to call is_valid but also unfolded to access inner. The issue was fixed by encoding pure functions using snapshots, but then the impure encoding of pure functions reintroduced it. @vakaras plans to fix this by only using snapshots in the assertions of impure code. An alternative is to modify the fold-unfold algorithm to generate unfoldings in the leaves of assertions rather than at the top-level, but this would be less efficient in other cases.
A temporary workaround should be to move self.inner.len() to its own pure function.
Thanks for the suggested work-around, that works nicely :) The only change I had to make was:
#[pure]
pub const fn len(&self) -> usize {
self.inner.len()
}
#[pure]
#[ensures(forall(|i: usize| (result && index < self.len() && 0 <= i && i <= index) ==> (self.is_valid(i))) )]
pub fn test(&self, index: usize) -> bool { /* ... */ } // function body remained unchanged
Would it be helpful if I add the failing example program to verify_partial as a regression test for when the snapshot encoding is updated?
Would it be helpful if I add the failing example program to
verify_partialas a regression test for when the snapshot encoding is updated?
Yes, thanks. Since we decided to have verify_partial, adding tests for any open issue looks good to me.
I gave a better look at this bug. It's not exactly an instance of #364. It turns out that the fold-unfold algorithm generates the correct expression, but then the fix_quantifiers pass breaks the permissions by pulling out all unfolding ... in that are inside forall to outside of forall.
I have another variation of the example program that fails verification with a similar Viper error message Assert might fail. Assertion m_invariant__$TY$__Snap$struct$m_A$$bool$(snap$__$TY$__struct$m_A$Snap$struct$m_A(_old$pre$0)) might not hold. (lib.rs_A::[email protected])
pub struct A {
current: usize,
inner: [usize; 4],
}
impl A {
#[pure]
#[requires(index < self.len())]
pub fn is_valid(&self, index: usize) -> bool {
self.inner[index] <= isize::MAX as usize
}
#[pure]
#[ensures(result == self.inner.len())]
#[ensures(result == 4)]
pub const fn len(&self) -> usize {
self.inner.len()
}
#[pure]
#[ensures(forall(|i: usize| (result && index < self.len() && 0 <= i && i <= index) ==> (self.is_valid(i))) )]
pub fn inner_invariant(&self, index: usize) -> bool {
match index {
index if 0 < index && index < self.len() => self.is_valid(index) && self.inner_invariant(index - 1),
index if index == 0 => self.is_valid(index),
_ => false,
}
}
#[pure]
pub fn invariant(&self) -> bool {
self.current < self.len() && self.inner_invariant(self.len() - 1)
}
#[requires(self.invariant())]
#[requires(current < self.len())]
#[ensures(self.inner == old(self.inner))]
#[ensures(self.invariant())]
pub fn set_current(&mut self, current: usize) {
self.current = current;
}
}
This time, the error appears in the Viper program for A::set_current(). Note that in this example, the Viper program for A::inner_invariant() verifies okay (this is the same method as A::test() in the first example program, but with the work-around for self.inner.len() applied). The failing Viper statement is again an assert:
--- SNIP ---
label l3
// Fold predicates for &mut args and transfer borrow permissions to old
fold acc(usize(_1.val_ref.f$current), write)
fold acc(struct$m_A(_1.val_ref), write)
// obtain acc(struct$m_A(_1.val_ref), write)
_old$pre$0 := _1.val_ref
// Fold the result
fold acc(tuple0$(_0), write)
// obtain acc(tuple0$(_0), write)
// Assert possible strengthening
// Assert functional specification of postcondition
assert (unfolding acc(struct$m_A(_old$pre$0), write) in snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_old$pre$0.f$inner)) == old[pre](snap$__$TY$__Array$4$usize$Snap$Array$4$usize(_1.val_ref.f$inner)) && m_invariant__$TY$__Snap$struct$m_A$$bool$(snap$__$TY$__struct$m_A$Snap$struct$m_A(_old$pre$0))
// Assert type invariants
assert true
// Exhale permissions of postcondition (1/3)
exhale acc(struct$m_A(_old$pre$0), write)
// Exhale permissions of postcondition (2/3)
exhale acc(tuple0$(_0), write)
// Exhale permissions of postcondition (3/3)
goto end_of_method
label end_of_method
--- SNIP ---
If I remove the #[ensures(forall(...))] on A::inner_invariant, then the same error is also still present.
If I update fn invariant to:
#[pure]
pub fn invariant(&self) -> bool {
self.current < self.len() // call to recursive method removed
}
OR update fn inner_invariant to:
#[pure]
pub fn inner_invariant(&self, index: usize) -> bool {
true
}
then the Viper program for A::set_current verifies okay in both case, so this seems related to the function body of the recursive method A::inner_invariant (not just related to its forall postcondition).
Could you try updating Prusti? With Prusti version: commit 53f8dc4 2021-10-27 16:11:40 UTC, built on 2021-10-27 16:18:35 UTC I don't get that error, and I recently fixed a bunch of stuff in #730.
My output:
error: [Prusti: verification error] postcondition might not hold.
--> tmp/program.rs:40:15
|
40 | #[ensures(self.invariant())]
| ^^^^^^^^^^^^^^^^
|
note: the error originates here
--> tmp/program.rs:41:5
|
41 | / pub fn set_current(&mut self, current: usize) {
42 | | self.current = current;
43 | | }
| |_____^
Verification failed
I get the same error in Prusti as you describe (I was already on that commit luckily :smile: ). However, I hope I'm understanding correctly what Prusti expects in terms of specifications, I believe this error is a false positive.
For the second example, Prusti tells us [Prusti: verification error] postcondition might not hold. and the error behind that in Viper is Assert might fail. Assertion m_invariant__$TY$__Snap$struct$m_A$$bool$(snap$__$TY$__struct$m_A$Snap$struct$m_A(_old$pre$0)) might not hold. (lib.rs_A::[email protected]). In this case it's not exposed through Prusti as a unregistered verification error, because Prusti was able to tie it to the postcondition of fn set_current. In the first example, Prusti was not able to link it to the postcondition for some reason and pointed to the location (0, 0). (Apologies, I should have led with this first!)
What I would expect here, considering that fn set_current takes an argument that satisfies the invariant (current < self.len()), and that self.current == current && self.inner == old(self.inner), Prusti should be able to deduct that when the invariant holds before calling fn set_current, then the invariant should also hold at the end of the method call. I've been trying to add more specifications in the hopes of making Prusti believe me, but so far I have not found a way to do that. :smile:
I get the same error in Prusti as you describe (I was already on that commit luckily ). However, I hope I'm understanding correctly what Prusti expects in terms of specifications, I believe this error is a false positive.
Oh, I see. I thought that Prusti was spitting that Viper error message.
When self.current changes, all the pure functions with a signature that allows to read self.current are not guaranteed to evaluate to the same value. So, the postcondition has to be proved from scratch, opening the definition of the pure functions, and inner_invariant seems to be too complex to be proved automatically by Prusti/Z3.
Since is_valid and inner_invariant don't need to depend on self.current, you could try restricting their signature to something like inner_invariant(inner: &[usize; 4], index: usize), moving them out of the trait. This way, the solver has an easier job because it knows fore sure that inner_invariant doesn't depend on self.current.
In the first example, Prusti was not able to link it to the postcondition for some reason and pointed to the location (0, 0).
Yes, that's because a [application.precondition:insufficient.permission; 0] should never happen. If it happens, it always indicates a bug in the encoding. So, we don't care linking it to the source program.
Sorry to report back so soon :sweat_smile: This simplified program (signatures adjusted, moved out of impl A):
#[pure]
#[requires(index < inner.len())]
pub fn is_valid(inner: &[usize; 4], index: usize) -> bool {
inner[index] <= isize::MAX as usize
}
#[pure]
#[ensures(forall(|i: usize| (result && index < inner.len() && 0 <= i && i <= index) ==> (is_valid(inner, i))) )]
pub fn inner_invariant(inner: &[usize; 4], index: usize) -> bool {
match index {
index if 0 < index && index < inner.len() => is_valid(inner, index) && inner_invariant(inner, index - 1),
index if index == 0 => is_valid(inner, index),
_ => false,
}
}
is triggering an ICE during verification:
[2021-10-28T10:04:05Z INFO prusti_driver] Prusti version: commit 53f8dc438 2021-10-27 16:11:40 UTC, built on 2021-10-28 10:01:11 UTC
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] Received 3 functions to be verified:
[2021-10-28T10:04:05Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] - main (prusti_example::main)
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] Source: src/lib.rs:229:1: 229:14 (#0)
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] - is_valid (prusti_example::is_valid)
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] Source: src/lib.rs:13:1: 13:58 (#0)
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] - inner_invariant (prusti_example::inner_invariant)
[2021-10-28T10:04:05Z INFO prusti_viper::verifier] Source: src/lib.rs:19:1: 19:65 (#0)
[2021-10-28T10:04:05Z INFO prusti_viper::encoder::encoder] Encoding: main (prusti_example::main)
[2021-10-28T10:04:05Z INFO prusti_viper::encoder::encoder] Encoding: is_valid (prusti_example::is_valid)
[2021-10-28T10:04:05Z INFO prusti_viper::encoder::encoder] Encoding: inner_invariant (prusti_example::inner_invariant)
thread 'rustc' panicked at 'assertion failed: perm_amount.is_valid_for_specs()', prusti-viper/src/encoder/foldunfold/mod.rs:839:21
stack backtrace:
--- SNIP ---
At this point I'm wondering if I should take this to a separate Github issue, but somehow this still might be related (referring to my earlier comment: "this seems related to the function body of the recursive method A::inner_invariant"). The relevant code from vir/gen/vir_gen.rs is:
impl PermAmount {
#[doc = " Can this permission amount be used in specifications?"]
pub fn is_valid_for_specs(&self) -> bool {
match self {
PermAmount::Read | PermAmount::Write => true,
PermAmount::Remaining => false,
}
}
}
Which seems to hint at some kind of permission error, which Viper was also complaining about in the previous example.
Mmm, the latest error seems to be a bug in the encoding of the expiration of shared references. Maybe shared references of slice types are handled incorrectly. It's definitely a different issue.
Minimal example:
use prusti_contracts::*;
#[pure]
#[trusted]
pub fn foo(inner: &[usize; 4]) {}
#[pure]
pub fn bar(inner: &[usize; 4]) -> bool {
foo(inner);
foo(inner);
true
}
#[trusted]
fn main() {}
The suggested minimal example gives a different error for me (internal error: entered unreachable code: Tuple([]), the one from #298). An even more minimal example which triggers assertion failed: perm_amount.is_valid_for_specs() is:
use prusti_contracts::*;
#[pure]
pub fn foo(inner: &[usize; 4]) -> bool { true }
#[pure]
pub fn bar(inner: &[usize; 4]) -> bool {
foo(inner);
foo(inner);
true
}
fn main() {}
Shall I also create a new Github issue for this one?
Shall I also create a new Github issue for this one?
Yes, thanks!
(I didn't get that error because I was on #732, good point.)
I gave a better look at this bug. It's not exactly an instance of #364. It turns out that the fold-unfold algorithm generates the correct expression, but then the fix_quantifiers pass breaks the permissions by pulling out all unfolding ... in that are inside forall to outside of forall.
I'm currently looking a bit deeper into this one :) At a high level the problem seems to be that there is an implication A ==> B inside the forall, for which the unfolding acc(X) in ... sits inside the antecedent A, but then acc(X) is also required within the consequent B (as a pre-condition to one of the functions called in the consequent B). When the unfolding acc(X) in ... is moved outside of the forall, the acc(X) permission is no longer available to consequent B, because it's already used by the outer unfolding.
One idea I have to fix this is not to pull the unfolding out of the forall if it lives insides an implication by overriding <UnfoldingExtractor as vir::ExprFolder>::fold_bin_op() not to traverse a BinOp of kind BinaryOpKind::Implies. Would this be a sound approach?
I'm planning to skip folding the entire implication in this case, because there could be multiple implications inside a forall, which all could potentially use acc(X) in the antecedent, consequent or both. Pulling just one of those out, could break the permissions for the other implications.
Thanks!
@Pointerbender FYI: This should be fixed in my refactoring (by completely getting rid of the problematic code). However, I am currently blocked waiting for @Aurel300 to finish his refactoring…
Thanks for the heads up! In that case I'll just apply a temporary hack on my local version of Prusti to disable moving out the unfoldings :)
@vakaras just in case, in the upcoming refactoring, were the only removed optimizations in the fix_quantifiers pass, or will other optimizations also be affected? The reason I'm asking is because I may have found a problem with the optimize_folding pass, which I'm currently investigating (I will open a separate issue once I figured out what is causing it). Thanks!
@vakaras just in case, in the upcoming refactoring, were the only removed optimizations in the
fix_quantifierspass, or will other optimizations also be affected? The reason I'm asking is because I may have found a problem with theoptimize_foldingpass, which I'm currently investigating (I will open a separate issue once I figured out what is causing it). Thanks!
All code that works with expressions will be affected in some way. Also, some code that works with statements.
The program in the first message now panics:
thread 'rustc' panicked at 'not yet implemented', prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs:34:5
The program in the first message now panics:
thread 'rustc' panicked at 'not yet implemented', prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs:34:5
For now this panic can be worked around by commenting out this statement and compile a custom build of Prusti:
https://github.com/viperproject/prusti-dev/blob/75c09b98d388e8d32a5521362c2c68010834466e/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs#L288-L294