Open-sourcing Facebook Infer: Identify bugs before you ship
code.facebook.com
code.facebook.com
I am not certain of the proposed value, except it's free to other than Facebook - but not to Facebook, who pays engineers to develop this... Is this some kind of NIH syndrom by Facebook, or is there something I missed ?
If you want to make static analysis part of the everyday development process, it has to be 1) very quick, ideally seconds; minutes at most 2) preferably something the developer can just run locally before pushing a change. If it's fast and easy enough, it simply becomes another code hygiene tool like a code formatter that you'll run continuously, perhaps even directly integrated into something like IntelliJ.
To me Infer sounds like a nice complement to Coverity to catch issues as close to where they are introduced as possible. It might even be Good Enough for many projects to be the only tool, since Coverity is pretty expensive.
Just to nitpick, I think your use of the term "static analysis" is a bit too broad. Every (or almost every) production compiler or JIT does static analysis intraprocedurally, that is, confined within a function / method / procedure. On the other hand, whole program / interprocedural static analysis quickly gets very expensive, usually because an alias / pointer analysis is involved, and that's what you need for null pointer checks and stuff.
So I guess my point is, there is plenty of static analysis going on all the time, just not expensive whole program bug-finding analysis. Cheap bug-finding static analysis stuff is common, for example in GCC all those warning options to catch undefined behavior.
It's true that it a procedure changes that you may have to re-analyze all dependent procedures (and calling procedures!) in the worst case. However, in the bottom-up scheme you only need to re-analyze a procedure when the code change produces a change in the computed summary, and in practice summaries are frequently quite stable.
By "change" I didn't mean code change, I meant change in the information about the procedure collected during an iteration of the fixed point computation. But from the sounds of things you aren't computing a fixed point.
For example: A calls B and B calls A. You have information A0 and B0 about A and B. Analyze B, you have information B1 about B. Then you go and analyze A using B1. This gives you A1. Now you have to redo B, and compute B2. Use this to compute A2. This carries on until the information is not changing, i.e. An = An + 1 and Bn = Bn + 1.
We cover C/C++/Java/C#. The tool runs on the order of 1-2x of the speed of your build, and is integrated into Eclipse, IntelliJ, and Visual Studio. It's very, very fast, and it covers much of same ground as Coverity, and more. Mail me at larry.edelstein@roguewave.com to arrange a demo.
Often perceived NIH at large companies for this sort of thing is simply a byproduct of scale that is unreasonable for external companies to have to worry about supporting.
== instead of .equals() in Java
The thing is, we were used to ignoring find bugs, but lo and behold it had pointed this problem out.
That said, paying a team of expert engineers is also very expensive, not to mention the opportunity cost.
But some reasons not to use Coverity then:
* Doing it in-house gives Facebook near total control over what the system is going to focus on; they can tailor it exactly to their problem set.
* It's a worthwhile open source project, since most values of "expensive" mean "other projects won't ever use it".
* If it gets any traction as an open source project, they can draft off the work other people will put into it.
* Facebook has recently hired a number of expert language theorists and practitioners. Doing it in-house
1) Gives them something to do
2) Serves to cement Facebook's language-expertise-brand recognition and dominance.
FB has achieved a vertical integration in the IT world rivaled only by Google, Apple and maybe MS.
I'm guessing their site is designed to sell to people and not have the details.
[1] http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht... [2] https://en.wikipedia.org/wiki/Coverity
Facebook employs thousands of developers and has a product that is pretty much done (or, IDK what they spend all their development budget on atm); they have the room to create new tools. TBF though, if this was a hobby project that wasn't linked to Facebook, it wouldn't get the attention it is getting right now.
The kinds of bugs it finds are listed at: http://fbinfer.com/docs/infer-bug-types.html
It's interesting to see how building tools with languages like OCaml can reduce bugs for teams, without them having to change the language itself. I do wonder what things would be like if such languages we're used directly more widely.
You can always go from math -> pragmatism, but the reverse is nearly impossible. People get set in their ways, and it takes time to develop mathematical rigor, even if you want to.
So when you need to get mathematical expertise, you wind up needing to hire it.
I've found Sourcegraph's srclib.org (Go) and Google's kythe.io (Cpp, Go) make some interesting strides in the static analysis field as well.
IMO, treating code as query-able data can open up a lot of possibilities, and OCaml suites the field like a glove.
† https://github.com/facebook/infer/blob/2bce7c6c3dbb22646e2d6...
We should really celebrate Facebook for doing the opposite here!
If you're familiar with old-school compiler construction, this is like having a souped-up BURG built into the language. For example, pattern matching lets you say things like "if I have Load(Var, Add(Var, Constant)) where constant is a small power of two, fold it into the x86 indexed addressing mode" in one line. Unsurprisingly this is useful not only for compiler construction but for any kind of term rewriting/symbolic manipulation.
If that's true, what are the features of Rust that make this so, and roughly how would they apply to that problem domain? (I could answer that question for Golang and emulators pretty quickly).
(Hopefully this question comes across the way I intend it to, which is: I have no plans on using OCaml any time soon, believe the comments that say you want a language with pattern matching to do this in, and would love to tinker more with both Rust and symbolic evaluation.)
I think if you want a really fast symbolic evaluation checker—say, the kind that you're going to run on $BIG_COMPANY's codebase on every checkin—Rust would be a really good fit, because you get pattern matching and excellent performance. Other than OCaml and (maybe?) F#, I don't know of a language that has as sophisticated a pattern matcher as Rust does, which helps a lot with this stuff. But, if you're building a one-off tool, a more dynamic language with a GC might be more convenient.
See http://stackoverflow.com/questions/24700762/or-patterns-in-h...
It also has view patterns which are quite useful. I don't know how to replicate that in OCaml.
Combining the two lets types expose fairly sophisticated interfaces as normal patterns, which is incredibly useful for things like graphs.
[1]: https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...
At least limited support has been done as a library providing a quasiquoter [0], and there is an open ticket for it as a ghc feature. [1]
[0] https://hackage.haskell.org/package/OrPatterns-0.1/docs/OrPa...
On top of that, Cristiano Calcagno, one of the co-founders of Monoidics, the startup that Facebook bought to get the "Infer" technology is one of the people behind MetaOcaml, and has coauthored a paper with Xavier Leroy, Ocaml's creator.
Another reason is the close relationship with theorem provers, in particular Coq. You can build certified and relatively efficient functional programs by 'pressing a button' in Coq that extracting programs from either Coq functions or Coq proofs of specifications. This now also works for Haskell IIRC, but I think originally this was just for Ocaml.
While I am not certain the premise holds (OCaml dominance), one possible explanation is that many programmers were introduced to ML/OCaml through the compiler construction course and Andrew Appel's book.
http://en.wikipedia.org/wiki/Algebraic_data_type
The other feature that I personally think is great in OCaml is pattern matching. This can help you expressing computation on symbols, where usually you have few options for the input. See following:
https://github.com/facebook/infer/blob/master/infer/src/chec...
Thank you, by the way! Actual code examples are kind of exactly what I'd like to see.
In fact one thing that you might notice in the beginning when reading OCaml is that the code seems more "dense". In C I was used to reading code by skipping over large chunks of it (again I'm oversimplifying here) like the one below, and one of the things I had to get used to when learning OCaml was to slow down and avoid skipping large chunks of code:
if (some_complex_condition == failed) {
/* ... large block of code for error handling to ignore on first read .. */
}
result = malloc(...);
result->... = ...;
result->... = ....;
A short example of implementing regular expression matching using Antimirov's partial derivatives that illustrates symbolic manipulation: http://semantic-domain.blogspot.ro/2013/11/antimirov-derivat...
A step-by-step explanation of a DSL optimizer that doesn't use too many advanced notions of OCaml: http://okmij.org/ftp/tagless-final/course/optimizations.html
A nice example of symbolic manipulation is this counter-example generator for regular expression equivalence: http://perso.ens-lyon.fr/damien.pous/symbolickat/
Here is one example, in this case type-checking a ternary operator (from http://www.cis.upenn.edu/~bcpierce/tapl/checkers/tyarith/cor...):
| TmIf(fi,t1,t2,t3) ->
if (=) (typeof t1) TyBool then
let tyT2 = typeof t2 in
if (=) tyT2 (typeof t3) then tyT2
else error fi "arms of conditional have different types"
else error fi "guard of conditional not a boolean"
A great deal of this also seems to be convention/pragmatism: e.g., pfff and Hack are in OCaml -- and predate the use of Haskell at FB -- hence FbInfer is as well. Coq, which is often used for proofs of correctness of type systems, is in OCaml so someone who already uses/hacks on Coq might as well use OCaml for implementation work.
"In mathematics and computer science, computer algebra, also called symbolic computation or algebraic computation is a scientific area that refers to the study and development of algorithms and software for manipulating mathematical expressions and other mathematical objects."
Now obviously if you have types in your language that make this easier than it is a win. I thought algebraic data types makes this easier. I might be wrong. On the pattern matching side, you are not concerned about the actual value of the variables in your expressions rather the patters those are matching to. That was my intention to show with the second URL in the previous comment, but again I might be wrong on that too.
I doubt that there are nicer general purpose languages than languages like Ocaml for compiler stuff, and symbolic execution somewhat by extension. Maybe languages that have more powerful matching and maybe even term rewriting, but I don't know if they would be considered general purpose (at least fairly fringe).
http://clang-analyzer.llvm.org/
(obviously it supports Java as well, but I assume Android Studio comes with some sort of static analyzer as well, so same question?)
It specifically calls out null pointer exceptions but those... aren't a thing... in Objective-C, messages passed to nil return all 0 bits, and that's okay (unless they mean null dereferences...).
About null dereferences, they are still a problem in ObjC: if you dereference a nil block it will crash, if you access an instance variable directly or try to pass nil to arrays or dictionaries it will crash. We try to find that kind of bugs.
You just need to insert it into your makefiles as an example of the thing that "compiles" stuff.
Its not a huge deal, but just pointing out its most definitely not ios only. :)
Findbugs can be useful too; it is more akin to linters.
So what is powering this thing?
1. http://sawja.inria.fr/ This is a OCaml library for parsing .class files into OCaml datastructures. There is some built-in analysis it uses
2. Clang and LLVM which is the popular thing to build you C family analysis framework on.
I use https://github.com/Sable/soot for Java analysis myself. It is extremely powerful out of the box and can analyze: java source code, jvm bytecode and dalvik bytecode. I recommend taking a look at that if you are interested in that sort of thing.
The innovation in the released tool seems to be the incremental checking. Haven't had a lot of time to dig into that but that seems to be the important part. In general it is great that they created something useful and practical, that is always a challenge.
Soot is also really slow if you're using SSA on large codebases, and the code is a mess.
https://github.com/facebook/infer/search?utf8=%E2%9C%93&q=mo...
For Java, it's Resource leaks and Null dereferences
For C and Objective C, the list is Resource leak Memory leak Null dereference Parameter not null checked Ivar not null checked Premature nil termination argument
Did you mean you were looking for something more specific?
$ npm i -g infer-bin && infer
Just opened the example in xcode, the analyzer itself already highglights a lot of issues, like the nil dereferencing: http://i.imgur.com/CdiYRYX.png. If it's written in more modern objective-C and supports the nullable/nonnull type, the compiler will also warn / fail to build when trying to assign nil to a nonnull type.
By contrast, Infer performs deeper inter-procedural reasoning that can track the flow of values across long chains of procedure calls to identify subtle bugs that are hard to see with the naked eye. Infer doesn't support as many bug patterns as these existing tools do yet, but it can find some deep bugs that these tools will miss.
71.9% OCaml, 19% Java
https://github.com/bbatsov/rubocop
Fast enough to integrate into a continuous integration build process and catches a lot of dumb mistakes/typos before deploying to production.
class Hello { private String s; int test() { return s.length(); } }
Infer does a bottom-up analysis (callees before callers), and will infer that test() expects "s" to be allocated to run correctly.
To get an actual error, you need to call test() without initialising s, or with s being set to null by some other means prior to the call.
Here is a modified version of your example that will get Infer to complain.
class Hello { private String s; int test() { return s.length(); } int foo() { Hello a = new Hello(); return a.test(); } int bar() { Hello a = new Hello(); a.s = null; return a.test(); } }
Running "infer -- javac Hello.java" will show an error in bar(). Infer also finds the error in foo() but doesn't report it as it considers it lower-probability. This is a trade-off made in Infer to try and report only high-probability bugs. In this case it could be improved. To see that Infer finds the error in foo(), run "infer --no-filtering -- javac Hello.java".
This is a multi-level project. At both the top level and the individual module level, the command below seems to do exactly nothing. Actual output:
org.eclipse.hudson.core$ infer -- mvn build
org.eclipse.hudson.core$ cd hudson-core/
hudson-core$ infer -- mvn build
hudson-core$