Summary: Modeling vector iterator with two internal fields: an internal array and an internal pointer. The internal array field points to the internal array field of a vector; the internal pointer field represents the current element of the array. For now `operator++` creates a fresh element inside the array.
Reviewed By: ezgicicek
Differential Revision: D21043304
fbshipit-source-id: db3be49ce
Summary:
The java source file parser should refuse to run on non
.java file. Also, as we expect some autogenerated source files to
break Java official syntax, we catch parsing error silently and
cancel location recording for them.
Reviewed By: jvillard
Differential Revision: D21089587
fbshipit-source-id: 35f1a1e28
Summary:
Now that only races rooted at formals or globals are reported, there is no point using the ownership domain to exclude accesses to locals, so remove the code that initialises the ownership of those.
Also, remove an accidentally quadratic use of `Map.bindings |> List.find` in `FormalMap` and simplify the analysis driver.
Reviewed By: skcho
Differential Revision: D21066855
fbshipit-source-id: 126080778
Summary:
Add a path condition to each symbolic state, represented in sledge's arithmetic domain. This gives a precise account of arithmetic constraints. In particular, it is relation and thus is more robust in the face of inter-procedural analysis.
This is gated behind a flag for now as there are performance issues with the new arithmetic.
Reviewed By: jberdine
Differential Revision: D20393947
fbshipit-source-id: b780de22a
Summary: Move state to summary conversion into the domain file, move a model matcher into the models file and simplify.
Reviewed By: skcho
Differential Revision: D21064351
fbshipit-source-id: bb5b07b6b
Summary:
There are two types of anonymous classes (not user defined classes):
- classic anonymous classes (defined as $<int> suffixes)
- lambda classes (corresponding to lambda expressions). Experimentally,
they all have form `$Lambda$_<int>_<int>`, but the code just uses
`$Lambda$` as a heuristic so it is potentially more robust.
# Problem this diff solves
When generate meta-issues for nullsafe, we are interested only in
user-defined classes, so we merge all nested anonymous stuff to
corresponding user-defined classes and hence aggregate the issues.
Without this diff, for each lambda in the code, we would report this as
a separate meta-issue, which would both screw up stats and be confusing
for the user (when we start reporting mode promo suggestions!).
Reviewed By: artempyanykh
Differential Revision: D21042928
fbshipit-source-id: a7be266af
Summary: In `PowLoc`, we focus on making every constructors of `PowLoc.t` return nomalized value. Thus, it is unnecessary to nomalize any `PowLoc.t` inputs.
Reviewed By: ezgicicek
Differential Revision: D21064893
fbshipit-source-id: d00a7f06b
Summary:
This diff revises how to handle the unknown location in inferbo in two ways:
* stop appending field to the `Unknown` location, e.g. `Unknown.x.a` is evaluated to `Unknown`
* redesign the abstract of multiple locations, like `Bottom` < `Unknown` < `Known` locations
I am doing them in one diff since applying only one of them showed bad results.
Background: `Unknown` was adopted for abstracting all unknown concrete locations, so we could avoid missing semantics of assignments to unknown locations. We tried to keep soundness. However, it brought some other problems related to precision and performance.
1. Sometimes especially when Inferbo failed to reason precise pointer values, `Unknown` may point to many other abstract locations.
2. At that time, value assignments to `*Unknown` makes the situation worse: many abstract locations are updated with imprecise values.
This problem harmed not only its precision, but also its performance since it introduced more location entries in the abstract memory.
Reviewed By: jvillard
Differential Revision: D21017789
fbshipit-source-id: 0bb6bd8b5
Summary: The flags `--biabduction-fallback-model-alloc-pattern` and `--biabduction-fallback-model-free-pattern` were unused because we removed the models from .inferconfig a while ago because of too many false positives. We are implementing a better memory leak check based on Pulse, and are adding the similar flags `--pulse-model-alloc-pattern` and `--pulse-model-free-pattern`.
Reviewed By: jvillard
Differential Revision: D21061511
fbshipit-source-id: 1b3476c22
Summary:
Instead of having to remember to update both the inferbo and the concrete
intervals domains of pulse, hide these details under a unified API. This
should help the transition to adding a third(!) numerical domain later
on (pudge!).
Reviewed By: ezgicicek
Differential Revision: D21022920
fbshipit-source-id: 783157464
Summary:
Now that the shape of the record type of AbductiveDomain.t is known, we
don't need this getter anymore. Keep `get_pre` and `get_post` as they
perform useful casting to `BaseDomain.t`.
Reviewed By: ezgicicek
Differential Revision: D21022924
fbshipit-source-id: 340f4edf8
Summary:
The "interface" modules define short forms for the internals of pulse
and also serve as a guide of which modules you are supposed to use at
which "level" in the pulse domains (base domain vs abductive domain vs
higher-level PulseOperations.ml). Make sure they are used.
Reviewed By: skcho
Differential Revision: D21022927
fbshipit-source-id: f890df245
Summary:
PulseAbductiveDomain.ml can be split into two distinct parts:
1. The definition of the "abductive domain" itself. This remains in that
file.
2. How to apply a given pre/post pair to the current state (during a
function call). This is about the same size as 1. in terms of lines
of code(!) and is now in PulseInterproc.ml.
Reviewed By: ezgicicek
Differential Revision: D21022921
fbshipit-source-id: 431fe061e
Summary:
I'm moving this code in the next diff and need this refactor. It should
be the same as before.
Reviewed By: ezgicicek
Differential Revision: D21022926
fbshipit-source-id: ebe644ef9
Summary:
See the code comment re: why don't we also recommend "strict" at this
stage. We can always change it later when we think users are happy with
strict.
Reviewed By: artempyanykh
Differential Revision: D21039553
fbshipit-source-id: 758ccf32c
Summary:
Having copypaste is painful to support. Lets make .mli the source of
truth.
Improved docs a bit, while I was here.
Reviewed By: artempyanykh
Differential Revision: D20948916
fbshipit-source-id: 1668dbc9c
Summary:
This diff is a step forward to the state when the list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes a case when we incorrectly defined possible promo mode (see
the test payload)
Reviewed By: artempyanykh
Differential Revision: D20948897
fbshipit-source-id: 616b96f96
Summary:
See the comments in the code why it makes logical sense.
This diff is a step forward the state when list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes majority of cases in ModePromotions.java
Reviewed By: artempyanykh
Differential Revision: D20948656
fbshipit-source-id: 82c0d530b
Summary:
Currently we exlude only if the method is based on deprecated config
packages.
Lets use the proper method, which covers both cases (config +
user-defined third party repo).
Reviewed By: artempyanykh
Differential Revision: D20946506
fbshipit-source-id: c3332667f
Summary:
Previously, we learned to detect if Default mode class can be made
Nullsafe(LOCAL).
Lets generalize it and calculate the precise mode.
NOTE 1: We don't distinct shades of "Trust some". We also don't
recommend trust some and recommend "Trust all" instead.
NOTE 2: As you can see from the test payload (see ModePromotions.java),
the precise calculation is not working as expected. This is due to a bug
in nullsafe implementation/design. See follow up diffs that will fix
this test.
Reviewed By: artempyanykh
Differential Revision: D20941345
fbshipit-source-id: 2255359ba
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
Summary:
`IssueLog` is used by the file-level analysis callbacks to store reports outside error logs so as to avoid racing on spec files. Each file should generate a single issue log which is then written to an appropriate file. The starvation checker was breaking that contract because it ostensibly needs to write out multiple issue files when analysing a single source file.
This is unnecessary, because the existing mechanisms for deduplication ensure only one issue file needs to be written out.
The whole-program mode still needs that capability, but this is implemented outside the file-analysis callback.
Reviewed By: mityal
Differential Revision: D20736135
fbshipit-source-id: 620e5484d
Summary:
Sometimes buck emits a timestamp, leading to a crash
> External Error: Failed to parse `buck targets --show-output ...` line of output:
> 2020-03-30 20:03:51
Reviewed By: dulmarod
Differential Revision: D20766438
fbshipit-source-id: 47cc00150
Summary:
OCaml 4.10.0 flagged that the `Extension` functor argument was unused.
Delete it and remove one layer of module in the file too now that it
doesn't need to be a functor.
Reviewed By: mityal
Differential Revision: D20669652
fbshipit-source-id: 089043d7d
Summary:
1. The return value is annotated as Nullable in codebase
2. The second parameter can be null as well.
Reviewed By: artempyanykh
Differential Revision: D20766243
fbshipit-source-id: 9aad37a8c
Summary:
This was needed countless of times. We log current signature, but not
callees.
Reviewed By: dulmarod
Differential Revision: D20765107
fbshipit-source-id: 399926c65
Summary:
This declaration is heavily used in Guava library.
Quick inspection shows that majority of methods are annotated correctly.
This will hide previosly hidden unsoundness issues in the codebase.
Reviewed By: artempyanykh
Differential Revision: D20737104
fbshipit-source-id: aa048bfc1
Summary:
The attribute `[no_return]` signifies that a function doesn't return. Previously, pre-analysis had cut the links to successor nodes of such no-return function nodes. This was intended to help with suppressing reporting on unreachable paths for some analyses. However, this results in having these nodes as dangling, with no connection to exit nodes.
This diff additionally shortcuts these no-return function nodes to exit node. This would allow us to enhance inter-procedural analyses like pulse to kepp track of paths that do not return since we will be keeping their connections at exit node rather than completely cutting them of as before. It would also allow us to assume that all paths start at the one start node and end at the one exit node (at least syntactically in the CFG).
Reviewed By: skcho
Differential Revision: D20736043
fbshipit-source-id: 0eace1bdb
Summary:
D20416859 introduced a new utility
`Process.create_process_and_wait_with_output` that:
1. executes the process to completion
2. reads stdout in full
3. reads stderr in full
Unfortunately, writing to stdout/stderr can be a blocking operation for
the callee process in that situation. Double unfortunately, reading both
stdout and stderr in a way that avoids starvation requires sophisticated
Unix-fu. Fortunately, callers of this utility only ever need to read
*one* of stdout or stderr.
Fix the starvation by:
1. reading *one* channel only (either stdout or stderr)
2. doing the reading *before* `wait`ing on the process to finish
3. redirecting the other channel to the console
Reviewed By: skcho, ngorogiannis
Differential Revision: D20737388
fbshipit-source-id: 2988ac865
Summary:
Knowing the number associated with each issue is useful to pass to
`infer explore --select XXX`.
Reviewed By: skcho
Differential Revision: D20696724
fbshipit-source-id: f6f368aa1
Summary:
Used `2to3` but had to (poorly, sorry!) fix byte -> string output of processes.
update-submodule: facebook-clang-plugins
Reviewed By: ngorogiannis
Differential Revision: D20672767
fbshipit-source-id: 852c7e973
Summary:
infer/lib/python/'s not pinin'! It's passed on! This library is no more!
It has ceased to be! It's expired and gone to meet its maker! It's a
stiff! Bereft of life, it rests in peace! If you hadn't nailed it to the
perch it'd be pushing up the daisies! 'ts metabolic processes are now
'istory! It's off the twig! It's kicked the bucket, it's shuffled off
its mortal coil, run down the curtain and joined the bleedin' choir
invisible!! THIS IS AN EX-PYTHON!!
Reviewed By: ngorogiannis
Differential Revision: D20672771
fbshipit-source-id: 7808c0ece
Summary:
Re-implement the generation of an HTML report (with bug traces) in
OCaml.
Kills the --only-show as a side-effect, it is of dubious use since there
is already infer-out/report.txt to get the report list as text. A
follow-up diff adds numbers to the list in infer-out/report.txt for easy
cross-referencing with `infer explore --select 123`.
Reviewed By: skcho
Differential Revision: D20672769
fbshipit-source-id: 39b3a299d
Summary:
When executing unit tests, don't parse the arguments as they will be
parsed by OUnit.
Reviewed By: skcho
Differential Revision: D20669675
fbshipit-source-id: 897ec10ee
Summary:
The text is ambiguous because it sounds as if it recommends annotating the current class as `ThreadSafe`, not the interface invoked.
Also, remove the not useful part "or using an interface known to be thread-safe" because developers don't know in general what interfaces Infer thinks are thread-safe.
Reviewed By: skcho
Differential Revision: D20675729
fbshipit-source-id: 9da438621
Summary:
Morally, INTERFACE_NOT_THREAD_SAFE is issued when an interface method is invoked from `ThreadSafe`-annotated code on an interface that is not known to be thread-safe or annotated so.
However, the ultimate purpose is to prevent races. Thus it should never be issued on an owned object or on objects we would not report races on for any reason (local variables, non-source variables, etc).
This diff equips interface call records with the abstract address they are invoked on, and uses the same rules for maintaining those records or not.
Reviewed By: skcho
Differential Revision: D20669259
fbshipit-source-id: 6c7841e6a
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff improves the domain interface and consolidates all the various validity invariant checking for accesses inside their constructors.
Reviewed By: skcho
Differential Revision: D20668611
fbshipit-source-id: 45806d40d
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff inverts 2 and 1.
Reviewed By: skcho
Differential Revision: D20644100
fbshipit-source-id: 89d810b68
Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. `Access`, the abstract addressed accessed and the type of access.
This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.
This diff introduces functions in (1) that mask calls to (2), making the flip easier.
Reviewed By: skcho
Differential Revision: D20619614
fbshipit-source-id: 19fda0916
Summary: In an intra-procedural analysis we assume that parameters passed by reference to a function will be initialized inside that function. We use the type information of an actual parameter to initialize the fields of the struct. This does not work if a function has a parameter of type void* as the actual parameters also has type void*. To solve this issue, we use type information from local variables.
Reviewed By: jvillard
Differential Revision: D20670253
fbshipit-source-id: dc9f051ef
Summary:
This diff adds a procedure name to the head of the trace in order to distinguish issues in the same line.
"Updated Cost is ..." is changed to "Updated Cost of <proc name> is ..."
Reviewed By: ezgicicek
Differential Revision: D20672214
fbshipit-source-id: 303b4492f
Summary:
- Model `System.exit()` as early_exit and add a test
- Tweak message of methods that are impure due to having no pulse summary (and add a test)
Reviewed By: skcho
Differential Revision: D20668979
fbshipit-source-id: 6b5589aae
Summary:
Introducing a generalization of map_changed that can now
use a context on each instruction. The context is computed with
the previous instructions in the collection.
Reviewed By: skcho, jvillard
Differential Revision: D20669993
fbshipit-source-id: 58fdee1d9
Summary: This diff avoids that an invalid interval value, e.g. [0, -1], is genrated by interval pruning.
Reviewed By: ezgicicek
Differential Revision: D20645488
fbshipit-source-id: 6516c75d1
Summary:
Hopefully no one uses this. This is in Python and we'd like to get rid
of it. Easy enough to either re-implement if needed or to be
re-implemented by a third party.
Reviewed By: ngorogiannis
Differential Revision: D20626344
fbshipit-source-id: 484022482
Summary:
Seems like a more sensible name. Most tooling should read report.json so
won't notice.
Still output a bugs.txt file with a message to point to report.txt while
people migrate.
Reviewed By: mityal, artempyanykh
Differential Revision: D20626111
fbshipit-source-id: efb84d098
Summary:
The documentation of `--quiet` dates back from when it applied only to
`InferPrint.ml`. Make it more general and more in line with
expectations one might have about a `--quiet` option:
- change the doc
- make it disable the progress bar
Reviewed By: ngorogiannis
Differential Revision: D20626110
fbshipit-source-id: db096fd31
Summary:
This is a fairly popular class that have bunch of nullable methods.
Providing an alternative will make an error message actionable.
Note that this involves some duplication, and the whole API could be
improved. But let's leave it for future improvements.
Reviewed By: jvillard
Differential Revision: D20649099
fbshipit-source-id: bfcc7fd95
Summary: The current message is recommending to change `View.findViewById()` to `View.requireViewById()`, but the latter method is not supported in all API, so might lead to a crash in runtime.
Differential Revision: D20619361
fbshipit-source-id: 542746c79
Summary: Use the an LRUCache in Ondemand.LocalCache to avoid clearing it after every toplevel analysis.
Reviewed By: ngorogiannis
Differential Revision: D20281932
fbshipit-source-id: 752c8e1ea
Summary:
- the order of call state was wrong when printing contradiction for CItv
- add a test for impurity
Reviewed By: jvillard
Differential Revision: D20646181
fbshipit-source-id: 1c86fd0a4
Summary: There are no plans currently to track which lock protects each access, so reduce to the functional equivalent of having a singleton lock domain.
Reviewed By: skcho
Differential Revision: D20595013
fbshipit-source-id: d5100ac49
Summary:
As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by:
- discovering aliasing in memory
- widening limited number of times in loops and concluding that loop exit conditions are never taken
However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts:
```
Pulse: 1 pre/post(s)
#0: PRE:
{ roots={ };
mem ={ };
attrs={ };}
POST:
{ roots={ };
mem ={ };
attrs={ };}
SKIPPED_CALLS: { }
```
The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure.
Reviewed By: skcho
Differential Revision: D20619504
fbshipit-source-id: 3a8502c90
Summary:
Although try-with-resource is supported by nullsafe this code pattern
throws it off and make nullsafe report on a virtual **b**yte-**c**ode
variable.
Check out debug output from `TryWithResource` (or attached
visualisation of CFG):
0. node14: $bcvar2=null (on entry to try-with-resource).
1. node16: n$14=$bcvar2, but **also** PRUNE(!(n$14 == null), true). Then we go to
2. node18: do something here and in case of exception go to
3. node25->node23->node19->node20: and here we do
$bcvar2->addSuppressed(...).
Because on step 1 we refined nullability of n$14, but didn't refine
nullability of $bcvar20, on step 3 we are sure that $bcvar is null and
therefore issue an error.
Reviewed By: mityal
Differential Revision: D20558343
fbshipit-source-id: 520505039
Summary:
This is likely not the final refinement, rather one step forward.
We classify all classes by 3 categories:
- Nullsafe and 0 issues
- can add Nullsafe and will be 0 issues
- the rest (class needs improvement)
Each class will fall into exactly one category.
Error messaging is WIP, they are not intended to be surfaced to the user
just yet.
Note how this diff uses the result of the previous refactoring.
Reviewed By: artempyanykh
Differential Revision: D20512999
fbshipit-source-id: 7f462d29d
Summary: Add a flag `is-inclusive-cost` (`true` by default) which computes inclusive cost for each function. Setting the flag to `false` computes exclusive cost of the function where the cost of the callees are assumed to be `0`.
Reviewed By: skcho
Differential Revision: D20558275
fbshipit-source-id: 6b5798916
Summary:
This function is used to adapt the callee summary at a call site. It did two things for every domain element in the callee summary:
- A linear search through the list of actuals.
- For each such actual, it would (repeatedly) compute its ownership (!).
For large summaries this can be substantial. The right way is to precompute the ownership for all actuals once and then simply retrieve it (via an array).
Reviewed By: jberdine
Differential Revision: D20564447
fbshipit-source-id: 1ca3121c2
Summary: The attribute types present are exclusive, so sets are not needed for the attribute map domain. This changes `Attribute` to a flat domain and removes the set on top of that.
Reviewed By: jberdine
Differential Revision: D20560240
fbshipit-source-id: 83e59d73e
Summary:
Both modules define properties the analysis maps to addresses, there is no reason to have two modules for this.
Also remove an instance of `Caml.Not_found` usage.
Reviewed By: jberdine
Differential Revision: D20558683
fbshipit-source-id: eacafd780
Summary:
# Problem
Consider
```
some_method(Object a) { a.deref(); }
```
What is nullability of `a` when we dereference it?
Logically, things like "LocallyCheckedNonnull" etc are not applicable
here.
This would be applicable if we called some_method() outside! But not
inside. Inside the function, it can freely treat params as non-null, as
long they are declared as non-nullable.
The best we can capture it is via StrictNonnull nullability.
Reviewed By: artempyanykh
Differential Revision: D20536586
fbshipit-source-id: 5c2ba7f0d
Summary:
# Problem
Yes, nullsafe is not null-safe, such an irony.
ErrorRenderingUtils overuses `option` and `let+` constructions. Most of
internal functions can return `None` when "something is wrong".
On top of this, "default" pattern match is overused either.
Because of this, `ErrorRenderingUtils.mk_nullsafe_special_issue` returns
optional type. In practice, this result can be None for many unclear
reasons, and it is super tricky to even understand them all.
This in turn forced AssignmentRule and DereferenceRule to process this
None is defensive way. The rules have some theory why None was returned,
and have assertions along the way.
Turns out those theories might be wrong. This diff will make triaging wrong assumptions easier.
Reviewed By: artempyanykh
Differential Revision: D20535720
fbshipit-source-id: 2b81e25b7
Summary: When we have clashing args to bug (for instance -j and -Xbuck --num-threads) CLI passed -Xbuck args should win.
Reviewed By: jvillard
Differential Revision: D20557060
fbshipit-source-id: 726fc501a
Summary:
`make test` failed in some test directories, because we were getting warnings
```
Foo.java uses unchecked or unsafe operations.
```
This diff fixes or suppresses these warnings.
Reviewed By: skcho
Differential Revision: D20557572
fbshipit-source-id: 63ecd3dfa
Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.
Reviewed By: jvillard
Differential Revision: D20444097
fbshipit-source-id: 33b6b25a2
Summary:
- Add more naive pulse models for:
- `System.arraycopy`
- `StringBuilder.setLength`
- `StringBuilder.delete`
- Model the following as pure
- `SparseArrayCompat.valueAt`
- `File.get...`
- Add a nice test
Reviewed By: jvillard
Differential Revision: D20513397
fbshipit-source-id: 6d412d13a
Summary:
`to_reportable_violation` is responsible for identifying if the
violation is reportable in this mode or not.
This logic is higly coupled with other functions in
`ReportableViolation`, such as `get_description`: You can not have
sensible description on the violation that is NOT reportable in a given
mode.
So from logical perpsective, creation of `ReportableViolation.t` should
belong to this module itself, not to the parent `Rule` module.
This change will make design clearer.
Reviewed By: artempyanykh
Differential Revision: D20511756
fbshipit-source-id: ef27b5057
Summary:
This diff finishes work in D20491716.
We removed dependency on nullsafe mode for field initialization in
D20491716, so this diff just formalizes it.
Reviewed By: jvillard
Differential Revision: D20493164
fbshipit-source-id: 6ac612e78
Summary:
This diff continues work in D20491716.
This time for Inheritance Rule.
Reviewed By: jvillard
Differential Revision: D20492889
fbshipit-source-id: c4dfd95c3
Summary:
This diff continues work in D20491716.
This time for Dereference Rule.
Reviewed By: jvillard
Differential Revision: D20492296
fbshipit-source-id: ff7f824f9
Summary:
# Problem
In current design, Rules (assignment rule, dereference rule, inheritance
rule) decide, depending on the mode, wether the issue is legit or not.
If the issue is not actionable for the given mode, it won't be created
and registered.
For meta-issues, we want to be able to do smart things like:
- Identify if we can raise strictness of the mode without
introducing new issues
- Classify classes on "clean" vs "broken", taking into account issues
that are currently invisible.
# Solution
In the new design:
1. Rules are issuing violations independently of mode. This makes sense
semantically. Mode is "level of trust we have for suspicious things",
but the thing does not cease to be suspicious in any mode.
2. Each Rule decides if it is reportable or not in a given mode.
3. `nullsafe_mode` is passed to the function `register_error`, that 1)
adds error so it can be recorded in summary for file-level analysis
phase 2) reports some of them to the user.
# This diff
This diff converts only AssignmentRule, follow up will include
conversion of other rules, so no issue encapsutes the mode.
Reviewed By: jvillard
Differential Revision: D20491716
fbshipit-source-id: af17dd66d
Summary:
`make deadcode` is failing on master but our CI jobs didn't catch it :(
Let's fix existing deadcode for now.
Reviewed By: martintrojer
Differential Revision: D20510062
fbshipit-source-id: 4a5e5f849
Summary:
Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals. However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes.
For instance, for the following functions
```
public static boolean is_null(Byte a) {
return a == null;
}
public static boolean call_is_null(Byte a) {
return is_null(a);
}
```
We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts):
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null,
BoItv ([max(0, v2), min(0, v2)]),
WrittenTo-----------WRONG },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1),
WrittenTo-----------WRONG },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1) },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
Reviewed By: skcho
Differential Revision: D20490102
fbshipit-source-id: 253d8ef64
Summary:
Make all arguments named and move function from `Procname.Java` to `Procname`, and making it return a `Procname.t` as opposed to `Procname.Java.t` (all callers want a `Procname` eventually).
Various other small fixes in the callers.
Reviewed By: skcho
Differential Revision: D20492305
fbshipit-source-id: e646cc799
Daiva Naudziuniene
David Pichardie
Nikos Gorogiannis
Jules Villard
Sungkeun Cho
Mitya Lyubarskiy
Dulma Churchill
Ezgi Çiçek
Fernando Gasperi Jabalera
Artem Pianykh
Martin Trojer