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:
In the follow up diff we will use it to render more informative
error message when type error is relevant to the fact that the code is
third-party
Reviewed By: artempyanykh
Differential Revision: D18569783
fbshipit-source-id: 4f6dcc404
Summary:
Let the functions return the modified storage, not unit.
It will play nicely with the next diff, which will add more data to
storage which will be non-mutable.
Reviewed By: artempyanykh
Differential Revision: D18569768
fbshipit-source-id: ade5685be
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:
By default `install` will always overwrite the destination, which in
particular makes the target looks newer to `make`. This was causing the
models to be rebuilt on every `make`.
Passing `-C` helps with that:
-C, --compare
compare each pair of source and destination files, and in some cases, do not modify the destination at all
Reviewed By: martintrojer
Differential Revision: D18574558
fbshipit-source-id: 40758d689
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:
This diff also removes clumsy typeErr.origin_desc and improves interface
of TypeOrigin.
This will allow to render smarter error message, depending on the
context (see follow up diff).
Reviewed By: ngorogiannis
Differential Revision: D18527692
fbshipit-source-id: b7eb11db8
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 was causing loads of false positives later in the stack.
Invalidating the address of the object seems to be enough here as it
doesn't break any tests.
Reviewed By: ezgicicek
Differential Revision: D18246090
fbshipit-source-id: 2ef9a6a5c
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 is a part of work teaching Nullsafe to explain decisions it's
making.
We used to use default for this, which is both buggy and hard to
diagnose. Now we explicitly document nullsafe behaviour in this case.
Reviewed By: artempyanykh
Differential Revision: D18481220
fbshipit-source-id: 0b0cf8b38
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: Let's make UI/Cold start parts of the message bold to get more attention.
Reviewed By: jvillard
Differential Revision: D18504857
fbshipit-source-id: b0f199f55
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:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.
This method was the last escape hatch for InferredNullability to
misreport about its origin.
Now each time we change nullability we provide origin that is consistent
with the nullability itself.
Reviewed By: artempyanykh
Differential Revision: D18453567
fbshipit-source-id: 3d9b7fa2e
Summary:
This is one of key diff in this refactoring stack.
Previously, we used to set nullability independently of type origin,
which opened doors for inconsistent states, bugs, and overcomplicated
code.
Now we have just two method left:
1. `create` -> the main one, yay
2. `set_nonnull` -> will get rid of this in the next diff.
Reviewed By: artempyanykh
Differential Revision: D18451950
fbshipit-source-id: edc485709
Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.
In this diff, we merely rename the value to clearly reflect its currect
usage.
In follow up diffs we are going to make usages of this instance more
restricted and concentrate them in several places in the code.
Reviewed By: artempyanykh
Differential Revision: D18451290
fbshipit-source-id: cf3773364
Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.
1. `Formal` was bit cryptic name.
2. Splitting method param and this makes a lot of sense. It is almost an
implementation detail that hey happen to come from "param" in the
method's signature.
3. Apart from others, this diff fixes a minor bug - we used to treat
this as DeclaredNonnull, which (in future) means suppressing legit warnings
like condition redundant. This would be an issue if we were to start
showing "high confidence" condition redundant warnings.
Reviewed By: ngorogiannis
Differential Revision: D18451294
fbshipit-source-id: acc295e3f
Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.
1. Make Field origin a record: consistent with Proc; more readable; will
add more elements in follow up diffs.
2. `Proc` is bit ambiguous: it is unclear if this is a method call result or param.
Let's make it clear that it is the result of a method call.
Reviewed By: ngorogiannis
Differential Revision: D18450188
fbshipit-source-id: c5abae3ad
Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.
Using `New` was definitely not a good idea here, we need a specific
data type value here.
Reviewed By: artempyanykh
Differential Revision: D18450174
fbshipit-source-id: 7ce7cc7e8
Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.
Introducing more specific origins will allow us to automatically infer
nullability based on type origin (in follow up diffs).
Reviewed By: ngorogiannis
Differential Revision: D18450165
fbshipit-source-id: 9dc0d25c0
Summary:
This diff uses `of_java_array_alloc` instead of `of_c_array_alloc`. Java's array does not have
offset and stride. While this simplifies abstract memories in Java, there is not visible changes I can think of.
Reviewed By: ezgicicek
Differential Revision: D18453474
fbshipit-source-id: 36bdf3daf
Summary:
We were not tracking static `create ` and `build` methods intra-procedurally in the analysis and we just looked up their summaries. This resulted in not having static `create` methods in the trace. Let's fix that by pushing static check into `satisfy_heuristic`.
This results in a few FPs, but such cases are not very common in the codebase.
Reviewed By: skcho
Differential Revision: D18451955
fbshipit-source-id: d4ccf46f5
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:
`getThis` is an idiom for allowing Builder sub-classes to jump through the hoops of covariance plus java generics with self types. It's declared as abstract in the (generic) inner `Builder` class of a root class, and subclasses declare generic `Builder`s that inherit from the generic root `Builder` and trivially implement this method by returning `this`. Obviously, this returns conditional ownership (if `this` is owned, then the return value is owned).
The way it's typically used is
```
T foo() {
...
return getThis();
}
```
However, because abstract methods need dynamic dispatch for proper summarisation, we miss all that. A workaround was been implemented in D8947992 (see that for context), but it was buggy -- it required that the LHS type in the assignment
```
lhs = this.getThis();
```
is the same as the type of `this`, but this is too strict (eg, when using casts).
Here, the condition is changed to requiring that the return type of the method is the same as the type of `this`.
We also avoid asking for the `procdesc` as everything needed is in the attributes.
Reviewed By: jberdine
Differential Revision: D18450737
fbshipit-source-id: e67f0495c
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:
The order was wrong: the map from procnames to node-ids was cleaned first, but to clean the map from node-ids to nodes, we need the id and we have already removed it.
The symptom was that effectively no new leaves are created by "removing" a node, so the call graph scheduler quickly devolves to the file-based one.
Reviewed By: skcho
Differential Revision: D18448209
fbshipit-source-id: f272a8112
Summary:
There was some over-general treatment of reachability, in anticipation of changes that didn't happen.
In particular, we only need to flag/remove single nodes, as they must be leaves to be scheduled,
therefore we never need to traverse their successors, because there aren't any.
Reviewed By: jvillard
Differential Revision: D18425905
fbshipit-source-id: b86490542
Summary:
- Convert `task_generator` into a module of `ProcessPool` and collect inside the two combinators which were in semi-random places.
- Make `SyntacticCallGraph` export a `task_generator` as opposed to a call-graph builder.
- Separate `target` type and put it in its own module to avoid dependency cycles.
Reviewed By: skcho
Differential Revision: D18425718
fbshipit-source-id: 7957edac8
Summary:
`typecheck_instr` is a function that essentially does most of nullsafe typechecking
work: it pattern matches the instruction and handles most of business logic (e.g. knowledge about builtins, rules of PropagatesNullable, flow-sensitive rule for condition branches etc etc etc.
This is a gigantic function consisting of huge amount of nested
function. No way it can fit in someone's head and it is super hard to
read. It also captures many things like node and node'.
This diff does fairly shallow work:
1. Moves most of nested subfunctions into top-level functions. It also
means that what was previously hiddenly captured is now made an explicit
dependency.
2. Some (minority) of them are renamed to better indicate the context.
3. Some (minority) of params are renamed to clear indicate the
difference.
4. Some params are made named params, especially booleans and params
that have the same types so could be confused.
5. In some placed, added bit more clear comments.
This diff DOES NOT do:
1. Tries to fully resolve confusion between cryptic names. In couple of places, instead of node'
and node we use node and original_node, which is barely better. But we
still have ugly things like typestate and typestate1 leaving together.
Baby steps!
2. Tries to create better or consistent names in functions. I did it for
most obvious cases, that's it.
3. Order or params is arbitrary. I just used the order that was easy to
come up with, no consistency here.
Reviewed By: artempyanykh
Differential Revision: D18425965
fbshipit-source-id: 7a775f08d
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:
We still have few remaining places which we have a logic not encoded in
as a Nullability type. Ignoring third party param calls is one of them.
We don't want this behavior for strict mode.
Reviewed By: artempyanykh
Differential Revision: D18396639
fbshipit-source-id: dbfedc769
Summary:
The upcoming whole-program analysis will need to log reports in different source files simultaneously.
Here, the data structure containing the reports, and in charge of deduplication is generalised to
a map from source file to what it was previously. This way, writing out the reports is possible even
with multiple source files.
Reviewed By: skcho
Differential Revision: D18394994
fbshipit-source-id: 5f5ecc27c
Summary:
This is a dirty hack to make nullsafe behave consistently for internal
and external models.
Medium term this code needs to be rewritten in a better way, so that we
pass all information in annotated signature (either in form of Inferred
nullability, or type origin, which tracks third party calls).
As a follow up, we will make reporting more clear.
Reviewed By: artempyanykh
Differential Revision: D18372660
fbshipit-source-id: 12c2449e1
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:
Ability to accept relative path is convenient for testing and local
debugging.
Ability to accept absolute paths is needed for buck integration - buck
knows absolute path (to properly invalidate cache when the content of
the folder is changed) and passes it to infer.
Reviewed By: artempyanykh
Differential Revision: D18370407
fbshipit-source-id: be7f12ae1
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:
In next diffs, we will:
1/ teach nullsafe to read nullability information from the 3rd party
annotation folder
2/ use this storage in addition to our hard-coded
models to respect nullability during type-checking
Reviewed By: artempyanykh
Differential Revision: D18247538
fbshipit-source-id: ee45bc80e
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:
It extracts RHS of alias from `AliasTarget.t`, so it changes the `AliasMap` domain:
```
before : KeyLhs.t -> AliasTarget.t // AliasTarget.t includes KeyRhs.t
after : KeyLhs.t -> KeyRhs.t * AliasTarget.t
```
Reviewed By: ezgicicek
Differential Revision: D18299537
fbshipit-source-id: 1446580a8
Summary: We only care about expensive invariant calls. Let's disable the usual one since it is not used and there is no point filling up our dbs.
Reviewed By: dulmarod
Differential Revision: D18298530
fbshipit-source-id: 7a933c8da
Summary:
More rigid format for 3rd party annotation repo
To simplify external processing by tools, lets not accept any divergence from a
format, which is:
<fully qualified class name>#<method_name>(<params>)[ Nullable]
<params> = <list of param separated by ", ">
<param> = [Nullable ]<fully qualified type>
Particularly:
- Dont accept spaces in arbitrary places
- Require a single space after each comma separating params
- Require a single space between closing parethesis and nullable
annotation, if present
- Require at least one '.' in a class name (to prevent errors when
somebody did not specify a package).
This diff also makes error messaging more user-friendly, because now it
is easy to do a minor mistake like forget a space after comma.
Reviewed By: asm89
Differential Revision: D18297382
fbshipit-source-id: 91aab6823
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:
Now that we have two similar functions, it becomes confusing, because `Pp.to_string` and `Pp.string_of_pp` can seem to do the same stuff, while in reality they do the opposite.
Well, it is still bit confusing, because the proper names would be
`Pp.pp_of_to_string` and `Pp.to_string_of_pp`, but I think this high
level order names are not necessary given that in most cases they will
be used as concrete functions.
I think `Pp.of_string` captures such usages better than `to_string` used to do: you need to pp stuff,
but you have a string (or, technically, a function that returns a string), so you pretty print OF that string, aren't you?
Reviewed By: jvillard
Differential Revision: D18245876
fbshipit-source-id: fd4b6ab68
Summary:
This is a helper module for reading info from a 3rd party nullability repository.
Next diffs are going to use it for reading nullability repository from
disk.
Reviewed By: artempyanykh
Differential Revision: D18225473
fbshipit-source-id: 06a2dc97e
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:
When reporting null dereference it is useful to know where the null came
from.
Reviewed By: skcho
Differential Revision: D18206459
fbshipit-source-id: 0c8e6781b
Summary:
This simplifies the code overall. It also makes accessing the action of
a "trace" (which is now stored alongside it instead of deep inside it)
constant time instead of linear in the number of nested calls.
Reviewed By: skcho
Differential Revision: D18206460
fbshipit-source-id: 9546ff36f
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:
Instead of checking that each address in the pre that must be valid is
not invalid in the caller (and error out if it turns out it is invalid)
as we discover them, save these checks for after we are sure that the
precondition can be applied. It is in fact a bug that we can report an
error when trying to apply a precondition that is actually not
satisfiable in the current state for other reasons than lifetime issues.
We still want to skip calls in case of weird issues like mismatch in
number of formals vs actuals.
This will have more obvious effects later when we also check that
arithmetic facts in preconditions are satisfied at the call site: if a
pre mandates "x=1" and "y must be valid" and we have "x=0" and "y
invalid" then we shouldn't report an error.
Reviewed By: skcho
Differential Revision: D18115229
fbshipit-source-id: ad4ce72ff
Summary:
If a precondition cannot be applied, it means that this program path
somehow doesn't make sense for the caller and so should be pruned. Right
now we just treat this as skipping over the call instead.
This will become more important when specs start mentioning arithmetic
facts that must be satisfied at the call site. As it is we will only
stop if we discover aliasing in the pre not present at the call site or
vice versa.
Reviewed By: dulmarod
Differential Revision: D18115230
fbshipit-source-id: 4f1c7a583
Summary: The way `<=` is used in `AbstractDomain` prevents infix use and forces bracketing it everywhere. Replace with simple `leq`.
Reviewed By: jvillard
Differential Revision: D18201854
fbshipit-source-id: 8175224e4
Summary: Abstract state tracks stuff that is not needed for summaries, wasting space/time.
Reviewed By: jvillard
Differential Revision: D18171499
fbshipit-source-id: 25483ced9
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:
This diff adds SafeInvertedMap, which is similar to InvertedMap but it
guarantees that there is no top elements in the tree of the map.
Reviewed By: ezgicicek
Differential Revision: D18062174
fbshipit-source-id: 2fbc51f31
Summary: `Str.regexp_string` should be used to find a method name instead of `Str.regexp`.
Reviewed By: ezgicicek
Differential Revision: D18136598
fbshipit-source-id: c4b56dd64
Summary:
The reporting phase would go through the critical pairs in the summary roughly three times, once for each major type of warning (starvation, lockless violation, deadlock). This is wasteful, and also led to some code duplication. Fix.
Also, use the more efficient annotation matcher in `ConcurrencyModels` and move some model matchers to `StarvationModels`.
Reviewed By: artempyanykh
Differential Revision: D18118149
fbshipit-source-id: ff4dc3d07
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 will be more useful later when adding another one.
Reviewed By: ezgicicek, jberdine
Differential Revision: D18115231
fbshipit-source-id: a0a01901a
Summary:
The business of translating `Top/True/False` to `true/false` can be
hidden more.
Reviewed By: skcho
Differential Revision: D18115228
fbshipit-source-id: 071fcbddf
Mitya Lyubarskiy
Jules Villard
Dulma Churchill
Nikos Gorogiannis
Ezgi Çiçek
Sungkeun Cho
Josh Berdine
Martin Trojer