10 ms·
Prusti: Static Analyzer for Rust
- za3faran 4y agoWhat 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.
- solomatov 4y agoBig tech uses static analyzers a lot. See for example, these projects: - https://fbinfer.com/ https://fbinfer.com/ (<- This one was a breakthrough in static analysis in its time) - https://github.com/google/error-prone https://github.com/google/error-prone - https://github.com/facebook/SPARTA https://github.com/facebook/SPARTA And many others
- boulos 4y agoMany of Google's general checks in clang-tidy should be directly available, too. For example, the absl checks seem to be on the list of clang-tidy checks: https://clang.llvm.org/extra/clang-tidy/checks/list.html https://clang.llvm.org/extra/clang-tidy/checks/list.html
- johnny-lee 4y agoMicrosoft bought and adapted PREfix and created a simpler, faster version called PREfast (and the Visual Studio -analyzer switch for C/C++/C# code). see tools section in https://learn.microsoft.com/en-us/previous-versions/tn-archive/cc723542(v=technet.10) https://learn.microsoft.com/en-us/previous-versions/tn-archi...
- haskellandchill 4y agoWe have some critical systems code in C that I'm going to try to run static analysis on for our Hack Week. There are probably 100 engineers at my company and not much interest in anything beyond Google SRE and language specific release updates. We use Bash, Php, Python, Ruby, Node, C, Go, and Rust.
- nerdponx 4y agoA lot of Python teams use a linter that can catch errors like "variable used before defined" as well as matters of code style, and increasingly a static type checker in addition to that (which also does its own set of such checks).
- aviramha 4y agoStatic analyzers are free CR in most cases. I highly recommend using it, and do know that in some companies people are unaware of those unfortunately..
- pjmlp 4y agoIn the typical enterprise projects I work on they are quite typical, usually we tend to use stuff like SonarQube and it breaks the build for specific errors. Usually it doesn't matter if devs themselves don't care, because when devops have the management support, they will care to fix that broken build.
- drwoland 4y agoWhen 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 mixed blessing but that is probably because every time ive seen them deployed the budget hasnt included sufficient engineering time, training or prof services to cut down huge numbers of false positives.
- wyldfire 4y ago> 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.
- IshKebab 4y agoI can't even convince my co-workers to use Typescript. :-/ I think it varies by industry though.
- Agingcoder 4y agoThey work really well, and people, while initially skeptical, eventually get the idea. The key is to run a first pass on your codebase, find and fix real bugs, and share your findings. This turns a very theoretical tool into 'see, it works, and that's one nasty bug we won't have in production'.
- ainar-g 4y agoI 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.
- smaddox 4y agoCould you comment on the others you use? I would like to start using a lot more static analysis at $job.
- ainar-g 4y agoLuckily for you, it's all open-source, heh. https://github.com/AdguardTeam/AdGuardDNS/blob/master/scripts/make/go-tools.sh#L40-L52 https://github.com/AdguardTeam/AdGuardDNS/blob/master/script... https://github.com/AdguardTeam/AdGuardDNS/blob/master/scripts/make/go-lint.sh#L196-L249 https://github.com/AdguardTeam/AdGuardDNS/blob/master/script... There's some mess in there, but if you only need a list of analysers and examples of usage, these should be enough.
- Ericson2314 4y agoI'm a "hard core PLer" and I am skeptical. I don't like automated solvers where there is no way to manually include a proof (to be checked).
- pm215 4y agoI find it depends a lot on the static analyzer. (My experience is largely with C code.) In particular, if the analyzer produces a lot of false positives it is dumping a pile of work onto the developers to work through each report and satisfy themselves that it's invalid, and hiding the real bugs under a pile of garbage. If it is more careful to avoid false positives then it's more workable as a development tool (but of course it then finds fewer interesting issues). The other key static analyzer question is "how easy is it to run and does that happen early in the development cycle?". A static analysis pass built right into the compiler and generating warnings every time you compile has the most chance of having its reports paid attention to. Something that runs at CI time is more annoying. Something that runs only on trunk a week or more behind the leading edge of development and which just lists its reported issues on a webpage somewhere is in grave danger of being outright ignored, or only read by one or two enthusiasts who are forever fixing up other peoples' code...
- heywire 4y agoNot sure how relevant my experience is, but I work on a 30+ year old Windows application that started life as a DOS application. It is written in a mix of C and C++. We still do things pretty old school. As part of submitting your work for code review (which is required for every change), you submit the output of cppcheck. When we first introduced cppcheck, there were thousands of warnings and errors that we slowly worked through. Now it is expected that the cppcheck output is empty.
- johnny-lee 4y agoThat's what scares a lot of people when they run a static analyzer on code for the first time - all the possible problems. Some of the possible problems are easy to confirm or deny just by looking at one line of code, but others will require much more analysis. You need a tool/viewer to show the possible problem and what caused the possible problem. Such a tool improves the user experience dealing with static analyzer results.
- nine_k 4y agoOur CI test run includes mypy; even in the mode where it skips certain checks, it finds subtle, non-obvious bugs time and again. I run mypy as a part of Emacs flycheck mode for Python. Switching on a static analyzer is usually somehow painful, because old code does not typecheck, or has issues that static analysis discovers but which never get triggered in real life. You have to face constant (and rightful) nagging until you fix all key parts of your code so that the static analyzer no longer has concerns. In his regard, Python is noticeably behind Typescript, because TS's type system and other amenities allow for more complete and precise descriptions of invariants that hold in the program, and which static analysis tools check.
- haskellandchill 4y agoThis looks good, I'm going to have to try out their work for Go, Gobra, since that's what I'm mostly writing these days.
- piterdevries 4y agoWhy would you need a static analyzer for a language that promotes itself as safe out of the box.
- School-Cotton 4y agoRust claims to make a particular class of bugs more difficult to write. It doesn’t claim to magically eliminate all of them.
- the-lazy-guy 4y agoIt is written in the linked README, but I will state it here. Rust checks integer overflows at runtime (or not at all, if building for maximum speed). It is safer than not checking at all. But costs performance and can lead to (predictable) crashes. This tool is a way to prove that overflows can not happen at compile time. Which is extremely hard in the general case.
- kibwen 4y agoAlso note that the reason that Rust can get away with not checking for integer overflow while still being memory-safe is because indexing operations are bounds-checked, so an overflowing index variable panics anyway.
- cesarb 4y ago> so an overflowing index variable panics anyway. Unless it overflows all the way to a valid index. Which might lead to unexpected results if the code does not expect to be using a smaller index (for instance, a code trying to access index i+2 might not be expecting it to suddenly access indexes 0 or 1).
- iudqnolq 4y agoBut Rust is still memory safe because unsafe code "morally" is unsound if it assumes something like that can't happen.
- 4y ago
- wongarsu 4y agoThat looks incredibly useful. Proving the absence of panics and overflows is already great, and with the annotations you can guarantee properties you'd normally write property tests for, like in this example from the docs: impl List { #[ensures(self.len() == old(self.len()) + 1)] pub fn push(&mut self, elem: i32) { // TODO } }
- turboponyy 4y agoCan't wait for dependently typed type systems
- Yoric 4y agoI've written code with dependently typed languages. It's very powerful, but it really is time-consuming. That won't be appropriate for all developments/developers.
- pjmlp 4y agoNo need to wait, you can pick Idris today, but it won't be a productive experience versus mainstream development tooling.
- mboekhoff 4y agoThis really reminds me of design by contract, which I find absolutely fascinating. Another library that implements this, albeit at runtime (and optionally using MIRAI is https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/
- hn92726819 4y agoI 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 agoYou 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 agoYou 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 agoI 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
- nerdponx 4y agoAccording to the Readme, this is based on a more-general verification framework called Viper, which apparently works for several languages (including Rust): https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.ch/research/viper.html There also appear to be equivalents of this tool in Python ("Nagini" https://www.pm.inf.ethz.ch/research/nagini.html https://www.pm.inf.ethz.ch/research/nagini.html) and Go ("Gobra" https://www.pm.inf.ethz.ch/research/gobra.html https://www.pm.inf.ethz.ch/research/gobra.html). I'll definitely be checking out Nagini for my work!
- insanitybit 4y agoThis 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 verification extensions to the language we can really push confidence in a working, safe product.
- jahewson 4y ago> compiles to a seccomp + apparmor profile That’s a really nice demonstrable and practical impact of using effects!
- fire 4y ago> 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
- insanitybit 4y agoI'll see if I can open source it this weekend. I'm not trying to be the "like and subscribe for updates" but if you want to see it when it's open source I'd suggest following me on Twitter (or Github? Does Github have a follow thing?) cause I won't remember to reply on HN. Here's a little snippet: #[effect::declare( args=(inner_tmp as I) returns=("/tmp/" + I) )] fn tmp_dir(inner_tmp: Path) -> Path { Path::from("tmp/").join(inner_tmp) } So it can reason about that Path's constraints. When that Path gets used by, say, "File::create(path)", it gets turned into a rule and added to an apparmor policy. Apparmor doesn't support a "hey I'm a process, please sandbox me" so I have to write a privileged daemon that manages that bit. I also have a way to apply effects to functions you don't own, mutating functions, functions that branch, etc. None of that is implemented yet, just designed.
- fire 4y ago
- WalterBright 4y agoLooks like I need to fix my binary search code!
- childintime 4y ago[off-topic] While you're at it, how about integrating D with cargo? D could: - act as a C/C++ compiler for legacy code, - shine where Rust is weakest: strings-first apps and apps that benefit from classes, - get us to a world where the best C++ is a frozen C++ Too tall an order?
- WalterBright 4y agoI'm not really qualified to judge what is the right feature set for a build system like dub or cargo.
- burjui 4y agoSadly, D has its own set of problems and design flaws. It's better than C++ in many ways, but still far from Rust in terms of solid foundation in computer science and language design. Frankly, I see no point in integrating it with Rust. And what do you mean by Rust being weakest in these categories anyway, and why do you think it is? What are "string-first apps"? And how is not adopting inheritance-based OOP a weakness? I think, many experienced programmers, especially those familiar with ML family of languages and otherwise well-versed in different paradigms, will argue that this particular flavour of OOP is more harmful than helpful.
- WalterBright 4y agoI admit I do not come from an academic computer science background. What I do bring to programming language design, however, is decades of experience in programming, compilers, and being on the front lines doing tech support on them. In other words, the human factors facet of language design. D does very well as a friendly language from a human factors perspective. A simple example of this is `+` is commonly used to mean both addition and concatenation, leading to confusion with awkward resolutions. D uses `+` for addition, and `~` for concatenation. It's been working great. We also regularly correct errors in the design of D.
- Klasiaster 4y agoIt 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. I wonder if this can be used to prove that unsafe code is memory safe.
- Aurel300 4y agoThis is an active research topic in our group. Within unsafe Rust code you lose the guarantees of the Rust ownership type system, which are important for framing (figuring out which parts of the memory _could_ be affected by the given operations). As a result, for e.g. pointer-manipulating unsafe code, the code will probably need to be annotated more heavily, to track which values are "owned" by whom etc.
- epilys 4y agoNitpick, unsafe doesn't turn off the borrow checker. It just allows you to dereference raw pointers which are the things you must be careful about by reasoning about the actual safety yourself as a programmer. Everything else that uses safe pointers (references and mutable references) remain safe.
- nine_k 4y agoBut how passing around a (constant) raw pointer is not sidestepping borrow checker? Since the pointer (AFAICT) does need to be borrowed, because it's manifestly immutable, it could be passed into several functions that alter the pointed-at memory in arbitrary order.
- epilys 4y agoYeah it is sidestepping as you say! The distinction is that if you don't sidestep by dereferencing raw pointers, the borrow check still works. Observe that you can cast as raw pointers in safe rust. What unsafe {} changes is that you can dereference them. The borrow checker still works for regularly borrowed values (&var and &mut var etc). This is probably obvious for Rust users, but I find some people take the "turn the borrow checker off" literally by assuming they won't get lifetime errors if the put an unsafe { } around their code.
- temp123789246 4y agoOut of curiosity, does anyone know how this compares to something like Liquid Haskell? Is one more or less powerful than the other?
- Aurel300 4y agoThe two tools address similar problems. The kinds of properties you can prove (automatically) should also be similar, because both Prusti and Liquid Haskell ultimately use an SMT solver to check if assertions hold. From what I have seen LH focuses on integrating into the type system (it is Liquid as in the 2008 Liquid Types paper). Generally it is possible to rewrite properties attached to a type to contracts, e.g. a non-zero Int input becomes a precondition that says that argument is non-zero. Checking termination with Prusti is also something we are working on.
- dochtman 4y agoWas a bit disappointed to discover that the advertised Prusti Assistant VS Code assistant sort of silently sits there waiting ("Checking requirements...") if you don't have Java installed. I feel like assuming Java is installed doesn't really fit the audience.
- Aurel300 4y agoWe are working on improving the error reporting for the IDE extension. Regardless of the audience, Prusti is based on the Viper verification framework which is mainly implemented in Scala.
- Animats 4y agoThat's nice. Classic verification. Someday the compiler should do this as part of optimizing run-time checks. Most of the time, either overflow is impossible, or you really needed a run time check. The static analysis I'd like for Rust is deadlock analysis. If you lock things in different orders in different threads, you can deadlock. That is, if thread A locks X, then Y, and thread B locks Y, then X, there is a potential deadlock. Whole-program static analysis can detect that. It's a good check to have, because infrequent deadlocks of this type may pass testing.
- nextaccountic 4y agoHere's a 2020 overview of Rust verification tools https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/ - it says > Auto-active verification tools > While automatic tools focus on things not going wrong, auto-active verification tools help you verify some key properties of your code: data structure invariants, the results of functions, etc. The price that you pay for this extra power is that you may have to assist the tool by adding function contracts (pre/post-conditions for functions), loop invariants, type invariants, etc. to your code. > The only auto-active verification tool that I am aware of is Prusti. Prusti is a really interesting tool because it exploits Rust’s unusual type system to help it verify code. Also Prusti has the slickest user interface: a VSCode extension that checks your code as you type it! > https://marketplace.visualstudio.com/items?itemName=viper-admin.prusti-assistant https://marketplace.visualstudio.com/items?itemName=viper-ad... Now, on that list, there is also https://github.com/facebookexperimental/MIRAI https://github.com/facebookexperimental/MIRAI that, alongside the crate https://crates.io/crates/contracts https://crates.io/crates/contracts (with the mirai_assertion feature enabled) enables writing code like this #[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))] fn geeting(person_name: Option<&str>) -> String { let mut s = String::from("Hello"); if let Some(name) = person_name { s.push(' '); s.push_str(name); } s.push('!'); s } And have it checked at compile time that the assertion holds! Which is a bit like Liquid Haskell in capability: https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/ ... and now I just noticed that prusti has a crate prusti_contracts that can do the same thing!! https://github.com/viperproject/prusti-dev/blob/master/prusti-tests/tests/verify_overflow/pass/overflow/bisect.rs https://github.com/viperproject/prusti-dev/blob/master/prust... Now I'm wondering which tool is more capable (as I understand, they leverage a SMT solver like Z3 to discharge the proof obligations, right?)