Summary:
This seems to make sense as it's a separate analysis (that depends on
biabduction). This introduces unpleasant `|| is_checker_enabled TOPL`
whenever we try to figure out if biabduction will run. I think this is a
more general problem that deserves a more general solution to express
the fact that checkers can depend on others, so that, eg,
`is_checker_enabled Purity` is true when we pass `--loop-hoisting`. Will
address in another diff.
Reviewed By: ngorogiannis
Differential Revision: D21618460
fbshipit-source-id: 8b0c9a015
Summary: Later on, this can be changed again or made customizable.
Reviewed By: artempyanykh
Differential Revision: D21618730
fbshipit-source-id: fe517c766
Summary:
Start with tests about dynamic dispatch to test the upcoming
pre-analysis.
Reviewed By: ezgicicek
Differential Revision: D21594496
fbshipit-source-id: 1771ea968
Summary: We mistakenly invalidated the set element which causes spurious vector invalidation errors. Instead, we should modify it without any invalidation.
Reviewed By: jvillard
Differential Revision: D21521943
fbshipit-source-id: 67963967e
Summary:
This diff adds semantics of assume null, heuristics. When `assume(x == null)`, it removes the
methods called on the builder `*x` from the abstract state.
```
x -> {p}
p -> {method1 called}
assume(x == null)
x -> {p}
```
This heuristics is unsound: Even though `x` (a pointer to builder object) points-to an builder
object, which cannot imply that the object `p` does not exist in the concrete semantics. The
unsoundness may appear when there is an alias (see the FP test added).
Reviewed By: ezgicicek
Differential Revision: D21502923
fbshipit-source-id: 2e392bd89
Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array.
Reviewed By: skcho
Differential Revision: D21448322
fbshipit-source-id: 7d44354b5
Summary:
These 2 methods are automatically supplied for all enums, with
predefined behavior and nullability: https://www.geeksforgeeks.org/enum-in-java/
(Note that they are not part of java.lang.Enum class).
This will allow using them in unvetted third part and under strict mode.
Reviewed By: artempyanykh
Differential Revision: D21501716
fbshipit-source-id: 104082d15
Summary:
This diff changes way we treat classes w.r.t. to Nullsafe modes when
issuing meta-issues.
Previously, we considered nested class independently of the outer one.
This was leading to a tricky case: when the class is clean but nested
class needs fixing, meta-info told that class can be Nullsafe.
This is counter-intutive and lead to problems when users tried to follow
wrong nullsafe suggestions for this case.
After this diff we:
1. Start calculating meta-issues only on the outermost level. This will simplify
reasoning about nullsafe stats.
2. Aggregate all nested issues counters to corresponding outer-level class.
Among others, CLASS_CAN_BE_NULLSAFE Advice will finally become
actionable in all known cases.
Reviewed By: artempyanykh
Differential Revision: D21353607
fbshipit-source-id: a17c6958a
Summary:
We have a common entry point where we skip analysis in nullsafe.
This logic is copied from `Reporting.log_issue_from_summary`.
I believe this should not exist in Reporting: it is not the right place
to decide whether to suppress issues: we should not try to report it in
first place.
Because of that we falsely report "needs improvement" meta-issue while
we don't issue any (they were suppressed but participated in needs
improvement count calculations).
Now this change will make meta-issue to be synced with what the user
actually sees.
Down the line we should have a more reliable fix for that.
So far I reviewed suppressing code and looks like we should not suppress
anything else (unless explicitly SuppressLint-ed, which is fine).
Reviewed By: artempyanykh
Differential Revision: D21328634
fbshipit-source-id: 120ce06d1
Summary:
The directory was created to have several sets of nullsafe tests but
there is only one in the end. Remove the redundant "-default".
Reviewed By: mityal
Differential Revision: D21300205
fbshipit-source-id: 46ed8b032
Summary:
The directory names had some interesting variety due to historical
reasons.
- {c,cpp,objc,objcpp}/errors/ date from the time when infer was only
biabduction
- java/infer/ dates from the time when we had an "--analyzer" option and
"infer" was one of them (sic), and eg another was "eradicate".
- c/biabduction/ dates from the time when the biabduction analysis was
being migrated to the "checkers" (AI) framework. For some reasons the
tests there are not a subset of c/infer/ but seem to be entirely new
tests.
The convention now dictates that we should name all of these
*/biabduction/. This diff moves the existing tests from c/biabduction/
into c/biabduction/misc/.
Reviewed By: mityal
Differential Revision: D21300147
fbshipit-source-id: 516d1cb15
Summary:
In the previous diffs, nullsafe behavior was changed to the following:
nested class mode is inherited from the outer class mode.
Though it is possible to e.g. make nested class Nullsafe and outer not,
or make nested class STRICT and outer just LOCAL, this is an edge case
and we don't want to recommend annotating nested classes by default. The
right way is to make outer class Nullsafe instead.
In this decision, we take into account user experience and codebase
readability.
Reviewed By: ngorogiannis
Differential Revision: D21255806
fbshipit-source-id: 0200cb555
Summary:
With this change, set of possibilities will be more actionable. Most
importantly, this will also educate users and make them realize how
Nullsafe trust works.
NOTE: yes, parenthesis are bit clumsy, but it was the easiest way to
make this change and let the phrase remain grammatically correct.
Reviewed By: artempyanykh
Differential Revision: D21231468
fbshipit-source-id: 4b5349fb5
Summary:
In the previous diff we changed the semantics of nested classes w.r.t.
to Nullsafe.
Let's make it clear if users will attempt to misuse it.
Reviewed By: artempyanykh
Differential Revision: D21230717
fbshipit-source-id: 0ecc0dd06
Summary: Similarly to Enum.name, we model Class.getCanonicalName as returning an arbitrary non-empty string.
Reviewed By: ngorogiannis
Differential Revision: D21207120
fbshipit-source-id: 1e2dbd1fd
Summary:
From the user perspective, the current behavior is confusing.
The users intutitively expect the inner class to inherit Nullsafe mode
from the outer one.
Having a class that is Nullsafe but the inner is not is hence dangerous
and misleading.
For the sake of completeness and to support gradual strictification, we
allow the nested class to improse additional strictness. Particularly,
the inner class can be Nullsafe but the outer can be not.
A follow up to this diff will include warnings telling about redundant and wrong usages of nested annotations.
Reviewed By: artempyanykh
Differential Revision: D21228055
fbshipit-source-id: 75755ad1d
Summary:
We model Enum.name as returing a constant name, rather than getting real field names. We did this
because we couldn't think of any big gains, in terms of analysis precision/performance, from getting
the real names.
Reviewed By: ezgicicek
Differential Revision: D21201730
fbshipit-source-id: a2dc01a44
Summary: This diff revises the models of Collection.set and get to handle its elements.
Reviewed By: ezgicicek
Differential Revision: D21201242
fbshipit-source-id: 9c248453d
Summary: Java has this pattern of wrapping non-thread-safe containers in factory methods producing identically-typed results, but wrapped in a synchronised shell. This diff teaches RacerD about some common factory methods and uses the attribute domain to track the dynamic type of their results.
Reviewed By: ezgicicek
Differential Revision: D21155538
fbshipit-source-id: 42ebe6251
Summary: Complete the set of models for java containers that Infer should not report thread safety violations.
Reviewed By: ezgicicek
Differential Revision: D21138280
fbshipit-source-id: 01e1944b6
Summary: Models were partial and/or simply missing (`Map` writes!). Now the modelled containers use inheritance for conciseness (`List` reads are only those not caught by the `Collection` matcher, etc). Also, add URLs to documentation sources.
Reviewed By: ezgicicek
Differential Revision: D21132069
fbshipit-source-id: fefb360f0
Summary: This diff suppresses cost issues on lambda and auto-generated procedures, since they were too noisy.
Reviewed By: ezgicicek
Differential Revision: D21153619
fbshipit-source-id: 65ad6dcc3
Summary:
Replace horrible hack with ok hack.
The main difficulty in implementing the disjunctive domain is to avoid
the quadratic time complexity of executing the same disjuncts over and
over again when going around loops:
First time around a loop, assuming for example a single disjunct `d`:
```
[d]
loop body
[d1' \/ d2']
```
Second time around the same loop: the new pre will be the join of the
posts of predecessor nodes, so `old_pre \/ post(loop,old_pre)`, i.e.
`d \/ d1' \/ d2'`. Now we need to execute `loop body` again
*without running the symbolic execution of `d` again* (and the time after
that we'll want to not execute `d`, `d1'`, or `d2'`).
Horrible hack (before): Disjuncts have a boolean "visited" attached
that does its best to keep track of whether a given disjunct is old or
new. When executing a single *instruction* look at the flag and skip the
state if it's old. Of course we have no way to know for sure so it turns
out it was often wrongly re-executing old disjuncts. This was also
producing the wrong results over even simple loops: only the last
iteration would make it outside the loop for some reason. Overall, the
semantics were pretty untractable and shady at best.
New hack (this diff): only run instructions of a given *node* on
disjuncts that are not physically equal to the "pre" ones already in the
invariant map for the current node.
This gives the correct result over simple loops and a nice performance
improvement in general (probably the old heuristic was hitting the
quadratic bad case more often).
Reviewed By: skcho
Differential Revision: D21154063
fbshipit-source-id: 5ee38c68c
Summary:
1. Package will make the error too verbose.
2. We don't even need to say it is "class" because we say it in the error
description ("Class has 0 issues and can be marked Nullsafe").
Reviewed By: artempyanykh
Differential Revision: D21131998
fbshipit-source-id: 6ccca7615
Summary:
One source of false positives on container races is when the container member field is initialised to a concurrent version in a constructor, but the static type of the field doesn't reflect the thread safety of it.
This solution
- tracks flows from constructors of safe data structures to abstract addresses;
- initialises the initial attribute state when analysing a non-constructor method to that achieved by all constructors/class-initializers.
- checks for that attribute when recording container accesses.
Reviewed By: jvillard
Differential Revision: D21089428
fbshipit-source-id: 02a88f6e8
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:
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:
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:
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: 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:
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:
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:
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:
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:
- 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: 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: 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:
- 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
Jules Villard
David Pichardie
Mitya Lyubarskiy
Ezgi Çiçek
Sungkeun Cho
Nikos Gorogiannis
Daiva Naudziuniene