Summary: `litho` checker contained two checkers: required-props and graphQL field accesses. Although they use the same domain, their reporting conditions and analysis details are different. However, they were bundled into the same analysis by adding disjunctions to `exec_instr` to handle both cases. Let's separate them into two different checkers, keeping a modular transfer function and analyzer that is reused by these two checkers.
Reviewed By: skcho
Differential Revision: D17788834
fbshipit-source-id: 47d77063b
Summary: The regexp would match `ge` and is also unnecessary and was compiled on every call. Save some cpu cycles while fixing it.
Reviewed By: jvillard
Differential Revision: D17789586
fbshipit-source-id: a3f6612c6
Summary:
At some point it was thought that we can assume that any annotation starting with "On" means the method is on the UI thread.
That's too imprecise and has led to false positives and negatives. Restrict to a well-known safe set.
Reviewed By: ezgicicek
Differential Revision: D17769376
fbshipit-source-id: 0f8fee059
Summary:
Currently, lock state is a map from locks to stacks of lock acquisitions.
Since we now have the separate acquisitions component, we no longer need to
remember the stack of acquisitions for a lock. Instead we only need a lock count,
thus reducing the memory footprint.
At the same time, change acquire and release so that they make one tree operation per
component (map/acquisition) as opposed to two (search/update) operations.
Reviewed By: ezgicicek
Differential Revision: D17736727
fbshipit-source-id: 7579eb61e
Summary:
If we acquire n nested locks we end up with n critical pairs, and for each pair the held-locks component goes up linearly, thus total space/time is O(n^2).
If the sets of held-locks are constructed with maximal sharing (intuitively, if they derive from the same set by additions) then the total space/time is O(n logn).
To do this, we must avoid constructing a new set every time we ask what the currently held locks are. Here we maintain (care is needed in the presence of recursive locks) that set across lock acquisitons and removals.
Reviewed By: skcho
Differential Revision: D17736252
fbshipit-source-id: 0f9b292c4
Summary:
This diff tries to narrowing the fixpoint of outermost loops, so that over-approximated widened values do not flow to the following code.
Problem: There are two phases for finding a fixpoint, widening and narrowing. First, it finds a fixpoint with widening, in function level. After that, it finds a fixpoint with narrowing. A problem is that sometimes an overly-approximated, imprecise, values by widening are flowed to the following loops. They are hard to narrow in the narrowing phase because there is a cycle preventing it.
To mitigate the problem, it tries to do narrowing, in loop level, right after it found a fixpoint of a loop. Thus, it narrows before the widened values are flowed to the following loops. In order to guarantee the termination of the analysis, this eager narrowing is applied only to the outermost loops.
Reviewed By: ezgicicek
Differential Revision: D17740265
fbshipit-source-id: e2d454036
Summary:
This diff extends the alias domain to analyze loop with list comprehensions form in Java precisely.
```
list2 = new List();
for (Element e : list1) {
list2.add(e);
}
```
1. `IteratorOffset` is a relation between a iterator offset and a length of another array. For example, in the above example, after n-times of iterations, the offset of the iterator (if it exists) and the length of `list2` are the same as `n`.
2. `IteratorHasNext` is a relation between iterator and its `hasNext` result.
3. At the conditional nodes, it prunes the alias list length of `list2` by that of `list1`.
* if `hasNext(list1's iterator)` is true, `list2`'s length is pruned by `< list1's length`
* if `hasNext(list1's iterator)` is false, `list2`'s length is pruned by `= list1's length`
Reviewed By: ezgicicek
Differential Revision: D17667128
fbshipit-source-id: 41fb23a45
Summary: This diff fixes a potential race in writing to pipe channel.
Reviewed By: ngorogiannis
Differential Revision: D17710123
fbshipit-source-id: 477492750
Summary:
The old domain keeps two sets:
- `events` are things (including lock acquisitions) which eventually happen during the execution of a procedure.
- `order` are pairs of `(lock, event)` such that there is a trace through the procedure which at some point acquires `lock` and before releasing it performs `event`.
A deadlock would be reported if for two procedures, `(lock1,lock2)` is in `order` of procedure 1 and `(lock2,lock1)` is in `order` of procedure 2. This condition/domain allowed for the false positive fixed in the tests, as well as was unwieldy, because it required translating between the two sets.
The new domain has only one set of "critical pairs" `(locks, event)` such that there is a trace where `event` occurs, and *right before it occurs* the locks held are exactly `locks` (no over/under approximation). This allows keeping all information in one set, simplifies the procedure call handling and eliminates the known false positive.
Reviewed By: mityal
Differential Revision: D17686944
fbshipit-source-id: 3c68bb957
Summary: Holding a master lock and then acquiring two other locks inside can generate a false positive as shown.
Reviewed By: mityal
Differential Revision: D17710076
fbshipit-source-id: 5bc910ba2
Summary:
Previously deduplication was always on which is not great for testing.
Also split tests so that we can still test deduplication separately.
Reviewed By: mityal
Differential Revision: D17686877
fbshipit-source-id: 280d91473
Summary:
The documentation and uses of filtering disagree. One typical usage is deduplication.
Split that where obvious, add comments where not obvious, and leave alone when obviously unrelated to deduplication.
Reviewed By: mityal
Differential Revision: D17715329
fbshipit-source-id: ec757927b
Summary:
Ideally the analyser should equate locks `this.x.f` and `a.x.f` in different methods if they can alias.
The heuristic removed here was rarely used and is in the way of a re-write of the analysis.
It was also badly implemented, as this should ideally be the comparison relation of `Lock`.
Reviewed By: mityal
Differential Revision: D17602827
fbshipit-source-id: 4f4576c1a
Summary:
This diff generates a symbolic value when a function returns only
exceptions. Previously, the exception expression is evaluated to top,
thus it was propagated to other functions, which made those costs as
top. For preventing that situation, this diff changed:
* exception expressions are evaluated to bottom, and
* if callee's return value is bottom, it generates a symbolic value
for it.
Reviewed By: ezgicicek
Differential Revision: D17500386
fbshipit-source-id: 0fdcc710d
Summary: This diff introduces an inequality for the size alias targets, in order to get preciser array lengths after loops. The alias domain in inferbo was able to express strict equality between alias source and its targets, e.g. x=size(array). Now, for the size alias target, it can express less than or equal relations, e.g. x>=size(array).
Reviewed By: ezgicicek
Differential Revision: D17606222
fbshipit-source-id: 2557d3bd0
Summary: Component.Builder has its own non-required props that are inherited by the MyComponent.Builder. Add tests where these common props are set in the chain of calls.
Reviewed By: Katalune
Differential Revision: D17710294
fbshipit-source-id: f3c5ef28c
Summary:
This reverts commit 9d5c322202a479e73b60f00ffb318f1c7948e407.
INFERVERSION forcing a version check proved to be problematic for
integrations, thus is reverted.
Reviewed By: ngorogiannis
Differential Revision: D17627638
fbshipit-source-id: f988207aa
Summary:
This diff is to refactoring some stuffs for the following diff.
* revised pretty print of the alias domain
* moved `eval_array_locs_length` to `BufferOverrunSemantics`.
Reviewed By: jvillard
Differential Revision: D17667123
fbshipit-source-id: c95611df5
Summary:
Sawja and Javalib have recently released new versions that drop off
the camlp4 dependency. This is a minimal diff in order to update infer
opam depedencies.
Last (1.5.7) generates invokedynamic, but work on InvokeDynamic is still
in progress in Infer and not activated here yet. In this version, the
Java frontend will still replace any InvokeDynamic by a dummy
InvokeStatic call (as introduced by Jeremy a long time ago).
Reviewed By: jvillard
Differential Revision: D17662979
fbshipit-source-id: f686ba442
Summary:
Unfortunately it is very hard to predict when
`Typ.Procname.describe` will add `()` after the function name, so we
cannot make sure it is always there.
Right now we report clowny stuff like "error while calling `foo()()`",
which this change fixes.
Reviewed By: ezgicicek
Differential Revision: D17665470
fbshipit-source-id: ef290d9c0
Summary:
Having just numbers for abstract values is a tad confusing. The change
is also needed for having actual constant values later.
Reviewed By: ezgicicek
Differential Revision: D17665469
fbshipit-source-id: 20dff7bbe
Summary: `Prop(varArg = myProp) List <?> myPropList` can also be set via `myPropList()` or `myProp()`. Add support for picking up the `varArg` and checking this form of required props.
Reviewed By: ngorogiannis
Differential Revision: D17571997
fbshipit-source-id: 7956cb972
Summary:
Turns out `Memory.add_attributes` was only used to add singletons so
deleted that in the process.
Reviewed By: skcho
Differential Revision: D17627725
fbshipit-source-id: 0abe3889d
Summary:
This was bogus: when evaluating `e[e']` we were checking that `e'` is a
valid pointer.
Reviewed By: ezgicicek
Differential Revision: D17627727
fbshipit-source-id: 536384e95
Summary:
This is a preparation for coming introducing of Unknown nullability.
When this happens, a value will be able to be neither nullable, nor
non-nullable.
This will break many checks that implicitly assume "not nullable means non-null".
In this diff, we review all such checks and change them accordingly.
Reviewed By: artempyanykh
Differential Revision: D17600177
fbshipit-source-id: c38d87175
Summary:
It took a while for me to figure out what does this method do; the
reasons were:
1. a lot of names were cryptic and/or misleading
2. because everything is inline one needs to read everything to figure
out what is going on here.
So this diff changes the names a bit and moves some of methods outside.
This is still far not perfect, but I believe it is better than was
before.
Reviewed By: artempyanykh
Differential Revision: D17600175
fbshipit-source-id: ca7175b2e
Summary:
Eradicate.ml is way too big to reason about.
This diff is shallow, it does only the following:
1. Moves the module
2. Adds documentation in the header.
3. Exports two public methods as is
4. Adds corresponding params to all methods for values that were
captured in the module-as-closure before
Reviewed By: artempyanykh
Differential Revision: D17600173
fbshipit-source-id: ba7981228
Summary:
Turns out, we did not have such a test in place.
Known issue: we report over-annotated warnings for each fields N times,
one per constructor, which is wrong.
Reviewed By: artempyanykh
Differential Revision: D17574791
fbshipit-source-id: def992691
Summary:
Now, that we consistently use `AnnotatedType`, `AnnotatedNullability`,
and `AnnotatedSignature`, `AnnotatedField` is a natural name for this
datatype.
Together `AnnotatedSignature` and `AnnotatedField` represent two entry
points for fetching information about Java type from the codebase.
Reviewed By: artempyanykh
Differential Revision: D17570534
fbshipit-source-id: 31ef52033
Summary:
1. This diff finishes the work of getting rid of using `Annot.Item.t`
for making judgements about nullability. Instead, `AnnotatedNullability`
is now used consistently in the codebase. Corresponding TODO items are
deleted.
2. This diff proceeds consolidating checks to `NullsafeRules` (which
will simplify introducing non-binary nullability in follow up diffs).
3. Code is simplified: we get rid of `fold2/ignore` + inlined
calculation of the param position in favor of
more straightward `zip` + `iteri` combo.
Reviewed By: artempyanykh
Differential Revision: D17570439
fbshipit-source-id: 52acf2c66
Summary:
This continues work of getting rid of using low-level Annot.Item.t in
favor of a new, more specific and flexible data structure.
Migrating this code further to NullsafeRules is bit tricky right now, so
let's defer it.
Reviewed By: ngorogiannis
Differential Revision: D17549479
fbshipit-source-id: 418b4b394
Summary:
This diff also introduces "subtyping function" into NullsafeRule, which
will be the core check for other rules we will introduce in follow up
diffs
Reviewed By: ngorogiannis
Differential Revision: D17500466
fbshipit-source-id: 5821caa6e
Summary:
As suggested by artempyanykh:
1. Since we recently introduced InferredNullability, AnnotatedNullability deserves its own class which now plays nicely with its counterpart.
2. AnnotatedType is more specific then NullsafeType
Reviewed By: artempyanykh
Differential Revision: D17547988
fbshipit-source-id: 785def23a
Summary: The analysis is not intra-procedural, hence we don't really read the payload. Let's remove it.
Reviewed By: ngorogiannis
Differential Revision: D17603911
fbshipit-source-id: c92b5c602
Summary:
This diff avoids giving the top value to unknown globals in Java,
because they harm precision of the cost checker. Instead, it doesn't
subst the global symbols at function calls.
Reviewed By: ezgicicek
Differential Revision: D17498714
fbshipit-source-id: d1215b3aa
Summary:
This diff adds an eval mode for the substitutions of the cost results, in order to avoid precision
loss by joining two symbols.
The usual join of two different symbolic values, `s1` and `s2`, becomes top due to the limitation of
our domain. On the other hand, in the new eval mode, it returns an upperbound `s1+s2`, because the
cost values only care about the upperbounds.
Reviewed By: ezgicicek
Differential Revision: D17573400
fbshipit-source-id: 2c84743d5
Summary:
This was causing a crash, because when trying to create a procname from a block at that point we don't have the block return type, which is needed for the name. I don't understand why BlockDecl doesn't contain the type, but I looked again and it doesn't (also in clang). So in general we need to pass it from the context, but that's not possible in this case.
Also, one could argue that such a block is not a method from the struct, since it's just a block that is assigned to a field as initialization.
Reviewed By: skcho
Differential Revision: D17575197
fbshipit-source-id: 3974ead3f
Summary: When we have an annotation like `Prop(varArg = X)` or ` ThreadSafe(enableChecks = true)`, we were not able to pick up the names of the parameters like `varArg` or `enableChecks`. This diff fixes that.
Reviewed By: skcho, ngorogiannis
Differential Revision: D17571377
fbshipit-source-id: 5293b5810
Summary:
Events can be many things, including lock acquisitions. Lock state keeps a set of events, all of which must be lock acquisitions.
Enforce this via the type checker by specialising the types so that lock state satisfies this by construction.
Reviewed By: ezgicicek
Differential Revision: D17571428
fbshipit-source-id: 2f5a33b98
Summary:
Instead of polluting the signature of trace endpoints, have
the call printer be a module argument to the functors
producing trace elements.
Reviewed By: skcho
Differential Revision: D17550111
fbshipit-source-id: ab5af94c6
Summary:
This proceed the work of getting rid of Annot.Item.t.
This diff:
- Moves "check assignment rule" to recently supported NullsafeRules
- Implements their own "check overannotated" (defers consolidating this
check into NullsafeRule for the future diffs).
Note that we don't need PropagatesNullable logic anymore because it is
already ported to NullsafeType (return value will be marked as Nullable
in NullsafeType)!
implicit_nullable (a.k.a. Void types) will require a follow up diff to
model.
Reviewed By: artempyanykh
Differential Revision: D17499246
fbshipit-source-id: 14b473f29
Summary:
In nutshell, Nullsafe is driven by relatively simple set of rules.
It is currently not well reflected in code: we are duplicating the same logic in different places, which is:
- error prone (we need to adjust ensure all places are addressed if a new feature is introduced)
- complicates understanding of nullsafe
Consolidating checks will simplify introducing Unknown Nullability and
strict/partial check modes.
## this diff
This diff does it for one particular check.
See follow up diffs re that proceed consolidation.
## future diffs
Future diffs will:
- consolidate other checks that use 'assignment rule'
- introduce other rules, most notably 'dereference rule' and
'inheritance rule'
Reviewed By: artempyanykh
Differential Revision: D17498630
fbshipit-source-id: 079d36518
Summary:
Now, after series of modifications with TypeAnnotation, we are ready to
rename it to reflect what it means in the code.
See the documentation in the class for details.
Also:
- renamed methods for clarity
- added some documentation
- renamed local variables around the usages
Reviewed By: jvillard
Differential Revision: D17480799
fbshipit-source-id: d4408887a
Summary:
This continues work for eliminating Annot.Item.t from Nullsafe low-level
code.
The introduced function `from_nullsafe_type` is called when we infer
initial type of the equation based on the function or field formal signature.
Before that, we did it via reading the annotation directly, which
complicates the logic and making introducing Unknown nullability tricky.
## Clarifying the semantics of PropagatesNullable
This diff also clarifies (and changes) the behavior of PropagatesNullable params.
Previously, if the return value of a function that has PropagatesNullable params was
annotated as Nullable, nullsafe was effectively ignoring PropagatesNullable effect.
This is especially bad because one can add Nullable annotation based on the logic "if the function can return `null`, it should be annotated with Nullable`.
In the new design, there is no possibility for such a misuse: the code that
applies the rule "any param is PropagatesNullable hence the return
value is nullable even if not explicitly annotated" lives in NullsafeType.ml, so
this will be automatically taken into account.
Meaning that now we implicitly deduce Nullable annotation for the return value, and providing it explicitly as an alternative that does not change the effect.
In the future, we might consider annotating the return value with `Nullable` explicit.
Reviewed By: jvillard
Differential Revision: D17479157
fbshipit-source-id: 66c2c8777
Ezgi Çiçek
Nikos Gorogiannis
Dulma Churchill
Sungkeun Cho
Artem Pianykh
David Pichardie
Jules Villard
Mitya Lyubarskiy