Summary:
This diff moves the implementation that considers the default value of
--models to be Config.models_jar if it exists from analyze.py to ZipLib.
Reviewed By: cristianoc
Differential Revision: D4100421
fbshipit-source-id: 322fbcf
Summary:
Previously, we recorded direct sinks as sinks and transitive sinks as passthroughs. This makes it difficult to create an expanded interprocedural trace when recording an error because we can't distinguish between sinks (which we want to expand) and passthroughs (which we don't). This diff changes recording of sinks so that a sink is now the *last* function in a trace to call a sink. To find out what the original sink was, the summary for the transitive sink in the trace will now need to be (recursively) expanded until we bottom out in the original sink.
Will do the same for sources in a follow-up diff.
Reviewed By: cristianoc
Differential Revision: D4103759
fbshipit-source-id: 6f435f5
Summary:
Needed to support upcoming diff(s) that change the nature of sources/sinks in a trace. Today they are the *original* source/sink, but in the future they will be the *transitive* source/sink (last procedure to return a source/call a sink).
This new convention will make the `returnAllSources`/`callAllSinks` form of these tests not so useful, since `returnAllSources`/`callAllSinks` will now show up as a single source/sink in the trace (at least without expanding the trace). By making these tests intraprocedural, we can make sure that we're still testing everything that we want to.
Reviewed By: cristianoc
Differential Revision: D4103754
fbshipit-source-id: 1733ecf
Summary:
This diff unifies the --specs-library and --zip-specs-library options,
delaying the point where their relative order gets lost to at least
after option parsing. This also moves the treatment of non-cached jar
libraries from Config to where they are used in ZipLib. The
implementation of expanding the cached jars is slightly simplified and
untangled from option parsing.
Reviewed By: jvillard
Differential Revision: D4100015
fbshipit-source-id: cf840a7
Summary: This is assumed everywhere, and so set it in `ClangWrapper` instead of `InferClang`
Reviewed By: jberdine
Differential Revision: D4095766
fbshipit-source-id: f77625e
Summary:
See code comment about `throw exn` being translated as `return exn`.
This problem was revealed by D4081279, which started grabbing access paths from exceptions.
Reviewed By: jvillard
Differential Revision: D4096391
fbshipit-source-id: 9d91513
Summary:
this makes frontends no longer depend on SymExec.ml. `ModelBuiltins` was split into two modules:
- `BuiltinDecl` with procnames for builtins (used to determine whether some function is a builtin)
- `BuiltinDefn` with implementations used by `SymExec`
- they both have similar type defined in `BUILTINS.S` which makes sure that new builtin gets added into both modules.
During the refactor I ran some scripts:
`BuiltinDecl.ml`:
let X = create_procname "X"
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,$4,"\42"$2"\42"} '
then manually confirm string match. Exceptions:
"__exit" -> "_exit"
"objc_cpp_throw" -> "__infer_objc_cpp_throw"
__objc_dictionary_literal
nsArray_arrayWithObjects
nsArray_arrayWithObjectsCount
`BuiltinDefn.ml`:
let X = Builtin.register BuiltinDecl.X execute_X
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,"Builtin.register BuiltinDecl."$2,"execute_"$2} '
then, fix all compilation problems
Reviewed By: jberdine
Differential Revision: D3951035
fbshipit-source-id: f059602
Summary: Doing `sychronized(A.class)` where `A` is an inner class was not previously recognized by the `GuardedBy` checker.
Reviewed By: peterogithub
Differential Revision: D4095094
fbshipit-source-id: c832f9e
Summary:
Now that it's possible to run clang wrapper as a function from another process,
Logging module cannot rely on `Config.current_exe` to determine which directory
it should write to.
Reviewed By: jeremydubreil
Differential Revision: D4095455
fbshipit-source-id: d989b06
Summary:
InferClang knows what to do if its name ends in ++. So it is not
necessary to pass whether or not the original clang executable ended in
++ to InferClang using the the INFER_XX environment variable. Instead,
create an InferClang++ symbolic link and make the clang wrapper call
either InferClang or InferClang++ as needed.
Reviewed By: jvillard
Differential Revision: D4078416
fbshipit-source-id: 3b5d5d0
Summary:
We issue a thread safety warning on a class not
marked ThreadSafe, when it has a super that is. This makes some sense. But,
it will be nice to remind that a super is so maeked, else the mesg could
seem out of context or surprising
Reviewed By: sblackshear
Differential Revision: D4075145
fbshipit-source-id: ebc2b83
Summary:
This diff revises the makefiles for java tests so that they are based on
the files actually produced and depended on, instead of the existing
imperative style. This is, I think, clearer and easier to modify, and
enables a little more parallelism.
Reviewed By: jvillard
Differential Revision: D4072560
fbshipit-source-id: c16d4bd
Summary: Now that InferClang is in ocaml there is nothing stopping us from exposing functionality of `InferClang` as a function in addition to binary
Reviewed By: jvillard
Differential Revision: D4081026
fbshipit-source-id: 86d500b
Summary:
Change command line options for dynamic dispatch to capture that the
alternatives are mutually exclusive.
Reviewed By: jeremydubreil
Differential Revision: D4074540
fbshipit-source-id: c329717
Summary: The lazy dynamic dispatch algorithm works by re-analyzing the generic methods with the more specialized types encountered during the symbolic execution. In order to do that, the analysis must access the procedure description of the method to reanalyze in order to run the analysis of the specialized procedure description on demand. This diff adds the procedure description on the summary as the summary are stored in the Buck cache and can easily be retrieved by procname.
Reviewed By: sblackshear
Differential Revision: D4077415
fbshipit-source-id: c2f1cc8
Summary:
- do a semantic analysis of each variable initializer to figure out if they need initialization
- add a flag to globals that is true when they are `constexpr`. In that case, no analysis is needed as the user + compile guarantee that it is a compile-time constant.
Reviewed By: sblackshear
Differential Revision: D4081273
fbshipit-source-id: 44dbe29
Summary:
1. `--version` never makes it to infer.py
2. `--project_root` should always be set by infer.ml invocation
3. there is no need to set `--project_root` to the same value again
Reviewed By: jberdine
Differential Revision: D4074227
fbshipit-source-id: c3e93ee
Summary:
Right now, taint gets lost if it flows into a constructor or procedure whose implementation is missing.
Since the core Java (e.g., String) and Android classes (e.g, Intent) are among these, this is bad.
We could handle this by writing a bunch of models instead, but that would be a lot of work (plus we may still miss cases).
Reviewed By: jvillard
Differential Revision: D4051591
fbshipit-source-id: 65851c8
Summary: For some reason, the frontend was always caching the name of the translated classes even when the `--dependencies` was not passed
Reviewed By: jberdine
Differential Revision: D4074225
fbshipit-source-id: 8aa2c79
Summary:
Merging the results directories of targets on buck projects involved creating symbolic links into buck-out.
The bulk of files are .attr files: one per procedure. Creating these links can be a bottleneck, and the merge phase can be slower than the analysis phases on projects with many procedures.
This diff introduces multilinks to speed up merge.
A multilink is a file `multilink.txt` containing a sequence of paths
```
path/to/file1.ext
path/to/file2.ext
...
```
A multilink file is a compact way to represent a link for each entry.
This diff creates a multilink file for each `attributes/dir` directory, instead of one symbolic link for each file.
Reviewed By: jberdine
Differential Revision: D4067428
fbshipit-source-id: 911f8a9
Summary: The frontend replaces global variables that are constant with their values as a quick hack to improve the precision of the analysis. This should apply to `constexpr` too.
Reviewed By: dulmarod
Differential Revision: D4058097
fbshipit-source-id: be4fea6
Summary: This diff simplifies the workflow of creating the procedure descriptions. Instead of creating the all procedure descriptions in a first step and translating the method bodies afterwards, it is simpler to translate to do the two in one step.
Reviewed By: cristianoc
Differential Revision: D4067674
fbshipit-source-id: be9e853
Summary: Doing like this makes it easier to keep the phony declarations in sync with the target definitions
Reviewed By: jvillard
Differential Revision: D4067679
fbshipit-source-id: 723bc0e
Summary:
In several places the tests were using whatever 'infer' executable was
found in PATH, instead of the one build from the source to be tested.
Reviewed By: jeremydubreil
Differential Revision: D4065019
fbshipit-source-id: 9b65099
Summary: Fix the resolution of symbolic links. The previous version did not work if the path itself was not a symbolic link, but there was a symbolic link somewhere up in the path tree. For example: `path/to/file` where `file` is not a symbolic link, but `to` is a symbolic link.
Reviewed By: jberdine
Differential Revision: D4062947
fbshipit-source-id: 394221d
Summary: Creating a "fake" procedure description the methods that are called is no longer required by the backend. So this diff cleans up the creation of the procedure descriptions
Reviewed By: jberdine
Differential Revision: D4057185
fbshipit-source-id: b444756
Summary: This code is an old experiement and has never really be used in prod because it was creating false positive. Dealing static final fields should be done in the backend instead so that it can used by the different languages C, Objective C, C++ and Java.
Reviewed By: jberdine
Differential Revision: D4055292
fbshipit-source-id: f1dc715
Summary:
Config.analyze_models, set by the INFER_ANALYZE_MODELS environment
variable, is redundant with Config.models_mode.
Reviewed By: jvillard
Differential Revision: D4047338
fbshipit-source-id: 4522d65
Summary:
Also be more careful when escaping arguments and create a module for shared
functionality between the clang frontend and the buck compilation database.
Reviewed By: jberdine
Differential Revision: D4036627
fbshipit-source-id: c981184
Summary: Some arguments passed from infer.ml to infer.py were only used to pass further to infer.ml invocations. Those args should be passed by env variable anyway (???)
Reviewed By: jberdine
Differential Revision: D4048003
fbshipit-source-id: 6f5fbeb
Summary:
Fix an issue where, when `-reactive` mode is used, files captured in the first second are not considered modified, and are not analyzed. This happens because file timestamps are used, and the resolution is one second.
Change the front-ends to change the timestamp of the directory where artifacts are created, so that the timestamps are 1 second in the future.
Small reactive commands such as the following now analyze correctly:
rm -rf infer-out && infer --reactive -- clang -c test.c
Reviewed By: jberdine
Differential Revision: D4050689
fbshipit-source-id: 6271860
Summary:
Move compilation database into separate module which loads said database from json file.
It will allow to load database from json file without calling buck.
Reviewed By: dulmarod
Differential Revision: D4049255
fbshipit-source-id: b2fa29f
Summary:
The integration would not work if other arguments were passed to Buck via infer
using Xbuck.
Reviewed By: akotulski
Differential Revision: D4044371
fbshipit-source-id: 742b5b3
Summary:
Declared and defined procedure attributes are now saved in different files (hashed_name.decl.attr and hashname.attr).
We always try to load using the filename of defined procedure attributes first,
and fall back to loading the file for declared ones if it does not exist.
The logic for replacing an existing file stays the same, with one extra thing:
when a file for a defined attribute is written, the one for the declared one
is deleted if it exists.
At the end of a capture, either a declared or a defined file exist, but not both.
The reason for this change is that when captures of different subprojects are
merged together, it can happen that a link gets created to a declared attributes
file even though a defined one exists, so the body of the procedure will not be analyzed.
After this diff, both links will be created, and the defined one will be loaded
by the back-end.
Reviewed By: dulmarod
Differential Revision: D4037423
fbshipit-source-id: 74fb7e6
Summary: failing to resolve was making the Java analysis to report errors with absolute paths instead of relative paths.
Reviewed By: sblackshear
Differential Revision: D4032764
fbshipit-source-id: e316193
Summary:
Python isn't needed anymore to pass options between `infer` and `InferClang`.
However, it is still needed to set up `PATH` so that we pick up compilation
commands.
Reviewed By: jberdine
Differential Revision: D4008469
fbshipit-source-id: 05c5716
Summary: This avoids issues where the command-line may get too large.
Reviewed By: jberdine
Differential Revision: D4008328
fbshipit-source-id: c1558b9
Summary:
This also adds `-a compile` support to `InferClang`. This is needed for the
`xcodebuild` integration, which is hard to fold into the same binary as the
rest.
Reviewed By: jberdine
Differential Revision: D4008262
fbshipit-source-id: 0bbd53f
Summary:
Checker for the Static Initialization Order Fiasco pattern:
https://isocpp.org/wiki/faq/ctors#static-init-order
1. Collect all globals (transitively) accessed in any given procedure.
2. Once the interprocedural analysis has finished, look at globals accessed in
initializers that do not belong to the current translation unit.
Reviewed By: sblackshear
Differential Revision: D3780266
fbshipit-source-id: 1d07161
Summary:
Create dummy functions representing the initializers of global variables. This
is so we can implement checks in the backend that can look at the initializer
expressions of global variables. We try not to create these dummy functions
when the initializer is not present, although for some reason we sometimes end
up with empty initializers.
Also add source file info to global variables in the backend (Pvar.re).
Reviewed By: sblackshear
Differential Revision: D3780238
fbshipit-source-id: 2dca87e
Summary:
There's no reason for infer to be in lib/ anymore, move it to the same place as
the other binaries. Thus all binaries are in the same directory and Config.ml
can better know where things are.
Reviewed By: jberdine
Differential Revision: D4015958
fbshipit-source-id: c5e851f
Summary: `tput cols` spams the terminal when it finds `$TERM` confusing. Reimplement what we need, which is very little, in C.
Reviewed By: jberdine
Differential Revision: D3960620
fbshipit-source-id: afe357e
Summary:
Before, if I wrote code like
```
x = src()
sink(x)
sink(x)
```
we would report three times instead of two.
The first flow would be double-reported.
Reviewed By: jeremydubreil
Differential Revision: D4024678
fbshipit-source-id: fcd5b30
Summary: when a method has writes to a field outside of synchrnoization, issue an appropriate error message identifying the fields
Reviewed By: sblackshear
Differential Revision: D4015612
fbshipit-source-id: 4f697fc
Summary:
This diff adds a make target to generate interface files from
implementation files. These generated interface files can then be used
as a starting point for documenting and restricting the exposed module
interface. For example, to generate an interface for JavaTaintAnalysis.ml,
execute:
```
make -C infer/src M=quandary/JavaTaintAnalysis mli
```
Note that this relies on `ocamlc -i`, which for reason currently
produces syntactically ill-formed files.
Reviewed By: sblackshear, jvillard
Differential Revision: D3998175
fbshipit-source-id: f653737
Summary: Also make sure it's not dead code, so we don't break it again by accident.
Reviewed By: jeremydubreil
Differential Revision: D4015793
fbshipit-source-id: 017d862
Summary:
During the development/debugging of AST checks, it will be possible to emit dotty graphs with a representation of the evaluation of formulas.
The formulas, expressed using the notation of CTL (https://en.wikipedia.org/wiki/Computation_tree_logic) are represented in a graph alongside the current ast-node and their final evaluation result (green for true, red for false)
To get the dotty graph, run infer with the `--debug` flag
Reviewed By: ddino
Differential Revision: D3937787
fbshipit-source-id: 163e17d
Summary: Avoid polluting stdout and stderr for executables that are always supposed to log into files.
Reviewed By: dulmarod
Differential Revision: D4008888
fbshipit-source-id: 1366498
Summary: Nothing mutates those fields so there is no need to make them `mutable`
Reviewed By: cristianoc
Differential Revision: D4009166
fbshipit-source-id: b840a4b
Summary:
It's not necessary if compiling tests in infer environemnt. It may be required if compiling some C++ tests
without infer. `infer/tests/codetoanalyze/cpp/shared/attributes/depracated_hack.cpp` is one of them
Reviewed By: cristianoc
Differential Revision: D4008850
fbshipit-source-id: 5d94bdf
Summary:
This fixes a perf issue on large files, where a copy of the type environment and control flow graph were loaded for each procedure analyzed in the file.
If the type environment or the control flow graph are big, and the file contains many procedures, this can cause a big memory overhead.
Reviewed By: jvillard
Differential Revision: D4008655
fbshipit-source-id: 11d07c1
Summary:
This changes executions of the former InferClang into a function call. In
particular, it can be called several times per execution.
The new InferClang must be called as if it was clang, and knows how to run
clang with our plugin to get the AST of the source file.
Reviewed By: akotulski
Differential Revision: D3981017
fbshipit-source-id: 7af6490
Summary:
This diff removes the unused support for reporting props, which enables
refactoring so that the 'base' directory has no dependencies, and the
'IR' directory depends only on 'base'.
Reviewed By: jvillard
Differential Revision: D3981352
fbshipit-source-id: 3700a23
Summary:
Color modules in dependency graph based on directory, and cluster
modules together into a subgraph if their directory is listed in the
`clusters` variable of infer/src/Makefile.
Reviewed By: akotulski
Differential Revision: D3979253
fbshipit-source-id: dffd76b
Summary: Infer should always include the version of the Java compiler as part of the target key used by Buck
Reviewed By: jvillard
Differential Revision: D3989649
fbshipit-source-id: 605ab2f
Summary: Introduce `--enable-ocamlopt-custom-cc` configure flag (disabled by default). Normally it doesn't have to be set. However, when cross-compiling infer itself for another platform it may have to be set.
Reviewed By: jberdine
Differential Revision: D3995032
fbshipit-source-id: ce2fd72
Summary: it seems to have no effect on analysis. As such it should be ok to add cg nodes for builtin model calls
Reviewed By: jberdine
Differential Revision: D3967399
fbshipit-source-id: 06c32e5
Summary:
This changes the algorithm for pure join to keep the constraints that,
after normalization, occur in both arguments. Previously pure join
would normalize, filter, and then union the constraints of the
arguments.
Reviewed By: sblackshear
Differential Revision: D3970394
fbshipit-source-id: 3dc1672
Summary:
Add a test case for a problem peterogithub uncovered with join of
attributes. The expected result is currently incorrect, to be fixed
later.
Reviewed By: sblackshear
Differential Revision: D3970363
fbshipit-source-id: 077705d
Cristiano Calcagno
Josh Berdine
Sam Blackshear
Peter O'Hearn
Andrzej Kotulski
Yunxing Dai
Jules Villard
Dino Distefano
Dulma Churchill
Ryan Rhee
Jeremy Dubreil
Martino Luca