Summary:
The full inventory of everything in infer-out/. The main change is
around "issues directories": instead of registering them dynamically
they are now all declared statically (well, they kind of were already in
Config.ml).
Reviewed By: ngorogiannis
Differential Revision: D20894305
fbshipit-source-id: 1a06ec09d
Summary:
This is another entry in infer-out/, we want these to be predictable,
not user-defined.
Reviewed By: dulmarod
Differential Revision: D20894302
fbshipit-source-id: ee60ddbcf
Summary:
This is an entry in infer-out/, we want these to be predictable, not
user-defined.
Reviewed By: ngorogiannis
Differential Revision: D20894307
fbshipit-source-id: 332f85969
Summary:
This option allowed one to customise the name of the log file, but the
log file lives in infer-out/ so that flexibility is not needed and even
undesirable: we want entries in infer-out/ to be predictable.
Reviewed By: skcho
Differential Revision: D20894304
fbshipit-source-id: 760d91df3
Summary: Another entry to practice adding entries to ResultsDirEntryName.
Reviewed By: skcho
Differential Revision: D20894299
fbshipit-source-id: 9c387e0f3
Summary:
First real step to keep an inventory of all the entries in infer-out/ in
a single place, and associate meta-data to each entry. In particular, we
want to avoid adding things in infer-out/ without a clear idea of
whether they should be cleaned up before going into a cache, or before
an incremental analysis.
Migrate infer-out/tmp/ first just as an example and an excuse to write
the scaffolding code needed for all the other entries.
Reviewed By: skcho
Differential Revision: D20894300
fbshipit-source-id: f796fca55
Summary:
The only accurate entry it contains is the number of files analysed and
we can already get that information from the log file (and console
output).
Reviewed By: dulmarod
Differential Revision: D20894303
fbshipit-source-id: bc180015a
Summary: Needed for later: RunState needs to run files in ResultsDir.
Reviewed By: skcho
Differential Revision: D20894306
fbshipit-source-id: 259b7da69
Summary:
I wanted to change the order in which we try loading them but it changes
analysis results too much for the cost analysis.
Reviewed By: skcho
Differential Revision: D20891172
fbshipit-source-id: f972f314e
Summary:
Simplifies the models story. The model jar is still needed to look up
fields in modelled classes (we save the .class of each model!). This is
sad as we should be able to get these from the models' tenv, which
should be more compact, but that's a bigger change.
Reviewed By: skcho
Differential Revision: D20891117
fbshipit-source-id: fcb5104ae
Summary:
Parsing the standard output of buck is brittle. Instead, use the `--build-report` option, which generates a json file, with a mapping from target name to output path. This already contains all the information required.
This diff adapts the buck-java integration.
Reviewed By: artempyanykh
Differential Revision: D20942858
fbshipit-source-id: faf3f2078
Summary: Unify the models of malloc and for the Create and Copy functions for Core Graphics. This add the null case from the malloc model to the Core Graphics models.
Reviewed By: jvillard
Differential Revision: D20890956
fbshipit-source-id: 278ac9d2f
Summary:
- Open-source stubs are in a library with no dependencies
- That library is included in InferBase, but in facebook builds it
contains no modules
Reviewed By: ezgicicek
Differential Revision: D20922574
fbshipit-source-id: af918a687
Summary:
As soon as pulse detects an error, it completely stops the analysis and loses the state where the error occurred. This makes it difficult to debug and understand the state the program failed. Moreover, other analyses that might build on pulse (e.g. impurity), cannot access the error state.
This diff aims to restore and display the state at the time of the error in `PulseExecutionState` along with the diagnostic by extending it as follows:
```
type exec_state =
| represents the state at the program point that caused an error *)
```
As a result, since we don't immediately stop the analysis as soon as we find an error, we detect both errors in conditional branches simultaneously (see test result changes for examples).
NOTE: We need to extend `PulseOperations.access_result` to keep track of the failed state as follows:
```
type 'a access_result = ('a, Diagnostic.t * t [denoting the exit state] ) result
```
Reviewed By: jvillard
Differential Revision: D20918920
fbshipit-source-id: 432ac68d6
Summary: Consider functions that simply exit as impure by extending the impurity domain with `AbstractDomain.BooleanOr` that signifies whether the program exited.
Reviewed By: skcho
Differential Revision: D20941628
fbshipit-source-id: 19bc90e66
Summary: The pruning location of array size was dummy. This diff gives a right location to traces in the pruning.
Reviewed By: ezgicicek
Differential Revision: D20915167
fbshipit-source-id: 55cc583df
Summary:
Instead of looking up each proc name in models/, pre-compute the list of
models and do lookups there instead of in the filesystem.
Reviewed By: ngorogiannis
Differential Revision: D16603148
fbshipit-source-id: 5eb534a14
Summary:
Java bytecode format does not record the declarations location
for classes and fields. We set up a first infrastructure to recover this
information. Currently we only track location for classes and only gives
the first line of the corresponding source file. We will enhance this location
with source file (baby) parsing in a next diff.
Reviewed By: mityal
Differential Revision: D20868187
fbshipit-source-id: d355475e9
Summary:
This information can be useful for tooling responsible for further
processing (e.g. metric calculation and logging)
Reviewed By: artempyanykh
Differential Revision: D20914583
fbshipit-source-id: 61804d88f
Summary: The heuristics is to find a method in non-abstract sub-classes. See D20647101.
Reviewed By: jvillard
Differential Revision: D20491461
fbshipit-source-id: 759713ef4
Summary:
This diff distinguishes array declaration and size-setting in trace. For example, when there is an
assume statement on an array size, the array size can be pruned to another value. In which case, we
want to see "Set array size" in the trace, instead of "Array declaration".
Reviewed By: jvillard
Differential Revision: D20914930
fbshipit-source-id: 0253fb69e
Summary:
This diff lifts the `PulseAbductiveDomain.t` in `PulseExecutionState` by tracking whether the program continues the analysis normally or exits unusually (e.g. by calling `exit` or `throw`):
```
type exec_state =
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *)
| ExitProgram of PulseAbductiveDomain.t
(** represents the state originating at exit/divergence. *)
```
Now, Pulse's actual domain is tracked by `PulseExecutionState` and as soon as we try to analyze an instruction at `ExitProgram`, we simply return its state.
The aim is to recover the state at the time of the exit, rather than simply ignoring them (i.e. returning empty disjuncts). This allows us to get rid of some FNs that we were not able to detect before. Moreover, it also allows the impurity analysis to be more precise since we will know how the state changed up to exit.
TODO:
- Impurity analysis needs to be improved to consider functions that simply exit as impure.
- The next goal is to handle error state similarly so that when pulse finds an error, we recover the state at the error location (and potentially continue to analyze?).
Disclaimer: currently, we handle throw statements like exit (as was the case before). However, this is not correct. Ideally, control flow from throw nodes follows catch nodes rather than exiting the program entirely.
Reviewed By: jvillard
Differential Revision: D20791747
fbshipit-source-id: df9e5445a
Summary:
Malloc returns either an allocated object or a null pointer if there is no memory available. Modelling that.
This has always been a bit contentious because this leads to NPEs that people often ignores because they don't care. But if we don't model this, then we have FPs when people do take this into account when freeing the memory.
Reviewed By: jvillard
Differential Revision: D20791692
fbshipit-source-id: 6fd259f12
Summary:
infer-out/tmp/ should be deleted before sending infer-out/ to any cache.
Also separate the list of directories to delete in `delete_capture_and_results_data` and in `scrub_for_caching` as it was only confusing to try to share them.
Reviewed By: ngorogiannis
Differential Revision: D20772512
fbshipit-source-id: b1e4e252c
Summary: This makes it similar to the other dir names in infer-out/.
Reviewed By: ngorogiannis
Differential Revision: D20795359
fbshipit-source-id: 88729d26d
Summary:
This diff limits the depth of abstract location by a constant.
problem: Inferbo generated too many of abstract locations, especially when struct types had many pointer fields and Inferbo was not able to analyze the objects precisely. Since the number of generated abstract locations were exponential to the number of fields, it resulted in OOM in the end.
(reported by zyh1121 in https://github.com/facebook/infer/issues/1246)
Reviewed By: jvillard
Differential Revision: D20818471
fbshipit-source-id: f8af27e5c
Summary:
Currenlty the cost issue is printed at the first node of a function, which is usually the first
statment of the function. This may give a wrong impression that the cost of the statement is
changed.
This diff re-locate where to print issues with heuristics. Going backward from the first node
lines, it looks up a line satisfying,
1. A line should start with <fname> or should include " <fname>".
2. The <fname> found in 1 should be followed by a space, '<', '(', or end of line.
Reviewed By: jvillard
Differential Revision: D20766876
fbshipit-source-id: b4fee3180
Summary:
It's easy to create large arrays in code, eg `int x[1UL << 16];`, but
these can generate huge nodes in SIL because zero-initialization is
translated by zero-ing structures element by element. Introduce a
builtin to use instead. Keep the naive method for small structures (with
a configurable limit on "small").
Reviewed By: dulmarod
Differential Revision: D20836836
fbshipit-source-id: 6bf5410f8
Summary: Modelling `CG.*Release ` and `CFRelease` as `free`. This is what we were doing in biabduction.
Reviewed By: skcho
Differential Revision: D20767174
fbshipit-source-id: c77c1cdc6
Summary:
This models all the Create and Copy functions from CoreGraphics, examples in the tests.
These functions all allocate memory that needs to be manually released.
The modelling of the release functions will happen in a following diff. Until then, we have some false positives in the tests.
This check is currently in biabduction, and we aim to move it to Pulse.
Reviewed By: jvillard
Differential Revision: D20626395
fbshipit-source-id: b39eae2d9
Summary: Sometimes buck hangs with the new integration and using pipes. Use a temp file for standard output and redirect stderr.
Reviewed By: jvillard
Differential Revision: D20856346
fbshipit-source-id: 13a5f90d5
Summary:
Fix all the docstrings that `odoc` or `ocamlformat` is not happy about.
Delete all `[@@ocamlformat "parse-docstring = false"]` pragmas as a
result.
Reviewed By: jberdine, ngorogiannis
Differential Revision: D20798913
fbshipit-source-id: 728d9e45c
Summary:
All dune libraries in infer/src/ were declared with their own public
names, each one needing its own .opam file. There's no need for that:
they can all be part of the `infer` library by calling them `infer.Foo`.
One wrinkle: now we need to explicitly point at their .mld files in the
generated documentation.
Reviewed By: jberdine
Differential Revision: D20798914
fbshipit-source-id: 64b64261c
Summary:
This avoids dune scanning 2000+ directories (according to its logs),
mostly due to scanning infer/tests/ I think.
Reviewed By: artempyanykh
Differential Revision: D20798915
fbshipit-source-id: 3764cd3fb
Summary:
- Add `no_return` models for Java's `exit(...)` methods (can be extended further later on)
- handle throw-catch better by short-cutting throw nodes to not exit node but to all **catch nodes** that are reachable by the node. If there is no catch node, we short-cut to the exit node as before.
This removes a FP from deadstore tests because before we simply were not able to handle CF from throw-> catch nodes at all.
Reviewed By: skcho
Differential Revision: D20769039
fbshipit-source-id: e978f6cdb
Summary:
To find a method in non-abstract sub-classes, this diff applies the
same heuristics of inferbo.
* If the class is an interface: Find its unique sub-class and apply the heuristics recursively.
* If the class is an abstract class: Find/use its own summary if possible. If not found, find
one (arbitrary but deterministic) summary from its sub-classes.
* Otherwise: Find its own summary.
Reviewed By: ezgicicek
Differential Revision: D20647101
fbshipit-source-id: 2f8f3ff81
Summary: When looking at some reports I realised that adding the place where the memory becomes unreachable to the trace makes it more readable.
Reviewed By: skcho
Differential Revision: D20790277
fbshipit-source-id: d5df69e68
Jules Villard
Nikos Gorogiannis
Dulma Churchill
Ezgi Çiçek
Sungkeun Cho
David Pichardie
Mitya Lyubarskiy
Anton Kochkov