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
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
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
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: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
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
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
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
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
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
Do same thing we do to CXXDefaultArgExpr
Reviewed By: dulmarod
Differential Revision: D2954128
fb-gh-sync-id: 2c92c16
shipit-source-id: 2c92c16
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
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
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
Jules Villard
Josh Berdine
Dulma Rodriguez
Cristiano Calcagno
Sam Blackshear
Dino Distefano
jrm
Andrzej Kotulski
Nick Firmani
Peter O'Hearn
kstreee