What's the advantage for Facebook of doing this,
compared to moving their developers to OCaml or Haskell?
Or is that just too hard ?
Open-sourcing Facebook Infer: Identify bugs before you ship
61–70 of 121 posts
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#62Earlier 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...
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?
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#63Earlier quoted context omitted.
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…
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?
The team is based in London, but when you get here it should be easy to connect with them.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#64I am extremely happy to see Facebook using OCaml, it is good the get some more traction in that community. I hope it gains velocity over time and becomes a viable option especially for startups where there is no technical debt. It has amazing features and as you can see even very complex problems can be solved in a concise, terse way. Kudos to Facebook on this one.
As it is pointed out, OCaml has support for algebraic data types and symbolic evaluation, doesn't this make it an excellent language for natural language processing? Are there any more examples anyone is aware of?
I guess so. I am only familiar with the following in this category:
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#65Earlier 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.
If I oversimplify I would say that due to pattern matching and functional nature of OCaml you can avoid
much of the boilerplate code needed for building tree nodes, or finding the node you want, allowing you to focus on the high-level task you want to actually achieve.
In fact one thing that you might notice in the beginning when reading OCaml is that the code seems more "dense". In C I was used to reading code by skipping over large chunks of it (again I'm oversimplifying here) like the one below, and one of the things I had to get used to when learning OCaml was to slow down and avoid skipping large chunks of code:
if (some_complex_condition == failed) {
/* ... large block of code for error handling to ignore on first read .. */
}
result = malloc(...);
result->... = ...;
result->... = ....;
A short example of implementing regular expression matching using Antimirov's partial derivatives that illustrates symbolic manipulation: http://semantic-domain.blogspot.ro/2013/11/antimirov-derivat...
A step-by-step explanation of a DSL optimizer that doesn't use too many advanced notions of OCaml: http://okmij.org/ftp/tagless-final/course/optimizations.html
A nice example of symbolic manipulation is this counter-example generator for regular expression equivalence: http://perso.ens-lyon.fr/damien.pous/symbolickat/
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#66More 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…
We use Pfff internally to generate code-graph of large polyglot code-bases (think AOSP). This graph powers the querying engine that finds all tests to be run given a diff. It is incredibly useful. My only gripe is that Pfff isn't being maintained. Pfff can barely support Java 7, let alone Java 8. C/CPP support isn't as extensive as is for PHP. How I wish Pfff was being actively maintained...
I've found Sourcegraph's srclib.org (Go) and Google's kythe.io (Cpp, Go) make some interesting strides in the static analysis field as well.
IMO, treating code as query-able data can open up a lot of possibilities, and OCaml suites the field like a glove.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#67Earlier 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?
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?).
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#68Earlier quoted context omitted.
In addition to what the other commenter said, pattern matching is really nice for this kind of thing. Of all of the functional programming languages, OCaml has probably the most sophisticated pattern matching engine around (and we basically copied it into Rust, incidentally), supporting or-patterns, multiple bindings, guards, and so forth. Pattern matching lets you essentially match on the shape of subtrees of arbitr…
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)…
Okay, an off-topic question: Can you pls briefly explain Golang-emulators-fit? Links to projects/blogs would help too. Thx.
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#69Earlier quoted context omitted.
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…
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
Re: Open-sourcing Facebook Infer: Identify bugs before you ship
#70The 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…
> 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, usually because an alias / pointer analysis is involved, and that's what you need for null pointer checks and stuff.
So I guess my point is, there is plenty of static analysis going on all the time, just not expensive whole program bug-finding analysis. Cheap bug-finding static analysis stuff is common, for example in GCC all those warning options to catch undefined behavior.