Summary:
This diff extends the alias domain, so each variable can have multiple aliases.
It changed `KeyLhs` can be mapped to multiple alias targets in the `AliasMap` domain:
```
before : KeyLhs.t -> KeyRhs.t * AliasTarget.t
after : KeyLhs.t -> KeyRhs.t -> AliasTarget.t
```
Reviewed By: ezgicicek
Differential Revision: D18062178
fbshipit-source-id: b325a6055
Summary:
This diff tries to make less imprecise division by constants results.
For example, the results of the division `[l, u] / c`, where `c` is a positive constant, are:
1. If `l/c` or `u/c` is representable in the bound domain, it uses the precise bounds, i.e., `[l/c, u/c]`.
2. If it is not representable, it tries to make conservative results:
if `0<=l<=u`, it returns `[0, u]` because `0 <= [l/c, u/c] <= u`
if `l<=u<=0`, it returns `[l, 0]` because `l <= [l/c, u/c] <= 0`
if `l<=0<=u`, it returns `[l, u]` because `l <= [l/c, u/c] <= u`
3. otherwise, it returns top, `[-oo, +oo]`
Reviewed By: ezgicicek
Differential Revision: D18270380
fbshipit-source-id: 8fb14c0e4
Summary:
Add precision to analysis by elaborating the thread-status domain. This is done by having unknown (bottom), UI, BG or Any (both/top) elements in the lattice. This way, when we branch on thread-identity (if I am on UI thread do this, otherwise do that), we know that in one branch we are on UI thread and on the other we are *not* on the UI thread (BG thread), where previously the other branch would just go to top.
With this knowledge we can throw away pairs that come from callees which run on a thread that is impossible, given the current caller thread identity. This can happen when annotations are used incorrectly, and since this is the purview of annot-reachability, we just drop those pairs entirely.
Reviewed By: skcho
Differential Revision: D18202175
fbshipit-source-id: be604054e
Summary:
Steal a page from RacerD (and improve interface of) on using certain calls to assert
execution on a particular thread. Reduces FPs and FNs too.
Reviewed By: dulmarod
Differential Revision: D18199843
fbshipit-source-id: 5bdff0dfe
Summary:
The zero cost of node does not make sense especially when the abstract memory is non-bottom. This
resulted in unreasonable zero cost results sometimes, e.g. when the checker could not find
appropriate control varaibles having interval values of iteration. This diff fixes this, so sets
the minimum basic cost as 1, if the abstract memory at the node is non-bottom.
Reviewed By: ezgicicek
Differential Revision: D18199291
fbshipit-source-id: b215d10e5
Summary:
This adds a more interesting value domain to pulse: concrete intervals.
There are still two main limitations:
1. arithmetic operations are all over-approximated: any assignment involving arithmetic operations is replaced by non-determinism
2. abstract values that are discovered to be equal are not merged into one
Reviewed By: skcho
Differential Revision: D18058972
fbshipit-source-id: 0492a590f
Summary:
This does several things because it was hard to split it more:
1. Split most of the arithmetic reasoning to PulseArithmetic.ml. This
doesn't need to be reviewed thoroughly because an upcoming diff
changes the domain from just `EqualTo of Const.t` to an interval domain!
2. When going through a prune node intra-procedurally, abduce arithmetic
facts to the pre (instead of just propagating them). This is the "assume
as assert" trick used by biabduction 1.0 too and allows to propagate
arithmetic constraints to callers.
3. Use 2 when applying summaries by pruning specs whose preconditions
have un-satisfiable arithmetic constraints.
This changes one of the tests! Pulse now does a bit more work to find
the false positive, as can be seen in the longer trace.
Reviewed By: skcho
Differential Revision: D18117160
fbshipit-source-id: af3b2c8c0
Summary:
Primitive types are not annotated. Because of that, we used to implicitly derive
`DeclaredNonnull` type for them. This worked fine, but this leads to errors in Strict mode, which does
not believe DeclaredNonnull type.
Now lets offifically teach nullsafe that primitive types are
non-nullable.
Reviewed By: jvillard
Differential Revision: D18114623
fbshipit-source-id: 227217931
Summary: It is now possible to push the thread status into each critical pair. This leads to higher precision, because when code branches on whether it is on the UI thread, the final abstract state of the procedure will be `AnyThread`, but pairs created in the UI thread branch should know that their status is `UIThread`, not `AnyThread`.
Reviewed By: jvillard
Differential Revision: D18114273
fbshipit-source-id: cbb99b46f
Summary:
This diff avoids making top values on unknown non-static function,
such as abstract function, calls. This is necessary because the
generated top values ruin the precision of the cost checker.
Reviewed By: ezgicicek
Differential Revision: D17418611
fbshipit-source-id: aeb759bdd
Summary:
The wrong function was used when we tried to see if the class is
annotated with NullsafeStrict. This made it work only for non-static
methods.
Now we use the proper way.
Reviewed By: ngorogiannis
Differential Revision: D18113848
fbshipit-source-id: 02b7555be
Summary:
Previously, we considered a function which modifies its parameters to be impure even though it might not be modifying the underlying value. This resulted in FPs like the following program in Java:
```
void fresh_pure(int[] a) {
a = new int[1];
}
```
Similarly, in C++, we considered the following program as impure because it was writing to `s`:
```
Simple* reassign_pure(Simple* s) {
s = new Simple{2};
return s;
}
```
This diff fixes that issue by starting the check for address equivalnce in pre-post not directly from the addresses of the stack variables, but from the addresses pointed to by these stack variables. That means, we only consider things to be impure if the actual values pointed by the parameters change.
Reviewed By: skcho
Differential Revision: D18113846
fbshipit-source-id: 3d7c712f3
Summary: We stop tracking at builder boundaries. Let's tract create methods as well so that trace is more informative.
Reviewed By: skcho
Differential Revision: D18038637
fbshipit-source-id: a99b6431f
Summary:
This is the first take on strict mode semantics.
The main invariant of strict mode is the following:
If the function passes `NullsafeStrict` check and its return value is
NOT annotated as Nullable, then the function does not indeed return
nulls, subject to unsoundness issues (which should either be fixed, or
should rarely happen in practice).
This invariant helps the caller in two ways:
1. Dangerous usages of non strict functions are visible, so the caller is enforced to check them (via assertions or conditions), or strictify them.
2. When the function is strict, the caller does not need to worry about
being defensive.
Biggest known issues so far:
1. Condition redundant and over-annotated warnings don't fully
respect strict mode, and this leads to stupid false positives. (There is
so much more stupid false positives in condition redundant anyway, so
not particularly a big deal for now).
2. Error reporting is not specific to mode. (E.g. we don't distinct real nullables and non-trusted non-nulls, which can be misleading). To be
improved as a follow up.
Reviewed By: artempyanykh
Differential Revision: D17978166
fbshipit-source-id: d6146ad71
Summary:
This is an intermediate nullability type powering future Strict mode.
See the next diff.
Reviewed By: artempyanykh
Differential Revision: D17977909
fbshipit-source-id: 2d5ab66d4
Summary: In preparation for improvements to the arithmetic reasoning.
Reviewed By: dulmarod
Differential Revision: D17977207
fbshipit-source-id: ee98e0772
Summary:
Domain for thread-type. The main goals are
- Track code paths that are explicitly on UI thread (via annotations, or assertions).
- Maintain UI-thread-ness through the call stack (if a callee is on UI thread then the
trace any call site must be on the UI thread too).
- If we are not on the UI thread we assume we are on a background thread.
- Traces with "UI-thread" status cannot interleave but all other combinations can.
- We do not track other annotations (eg WorkerThread or AnyThread) as they can be
erroneously applied -- other checkers should catch those errors (annotation reachability).
- Top is AnyThread, and is used as the initial state for analysis.
Interestingly, by choosing the right strategy for choosing initial state and applying callee summaries gets rid of some false negatives in the tests even though we have not introduced any path sensitivity yet.
Reviewed By: jvillard
Differential Revision: D17929390
fbshipit-source-id: d72871034
Summary:
bigmacro_bender
There are 3 ways pulse tracks history. This is at least one too many. So
far, we have:
1. "histories": a humble list of "events" like "assigned here", "returned from call", ...
2. "interproc actions": a structured nesting of calls with a final "action", eg "f calls g calls h which does blah"
3. "traces", which combine one history with one interproc action
This diff gets rid of interproc actions and makes histories include
"nested" callee histories too. This allows pulse to track and display
how a value got assigned across function calls.
Traces are now more powerful and interleave histories and interproc
actions. This allows pulse to track how a value is fed into an action,
for instance performed in callee, which itself creates some more
(potentially now interprocedural) history before going to the next step
of the action (either another call or the action itself).
This gives much better traces, and some examples are added to showcase
this.
There are a lot of changes when applying summaries to keep track of
histories more accurately than was done before, but also a few
simplifications that give additional evidence that this is the right
concept.
Reviewed By: skcho
Differential Revision: D17908942
fbshipit-source-id: 3b62eaf78
Summary:
Java method annotations are ambiguous in that there is no difference between
annotating the return value of a method, and annotating the method itself.
The disambiguation is done entirely based on the meaning of the annotation.
Here, while `UiThread`/`MainThread` are genuine method/class annotations
and not return annotations, the reverse is true for `ForUiThread`/`ForNonUiThread`.
This means that these latter annotations do not determine the thread status of
the method they are attached to.
Here we fix that misunderstanding.
Reviewed By: jvillard
Differential Revision: D17960994
fbshipit-source-id: 5aecfb124
Summary: As per title. These test pass already because the previous thread domain was sufficient to express them. This won't necessarily be true when the whole-program analysis version comes around, because we may decide to not report on the `Threaded` elements (see domain).
Reviewed By: dulmarod
Differential Revision: D17930653
fbshipit-source-id: 2174f6b22
Summary:
- add the variable being declared so we can report it back in the trace in addition to its location
- distinguish between local vars and formals
Reviewed By: skcho
Differential Revision: D17930348
fbshipit-source-id: a5b863e64
Summary:
Eventually thread status will be stored inside every critical pair so as to allow path sensitivity. That means that the status can no longer be a whole trace, as this will quickly become intractable, because each domain element would have to maintain its own trace as well as its own thread-status trace.
This is not great, as we lose information here, but I don't see any other way around it that is not super complicated/costly (sharing will be limited when moving from callee to caller).
Other diffs up the stack will clean up infrastructure no longer used meaningfully (ie models and domains).
Reviewed By: mityal
Differential Revision: D17908908
fbshipit-source-id: 3bf353e33
Summary:
Starvation is currently path insensitive. Two special cases of sensitivity cover a large range of useful cases:
- sensitivity on whether the current thread is a UI/background thread;
- sensitivity on whether a lock can be acquired (without blocking) or not.
We add a few tests capturing some of the false positives and negatives of the current analysis.
Reviewed By: mityal
Differential Revision: D17907492
fbshipit-source-id: fbce896ac
Summary:
This diff adopts an array length evaluation function that is conservative. It is useful when our
domain cannot express length result precisely.
For example, suppose there is an array pointer `arr_locs` that may point to two arrays `a` and `b`,
and their lengths are `a.length` and `b.length` (symbols), respectively. Using the usual
evaluation, our current domain cannot express `a.length join b.length` (join of two symbolic
values), so it returns top.
In this case, we can use the conservative function intead. It evaluates the length as `[0,
a.length.ub + b.length.ub]`, since we know every array length is positive. The result is not
precise, but better than top.
Reviewed By: ezgicicek
Differential Revision: D17908859
fbshipit-source-id: 7c0b1591b
Summary:
Instead of a string argument named `~str` pass `Formal | Global` and let
`add_to_errlog` figure out how to print it.
Reviewed By: ezgicicek
Differential Revision: D17907657
fbshipit-source-id: ed09aab72
Summary:
When we make the decision to go into a branch "v = N" where some
abstract value is compared to a constant, remember the corresponding
equality. This allows to prune simple infeasible paths
intra-procedurally.
Further work is needed to make this useful interprocedurally, for
instance either or both of these ideas could be explored:
- abduce v=N in the precondition and do not apply summaries when the
equalities in the pre are not satisfied
- prune post-conditions that lead to unsat states where a value has to
be equal to several different constants
Reviewed By: skcho
Differential Revision: D17906166
fbshipit-source-id: 5cc84abc2
Summary:
When we know "x = 3" and we have a condition "x != 3" we know we can
prune the corresponding path.
Reviewed By: skcho
Differential Revision: D17665472
fbshipit-source-id: 988958ea6
Summary:
Let's add basic Java support to impurity checker. Since impurity checker relies on pulse, we need to add Java with Pulse callback as well. Pulse doesn't officially support Java yet, but we can enable it for impurity checker for now.
Many Java primitives/operations are not yet modeled (such as creation of new objects, support for collections etc.). Still, it is good to run impurity checker on the existing tests of the purity checker. Also, it is nice to see that we can identify most of the impure functions correctly in the purity dir. There are a lot of FNs though.
Reviewed By: skcho
Differential Revision: D17906237
fbshipit-source-id: 15308d285
Summary:
This diff introduces inequality for the iterator alias target, as we
did for the size target before.
Reviewed By: ezgicicek
Differential Revision: D17879208
fbshipit-source-id: cc2f6a723
Summary: If we have no pulse summary (most likely caused by pulse finding a legit issue with the code), let's consider the function as impure.
Reviewed By: jvillard
Differential Revision: D17906016
fbshipit-source-id: 671d3e0ba
Summary:
This diff revises the semantics of hasNext model to add the lengths of
arrays, rather than join them to top.
Reviewed By: ezgicicek
Differential Revision: D17882388
fbshipit-source-id: f5edaedb3
Summary:
[androidx.collection.SimpleArrayMap](https://developer.android.com/reference/androidx/collection/SimpleArrayMap.html) also has `keySet` and `entrySet` methods which make them eligible for inefficient keyset checker. Let's add it.
Title
Reviewed By: skcho
Differential Revision: D17831594
fbshipit-source-id: 32e831e18
Summary:
The current usage has several issues reducing code maintainability and
readability:
1. Null_field_access was misleading: it was used for checking accesing
to arrays as well!
2. But actually, when checking access to array via `length`, we sometimes
pretended it is a field access (hence very tricky code in rendering the
error).
3. "Call receiver consistency" is unclear name, was not obvious that it is all about
calling a method in an object.
Let's also consolidate code.
Reviewed By: artempyanykh
Differential Revision: D17789618
fbshipit-source-id: 9b0f58c9c
Summary: Before, we didn't track litho framework callees on client code which was wrong. Now, we replace this with the following: If the callee is `build()` itself or doesn't contain a `build()` in its summary, then we want to track it in the domain. The former makes sense since we always want to track `build()` methods. The latter also makes sense since such a method could be a setter for a prop (as in the case of `prop1` in `buildPropLithoOK` which we were missing before due to the imprecise heuristic that prevented picking up callees in litho).
Reviewed By: ngorogiannis
Differential Revision: D17810704
fbshipit-source-id: 87d88e921
Summary: As a heuristic, litho library calls on non-litho callers are not tracked. This is very imprecise and results in FPs and FNs as exemplified by newly added tests. Instead, we should check to see if the summary contains a `build()` method as will be done in the next diff. This diff adds these tests and refactors the test code.
Reviewed By: skcho
Differential Revision: D17809536
fbshipit-source-id: 6dff1868c
Summary:
Improve the trace by incorporating the callees and their locations in the call chain (i.e. chain of methods starting from `build()` call)
- extend the domain to contain the callee location
- replace the test results with the new traces
This makes our job much easier to debug FPs in a big codebase.
Reviewed By: skcho
Differential Revision: D17788996
fbshipit-source-id: 31938b5fe
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:
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:
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:
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:
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:
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: `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, 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:
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 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
Summary: Our annotation parameter parsing is too primitive to identify `resType` and before we only assumed that all Prop's can be set by any of the two suffixes: `Attr` and `Res`. After talking to Litho team, there is 3 more additions to these suffixes: `Dip`, `Sip`, and `Px`.
Reviewed By: ngorogiannis
Differential Revision: D17528482
fbshipit-source-id: 8d7f49130
Summary: Before, we were mistakenly checking any annotation that ends with Prop such as TreeProp. This was wrong. Instead, we should only check Prop as adviced by the Litho team.
Reviewed By: ngorogiannis
Differential Revision: D17527769
fbshipit-source-id: b753dd87a
Summary:
Introduce a new experimental checker (`--impurity`) that detects
impurity information, tracking which parameters and global variables
of a function are modified. The checker relies on Pulse to detect how
the state changes: it traverses the pre and post pairs starting from
the parameter/global variable and finds where the pre and post heaps
diverge. At diversion points, we expect to see WrittenTo/Invalid attributes
containing a trace of how the address was modified. We use these to
construct the trace of impurity.
This checker is a complement to the purity checker that exists mainly
for Java (and used for cost and loop-hoisting analyses). The aim of
this new experimental checker is to rely on Pulse's precise
memory treatment and come up with a more precise im(purity)
analysis. To distinguish the two checkers, we introduce a new issue
type `IMPURE_FUNCTION` that reports when a function is impure, rather
than when it is pure (as in the purity checker).
TODO:
- improve the analysis to rely on impurity information of external
library calls. Currently, all library calls are assumed to be nops,
hence pure.
- de-entangle Pulse reporting from analysis.
Reviewed By: skcho
Differential Revision: D17051567
fbshipit-source-id: 5e10afb4f
Summary:
`ModeledRange` represents how many times the interval value can be updated by modeled functions. This
domain is to support the case where there are mismatches between value of a control variable and
actual number of loop iterations. For example,
```
while((c = file_channel.read(buf)) != -1) { ... }
```
the loop will iterates as the file size, but the control variable `c` does not have that value. In
these cases, it assigns a symbolic value of the file size to the modeled range of `c`, then which
is used when calculating the overall cost.
Reviewed By: jvillard
Differential Revision: D17476621
fbshipit-source-id: 9a81376e8
Summary:
This diff extends the `Simple` alias domain to address Java's
temporary variables better. It now has an additional field to denote
an alias temporary variable.
Reviewed By: jvillard
Differential Revision: D17421907
fbshipit-source-id: 8b8b47461
Summary:
D17397144 adds dedicated tests for condition redundant.
We also have tests for overannotated methods.
This makes these test cases redundant. Let's not pollute the results.
Reviewed By: jberdine
Differential Revision: D17398757
fbshipit-source-id: 10f6beeca
Summary:
This will simplify modifying functionality around this type of error.
Also rename the file for clarity.
Reviewed By: jvillard
Differential Revision: D17397144
fbshipit-source-id: 552215243
Summary:
This diff revises widening functions of bounds that have a linear form and a min/max form.
For example, for lower bounds,
* 3 ▽ (1+min(2, x)) = (1+min(2, x))
* 3+x ▽ (3+min(2, x)) = (3+min(2, x))
Reviewed By: jvillard
Differential Revision: D17420786
fbshipit-source-id: ff9eebed3
Summary:
This diff addresses collection adds in loop. For example,
```
ArrayList<...> a = new ArrayList<>();
for (int i = 0; i < size; i++) {
a.add(...);
}
// we want to know the size of `a` here!
```
This is a common pattern on initializing a collection in Java.
How we did: Instead of adopting general (but complicated) solutions such as relational domain, we
extended the current alias domain of inferbo, to be able to handle this specific case:
* An array `a` should have size 0, at the entry of the loop.
* The iterating variable `i` should start with 0.
* `add` should be called once inside the loop.
Reviewed By: jvillard
Differential Revision: D17319350
fbshipit-source-id: 99b6acae1
Summary:
In D17156724, we forked nullsafe tests, which was a strategy to
introduce nullsafe-gradual mode back then.
The reason was "gradual" mode is a pretty big change in a way Infer
handles annotations, so we wanted to tests both scenarios: gradual and
non-gradual mode.
The plan was to deprecate "non-gradual" tests at some point, hence we
decided to go with duplication.
Now we have a better approach to ensure "gradual" features are well
covered. The approach is the following.
1. [Mostly finished] Improve existings tests so that they cover negative and positive
cases. With this, we can safely add something like
--non-annotated-default UNKNOWN_NULLABILITY to the test config and be sure tests still make
sense (i.e. don't pass simply because annotations don't make sense
anymore)
2. [In progress]. Refactor nullsafe code so that instead of using of Annot.ml everywhere we use a special abstraction telling if the class is annotated with Nullable, Nonnull, or not annotated. With this change, we essenstially have a single place we need to test, which removes the need to have 2 pair of tests for each feature.
3. [To be done]. Introduce Uknown nullability and add small number of tests specifically
for that feature (together with existing tests).
NOTE: I did not rename `nullsafe-default` back to `nullsafe` to not
pollute blame without need.
Reviewed By: artempyanykh
Differential Revision: D17395743
fbshipit-source-id: 3d3e062f6
Summary:
Get rid of helper class `C`, normal Object serves the same goal well
Don't return values from a function, focus only on nullable
dereferences.
Reviewed By: jberdine
Differential Revision: D17314569
fbshipit-source-id: d70e66b5f
Summary:
1. Split into 3 subclasses for 3 major set of features we test
2. Document a known FP
3. More clear names
Reviewed By: jberdine
Differential Revision: D17285902
fbshipit-source-id: 66e3b5668
Summary:
Let's consolidate "positive" and "negative" cased together by adding an example
of not annotated class as a source of "negative" cases.
Also join the case with modelled methods to the same class.
Reviewed By: jberdine
Differential Revision: D17284101
fbshipit-source-id: e15e60691
Summary:
There are currently plenty of ways to suppress the warning, including Inject, Initializer, and SuppressFieldNotInitialized annotations.
This one (annotating field with Nonnull) is counter-intuitive and does not align with gradual nullsafe
semantics we are working on.
Reviewed By: artempyanykh
Differential Revision: D17281702
fbshipit-source-id: 132e1b687
Summary:
This diff ignores character symbols in the cost results, in order to
avoid FPs from parser code.
Reviewed By: ezgicicek
Differential Revision: D17132053
fbshipit-source-id: d9cf8bd26
Summary: let's always have positive and negative case for each feature we test
Reviewed By: ngorogiannis
Differential Revision: D17206785
fbshipit-source-id: 5791ace48
Summary:
1. Let's move it to the file dedicated to this particular warning.
2. Make it more general (Activity was just a particular case) and describe in comments what it really does.
Reviewed By: ngorogiannis
Differential Revision: D17205919
fbshipit-source-id: 82bf5e9bd
Summary:
1. Remove boilerplate with builder that uses builder initializer; it
demostates a usecase but it is not really relevant for the test so it
distracts attention.
Instead, describe the usecase in the comment
2. Add good and bad cases so it is obvious what exactly do we test.
Reviewed By: artempyanykh
Differential Revision: D17204969
fbshipit-source-id: 005ea078b
Summary:
Let's combine with the one that tests a very similar thing for known
cleanup methods
Reviewed By: ngorogiannis
Differential Revision: D17204206
fbshipit-source-id: dbdbde903
Summary:
1. Remove manipulations with "shadowed" fields and abstract class, I don't believe they produced high quality signal (and no related warnings in the test output).
2. For each failure case provide corresponding success case and the
reverse
Reviewed By: artempyanykh
Differential Revision: D17203240
fbshipit-source-id: c809857ed
Summary:
1. Let's make the intention of the test more visible, also let's provide an example
when the error does occur.
2. `onDestroy` silence "field not nullable" warnigs not only for `View`, but for any objects, so let's use `String` (as an example of a trivial object) instead.
Original diff that introduced the test: D10024458
Reviewed By: artempyanykh
Differential Revision: D17202839
fbshipit-source-id: 037d937e4
Summary: This diff adds models of Java String. In order to keep the precision of cost checker, I fixed cost models for String in this diff too.
Reviewed By: ngorogiannis
Differential Revision: D17203309
fbshipit-source-id: 8cc2814fc
Summary: This shows that the current Pulse analyzer works fine in the C++ part of the Objc++ files.
Reviewed By: martintrojer
Differential Revision: D17225683
fbshipit-source-id: faf51c5fa
Summary: Use_after_free was used both for biabduction and pulse, and the biabduction version is blacklisted by default. As a result, the Pulse version was also disabled unintentionally. This changes the name of the old use_after_free so that now we can get use_after_free bugs whenever pulse is enabled.
Reviewed By: skcho
Differential Revision: D17182687
fbshipit-source-id: 539ca69de
Summary:
See motivation below.
This diff is dealing with FieldNotNullable:
- move not relevant subclasses into dedicated classes and files
- modify the tests so they comply with the standards below
--Motivation--
Gradual mode we are going to introduce is an invasive change in how Infer
treats nullability semantics.
In order to make the change in a controllable way, we need the tests to comply with the
following standards and conventions.
1. For each code peace where we expect a bug to happen, the there should be
corresponding (minimally different from above) peace of code where we expect a bug to NOT happen. (This is to ensure bug is happening for exact reason we think it is happening).
2. Conversely: for each peace of code where we expect a bug to be NOT
present, there shuold be a peace of code where the bug IS happening.
(Otherwise there can be too many reasons for a bug NOT to happen).
3. Convention: end corresponding methods IsOK and IsBUG correspondingly.
4. Keep code examples as small as possible.
Reviewed By: ngorogiannis
Differential Revision: D17183222
fbshipit-source-id: 83d03e67f
Summary: With this predicate we are able to check for static global variables in AL.
Reviewed By: ddino
Differential Revision: D17164848
fbshipit-source-id: a3d10598c
Summary:
In next diff, we are going to introduce a new mode of nullsafe
(gradual). For testing, we are going to employ the strategy used by jvillard
for Pulse.
In this diff we split tests into two subfolders, one for the default and one for the gradual
mode.
We are planning to make the gradual mode default eventually. For that, most
new features will make sense for gradual mode, and we will mostly evolve
tests for that mode.
As for 'default' mode, we need to preserve tests mostly to ensure we don't introduce
regressions.
Occasionally, we might make changes that make sense for both modes, in
this (expected relatively rare) cases we will make changes to both set
of tests.
An alternative strategy would be to have two sets of issues.exp files,
one for gradual and one for default mode. This has an advantage of each
java file to be always tested twice, but disadvantage is that it will be
harder to write meaningful test code so that it makes sense for both
modes simultaneously.
Reviewed By: ngorogiannis
Differential Revision: D17156724
fbshipit-source-id: a92a9208f
Summary:
`Present` annotation was an experiment made many years ago that never
got into real usage. The idea was to annotate Optional<> types with
Present, which means that it is safe to call get().
We don't plan to support `Present` annotation for optional types in the
near future.
Support of `Present` annotation requires extra levels of abstraction
that make the changing the behavior and introducing new features harder.
A lot of checks for nullability are written in generic way so they also
check for presense.
Getting rid of that will allow us to simplify our
work for introducing new semantics for nullsafe.
Reviewed By: ngorogiannis
Differential Revision: D17153432
fbshipit-source-id: c5ea9bdf1
Ezgi Çiçek
Sungkeun Cho
Dulma Churchill
Nikos Gorogiannis
Jules Villard
Mitya Lyubarskiy