3 ms·

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

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

kibwen 4y ago
You can enable (or disable) panic-on-overflow in Rust via a compiler flag or the corresponding value in Cargo.toml: https://doc.rust-lang.org/cargo/reference/profiles.html#overflow-checks https://doc.rust-lang.org/cargo/reference/profiles.html#over...
- hn92726819 4y ago
  > 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. Edit: here's the lint that warns you that a panic or overflow can be caused: https://rust-lang.github.io/rust-clippy/master/#integer_arithmetic https://rust-lang.github.io/rust-clippy/master/#integer_arit...
Ericson2314 4y ago
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.
- hn92726819 4y ago
  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
wongarsu 4y ago
I read that as "verifies (absence of integer overflows) and (panics by proving that statements such as unreachable!() and panic!() are unreachable)". I think the docs also support this reading, overflow detection and panic detection are listed as separate features [1]. But it is poorly worded, and the readme could certainly be improved. 1: https://viperproject.github.io/prusti-dev/user-guide/verify/summary.html https://viperproject.github.io/prusti-dev/user-guide/verify/...
- hn92726819 4y ago
  Okay two separate checks, I don't know why my mind couldn't come up with that wording.
Aurel300 4y ago
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.
- hn92726819 4y ago
  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/ 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?
  - Aurel300 4y ago
    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.

kibwen 4y ago

You can enable (or disable) panic-on-overflow in Rust via a compiler flag or the corresponding value in Cargo.toml: https://doc.rust-lang.org/cargo/reference/profiles.html#overflow-checks https://doc.rust-lang.org/cargo/reference/profiles.html#over...

hn92726819 4y ago
> 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. Edit: here's the lint that warns you that a panic or overflow can be caused: https://rust-lang.github.io/rust-clippy/master/#integer_arithmetic https://rust-lang.github.io/rust-clippy/master/#integer_arit...

Ericson2314 4y ago

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.

hn92726819 4y ago
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

wongarsu 4y ago

I read that as "verifies (absence of integer overflows) and (panics by proving that statements such as unreachable!() and panic!() are unreachable)". I think the docs also support this reading, overflow detection and panic detection are listed as separate features [1]. But it is poorly worded, and the readme could certainly be improved. 1: https://viperproject.github.io/prusti-dev/user-guide/verify/summary.html https://viperproject.github.io/prusti-dev/user-guide/verify/...

hn92726819 4y ago
Okay two separate checks, I don't know why my mind couldn't come up with that wording.

Aurel300 4y ago

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.

hn92726819 4y ago
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/ 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?
- Aurel300 4y ago
  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.