Summary:
More newer = more better.
This flips the Not_found -> Not_found_s switch, and forbids a bunch more
polymorphic comparisons (mostly turned into `int` comparisons for
convenience). Earlier diffs prepare for this so this diff is only about
breaking changes in the API, of which there are only a few.
Reviewed By: jberdine
Differential Revision: D19861583
fbshipit-source-id: fe54ce8f0
Summary:
This diff adds a taint domain in Inferbo. The taint value will be used to find vulnerable array
accesses in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D19391028
fbshipit-source-id: 566b4c0fe
Summary:
Quoting the doc:
> `dune check` builds the minimal set of targets required for tooling
support. Essentially, this is .cmi, .cmt, .cmti, and .merlin files.
So, running `make check` can be a tad faster and more economical
way to typecheck the code as you develop (and make merlin understand
what's going on).
We already had `check` taget defined in `infer/src/Makefile` but it
was not exposed at the top level. Fixing it.
Reviewed By: jberdine
Differential Revision: D19619920
fbshipit-source-id: c143cecd8
Summary:
Kill these tests as that mode is not supported anymore.
Note that :
- "buck_cross_module" was effectively already dead since it's not hooked up to `make test`
- "buck" is actually another copy of "genrule" so wasn't testing anything
Reviewed By: ngorogiannis
Differential Revision: D19176166
fbshipit-source-id: b5bb90448
Summary:
Inferbo does not use the external relational domains, apron and elina. At some point, the parts of
inferbo using them were broken and they do not seem to be fixed easily in the near future. Let's
remove them and keep the code base cleaner.
Reviewed By: jvillard
Differential Revision: D19022905
fbshipit-source-id: e0eafe79f
Summary: The new domain is much better than the old one. Let's kill the old one (along with old litho tests) and simplify things.
Reviewed By: skcho
Differential Revision: D18959627
fbshipit-source-id: df77ae20e
Summary:
Let's add basic Java support to impurity checker. Since impurity checker relies on pulse, we need to add Java with Pulse callback as well. Pulse doesn't officially support Java yet, but we can enable it for impurity checker for now.
Many Java primitives/operations are not yet modeled (such as creation of new objects, support for collections etc.). Still, it is good to run impurity checker on the existing tests of the purity checker. Also, it is nice to see that we can identify most of the impure functions correctly in the purity dir. There are a lot of FNs though.
Reviewed By: skcho
Differential Revision: D17906237
fbshipit-source-id: 15308d285
Summary:
Introduce a new experimental checker (`--impurity`) that detects
impurity information, tracking which parameters and global variables
of a function are modified. The checker relies on Pulse to detect how
the state changes: it traverses the pre and post pairs starting from
the parameter/global variable and finds where the pre and post heaps
diverge. At diversion points, we expect to see WrittenTo/Invalid attributes
containing a trace of how the address was modified. We use these to
construct the trace of impurity.
This checker is a complement to the purity checker that exists mainly
for Java (and used for cost and loop-hoisting analyses). The aim of
this new experimental checker is to rely on Pulse's precise
memory treatment and come up with a more precise im(purity)
analysis. To distinguish the two checkers, we introduce a new issue
type `IMPURE_FUNCTION` that reports when a function is impure, rather
than when it is pure (as in the purity checker).
TODO:
- improve the analysis to rely on impurity information of external
library calls. Currently, all library calls are assumed to be nops,
hence pure.
- de-entangle Pulse reporting from analysis.
Reviewed By: skcho
Differential Revision: D17051567
fbshipit-source-id: 5e10afb4f
Summary:
In D17156724, we forked nullsafe tests, which was a strategy to
introduce nullsafe-gradual mode back then.
The reason was "gradual" mode is a pretty big change in a way Infer
handles annotations, so we wanted to tests both scenarios: gradual and
non-gradual mode.
The plan was to deprecate "non-gradual" tests at some point, hence we
decided to go with duplication.
Now we have a better approach to ensure "gradual" features are well
covered. The approach is the following.
1. [Mostly finished] Improve existings tests so that they cover negative and positive
cases. With this, we can safely add something like
--non-annotated-default UNKNOWN_NULLABILITY to the test config and be sure tests still make
sense (i.e. don't pass simply because annotations don't make sense
anymore)
2. [In progress]. Refactor nullsafe code so that instead of using of Annot.ml everywhere we use a special abstraction telling if the class is annotated with Nullable, Nonnull, or not annotated. With this change, we essenstially have a single place we need to test, which removes the need to have 2 pair of tests for each feature.
3. [To be done]. Introduce Uknown nullability and add small number of tests specifically
for that feature (together with existing tests).
NOTE: I did not rename `nullsafe-default` back to `nullsafe` to not
pollute blame without need.
Reviewed By: artempyanykh
Differential Revision: D17395743
fbshipit-source-id: 3d3e062f6
Summary: Adding a test to the top level makefile that I forgot to add (ooops)
Reviewed By: jvillard
Differential Revision: D17366065
fbshipit-source-id: 8111ccf7a
Summary: This shows that the current Pulse analyzer works fine in the C++ part of the Objc++ files.
Reviewed By: martintrojer
Differential Revision: D17225683
fbshipit-source-id: faf51c5fa
Summary:
In next diff, we are going to introduce a new mode of nullsafe
(gradual). For testing, we are going to employ the strategy used by jvillard
for Pulse.
In this diff we split tests into two subfolders, one for the default and one for the gradual
mode.
We are planning to make the gradual mode default eventually. For that, most
new features will make sense for gradual mode, and we will mostly evolve
tests for that mode.
As for 'default' mode, we need to preserve tests mostly to ensure we don't introduce
regressions.
Occasionally, we might make changes that make sense for both modes, in
this (expected relatively rare) cases we will make changes to both set
of tests.
An alternative strategy would be to have two sets of issues.exp files,
one for gradual and one for default mode. This has an advantage of each
java file to be always tested twice, but disadvantage is that it will be
harder to write meaningful test code so that it makes sense for both
modes simultaneously.
Reviewed By: ngorogiannis
Differential Revision: D17156724
fbshipit-source-id: a92a9208f
Summary:
- run the tests! they weren't hooked up to the main Makefile :/
- add some html debug messages
- formatting
Reviewed By: skcho
Differential Revision: D16895578
fbshipit-source-id: e96d737cc
Summary: Test that cost analysis works with incremental analysis enabled
Reviewed By: ezgicicek
Differential Revision: D16620101
fbshipit-source-id: b41403954
Summary:
It's not being worked on and is not in a state where it works.
It would probably better to write this as a script of some kind or else
resurrect this subcommand in a form where it behaves more like a script,
ie fork/execs infer analyses instead of having them be function calls
(but then it might as well *be* a script as it would likely be more
flexible).
In any case...
youarealreadydead
Reviewed By: ezgicicek
Differential Revision: D16602417
fbshipit-source-id: d0d129539
Summary:
These have proved to be too fragile to maintain as they would often break
compilation of user code. They have been off by default for more than a year
now (D7350715).
Removing the include models shows a more accurate picture of what infer results
look like in production. As such, lots of tests have changed, mostly
biabduction but also in inferbo. SIOF was using include-based models too but
now libc++ is better and iostreams are implemented in a way that SIOF
understands (instead of being magical creatures) so nothing changed there.
Reviewed By: skcho
Differential Revision: D16602171
fbshipit-source-id: ce38f045b
Summary:
Write a test for the invalidation of changed procedures
Reverse analysis graph for this test: https://fburl.com/graphviz/ybidpidq
The procedures marked as changed are `a` and `d`, and this causes `a,b,c,d,e,main` to be invalidated as expected
Reviewed By: jvillard
Differential Revision: D16579526
fbshipit-source-id: cbec304ce
Summary:
Add test `incremental_analysis_remove_file` to the toplevel makefile so that it is called by `make test` etc
Also swapped the src_before and src_after files so the test checks file removal instead of addition.
Reviewed By: jvillard
Differential Revision: D16562340
fbshipit-source-id: 79bab5f66
Summary:
The default values of config options can sometimes depend on build-time
configuration values. This makes checking that the manuals "remain the same"
trickier as the manuals can be different depending on the platform. This
removes *all* default values from the checked-in manuals. We could be more
fine-grained and scrub only the values that are susceptible to change but for
now this is probably good enough.
This is done by implementing new options `--help-scrubbed` and
`--help-scrubbed-full` and using these in our tests instead of `--help` and
`--help-full` (which remain unaffected).
Also don't wrap the default values in `$(i,...)` anymore because the defaults
can trigger line breaks and then the man page is ill-formatted because that
format is stupid.
Reviewed By: mityal
Differential Revision: D16543779
fbshipit-source-id: bc929ff8c
Summary: This test wasn't building correctly or being called by the toplevel makefile
Reviewed By: jvillard
Differential Revision: D16458386
fbshipit-source-id: 48a0c2f36
Summary:
newer is better, right?
All the code changes in infer are because of core being bumped to v0.12.
Reviewed By: jberdine
Differential Revision: D16223183
fbshipit-source-id: f3c339966
Summary:
Replaced by pulse. `--ownership` is now a deprecated form of `--pulse`.
The ownership checker is starting to give wrong answers due to changes in the
clang frontend, so it's better to remove it in favour of pulse.
there_goes_my_hero
Reviewed By: ngorogiannis
Differential Revision: D16107650
fbshipit-source-id: bb2446a19
Summary:
This is a simple checker that identifies inefficient uses of `keySet` iterator where (not only the key but also) the value is accessed via `get(key)`. It is more efficient to use `entrySet` iterator which already returns both key-value pairs. This optimization would get rid of many extra lookups which can be expensive.
We simply traverse the CFG starting from the loop head upwards and pick up the map that is iterated over. Then, we check in the loop nodes if there is a call to `get(...)` over this map. If, so we report.
Reviewed By: ngorogiannis
Differential Revision: D15737779
fbshipit-source-id: 702465b4e
Summary:
That test wasn't hooked up to `make test` and so regressed at some
unknown time in the past. Just recording the new state of things for
now.
Reviewed By: ngorogiannis
Differential Revision: D15495234
fbshipit-source-id: 14fb112de
Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.
Reviewed By: jvillard
Differential Revision: D14477671
fbshipit-source-id: c38a8ef37
Summary:
Figure out where libgmp and libmpfr are auto-magically by looking at where
`ldd` (or `otool` on osx) thinks they are.
This way we don't need to hardcode as much.
Reviewed By: ngorogiannis
Differential Revision: D14208580
fbshipit-source-id: 3b2dca5b2
Summary: Provide hooks into the autoconf configure script to define where libgmp and libmpfr may be found. Use these and opam to copy the more exotic library objects into the installation of infer on a new `make install-with-libs` target so that the binaries can be distributed usefully, i.e., without users having to install gmp, mpfr, and more importantly apron and elina (which need ocaml + opam + ..., which would defeat the point of having binaries).
Reviewed By: skcho
Differential Revision: D14065317
fbshipit-source-id: 9a2ac7200
Summary:
Building clang takes long and sometimes only some minor step in the setup
script has changed, triggering a spurious rebuild. Print a big bold message
letting the user know of their options, but only if clang has been installed
previously.
```
(warn_clang)jul@devvm2701:~/infer$ make -j 19
[04:02:44][2288770] Facebook setup...
*** Now building clang, this will take a while...
*** If you believe that facebook-clang-plugins/clang/install is up-to-date you can(TERM_RESET)
*** interrupt the compilation (Control-C) and run this to prevent clang from being rebuilt:
/home/jul/infer/facebook-clang-plugins/clang/setup.sh --only-record-install
(TIP: you can also force a clang rebuild by removing /home/jul/infer/facebook-clang-plugins/clang/installed.version)
[...]
```
Reviewed By: katiejots
Differential Revision: D13956431
fbshipit-source-id: da163643d
Summary:
`make clean` would fail calling `xcodebuild` to clean. It also calls `ant
clean`. Instead, do the cleaning ourselves by deleting the appropriate stuff so
that it's faster and more reliable.
Also clean the OCaml build before cleaning the tests as that's what more
important most of the time.
Also don't delete the man pages as part of `make clean` as they are checked in.
Also fix ant's Makefile so that the build points at the right .class files (the
path to the .class files was wrong so `make -C infer/tests/build_systems/ant`
would start `ant` for *each* file instead of once).
Reviewed By: martintrojer
Differential Revision: D13956218
fbshipit-source-id: bce27fe11
Summary: Publish solutions to the lab, and a Docker file and image to get started more quickly with infer hacking.
Reviewed By: mbouaziz
Differential Revision: D13648847
fbshipit-source-id: daf48ad03
Summary:
Switches from opam 1 to opam 2.
Opam2 has some cool new features that simplify some of the scripting.
Notable changes:
1. Use the new `opam lock` *plugin* from https://github.com/AltGr/opam-lock/ instead of https://github.com/rgrinberg/opam-lock. This has a simpler interface for our purposes.
2. Change the way `./build-infer.sh` can be called to use an already existing switch: simply pass `--user-opam-switch` to the script and it won't attempt to create/set the current switch. This can be used to build infer in a local switch for instance.
3. Take advantage of automatic pinning where possible, eg to install infer deps without using opam.locked.
Reviewed By: ngorogiannis
Differential Revision: D13167863
fbshipit-source-id: 1a667c270
Summary: Reports will now be issued for the class loads of the methods specified by the option `--class-loads-roots`.
Reviewed By: jvillard
Differential Revision: D10466492
fbshipit-source-id: 91456d723
Summary:
New analysis in foetal form to detect invalid use of C++ objects after their
lifetime has ended. For now it has:
- A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended)
- The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid.
- A simple transfer function reads and updates the stack and heap in a rudimentary way for now
- C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations
- Also, the domain has a really crappy join and widening for now (see comments in the code)
With this we already pass most of the "use after delete" tests from the
Ownership checker. The ones we don't pass are only because we are missing
models.
Reviewed By: mbouaziz
Differential Revision: D10383249
fbshipit-source-id: f414664cb
Summary:
Fix the logic for computing duplicate symbols. It was broken at some point and some duplicate symbols creeped into our tests. Fix these, and add a test to avoid duplicate symbols detection to regress again.
Also, this removes one use of `Cfg.load`, on the way to removing file-wide CFGs from the database.
Reviewed By: ngorogiannis
Differential Revision: D10173349
fbshipit-source-id: a0d2365b3
Summary:
Also changes `clang_plugin_test` so that it also runs the clang-ocaml tests, and add a new `clang_plugin_test_replace` target.
The controller you requested could not be found.: facebook-clang-plugins
Reviewed By: jberdine
Differential Revision: D10141902
fbshipit-source-id: 927c55a4f
Summary:
The method matcher is now used sufficiently it warrants refactoring out into its own module.
Also, kill dev-android-strict-mode and leave starvation-strict-mode as the stronger option.
Reviewed By: jeremydubreil
Differential Revision: D9990753
fbshipit-source-id: 626a70a19
Summary:
This allows infer devs to see the effects their changes have on the infer manuals.
Check in the manuals for each subcommand + the output of `--help-full` to get a
complete picture. If this is too annoying we can also check in only
`--help-full`.
Reviewed By: mbouaziz
Differential Revision: D9916404
fbshipit-source-id: b981e2c33
Summary:
Turn off by default until mature enough.
Also rename the dev-strict-mode test dir to highlight the dev part.
Reviewed By: mbouaziz
Differential Revision: D9775571
fbshipit-source-id: c3a41bbdf
Summary:
First step in writing an analyzer that is meant to run only on Android core library implementation.
This will, when finished, compute the library entrypoints that may lead to a strict mode violation.
The normal analyzer will use those to statically flag strict mode violations in app code.
Strict Mode is an Android debug mode, where doing certain things (like disk read/write or network activity) on the UI thread will raise an exception. We want to statically catch these, as well as indirect versions (the UI thread takes a lock and another thread holding that lock calls a method that would be a strict mode violation).
Reviewed By: mbouaziz
Differential Revision: D9634407
fbshipit-source-id: c30bcedb3
Summary:
Some paths are hardcoded in infer as being relative to the current executable,
for instance the directory where to find the models. By copying infertop.bc to
infer/bin like we do for `infer` these relative paths lead to the expected
place, which means models can be loaded in the toplevel like they would be in a
normal infer execution. This is more useful for debugging than previously.
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D9197142
fbshipit-source-id: 48c4f82fb
Summary:
This makes sure that the javac_jar is disabled when setting the external compiler option to point at the Infer wrapper
Closes#976
Reviewed By: jvillard
Differential Revision: D9193336
fbshipit-source-id: abafb51fc
Summary:
See the results online!
http://fbinfer.com/docs/man-pages.htmlhttp://fbinfer.com/docs/internal-API.html
These html pages are written by hand, but their target is auto-generated.
I cheated a bit by generating the docs for the current version of infer and not
0.15.0 but they are hopefully very similar.
Depends on D8314572
Reviewed By: jeremydubreil
Differential Revision: D8318132
fbshipit-source-id: ffca43c
Summary:
`make doc` will use `jbuilder` (which in turn uses `odoc`) to generate the
documentation for infer's modules. This is useful to browse the APIs of infer
and gives a more discoverable place to host more general documentation about
infer's internals.
Besides the actual plumbing necessary to generate the docs, this diff also
- Moves the various infer/src/*/README.md to index.mld files that make it to the generated docs
- Fixes some doc comments that would anger `ocamldoc`
Closes#435
Reviewed By: mbouaziz
Differential Revision: D8314572
fbshipit-source-id: 4a5c70e
Jules Villard
Sungkeun Cho
Artem Pianykh
Ezgi Çiçek
Nikos Gorogiannis
Josh Berdine
Dulma Churchill
Mitya Lyubarskiy
Phoebe Nichols
Martin Trojer
Radu Grigore
Dino Distefano
Nikos Gorogiannis
Mehdi Bouaziz
Julian Sutherland
Martino Luca
Jeremy Dubreil