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 enables us to quickly pick up the Component typ when checking which required props to check.
Reviewed By: skcho
Differential Revision: D18807925
fbshipit-source-id: 47e407394
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: This diff adds a map from an object to a set of methods that has been called.
Reviewed By: ezgicicek
Differential Revision: D18781461
fbshipit-source-id: 47c10adaa
Summary: This adds a map from access expressions to locations where specific object is created by `create` method call.
Reviewed By: ezgicicek
Differential Revision: D18779985
fbshipit-source-id: f327450cd
Summary: This diff stack is to revise overall domain and semantics of litho checker. Some of the following diffs will not have visible changes until we replace the current checker with the new one.
Reviewed By: ezgicicek
Differential Revision: D18779592
fbshipit-source-id: d210d9bd1
Summary:
This can happen for a number of reasons that are not errors (mostly the exit node being unreachable) so isn't actionable, and definitely not worth showing the user. It could be a debug message but I don't think that's even worth it. Other checkers don't warn in similar circumstances.
With OCaml 4.08 we started actually seeing these error messages (differences in flushing behaviour?) so their annoying nature was revealed.
Reviewed By: ngorogiannis
Differential Revision: D18808460
fbshipit-source-id: a47a1dcb4
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: The clang plugin exports C++ mangled names in hashed form for perf reasons, so we need to hash the incoming mangled names in the profiler samples, so that we can compare them.
Reviewed By: skcho
Differential Revision: D18761842
fbshipit-source-id: 3072b5e33
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:
For now lets support the simplest form: "//"-style comments.
Having comments is useful:
1. It serves as documentation for API.
2. It serves as justification of why such and such method or param is
nullable or not (so the future readers can understand the reasoning of
the person who added the signature).
Reviewed By: artempyanykh
Differential Revision: D18762289
fbshipit-source-id: 90c515ea8
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 enables parsing and auto-formatting documentation
comments (aka docstrings).
I have looked at this entire diff and manually made some changes to
improve the formatting. In some cases it looked like it would take too
much time, or benefit from someone more familiar with the code doing
it, and I instead disabled auto-formatting docstrings in those files.
Also, there are some source files where the docstrings are invalid,
and some where the structure detected by the parser appears not to
match what was intended. Auto-formatting has been disabled for these
files.
Reviewed By: ezgicicek
Differential Revision: D18755888
fbshipit-source-id: 68d72465d
Summary:
RacerD is angelic in the sense that when a method has no summary, no accesses are added to the symbolic state when we call that method. However, when the method returns an object we then proceed to access, this leads to non-angelic behaviour: if the object is assumed to be un-owned, then the accesses may lead to a race.
This manifests itself on Litho components, which are generated code without sources and thus RacerD has no CFG to analyse, and therefore produces no summary. The `Builder` patterns used in these classes are ubiquitous, and full of spurious races due to the fact that the returned objects, even though freshly allocated, are un-owned as far as RacerD knows.
Here, instead of going full-angelic and assuming that every method without a summary returns an owned object (which is a bit extreme), we try to model the `Builder` pattern wrt ownership. That is, static `create` methods returning `Builder` types are assumed to return full ownership; and, non-static methods of a `Builder` class which return the same type as their receiver are assumed to return conditional ownership.
Reviewed By: ezgicicek
Differential Revision: D18748423
fbshipit-source-id: bd53d4b67
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:
We already have a number of `[pkg].Preconditions.checkNotNull`
modelled, but the one from `androidx` is missing yet widely used.
Reviewed By: mityal
Differential Revision: D18748550
fbshipit-source-id: 83d3317ae
Summary:
The introduction of inferbo intervals as pulse attributes creates the
first relational attributes. To make sense of inferbo intervals
appearing in summaries when in a caller context, we need to substitute
the abstract values they contain in the callee with the abstract values
they correspond to in the caller.
This has a significant consequence: we have to delay the check that
arithmetic constraints in the callee are satisfiable at the call-site
until *after* we have discovered all the relationships between callee
values and caller values from the heap. To solve this, we now run an
arithmetic constraints check *after* having materialised all the
addresses.
We also need to translate the abstract values in the attributes in the
post before recording them in the caller, for the same reasons.
Quite some code in this diff is concerned with substituting pulse values
inside inferbo intervals. There is a complication there too: even after
having discovered relationships between caller and callee abstract
values induced by the heap shapes, there could be abstract values in the
callee's attributes that we haven't seen yet. We need to make up new
values for these in the caller, so this substitution has to return a
potentially extended substitution.
Reviewed By: skcho
Differential Revision: D18745695
fbshipit-source-id: 077ae7670
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 extends semantics of binary operator for BoItv. If there is no known interval value for a pulse value, it returns a symbolic value of the pulse value.
Reviewed By: jvillard
Differential Revision: D18726768
fbshipit-source-id: ed8ecf78b
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 will make our analysis more precise. E.g. in the future we can classify
"condition redundand" warnings by origin, and warn only for
InferredNonnull, or autogenerate fixes based on the origin.
Error messaging does not currently take into account origin for nonnull
types, but this can be changed in the future
Reviewed By: ngorogiannis
Differential Revision: D18685304
fbshipit-source-id: 6a1f263f5
Summary: The debugger in the middle of the evaluation makes working on that file difficult. Separating modules a bit, so that we can change the code easier. This is in preparation to trying to add aliases and witnesses to formulas in a next diff.
Reviewed By: jvillard
Differential Revision: D18708542
fbshipit-source-id: 523f30fc9
Summary: The tableaux evaluation was an experiment and it was turned off because of bad perf. Let's kill it to clear up the code.
Reviewed By: jvillard
Differential Revision: D18708388
fbshipit-source-id: 099f5a3d3
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: Rather than repeatedly matching actuals, let's use `ProcnameDispatcher.ModeledCall` to pick up the actual arguments with their corresponding values. This simplifies the models.
Reviewed By: jvillard
Differential Revision: D18685855
fbshipit-source-id: 7788bd8bb
Summary: This diff removes `'markers` and `'captured_types` from the procname dispatcher. They are for checking an integrity when a type is captured from template parameters then it is used to match in parameters. However, we have not used that feature, so which simply complicates the types in the dispatcher without any gain at the moment.
Reviewed By: jvillard
Differential Revision: D18706254
fbshipit-source-id: f493778d7
Summary: Preperation diff to use `ProcnameDispatcher` for Pulse: it changes function arguments, i.e. `ProcnameDispatcher.Call.FuncArg`, to a record in order to track the value of arguments. To do that, it changes `ProcnameDispatcher.Call` into a functor so that we can parametrize over the type of the value without making changes upwards.
Reviewed By: jvillard
Differential Revision: D18590224
fbshipit-source-id: 6a13fbc1a
Summary:
This will allow us tune nullsafe behavior in a more fine-grained way.
See e.g. a follow up diff when we report errors more clearly.
Reviewed By: ngorogiannis
Differential Revision: D18683747
fbshipit-source-id: 7b5c42a03
Summary:
We were wrongly not supressing third-party calls in
case third party repo is provided: there was a bug in the function is_modelled_externally.
because of this we accidentally stopped supressing third party and
started to advertise it in non-strict mode.
we do plan doing that, but little bit further ahead :)
So let's add a param guiding this.
Reviewed By: artempyanykh
Differential Revision: D18658271
fbshipit-source-id: 703f2675b
Summary:
We will migrate to the new representation in the future, but for now
let's keep both active.
Reviewed By: artempyanykh
Differential Revision: D18657955
fbshipit-source-id: 9deb03f1f
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:
The infer/src/c_stubs directory contains a dune-project file. This
causes ocamlformat to conclude that the root of the project is
infer/src/c_stubs, and there is no .ocamlformat file there, so it does
not apply to the Fnv64Hash.ml file.
(There is currently a bug where it does apply anyway, but it is fixed
in master.)
Reviewed By: dulmarod
Differential Revision: D18684831
fbshipit-source-id: bcb53ce94
Summary:
Some field types of structs are missing in Java. The reason is:
* When capture, empty struct types are added without their fields.
* The empty struct types are overwritten to the global tenv when merging all tenvs.
As a fix, this diff add a boolean field, `dummy`, in `Typ.Struct.t`, then avoids that non-dummy types are replaced by dummy types.
Reviewed By: ngorogiannis
Differential Revision: D18657323
fbshipit-source-id: 4a263f8e7
Summary:
This is a better home for knowing whether a function has sentinel args
according to its prototype declaration.
Reviewed By: dulmarod, artempyanykh
Differential Revision: D18573919
fbshipit-source-id: 13f58eaa2
Summary: Another dead flag that one could mistakenly think is accurate.
Reviewed By: dulmarod
Differential Revision: D18573925
fbshipit-source-id: 129a9cff5
Summary:
This was never set to true except in a wrong way in the Java frontend
(see previous diff).
Reviewed By: dulmarod
Differential Revision: D18573927
fbshipit-source-id: 4c9d1a855
Summary:
This seems just wrong: the assume statement can return if the expression
is true.
Reviewed By: skcho
Differential Revision: D18573921
fbshipit-source-id: 47a5b0ea0
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: This diff get static value with `EMPTY` field from class initializer.
Reviewed By: ngorogiannis
Differential Revision: D18616588
fbshipit-source-id: 26414c9b2
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:
This allows us to move the CFG rendering to IR/.
The parts of that file concerning CFGs and those concerning Biabduction
specs were entirely disjoint, it turns out, so that was easy.
Reviewed By: jberdine
Differential Revision: D18573924
fbshipit-source-id: 0a5ab6478
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:
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
Summary:
Warning 33 (unused open) is enabled but the module open is not really
unused, it's just also opened at the top of the file...
Reviewed By: skcho
Differential Revision: D18114385
fbshipit-source-id: 2a8f9512a
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: As suggested by artempyanykh, this will make it bit more clear
Reviewed By: artempyanykh
Differential Revision: D18037204
fbshipit-source-id: 65cb96815
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:
Although, we have Makefile and BUCK build def, this is a maven project
which is supposed to be released to Maven Central, so it's worth
having a short instruction on how to build it with maven.
Reviewed By: mityal
Differential Revision: D18037109
fbshipit-source-id: 6aebf4384
Summary: Adding support to matching block names. We match mangled block names. We also needed to extend the function for extracting the range for each method, to also traverse the stmts to be able to find the block declarations.
Reviewed By: skcho
Differential Revision: D17956931
fbshipit-source-id: 707908812
Summary:
We support only class level annotations for now. We will add more when
we support more.
Reviewed By: artempyanykh
Differential Revision: D18036213
fbshipit-source-id: 44791318e
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:
Currently, we have NullsafeRules.ml responsible for detecting the
violation fact. All other logic: what should be the error type,
severity, and error message, is in TypeErr.ml.
In this diff, we move logic from NullsafeRules.ml and TypeErr.ml to
dedicated modules like AssignmentRule.ml etc.
Each such module is responsible for:
- detecting the violation fact (this is moved from NullsafeRules.ml)
- rendering the violation error (this is moved from TypeErr.ml).
This approach makes sense for two reasons:
1. The violation fact and the way we show error are logically related to
each other.
2. In future diffs, we will support more features guiding rule behavior,
such as a) decision whether to hide or show the error depending on type
information and mode; b) the way we render error depending on type
information and role.
Having dedicated modules incapsulating knowledge about rules is a natural way to support 2.
Reviewed By: artempyanykh
Differential Revision: D17977891
fbshipit-source-id: a53d916d3
Summary:
1. For each Nullsafe Rule, lets have a dedicated IssueType.
2. Split error reporting to three subfunctions: description, field type,
and infer issue.
This allows to introduce additional capabilities in a consolidated
manner. Example of such capabilities is should we hide or show an error,
what should be error severity depending on strictness mode, and how
exactly the error should be reported depending on how exactly
nullability is violated.
Reviewed By: artempyanykh
Differential Revision: D17977887
fbshipit-source-id: 860d67d2f
Summary:
This function can return `None` if the result is equal to the first
argument of join (why first?). It is unclear if it was an optimization
attempt of over-complicated logic.
Reviewed By: artempyanykh
Differential Revision: D17876561
fbshipit-source-id: 9628fb86e
Summary:
The goal of this logic is unclear:
1/ See the comments
2/ I can not see the scenario where classes and proper types can be
joined in a legit Java program
3/ Even it if was the case, I don't see how this heuristic is justified.
So I assume it is not.
Reviewed By: artempyanykh
Differential Revision: D17876568
fbshipit-source-id: c9c6cd604
Summary:
It is unclear what is the purpose of doing so, and it adds complexity to
codebase.
1/ The semantics of this is not clear, it more or less corresponds to
"where are all original locations that contributed to the type
calculation", but many branches in CFG have nothing to do with
nullability; also it was used not always consistently.
2/ The only place where this was used is logs, so this is no-ops. It is
unclear how seeing all locations can help debugging, given 3/ - see
below
3/ We have the right place to store such informatin, namely TypeOrigin,
where we store locations associated with types where we merge them in
CFG. Currently, we store only "winner" - the most relevant locations
that contributed to nullability in the most informative way. We show
this to the user when we report an error.
4/ If we want to support more things (e.g. show something more to the user), TypeOrigin
seems to be the right place. Or, alternatively, we might still merge
locations in `range`, but this will be better to organize in a tree form
instead of flat list that is not really informative and helpful. It is
all speculative though since need to support things like that seems
unclear.
Reviewed By: artempyanykh
Differential Revision: D17857198
fbshipit-source-id: 6cf6e48a2
Summary:
That module's interface was repeated twice to avoid exposing its
internals to PulseDomain itself. It's also quite long so it makes sense
to move it to its own file.
Reviewed By: ezgicicek
Differential Revision: D17977209
fbshipit-source-id: 56a2dac24
Summary:
Another poorman's library, this time about Pulse Domains. Also renames
`PulseDomain` to `PulseBaseDomain`.
Reviewed By: ezgicicek
Differential Revision: D17955287
fbshipit-source-id: 9c947cf98
Summary:
The name had rotten: it should be `AddrHistPair`. There is little value
of exposing the type of the pair `AbstractValue.t * ValueHistory.t`,
just inline its definition everywhere.
Reviewed By: ezgicicek
Differential Revision: D17955283
fbshipit-source-id: d145251e0
Summary:
See explanations in D17955104.
This renames `AbstractAddress` to `AbstractValue` since they are not
necessarily addresses.
Reviewed By: ezgicicek
Differential Revision: D17955290
fbshipit-source-id: 8bb4c61f2
Summary:
See explanations in D17955104. I put Attributes inside PulseAttribute
instead of creating a new file to avoid exposing more internals about
ranks.
Reviewed By: ezgicicek
Differential Revision: D17955284
fbshipit-source-id: a8719a58f
Summary:
Problem: PulseDomain.ml is pretty big, and contains lots of small
modules. The Infer build being a bit monolithic at the moment, it is
hard to split all these small modules off without creating some
confusion about which abstraction barries lay where. For instance, it's
fine to use `PulseDomain.ValueHistory` anywhere, but using `PulseDomain`
itself is sometimes bad when one should use `PulseAbductiveDomain`
instead.
Proposal: a poorman's library mechanism based on module aliasing. This
stack of diffs creates new Pulse* modules for all these small, safe to
use modules, together with `PulseBasicInterface.ml`, which aliases these
modules to remove the `Pulse` prefix. At the end of the stack, it will
contain:
```
module AbstractValue = PulseAbstractValue
module Attribute = PulseAttribute
module Attributes = PulseAttribute.Attributes
module CallEvent = PulseCallEvent
module Diagnostic = PulseDiagnostic
module Invalidation = PulseInvalidation
module Trace = PulseTrace
module ValueHistory = PulseValueHistory
```
This "interface" module can be opened in other pulse modules freely.
Reviewed By: ezgicicek
Differential Revision: D17955104
fbshipit-source-id: 13d3aa2b5
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: For Objective-C methods we match the mangled names (the field is name in the profiler samples).
Reviewed By: skcho
Differential Revision: D17952552
fbshipit-source-id: 308d415f6
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:
- Adds ATD file to parse the clang profiler samples
- Procnames don't help us here because we want to use mangled names, not the version of names that Infer needs, so passing in the RangeMap also ClangProc that just include the names and mangled names.
- First matching of c functions to have something in place to add a test, matching further method kinds to be done in next diff.
Reviewed By: skcho
Differential Revision: D17877071
fbshipit-source-id: b31d651a7
Summary:
I dunno, seemed wrong before. About to introduce another attribute with
similar arguments so making them consistent in advance.
Reviewed By: skcho
Differential Revision: D17930349
fbshipit-source-id: 944b58bac
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:
- Putting test determinator in own directory
- Putting Java procname creation stuff in its own module
Reviewed By: skcho
Differential Revision: D17929885
fbshipit-source-id: 4f2578566
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:
This will avoid printing stuff like
"0$?%__sil_tmpSIL_materialize_temp__n$2 declared" to the poor
unsuspecting user. The non-verbose stuff is used only by pulse so far as
far I can tell so hopefully this doesn't break anything.
Reviewed By: ezgicicek
Differential Revision: D17908943
fbshipit-source-id: 8ef4f1a8f
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:
First step in having a value domain: record concrete values. We record
them as equalities to abstract values using a new attribute `Constant`.
In a way, attributes are already our "pure" part in the "formulas" that
are pulse abstract domains, so this is reminiscent of existing
separation logic implementations. Trying to add values directly in the
"heap" part proved very cumbersome whereas this approach is very simple,
allowing us to ignore values most of the time except when we actually
care.
Reviewed By: skcho
Differential Revision: D17665473
fbshipit-source-id: b8033ad9c
Summary:
It's annoying to see `sexp_list` everywhere instead of `list`, eg in
merlin.
See also D17907938.
Reviewed By: ngorogiannis
Differential Revision: D17927994
fbshipit-source-id: 84599e8bc
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:
By some unfortunate logic, OCaml often decides to use
`sexp_list`/`sexp_option` instead of just `list`/`option`. Sometimes
these get copy/pasted in interface files.
It would be good to tell OCaml not to do that in the first place but in
the meantime: this diff.
Reviewed By: ngorogiannis
Differential Revision: D17907938
fbshipit-source-id: 7546834a2
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:
Describe what the --report-*-* options actually do instead of their
outdated documentation from the time where this was
`--checkers-blacklist-regex`, `--infer-blacklist-regex` and the like.
Reviewed By: dulmarod, mityal
Differential Revision: D17906015
fbshipit-source-id: 204349e9e
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: Not used feature and with no obvious roadmap anymore.
Reviewed By: jberdine, jvillard
Differential Revision: D17855860
fbshipit-source-id: fd75b9d62
Summary: This makes more explicit what we are talking about here. Also, in extending test determinator to clang, the name is incorrect, but the set is generic procnames which is fine to use for clang, just the name is wrong.
Reviewed By: ngorogiannis
Differential Revision: D17855338
fbshipit-source-id: e93bae083
Summary: This diff models the cost of `ImmutableSet.chooseTableSize(setSize)` as `O(log setSize)` and `construct(n, ...)` as `O(n)`.
Reviewed By: ezgicicek
Differential Revision: D17829850
fbshipit-source-id: 0ee318cc3
Summary:
This diff fixes a data race in ProcessPool: out channel flush was
outside of the critical section.
Reviewed By: ezgicicek
Differential Revision: D17853991
fbshipit-source-id: ac0fd2a69
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:
Starvation analysis keeps a trace documenting why a method is seen as on the UI thread (many reasons possible, often confusing). This was a call-stack plus string, for keeping the explanation of why the last callee is on the UI thread. This is bad, because it takes too much memory/storage (each string is custom-made to the classes/method involved), and is effectively untyped.
Switch to a proper type for explaining this, so the cost is just a few pointers plus shared procnames/types, and then convert to string only when reporting. This will also allow to push the UI trace inside each element of the starvation domain, so as to allow path sensitivity etc, without blowing up summary size.
Reviewed By: ezgicicek, artempyanykh
Differential Revision: D17810007
fbshipit-source-id: cdd743975
Summary:
This diff proceeds work for consolidating nullsafe logic and making it
type-agnostic
Reviewed By: artempyanykh
Differential Revision: D17808485
fbshipit-source-id: 85356c625
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:
This proceeds work on abstracting out operations requiring raw
nullability operations from infer core code. This will simplify coming
introducing of intermediate nullability levels
Reviewed By: artempyanykh
Differential Revision: D17789612
fbshipit-source-id: 9a2bea2ed
Summary:
In previous refactoring stages, we operated on AnnotatedNullability
(nullability of a field or method signature together with its origin),
and InferredNullability (nullability of a value in typestate together
with its origin).
Now it is time to extract common Nullability as a type system concept,
together with `<:` and `join` functionality. This was sketched in
`NullsafeRules`, so this diff consolidates this as well.
In follow up diffs, we will reduce/get rid of direct usages of things like
`InferredNullability.is_nullable`. This will simplify introducing
intermediate Nullability types.
Reviewed By: artempyanykh
Differential Revision: D17789599
fbshipit-source-id: f1b9d2dd0
Summary: StarvationModels depended on StarvationDomain which is the wrong way around, and forbids using *Models from *Domain.
Reviewed By: mityal
Differential Revision: D17809431
fbshipit-source-id: 5aa369e7c
Summary: The type hierarchy was traversed multiple times when searching for annotations: once for methods/overrides annotated and once for superclasses. This can be done in one pass.
Reviewed By: dulmarod
Differential Revision: D17787172
fbshipit-source-id: 248dd4c27
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: The regexp would match `ge` and is also unnecessary and was compiled on every call. Save some cpu cycles while fixing it.
Reviewed By: jvillard
Differential Revision: D17789586
fbshipit-source-id: a3f6612c6
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:
Currently, lock state is a map from locks to stacks of lock acquisitions.
Since we now have the separate acquisitions component, we no longer need to
remember the stack of acquisitions for a lock. Instead we only need a lock count,
thus reducing the memory footprint.
At the same time, change acquire and release so that they make one tree operation per
component (map/acquisition) as opposed to two (search/update) operations.
Reviewed By: ezgicicek
Differential Revision: D17736727
fbshipit-source-id: 7579eb61e
Summary:
If we acquire n nested locks we end up with n critical pairs, and for each pair the held-locks component goes up linearly, thus total space/time is O(n^2).
If the sets of held-locks are constructed with maximal sharing (intuitively, if they derive from the same set by additions) then the total space/time is O(n logn).
To do this, we must avoid constructing a new set every time we ask what the currently held locks are. Here we maintain (care is needed in the presence of recursive locks) that set across lock acquisitons and removals.
Reviewed By: skcho
Differential Revision: D17736252
fbshipit-source-id: 0f9b292c4
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: This diff fixes a potential race in writing to pipe channel.
Reviewed By: ngorogiannis
Differential Revision: D17710123
fbshipit-source-id: 477492750
Summary:
The old domain keeps two sets:
- `events` are things (including lock acquisitions) which eventually happen during the execution of a procedure.
- `order` are pairs of `(lock, event)` such that there is a trace through the procedure which at some point acquires `lock` and before releasing it performs `event`.
A deadlock would be reported if for two procedures, `(lock1,lock2)` is in `order` of procedure 1 and `(lock2,lock1)` is in `order` of procedure 2. This condition/domain allowed for the false positive fixed in the tests, as well as was unwieldy, because it required translating between the two sets.
The new domain has only one set of "critical pairs" `(locks, event)` such that there is a trace where `event` occurs, and *right before it occurs* the locks held are exactly `locks` (no over/under approximation). This allows keeping all information in one set, simplifies the procedure call handling and eliminates the known false positive.
Reviewed By: mityal
Differential Revision: D17686944
fbshipit-source-id: 3c68bb957
Summary: Holding a master lock and then acquiring two other locks inside can generate a false positive as shown.
Reviewed By: mityal
Differential Revision: D17710076
fbshipit-source-id: 5bc910ba2
Summary:
Previously deduplication was always on which is not great for testing.
Also split tests so that we can still test deduplication separately.
Reviewed By: mityal
Differential Revision: D17686877
fbshipit-source-id: 280d91473
Summary:
The documentation and uses of filtering disagree. One typical usage is deduplication.
Split that where obvious, add comments where not obvious, and leave alone when obviously unrelated to deduplication.
Reviewed By: mityal
Differential Revision: D17715329
fbshipit-source-id: ec757927b
Summary:
Ideally the analyser should equate locks `this.x.f` and `a.x.f` in different methods if they can alias.
The heuristic removed here was rarely used and is in the way of a re-write of the analysis.
It was also badly implemented, as this should ideally be the comparison relation of `Lock`.
Reviewed By: mityal
Differential Revision: D17602827
fbshipit-source-id: 4f4576c1a
Summary:
This diff generates a symbolic value when a function returns only
exceptions. Previously, the exception expression is evaluated to top,
thus it was propagated to other functions, which made those costs as
top. For preventing that situation, this diff changed:
* exception expressions are evaluated to bottom, and
* if callee's return value is bottom, it generates a symbolic value
for it.
Reviewed By: ezgicicek
Differential Revision: D17500386
fbshipit-source-id: 0fdcc710d
Summary: This diff introduces an inequality for the size alias targets, in order to get preciser array lengths after loops. The alias domain in inferbo was able to express strict equality between alias source and its targets, e.g. x=size(array). Now, for the size alias target, it can express less than or equal relations, e.g. x>=size(array).
Reviewed By: ezgicicek
Differential Revision: D17606222
fbshipit-source-id: 2557d3bd0
Summary: Component.Builder has its own non-required props that are inherited by the MyComponent.Builder. Add tests where these common props are set in the chain of calls.
Reviewed By: Katalune
Differential Revision: D17710294
fbshipit-source-id: f3c5ef28c
Summary:
This reverts commit 9d5c322202a479e73b60f00ffb318f1c7948e407.
INFERVERSION forcing a version check proved to be problematic for
integrations, thus is reverted.
Reviewed By: ngorogiannis
Differential Revision: D17627638
fbshipit-source-id: f988207aa
Summary:
This diff is to refactoring some stuffs for the following diff.
* revised pretty print of the alias domain
* moved `eval_array_locs_length` to `BufferOverrunSemantics`.
Reviewed By: jvillard
Differential Revision: D17667123
fbshipit-source-id: c95611df5
Summary:
Sawja and Javalib have recently released new versions that drop off
the camlp4 dependency. This is a minimal diff in order to update infer
opam depedencies.
Last (1.5.7) generates invokedynamic, but work on InvokeDynamic is still
in progress in Infer and not activated here yet. In this version, the
Java frontend will still replace any InvokeDynamic by a dummy
InvokeStatic call (as introduced by Jeremy a long time ago).
Reviewed By: jvillard
Differential Revision: D17662979
fbshipit-source-id: f686ba442
Summary:
Unfortunately it is very hard to predict when
`Typ.Procname.describe` will add `()` after the function name, so we
cannot make sure it is always there.
Right now we report clowny stuff like "error while calling `foo()()`",
which this change fixes.
Reviewed By: ezgicicek
Differential Revision: D17665470
fbshipit-source-id: ef290d9c0
Summary:
Having just numbers for abstract values is a tad confusing. The change
is also needed for having actual constant values later.
Reviewed By: ezgicicek
Differential Revision: D17665469
fbshipit-source-id: 20dff7bbe
Summary: `Prop(varArg = myProp) List <?> myPropList` can also be set via `myPropList()` or `myProp()`. Add support for picking up the `varArg` and checking this form of required props.
Reviewed By: ngorogiannis
Differential Revision: D17571997
fbshipit-source-id: 7956cb972
Summary:
Turns out `Memory.add_attributes` was only used to add singletons so
deleted that in the process.
Reviewed By: skcho
Differential Revision: D17627725
fbshipit-source-id: 0abe3889d
Summary:
This was bogus: when evaluating `e[e']` we were checking that `e'` is a
valid pointer.
Reviewed By: ezgicicek
Differential Revision: D17627727
fbshipit-source-id: 536384e95
Summary:
This is a preparation for coming introducing of Unknown nullability.
When this happens, a value will be able to be neither nullable, nor
non-nullable.
This will break many checks that implicitly assume "not nullable means non-null".
In this diff, we review all such checks and change them accordingly.
Reviewed By: artempyanykh
Differential Revision: D17600177
fbshipit-source-id: c38d87175
Summary:
It took a while for me to figure out what does this method do; the
reasons were:
1. a lot of names were cryptic and/or misleading
2. because everything is inline one needs to read everything to figure
out what is going on here.
So this diff changes the names a bit and moves some of methods outside.
This is still far not perfect, but I believe it is better than was
before.
Reviewed By: artempyanykh
Differential Revision: D17600175
fbshipit-source-id: ca7175b2e
Summary:
Eradicate.ml is way too big to reason about.
This diff is shallow, it does only the following:
1. Moves the module
2. Adds documentation in the header.
3. Exports two public methods as is
4. Adds corresponding params to all methods for values that were
captured in the module-as-closure before
Reviewed By: artempyanykh
Differential Revision: D17600173
fbshipit-source-id: ba7981228
Summary:
Turns out, we did not have such a test in place.
Known issue: we report over-annotated warnings for each fields N times,
one per constructor, which is wrong.
Reviewed By: artempyanykh
Differential Revision: D17574791
fbshipit-source-id: def992691
Summary:
Now, that we consistently use `AnnotatedType`, `AnnotatedNullability`,
and `AnnotatedSignature`, `AnnotatedField` is a natural name for this
datatype.
Together `AnnotatedSignature` and `AnnotatedField` represent two entry
points for fetching information about Java type from the codebase.
Reviewed By: artempyanykh
Differential Revision: D17570534
fbshipit-source-id: 31ef52033
Summary:
1. This diff finishes the work of getting rid of using `Annot.Item.t`
for making judgements about nullability. Instead, `AnnotatedNullability`
is now used consistently in the codebase. Corresponding TODO items are
deleted.
2. This diff proceeds consolidating checks to `NullsafeRules` (which
will simplify introducing non-binary nullability in follow up diffs).
3. Code is simplified: we get rid of `fold2/ignore` + inlined
calculation of the param position in favor of
more straightward `zip` + `iteri` combo.
Reviewed By: artempyanykh
Differential Revision: D17570439
fbshipit-source-id: 52acf2c66
Summary:
This continues work of getting rid of using low-level Annot.Item.t in
favor of a new, more specific and flexible data structure.
Migrating this code further to NullsafeRules is bit tricky right now, so
let's defer it.
Reviewed By: ngorogiannis
Differential Revision: D17549479
fbshipit-source-id: 418b4b394
Summary:
This diff also introduces "subtyping function" into NullsafeRule, which
will be the core check for other rules we will introduce in follow up
diffs
Reviewed By: ngorogiannis
Differential Revision: D17500466
fbshipit-source-id: 5821caa6e
Summary:
As suggested by artempyanykh:
1. Since we recently introduced InferredNullability, AnnotatedNullability deserves its own class which now plays nicely with its counterpart.
2. AnnotatedType is more specific then NullsafeType
Reviewed By: artempyanykh
Differential Revision: D17547988
fbshipit-source-id: 785def23a
Summary: The analysis is not intra-procedural, hence we don't really read the payload. Let's remove it.
Reviewed By: ngorogiannis
Differential Revision: D17603911
fbshipit-source-id: c92b5c602
Summary:
This diff avoids giving the top value to unknown globals in Java,
because they harm precision of the cost checker. Instead, it doesn't
subst the global symbols at function calls.
Reviewed By: ezgicicek
Differential Revision: D17498714
fbshipit-source-id: d1215b3aa
Summary:
This diff adds an eval mode for the substitutions of the cost results, in order to avoid precision
loss by joining two symbols.
The usual join of two different symbolic values, `s1` and `s2`, becomes top due to the limitation of
our domain. On the other hand, in the new eval mode, it returns an upperbound `s1+s2`, because the
cost values only care about the upperbounds.
Reviewed By: ezgicicek
Differential Revision: D17573400
fbshipit-source-id: 2c84743d5
Summary:
This was causing a crash, because when trying to create a procname from a block at that point we don't have the block return type, which is needed for the name. I don't understand why BlockDecl doesn't contain the type, but I looked again and it doesn't (also in clang). So in general we need to pass it from the context, but that's not possible in this case.
Also, one could argue that such a block is not a method from the struct, since it's just a block that is assigned to a field as initialization.
Reviewed By: skcho
Differential Revision: D17575197
fbshipit-source-id: 3974ead3f
Summary: When we have an annotation like `Prop(varArg = X)` or ` ThreadSafe(enableChecks = true)`, we were not able to pick up the names of the parameters like `varArg` or `enableChecks`. This diff fixes that.
Reviewed By: skcho, ngorogiannis
Differential Revision: D17571377
fbshipit-source-id: 5293b5810
Summary:
Events can be many things, including lock acquisitions. Lock state keeps a set of events, all of which must be lock acquisitions.
Enforce this via the type checker by specialising the types so that lock state satisfies this by construction.
Reviewed By: ezgicicek
Differential Revision: D17571428
fbshipit-source-id: 2f5a33b98
Summary:
Instead of polluting the signature of trace endpoints, have
the call printer be a module argument to the functors
producing trace elements.
Reviewed By: skcho
Differential Revision: D17550111
fbshipit-source-id: ab5af94c6
Summary:
This proceed the work of getting rid of Annot.Item.t.
This diff:
- Moves "check assignment rule" to recently supported NullsafeRules
- Implements their own "check overannotated" (defers consolidating this
check into NullsafeRule for the future diffs).
Note that we don't need PropagatesNullable logic anymore because it is
already ported to NullsafeType (return value will be marked as Nullable
in NullsafeType)!
implicit_nullable (a.k.a. Void types) will require a follow up diff to
model.
Reviewed By: artempyanykh
Differential Revision: D17499246
fbshipit-source-id: 14b473f29
Summary:
In nutshell, Nullsafe is driven by relatively simple set of rules.
It is currently not well reflected in code: we are duplicating the same logic in different places, which is:
- error prone (we need to adjust ensure all places are addressed if a new feature is introduced)
- complicates understanding of nullsafe
Consolidating checks will simplify introducing Unknown Nullability and
strict/partial check modes.
## this diff
This diff does it for one particular check.
See follow up diffs re that proceed consolidation.
## future diffs
Future diffs will:
- consolidate other checks that use 'assignment rule'
- introduce other rules, most notably 'dereference rule' and
'inheritance rule'
Reviewed By: artempyanykh
Differential Revision: D17498630
fbshipit-source-id: 079d36518
Summary:
Now, after series of modifications with TypeAnnotation, we are ready to
rename it to reflect what it means in the code.
See the documentation in the class for details.
Also:
- renamed methods for clarity
- added some documentation
- renamed local variables around the usages
Reviewed By: jvillard
Differential Revision: D17480799
fbshipit-source-id: d4408887a
Summary:
This continues work for eliminating Annot.Item.t from Nullsafe low-level
code.
The introduced function `from_nullsafe_type` is called when we infer
initial type of the equation based on the function or field formal signature.
Before that, we did it via reading the annotation directly, which
complicates the logic and making introducing Unknown nullability tricky.
## Clarifying the semantics of PropagatesNullable
This diff also clarifies (and changes) the behavior of PropagatesNullable params.
Previously, if the return value of a function that has PropagatesNullable params was
annotated as Nullable, nullsafe was effectively ignoring PropagatesNullable effect.
This is especially bad because one can add Nullable annotation based on the logic "if the function can return `null`, it should be annotated with Nullable`.
In the new design, there is no possibility for such a misuse: the code that
applies the rule "any param is PropagatesNullable hence the return
value is nullable even if not explicitly annotated" lives in NullsafeType.ml, so
this will be automatically taken into account.
Meaning that now we implicitly deduce Nullable annotation for the return value, and providing it explicitly as an alternative that does not change the effect.
In the future, we might consider annotating the return value with `Nullable` explicit.
Reviewed By: jvillard
Differential Revision: D17479157
fbshipit-source-id: 66c2c8777
Summary:
In the cost checker, the range of selected control variables are used to estimate the number of loop iteration. However, sometimes the ranges of control variables are not related to how many times the loop iteration. This diff strengthens the condition for them as:
1. integers from `size` models
2. integers constructed from `+` or `-`
3. integers constructed from `*`
For the last one, the loop iteration is likely to be log scale of the range of the control variable:
```
while (i < c) {
i *= 2;
}
```
We will address this in the future.
Reviewed By: ezgicicek
Differential Revision: D17365796
fbshipit-source-id: c1e709ae8
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:
As per previous diff, attempt to allocate fewer strings. This doesn't
seem to affect perf although allocating less might reduce memory
pressure.
Reviewed By: mityal
Differential Revision: D17423973
fbshipit-source-id: e2e37b071
Summary:
My spidey senses were tingling. Next diff uses the `pp` functions
everywhere it was kind of obvious how to change the code to do so. It
doesn't improve perf but is less clowny that way. It might lessen memory
pressure since allocating strings is expensive and this code was doing a
lot of it.
Reviewed By: ngorogiannis
Differential Revision: D17450324
fbshipit-source-id: 632cee584
Summary:
The code was already trying to do that but failing. Now it works.
This revealed a slight bug where the progress bar would always stop at
N-1/N 99% jobs. Fixed by moving the progress bar updates *after* the
operation that might decrease the number of jobs left.
Reviewed By: mityal
Differential Revision: D17423978
fbshipit-source-id: fc32db5f3
Summary:
Previously we would incorrectly report the time for the whole process
and this could include capture time too.
Reviewed By: mityal
Differential Revision: D17423977
fbshipit-source-id: b3ed754b3
Summary: We should be able to run this processing ast steps without running linters or capture. This also adds a new module ProcessAST to do the processing, Capture.ml should not know anything else than calling the respective modules for capture, linting or processing.
Reviewed By: ngorogiannis
Differential Revision: D17501453
fbshipit-source-id: 30adba5b1
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:
1/ Nikos Gorogiannis pointed out that
- for highly reused public types, records (especially when >= 3 params) are generally more readable than tuples.
- Records simplify code modifications, especially adding new fields. And we are going to add some, namely param flags, in the future.
2/ Let's make the fact that annotated signature is deprecated more
visible; it will also simplify searching for usages when we will be
getting rid of them.
Reviewed By: ngorogiannis
Differential Revision: D17475033
fbshipit-source-id: 7740c979b
Summary:
- Instead of merging one target DB into the main DB at a time, merge all target DBs into an in-memory DB (thus, no writing) and then dump it into the main DB at the end. This makes merging faster.
- When using the sqlite write daemon, there is no reason to drive the merge process from the master, sending each individual target to merge down the socket and doing one DB merge at a time. Here we move all the DB merging logic in the daemon, and expose a single function that does it all.
- Refactor some common functionality (notably the `iter_infer_deps` function is now in `Utils`) and remove dead files.
This can be also done using a temporary DB (which is not limited to memory) but this showed worse perf in tests than the in-memory solution as well as the current state of things (! possibly Sqlite-version related?).
Reviewed By: skcho
Differential Revision: D17182862
fbshipit-source-id: a6f81937d
Summary:
`get_field_annotation` is (together with
`get_modelled_annotated_signature`) an entry point when Nullsafe fetches
annotation information.
In follow up diffs we are going to utilize added information; see also
TODO in the code
Reviewed By: ngorogiannis
Differential Revision: D17475034
fbshipit-source-id: dab77bc7b
Summary:
"Unannotated" is misleading and ambiguous concept, it can have different
meanings depending on agreements.
The current logic treats them as Nonnull, which is exactly what we want
to preserve.
(If we need to partially model some functions where we don't have
opinion on some of types in the signature, we can explicitly model
unknown nullability later on).
Note that I am not aiming for substantial refactoring of
modelsTables.ml; the scope of this diff is merely to clarify things.
Reviewed By: ngorogiannis
Differential Revision: D17449347
fbshipit-source-id: 43c798ce7
Summary:
This function is the main entry point for getting annotated signature
for nullsafe.
We will modify it and its callees in follow up diffs to migrate other
features of Annot.items to specialized types.
Reviewed By: ngorogiannis
Differential Revision: D17448082
fbshipit-source-id: be00b4737
Summary:
This is a central abstraction for coming future unknown nullability support.
# Context
Annot.ml is a low-level module:
- it contains lists of raw (string) annotations
- no algebraic datatypes for annotations
- it mixes annotations that Nullsafe should be aware of with all sorts of other annotations
- some annotations make sense for return values, some make sense for params, and some make sense for methods.
But, most importantly, it does not contain information about source of an annotation, making it hard to distinct things like "Nonnull as default" vs "Nonnull as explicitly annotated" vs "Nonnull as modelled". Ditto for nullable.
Because of this, it is tricky to introduce unknown nullability in an elegant way.
Let's get rid of using Annot.Item.t in nullsafe code in the following way:
- Move nullability information associated with the Java type to a dedicated algebraic DT.
- Split other annotations that are important for nullsafe into param flags, ret value flags, and method flags, and introduce corresponding datatypes.
# This diff
This diff introduces NullsafeType and adds this to AnnotatedSignature.
It is not used yet, hence the diff is a no-op.
In future diffs, we are going to (see also TODOs in the code):
- actually use this information instead of accessing Annot.item
- add more information to AnnotatedSignature
- remove Annot.item from AnnnotatedSignature
- when this is done, introduce notion of unknown nullability.
Reviewed By: ngorogiannis
Differential Revision: D17420595
fbshipit-source-id: b30706d9b
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:
We historically had Model.Inference, which was an attempt to enhance
models with additional abilities to get the annotation.
This feature got removed in D9805110, including removing of the key
condition Models.Inference.field_is_marked.
This code also is not executed: `Config.eradicate` condition
was an old artefact of migrating Eradicate to callback infrastructure:
D1508451. We run eradicate only as a callback as of now, so this flag is
always true.
In follow up diffs we refactor AnnotationSignature module, and this
cleanup simplifies the refactoring.
Reviewed By: ngorogiannis
Differential Revision: D17419173
fbshipit-source-id: 1b30555de
Summary:
CONDITION_REDUNDANT_NONNULL was an attempt to reduce number of false
positives for condition redundant. (It is the most popular check as of
now).
The root case for most of false positives is that a lot of code is
simply not annotated (but should have been), so blaming developers for defense programming is
not actionable.
In attempt to solve the problem, a special issue type (for case when the
code is explicitly annotated with Nonnull) was introduced.
In follow up diffs we are going to introduce a generic way of doing the
same, not limited to this particular check only.
Namely, we will introduce notion of unknown nullability, so it will be
possible to distinguish not annotated yet (hence no warnings) and already
annotated (hence warnings) parts of code.
This piece of logic is incompatible with the aforementioned work, hence
we need to remove it.
Reviewed By: jvillard
Differential Revision: D17398768
fbshipit-source-id: 8bddf10e5
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 simplifies two similar alias targets: AliasTarget.Simple and
AliasTarget.SimplePlusA. Since the latter is simply extended version
of the former, they are better to have a common constructor.
Reviewed By: jvillard
Differential Revision: D17421416
fbshipit-source-id: e0946a73b
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 ignores field's type in their comparisons. They should be distinguished by their names and struct types.
Reviewed By: dulmarod
Differential Revision: D17284621
fbshipit-source-id: ae8a33083
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:
Sqlite versions set their own default page and cache size. Old versions use crazy-non-optimal settings.
Allow setting both from command line and set up reasonable defaults. See, e.g.,
https://wiki.mozilla.org/Performance/Avoid_SQLite_In_Your_Next_Firefox_Feature
for page size notes.
The defaults will cost a maximum of 64Mb in cache per Infer process. These improve merging times significantly.
Reviewed By: jvillard
Differential Revision: D17364643
fbshipit-source-id: b9abab10f
Summary:
At some point, there was a custom equality function that deliberately ignored some fields in err_instance. It was deleted in D4232422, so having a custom hash function does not serve any purpose anymore.
Since 2016 there was no known problems with the change in D4232422.
If we decide that we need similar behavior that was before D4232422, it will be easier to reimplement the functionality again.
Reviewed By: jberdine
Differential Revision: D17313660
fbshipit-source-id: 5c6c29a0b
Summary:
We want to allow following declaration
```
CK::UIContext t(foo);
```
In this case t is only part of the scope and we don't want to check that is never mutated.
Reviewed By: kfirapps
Differential Revision: D17367040
fbshipit-source-id: 5312a1249
Summary: Adding a test to the top level makefile that I forgot to add (ooops)
Reviewed By: jvillard
Differential Revision: D17366065
fbshipit-source-id: 8111ccf7a
Summary: This calls the method `delete_capture_and_analysis_data` introduced in D17184424 once the appropriate specs files for incremental analysis have been deleted. This fixes two bugs that I observed in incremental analysis that were arising because of stale state left in the results directory.
Reviewed By: ngorogiannis
Differential Revision: D17184424
fbshipit-source-id: d63f59db9
Summary:
I observed a bug in incremental analysis for thread safety analysis, where a thread safety violation was not being reported because the folder `racerd` was not being cleaned. This meant that the violation was determined to be a preexisting issue when it was actually an introduced issue.
This method can be used to fix this problem by cleaning the `racerd` folder. It also cleans the `captured` folder, I've done this following the original version of the method (see D16602417).
I'm not sure if the `captured` folder is used; it wasn't used in the tests I did. Thoughts about this?
Reviewed By: ngorogiannis
Differential Revision: D17261504
fbshipit-source-id: 8fea23e98
Summary:
There is currently a bug in incremental analysis because the capture data is not reset once the specs files have been invalidated. This has caused a problem where cost issues that should be reported are not spotted. I'm introducing this method so I can use it to fix incremental analysis.
This method is resurrected from D16602417
Reviewed By: ngorogiannis
Differential Revision: D17184401
fbshipit-source-id: e84925324
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: It prints debug information when top values is generated.
Reviewed By: ngorogiannis
Differential Revision: D17285448
fbshipit-source-id: 0621fd36d
Summary:
This check was an incomplete attempt to make nullsafe check nutritious
annotations for fields that get modified.
This was never fully productionized, and this check is turned off by
default.
In near future, we don't anticipate supporting this feature, so let's
remove it to simplify the code.
Reviewed By: artempyanykh
Differential Revision: D17282015
fbshipit-source-id: d63a2f1f7
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 diff makes the checkers, except biabduction, to use `typ` instead
of `root_typ` of `Load`/`Store` statemetns.
Reviewed By: dulmarod
Differential Revision: D17203105
fbshipit-source-id: 8be9b5158
Summary:
It adds typ field in Sil.Store. The field will be used by the analyzer in the following diffs.
Motivation: Interbo generates a symbolic value when evaluating expressions including parameter symbols. At that time, it is done with depending on their types, e.g., an integer, a pointer to struct or a pointer to array. Without the type, it is hard to generate a correct symbolic value that will be instantiated later in call sites. Thus, evaluating RHS of the store statement, the type of RHS is better to be given.
Reviewed By: dulmarod
Differential Revision: D17185346
fbshipit-source-id: f0945c40f
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:
In integrations where the capturing process isn't forked off the main Infer process, but launched, eg, via a script pretending to be a compiler, the reference indicating whether the server is running will always be false, and thus such integrations will never try to connect to the write daemon.
Fix this by
- making `sqlite-write-daemon` authoritative wrt connecting to the daemon.
- launching the daemon earlier in the setup process.
Reviewed By: jberdine
Differential Revision: D17204002
fbshipit-source-id: 23d452fac
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:
It adds `typ` field in Sil.Load. The field will be used by the analyzer in the following diffs.
Motivation: Interbo generates a symbolic value when evaluating expressions including parameter symbols. At that time, it is done with depending on their types, e.g., an integer, a pointer to struct or a pointer to array. Without the type, it is hard to generate a correct symbolic value that will be instantiated later in call sites. Thus, evaluating RHS of the load statement, the type of RHS is better to be given.
Reviewed By: jvillard
Differential Revision: D17163350
fbshipit-source-id: f7f0f1429
Summary:
It uses inline record for Sil.Load and Sil.Store for preparing the
following extention.
Reviewed By: dulmarod
Differential Revision: D17161288
fbshipit-source-id: 637ea7bfa
Summary: It prints non-verbose program variables in the report.
Reviewed By: ngorogiannis
Differential Revision: D17163943
fbshipit-source-id: c3f3c2887
Summary:
An exception thrown during capture/analysis may leave the daemon
running. Kill it even when one is thrown.
Reviewed By: martintrojer
Differential Revision: D17181090
fbshipit-source-id: a7b002f23
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:
We currently use storage_class only for checking is_static, adding the flag instead in the plugin to improve perf by avoiding string comparisons.
update-submodule: facebook-clang-plugins
Reviewed By: ngorogiannis
Differential Revision: D17156173
fbshipit-source-id: 2b84a0b84
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:
This abstraction was not always used consistently.
Its usage made more sense when it supported both present annotations and
optional annotation (which got removed in previous diff).
The rought semantic of that was "what is the inferred type for such and
such value (variable or expression) in typestate". So it is not really
_annotation_ in first place, it is more like "what we inferred about
nullability given annotations, known special cases, and current sybmolic
execition state".
Let's explicitly rename `map` to `is_nullable`. If/when we need to
enhance this further (and we likely will), we will do it accordingly.
Reviewed By: jvillard
Differential Revision: D17153434
fbshipit-source-id: 3c85b56df
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
Summary:
Implementation of write-serializer for Sqlite. Points of note:
- A Unix socket is used for communication. This avoids buffer-size limitations, as the objects we send for writing may exceed said limits.
- No daemon is used if running under buck or in genrule mode, as this usually means a single-threaded job capturing into the DB.
- When the daemon is running, read-only access is *not* enforced for other processes. This makes starting and stopping the daemon during Infer execution easier and more robust. In WAL mode this should not have any effect on performance.
- This version is not economical with connections, it uses one per query, todo.
Reviewed By: jvillard
Differential Revision: D17077183
fbshipit-source-id: fa9877d6c
Summary: Developing the Sqlite-writer process further, a type `command` is introduced, which will used for sending instructions down a communications channel to the daemon. For now, the commands are interpreted locally.
Reviewed By: skcho
Differential Revision: D16985056
fbshipit-source-id: 2aa20908d
Summary:
Write contention is becoming a problem in parallel capture (eg when make runs with high parallelism) or when analysis writes CFGs to the DB in parallel (eg when analysing blocks in ObC). This is believed to lead to BUSY errors in Sqlite.
This is step 1 of a process where all writes are cordoned-off in one module, and fixing the interface for that module.
Reviewed By: skcho
Differential Revision: D16985034
fbshipit-source-id: 3d7ce381b
Summary:
When running with high parallelism and a large number of insertions in the DB (eg, ObjC analysis with block specialisation), we see MISUSE exceptions thrown by Sqlite **when trying to bind parameters to queries**. It does not always occur, and maybe that's because the check in Sqlite that throws this error is documented as "probabilistic". For the same reason, it is plausible that high parallelism increases the chance of detection.
According to documentation this unequivocally means a bug in our usage of the API (https://www.sqlite.org/rescode.html#misuse), in particular that a parameter is re-bound while the query is running (https://www2.sqlite.org/cvstrac/wiki?p=LibraryRoutineCalledOutOfSequence). I believe this may have to do with `result_fold_rows` (as it's the only one that uses a query that can be continued, and thus misused), but I have not managed to track the bug.
Always resetting the query before using it is a defensive measure that seems to make these errors go away (and turn some of them to BUSY timeouts, which should be addressed by a write serialiser, but in any case it's a more logical state of affairs = higher parallelism means more contention thus possibly timeouts due to lock usage).
Reviewed By: jvillard
Differential Revision: D17147447
fbshipit-source-id: 7ef3cc73f
Summary:
Since it does not make sense to get ranges of non-integer values and
use them as approximate iteration numbers, this diff ignores control
values that only contain non-integer symbols.
Reviewed By: ezgicicek
Differential Revision: D17130967
fbshipit-source-id: f5ba58d52
Summary: This tests the previous commit D17093980, which moves incremental analysis to run before capture
Reviewed By: ngorogiannis
Differential Revision: D17113475
fbshipit-source-id: 702d967b3
Summary:
Currently, the specs directory is cleaned after running capture. This means that the `changed-files` are interpreted in the context of the second set of source files. Therefore if a procedure is deleted from the second set of source files, its specs file will not be deleted.
This moves the cleaning of the specs directory to before capture, to avoid this problem.
Reviewed By: ngorogiannis
Differential Revision: D17093980
fbshipit-source-id: e1a8d8a54
Summary: This diff extends size alias domain for keeping one more alias of a Java temporary variable.
Reviewed By: ezgicicek
Differential Revision: D16984082
fbshipit-source-id: 244bbd0ee
Summary: This diff ignores boundends when getting the value range.
Reviewed By: ezgicicek
Differential Revision: D17114363
fbshipit-source-id: cca8745e3
Summary: Like we removed empty edges from the `pre_heap` in D16419183, let's do the same to `post_heap`.
Reviewed By: skcho
Differential Revision: D17111336
fbshipit-source-id: c35fcbabb
Summary:
Before this diff we would record when some values came from the "address
of" logical variables. This makes no sense and also was incorrectly
marking these addresses as "written to" when they appeared in the post
of a procedure, because their attributes weren't empty (they had the
"address of stack variable" attribute).
Reviewed By: ngorogiannis
Differential Revision: D17131210
fbshipit-source-id: 6cc3c465a
Summary: When a positive bound is expected, min(1,x) can be simplified to 1.
Reviewed By: ezgicicek
Differential Revision: D17091884
fbshipit-source-id: 3a89a44fa
Summary:
This did not work. One can not create a param that depends on another param (dynamic!) value
```
infer --dynamic_dispatch
/Users/mityal/infer/infer/bin/infer: unknown option '--dynamic_dispatch'.
```
No info in the manual:
```
find . -name "*.txt" | xargs grep "dynamic"
```
Reviewed By: jvillard
Differential Revision: D17113568
fbshipit-source-id: 87d0a18ba
Summary:
I found it very confusing that running infer with --debug makes the
report to be different.
Intuitively, I expect (and I think majority of users would expect) that
`--debug` makes things more verbose (and potentially more slow / consuming
more memory and disk space), but does not change anything apart from it.
One pro of preserving existing behavior, pointed by jvillard:
- Suppose some check is experimental or disabled in the config. The
users expect the issue to be found, but it does not show up. They run
`infer --debug` to understand the behavior, and suddenly the issue shows
up.
I, hovewer, find this pro not important enough and potentially confusing
the users even more.
(If they want to investigate seriously, they can always use
--no-filtering, and there are a lot of cases when the issue does not
show up for others, much hard to undertand reasons, than the fact that
it is disabled).
Reviewed By: jvillard
Differential Revision: D17113750
fbshipit-source-id: 46cc93503
Summary:
The purpose of DefinitelyNotNullable currently is bit unclear; let's
rename it so that the intention is obvious.
Reviewed By: artempyanykh
Differential Revision: D16984529
fbshipit-source-id: 696d58315
Summary:
`nullsafe` currently allows the following:
```
public void Nonnull Object willBeOK() { return null; }
```
But disallows the following:
```
public void Object willBeAnIssue() { return null; }
```
This was a deliberate choice made back in 2014.
The motivation was to provide a way to tell the checker "I know it can not be null, trust me".
A huge problem with that approach is that it is extremely non-intuitive and surprising, and contradicts with pretty much everything when Nonnull or similar annotations are used in external world.
This is not the way how checkers should be supressed.
We do provide 2 options to express this intention, namely `assertNotNull` and `assumeNotNull` would do the thing.
This is a much better approach for additional reason: assertNotNull is
granular and applies only to the exact expression that is under
question. In contrast, suppressing the check on the whole function level
make any modifications of a function dangerous.
Reviewed By: artempyanykh
Differential Revision: D16984213
fbshipit-source-id: 0ba0f623b
Summary:
This diff revises some models of Java String.
They had been implemented by C's string models such as models of
`strlen` or `strcat`, however, Java's String is different to C's,
rather is similar to C++'s String object.
Reviewed By: ezgicicek
Differential Revision: D17093136
fbshipit-source-id: b4f2cb4d0
Summary: Numeric attribute ranks are getting confused with addresses. Add an option (false by default) to MakePPUniqRankSet which prevents printing of the ranks.
Reviewed By: jvillard
Differential Revision: D17094269
fbshipit-source-id: 353c52fca
Summary:
`from_string` is too benign in constrast with what this method is really
doing (and oh my what it is really doing).
There are a lot of potential follow ups to clean this up even more, but
this is beyond the scope of this diff
Reviewed By: jvillard
Differential Revision: D17070826
fbshipit-source-id: 3d190039e
Summary:
`__inferbo_empty`, `__inferbo_min`, and `__inferbo_set_size` were in the
"include-based" cpp model.
Reviewed By: jvillard
Differential Revision: D17072034
fbshipit-source-id: dd840331f
Summary:
This diff uses the models of vector for modelling string in Cpp.
Depends on D16963153
Reviewed By: ezgicicek
Differential Revision: D16963166
fbshipit-source-id: 5effe2d72
Summary:
This is more powerful than `"symbols"` for more advanced use-cases. Keep
`"symbols"` unchanged to make migrating easier.
Differential Revision: D16985756
fbshipit-source-id: dfbb09393
Summary: Adding new predicate for checking whether a variable is defined as extern. May be useful in AL rules.
Reviewed By: jvillard
Differential Revision: D16961690
fbshipit-source-id: 0677077dc
Summary:
The clang frontend has bugs. When a bug we know about happens some
exception is raised and, most of the time, logged away so as not to
crash the whole process. This catching of exceptions wasn't done from
testDeterminator so it could crash where capture didn't. This diff wraps
the crashy function in test determinator to avoid that.
Reviewed By: ngorogiannis
Differential Revision: D16963178
fbshipit-source-id: 87a4ff70b
Summary:
This isn't really a "config" part of the frontend and this change is
needed later to catch these errors more robustly.
Reviewed By: ngorogiannis
Differential Revision: D16963177
fbshipit-source-id: 293b23acf
Summary: This diff prunes array sizes in Java by adding the size alias on the `get_array_length` function calls.
Reviewed By: ezgicicek
Differential Revision: D16983501
fbshipit-source-id: a924af09d
Summary:
Rename some AL source files so they mention AL explicitly instead of
"cFrontend" which could be confused with the clang frontend itself.
Reviewed By: ezgicicek
Differential Revision: D16962539
fbshipit-source-id: 29237cd1c
Summary: AL makes for close to a third of the source files in clang/. Put the code in its own folder for clarity.
Reviewed By: ezgicicek
Differential Revision: D16962438
fbshipit-source-id: 3373e69b9
Summary:
This diff avoids that an integer value is pruned to the bottom by
comparing to a pointer.
For example, before this diff,
assume((int*)x == p);
assume((int*)x != p);
where x is an integer, x is pruned to the bottom in both of the assume
cases. So, there were some, unintentional and false, unreachable
code.
Depends on D16960199
Reviewed By: ezgicicek
Differential Revision: D16964735
fbshipit-source-id: 90a3c8c80
Summary:
It changes the order of StdBasicString and StdVector for easier
reviewing of the following diff.
Reviewed By: ezgicicek
Differential Revision: D16963153
fbshipit-source-id: 50325e4e1
Summary:
The access path format forced some weird patterns on this code, simplify
using the access expression structure.
Reviewed By: ezgicicek
Differential Revision: D16960660
fbshipit-source-id: e8faf619e
Summary:
It prunes the size of collections when the size function is called in the condition expression. The diff extended the alias domain to understand temporary variables of SIL from Java.
Depends on D16761461
Reviewed By: ezgicicek
Differential Revision: D16761611
fbshipit-source-id: 849c5c71c
Summary:
This adds logging of the number of nodes in the reverse analysis call graph, and the number of these nodes that are invalidated by incremental analysis.
This data will show the precision of incremental analysis.
Reviewed By: ngorogiannis
Differential Revision: D16939101
fbshipit-source-id: 1e465f1a6
Summary:
It revises Java's cast model to keep type in the location when it has a field.
The type information is useful especially when generating ondemand values of Collection elements.
Depends on D16807299
Reviewed By: ezgicicek
Differential Revision: D16807378
fbshipit-source-id: 636e54429
Summary:
It doesn't make sense to use incremental analysis without specifying changed files. This is a possible source of future bugs.
This commit causes infer to die if incremental analysis is used without changed files.
---
Previously:
I think this code is currently a bit brittle because the CI shadow builds sometimes use `--incremental-analysis` because they are called with the same command as the diff analysis.
I am worried that in the future the shadow builds could be broken by this, although everything looks like it works right now. This diff would prevent breaking smoke builds in future because the shadow builds don't set changed-files (afaik).
However, possibly this is not the right place to fix the problem. It might be better to change the CI, I'm not sure.
Reviewed By: mityal
Differential Revision: D16829192
fbshipit-source-id: 5ee1ce9d0
Summary:
Use whatever information we can to decide whether to use C or Java
syntax when outputting an access expression, now that we store them as
such.
Also, make cluster callbacks explicitly set the language, as this was not done before and led to some confusion (Clang being set when analysing a Java file).
Reviewed By: skcho
Differential Revision: D16884160
fbshipit-source-id: 40adf9f35
Summary:
Access paths are too coarse to properly address C/C++ instructions, and lead to false positives and negatives. Begin the process of porting the underlying domains to access expressions, in a results-preserving way. This roughly consists in:
- Adding missing functions in `AccessExpression` to mirror those in `AccessPath`.
- Replacing `AccessExpression` for `AccessPath` and removing conversions from the former to the latter except in:
- Printing functions, to ensure formatting issues won't change tests/CI.
- Reporting/deduplication still happens through access path conversion, as we need an analogue of `ModuloThis` for `AccessExpression`.
- In selected places, ignore any access type not present in `AccessPath` (ie. dereference/take address of).
Reviewed By: jberdine
Differential Revision: D16856721
fbshipit-source-id: 5e3a88b75
Summary: Ideally, we should be able to handle them like pruning if statements but for now, let's add the test.
Reviewed By: skcho
Differential Revision: D16938842
fbshipit-source-id: 04fae9559
Summary:
It uses inline record for Loc.Field
Depends on D16807279
Reviewed By: ezgicicek
Differential Revision: D16807299
fbshipit-source-id: 45eab34a4
Summary: Checker configs were defined as tuples which are amenable to problems with wrong ordering. Let's make convert them to a record type to prevent such issues.
Reviewed By: jvillard
Differential Revision: D16936737
fbshipit-source-id: 32aad6e97
Summary: Javalib is not happy about some class signature, let's try to silence it temporarily.
Reviewed By: ngorogiannis
Differential Revision: D16917273
fbshipit-source-id: 39ce4adee
Summary:
Change the logic of the annotation reachability checker in the following
ways:
1. Sanitizers take priority over sinks, i.e. a procedure that is both a
sink and a sanitizer is not a sink. This changes the existing tests
that seemed to assume the opposite. However I think that way is more
useful and goes better with the fact that sanitizers are specified as
"overrides".
2. When applying a summary, check again that we are not in a sanitizer
for the corresponding sink.
Without (2) this there was a subtle bug when several rules were
specified. For example, if `sink_wrapper()` wraps `sink()` for a rule
`R` then the summary of `sink_wrapper()` will be: `R-sink : call to sink()`.
Then, suppose `sanitizer()` calls `sink_wrapper()` and `sanitizer()` is
a sanitizer for `R` but not for another rule `R'`. The previous code
would add the call to `sink()` to the summary of `sanitizer()` because
it's not a sanitizer for `R'`, even though `sink()` is not a sink for
`R'`!
The current code will re-apply the rules correctly so that sinks are
matched only against the right sanitizers.
Reviewed By: skcho
Differential Revision: D16895577
fbshipit-source-id: 266cc4940
Summary:
- run the tests! they weren't hooked up to the main Makefile :/
- add some html debug messages
- formatting
Reviewed By: skcho
Differential Revision: D16895578
fbshipit-source-id: e96d737cc
Summary:
I added this logging in D16730426, to try and debug incremental analysis.
I don't need the logging anymore, so I'm taking it out. I don't this it's very useful for users.
Reviewed By: ezgicicek
Differential Revision: D16904498
fbshipit-source-id: 88b0f1cb5
Summary:
Since it is non-sense to get ranges of boolean values, this diff
ignores control values that only contain boolean symbols.
Depends on D16804802
Reviewed By: ezgicicek
Differential Revision: D16804808
fbshipit-source-id: ccb25db4d
Summary: The pattern "check if an access has already been reported, otherwise see if it is a violation, report it, then add it to the set of reported accesses" is too much copy pasta. Push that into the reporting functions.
Reviewed By: ezgicicek
Differential Revision: D16859208
fbshipit-source-id: 5370efd41
Summary: I'm not entirely sure why this function was written in such a horrendous way :)
Reviewed By: skcho
Differential Revision: D16858396
fbshipit-source-id: d998e17f3
Summary: Functions with empty body have unit cost, not zero. The unit cost comes from the start node.
Reviewed By: skcho
Differential Revision: D16855642
fbshipit-source-id: 6b5181faf
Summary:
Before this diff it returned `[0,size-1]`, but which became bottom
when size was given by 0. As a result, it made the both branches of
`if(iterator.hasNext())` unreachable. Similarly, if the size was 1,
it only visited the false branch of the if condition because the
condition value was `[0,0]` at that time.
This diff changes it to return `[0,size]`, so that
* the false branch is reachable when the size is 0
* the both branches are reachable when the size is 1
Reviewed By: ezgicicek
Differential Revision: D16803000
fbshipit-source-id: f8772be27
Summary: We want to keep big O notation as simple as possible in cost analysis reports (especially in diff time). Therefore, let's not show constants/min/max in big O notations even though the resulting asymptotic bound might be inaccurate. Developers can click on the trace and see the actual cost.
Reviewed By: skcho
Differential Revision: D16731351
fbshipit-source-id: 2e16f7eca
Summary: In order to test changes to bigO notation, let's record them in test results.
Reviewed By: skcho
Differential Revision: D16763972
fbshipit-source-id: c1376909b
Summary:
It renames a function to make it clear what it does.
Depends on D16761451
Reviewed By: ezgicicek
Differential Revision: D16761461
fbshipit-source-id: b989cc274
Summary: We do not need to keep the elements type of vector in the field.
Reviewed By: ezgicicek
Differential Revision: D16761451
fbshipit-source-id: 6d5384662
Summary: Add a sanity check that looks up the `INFERVERSION` environment variable and, if set, checks that the current binary matches that version.
Reviewed By: skcho
Differential Revision: D16761575
fbshipit-source-id: 9d5c32220
Summary:
Incremental analysis isn't behaving as expected in production, and I think the deletion and re-creation of the results directory is why
Adding logging to test this theory
Reviewed By: ngorogiannis
Differential Revision: D16730426
fbshipit-source-id: 0a670cabf
Summary:
Correct the models of ArrayList initialization. Basically, there are two ways to initialize:
- by setting an initial capacity, which creates an empty list
- by passing another collection as an argument
Before, we had only modeled the second case which was resulting in wrong memory model for the first case. This diff fixes that.
Reviewed By: skcho
Differential Revision: D16711055
fbshipit-source-id: e82faf191
Summary: Remove duplicate `s` when printing the time taken by the analysis
Reviewed By: ngorogiannis
Differential Revision: D16710277
fbshipit-source-id: 3ba7f6693
Summary:
It adds a vector model of `data` method.
Depends on D16687280
Reviewed By: ezgicicek
Differential Revision: D16689400
fbshipit-source-id: 156016b3c
Summary:
It adds a model of vector::push_back
Depends on D16687225
Reviewed By: ezgicicek
Differential Revision: D16687269
fbshipit-source-id: 9d2a73fca
Summary:
It enables pruning of vector's size when the return value of the function call of `vector::size` is pruned.
Depends on D16687167
Reviewed By: ezgicicek
Differential Revision: D16687225
fbshipit-source-id: 793a21b3a
Summary:
Add logging for the number of procedures whose summaries are invalidated by incremental analysis
This will help verify that incremental analysis is working as expected in production
Reviewed By: ngorogiannis
Differential Revision: D16686911
fbshipit-source-id: 53c89c3bb
Summary:
It generates vector value ondemand when it is given as a parameter.
Depends on D16645589
Reviewed By: ezgicicek
Differential Revision: D16645624
fbshipit-source-id: 7498c8ab2
Summary:
This diff makes it sure that Inferbo does nothing on relational domain
at function calls when the command line option for them is not given.
Reviewed By: ezgicicek
Differential Revision: D16647903
fbshipit-source-id: 74ef251fe
Summary: Test that cost analysis works with incremental analysis enabled
Reviewed By: ezgicicek
Differential Revision: D16620101
fbshipit-source-id: b41403954
Summary:
The models are only for biabduction so try to make that clearer in the
code and documentation.
Reviewed By: skcho
Differential Revision: D16603147
fbshipit-source-id: 4a2be53de
Summary:
It's not being worked on and is not in a state where it works.
It would probably better to write this as a script of some kind or else
resurrect this subcommand in a form where it behaves more like a script,
ie fork/execs infer analyses instead of having them be function calls
(but then it might as well *be* a script as it would likely be more
flexible).
In any case...
youarealreadydead
Reviewed By: ezgicicek
Differential Revision: D16602417
fbshipit-source-id: d0d129539
Summary:
These have proved to be too fragile to maintain as they would often break
compilation of user code. They have been off by default for more than a year
now (D7350715).
Removing the include models shows a more accurate picture of what infer results
look like in production. As such, lots of tests have changed, mostly
biabduction but also in inferbo. SIOF was using include-based models too but
now libc++ is better and iostreams are implemented in a way that SIOF
understands (instead of being magical creatures) so nothing changed there.
Reviewed By: skcho
Differential Revision: D16602171
fbshipit-source-id: ce38f045b
Summary:
Write a test for the invalidation of changed procedures
Reverse analysis graph for this test: https://fburl.com/graphviz/ybidpidq
The procedures marked as changed are `a` and `d`, and this causes `a,b,c,d,e,main` to be invalidated as expected
Reviewed By: jvillard
Differential Revision: D16579526
fbshipit-source-id: cbec304ce
Summary:
Add test `incremental_analysis_remove_file` to the toplevel makefile so that it is called by `make test` etc
Also swapped the src_before and src_after files so the test checks file removal instead of addition.
Reviewed By: jvillard
Differential Revision: D16562340
fbshipit-source-id: 79bab5f66
Summary: Models of Java's Collection mistakenly assumed that there was an argument for empty set whereas `Collections.emptySet()` doesn't have any actuals. This diff fixes that an also removes the type argument from the corresponding model definition.
Reviewed By: skcho
Differential Revision: D16582314
fbshipit-source-id: d4304dc60
Summary: Sometimes programmers use integer underflow to get a maximum number of that type. This diff assumes that integer underflows from the syntactical form `(unsigned 0) - constant` is intended by the programmer, and suppresses the alarms of which.
Reviewed By: ezgicicek
Differential Revision: D16560639
fbshipit-source-id: 206f30dbc
Summary:
Count the following:
- how many procedures were *actually* analyzed (i.e. some checkers ran
on them)
- how many times an analysis result was retrieved from the local cache
and how many times it was missed
Reviewed By: skcho
Differential Revision: D16561867
fbshipit-source-id: 8c43ce13c
Summary:
Instead of `let incr_foo () = global_stats.foo <- global_stats.foo + 1` where you have to
check that you copy/pasted the right stuff and substituted `foo`
everywhere, write `let incr_foo () = incr Fiels.summary_foo` where
there's less room for errors.
Reviewed By: artempyanykh
Differential Revision: D16561868
fbshipit-source-id: 77ea09bef
Summary:
Before this diff, it gave up pruning of linear bound by minmax bound.
For example, `overapprox_min (x+c1, c2+min(d1,y))` was `x+c1`.
However, we can get a bit more preciser value as follows.
```
overapprox_min (x+c1, c2+min(d1,y))
<= min (x+c1, c2+d1)
= c1+min(c2+d1-c1, x)
```
Reviewed By: ezgicicek
Differential Revision: D16543837
fbshipit-source-id: 8fdbce097
Summary:
- make most behaviours independent of the java version so that either works fine without user intervention
- modify regexp used to parse `javac` output to work for all versions
- no need to be sure we are in Java 11 to match java 11-only method name in quandary
- for the rest, provide a command-line flag to specify the java version manually in case it differs from the version that infer was built against
- this only affects the Maven integration for now
To do all that, also change the configure script to record the version of java instead of just a boolean for whether it's >= 10.
Reviewed By: ezgicicek
Differential Revision: D16493988
fbshipit-source-id: 622e91b25
Summary:
The default values of config options can sometimes depend on build-time
configuration values. This makes checking that the manuals "remain the same"
trickier as the manuals can be different depending on the platform. This
removes *all* default values from the checked-in manuals. We could be more
fine-grained and scrub only the values that are susceptible to change but for
now this is probably good enough.
This is done by implementing new options `--help-scrubbed` and
`--help-scrubbed-full` and using these in our tests instead of `--help` and
`--help-full` (which remain unaffected).
Also don't wrap the default values in `$(i,...)` anymore because the defaults
can trigger line breaks and then the man page is ill-formatted because that
format is stupid.
Reviewed By: mityal
Differential Revision: D16543779
fbshipit-source-id: bc929ff8c
Summary:
This diff prevents that the latest prune value is overwritten as top
from callees.
Reviewed By: jvillard
Differential Revision: D16540391
fbshipit-source-id: bdd5b42ed
Summary:
This diff improves the precision of the mod operator.
For example, result of x % c (when x>=0 and c>0) is
(before) [0, c-1]
(after) [0, min(c-1,x)]
Reviewed By: ezgicicek
Differential Revision: D16518578
fbshipit-source-id: a68660ee7
Summary: This diff tries to do weak update for the abstract locations by pointer arithmetic, e.g. `p[n]` or `p+n`, even if the type of `p` is declared as a simple pointer, not an array.
Reviewed By: ezgicicek
Differential Revision: D16458367
fbshipit-source-id: 3b4cdd7e4
Summary:
A test that records the expected output of:
- reverse analysis call graph
- introduced/pre-existing/fixed issues
- cost analysis results
Currently only the call graph is non-empty.
Reviewed By: PhoebeMay
Differential Revision: D16495470
fbshipit-source-id: f186d73d2
Summary:
The `represents_multiple_values` flag was adopted to decide whether updating abstract value strongly or weakly. However, the flag was included in the `Val` domain, which is strange, because it is a property of abstract locations, rather than abstract values. This makes the behavior of memory update function depend on the abstract value to update, making its code complicated.
This diff detach the `represents_multiple_values` flag from the `Value` domain, thus the memory update does not depend on the abstract value. Since this is a refactoring, I believe the diff should not make many semantic changes.
Reviewed By: ezgicicek
Differential Revision: D16441734
fbshipit-source-id: 4c10779d7
Nikos Gorogiannis
Ezgi Çiçek
Sungkeun Cho
Jules Villard
Dulma Churchill
Martin Trojer
Mitya Lyubarskiy
Josh Berdine
Artem Pianykh
David Pichardie
Taras Tsugrii
Fabio Milano
Phoebe Nichols