Summary: For performance critical sections of the code, this checker detects memory allocations or calls to methods annotated as expensive. However, such cases of memory allocations or expensive calls are acceptable is occuring in rare cases. This diff adds supports for the "unlikely" branch prediction method and does not track expensive calls in unlikely branches.
Reviewed By: sblackshear
Differential Revision: D3193473
fb-gh-sync-id: ea87e49
fbshipit-source-id: ea87e49
Summary:InferPrint has a special case code path that does not add results_dir to
the specs_library if it is the default. This seems to be unnecessary.
Reviewed By: jeremydubreil
Differential Revision: D3195088
fb-gh-sync-id: 67e968a
fbshipit-source-id: 67e968a
Summary:BinaryConditionalOperator should evaluate condition expression once, but we used to evaluate it twice.
Fix translation to account for it.
Reviewed By: dulmarod
Differential Revision: D3179803
fb-gh-sync-id: a801a7e
fbshipit-source-id: a801a7e
Summary:Improve the error traces so that:
- the error get reported on the first offending call, which is more intuitive for inline comments
- the traces now jump from call location to callee definition and so forth until the end of the call stack
Reviewed By: sblackshear
Differential Revision: D3183756
fb-gh-sync-id: 089ddaf
fbshipit-source-id: 089ddaf
Summary:This diff translate cpp lambdas. For the moment it does not take care of
captured variables. Captured variables will come in the next diff.
Reviewed By: dulmarod
Differential Revision: D3114790
fb-gh-sync-id: bf36450
fbshipit-source-id: bf36450
Summary:Make node ids be `private int` to make sure we don't mix them with random
integers from other sources.
Reviewed By: sblackshear, cristianoc
Differential Revision: D3179670
fb-gh-sync-id: 4bcf4f0
fbshipit-source-id: 4bcf4f0
Summary:This wasn't used anywhere. Frontends that wish to do something like goto can
just set the targets of the goto as successors of the current node, no need for
a special instruction to do that.
Reviewed By: sblackshear
Differential Revision: D3179826
fb-gh-sync-id: 572a6f2
fbshipit-source-id: 572a6f2
Summary:public
When a conditional is the last instruction, there will be a join node leading directly to the exit node.
Some instructions, such as nullification of dead variables, and abstraction, are added to the control flow graph automatically. But, join nodes cannot contain instructions. So when a procedure ends with a conditional, there might be no place to store these instructions.
This diff adds one extra node between the join and the exit node in that situation.
Reviewed By: jvillard
Differential Revision: D3179056
fb-gh-sync-id: 2b9cd7e
fbshipit-source-id: 2b9cd7e
Summary:public
This extends infer/src/Makefile with a mod_dep.dot target that builds a
dot graph of module dependencies.
This also adds ocamldot, which is in the public domain and available
from http://trevorjim.com/projects/ocamldot/ocamldot.tar .
Reviewed By: cristianoc
Differential Revision: D3168488
fb-gh-sync-id: 267fb0e
fbshipit-source-id: 267fb0e
Summary:public
The code:
DataInputStream in = new DataInputStream(new BufferedInputStream(new FileInputStream(file)));
creates a resource with `FileInputStream()` and wraps it twice as a field of `BufferedInputStream` and then as a field of `DataInputStream`. Then calling:
in.close();
needs to go down the wrappers hierachy: `DataInputStream.close()` -> `FilterInputStream.close()` which then calls `BufferedInputStream.close()` -> `FilterInputStream.close()` -> `FileInputStream.close()`.
Going down the wrapper was not working before because `FilterInputStream.close()` was only going further when the type of field `in` was `FileInputStream` wheras it should also continue when the type of the field is any subtype of `FilterInputStream`, e.g. `DataInputStream` and `BufferedInputStream` like in the test example. This diff fixes this last aspect.
Reviewed By: sblackshear
Differential Revision: D3174822
fb-gh-sync-id: 3adbb7e
fbshipit-source-id: 3adbb7e
Summary:public
Report statistics on consumed time and memory in results_dir/perf_stats.json.
Reviewed By: martinoluca
Differential Revision: D3162381
fb-gh-sync-id: e802faa
fbshipit-source-id: e802faa
Summary:public
Instead of translating code from headers blindly, translate only gets transitively referenced from source code.
It won't translate functions from system headers, but in the future we could do that as well
since most of them aren't used and it shouldn't add much overhead.
For now this functionality is hidden behind --cxx-experimental flag
Reviewed By: dulmarod
Differential Revision: D3163519
fb-gh-sync-id: 0c53b10
fbshipit-source-id: 0c53b10
Summary:public
Refactor Utils.SymOp into a separate module, bringing the failure_kind
type and associated operations.
Reviewed By: cristianoc
Differential Revision: D3161640
fb-gh-sync-id: be3d7c9
fbshipit-source-id: be3d7c9
Summary:public
Eliminate the use of the -open Utils command line option passed to the compiler in favor of `open! Utils` in each source file. While slightly convenient, this option causes more headaches than it is worth with other tools e.g. merlin.
Reviewed By: jvillard
Differential Revision: D3168193
fb-gh-sync-id: 4285ef6
fbshipit-source-id: 4285ef6
Summary:public
This will allow us to run translation of more than one function at the same time.
Reviewed By: dulmarod
Differential Revision: D3167965
fb-gh-sync-id: 41e9935
fbshipit-source-id: 41e9935
Summary:public
Also build checkcopyright in the byte code test build.
Reviewed By: martinoluca
Differential Revision: D3161885
fb-gh-sync-id: cf07a59
fbshipit-source-id: cf07a59
Summary:public
This information is no longer needed - ASTExporter always exports pointer to parent for C++/objC methods.
This code is from time it was not true.
Reviewed By: jvillard
Differential Revision: D3162455
fb-gh-sync-id: 35570da
fbshipit-source-id: 35570da
Summary:public
Refactor the ml_loc type and associated operations from Utils to Logging. Seems a better fit, and reduces dependencies.
Reviewed By: cristianoc
Differential Revision: D3161440
fb-gh-sync-id: 2e09c25
fbshipit-source-id: 2e09c25
Summary:public
Instead of using location of init_stmt, use location of variable when translating initialization.
Most of the time it change anything with some exceptions:
// example1 - C/C++/objC
int x = // now: assignment happens in this line
3; // past: assignment happens in this line
// example2: valid in C++11 only
struct X {
int x = 0; // now: one assignment here
int y = 2; // now: one assigmnent here
X() = default; // before: 2 assignments in this line
};
Reviewed By: dulmarod
Differential Revision: D3155870
fb-gh-sync-id: f38c78c
fbshipit-source-id: f38c78c
Summary:public
The merge option -m would link every file in a captured results dir.
This includes the .start file, which would compromise the subsequent checks for modified files during reactive analysis.
Now only link files inside directories inside the results dir (don't link any files in the first 2 levels).
Reviewed By: jberdine
Differential Revision: D3155819
fb-gh-sync-id: 8ad180f
fbshipit-source-id: 8ad180f
Summary:public
This may be unnecessary, but I found stale files while debugging and had to ask if they were the problem.
Reviewed By: jvillard
Differential Revision: D3130087
fb-gh-sync-id: d3222c3
fbshipit-source-id: d3222c3
Summary:public
Add modeling of methods that can raise exceptions when parameters are
nil, and that return nil when passed nil.
Reviewed By: dulmarod
Differential Revision: D3101739
fb-gh-sync-id: 76af5a2
fbshipit-source-id: 76af5a2
Summary:public
Use getconf to compute NCPU as it is uniform across platforms.
Use result in several places to avoid fork bombs. I routinely see
errors about fork running out of memory when building e.g. the clang
plugin.
Reviewed By: jvillard
Differential Revision: D3148970
fb-gh-sync-id: 6d071c9
fbshipit-source-id: 6d071c9
Summary:public
Remove option to filter source files from being analysed from clang wrapper.
The option is unused and there should be better mechanism to do so if we need it.
This will slightly simplify the script and allow to analyze files that are from
outside of "blessed" extensions (such as .cxx or .hpp)
Reviewed By: dulmarod
Differential Revision: D3126330
fb-gh-sync-id: 1628913
fbshipit-source-id: 1628913
Summary:public
clang-format changed filename inside __has_include(<FILENAME>), turn off
clang format for that part of the code.
Reviewed By: jberdine
Differential Revision: D3133593
fb-gh-sync-id: c601514
fbshipit-source-id: c601514
Summary:public
In order to make infer more resiliant to compilation failure,
make static_assert to do nothing.
As a bonus, set _FORTIFY_SOURCE inside same file instead of command line
Reviewed By: jvillard
Differential Revision: D3133446
fb-gh-sync-id: 590f4ad
fbshipit-source-id: 590f4ad
Summary:public
Will be needed later to avoid circular dependencies between dom.ml and upcoming
numericalDomain.ml.
Reviewed By: jberdine
Differential Revision: D3126697
fb-gh-sync-id: 678d49f
fbshipit-source-id: 678d49f
Summary:public
Models in headers are purely C++ concept and it's
useless if C++ mode is turned off. Since those
models can lead to compilation errors, turn them
off for non-C++ analysis
Reviewed By: martinoluca
Differential Revision: D3126294
fb-gh-sync-id: 0912e7b
fbshipit-source-id: 0912e7b
Summary:public
This fixes the compilation of Infer from a path containing symbolic links.
Reviewed By: jberdine
Differential Revision: D3123244
fb-gh-sync-id: 09dbd13
fbshipit-source-id: 09dbd13
Summary:public
1. Make detection of libc++/stdlibc++ headers more robust
2. Turn on c++11 only for newer versions of stdlibc++
Reviewed By: jvillard
Differential Revision: D3121187
fb-gh-sync-id: c2e5be5
fbshipit-source-id: c2e5be5
Summary:public
It could happen that the modification times of symbolic links and
original files checked by reactive mode could be exactly the same. In
this case, some files would perpetually be re-analyzed.
This diff creates symlinks and sets their accessed and modified times
to 1 second in the future so that strict timestamp checking is robust.
Reviewed By: cristianoc
Differential Revision: D3098451
fb-gh-sync-id: 3724468
fbshipit-source-id: 3724468
Summary:public It's useful for the transfer functions to understand what the current procedure is. Applications include debugging, implementing context-sensitivity, asking which program variables are parameters, and the list goes on.
In the future, we'll almost certainly want to pass the tenv to the transfer functions as well.
Reviewed By: jberdine
Differential Revision: D3104997
fb-gh-sync-id: 1c0df8f
fbshipit-source-id: 1c0df8f
Summary:public
This create `make install` and `make uninstall` targets that can be used to
install Infer on a system. All the files needed are installed under
"/usr/local/lib/infer" (by default, but can be configured with ./configure
flags as usual), pretty much like their git infer/ counterparts. Moreover,
"infer" and "inferTraceBugs" are installed in /usr/local/bin (similarly
configurable).
As a bonus, `opam install infer` and `opam remove infer` now work. To use
these, it's better to pin the git repo with "-k git":
cd ~/infer/ # where the repo is
opam pin add -k git --yes infer .
The reason is that otherwise, and only if the repo is not clean, opam will
convert symlinks into regular files, which is not good (compilation will fail).
Reviewed By: jberdine
Differential Revision: D3109337
fb-gh-sync-id: 96c9fd1
fbshipit-source-id: 96c9fd1
Summary:public
This is needed to have a working `opam install infer`. Actual working `opam
install infer` in a follow-up diff.
Reviewed By: jberdine
Differential Revision: D3109308
fb-gh-sync-id: 49d7276
fbshipit-source-id: 49d7276
Summary:public
Simplifies the way to configure cmake to run infer's fake compiler commands.
Instead of `CC=/path/to/infer/infer/lib/capture/clang cmake .`, which is what
is advised on #25 and is now outdated because the paths to infer's clang has
changed since, simply run `infer -- cmake .`. The only caveat is that infer
tries to analyze the end result, and prints "No issues found". This could be
fixed later.
Reviewed By: jeremydubreil
Differential Revision: D3093162
fb-gh-sync-id: 99df50a
fbshipit-source-id: 99df50a
Summary:public
Rename functions and arguments to be more uniform, and change several to simplify types by using Builtin.t.
Reviewed By: cristianoc
Differential Revision: D3107836
fb-gh-sync-id: 8445f79
fbshipit-source-id: 8445f79
Summary:public
Allow the use of `infer -- ./configure`. This can be useful if the full path to
the compiler is recorded by the `./configure` command. That is the case for the
samba source tree for instance (because `./configure` calls `waf configure`
under the hood).
Reviewed By: jeremydubreil
Differential Revision: D3093065
fb-gh-sync-id: 2663418
fbshipit-source-id: 2663418
Summary:public
This will allow SymExec to depend on Inferconfig with introducing
circular dependencies, as Inferconfig calls Builtin.is_registered.
Reviewed By: jeremydubreil
Differential Revision: D3100614
fb-gh-sync-id: 786cf62
fbshipit-source-id: 786cf62
Summary:public
To ensure that e.g. Config.results_dir is not used before being set.
Reviewed By: cristianoc
Differential Revision: D3102724
fb-gh-sync-id: ced0974
fbshipit-source-id: ced0974
Summary:public
Eradicate need the procedure attributes for callees.
It relies on the java front-end to create proc descs for callees that are declared but not defined.
This diff remove that needs, and when a callee without prodedure attributes is found, it creates one on the fly. The attribute created is similar to what the Java front-end would do, except
that the number and types of arguments are part of the call instruction, so they can
be used to create the formal parameters.
Reviewed By: jeremydubreil
Differential Revision: D3073904
fb-gh-sync-id: 381ff67
fbshipit-source-id: 381ff67
Summary:public
Allow the value of the INFER_ONDEMAND_FILE environment variable to be
either an absolute path, or relative to the project root.
Likewise, allow the entries in the file determined by
INFER_ONDEMAND_FILE to be either absolute or relative to the project
root. Note, however, that if they are absolute but not under the
project root, they will not be found.
Reviewed By: cristianoc
Differential Revision: D3098489
fb-gh-sync-id: e861300
fbshipit-source-id: e861300
Summary:public
In Python 2, `shutil.rmtree()`, `os.walk()`, `os.path.join()`, etc. are not
happy when the locale cannot decode the filenames they have to deal with.
Decrease the likelihood of this happening by making the file names generated by
infer ascii-only.
Also ignore character decoding errors optimistically when reading the json
report file.
Add tests that we are able to run the analysis and report the bug on a function
with a utf8 name, and that we are able to remove the previous results
directory.
closes#287
Reviewed By: cristianoc
Differential Revision: D3058858
fb-gh-sync-id: b88cd35
shipit-source-id: b88cd35
Summary:public
see the file for some example usage
Reviewed By: sblackshear, jeremydubreil
Differential Revision: D3058440
fb-gh-sync-id: c891dfe
shipit-source-id: c891dfe
Summary:public
D2987288 introduced a regression where usage messages were no longer printed, and instead exceptions went uncaught.
Reviewed By: jeremydubreil
Differential Revision: D3089620
fb-gh-sync-id: 1cca0c6
shipit-source-id: 1cca0c6
Summary:public
It seems that creating the procedure description of the callees this should no longer be useful to run the checkers
Reviewed By: sblackshear
Differential Revision: D3083523
fb-gh-sync-id: 040b104
shipit-source-id: 040b104
Summary:public
The "fake" procedure description of the callees, containing info about the formal parameters, is current used by Eradicate. This diff forces the creation of the callee procedure descriptions when running Infer with Buck.
Reviewed By: sblackshear
Differential Revision: D3083452
fb-gh-sync-id: 24a70e6
shipit-source-id: 24a70e6
Summary:public
It seems that the support for using the Buck cache with Infer has been brocken for a while.
Reviewed By: sblackshear
Differential Revision: D3079493
fb-gh-sync-id: fd92d1c
shipit-source-id: fd92d1c
Summary:public
Conversion constructor of unique_ptr should be explicit. Fix it.
Reviewed By: cristianoc
Differential Revision: D3075661
fb-gh-sync-id: e911d8c
shipit-source-id: e911d8c
Summary:public
The option -merge_captured specifies that this is merging the results of capture
using the buck integration. The file specifying the targets is read from `infer-out/infer-deps.txt`.
Each dependency specifies a path in buck-out for one target:
where the results directory after capture is.
The option triggers a merge of the results directories into infer-out.
The merge consists in making a virtual copy, where each file in a
target in `buck-out` gets virtually copied into infer-out by making
one symbolic link per file.
There is a mechanism to detect when the capture of a target has already
been copied: when each source file already exists at the destination.
There's also an option `-modified_targets modified_targets.txt`.
If a target is listed in `modified_targets.txt`, this will force a new creation of links
for that target, whether those links exist or not.
Reviewed By: martinoluca
Differential Revision: D3070318
fb-gh-sync-id: 6d2e7a5
shipit-source-id: 6d2e7a5
Summary:public
TOgether with compiling Infer in debug mode, this allows to get exceptions stack traces when Infer fails
Reviewed By: sblackshear
Differential Revision: D2899992
fb-gh-sync-id: 55b4d3d
shipit-source-id: 55b4d3d
Summary:public
Create a model of std::unique_ptr in similar fashion to what was done to std::shared_ptr.
For now, we are modeling it as container of raw pointer (no ownership concept).
This time unique_ptr is not derived from std__unique_ptr (unlike shared_ptr, it was easier to not do that) and so we need to provide implementations for all non-member functions per C++ reference:
http://en.cppreference.com/w/cpp/memory/unique_ptr
Reviewed By: dulmarod
Differential Revision: D3048209
fb-gh-sync-id: a9a6455
shipit-source-id: a9a6455
Summary:public
Whenever infer-deps.txt and report.json files are encountered after the analysis with Buck
they will be automatically merged and deduplicated with all the other files of the same kind.
This change also emits the results of the analysis to stdout.
Reviewed By: jvillard
Differential Revision: D3064487
fb-gh-sync-id: 3599fba
shipit-source-id: 3599fba
Summary:public
Before this diff, the Java frontend was not adding the definition of the inherited interfaces to the type environment, thus failing to answer questions like "does type X implements Closeable". Infer was therefore missing to detect resource leaks when the resource was indirectly implementing Closeable via an intermediate interface.
Reviewed By: sblackshear
Differential Revision: D3067555
fb-gh-sync-id: 86d0760
shipit-source-id: 86d0760
Summary: public Like the pre-analysis, these should be called for every CFG. This is a stepping stone toward getting rid of remove_tmps and making it part of the liveness analysis.
Reviewed By: jvillard
Differential Revision: D3059021
fb-gh-sync-id: 3a8d818
shipit-source-id: 3a8d818
Summary:public
Implementation of std::move is straightforward and infer understands it without
any problems. To use it, we translate it even though it's coming from system headers.
Reviewed By: jvillard
Differential Revision: D3064019
fb-gh-sync-id: 823ae75
shipit-source-id: 823ae75
Summary:public
This give more freedom to use the tools, especially in the open-source context.
Reviewed By: cristianoc
Differential Revision: D3061192
fb-gh-sync-id: 0e0d4ed
shipit-source-id: 0e0d4ed
Summary:public
Generalize command line option parsing to query an environment variable
for args, and then parse the environment and command line arguments.
Each executable uses a distinct environment variable:
- InferAnalyze: INFER_ARGS
- InferJava: INFERJAVA_ARGS
- InferClang: INFERCLANG_ARGS
- InferLLVM: INFERLLVM_ARGS
- checkCopyright: CHECKCOPYRIGHT_ARGS
For now these variables need to be set manually. So the usability is
still pretty bad, but is a step in the direction of enabling debugging
the analyzer on code built with buck.
Reviewed By: cristianoc, martinoluca
Differential Revision: D2987288
fb-gh-sync-id: f477611
shipit-source-id: f477611
Summary:public
Assert false have been observed in Procname when analyzing some C projects.
This diff changes the Procname API to make it safe for Java: the java functions in the module don't assert false now. This takes care of the errors observed in C projects.
The new API forces changes throughout the codebase. In particular, the constant propagation module was making assumptions that it would only be executed on Java code, triggering assert false on C. Now it is safe.
For the remaining functions in the Procname module, those for other languages, a special assert false in Utils is used to print stack traces. This is for future debugging.
Reviewed By: sblackshear
Differential Revision: D3054077
fb-gh-sync-id: a77f1d7
shipit-source-id: a77f1d7
Summary:public
Refactoring to make utils.ml more manageable in size.
Reviewed By: cristianoc
Differential Revision: D3058341
fb-gh-sync-id: 7696299
shipit-source-id: 7696299
Summary:This pull request adds the SuppressViewNullability annotation.
The reasoning behind this is that in libraries, one cannot use Butterknife for view binding, which forces you to do it manually. Basically, this makes a new annotation that infer treats the same way as Bind/InjectView
Closes https://github.com/facebook/infer/pull/301
Reviewed By: jvillard
Differential Revision: D3047235
Pulled By: cristianoc
fb-gh-sync-id: 6286d2b
shipit-source-id: 6286d2b
Summary:We currently only output the report as JSON or plain text, however other analyzers use XML and there are tools and plugins to process them, for instance TeamCity XML Report Processing plugin.
Author: Deniz Türkoglu <deniz@spotify.com>
Author: Jules Villard <jul@fb.com>
Closes https://github.com/facebook/infer/pull/300
Reviewed By: cristianoc
Differential Revision: D3047181
Pulled By: jvillard
fb-gh-sync-id: 9026ca2
shipit-source-id: 9026ca2
Summary:public
This diff refactors the current recursive module. It simplifies the structure
making CMethod_decl redoundand.
The idea is to have now two recursive functors: cTrans.ml and cFrontend.ml.
The first dealing with all the expressions and the latter dealing with all
the declarations (in a later diff, we may want to change names of these moules
to reflect Expr and Decl).
This structure will enable to implement lambdas. The previous version
would require some more complex solution where another recursive module
would be involved.
I'm breaking the refactoring in several diffs to make it easier to review.
Reviewed By: akotulski
Differential Revision: D3035122
fb-gh-sync-id: 7dabe9e
shipit-source-id: 7dabe9e
Summary:public
The reactive analysis starts from the set of changed files/procedures, and proceeds
reactively to analyze their dependencies.
This means that after every command, the set of changed files/procedures is reset.
With the --continue option, the capture is continued: all the files/procedures marked
as changed stay changed, plus any additional changes are recorded.
In addition to allowing to spread capture over several commands, the option also allows to separate capture and analysis in reactive mode, or to repeat the analysis.
Reviewed By: sblackshear
Differential Revision: D3046361
fb-gh-sync-id: b6e3797
shipit-source-id: b6e3797
Summary:public
Use the configuration file .inferconfig to model the library method that are considered expensive
Reviewed By: cristianoc
Differential Revision: D3045288
fb-gh-sync-id: e58d85c
shipit-source-id: e58d85c
Summary:public
Revert 6fa9b995e5 (D2843010).
It's slightly less worse to silently ignore Java8 rather than crashing. We'll
wait for an upstream fix to Javalib to resolve the issue of leaked file
descriptors that the original diff was trying to address.
Reviewed By: sblackshear
Differential Revision: D3040978
fb-gh-sync-id: 4020221
shipit-source-id: 4020221
Summary:public
Create initial model of C++ std::shared_ptr. This means that infer will replace implementation of
shared_ptr and the resulting binary will change. Make sure no one will run it by crashing any binary that includes that code.
Reviewed By: jvillard
Differential Revision: D2999948
fb-gh-sync-id: 5753559
shipit-source-id: 5753559
Summary:public
Simplifies the code to collect the `SuppressWarnings` annotations and makes the code more robust in the sense that not finding the output of the annotation processor will result in an error directly at the top-level instead of later on when trying to load the output file in the Java frontend.
Reviewed By: sblackshear
Differential Revision: D3034690
fb-gh-sync-id: 60caa0c
shipit-source-id: 60caa0c
Summary: public Many abstract domains are backed by sets or maps. It's tedious to write the code to pretty-print a set or map each time. These utilities allow pretty-printing of a set/map given functions for printing elements/keys and values.
Reviewed By: jeremydubreil
Differential Revision: D3031196
fb-gh-sync-id: 3bdbde5
shipit-source-id: 3bdbde5
Summary:public
In order to implement the lazy dynamic dispatch algorithm, we need to generate a procedure description based on the types encountered during the symbolic execution. This diff adds support for analyzing such a prodecure description directly, without having to first serialize it to disk, which is slow and not necessary.
Reviewed By: cristianoc
Differential Revision: D3028226
fb-gh-sync-id: 1b2360e
shipit-source-id: 1b2360e
Summary: public Taint errors are complex, and each type requires its own specialized recommendation.
Reviewed By: jeremydubreil
Differential Revision: D3025921
fb-gh-sync-id: 8d7b45b
shipit-source-id: 8d7b45b
Summary:public
Cleanup toplevel of InferAnalyze:
- Make the toplevel flow of InferAnalyze more explicit (no exit).
- Always tear down the logging at the end.
- Fix printing of stats to include only the files actually analyzed with --reactive.
- In the progress bar, print F for files and . for procedures.
Example outputs:
Starting analysis (Infer version v0.7.0-b2fb8fc)
F.....
Analyzed 1 file
where it can say 0 if no file was modified.
Or F without dots if a file was modified but no procedure was.
Reviewed By: sblackshear, jvillard
Differential Revision: D3016934
fb-gh-sync-id: 32cf89c
shipit-source-id: 32cf89c
Summary:public
Adds a mock gradle to test the gradle integration even when gradle is not
installed.
Reviewed By: jeremydubreil
Differential Revision: D2995664
fb-gh-sync-id: f974a67
shipit-source-id: f974a67
Summary:public
bugs.txt only contains the summary of each report. The terminal output contains
a bit more information, such as source excerpts. If one wants to save the
terminal output into a file, they can always use shell redirection anyway.
closes#294
Reviewed By: martinoluca
Differential Revision: D3023796
fb-gh-sync-id: 9a21d17
shipit-source-id: 9a21d17
Summary:public
It's a test, so infer/tests/ is a good place for it. Also, park the expected
outputs all in their own directory. This will help a future diff that changes
the gradle integration test.
Reviewed By: jeremydubreil
Differential Revision: D3019305
fb-gh-sync-id: d3a3ed8
shipit-source-id: d3a3ed8
Summary:public
Instead of using the collection of suppress warnings annotations to filter out the errors while generating the error reports, we just add this SuppressWarnings at translation time, like any other annotations, and the reporting functions in the Reporting module will just skip the errors when the method is annotated with SuppressWarnings.
This allows us to have a suppress warnings mechanism that is independant from the integration with the build system.
Reviewed By: sblackshear
Differential Revision: D3012395
fb-gh-sync-id: 35f5f9b
shipit-source-id: 35f5f9b
Summary:public This also required a refactoring of InitListExpr.
The idea is that ImplicitValueInitExpr can stand for initialising a whole struct,
so we translating as a list of zero expressions, according to the struct's fields,
which is then paired with a list of field expressions, such that one get a list of
assignment instructions.
Reviewed By: ddino
Differential Revision: D2999875
fb-gh-sync-id: 7f609a0
shipit-source-id: 7f609a0
Summary:public
With this change, all the `infer-deps.txt` files generated by buck for those targets
running with the `#infer` flavor, will be merged into one `infer-deps.txt` located in the
designated output folder.
Reviewed By: jvillard
Differential Revision: D2994397
fb-gh-sync-id: 14d8109
shipit-source-id: 14d8109
Summary:public
Lazy dynamic dispatch handling works as follows:
Assuming a call of the form:
foo(a);
where the static type of `a` is `A`. If during the symbolic execution, the dynamic type of the variable `a` is `B` where `B <: A`, then we create on-demand a copy `foo(B)` of `foo(A)` where all the uses of the typed parameter `a` are replaced with a parameter of type `B`. Especially, if `foo` contains virtual call, say `get` where `a` is the receiver, then the call gets redirected to the overridden method in `B`, which simulates the runtime behavior of Java.
This lazy dynamic dispatch mode is only turn on for the tracing mode for now in order to avoid conflicts with sblackshear's approach for sound dynamic dispatch.
Reviewed By: sblackshear
Differential Revision: D2888922
fb-gh-sync-id: 3250c9e
shipit-source-id: 3250c9e
Summary:public
Remove back-end infrastructure that exists only when on-demand mode is disabled.
This, together with removing a few command-line options, sheds a lot of weight in the back-end.
No changes expected for on-demand mode.
Reviewed By: sblackshear
Differential Revision: D2960242
fb-gh-sync-id: 220d821
shipit-source-id: 220d821
Summary:public
Deprecate the incremental mode.
Several parts of the back-end can be removed.
The options for incremental analysis -i at the python level are now deprecated, and re-routed to --reactive.
The main difference with --reactive is that it does not produce an analysis of the whole project, but is limited to what is reachable via reactive propagation starting from the changed files.
Reviewed By: sblackshear
Differential Revision: D2960078
fb-gh-sync-id: 6e8b46b
shipit-source-id: 6e8b46b
Summary:public
An observer object that registered to a notification center needs to be
unregistered before it is deallocated.
If not, the notification center may send a notification to a gost object.
This diff introduce a checker for this problem.
Reviewed By: dulmarod
Differential Revision: D2949692
fb-gh-sync-id: 1653cec
shipit-source-id: 1653cec
Summary:public
In tracing mode, we translate the runtime checks done by the JVM, so the checks for null happen independently from the what happens before the dereference.
Reviewed By: cristianoc
Differential Revision: D2981515
fb-gh-sync-id: 695de07
shipit-source-id: 695de07
Summary:public
`print(tracer)` has an automatic conversion to string that was missed when
migrating to `utils.stdout(tracer)`.
Reviewed By: peterogithub
Differential Revision: D2982104
fb-gh-sync-id: 4c26727
shipit-source-id: 4c26727
Summary:public
- s/"/'/ in python strings
- kill `utils.error()` in favour of the new, identical `utils.stderr()`
- one more `print(utils.encode())` to `utils.stderr()` conversion
Reviewed By: jeremydubreil
Differential Revision: D2976710
fb-gh-sync-id: 6c0fdfa
shipit-source-id: 6c0fdfa
Summary:public
Revamped Timeout module by storing elapsed wallclock seconds, and the status of symops, in case of recursive calls.
Extended the API with suspend() and resume() to pause and resume the current timeout.
These are used before and after an on-demand call to the analysis functions.
This achieves the effect that each procedure, even though is interrupted, has its own time and symop counters, which are suspended and resumed as required.
Reviewed By: jeremydubreil
Differential Revision: D2976918
fb-gh-sync-id: 0ed1079
shipit-source-id: 0ed1079
Summary:public
This class expects a working `jwlib.CompilerCommand` even when we're not doing
anything Java-related. Split the java-specific functionality into a new child
class in jwlib.py.
Reviewed By: jeremydubreil
Differential Revision: D2965832
fb-gh-sync-id: e895b33
shipit-source-id: e895b33
Summary:public
Improved/simplified framework for fronend checkers.
Now we have a unique hook from cTrans to run checkers on statements and a unique
hook from cFrontent to run checkers on declarations.
So now when adding a checker we don't have to modify cTrans/cFrontend.
Moreover made more sistematic the way checkers are invoked. This simplify the definition
of checkers and the way we use them.
Code is now simpler.
Reviewed By: jvillard
Differential Revision: D2976589
fb-gh-sync-id: fbe22d4
shipit-source-id: fbe22d4
Summary:public
java-specific code such as this belongs in jwlib.py. It will also help the
refactoring in the next diff.
Reviewed By: sblackshear
Differential Revision: D2965814
fb-gh-sync-id: c3adc03
shipit-source-id: c3adc03
Summary:public
The NoAllocation checker should not report on the creation of exceptions
Reviewed By: sblackshear
Differential Revision: D2969719
fb-gh-sync-id: 4a8ffc8
shipit-source-id: 4a8ffc8
Summary:public
Add extra dereference when accessing fields that have T& type. It is similar
to what is done when accessing variables of T& type.
The only difference is that we need to handle constructor initializer list
separately (this is the only place where the field can be initialized)
Reviewed By: ddino
Differential Revision: D2965887
fb-gh-sync-id: 1b8708b
shipit-source-id: 1b8708b
Summary:public
This just simplifies the end-to-end tests for Dividde By Zero to make the debugging easier when this test fails.
Reviewed By: cristianoc
Differential Revision: D2966296
fb-gh-sync-id: 5eaa1b5
shipit-source-id: 5eaa1b5
Summary:public
This will avoid a circular dependency between analyze.py and jwlib.py in an
upcoming refactoring.
Reviewed By: martinoluca
Differential Revision: D2965734
fb-gh-sync-id: 1cb69d4
shipit-source-id: 1cb69d4
Summary:public
This attempts to properly sanitise text input/output in the Python parts of
infer. Do three things:
- encode user input (coming from the command-line or reading files)
- decode infer output
- in both cases, we may be using the wrong encoding, eg: locale says we're in
ascii, but the source code contains utf-8. In many cases, like error
messages, it's safe to ignore these encoding mismatches.
Also, since we `import __future__.unicode_literals`, it's safe to remove `u'`
prefixes on many unicode literals.
Reviewed By: martinoluca
Differential Revision: D2960493
fb-gh-sync-id: 9812d7d
shipit-source-id: 9812d7d
Summary:public
Do same thing we do to CXXDefaultArgExpr
Reviewed By: dulmarod
Differential Revision: D2954128
fb-gh-sync-id: 2c92c16
shipit-source-id: 2c92c16
Summary:public
Bring merlin config in sync with makefile, in particular so that it can
find values and types in Utils, and so that it reports the same warnings.
Reviewed By: jvillard, cristianoc
Differential Revision: D2959425
fb-gh-sync-id: 9e7b443
shipit-source-id: 9e7b443
Summary:Resolve a bug that Infer does not analyze procedures when the analyzer is run on '/'.
This bug is reported by btakeya on facebook/infer#283.
Closes https://github.com/facebook/infer/pull/284
Reviewed By: cristianoc
Differential Revision: D2960328
Pulled By: jvillard
fb-gh-sync-id: 55e8b0c
shipit-source-id: 55e8b0c
Summary:public
When compiling projects with this macro set to 1 (which is default on my mac),
infer couldn't get specs for some calls. They were replaced with
different functions by preprocessor.
Reviewed By: ddino
Differential Revision: D2944618
fb-gh-sync-id: df8b457
shipit-source-id: df8b457
Summary:public
Add command-line argument --reactive to enable reactive propagation mode.
When the mode is active, the files changed during compilation are detected, and the analysis propagates reactively starting from the modified files.
The reactive mode allows to analyze a subset of the files in a project and follow their dependencies, without storing the results of previous analyses (specs files). Captured files are preserved from previous runs of the analysis (for example, when the previous analysis was the initial capture), so the mode can be used repeatedly while changing code.
Reviewed By: jvillard
Differential Revision: D2931697
fb-gh-sync-id: 9d6dda0
shipit-source-id: 9d6dda0
Summary:public
Running clang-format on symbolic link replaced it with another file.
This is second diff out of two to fix that problem.
Reviewed By: jvillard
Differential Revision: D2960206
fb-gh-sync-id: 0f21a8f
shipit-source-id: 0f21a8f
Summary:public
Running clang-format on symbolic link replaced it with another file.
This is first diff out of two to fix that problem.
Reviewed By: jvillard
Differential Revision: D2960204
fb-gh-sync-id: aaa3231
shipit-source-id: aaa3231
Summary:public
Adds test_build target to toplevel Makefile, which compiles
InferAnalyze, InferPrint, InferClang, and InferJava where warnings
listed in OCAML_FATAL_WARNINGS defined in infer/src/Makefile are fatal.
Other builds do not treat warnings as fatal. The test build is
performed in parallel with the tests by scripts/test.sh. This makes
refactoring and debugging easier, but prevents warnings from slipping
into the repo.
Also, make test target robust wrt parallel make.
Reviewed By: jvillard
Differential Revision: D2953085
fb-gh-sync-id: 5c0282a
shipit-source-id: 5c0282a
Summary:public
This is intended as a target to build during development when quick
compilation and no duplicate compilation warnings are desired.
This builds byte code for InferAnalyze, InferPrint, InferJava, and
InferClang. This is one ocamlbuild invocation, so builds (and reports
warnings on) each source file once. Building bytecode is currently
about twice as fast as native code.
The llvm frontend is currently not built by this since it requires
menhir and standard ocamlyacc is required by the backend, and ocamlbuild
can only use one at a time.
Reviewed By: jvillard
Differential Revision: D2953050
fb-gh-sync-id: 2e90fcd
shipit-source-id: 2e90fcd
Summary:public
Create separate specs for C models compiled in C++. It will allow us to tweak behavior/names of certain
functions based on the compilation language (such as adding `std::` namespace in C++).
Reviewed By: jvillard
Differential Revision: D2938992
fb-gh-sync-id: 73902f8
shipit-source-id: 73902f8
Summary:public
Now use -safe-string and the Bytes module and bytes type.
Reviewed By: jvillard
Differential Revision: D2949369
fb-gh-sync-id: 58aa688
shipit-source-id: 58aa688
Summary:public
Names of templated types can be very long. The default 4k characters is not long
enough to handle folly library. Increase it to 16k characters and log when deserialization
fails.
Reviewed By: jberdine
Differential Revision: D2948935
fb-gh-sync-id: a659b23
shipit-source-id: a659b23
Summary:public
I have seen enough comments in this space by people during code review to switch on the analyses the compiler can already do. This diff is an automated renaming of unused identifiers to _, with a few additional changes made when reading the diff of the results for things that stood out as particularly strange. This base-lines all of the existing warnings. I'm not sure this is a good idea, since it might be better for those familiar with each part of the code to look at these warnings and use them as pointers to suspicious code.
Reviewed By: jeremydubreil
Differential Revision: D2938376
fb-gh-sync-id: 6e67817
shipit-source-id: 6e67817
Summary:public
Add to the code to detect violation of the `NoAllocation` annotation. This diff adds the code to detect such issue based on the code of the `PerformanceCritical` checker. In the next diff, I will refine the list of acceptable allocations, like new exceptions, etc, and add the list of corresponding tests.
Reviewed By: sblackshear
Differential Revision: D2938641
fb-gh-sync-id: 9a047dd
shipit-source-id: 9a047dd
Summary:public
Before this diff, the checker was collecting in a bottom-up fashion all possible call trees from `PerforamanceCritical`-annotated methods to `Expensive`-annotated ones. With this diff, we just collect the names of the direct transitively expensive callees and compute the expensive call stacks when reporting errors only.
Reviewed By: sblackshear
Differential Revision: D2938635
fb-gh-sync-id: dcdd13c
shipit-source-id: dcdd13c
Summary:public We model it as the builtin __instanceof which models the instanceof construct of Java.
The behaviour is the same.
Reviewed By: jvillard
Differential Revision: D2938969
fb-gh-sync-id: 2258de3
shipit-source-id: 2258de3
Summary:public
Translate headers every time they are included provided that they are located inside project_root directory.
While this is suboptimal (we might end up translating same header many times), doing it exactly once
is hard due to parallel compilation and template instantiations
Reviewed By: dulmarod
Differential Revision: D2916799
fb-gh-sync-id: 93b72c4
shipit-source-id: 93b72c4
Summary:public
Is seems that automatically inheriting annotations like `PerformanceCritical` or `NoAllocation` is the right thing to do in general. Otherwise, we need to enforce sub-typing rules which in the best case just adds a little bit of documentation, but could miss important issues when the code is not fully annotated. I am simplifying this part to avoid adding boilerplate code for the `NoAllocation` case.
Reviewed By: sblackshear
Differential Revision: D2938627
fb-gh-sync-id: ddb668b
shipit-source-id: ddb668b
Summary:public
Type-based resolution of fields, constructors, etc. can be ambiguous if
types are not principal. Compile with -principal and enable warnings 18
and 19 to check these cases.
Reviewed By: jvillard
Differential Revision: D2938237
fb-gh-sync-id: bb4237b
shipit-source-id: bb4237b
Summary:
public
This model does not seem to bring anything anymore. Useless because ...
Reviewed By: cristianoc
Differential Revision: D2920118
fb-gh-sync-id: 7f708d7
shipit-source-id: 7f708d7
Summary:
public
Avoid problems of overwriting good type information with incomplete information
when type declaration happens after its complete definition.
The solution is that we will only time we *update* type information is
when struct declaration has definition as well (which should happen once)
Reviewed By: cristianoc, sblackshear
Differential Revision: D2921811
fb-gh-sync-id: 16baba3
shipit-source-id: 16baba3
Summary:
public
The inductive list predicate was not firing during abstraction because of a type mismatch between C and Java. In Java, the second parameter of the `Sil.Sizeof` constructor is always `Sil.Subtype.exact` in C but is `Sil.Subtype.subtypes` in Java. This diff fixes the confution by comparing the `Sil` types only instead of the type expressions.
Reviewed By: jberdine
Differential Revision: D2912493
fb-gh-sync-id: 3f712a8
shipit-source-id: 3f712a8
Summary:
public
The analysis of the Buck project was failing because this script converts the aliases into their expanded target names. It turns out that for Buck, the name of the command is `buck` and the name of the alias is also `buck`, which led to conflicts. This is now fixed by only replacing the targets in the part of the command line that is after `build` in `buck build ...`
Reviewed By: sblackshear
Differential Revision: D2914446
fb-gh-sync-id: ddce4ed
shipit-source-id: ddce4ed
Summary:
public
Java synthetic methods used to be inlined when a procedure was being analyzed.
This was done almost everywhere. A missing case was when a cfg is loaded during an existing analysis because on-demand needs access to a procedure.
Intead of trying to maintain an invariant in all access paths, we now inline them systematically before saving the cfg to disk.
A secondary consequence of this is that in debug mode the cfg dotty file will show the inlined cfg, so there's no difference between that view and what happens during analysis.
Reviewed By: jeremydubreil
Differential Revision: D2903366
fb-gh-sync-id: 252604c
Summary:
public
The PerformanceCritical Checker was not running on Buck project due to a conflict between the incremental mode and the ondemand mode.
Reviewed By: cristianoc
Differential Revision: D2891649
fb-gh-sync-id: 0a503d8
Summary:
public
This expression is used to value-initialize non-class types. Per definition of value initialization for non-class types:
1. If it's an array, value-initialize each of its elements
2. Otherwise, zero-initialize it
http://en.cppreference.com/w/cpp/language/value_initialization
I was unable to reproduce (1) in a way that produced CXXScalarValueInitExpr and so this diff
deals with case (2)
Reviewed By: jvillard
Differential Revision: D2901311
fb-gh-sync-id: beeafa2
Summary:
public Add typ information to trans_state.var_exp and use it
in constructor translation.
This information is necessary to call constructor of class Base on object with
different type (which is derived from Base)
Reviewed By: jberdine
Differential Revision: D2890850
fb-gh-sync-id: 8075db1
Summary:
public
Add type of return parameter to the context. It allows for better translation
of returnStmt and will be necessary for easy implementation of constructor init lists
Reviewed By: cristianoc
Differential Revision: D2890838
fb-gh-sync-id: e791c3d
Summary:
public
The "dotty" field in json reports is only used when reporting retain cycles. It
makes sense not to emit it by default (when it's `None`).
Reviewed By: akotulski
Differential Revision: D2891320
fb-gh-sync-id: 54292a9
Summary:
public
- add to json reports the location in the ocaml code of assertions raised
during the analysis
- only add when in debug mode. For this, add a flag to `InferPrint` that is
passed by the toplevel `infer` whenever `infer -g` is used.
Reviewed By: jeremydubreil
Differential Revision: D2891286
fb-gh-sync-id: ad4577c
Summary:
public
xvalues is concept introduced in C++11. While they are not same as lvalues, they have one common trait:
They have identity which means that:
> it's possible to determine whether the expression refers to the same entity as another expression, such as by comparing addresses of the objects or the functions they identify (obtained directly or indirectly);
It means that as far as backend is concerned, they should be treated in same way. Right now there is no concept of "move" in the backend and so we don't have
to differentiate between them.
Reference:
http://en.cppreference.com/w/cpp/language/value_category
Reviewed By: cristianoc
Differential Revision: D2895593
fb-gh-sync-id: 5101e28
Summary:
public
C++ allows for parameters with empty names (unused/default copy constructors). Make backend happy by assigning a non-empty
name to these variables
Reviewed By: jvillard
Differential Revision: D2895550
fb-gh-sync-id: b466397
Summary:
public
The env variables used by the Infer backend were only passed in multicore mode. They are now passed before the generation of clusters, whether in single core mode or in multicore mode.
Reviewed By: cristianoc
Differential Revision: D2891816
fb-gh-sync-id: 25074af
Summary:
public
It turns out that C-like structs in C++ may have methods generated by clang (constructors for example).
If struct has a method, it needs to have Sil.Class type - make all CXXRecordDecls Sil.Class types by default.
Reviewed By: cristianoc
Differential Revision: D2895567
fb-gh-sync-id: 8eb18c3
Summary:
The annotations won't work on Android unless you target JDK 1.7 (otherwise it can't DEX the app or library).
Closes https://github.com/facebook/infer/pull/257
Reviewed By: jeremydubreil
Differential Revision: D2889334
Pulled By: sblackshear
fb-gh-sync-id: c09adaa
Summary:
public
Backend needs to know whether parameter has Derived* type - otherwise subtyping in backend doesn't work. Skipping `DerivedToBase` does that
Reviewed By: dulmarod
Differential Revision: D2890673
fb-gh-sync-id: a79abbc
Summary:
public
Simplify our frontend by using information from clang.
It will also make default argument resolution more robust
with templates
Reviewed By: jvillard
Differential Revision: D2890451
fb-gh-sync-id: 9db4beb
Summary:
public
The Worklist module currently encapsulates a global data structure. Likewise for the global variables for the join state and pathset todo and visited.
This diff refactors the Worklist module into an API where instances of the record can be created and passed around. All the global state is included in the record.
The Worklist data structure never escapes the Interproc module.
Reviewed By: sblackshear
Differential Revision: D2887674
fb-gh-sync-id: 65cb234
Summary:
It has a similar lifecycle to activities and fragments, it would be nice to support `onCreate` as an initializer by default.
Closes https://github.com/facebook/infer/pull/258
Reviewed By: jeremydubreil
Differential Revision: D2887325
Pulled By: cristianoc
fb-gh-sync-id: ed31df5
Summary:
public
These casts are responsible for 100 crashes in the frontend on rocksdb.
Reviewed By: dulmarod
Differential Revision: D2879532
fb-gh-sync-id: c4594fb
Summary:
public
1. Add support for temporary C++ objects.
2. Make constructor calls return constructed objects - it allows us pass them as parameters to another constructs (such as parameters, member expressions etc.)
3. Translate FunctionalCastExpr which sometimes is used instead of CXXTemporaryObjectExpr
Reviewed By: dulmarod
Differential Revision: D2874916
fb-gh-sync-id: d9ac2cc
Summary:
public
1. Change exps result of translating call expressions
2. Modify field/method_deref_trans to make them work with rvalues returned by function
3. Add E2E test
Reviewed By: jberdine
Differential Revision: D2874822
fb-gh-sync-id: 42c617d
Summary:
public
This is main reason for not translating rocksdb code right now. Deal with it.
Reviewed By: dulmarod
Differential Revision: D2874446
fb-gh-sync-id: 6f6cf3a
Summary:
public
1. Make function body one stmt instead of list
2. Revert list of statements in exec_trans_instrs
3. Simplify some code related to handling custom instructions
Reviewed By: jvillard
Differential Revision: D2865275
fb-gh-sync-id: b07ed06
Summary:
public
1. When function uses return parameter instead of returning directly, populate that parameter.
2. Turn on new feature for C/C++ functions/methods that return structured types
Reviewed By: jberdine
Differential Revision: D2865091
fb-gh-sync-id: e15e6eb
Summary:
public
This information will be useful when returning values
Reviewed By: jberdine, jvillard
Differential Revision: D2864864
fb-gh-sync-id: 36da0bb
Summary:
public
When method has return parameter, that parameter has to be added when method is called. This adds support for that feature.
Reviewed By: jberdine
Differential Revision: D2864857
fb-gh-sync-id: f7f4094
Summary:
public
Introduce additional parameter for functions returning struct types - instead of returning it, populate output parameter.
This diff just changes method signature, there are more coming
Reviewed By: jberdine
Differential Revision: D2864842
fb-gh-sync-id: 52fc12c
Summary:
public
Remove the need to create a record with two elements to create a procedure description
Reviewed By: cristianoc
Differential Revision: D2872744
fb-gh-sync-id: d26bbdc
Summary:
public
Remove some of the explicit pattern matches in favor of using trans_state.var_exp for
init lists and compound literals
Reviewed By: jvillard
Differential Revision: D2855203
fb-gh-sync-id: ce929f6
Summary:
public
Add optional field to trans_state that denotes variable that is being initialized.
This information will be used by certain constructs (such as c++ constructors or
list initialization).
Passing it in trans_state will enable us to deal with more complicated AST structures where
there might be multiple nodes between variable declaration and its initialization.
Reviewed By: jvillard
Differential Revision: D2854988
fb-gh-sync-id: c100380
Summary:
public
This diff fixes a race condition where errors found in a procedure by one checker could be overwritten by running on demand the analysis of the same procedure with another checker.
Reviewed By: cristianoc
Differential Revision: D2847308
fb-gh-sync-id: 4f0c78e
Summary: public use Sil.exp to pass variable to initialize instead of res_trans containing this Sil.exp.
Reviewed By: jvillard
Differential Revision: D2854981
fb-gh-sync-id: 0cb37f3
Summary:
public This assert false causes the whole analysis to crash.
It is currently happening intermittently which makes it hard to debug.
Other inconsistencies don't cause the whole analysis to crash normally,
so this one seems to be too strict.
Reviewed By: cristianoc
Differential Revision: D2849864
fb-gh-sync-id: de6dce0
Summary:
public
When no classpath was specified, Infer were considering it to be None instead of the current directory. The consequence is that we were replacing the current directory with the annotation processor for suppress warnings, leading to cases where `javac` was compiling fine but `infer -- javac` was failing with classes not found compilation issues. This diff fixes by always having at least "." in the classpath.
Reviewed By: sblackshear
Differential Revision: D2853035
fb-gh-sync-id: e69db7c
Summary:
public
I previously forgot to keep this feature when deleting BuckAnalyze.
Reviewed By: sblackshear
Differential Revision: D2850869
fb-gh-sync-id: d23f1ca
Summary:
public
otherwise Infer cannot know the type of the temporary variable
Reviewed By: dulmarod
Differential Revision: D2845054
fb-gh-sync-id: cf5fb8d
Summary:
public
The script `BuckAnalyze` has been deprecated for a while already. Time to remove it.
Reviewed By: sblackshear
Differential Revision: D2844414
fb-gh-sync-id: b5e1195
Summary:
public
The code to configure to configure the logging was duplicated, but was not not doing exactly the same thing. This diff makes all the code to call the same configuration function.
Reviewed By: sblackshear
Differential Revision: D2844361
fb-gh-sync-id: 9887cad
Summary:
public
Use Infer traces to follow the chain of calls from methods annotated PerformanceCritical to the methods annotated as Expensive.
This contains direct jumps from method definition to method definition. So the traces are of the form:
method definition of m1 -> definition of m2 -> definition of m3 -> ... -> definition of mN annotated as Expensive
In the next diff, I will make the checker create traces of the form:
definition of m1 -> call to m2 -> definition of m2 -> call to m3 -> ... -> call to mN -> definition of mN annotated as Expensive
and then simplify the error message whenever the chain of call is longer than, say, 5 calls.
Reviewed By: jberdine
Differential Revision: D2818398
fb-gh-sync-id: c566a44
Summary: public We are not assigning the location of the property rather than that of the class. It seems that it's no problem having the bugs reported in the .h files.
Reviewed By: ddino
Differential Revision: D2831226
fb-gh-sync-id: 026692e
Summary: public We are not assigning the location of the property rather than that of the class. It seems that it's no problem having the bugs reported in the .h files.
Reviewed By: ddino
Differential Revision: D2828005
fb-gh-sync-id: cf26549
Summary:
This will stop Infer from creating an `infer-out` directory when just running `infer`.
(I run `infer` without any arguments somewhat often to look at documenting.)
One downside to this is that there will be no logs when running Infer without any commands - is this bad?
Closes https://github.com/facebook/infer/pull/240
Reviewed By: cristianoc
Differential Revision: D2829752
Pulled By: jeremydubreil
fb-gh-sync-id: 6827ef9
Summary:
public
Reuse logic in cFrontend.ml to deal with nested structs. This allows to have less duplicated logic which will result
in less bugs.
As a bonus, it fixes the problem of nested template class (which wasn't be handled right).
And one random fix in c_type -> sil_type conversion (I'm amazed it worked before)
Reviewed By: dulmarod
Differential Revision: D2773687
fb-gh-sync-id: e312599
Summary:
public
In the case of Buck, the integration works by using the out directory of javac in order to store the analysis artifacts in the jar file. Making buck call:
infer -o infer_out -- javac -d classes_out ...
instead of every javac command is having no effect and is the same as Buck running:
infer -- javac -d classes_out ...
Reviewed By: sblackshear
Differential Revision: D2822642
fb-gh-sync-id: b13e067
Summary: public This map is the only reason we currently need to piggyback on the compiler. Once we have the map we should be able to point Infer at bytecodes + the map.
Reviewed By: jeremydubreil
Differential Revision: D2813110
fb-gh-sync-id: 91664de
Summary:
public
Get newest version of facebook-clang-plugin that replaces pointers from strings to ints.
Fix all compilation issues infer has
Reviewed By: jvillard
Differential Revision: D2815144
fb-gh-sync-id: e93d4b3
Summary:
public
CLocation.init_curr_source_file is now a no-op, so remove it.
Reviewed By: jvillard
Differential Revision: D2815238
fb-gh-sync-id: 00c8a08
Summary:
public
CLocation.current_source_file is always equal to DB.current_source, so
remove it.
Reviewed By: jvillard
Differential Revision: D2815236
fb-gh-sync-id: 9390d2b
Summary:
public
It seems that CLocation.current_source_file is always equal to
DB.current_source. This diff adds assertions to check this, as a
precondition for forthcoming diffs that simplify CLocation code.
Reviewed By: jvillard
Differential Revision: D2815231
fb-gh-sync-id: 88d1f32
Summary:
public
Fist resolve the method name based on the dynamic types found during the symbolic execution, then run the analysis on-demand with the resolved method name.
Reviewed By: cristianoc
Differential Revision: D2815744
fb-gh-sync-id: c55accd
Summary:
public
Add destructor calls on delete expression.
While not the most important, it is the simplest case of adding destructor calls.
This will help us in the future with more complex cases.
Reviewed By: ddino
Differential Revision: D2773483
fb-gh-sync-id: 4df9c73
Summary:
public
In the case of Java, the name of the method is enough to lookup the summary of the callees and run the symbolic execution. This revision separates the case of method call in Java and in C, C++ and Objective C. Most of the code for executing method calls was Clang specific and this is an intermediate step to be able to run the capture and analysis on demand.
Reviewed By: sblackshear
Differential Revision: D2809171
fb-gh-sync-id: da62dce
Summary:
public
Title - instead of just creating dot file in some location, include this information as part of bug description.
Reviewed By: ddino
Differential Revision: D2779941
fb-gh-sync-id: 6bfb02b
Summary:
public
Add extra field that will be used to store extra bug description
in dotty format. This will allow to create better bug reports for
bugs that require images to understand what is going on (such as
retain cycles or activity leaks)
Reviewed By: jeremydubreil
Differential Revision: D2779935
fb-gh-sync-id: d2ecc0d
Summary:
public
When reading from static fields, the translation was overwriting the list of class members with the list of static ones. The backend was only looking up fields from the list of non static fields.
Reviewed By: sblackshear
Differential Revision: D2801759
fb-gh-sync-id: fe8ed80
Summary:
public
While playing with the type environment for Java, I realised that the types in models.jar where not re-generated when modifying Infer. As a consequence, some changes in Infer where surprisingly having no effect. This diff forces the type environment to be absent when analyzing the models.
Reviewed By: sblackshear
Differential Revision: D2802517
fb-gh-sync-id: 1c2673a
Summary:
public
4feb93e91c disabled join of tuple values, but also of any two values of the same
type. However, we do know how to join integer values, so re-enable those.
Reviewed By: cristianoc
Differential Revision: D2803286
fb-gh-sync-id: 5bcc725
Summary:
public
Using Typename.t in the list of superclasses to match the type for the key of the type environment. This avoids to make back and forth convertions from typename to type (csu, mangled name).
Depends on D2786574
Reviewed By: jberdine
Differential Revision: D2792116
fb-gh-sync-id: 6100f1a
Summary:
public
This diff cleans up the detection of assertion failures in C, C++ and Objective C which was previously hacked on top of the tracing mode for Java. The code is also generalized to detect any custom errors which can be defined using the `__infer_fail` builtin, and the case of assertion failure is now just the specific case of translating `assert` using `__infer_fail` directly in the clang frontend.
Reviewed By: jberdine
Differential Revision: D2786574
fb-gh-sync-id: dd1e1cf
Summary:
public
It seems that restricting printing to stdout and stderr to developer
mode has broken InferPrint. So unconditionally turn developer mode on
in InferPrint.
Reviewed By: sblackshear
Differential Revision: D2786897
fb-gh-sync-id: 44b5772
Summary:
public
When building models, make was invoked explicitly with `make -j` rather
than with `$(MAKE)`. This prevented controlling parallelism from the
top-level make invocation.
Reviewed By: akotulski
Differential Revision: D2786812
fb-gh-sync-id: 7f6d58c
Summary:
public
Some functions were never used, and some other were always used with the same parameters
Reviewed By: sblackshear
Differential Revision: D2786118
fb-gh-sync-id: 666fba2
Summary:
public
The function Sil.get_typ was actually always call with the optional parameter being `Csu.Class`
Reviewed By: sblackshear
Differential Revision: D2786055
fb-gh-sync-id: 4337258
Summary:
public
The paramtere where defined as simple strings in the procedure description. This diff force the use of the Mangled module to avoid possible conflict when converting variable back and forth from string to pvar. The code is now more consistent as the local variable were already named using mangled names.
Reviewed By: jberdine
Differential Revision: D2782863
fb-gh-sync-id: 1867574
Summary:
public
Move the naming of types to it own module, so that it can be used by modules `Sil` depends from like `Procname`
Reviewed By: jberdine
Differential Revision: D2773148
fb-gh-sync-id: a89f595
Summary:
public
Move the representation of data-structure into it own module, so that it can be used by modules `Sil` depends from like `Procname`.
Reviewed By: jberdine
Differential Revision: D2772791
fb-gh-sync-id: cda4e3a
Summary: public In this example we now get a dangling pointer dereference, so contains exactly doesn't work.
Reviewed By: jvillard
Differential Revision: D2773769
fb-gh-sync-id: 64d1044
Summary: public The properties in those models needed to be made nonatomic.
Reviewed By: akotulski
Differential Revision: D2773650
fb-gh-sync-id: 903e7df
Summary:
public
Make Ast_utils.get_decl_from_typ_ptr function more forgiving.
It will return None instead of crashing when there is no decl for a given type.
This is done in prepratation to try to get destructor function of any type without crashing.
Reviewed By: dulmarod
Differential Revision: D2769302
fb-gh-sync-id: 7a9fcfe
Summary:
public
Factor resolving default parameters from common method/constructor translation function.
This is done in preparation to use same function for generating destructor calls.
Reviewed By: dulmarod
Differential Revision: D2769291
fb-gh-sync-id: 9c35cf8
Summary:
public
Treat destructors in the same way we treat methods/constructors.
It doesn't deal with inheritance/composition - we'll need to add calls to these
destructors later
Reviewed By: dulmarod
Differential Revision: D2769142
fb-gh-sync-id: b1c77e1
Summary: public Crashes during the analysis are classified as timeouts in the .specs file. In addition, when there is a timeout, it does not say *why* the timeout occurred (hard time, symops, or recursion). This diff adds this information to the .specs file and adds a "fail hard" mode where crashes and timeouts will actually stop the analysis in developer mode (but will still be hidden in the normal production mode).
Reviewed By: jeremydubreil
Differential Revision: D2725382
fb-gh-sync-id: b0b4e5e
Summary:
public
This fixes two things:
- `make -j9000` now works without crashing
- `make -C infer/src clang java` followed by `make -C infer/src clang` results
in a cached build the second time. Previously, a bug in ocamlbuild meant that
building infer/java would stomp over some files used by infer/clang, hence
infer/clang would get partially recompiled. More generally, alternating
between targets, or simply repeatedly calling `make` would result in unecessary
rebuilds.
Reviewed By: akotulski
Differential Revision: D2765544
fb-gh-sync-id: ecffdee
Summary: public Did this by adding an option to rearrange that turns of error reporting.
Reviewed By: dulmarod
Differential Revision: D2768396
fb-gh-sync-id: 4898d2d
Summary:
public
Infer would previously give confusing reports in the following case: two classes `foo.MyClass` defined in `MyClass.java` under directory `foo/` and `bar.MyClass` defined in file `MyClass.java` under `bar/` are compiled together in a single call to the Java compiler. Then the errors in `foo/MyClass.java` could potentially be reported in `bar/MyClass.java`, or the other way around.
The reason is: Infer starts the translation from the bytecode which only contains information about the base filename in the metadata. For example, both `foo.MyClass` and `bar.MyClass` will contains the information that the source file is `MyClass.java` but not the full path to the actual source file (hopefully).
In order to cope with this issue, this diff adds the possibility to read the package declaration from the source file so that we can map classes to the source files these classes are defined without ambiguity. In order to avoid having to open and read the source files when not necessary, the code will behave as before as long as no name conflict is found. Otherwise, it will only load and search for the package declaration when two or more sources files have the same basename but are defined in different subdirectories.
Closes t9395275
Reviewed By: jberdine
Differential Revision: D2763775
fb-gh-sync-id: 0adc1ac
Summary:
public
There was one oversight that caused frontend to mark C++ method as
objc instance method.
Reviewed By: dulmarod
Differential Revision: D2769060
fb-gh-sync-id: d7a92bc
Summary:
public To deal with ObjC nullability and give meaningful error
messages, we introduced the ObjC_NULL attribute in the symbolic execution to
mean that the object carrying the attribute is null because it was the result
of a method call from a null object. However, one cannot add attributes to null,
so we had to delay nullifying the object in order to have the attribute until we
can assign it to a program variable. However, if the temp variable was used in a condition,
we were not taking into account that its meaning is null. This diff addresses that and fixes
many FPs that we have encounter.
Reviewed By: ddino
Differential Revision: D2765167
fb-gh-sync-id: c0878dd
Summary:
public
Generating .annot files is expensive. Add a configure option to disable them:
./configure --disable-ocaml-annot
./configure --disable-ocaml-bin-annot
(the latter is more for completeness, as bin-annot are not very expensive to
generate)
`make` is 30% faster without annot files. Unless you use Eclipse you shouldn't
need them.
Reviewed By: jeremydubreil
Differential Revision: D2765508
fb-gh-sync-id: 086bc39
Summary: public First in a series of diffs fixing the __nullable checker for obj-c, which currently reports false positives on property accesses via getters and setters. To fix this problem, we need a special implementation of letderef and set for property accesses that don't report NPE errors. Factoring out the execution of these instructions from the main symbolic executor will make this easier.
Reviewed By: jeremydubreil
Differential Revision: D2763923
fb-gh-sync-id: 883a184
Summary:
public
`json.dump` does not have the same number of arguments in 2.7.3 and 2.7.9. Fix
this by naming the optional parameters explicitly.
Reviewed By: akotulski
Differential Revision: D2760579
fb-gh-sync-id: 7ebc69e
Summary:
public
This configure option disables building the java analysis and the associated
checks.
Refactor infer/src/Makefile.in to better isolate the Java-specific ocamlfind
dependencies.
Reviewed By: jeremydubreil
Differential Revision: D2712921
fb-gh-sync-id: 08077c2
Summary:
public
This moves the hardcoded version numbers in one place and simplifies the logic
to compute the version a bit.
Reviewed By: jberdine
Differential Revision: D2759779
fb-gh-sync-id: 0e4d3c1
Summary:
public Remove property of maps and make sure that we add to the tenv the property attributes
by folowing the link between the property and the corresponding ivar.
Reviewed By: ddino
Differential Revision: D2755887
fb-gh-sync-id: beeecaf
Summary:
public
Remove trans_state.parent_line_number because it's not used anymore.
This slightly cleans up codebase
Reviewed By: ddino
Differential Revision: D2755050
fb-gh-sync-id: b1b7e8e
Summary:
public
The contravariant subtyping rule for the PerformanceCritial annotation was meant to document the code but can be very too verbose on exisiting project. It is also not necessary as we can get this annotation from the supertypes. I am disabling it for now, but keep the code in case we want to revive it at some point in the future.
Reviewed By: sblackshear
Differential Revision: D2750212
fb-gh-sync-id: 2424281
Summary:
public
Lines other than the first of multi-line comments in non-ocaml files
were flush right instead of aligned.
Reviewed By: jvillard
Differential Revision: D2739752
fb-gh-sync-id: c85f56e
Summary:
public
The function `Procname.to_simplified_string ~withclass:true` used to print `MyClass.MyClass()` when printing the name of a Java constructor. It now prints `MyClass()`.
I made a separate diff for this changes as it affects the bug hash, especially for resource leaks.
Reviewed By: sblackshear
Differential Revision: D2748661
fb-gh-sync-id: 9f51871
Summary:
public
It is possible to return null according to
http://docs.oracle.com/javase/7/docs/api/java/lang/Class.html#getResource(java.lang.String).
Also, getResource throws NPE if passed null:
$ cat -n TestClassGetResourceArgument.java
1 import java.net.URL;
2
3 public class TestClassGetResourceArgument {
4
5 static URL testClassGetResourceArgument(Class cls) {
6 return cls.getResource(null);
7 }
8
9 public static void main(String[] args) {
10 System.out.println(testClassGetResourceArgument("".getClass()).toString());
11 }
12
13 }
$ javac TestClassGetResourceArgument.java && java TestClassGetResourceArgument
Exception in thread "main" java.lang.NullPointerException
at sun.misc.MetaIndex.mayContain(MetaIndex.java:243)
at sun.misc.URLClassPath$JarLoader.getResource(URLClassPath.java:830)
at sun.misc.URLClassPath.getResource(URLClassPath.java:199)
at sun.misc.URLClassPath.getResource(URLClassPath.java:251)
at java.lang.ClassLoader.getBootstrapResource(ClassLoader.java:1305)
at java.lang.ClassLoader.getResource(ClassLoader.java:1144)
at java.lang.ClassLoader.getResource(ClassLoader.java:1142)
at java.lang.ClassLoader.getSystemResource(ClassLoader.java:1267)
at java.lang.Class.getResource(Class.java:2145)
at TestClassGetResourceArgument.testClassGetResourceArgument(TestClassGetResourceArgument.java:6)
at TestClassGetResourceArgument.main(TestClassGetResourceArgument.java:10)
Reviewed By: cristianoc
Differential Revision: D2752301
fb-gh-sync-id: 888baf1
Sam Blackshear
jrm
Josh Berdine
Andrzej Kotulski
Dulma Rodriguez
Cristiano Calcagno
Dino Distefano
Jules Villard
martinoluca
Nick Firmani
Deniz Türkoglu
kstreee
Peter O'Hearn
Tony Cosentini