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:
Since the correcteness of the mapping from LLVM to llair depends on
LLVM being SSA, we need to formalise what that means. We also prove that
the domination relation is a strict partial order, which will probably
be helpful when reasoning about the translation.
Reviewed By: jberdine
Differential Revision: D17631456
fbshipit-source-id: a00eb3f87
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 LLVM semantics and translation was not consistently treating the
1-bit word value condition as signed or unsigned.
Reviewed By: jberdine
Differential Revision: D17605766
fbshipit-source-id: 77edf63b7
Summary:
Previously the LLVM semantics did the phi instructions at the head of a
block as part of executing the branch into that block. This looked a bit
weird, but had the advantage that the semantics knew which block was
being jumped from, which is necessary to run the phi instructions.
However, it meant that the rules for doing phi instructions would need
to show up with each branching construct. It was also annoying for the
LLVM->llair proof, since the phis are removed and their effect happens as
a distinct step from the branch.
Here we add a distinct Phi_ip instruction pointer to indicate that the
phi instructions at the start of the block should execute next, and then
be incremented to the usual numeric instruction pointer that points to
the non-phi instructions. The Phi_ip contains the identity of the
previous block.
Reviewed By: jberdine
Differential Revision: D17452416
fbshipit-source-id: 78fef7cca
Summary:
Give the llair semantics observable side effects (writes to global
variables) and a semantic function mirroring the LLVM semantics. Start
sketching out the LLVM/llair translation equivalence proof in a top-down
way from the obvious statement of equality of the semantics.
Reviewed By: jberdine
Differential Revision: D17399654
fbshipit-source-id: 2170678a8
Summary:
The simple LLVM semantics steps one instruction at a time, but the
generated llair does whole blocks at a time, since many individual LLVM
instructions can become a single llair expression. We add a bigger-step
LLVM semantics that does whole blocks at a time (except that it also
stops at function calls, since those end blocks in llair). The steps in
this bigger-step semantics should be at the same granularity as the
llair steps, making it easier to verify the translation.
We add a notion of observation to the LLVM semantics (right now, just
global variable writes) and use that to define two top-level semantic
functions, which we prove to be equivalent.
Reviewed By: jberdine
Differential Revision: D17396016
fbshipit-source-id: ee632fb92
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:
This diff allows domains to specify which abstract states can or can't
be merged together by the worklist. In particular, this is needed for
relational domains to ensure that Hoare triples are joined only when
they share a precondition.
Reviewed By: jberdine
Differential Revision: D17571148
fbshipit-source-id: d9345fdc9
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 diff adds a "-prenalyze-globals" flag to all analyze targets
which, when set, computes used-globals sets for all reachable
functions and then uses that information to track only relevant
global variables at calls in the main analysis.
Reviewed By: jberdine, jvillard
Differential Revision: D17526746
fbshipit-source-id: 1a114285c
Summary:
Fixes a bug in Llair.Frontend.xlate_value where the l-val register
of LLVM instruction calls was being marked as global.
Reviewed By: jberdine
Differential Revision: D17570458
fbshipit-source-id: e1b5924e2
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
Summary:
In the cost checker, the range of selected control variables are used to estimate the number of loop iteration. However, sometimes the ranges of control variables are not related to how many times the loop iteration. This diff strengthens the condition for them as:
1. integers from `size` models
2. integers constructed from `+` or `-`
3. integers constructed from `*`
For the last one, the loop iteration is likely to be log scale of the range of the control variable:
```
while (i < c) {
i *= 2;
}
```
We will address this in the future.
Reviewed By: ezgicicek
Differential Revision: D17365796
fbshipit-source-id: c1e709ae8
Nikos Gorogiannis
Sungkeun Cho
Ezgi Çiçek
Artem Pianykh
Scott Owens
David Pichardie
Jules Villard
Mitya Lyubarskiy
Dulma Churchill
Benno Stein