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
Nikos Gorogiannis
Dulma Churchill
Martin Trojer
Ezgi Çiçek
Sungkeun Cho
Jules Villard
Mitya Lyubarskiy