I don't understand how this could work from looking at the readme. It says:
> verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable
But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint.
So if it detects any panic! Then that's amazing. But if it only detects panic for integer operations, we already have that feature. Either way, the overflow/panic! wording is confusing because it either only applies to debug builds or applies to more than integer operations
Yes, we could improve the wording -- suggestions and users are welcome! The tool is indeed much more general purpose than integer overflows: it is a based on a deductive verifier which uses symbolic execution to figure out which nodes in the CFG are reachable and under what conditions. panic!, unreachable!, failed assert!s, etc are all checked. If one can be reached, the error to show to the user is reconstructed from the compiler's span information.
If I'm reading your comment correctly, then this is so much cooler than I thought :D. Closest thing to this would be https://docs.rs/no-panic/latest/no_panic/ I believe, and the error message leaves much to be desired.
I will definitely be trying this out, but one last question: std can panic when doing tons of things (slice indexing, str.split_at, etc). Can this be used to make never-panicing programs?
The short answer is: it could be used for that. But there's a couple of things to say:
- Prusti is doing _modular_ verification: every method is verified in isolation, and all calls in that method's code only use the contracts declared on the call targets. This is good for scalability and caching and it means that a method's signature + contract is the entire API (you don't depend on its internals).
- Methods without a contract are assumed to have the precondition `true` and postcondition `true` (in other words, such a method can always be called and makes no guarantees at all about what it did to its mutable arguments or result). For methods declared within the current project, this is fine: if they could panic, Prusti would identify this when verifying them and the user would have to declare a precondition. For external methods (whose implementation is not verified), this is potentially unsound.
- However, we are in the process of creating a library of specifications for stdlib methods. We use a large-scale analysis framework (rust-corpus/qrates) to evaluate which methods are used most often. We try to specify such methods first to cover real-world Rust code usages.
Making the default precondition for external functions "false" (unless specified otherwise) would be sound but would be quite restrictive. One goal of Prusti is also incremental verification: you should be able to start using Prusti for basic checks then gradually introduce more specifications to get stronger and stronger guarantees about the program's behaviour.
> - However, we are in the process of creating a library of specifications for stdlib methods. We use a large-scale analysis framework (rust-corpus/qrates) to evaluate which methods are used most often. We try to specify such methods first to cover real-world Rust code usages.
I asked somewhere else about the difference of prusti and mirai but, could mirai also make use of this specification?
I see that prusti_contracts and the contracts crate have a different syntax, but many contracts written for one could be translated for other, right? (IOW I don't know how much their semantics differ)
Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods.
In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of abstraction might differ. It might be necessary to prove program refinement, for example.
Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.
> If not specified, overflow checks are enabled if debug-assertions are enabled, disabled otherwise
Both of the values you can set don't give you a warning though. The linked article is about producing a warning or error when there can possibly be an overflow/panic, which clippy already does.
You are overthinking things. Those are just usee to mark places in the control flow it tries to proove are unreachable. The meaning of those constructs is irrelevant.
I think they're talking about literal panic!() calls though. They used parenthesis in their examples too, which indicates they're probably talking about the macro calls.
This is a static analyzer so I would expect it can trace calls to a panic handler (which both panic! and unreachable! use). I might be overthinking things, but it looks to me like this may be able to detect panic! calls even in, say, stdlib
> verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable
But integer overflows in release builds don't panic! and aren't unreachable!. Additionally, clippy already checks this for you if you enable an optional lint.
So if it detects any panic! Then that's amazing. But if it only detects panic for integer operations, we already have that feature. Either way, the overflow/panic! wording is confusing because it either only applies to debug builds or applies to more than integer operations