Looks like I need to fix my binary search code!
Prusti: Static Analyzer for Rust
41–50 of 93 posts
Re: Prusti: Static Analyzer for Rust
#42I 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…
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 fro…
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?
Re: Prusti: Static Analyzer for Rust
#43This is great. I'm building something similar, an effects system for rust, and it looks quite a bit like this. The difference is that my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time. I have a notion of purity as well :P I think the applications of this sort of thing are pretty limitless. Maybe rust has `unsafe` but with further…
> compiles to a seccomp + apparmor profile
That’s a really nice demonstrable and practical impact of using effects!
Re: Prusti: Static Analyzer for Rust
#44I 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…
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/...
Okay two separate checks, I don't know why my mind couldn't come up with that wording.
Re: Prusti: Static Analyzer for Rust
#45It doesn't mention unsafe in the README but the website says:
The first versions of our tools are under development, and target a small but interesting fragment of Rust without unsafe features; in the future, we plan to extend our work to tackle a large portion of the language, including certain patterns of unsafe Rust code.
Re: Prusti: Static Analyzer for Rust
#46Out of curiosity, does anyone know how this compares to something like Liquid Haskell?
Is one more or less powerful than the other?
Re: Prusti: Static Analyzer for Rust
#47This is great. I'm building something similar, an effects system for rust, and it looks quite a bit like this. The difference is that my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time. I have a notion of purity as well :P I think the applications of this sort of thing are pretty limitless. Maybe rust has `unsafe` but with further…
> my effects system compiles to a seccomp + apparmor profile so that your rust program is sandboxed at runtime based on info at compile time.
is this open or proprietary? I'd love a link to a repo
Re: Prusti: Static Analyzer for Rust
#48What are people's experiences with static analyzers at companies? Many people I have spoken with have either never heard of them, or expressed no interest. Usually those same people use dynamic languages like Ruby or Python.
I lead a Go team, and we pretty much never go (heh) anywhere without a suite of static analysers. go vet, govulncheck, errcheck, and staticcheck are the required minimum, but we do use some others. Back when I used to write Ruby, lack of static analysis was a serious problem. I've been able to add Rubocop later, but it's not exactly on the same level as staticcheck, to say nothing about Prusti from the OP.
Could you comment on the others you use? I would like to start using a lot more static analysis at $job.
Re: Prusti: Static Analyzer for Rust
#49Earlier quoted context omitted.
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 fro…
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.
Re: Prusti: Static Analyzer for Rust
#50What are people's experiences with static analyzers at companies? Many people I have spoken with have either never heard of them, or expressed no interest. Usually those same people use dynamic languages like Ruby or Python.
When I worked on a big c++ codebase I found them essential for both ci/cd systems and actively debugging an issue. The valgrind suite of tools like cachegrind are very useful for both troubleshooting as well as classic static analysis and I heartily recommend investing some time in learning valgrind if you're writing c/c++ code for a platform valgrind runs on. On the other hand commercial tools have been more of a mi…
> The valgrind suite of tools like cachegrind are very useful for both troubleshooting as well as classic static analysis and I heartily recommend investing some time in learning valgrind
valgrind is not a static analysis tool. But it is a great tool, especially memcheck.