Summary:
Making `MethodCalled` an inverted map from created location to method calls results in not being able to track a builder that is created in two different branches of a conditional with different types. Instead, we can make `MethodCalled` simply a map and also change `Created` to be a map from access paths to a set of created locations.
To deal with the case of setting a prop only in one branch, we need to ensure that whenever we call a create method, we add a binding to `MethodCalled` with an empty list of methods so that its intersection with a non-empty one is empty.
Reviewed By: skcho
Differential Revision: D18883097
fbshipit-source-id: b3464ca20
Summary: As long as the types match, it should be possible to call build on two components that are created at different locations.
Reviewed By: skcho
Differential Revision: D18881740
fbshipit-source-id: 356f9e168
Summary:
Finally use information from the inferbo intervals in pulse's domain to
make decisions about whether conditionals are feasible or not.
Reviewed By: skcho
Differential Revision: D18811193
fbshipit-source-id: d80a28657
Summary: Add a FN that is detected by the old domain but not the new one
Reviewed By: ngorogiannis
Differential Revision: D18854389
fbshipit-source-id: 9bdc90a6b
Summary: The map from `CreatedLocation` to `MethodCalls` already takes care of the association from create methods to their set props. `MethodCall` comparison should be oblivious the the receiver, otherwise, we risk mistakenly considering two props set at different locations as different.
Reviewed By: skcho
Differential Revision: D18829388
fbshipit-source-id: b5a0d628d
Summary: This diff check and report on every nodes. Problem of the previous design is that it has to report alarms only with the abstract memory of the exit node. However, the new abstract value becomes imprecise at every join points on the path to the exit node, since it is using inverted map, i.e., under-approximation on collecting called methods. As a solution, this diff report on every nodes where `.build` is called with the abstract memory at that node.
Reviewed By: ezgicicek
Differential Revision: D18809449
fbshipit-source-id: 4fd6165d1
Summary: Current method call comparison is too strong. As exemplified with the new test, one can also set the required prop by calling a version which contains the suffixes. The domain should take care of such cases now.
Reviewed By: skcho
Differential Revision: D18808869
fbshipit-source-id: 9f7672e75
Summary:
Sometimes clang9 does not return a boxing method (a name of function to apply), e.g., [@("str")].
To solve the issue, this diff uses "unknownSelector:" instead of giving up the translation.
Reviewed By: dulmarod
Differential Revision: D18831844
fbshipit-source-id: b9324ba39
Summary: This diff checks litho condition on the new abstract value. This is triggered with `--new-litho-domain`, but it is intra-procedural as of now.
Reviewed By: ezgicicek
Differential Revision: D18783203
fbshipit-source-id: 98570104e
Summary:
Also add logic for recognising excessive timeouts. Refactor the code
around timeouts a little.
Reviewed By: artempyanykh
Differential Revision: D18807836
fbshipit-source-id: df5a1b566
Summary:
`Object.wait()` must be called on a locked monitor and it releases the
lock immediately, as far as other threads are concerned
(it also magically re-takes the lock when the monitor is `notified`).
Starvation can only occur if the UI thread is waiting
a lock that is distinct to that being waited on.
The check present was over-approximate in that it was checking that there exists a lock held by the UI thread and the thread issuing the `wait`, but did not make sure that lock was *not* the one waited on.
Amusingly, the e2e test was correct, but the reporting code wasn't.
Reviewed By: dulmarod
Differential Revision: D18782919
fbshipit-source-id: b3b98239e
Summary: Similar to constructor established attributes, we do the same here for static initializers. That is, attributes of static properties are injected into the initial state of every method.
Reviewed By: ezgicicek
Differential Revision: D18763192
fbshipit-source-id: 3879a27c5
Summary: Raises an error when weakSelf is used multiple times in a block. The issue is that there could be unexpected behaviour. Even if `weakSelf` is not nil in the first use, it could be nil in the following uses since the object that `weakSelf` points to could be freed anytime.
Reviewed By: skcho
Differential Revision: D18765493
fbshipit-source-id: 37fc652e3
Summary: This diff extends the bound domain to express multiplication of bounds in some simple cases.
Reviewed By: ezgicicek
Differential Revision: D18745246
fbshipit-source-id: 4f2dcb42c
Summary:
One standard way to schedule work is by starting a thread. We treat this by
- Treating invocations of `start` on a receiver with the `Runnable _` attribute as scheduling that runnable for parallel execution in the background (as opposed to on the UI thread).
- If `start` is used on an object of a subclass of `Thread` everything already works thanks to the `get_exp_attributes` function which will implicitly ascribe to an expression the attribute `Runnable _` if the expression points to an object with a known `run` method. This will even take care of some degree of dynamic dispatch, yay!
- If `start` is used on a `Thread` object which has been created with a constructor call provided with a `Runnable` argument, we have to appropriately model that constructor call, which is what is done in `do_call`.
Reviewed By: jvillard
Differential Revision: D18726676
fbshipit-source-id: 0bd83c28e
Summary:
A current blind spot is when object construction stores specific executors / runnables to object fields, which are then never mutated and accessed from normal methods. IOW the attributes established in the constructor are necessary to report properly inside a normal method (assuming these attributes are not invalidated by method code).
To achieve this, first we retain a subset of the final state attributes in the summary (only those that affect instance variables, in constructor methods). Then, when we analyse a non-constructor method:
- we analyse all constructors
- remove all attributes from the attribute map whose key is not an expression of the form `this.x. ...`
- re-localise all remaining keys so that they appear as rooted in the `this` local variable of the current procedure
- join (intersect) all such attribute maps
- use the result in place of initial state as far as the attribute map is concerned for the analysis of the current procedure, which can now start.
This means we can catch idioms that use side-effectful initialisation for configuring certain object fields like executors or runnables.
Reviewed By: jvillard
Differential Revision: D18707890
fbshipit-source-id: 42ac6108f
Summary: Another way to schedule work in android is by posting it to a `Handler`. A handler can be constructed out of the main looper, which forces it to schedule work on the UI thread. To model all this, we add syntactic models for getting the main looper and for creating handlers, and dataflow attributes for tracking that an expression is a looper/the main looper, or a handler constructed out of a looper.
Reviewed By: skcho
Differential Revision: D18706768
fbshipit-source-id: 7c46e6913
Summary:
New syntax f1 AND-WITH-WITNESSES f2 : predicate_on_both_witnesses()
This is needed for a linter to check that a macro is present, see the test.
Reviewed By: skcho
Differential Revision: D18735988
fbshipit-source-id: a3be75c5e
Summary:
This gets rid of false positives when something invalid (eg null) is
passed by reference to an initialisation function. Havoc'ing what the
contents of the pointer to results in being optimistic about said
contents in the future.
Also surprisingly gets rid of some FNs (which means it can also
introduce FPs) in the `std::atomic` tests because a path condition
becomes feasible with havoc'ing.
There's a slight refinement possible where we don't havoc pointers to
const but that's more involved and left as future work.
Reviewed By: skcho
Differential Revision: D18726203
fbshipit-source-id: 264b5daeb
Summary:
It's a well-known fact that pulse should know too. To avoid splitting
the abstract state systematically, only act if we know the pointer is
exactly 0 to avoid reporting a nullptr dereference on `free(x)`.
Reviewed By: ezgicicek
Differential Revision: D18708575
fbshipit-source-id: 1cc3f6908
Summary:
Turns out code uses atomics in important places, modelling it removes
FPs.
The tests are copied from biabduction and adapted and extended a bit. I
didn't implement compare_exchange primitives for now (plus, giving them
a sequential semantics like in biabduction is probably a bit cheeky).
Reviewed By: skcho
Differential Revision: D18708576
fbshipit-source-id: a3581b8a4
Summary:
This diff adds inferbo's interval values to pulse's attributes. The added values will be used to
filter out infeasible passes in the following diffs.
Reviewed By: jvillard
Differential Revision: D18726667
fbshipit-source-id: c1125ac6e
Summary:
This diff fixes the model of substring.
Problem: The cost model of the substring function was to return `size of string - start index` as a
cost. However, sometimes this was a negative number, because of state abstractions on paths, array
elements, call contexts, etc, which caused an exception inadvertently.
This diff changes the model to return just `size of string`, when it cannot say `size of string` is
bigger than `start index`.
Reviewed By: ezgicicek
Differential Revision: D18707954
fbshipit-source-id: 63f27e461
Summary:
Instead of trying to figure out what runnable is directly passed to an executor,
use attributes to track the flow of a runnable. This has several advantages:
- Can track runnables across function return values.
- Can somewhat overcome the information loss under dynamic dispatch.
- Unifies handling with other attributes.
Reviewed By: skcho
Differential Revision: D18672676
fbshipit-source-id: a06a0e6ff
Summary:
- Unify treatment of modelled and annotated executors by making things go through attributes.
- Add a return attribute to summaries, so that we can track flows of thread guards/executors/future stuff through returned values.
- Dispatch modeled functions to model summaries.
This will help in following diffs where runnables will also go through attributes.
Reviewed By: skcho
Differential Revision: D18660185
fbshipit-source-id: e26b1083e
Summary:
A plugin update allows infer to know when a function doesn't return
according to its attributes. This propagates this info all the way to
the attributes of each function, and then use this information in a new
pre-analysis that cuts the links to successor nodes of each `Call`
instruction to a function that does not return.
NOTE: The "no_return" `CallFlag.t` was dead code, following diffs deal
with that (by removing it).
Reviewed By: dulmarod
Differential Revision: D18573922
fbshipit-source-id: 85ec64eca
Summary:
This also prints the CFGs *after* pre-analysis for individual procedures
in infer-out/captured/<filename>/<proc>.dot. One can also look up the
CFGs before pre-analysis in infer-out/captured/proc_cfgs_frontend.dot.
Context: I want to add a pre-analysis that needs to look at proc
attributes inter-procedurally. For this to make sense it has to happen
*after* all of capture, and before analysis.
Thus, this diff brings back the lazy running of the pre-analysis like in
D15803492, except that we still make sure to run the pre-analyses
systematically regardless of the checkers being run by running the
pre-analysis from ondemand.ml. Also we don't need to re-introduce the
"did_preanalysis" proc attribute for the same reason that the
pre-analysis is now run once and for all by ondemand.ml (instead of each
individual checker back in the days).
This has the benefit of running the pre-analysis only when needed, and
the drawback that several concurrent processes analysing the same proc
descs will duplicate work. Since pre-analyses are supposed to be very
fast I assume that neither is a big deal. If they become more expensive
then the benefit gets bigger and the drawback is just the same as with
regular analyses.
Reviewed By: skcho
Differential Revision: D18573920
fbshipit-source-id: de350eaef
Summary: When we see a call to schedule some work on an executor and we don't have evidence that it is on some specific thread (UI/BG), instead of dropping the work, assign it `UnknownThread` and treat it as running on the background by default.
Reviewed By: jvillard
Differential Revision: D18615649
fbshipit-source-id: e8bad64b6
Summary: Following D18351867, this diff adds more size alias: when initial array size is one.
Reviewed By: ezgicicek
Differential Revision: D18530598
fbshipit-source-id: 26d57fe30
Summary:
- more flexible API
- less error-prone thanks to named parameters
- also takes care of adjusting predecessors of the previous successors!
This fixes some (probably harmless) bugs in the frontends.
Reviewed By: dulmarod
Differential Revision: D18573923
fbshipit-source-id: ad97b3607
Summary: The transition HOLDS-NEXT WITH-TRANSITION Parameters was only implemented for ObjC methods, now it also works on function calls.
Reviewed By: jvillard
Differential Revision: D18572760
fbshipit-source-id: 06e615cbe
Summary:
Now we point to the root cause of the problem, and also provide
actionable way to solve the issue
Reviewed By: artempyanykh
Differential Revision: D18575650
fbshipit-source-id: ba4884fe1
Summary:
Two goals:
1. Be less assertive when speaking about third party code (it might be
written with different conventions).
2. Point to third party signatures folder so the users know how to
proceed
Reviewed By: artempyanykh
Differential Revision: D18571514
fbshipit-source-id: 854d6e746
Summary:
1/ We now support messaging for third-party: show file name and line
number
2/ We did not show information about internal models in case of param
calls
3/ Small change: we don't specify "modelTables.ml" anymore: no need to
expose implementation details
Reviewed By: artempyanykh
Differential Revision: D18569790
fbshipit-source-id: 28586c8ff
Summary:
Whole bunch of changes aimed to make error messages more clear and
concise.
1/ Wording and language is unified. We make errors sound more like a
type system violations, rather than linter reccomendations.
Particularly, we refrain from saying things like "may be null" - this is
a linter-style statement that may provoke discussions (what if the
developer knows it can not be null in this particular case).
Instead, we refer to declared nullability and nullability of actual values. This way, it is more clear that this is not a heuristic, this is how rules of a type-system work.
2/ Additionally, we drop things like field class in places when the
context should be clear by who looks at the error. We expect the user
sees the code and the error caption. So e.g. we don't repeat the word "field"
twice.
3/ In cases when we are able to retrieve formal param name, we include it for
usability.
4/ For Field not initialized error, we refer to Initializer methods:
this is a non-obvious but important nullsafe feature.
Reviewed By: artempyanykh
Differential Revision: D18569762
fbshipit-source-id: 9221d7102
Summary:
It make the message bit less heavy, and also it is kind of obvious that
it is origin.
In follow up diffs we will change the text so it is hopefully even more
obvious.
Reviewed By: artempyanykh
Differential Revision: D18527695
fbshipit-source-id: a305d547b
Summary:
1. We don't want to teach the users to ignore noise origin because
sometimes we are going to render something useful for them.
2. It just looks not cool.
Reviewed By: artempyanykh
Differential Revision: D18527694
fbshipit-source-id: 0ea248122
Summary: Android may spontaneously call these methods on the UI thread, so recognize the fact.
Reviewed By: ezgicicek
Differential Revision: D18530477
fbshipit-source-id: a8a798779
Summary:
First step towards a global analysis. A new command line flag activates the step in `Driver`.
The whole-program analysis is a simple, quadratic (inefficient-as-yet), iteration over all domain elements. However, it is restricted to those elements that are explicitly scheduled to run.
Reviewed By: skcho
Differential Revision: D17787441
fbshipit-source-id: 9fecd766c
Summary:
Note: Disabled by default.
Having some support for values, we can report when a null or constant
value is being dereferenced. The particularity here is that we don't
report when 0 is a possible value for the address, or even if we know
that the value of the address can only be 0 in that branch! Instead, we
allow ourselves to report only when we the address has been *set* to
NULL (or any constant).
This is in line with how pulse deals with other issues: only report when
1. we see an address become invalid, and
2. we see the same address be used later on
Reviewed By: skcho
Differential Revision: D17665468
fbshipit-source-id: f1ccf94cf
Summary:
This diff avoids unqualified variables by `ItvUpdatedBy` are qualified later. For example,
```
z = x & y;
z = z + 1;
```
While `z` should not be selected as a control variable, it wasn't, because it was qualified by the addition. This pattern introduces FPs in many cases.
Reviewed By: ngorogiannis
Differential Revision: D18505894
fbshipit-source-id: 13aec3008
Summary:
This diff excludes integer variables from control variables when their values are calculated by
binary operators.
Reviewed By: ezgicicek
Differential Revision: D18505826
fbshipit-source-id: 710533d4c
Summary: Adding a trace that includes when strongSelf was assigned to, and when it's used without a check.
Reviewed By: skcho
Differential Revision: D18506113
fbshipit-source-id: 778c4b086
Summary:
The variable strongSelf, because it is equal to a weak captured pointer, needs to be checked for null before being used, otherwise it could be null by the time the block is executed.
Added this check to the SelfInBlock checker, and removed it from biabduction.
We want to migrate all the objc checks from biabduction, so it will be easier to change and faster and more reliable. Moreover, this check is more general, it will flag any use of unchecked strongSelf, not just a dereference.
Reviewed By: skcho
Differential Revision: D18403849
fbshipit-source-id: a9cf5d80b
Summary:
There was a precision loss during the substitution of array block. For example:
Callee's abstract memory includes an array block as follows, where `a` is a parameter.
```
a.elements -> { a.elements[*] with a.elements.size }
```
Callers' abstract memory includes a pointer that may point to multiple array blocks.
```
c -> { x, y }
x.elements -> { x.elements[*] with x.elements.size }
y.elements -> { y.elements[*] with y.elements.size }
```
When the callee is called with the parameter `c`, the callees memory is substituted to:
```
x.elements -> { x.elements[*] with top , y.elements[*] with top }
y.elements -> { x.elements[*] with top , y.elements[*] with top }
```
because `a.elements[*]` was substituted to `{ x.elements[*] , y.elements[*] }`
and `a.elements.size` was substituted to `top ( = x.elements.size join y.elements.size )`.
This diff tries to keep the precision in the specific case, not to join the sizes of array blocks.
So now the same callee's abstract memory is substituted to:
```
x.elements -> { x.elements[*] with x.elements.size }
y.elements -> { y.elements[*] with y.elements.size }
```
Reviewed By: ngorogiannis
Differential Revision: D18480585
fbshipit-source-id: b70e63c22
Summary: Due to the weakness of the analysis which can't detect side-effecting prop setting (e.g. as in `builder.prop1(..)`), we currently have many broken chains that do do have any `create` method in their prefixes. Let's not report on these broken chains.
Reviewed By: skcho
Differential Revision: D18503523
fbshipit-source-id: 7506e34b7
Summary:
In some apps executors are obtained by calling standard framework methods (and not by using DI with annotations).
To treat this style, we need to
- Detect calls that return such executors (`do_executor_effect`) and tag the return result with an `Attribute` indicating that it is now an executor, plus what thread it uses.
- Use that information when calling `execute`, to resolve the executor, if any, and its thread (in `do_work_scheduling` via `AttributeDomain.get_executor_constraint`).
- All this requires a new domain component, mapping variables to attributes. This extends the component previously used for remembering whether a variable is the result of a check on whether we run on the UI thread.
At the same time, I un-nested some functions from the transfer function for readability.
Reviewed By: skcho
Differential Revision: D18476122
fbshipit-source-id: bc39b5c2f
Summary:
We consider Java collections to be like c++ std::vectors and add models for
- `Collections.get(..)`
- `__cast`
Reviewed By: skcho
Differential Revision: D18449607
fbshipit-source-id: 448206c84
Summary: `equals1` and `equals2` in `SafeInvertedMap.join` are references that indicate whether given parameters and the result is physically equal or not. This diff fixes a missing update of them.
Reviewed By: ezgicicek
Differential Revision: D18450680
fbshipit-source-id: bae19cbe9
Summary:
It returns non-top value when one of the parameters of band is positive, i.e., `x & 255` returns
`[0, 255]` instead of top.
Reviewed By: ezgicicek
Differential Revision: D18448614
fbshipit-source-id: aaa298a66
Summary:
Let's introduce a set of new cost analysis issue types that are raised when the function is statically determined to run on the UI thread. For this, we rely on the existing `runs_on_ui_thread` check that is developed for RacerD. We also update the cost summary and `jsonbug.cost_item` to include whether a method is on the ui thread so that we don't repeatedly compute this at diff time for complexity increase issues.
Note that `*_UI_THREAD` cost issues are assumed to be more strict than `*_COLD_START` reports at the moment. Next, we can also consider adding a new issue type that combines both such as `*_UI_THREAD_AND_COLD_START` (i.e. for methods that are both on cold start and run on ui thread).
Reviewed By: ngorogiannis
Differential Revision: D18428408
fbshipit-source-id: f18805716
Summary:
This diff tries more narrowing during analysis in order to get preciser results on nested loops.
In the widening phase, it does narrowing a loop right after its widening, for each loops. In general, this may make the widening phase non-terminating because it keeps the abstract state from monotonely increasing to the fixed point in a finite number of iterations. To avoid that situation, this diff applies the narrowing only when the first visit of the loop in the widening phase.
Reviewed By: ngorogiannis
Differential Revision: D18400631
fbshipit-source-id: cc76f7e85
Summary: Sometimes there is a code like `for(int i = 1; i < x; i++){ l.add(); }`, where the first element in a list is addressed specifically. This case was not analyzed precisely, because the alias value is added only when `i` is initialized by 0 by heuristic. This diff extends the heuristic, so it adds a size alias between `i` and `l.size()` when `i` is initialized by 0 or 1.
Reviewed By: ezgicicek
Differential Revision: D18351867
fbshipit-source-id: e7d19a4ec
Summary:
This diff adds semantics of Java function calls of enum `values` inside class initializers.
* Java class initializer function initializes a specific field `$VALUES`, which points to the list
of enum values.
* The `values` function of enum class returns the value of `$VALUES`.
The problem is when the `values` function is called inside the class initializer, for example:
```
enum Color {
RED,
GREEN,
BLUE;
static {
for (Color c : Color.values()) {}
}
}
```
This introduces a recursive dependency: the class initializer calls `Color.values` and the function
returns `Color.$VALUES` the value of which should be initialized in the class initializer.
To address the problem, this diff finds the value of `$VALUES` in its abstract memory when
`values` is called inside the class initializer.
Reviewed By: ezgicicek
Differential Revision: D18349281
fbshipit-source-id: 21766c20f
Summary:
This diff extends bound domain to express Min/Max of another bounds, so it can keep some more
precision in `Math.min/max`.
limitation: `MinMaxB`, the constructor of the bound, can contain only linear expressions or
previous min/max expressions.
Reviewed By: ezgicicek
Differential Revision: D18395365
fbshipit-source-id: fc90d27fd
Summary: Capture locations where work is scheduled to run in parallel (here, just Executors). Also add a test file with cases the upcoming whole-program analysis for starvation should catch.
Reviewed By: dulmarod
Differential Revision: D18346880
fbshipit-source-id: 57411b052
Summary: Follow ups will include error messaging that makes the choice clear
Reviewed By: artempyanykh
Differential Revision: D18347664
fbshipit-source-id: b6f005726
Summary:
In this diff, we just load the info from the storage. Next diff will be
actually using this information to infer nullability.
`ThirdPartyAnnotationGlobalRepo.get_repo` will be used in the next diff,
hence #skipdeadcode
Reviewed By: artempyanykh
Differential Revision: D18347647
fbshipit-source-id: 82a9223c6
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
Ezgi Çiçek
Jules Villard
Sungkeun Cho
Nikos Gorogiannis
Dulma Churchill
Martin Trojer
Mitya Lyubarskiy