Summary:
A good first step in order to run multiple checkers together is to prevent the analysis the analysis to side effect on the summaries of the method being analyzed from disk, or the shared specs summary. The idea is that `Ondemand` creates a summary for the procedure being analyzed and only saves the summary once all the checkers have been run. The summary for the caller (i.e. the procedure being analyzed) should never be looked up from disk during the analysis. In other words, the analysis should only ever lookup the summaries of the callees and the proposed solution to enforce this is to have `Ondemand.analyze_proc_name` be the only way to lookup the summary of a procedure.
Another objective is to make sure that the summaries are never saved to disk more than once.
Reviewed By: sblackshear
Differential Revision: D4549764
fbshipit-source-id: f0a6e21
Summary:
We waste a lot of space storing the types of field accesses and comparing them sets/maps with access paths.
Yet almost none of the code ever looks at these types (only a tiny piece of code in thread-safety).
If we know the base type, we have enough information to recover the type of the field.
Let's do that instead.
Reviewed By: jeremydubreil
Differential Revision: D4567996
fbshipit-source-id: e7fd2da
Summary:
This simplifies a bit the code to run the analysis on all the prcedures in the cluster. Before, the functions procedure_should_be_analyzed, which loads the attributes, and get_proc_desc were called twice for the analysis of every procedure.
The objective is to remove the calls to procedure_should_be_analyzed and hide it from the ondemand API since it is already called before the analysis of every procedure.
Reviewed By: sblackshear
Differential Revision: D4553397
fbshipit-source-id: 02cffaf
Summary: In C++ there are types that contain `<>` in their names (templates). When printing type to `html` those should be escaped
Reviewed By: jeremydubreil
Differential Revision: D4572506
fbshipit-source-id: a180537
Summary:
One gets very obscure errors when trying to run infer for clang when it was
compiled for Java, or vice-versa. This diff makes sure we crash early with the
appropriate error message. For instance:
```
$ ./build-infer java
$ infer -- clang -c hello.c
Uncaught exception:
(Failure
"Unsupported build mode: make/cc\
\nInfer was built with clang analyzers disabled.\
\nPlease rebuild infer with clang enabled.\
\n")
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "backend/infer.ml", line 398, characters 6-48
Called from file "backend/infer.ml", line 449, characters 20-38
$ infer --clang-compilation-db-files foo.json
Uncaught exception:
(Failure
"Unsupported build mode: clang compilation database\
\nInfer was built with clang analyzers disabled.\
\nPlease rebuild infer with clang enabled.\
\n")
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "backend/infer.ml", line 392, characters 8-65
Called from file "backend/infer.ml", line 449, characters 20-38
```
Reviewed By: sblackshear
Differential Revision: D4566641
fbshipit-source-id: d9a118f
Summary:
- inferbo introduced a dependency to extlib. When building Java analyzers, this
is implicitly pulled in by javalib, but it's missing when building only the
clang analyzers. Add `extlib` to the packages we build against.
- infer.ml and Javac.ml depend on Javalib, but it's easy to push down the code
that needs it to `jMain.ml` so that we can build without javalib for the
clang-only case.
- jMain.mli had 2 copies: one in java/ and one in java_stubs/. Make one a symlink to the other.
Reviewed By: jeremydubreil
Differential Revision: D4566581
fbshipit-source-id: 214a4eb
Summary:
Sevel auxiliary files made it to the output directory of the analysis of individual targets when analyzing Java projects build with Buck. However, these files are then taken into account= to compute the target rule key and then to decide whether to analyze the dependent targets. Since these auxiliary files were containing time sentive information, every cach miss on a given target would then invalitate the cache entries for all the dependent targets.
This diff cleans up the output directory to only keep the specs files, the `global.tenv` and the `report.json` files which are the only artifacts needed to analyze the dependent targets
This diff makes a minimal number of changes to see how it behaves in prod, but I intend to refoctor this more when continuing to add support for running Infer with genrules
Reviewed By: sblackshear
Differential Revision: D4562615
fbshipit-source-id: 4628420
Summary:
Xcode's compilation databases follows a different convention than cmake's and
escape the `"file"` and `"dir"` fields of each unit to make them shell-ready.
We need to treat them differently when reading them.
This adds a new `--clang-compilation-db-files-escaped` option and makes the
code related to reading compilation databases deal correctly with both
conventions.
Reviewed By: akotulski
Differential Revision: D4559239
fbshipit-source-id: 51120ae
Summary: Some compilation databases give relatives paths for the `"file"` field. This is not ambiguous as there is also a `"dir"` field, so use that to make the path absolute when needed.
Reviewed By: dulmarod
Differential Revision: D4559145
fbshipit-source-id: be36a16
Summary:
This avoids spurious warnings on projects using gcc with optimization flags
that are ignored by clang.
Reviewed By: akotulski
Differential Revision: D4559326
fbshipit-source-id: 14a2431
Summary: Should stop us from reporting on benign races of fields that are caching resources.
Reviewed By: peterogithub
Differential Revision: D4538037
fbshipit-source-id: 15236b4
Summary:
It seems that the `close()` method that should normally be called on an object `obj` of type `java.io.Closeable` is sometimes called on `obj` of type `java.lang.Object`. It did not fully understand in which case this happens but it could be coming from a bug in Sawja since the type of `obj` in the bytecode is correct, but the Sawja reciever expression given to the Java frontend has the type `java.lang.Object`.
In any case, it does not hurt to always consider that `obj.close()` will replace the `FILE` attribute on `obj` by a `MEM` attribute.
Reviewed By: sblackshear
Differential Revision: D4540627
fbshipit-source-id: 71f9c95
Summary:
This reorganises the contents of `infer --help`:
- Headings are more prominent (start with `**`)
- New "Java" section
- Delete "Analysis" section, distribute contents over other sections
- New "Quandary" section
- Under the hood, new "Buffer Overruns" and "Crashcontext" sections, but do not show them as we don't expect external use yet, although that may be a bit arbitrary
- typo: `--bufferoverrn` -> `--bufferoverrun`
- move some options from one section to another
Reviewed By: jberdine
Differential Revision: D4537500
fbshipit-source-id: a789375
Summary:
Native compilation seems to take a couple of seconds to build the unit test
binary, but we don't need it to be native (and neither do users building infer
to install it on their machines). In fact, the test mode rebuilds it in
bytecode mode. For the sake of being able to run the unit tests when developing
on infer (and thus possibly while having some fatal warnings showing up in the
code, preventing us from building the test target), also build InferUnit in
bytecode mode.
Reviewed By: sblackshear, martinoluca
Differential Revision: D4537455
fbshipit-source-id: 374c84c
Summary: In some cases where a function is called directly on a formal (e.g, `def foo(o) { callSomething(o) }`, we were failing to propagate the footprint trace to the caller.
Reviewed By: jeremydubreil
Differential Revision: D4502404
fbshipit-source-id: d4d632f
Summary: This will be important for maintaining ownership of `View`'s, which involve a lot of casting.
Reviewed By: peterogithub
Differential Revision: D4520441
fbshipit-source-id: fdef226
Summary:
Previously, we would lose track of ownership in code like
```
Obj owned = new Obj();
Obj stillOwned = id(owned); // would lose ownership here
stillOwned.f = ... // would report false alarm here
```
This diff partially addresses the problem by adding a notion of "unconditional" (always owned) or "conditional" (owned if some formal at index i is owned) ownership.
Now we can handle simple examples like the one above.
I say "partially" because we still can't handle cases where there are different reasons for conditional ownership, such as
```
oneOrTwo(Obj o1, Obj o2) { if (*) return o1; else return o2; } // we won't understand that this maintains ownership if both formals are owned
Obj stillOwned = oneOrTwo(owned1, owned2);
stillOwned.f = ... // we'll report a false alarm here
```
This can be addressed in the future, but will require slightly more work
Reviewed By: peterogithub
Differential Revision: D4520069
fbshipit-source-id: 99c7418
Summary: This will make it a cinch to track new "attributes" of memory locations, and to propagate more complex attributes such as conditional ownership (coming in a future diff).
Reviewed By: peterogithub
Differential Revision: D4523143
fbshipit-source-id: 57aa133
Summary: This fixes a wrong level of indirection when performing the type substitution.
Reviewed By: sblackshear
Differential Revision: D4521008
fbshipit-source-id: 7324ea6
Summary: Being forced to separately define `pp_element`/`pp_key` is uneccessary and makes it more cumbersome to create a set/map from an existing module that already defines `pp`.
Reviewed By: jeremydubreil
Differential Revision: D4517308
fbshipit-source-id: 9b17c9c
Summary: This method can return `null` if the parameter is not a supported system service. However, since this method tends to be called with a constant value as parameter, it does seem to be returning null often in practice.
Reviewed By: sblackshear
Differential Revision: D4509185
fbshipit-source-id: 4cb80ce
Summary:
At one point I thought we'd want to have lots of different schedulers for things like exploring loops in different orders, but that hasn't materialized.
Let's make the common use-case simpler by hiding the `Scheduler` parameter inside the `AbstractInterpreter` module.
We can always expose `MakeWithScheduler` later if we want to.
Reviewed By: jberdine
Differential Revision: D4508095
fbshipit-source-id: 726e051
Summary:
This fixes false positives we had in fields written by callees of a constructor (see new E2E test).
This is also a bit cleaner than what we did before; instead of special-casing constructors, we just use the existing ownership concept.
Reviewed By: peterogithub
Differential Revision: D4505161
fbshipit-source-id: a739ebc
Summary:
Constants are always "owned" in the sense that no one can mutate them.
In code like
```
Obj getX(boolean b) {
if (b) {
return null;
}
return new Obj();
}
```
, we need to understand this in order to infer that the returned value is owned.
This should fix a few FP's that I've seen.
Reviewed By: peterogithub
Differential Revision: D4485452
fbshipit-source-id: beae15b
Summary:
Propagating the arguments read in .inferconfig shouldn't be necessary as they
are parsed by each executable. There are corner cases where I think this diff
could change the behaviour of infer (eg, .inferconfig redefines project-root
and subsequent exes read a different .inferconfig thanks to the project-root in
INFER_ARGS), but I don't think there are good use cases like that.
Reviewed By: jberdine
Differential Revision: D4475092
fbshipit-source-id: 5c020d0
Summary:
Clients should use `Config.parse_action` instead to figure in what mode they
are operating.
In particular, the biggest change is in logging. Take the `parse_action` into
account instead of the exe, and change the log/ subdirectories to be "capture",
"driver", "analyze", and "print", corresponding to the various phases of an
infer run.
Reviewed By: jberdine
Differential Revision: D4474943
fbshipit-source-id: 6d33ad3
Summary:
Support several parsing modes: Infer, Javac, NoParse
The "Infer" mode specifies a list of sections, ie the parts of infer that are affected by an option (corresponds to the old notion of "exes"):
analysis, clang frontend, print, ...
- .inferconfig and INFER_ARGS always parsed
- outside .inferconfig and INFER_ARGS, do not parse subcommand arguments before the subcommand has been activated
- command-line is parsed or not based on the subcommand/executable selected
- executable dictates subcommand, so almost nothing depends on the executable outside of Config. Another diff will restrict the API around exes to reflect this.
Reviewed By: jberdine
Differential Revision: D4474886
fbshipit-source-id: 442dfef
Dulma Churchill
Jeremy Dubreil
Sam Blackshear
Andrzej Kotulski
Jules Villard
Cristiano Calcagno
Dino Distefano