Definition collector too strict

[Pointerbender]

I discovered another instance where the definition collector is too strict, here:

https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L423-L427

is_unfoldable is defined as:

https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L408-L409

Unfortunately, I don't have a minimal reproduction, but I will do my best to explain 2 corner cases that I hit:

1. Due to is_unfoldable being false, the enum discriminant axioms $discriminant_axiom and $discriminant_range were being discarded here:

https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L262-L272

Presumably due to calling a pure function (for which is_unfoldable is determined to be false) which indirectly relies on the enum discriminant domain function, which is then not properly registered as "used" and its axioms are not included in the Viper program.

2. In the other case the body of a #[pure] function was discarded, but the function remained present as an abstract Viper function. However, the body is required to make the proof verify. This then gives ICEs because Prusti can't map back the error positions to the proper postconditions. Again, for the first #[pure] function that was called in the chain of function calls, it was determined that is_unfoldable = false, resulting in the situation where the remaining chained function calls were not visited in a "directly calling state":

https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L394-L396

This in turn resulted into some of the other needed #[pure] function to be erroneously emitted as abstract Viper functions.

One way that fixes both of the scenarios above is to remove the entire if-check for is_unfoldable on line 423. Although, I have the feeling there might be a (better?) fix which updates the definition of is_unfoldable to also include pure functions that are called in a "directly calling state". I'm not sure of what the best fix would be, or how to make a minimal reproduction for this (I've tried, but did not manage to recreate a simple example :cry: I can reliably reproduce these in my larger code base, though).

Would removing the if-check be acceptable? Any ideas for a better solution or how to make a small regression test?

Thanks!

[Aurel300]

We have faced similar issues with @vl0w for deeply nested generics + iterators.

[Pointerbender]

It just got weirder, in some cases I need to make Prusti explicitly retain the $discriminant_axiom and $discriminant_range domain axioms for enums, even if is_unfoldable is true! Unfortunately, this is an even deeper nested corner case :P

Edit: this even happens when this if-check is commented out:

https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L423-L427

[Pointerbender]

We have faced similar issues with @vl0w for deeply nested generics + iterators.

Have you also seen problems related to nesting pure functions too deep so that the snap constructor of a Rust type is never referenced, leading to verification failures due to the domain axioms not triggering (because its quantifiers are triggered by the snap constructor)? If so, did you by any chance find a work-around for this/these issue? :)

(This would typically manifest itself as seeing the Viper method verify correctly, but then when its inserted as a Viper function in the Viper program for another method, then the postcondition of this Viper function fails verification - even though it originally verified as a Viper method).

[vakaras]

(This would typically manifest itself as seeing the Viper method verify correctly, but then when its inserted as a Viper function in the Viper program for another method, then the postcondition of this Viper function fails verification - even though it originally verified as a Viper method).

This bug should be fixed once we fully migrate to manual axiomatization of functions.

[Pointerbender]

This bug should be fixed once we fully migrate to manual axiomatization of functions.

Ah, thanks! Is this also part of the refactoring or is this a separate feature?

[Pointerbender]

I managed to make a reduced example for 2 out of the 3 bugs mentioned in this issue:

issue-1044-1.rs.txt

It is still larger than the usual examples, but at least it's somewhat better than a whole crate :)

To recap, the 3 issues mentioned are:

1. The is_unfoldable if-check sometimes decides to eagerly to start pruning Viper code.
2. Even with the is_unfoldable check disabled, the $discriminant_axiom and $discriminant_range domain axioms for enums are omitted by the definition collector in some extreme corner cases, even though the verification relies on these being present.
3. When nesting pure function calls too deep, a Rust method may verify as a Viper method, but not as a Viper function.

This reproduction covers the first and last issue. I still am unable to make a minimal reproduction for number 2.

When running the example (note the Prusti flags -Puse_new_encoder=false -Pcheck_overflows=false at the top), the first error you encounter is that <Seq as PartialEq>::eq does not verify. If you disable this check in Prusti, then Seq::eq will verify okay:

https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L423-L427

Then, with this work-around applied, we encounter issue 3 in methods <Seq as PartialEq>::ne and Seq::single. These both include the Viper function for Seq::eq in the Viper programs, but even though Seq::eq verifies as a Viper method, it fails verification as a Viper function.

[vakaras]

This bug should be fixed once we fully migrate to manual axiomatization of functions.

Ah, thanks! Is this also part of the refactoring or is this a separate feature?

It is part of the refactoring.