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

71–80 of 121 posts

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

#71

Post by jetru »

Rezo wrote: post #39
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…

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…

Have you tried Coverity Desktop analysis? It'll let you run Coverity on your code incrementally(for only code changes), assuming you already have a baseline.

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

#72

Post by guipsp »

timtadh wrote: post #56

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…

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

Soot is also really slow if you're using SSA on large codebases, and the code is a mess.

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

#73

Post by pcwalton »

marijn wrote: post #67
barosl wrote: post #62

Earlier quoted context omitted.

I'm mildly surprised, why isn't this a thing in Haskell? Can't it be easily added, considering an or pattern is trivially expanded to two (or more) patterns?

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.

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

#74

Post by OxO4 »

jrmd wrote: post #69
OxO4 wrote: post #46

Earlier quoted context omitted.

Sorry to hijack your comment but it sounds like you are one of the devs of Infer. I am working on static analysis as part of my PhD and I am going to be an intern at Facebook MPK this summer. Are you located at MPK as well? Any chance we could meet up for some coffee at some point?

Part of the team is in MPK. We will happy to have a chat about static analysis once you join us this summer

Cool! Looking forward to it.

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

#75

Post by dragonwriter »

barosl wrote: post #62
pcwalton wrote: post #49

Earlier quoted context omitted.

Or patterns. See http://stackoverflow.com/questions/24700762/or-patterns-in-h...

I'm mildly surprised, why isn't this a thing in Haskell? Can't it be easily added, considering an or pattern is trivially expanded to two (or more) patterns?

> Can't it be easily added, considering an or pattern is trivially expanded to two (or more) patterns?

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

[1] https://ghc.haskell.org/trac/ghc/ticket/3919

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

#77

Post by pokpokpok »

crudbug wrote: post #25
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.

I like this plot .. May be OCaml Movie :)

21 Jane Street

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

#78

Post by strlen »

tptacek wrote: post #29
istvan__ wrote: post #22

Earlier quoted context omitted.

I think one part of this is the OCaml type system. It just seems to be very suitable for symbolic manipulations. You can do a lot with algebraic data types. 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.…

I can sort of make sense of this, but I don't know enough OCaml or FbInfer to really grok it. Why would this be a particularly good example of how OCaml simplifies symbolic evaluation? Thank you, by the way! Actual code examples are kind of exactly what I'd like to see.

Not from pfff/FbInfer, but Benjamin Pierce's excellent book on types (Types and Programming Languages) uses OCaml as well, with heavy use of pattern matching on AST.

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"
In addition to pattern matching, SML and Ocaml are popular languages for this type of work as some of the graph algorithms used in static analysis are easier expressed with eager evaluation and mutability. I am guessing there are commonly accepted idioms and libraries around the use of functors, monads, applicatives, etc.. for doing these things in Haskell; there is a Haskell version of TAPL examples (as well as a Scala one). Here's a talk from Intel about their use of SML in this field, which (in a collegial manner) mocked Haskell by saying in a slide "yeah, I am sure Simon Peyton Jones has a paper on it somewhere..." (note: I attended this talk at CUFP in 2010... IIRC Simon Peyton Jones was in the room when this remark was made :-))

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.

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

#79

Post by ixtli »

svraghavan wrote: post #5

I assume it can also be used for java server side code?

I just used it to evaluate a rather large (50k LOC) java8 application deployed as a war to tomcat8. ( infer -- gradle build ) and it found a bunch of null refs that IntelliJ and humans had all missed.

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

#80

Post by ixtli »

This appears† to be the result of Facebook having purchased a UK company called Monoidics†† in 2013. It's nice to see these types of acquisitions resulting in code getting opensourced.

† https://github.com/facebook/infer/blob/2bce7c6c3dbb22646e2d6...

†† http://techcrunch.com/2013/07/18/facebook-monoidics/

Post reply on HN