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

101–110 of 121 posts

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

#101

Post by MichaelGG »

pcwalton wrote: post #32
tptacek wrote: post #27

Earlier quoted context omitted.

Ok, tangent question: if I wanted an interesting project to learn Rust with, would a symbolic evaluation checker for (say) C code be a really good fit? In the same sense as emulators turned out to be a fantastic fit for Golang? 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)…

Sure, I think it'd be a fun project to try! We use Rust for compiler construction, obviously, and it works great for us. Bear in mind, though, that Rust is manually memory managed, and there is significant cognitive overhead of having a compiler that checks that you're doing the manual memory management properly as opposed to just using a GC. I think if you want a really fast symbolic evaluation checker—say, the kind…

F# has Active Patterns, which really rock. They let you define custom patterns or destructuring functions, then use them like normal patterns.

https://msdn.microsoft.com/en-us/library/dd233248.aspx

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

#102

Post by gohrt »

pcwalton wrote: post #73
marijn wrote: post #67

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

How so? There's one case per branch. It's no more blowup than writing out the branches by hand would be.

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

#104

Post by buttproblem »

xjia wrote: post #90
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?

I'd be interested in this as well; all I could find on their site is that it is uses "patened techniques." Considering the first seperation logic paper was published in 2001 [1] and Coverity founded in 2002 [2], they probably did not (at least originally) use the same techniques.

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

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

#105

Post by cma »

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…

how does the post positive break compare?

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

#106

Post by rshaban »

ixtli wrote: post #80

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/

"Based on the success of these research advances, we formed a startup company, Monoidics, in 2009. Monoidics joined Facebook in 2013, and since then we have adopted the continuous development and deployment style practiced at Facebook and improved our analyzer based on an iterative feedback loop between our analyzer's development team and Facebook's mobile software engineers. We have demonstrated that verification technology can indeed thrive when applied to codebases at Facebook's scale and pace of change."

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

#108

Post by ixtli »

Lewisham wrote: post #37
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 was evaluated a number of times at Google, and IIRC we decided it wasn't going to scale to the codebase size we needed it to. A separate and unrelated effort ended up with us building Tricorder [1]. 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. [1] http://research.google.com/pubs/pub4…

Your second point is very good; I get the feeling that NIH is simply a buzzword at the moment. Especially since a cursory glance Infer's source code will show that it was, in fact, invented somewhere else and purchased by Facebook.

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

#109

Post by rattray »

ixtli wrote: post #80

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/

Companies often get a lot of hate for buying open-source and taking it closed.

We should really celebrate Facebook for doing the opposite here!

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

#110

Post by ribs »

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…

Blatant sales pitch: Klocwork (which I rep) is what you want. Our static analysis tool is fast enough so that your developers can run it just before a commit, but for many environments it will run when they save code, or even as they type. In a CI process you can run it on every commit. It's like a spellchecker, except that it does highly sophisticated static source code analysis.

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.

Post reply on HN