I am always interested in what powers these tools under the hood. I had to learn the hard way, you do not write a program analysis tool from scratch, if you can help it. I know I have tried. It is too much for one person to do. 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…
Open-sourcing Facebook Infer: Identify bugs before you ship
91–100 of 121 posts
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#92Earlier quoted context omitted.
(Infer dev here) One strength of Infer is that it is inter-procedural, yet not whole-program: each procedure gets analyzed independently. So it's cheap enough to run on large codebases while still able to find deep inter-procedural bugs.
If you're analyzing procedures independently, why is it interprocedural? Interprocedural just means that you use some information about another procedure. This is expensive because if the information about one procedure changes during the analysis, you have to go and reanalyze all the dependent procedures. There are cheap but less accurate pointer analyses, is that why it's fast?
Infer does bottom-up analysis: it starts at the bottom of the call graph and analyzes each procedure once independently of its callers. Analyzing the procedure produces a concise summary of its behavior that can be used in each calling procedure. This means that the cost of the analysis is roughly linear in the number of nodes in the call graph, which is not true for a lot of other interprocedural analysis techniques.
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.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#93Earlier quoted context omitted.
That's not a legend, it's true since they're doing a partnership with INRIA where OCaml was born. Those French computer scientists know something that American companies don't and that's that theory is important as an underlying foundation for extraordinary results.
I'd actually expand that to European - in my grad studies, the European CS world had a much more mathematical bent. Notice the the Glasgow Haskell Compiler, Coq, etc. 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 h…
room for all... zuck employs these guys and is anything but
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#94The types of issues discovered (they mention null pointer access and resource and memory leaks) is much smaller than what a tool like Coverity will find (I use it). And they analyze C and Java, two languages supported by Coverity, a very mature tool... 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 s…
Isn't Coverity expensive?
It is free for open source projects, but yes expensive otherwise.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#95Earlier quoted context omitted.
If you're analyzing procedures independently, why is it interprocedural? Interprocedural just means that you use some information about another procedure. This is expensive because if the information about one procedure changes during the analysis, you have to go and reanalyze all the dependent procedures. There are cheap but less accurate pointer analyses, is that why it's fast?
Infer does bottom-up analysis: it starts at the bottom of the call graph and analyzes each procedure once independently of its callers. Analyzing the procedure produces a concise summary of its behavior that can be used in each calling procedure. This means that the cost of the analysis is roughly linear in the number of nodes in the call graph, which is not true for a lot of other interprocedural analysis techniques…
Cool, thanks for the details. So... what do you do about cycles?
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.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#96Earlier quoted context omitted.
Legend has it there is a small room at FBHQ, containing a quorum of OCaml committers, all of them French for some reason, hacking away at level of abstraction beyond the ken of mortal man.
I guess, the OCaml committers are French, because Ocaml was invented by French dudes?
A pretty sizable chunk of the OCaml world is French. It was developed at INRIA, yeah, and maintains a lot of presence there. It's actually a tiny bit difficult from time to time in OCaml to find English resources.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#97Earlier quoted context omitted.
Infer does bottom-up analysis: it starts at the bottom of the call graph and analyzes each procedure once independently of its callers. Analyzing the procedure produces a concise summary of its behavior that can be used in each calling procedure. This means that the cost of the analysis is roughly linear in the number of nodes in the call graph, which is not true for a lot of other interprocedural analysis techniques…
Cool, thanks for the details. So... what do you do about cycles? 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 y…
Infer computes fixpoints whenever there is a cycle in the call graph, until it reaches stable procedure summaries or timeouts.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#98Earlier quoted context omitted.
I've been surprised/annoyed by this as well. My conclusion was that there are no practical problems that would make this hard, and it is most likely held back simply by the theoretical trivialness of it (what academic wants to work on something that doesn't make a good paper?).
I've heard that or-patterns can result in superlinear blowup in the number of cases, which is why Haskell compilers have not implemented it so far.
As far as I know, that's never really been a reason as to why we haven't implemented it in GHC. It's much more likely just that nobody has ever gotten around to implementing it. Shouldn't be especially hard, I imagine.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#99This is what it can find in openssl: http://marc.info/?l=openssl-dev&m=143406271519649&w=2
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#100Earlier quoted context omitted.
Cool, thanks for the details. So... what do you do about cycles? 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 y…
Infer computes fixpoints whenever there is a cycle in the call graph, until it reaches stable procedure summaries or timeouts.
Ok, thanks for indulging my curiosity guys!