Summary:
Handle building in debug mode by passing command line options set in
the Makefile, as all the other configuration of ocamlbuild is done
through command line options.
Reviewed By: jvillard
Differential Revision: D3202085
fb-gh-sync-id: d467019
fbshipit-source-id: d467019
Summary:
The computation of the perf stats file did not work in case -cluster was
passed a (relative) path.
Also, do not fail if the perf stats file cannot be opened/written, just
log a warning to stdout.
Reviewed By: jvillard
Differential Revision: D3269727
fb-gh-sync-id: c141ffa
fbshipit-source-id: c141ffa
Summary:
- [python] decode strings coming from `os.*` commands
- [python] decode strings coming from the command-line
- [python] encode a few remaining unicodes into strings
- [java] replace lex/yacc parser for javac verbose output by regex-based matching to handle unicode in paths
- [make] random fix of `make test` to have `make clean test` work
- [integration tests] add e2e build integration tests for utf8 in the PWD
Closes#76
Reviewed By: martinoluca
Differential Revision: D3240809
fb-gh-sync-id: 8c2e1ed
fbshipit-source-id: 8c2e1ed
Summary:
Results of AbsInt checkers are node id -> abstract state maps.
It's hard to compare/combine the results of multiple analyses if the node id types are different.
Needed for the upcoming improvements of the preanalysis.
Reviewed By: jvillard
Differential Revision: D3235669
fb-gh-sync-id: c5251cf
fbshipit-source-id: c5251cf
Summary:
The case where the right hand side of the `Letderef` expression is an identifier was missing. With this diff, the following example is now working as expected:
class A {
public Object foo() {
return new Object();
}
}
class B extends A {
public Object foo() {
return null;
}
}
public class Test {
static Object bar(A a) {
return a.foo();
}
static void shoulReport() {
B b = new B();
bar(b).toString();
}
}
using the command:
INFER_LAZY_DYNAMIC_DISPATCH=1 infer -- javac Test.java
Reviewed By: sblackshear
Differential Revision: D3238986
fb-gh-sync-id: d6059fb
fbshipit-source-id: d6059fb
Summary:
The philosophy of the tracing mode reporting is to not report the errors in a method if reaching this error does depend on information that can be false at call site. Typically with:
void foo(Object obj, int x) {
if (x == 3) {
obj.toString();
}
}
it may be that we always call `foo` with a non-null parameter or `x != 3`.
Thechnically, the reporting code matches the pairs of the form (precondition, error) and filtering out the cases where the precondtions was not imposing constraints on the calling context, and report the other cases. So the NPE could be reported in the following case:
void bar() {
foo(null, 3);
}
However, we were missing the case where there was anyway no way to call a method in a safe way, i.e. all the preconditions were of the form: (precondition, error), for example:
void baz(boolean b) {
if (b) {
foo(null, 3);
} else {
foo(null, 3);
}
}
In that case, the summary is of the form
PRE (1): b = false
POST: NullPointerException
PRE (2): b = true
POST: NullPointerException
In which case it is legit to report `NullPointerException` in `baz`.
Reviewed By: sblackshear, jberdine
Differential Revision: D3220501
fb-gh-sync-id: 7fb7d70
fbshipit-source-id: 7fb7d70
Summary: So that we no longer have to run `Tabulation.prop_is_exn` before running `Tabulation.prop_get_exn_name`.
Reviewed By: jberdine
Differential Revision: D3222545
fb-gh-sync-id: a7faa06
fbshipit-source-id: a7faa06
Summary:
As suggested in the discussion https://github.com/facebook/infer/issues/326 this pull request implements
```ocaml
get_overriden_method : Tenv.t -> Procname.java -> Procname.t
```
to get the method of a superclass that is being overridden by a specific java pname.
I thought of unit test this, but unfortunately I wasn't able to figure out how to create the proper context with OUnit2. Perhaps the easiest way to test this will be integration tests.
Feel free to reject the pull request if unit tests are mandatory (or for any other reason, of course).
Closes https://github.com/facebook/infer/pull/341
Reviewed By: jeremydubreil
Differential Revision: D3221254
Pulled By: sblackshear
fb-gh-sync-id: 9c26258
fbshipit-source-id: 9c26258
Summary:
I ran perf on rocksdb analysis and found out that ~40% of time is spent inside ocaml GC originating
from Prop.typ_normalize.
After this change, profile shows that GC is ~2% and Prop.typ_normalize takes 50% of the time.
Reviewed By: jberdine
Differential Revision: D3219113
fb-gh-sync-id: 27c34d9
fbshipit-source-id: 27c34d9
Summary:Local variable created by conditional operator translation is now declared in scope of whole
procedure. Semantically there is no difference, hopefuly backend will not complain about this
change. Also, nullifying that variable is deferred to preanalysis instead of calling it manually
Reviewed By: jvillard
Differential Revision: D3155733
fb-gh-sync-id: 6cec8fc
fbshipit-source-id: 6cec8fc
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
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
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
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
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
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
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
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
Jeremy Dubreil
Sam Blackshear
Josh Berdine
Jules Villard
Dulma Churchill
Luis Cruz
Andrzej Kotulski
Dino Distefano
Peter O'Hearn
Cristiano Calcagno
Nick Firmani