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

51–60 of 121 posts

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

#51

Post by Cthulhu_ »

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…

> Is this some kind of NIH syndrom by Facebook?

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.

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

#52

Post by s3nnyy »

aristus wrote: post #17
amirmc wrote: post #3

More OCaml code coming out of FB. Can add this to the list, which includes, Hack, Flow and Pfff [1]. 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 wide…

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?

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

#54

Post by omouse »

aristus wrote: post #17
amirmc wrote: post #3

More OCaml code coming out of FB. Can add this to the list, which includes, Hack, Flow and Pfff [1]. 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 wide…

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.

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

#55

Post by istvan__ »

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.

Yes you right, I am not exactly clear. My understanding of symbolic manipulation is the following (from wikipedia):

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

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

#56

Post by timtadh »

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

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

#57

Post by Locke1689 »

tptacek wrote: post #50
Locke1689 wrote: post #48

Earlier quoted context omitted.

I would say a Coverity installation at Facebook is probably a "let's talk" level of expensive. That said, paying a team of expert engineers is also very expensive, not to mention the opportunity cost.

Right, and for Facebook internally, whatever the number is, it's a speed bump. 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…

I'd add

* 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.
The very fact that hiring is focusing on this group signals to me that this is an area which Facebook takes seriously and wants to be taken seriously in.

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

#58

Post by tikhonj »

pcwalton wrote: post #49
jackpirate wrote: post #44

Earlier quoted context omitted.

In what ways is OCaml's pattern matching superior to Haskell's?

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

On the flipside, Haskell just got pattern synonyms[1] which are incredibly useful for being able to refactor and work with abstract types.

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

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

#59

Post by mitchty »

dulma wrote: post #36
sadert wrote: post #28

What's the difference between this and the Clang analyzer, which comes with Xcode already? I expected that comparison to be on the front page... 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 pass…

On iOS there is the Clang Static analyzer. Infer does some things different, in particular reasoning that spans across multiple files. But CSA checks for more kinds of issues and is also more mature than Infer when it comes to iOS: we send big respect to CSA! Infer has only got started there recently. Really, these tools complement one another and it would even make sense to use both. Indeed, that's what we do inside…

clang-scan-build/clang-can-view will run anywhere clang runs.

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

Post reply on HN