viperproject
Termination Measures for Loops and Functions
@Aurel300 Are there still unmerged PRs that would be invalidated if we rustfmt prusti-viper and prusti-interface?
@vakaras I think you still need the enum, what if we decide not to use a HashMap<u64, VerificationResult> for the data
@vakaras I think you still need the enum, what if we decide not to use a
HashMap<u64, VerificationResult>for thedata
Do we want to support two versions of the cache at the same time? If not, I do not see why we need that.
I mean you need to at least change this line to instead give an empty cache:
error!("Failed to read cache from \"{}\": {e}", cache_loc.display()),
I mean you need to at least change this line to instead give an empty cache:
error!("Failed to read cache from \"{}\": {e}", cache_loc.display()),
Why the already existing code does not do that?
I mean you need to at least change this line to instead give an empty cache:
error!("Failed to read cache from \"{}\": {e}", cache_loc.display()),
That already happens, right? In case of error the data_res remains None, so later the unwrap_or_else creates a fresh cache.
The only reason for the enum was to ensure that reading an old version of the cache doesn't succeed by mistake. However, I think that serde doesn't guarantees an error when deserializing with a different type, not even if the new type is in a new variant of the enumeration that we had. It can be, for example, that the serialization just calls 0 the last variant of an enumeration, and if so deserializing with the additional variant whould happily succeed. The order of the variants might not even be guaranteed across compiler versions, and when an enum has only one variant the discriminant might not even be serialized.
Adding a version field makes the check more explicit; we no longer rely on the serialization of the variants and I think it's better than before. The only failure that I think is still possible is that
- We change the
HashMapto aVecand bump the version of the cache. - At the same time, a change in serde or the compiler swaps the order in which fields are deserialized.
- By chance, decoding the old version of the cache happens to produce a version that matches the bumped version that we expect.
Not knowing exactly what are the safety guarantees of serde, I assume that (3) is very unlikely but still possible. If there was a way to force the serialization to always serialize the version field first then I think we would be fully covered.
![bors[bot] avatar](https://avatars.githubusercontent.com/in/1847?v=4 "Published by a pub.dev verified publisher"){kind=small}