Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Open-sourcing Facebook Infer: Identify bugs before you ship

code.facebook.com

Post reply on HN
Print view View original

81–90 of 121 posts

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#81

Post by pnathan »

omouse wrote: post #54
aristus wrote: post #17

Earlier 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.

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 hire it.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#82

Post by theblatte »

cactusface wrote: post #70
Rezo wrote: post #39

Earlier quoted context omitted.

Coverity is great, but for example on the mid-size service (10s but not 100s of kloc) that my team works on the analysis still takes hours. Therefore we only do it for prod releases, not on every commit or CI deployment. 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 b…

> If you want to make static analysis part of the everyday development process [...] 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, usuall…

(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.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#84

Post by mafribe »

tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

As a lot of other commenters say, pattern matching, ADTs and higher-order functions are ideal for symbolic manipulation. Nowadays many languages have that (Scala, Rust, F#, Haskell), but Ocaml is old and was probably the first language that offered these features and had a really fast, rock solid compiler producing really fast, high-quality code (since the 1990s). Programming language researchers know for a long time that ML-style languages are pretty sweet and started using them as soon as they became pragmatically viable with Ocaml in the 1990s, and a lot of them just stuck with Ocaml.

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.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#85

Post by defen »

I clicked through to the description of separation logic - http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht... - and I'm having a hell of a time understanding the first couple paragraphs. Is there a typo in there? How is z↦y∗y↦x "x points to y and separately y points to x"

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#86

Post by Dewie3 »

tptacek wrote: post #19

Can someone explain-it-like-I'm-a-90s-programmer (ELi90s?) why so much symbolic evaluation stuff gets done in OCaml? What does OCaml do that makes it so well suited for this problem domain? (I know a very little bit about symbolic evaluation and have done a very very little bit of it).

Static FP languages just feel so natural for compilers - the AST can often be perfectly naturally expressed with algebraic data types. Then you want to traverse the tree and do certain things when subtrees or nodes are of a certain shape... which turns out that pattern matching can express very nicely.

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).

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#87

Post by _shb »

defen wrote: post #85

I clicked through to the description of separation logic - http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht... - and I'm having a hell of a time understanding the first couple paragraphs. Is there a typo in there? How is z↦y∗y↦x "x points to y and separately y points to x"

There was indeed a typo in the description; it has been fixed. Sorry for the confusion!

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#88

Post by defen »

_shb wrote: post #87
defen wrote: post #85

I clicked through to the description of separation logic - http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht... - and I'm having a hell of a time understanding the first couple paragraphs. Is there a typo in there? How is z↦y∗y↦x "x points to y and separately y points to x"

There was indeed a typo in the description; it has been fixed. Sorry for the confusion!

Thanks! Was worried I was losing it.

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#89

Post by cactusface »

theblatte wrote: post #82
cactusface wrote: post #70

Earlier quoted context omitted.

> If you want to make static analysis part of the everyday development process [...] 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, usuall…

(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?

Re: Open-sourcing Facebook Infer: Identify bugs before you ship

#90

Post by xjia »

guepe wrote: post #14

The 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…

What is the underlying theory behind Coverity? Is it based on separation logic as well?
Post reply on HN