Summary:
I'm working on parameterizing access trees with a config that will limit max depth + perhaps width if needed.
This is a stepping stone to enforcing max depth.
Reviewed By: jvillard
Differential Revision: D5693453
fbshipit-source-id: c15b0ee
Summary:
Rather than printing the footprint using its actual representation (an access trie with bool nodes), print it as a set of access paths.
This makes it easier to read sources in Quandary specs/debug Quandary.
Reviewed By: jeremydubreil
Differential Revision: D5682630
fbshipit-source-id: ac55b7f
Summary:
Add `is_empty` to `AbstractDomain.WithBottom` sig and use the empty checks for nicer printing of access trees: don't print empty nodes/traces.
This should make it easier to debug Quandary; it's pretty hard to stare at an access tree and see what's going on right now.
Reviewed By: jberdine
Differential Revision: D5682248
fbshipit-source-id: 56d2a9d
Summary:
This gets rid of the horrible hack of asking jbuilder to build
_build/{default,test}/.ppx/ppx_compare/ppx.exe prior to starting several
jbuilds in parallel. We now refrain from starting several jbuilds in parallel.
Also, I finally understood that order-only deps do nothing for phony targets,
and not much else for non-phony ones. I hate make even more.
Reviewed By: jberdine
Differential Revision: D5678699
fbshipit-source-id: 52179e8
Summary:
This simplifies the jbuild files: no need to list these files explicitly
anymore, nor to exclude them explicitly from the main `InferModules` library
(due to their different compilation flags).
Isolate common parts into jbuild.common do `cat`-based code inclusion into
jbuild files to factorize code.
Reviewed By: jberdine
Differential Revision: D5678328
fbshipit-source-id: 6d7d925
Summary: In case of syntax errors in AL files, stdout will contain a JSON list with all files affected by the errors, including info like filename and line number.
Reviewed By: dulmarod, jvillard
Differential Revision: D5640272
fbshipit-source-id: 569b16d
Summary:
A function can both be a sink and propagate source info, but we currently ignore the summary for any function that is also a sink.
This will cause us to under-report for (e.g.) `src1 = source(); src2 = strcpy(dest, src1); exec(src2)`.
This is both a potential buffer overflow and a potential shell injection, but we won't report the second issue.
Reviewed By: jberdine
Differential Revision: D5676167
fbshipit-source-id: 232ab2f
Summary:
We now represent the footprint with an access trie, so this code is no longer required.
This lets us simplify things a bit
Reviewed By: jberdine
Differential Revision: D5664484
fbshipit-source-id: c35edf2
Summary:
In looking at summaries that Quandary took a long time to compute, one thing I notice frequently is redundancy in the footprint sources (e.g., I might see `Footprint(x), Footprint(x.f), Footprint(x*)`).
`sudo perf top` indicates that joining big sets of sources is a major performance bottleneck, and a large number of footprint sources is surely a big part of this (since we expect the number of non-footprint sources to be small).
This diff addresses the redundancy issue by using a more complex representation for a set of sources. The "known" sources are still in a set, but the footprint sources are now represented as a set of access paths (via an access trie).
The access path trie is a minimal representation of a set of access paths, so it would represent the example above as a simple `x*`.
This should make join/widen/<= faster and improve performance
Reviewed By: jberdine
Differential Revision: D5663980
fbshipit-source-id: 9fb66f8
Summary:
The previous widening operator added stars to the *end* of paths that existed in `next` but not `prev`. This is not enough to ensure termination in the case where the trie is growing both deeper and wider at the same time.
The newly added test demonstrates this issue. In the code, there's an ever-growing path of the form `tmp.prev.next.prev.next...` that wasn't summarized by the previous widening operator. The new widening is much more aggressive: it replaces *any* node present in `next` but not `prev` with a `*` (rather than trying to tack a star onto the end). This fixes the issue.
This issue was causing divergence on tricky doubly-linked list code in prod.
Reviewed By: jeremydubreil
Differential Revision: D5665719
fbshipit-source-id: 1310a92
Summary:
Saw these two types of errors before (but they're hard to reproduce locally) when building the models:
- `ERROR: Zip.Error("/mnt/btrfs/trunk-git-infer-739-1503054473/infer/bin/../lib/java/models.jar", "", "end of central directory not found, not a ZIP file")`. I think this means infer reads a partially-written models jar. We shouldn't try to load this in models mode.
- `install` would complain that the destination already exists. I think this can only happen if there's a race and the file gets created between when install first checks and when it tries to write to it.
This made me realise that the some of the models are computed in C and C++ mode
and we pick one computed spec arbitrarily. That sounds a bit dodgy but at least
now we do so in a non-racy way.
Reviewed By: jeremydubreil
Differential Revision: D5658389
fbshipit-source-id: 8077279
Summary: Also, stop trying to delete directories that do not exist: "sources" and "filelists".
Reviewed By: mbouaziz
Differential Revision: D5658089
fbshipit-source-id: e1cdb13
Summary:
This is a check for when an unavailable class is being allocated.
This diff also adds a check for the context to remove false positives: If the class is not available but the method calls are wrapped in a check whether the class is available, then don't report.
Reviewed By: jvillard
Differential Revision: D5631191
fbshipit-source-id: 2082dfe
Summary: Other parts of the code where using the checks in the AndroidFramework module. It is better to have those things in one place.
Reviewed By: sblackshear
Differential Revision: D5654247
fbshipit-source-id: 2a783e7
Summary:
Calling exit at the end of a proc does not create unreachable code, prior to this commit inferbo reports that it does.
We extend collect_instrs to detect when we're at the end of a procedure in C and not report on unreachable code if we call a procedure there.
Reviewed By: mbouaziz
Differential Revision: D5623637
fbshipit-source-id: 0d5f326
Summary: This check is not possible in Java as it natirally happens in the totally legit case of the `try ... finally`.
Reviewed By: sblackshear
Differential Revision: D5568802
fbshipit-source-id: 24ca074
Summary:
Instead of a whitelist and blacklist and default issue types and default
blacklist and filtering, consider a simpler semantics where
1. checkers can be individually turned on or off on the command line
2. most checkers are on by default
3. `--no-filtering` turns all issue types on, but they can then be turned off again by further arguments
This provides a more flexible CLI and is similar to other options in the infer
CLI, where "global" behaviour is generally avoided.
Dynamically created checkers (eg, AL linters) cause some complications in the
implementation but I think the semantics is still clear.
Also change the name of the option to mention "issue types" instead of
"checks", since the latter can be confused with "checkers".
Reviewed By: jberdine
Differential Revision: D5583238
fbshipit-source-id: 21de476
Summary:
Every module declared but not used in the same source file is warned about
currently. Disable the noisy warning.
For instance, before this diff (and after "M-x merlin-restar-process"):
1. open AbstractInterpreter.ml
2. merlin shows a warning for `module Make` inside emacs
Reviewed By: jberdine
Differential Revision: D5621383
fbshipit-source-id: c175e5d
Summary:
Seeing rrors in "/foo/bar/src/base/infer.ml" is less distracting than seeing
errors in "/foo/bar/src/./base/infer.ml".
Reviewed By: jberdine
Differential Revision: D5621060
fbshipit-source-id: 55ee069
Summary:
The issue was as follows:
- ppx.exe depended on all the ocaml source files
- ppx.exe is an implicit prerequisit of all the (non-automatically-generated) build objects in jbuilder
- as a result, when modifying a source file, we would recompile ppx.exe, thus all the source files
ppx.exe only needs to depend on all the generated source files, so that
jbuilder can find them all.
Reviewed By: jberdine
Differential Revision: D5621007
fbshipit-source-id: 92c5b9c
Summary:
The `-index-store-path` argument does not exist in Clang 5.0 and it gets discarded without any error message. The problem is that its argument, a folder, is not discarded, and Clang considers it as a source file. This leads to the following errors:
- `cannot specify -o when generating multiple output files` (this happens if a `-o` argument is passed)
- `error reading '<PATH>'` (this can be observed when running the "normalized" version of the clang command, generated via the -### flag)
This weird case can be observed when `-index-store-path` is passed in a sequence like the following: `-x c -index-store-path <PATH> -c`.
With this change, we remove the `index-store-path` option, and its argument, from the original clang command.
Reviewed By: jvillard
Differential Revision: D5601808
fbshipit-source-id: 4200308
Summary:
This gives additional information to users. For instance:
```
--biabduction
Activates: the separation logic based bi-abduction analysis using
the checkers framework (Conversely: --no-biabduction)
This option is relevant to infer-analyze(1).
```
Reviewed By: sblackshear
Differential Revision: D5583197
fbshipit-source-id: 2960b90
Summary:
We previously lumped ownership predicates in with all other predicates. That limited us to a flat ownership domain.
This diff separates out the ownership predicates so we can have a richer lattice of predicates with each access path.
This lets us be more precise; for example, we can now show that
```
needToOwnBothParams(Obj o1, Obj o2) {
Obj alias;
if (*) { alias = o1; } else { alias = o2; }
alias.f = ... // both o1 and o2 need to be owned for this to be safe
}
void ownBothParamsOk() {
needToOwnBothParams(new Obj(), new Obj()); // ok, would have complained before
}
```
is safe.
Reviewed By: jberdine
Differential Revision: D5589898
fbshipit-source-id: 9606a46
Summary:
This makes it easier to test a single checker.
Also refactor the code to make it harder to mess up the list of default/all checkers.
Reviewed By: sblackshear
Differential Revision: D5583209
fbshipit-source-id: 7c919b2
Summary:
This makes the CLI more complete: before, it was often impossible to "go back"
once some options were passed, namely options produced by `mk_*_{list,opt}`.
Now these automatically create an accompanying `--<long>-reset` option that
resets the config variable to its default value.
Also unify our naming of `~meta` arguments:
- no more spaces in them (except one instance where it's a whole sentence)
- use `+foo` if `foo` can be specified multiple times
Reviewed By: dulmarod
Differential Revision: D5583187
fbshipit-source-id: a8c2567
Summary:
Use jbuilder to build infer instead of ocamlbuild. This is mainly to get faster builds:
```
times in 10ms, ±differences measured in speedups, 4 cores
| | ocb total | jb | ±total | ocb user | jb | ±user | ocb cpu | jb | ±cpu | ocb sys | jb | ±sys |
|-----------------------------------+-----------+------+--------+----------+------+-------+---------+-----+------+---------+------+------|
| byte from scratch | 6428 | 2456 | 2.62 | 7743 | 6662 | 1.16 | 138 | 331 | 2.40 | 1184 | 1477 | 0.80 |
| native from scratch | 9841 | 4289 | 2.29 | 9530 | 8834 | 1.08 | 110 | 245 | 2.23 | 1373 | 1712 | 0.80 |
| byte after native | 29578 | 1602 | 18.46 | 4514 | 4640 | 0.97 | 170 | 325 | 1.91 | 543 | 576 | 0.94 |
| change infer.ml byte | 344 | 282 | 1.22 | 292 | 215 | 1.36 | 96 | 99 | 1.03 | 040 | 066 | 0.61 |
| change infer.ml native | 837 | 223 | 3.75 | 789 | 174 | 4.53 | 98 | 99 | 1.01 | 036 | 47 | 0.77 |
| change Config.ml byte | 451 | 339 | 1.33 | 382 | 336 | 1.14 | 97 | 122 | 1.26 | 056 | 80 | 0.70 |
| change Config.ml native | 4024 | 1760 | 2.29 | 4585 | 4225 | 1.09 | 127 | 276 | 2.17 | 559 | 644 | 0.87 |
| change cFrontend_config.ml byte | 348 | 643 | 0.54 | 297 | 330 | 0.90 | 96 | 67 | 0.70 | 038 | 102 | 0.37 |
| change cFrontend_config.ml native | 1480 | 584 | 2.53 | 1435 | 906 | 1.58 | 106 | 185 | 1.75 | 136 | 178 | 0.76 |
#+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2
50 cores
| | ocb total | jb | ±total | ocb user | jb | ±user | ocb cpu | jb | ±cpu | ocb sys | jb | ±sys |
|---------------------+-----------+------+--------+----------+------+-------+---------+----+------+---------+------+------|
| byte from scratch | 9114 | 2061 | 4.42 | 9334 | 5133 | 1.82 | | | 0/0 | 2566 | 1726 | 1.49 |
| native from scratch | 13481 | 3967 | 3.40 | 12291 | 7608 | 1.62 | | | 0/0 | 3003 | 2100 | 1.43 |
| byte after native | 3467 | 1476 | 2.35 | 5067 | 3912 | 1.30 | | | 0/0 | 971 | 801 | 1.21 |
#+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2
```
Menu:
1. Write a jbuild file, autogenerated from jbuild.in because we need to fill in
some information at build-time (really, at configure time, but TODO), such as
whether or not clang is enabled.
2. Nuke lots of stuff from infer/src/Makefile that is now in the jbuild file
3. The jbuild file lives in infer/src/ so it can see all the sources. If we put it somewhere else, eg, infer/, then `jbuilder` scans too many files (all irrelevant) and takes 2.5s to start instead of .8s. Adding irrelevant directories to jbuild-ignore does not help.
4. jbuilder does not support subdirectories, so resort to listing all the
source files in the generated jbuild (only source directories need to be
manually listed in jbuild.in though). Still, the generated .merlin is wrong
and makes merlin find source files in _build, so manually tune it to get
good merlin support. We also lose some of merlin for unit tests as it
cannot see their build artefacts anymore.
5. checkCopyright gets its own jbuild because it's standalone. Also, remove
some deprecation warnings in checkCopyright due to the new version of Core from
a while ago.
6. Drop less-used Makefile features (they had regressed anyway) such as
building individual modules. Also, building mod_dep.pdf now takes all the
source files available so they better build (before, it would only take the
source files from the config, eg with or without clang) (that's pretty minor).
7. The toplevel is now built as a custom toplevel because that was easier. It
should soon be even easier: https://github.com/janestreet/jbuilder/issues/210
8. Move BUILTINS.mli to BUILTINS.ml because jbuilder is not happy about
interface files without implementations.
In particular, I did not try to migrate too much of the Makefile logic to jbuilder,
more can be done in the future.
Reviewed By: jberdine
Differential Revision: D5573661
fbshipit-source-id: 4ca6d8f
Summary:
The only path to the `MergeCaptured.slink` function is when we should merge, so
it doesn't make sense to check `Config.merge` again. In the case of `infer run
--flavors -- buck ...`, this would create regular symlinks instead of the much
faster multilinks.
Reviewed By: jberdine
Differential Revision: D5574020
fbshipit-source-id: df710ca
Summary:
Fix for the #669. Recursion problem has been reproduced (see the new doctest in the latest commit) and eliminated. I guess the new version will work faster too (no more unnecessary slicing).
Closes https://github.com/facebook/infer/pull/697
Reviewed By: sblackshear
Differential Revision: D5507925
Pulled By: jvillard
fbshipit-source-id: 21fa07b
Summary:
This is a needed step in the direction of making prenalysis functional: it will return a view of the CFG rather than mutating the CFG.
ProcCfg already works by providing a view on the underyling CFG, but the bi-abduction can't leverage this because it uses the "raw" CFG.
This diff does a partial swap of the raw CFG for an exceptional ProcCfg. The goal is to make sure the bi-abduction never calls `Procdesc.get_instrs`; it should use the `ProcCfg` wrapper instead.
That way, preanalyses that add instructions (like the liveness prenalysis) will work.
There's still some calls to `Procdesc.get_succs` etc., but we can remove those in a future diff.
They're not on the critical path because the current preanalyses only add instructions, not nodes or edges.
Reviewed By: jeremydubreil
Differential Revision: D5556387
fbshipit-source-id: 4ffda00
Summary:
Previous version was hard to understand because it was doing many things within same code. New version has different code for Arrays, Structs and others.
There is some copy-paste, but it's easier to follow code (open to suggestions though)
Reviewed By: dulmarod
Differential Revision: D5547999
fbshipit-source-id: 77ecb24
Summary: It wasn't using code from `std::vector::empty` which recently was improved. Instead of inlining `std::vector::empty`, call it to know whether vector is empty or not.
Reviewed By: jvillard
Differential Revision: D5573379
fbshipit-source-id: e024a42
Summary: Useful for identifying user-controlled array accesses that could lead to buffer overflows
Reviewed By: mbouaziz
Differential Revision: D5520985
fbshipit-source-id: 92984f6
Summary:
When a sink name is specified in `.inferconfig` or in OCaml, it might conflict with a function of the same name that has a different number of args.
We shouldn't try to create a sink in this case, and we definitely shouldn't crash.
Reviewed By: jeremydubreil
Differential Revision: D5561216
fbshipit-source-id: fa1859b
Summary: This is unused, as far as I can tell. If we want to revive it, we can do it in AL or as a simple checker; it certainly doesn't require the full might of bi-abduction.
Reviewed By: jeremydubreil
Differential Revision: D5556325
fbshipit-source-id: e3895c2
Summary:
Replace `inferTraceBugs` with `infer-explore` with a similar CLI. Some options changed:
- --max-level -> --max-nesting, and "max" is the default value instead of a possible value
- --no-source -> --no-source-preview
Reviewed By: mbouaziz
Differential Revision: D5526651
fbshipit-source-id: 8383f37
Summary:
In some cases we normalize expressions to check some facts about them. In these
cases, trying to keep as much information as possible in the expression, such
as the fact it comes from a `sizeof()` expression, is not needed. Doing
destructive normalization allows us to replace `sizeof()` by its
statically-known value.
closes#706
Reviewed By: mbouaziz
Differential Revision: D5536685
fbshipit-source-id: cc3d731
Summary: A temporary workaround until we can understand why this happens and fix it.
Reviewed By: jeremydubreil
Differential Revision: D5559838
fbshipit-source-id: dc86eb9
Summary: That was too noisy. Propagate `--quiet` to the Python reporting hook so as to still emit bugs.txt and so on.
Reviewed By: martinoluca
Differential Revision: D5501106
fbshipit-source-id: 63b6451
Summary:
This allows the user to specify a different command to build the current version of the project vs to build the previous version of the project. Here's an example:
```
infer diff --gen-previous-build-command-script "echo clang -c hello.c" ... -- clang -c hello2.c
```
By default the two build commands are the same. If the script is to be used for both the current and the previous versions, then it's on the user to run it once first, eg:
```
infer diff --gen-previous-build-command-script "./myscript.sh previous" ... -- $(./myscript.sh current)
```
Reviewed By: martinoluca
Differential Revision: D5500989
fbshipit-source-id: 7374b44
Summary: Working on making CFG immutable by killing refs to functions that mutate them. This is an easy one because it doesn't do anything :).
Reviewed By: jeremydubreil, mbouaziz
Differential Revision: D5551521
fbshipit-source-id: bec76a9
Summary:
Record the list of access paths (if any) used in the index expression for each array access.
This will make it possible to use array accesses as sinks in Quandary
Reviewed By: jeremydubreil
Differential Revision: D5531356
fbshipit-source-id: 8204909
Summary:
Do not use the deprecated (and slower) `#infer` flavor. Instead, `infer-run`
runs capture with the `#infer-capture-all` flavor, followed by merging targets,
followed by the analysis.
Move the call to `MergeCapture` around to make this change easier.
Reviewed By: mbouaziz
Differential Revision: D5547199
fbshipit-source-id: 53c9996
Summary:
With current model, there are issues with cxx range loop. It looks like
it comes from std::vector::size model.
example of such FP:
```
int t = vec.size();
for(auto& elem : vec) {
auto x = elem
}
```
Reviewed By: jvillard
Differential Revision: D5545914
fbshipit-source-id: fbe55b3
Summary: Those are not particularly relevant for the biabduction analysis. It would be easy to have a dedicated checker for this if we happen to need one day.
Reviewed By: sblackshear
Differential Revision: D5530834
fbshipit-source-id: 316e60f
Summary:
The Eradicate `Nullable` checker should now be run using:
infer -a checkers --eradicate ...
Reviewed By: mbouaziz
Differential Revision: D5529226
fbshipit-source-id: 0de2956
Summary:
It's nice to have "raw" as the default kind of access path, since it's used much more often than the abstraction.
This is also a prereq for supporting index expressions in access paths, since we'll need mutual recursion between accesses and access paths.
Reviewed By: jeremydubreil
Differential Revision: D5529807
fbshipit-source-id: cb3f521
Summary:
This is unsound but will help the analysis to report less false alarms with the common pattern:
if (a.get() != null) {
a.get().foo();
}
Reviewed By: sblackshear
Differential Revision: D5528227
fbshipit-source-id: 750db4a
Summary:
Previously, only the bug type + file name (up to renaming) were taken into
account, which was too coarse. The key is file-independent and provides
additional signal.
Reviewed By: martinoluca
Differential Revision: D5536858
fbshipit-source-id: 70b732b
Sam Blackshear
Roy Li
Jules Villard
Martino Luca
Dulma Churchill
Daiva Naudziuniene
Jeremy Dubreil
Greg Nisbet
Jia Chen
Meng Zhang
Andrzej Kotulski
Alexander Slesarev