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