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
Nikos Gorogiannis
Mitya Lyubarskiy
Dulma Churchill
Josh Berdine
Sungkeun Cho
Artem Pianykh
Jules Villard
Ezgi Çiçek