Summary:
Emit the crucial parts of Pulse summaries as json to enable
post-processing by external tools. Stop somewhat arbitrarily at some
datatypes that are just emitted as "opaque" values.
For example:
```
$ infer debug --procedures --procedures-summary-json --select 0
[[["pulse",[["ContinueProgram",{"post":{"heap":[["v3",[[["Dereference"],["v4","_"]]]],["v7",[[["Dereference"],["v3","_"]]]]],"stack":[[["ProgramVar",{"plain":"return","mangled":null}],["v7","_"]]],"attrs":"_"},"pre":{"heap":[],"stack":[],"attrs":"_"},"skipped_calls":"_","path_condition":"_"}],["ContinueProgram",{"post":{"heap":[["v3",[[["Dereference"],["v4","_"]]]],["v8",[[["Dereference"],["v3","_"]]]]],"stack":[[["ProgramVar",{"plain":"return","mangled":null}],["v8","_"]]],"attrs":"_"},"pre":{"heap":[],"stack":[],"attrs":"_"},"skipped_calls":"_","path_condition":"_"}]]]]]
```
Reviewed By: ezgicicek
Differential Revision: D24503387
fbshipit-source-id: 9bd08e93b
Summary:
Output summaries in json format, so that other tools can exploit the
results of infer without having to be written inside infer itself.
For now the json for a summary is just one line saying "opaque" :)
Set up the infra to generate (yo)json automatically using
ppx_yojson_conv. See it in action in the next diff.
Reviewed By: ezgicicek
Differential Revision: D24503343
fbshipit-source-id: e24a2fff3
Summary:
- output the "menu" of the interactive mode on stderr instead of stdout
so that we can pipe the results, eg
`infer debug --procedures --procedures-summary | cat`
This will be more useful when we add an option to output json, as
otherwise the menu pollutes the json.
- Allow "--select" to work for infer-debug too:
`infer debug --procedures --procedures-summary --select 0`
Reviewed By: da319
Differential Revision: D24503301
fbshipit-source-id: d7fb4b713
Summary:
This diff revises `nextObject` model to handle multiple symbolic enumerators. Instead joining the
symbolic offsets of them, which sometimes introduces top, it sums the offsets. This is a sound &
conservative semantics since they are all non-negative integers.
Reviewed By: ezgicicek
Differential Revision: D24474513
fbshipit-source-id: 6707aa907
Summary:
This diff revises memory model of enumerator in ObjC to enable passing it as a parameter.
The cost checker was not able to analyze a function precisely when it gets an enumerator as a
parameter because the offset of an enumerator was available only when the analyzer knew the correct
relation between the enumerator and an array.
This diff simplifies the enumerator to have a similar value with `array->elements`, so its offset can
be taken without the relation between enumerator and array to get them.
Reviewed By: ezgicicek
Differential Revision: D24446574
fbshipit-source-id: 27cdc051e
Summary:
This diff adds an option hiding function pointers in costs to users: `cost-suppress-func-ptr` is
true by default.
Reviewed By: ezgicicek
Differential Revision: D24448212
fbshipit-source-id: 88f6b5ea1
Summary:
Before this diff we would just propagate the callee abstract state,
which doesn't make sense in the caller. We could just remove the state
from AbortProgram altogether as Pulse itself doesn't use it, but for now
let's at least make sure it's accurate.
Also needed for upcoming hackathon that will start from Pulse error
specs to try to produce tests :)
Reviewed By: ezgicicek
Differential Revision: D24448073
fbshipit-source-id: 9100b3f79
Summary:
Detect when changed files paths are trying to escape the project root
and try to guess their relative project root (which has to be a parent
of the current one).
This is perhaps a bit too hacky but it works for the case we need it to.
Reviewed By: martintrojer
Differential Revision: D24425427
fbshipit-source-id: 018651740
Summary:
Sometimes you need several project roots (eww), this makes paths make
sense even in that case.
Reviewed By: martintrojer
Differential Revision: D24336244
fbshipit-source-id: f087d533a
Summary:
Don't wait until pre-analysis has completed before updating the task
bar with the current procedure being analysed.
Reviewed By: skcho
Differential Revision: D24418609
fbshipit-source-id: afedaf687
Summary:
Move from Map to SafeInvertedMap:
- joining two branches where only one branch had the variable set to a
given closure or type should *not* keep that information around: now
we correctly get Top instead
- the "Safe" part is an optimisation that doesn't store Top values in
the map, which is important as most values are not closures so we
don't care about storing the fact that we don't know anything about
them
Reviewed By: ngorogiannis
Differential Revision: D24418560
fbshipit-source-id: 0ac701502
Summary:
This diff adds a model for NSFileManager.contentsOfDirectoryAtURL as returning a constant-length
collection.
The analyzer cannot know files in a directory. We have some options to handle such unknown data.
1. Use `Unknown` value, ie `top`
2. Use a symbolic value
3. Use a constant value
We had been used the first option. An upside of this is that the analyzer can remain as sound.
However, a downside of this is the top value can be propagated to other procedures, making their
costs top, thus we may miss some cost changes of them.
The second option is to introduce a symbolic value, ie. that for the number of files. A problem is
that the symbolic value will never be concretized. As a result, the symbol can be propagated to
other procedures, increasing the coefficient of the complexity or making top costs. Note that handling multiple
symbols is somewhat limited in Inferbo's interval domain.
The last option is to introduce a constant value. I think this is the best approach we can take among above.
Even though we may have FNs when there are a lot of files in a directory, we cannot reason or expect about
that at the analysis time anyway.
Reviewed By: ezgicicek
Differential Revision: D24418099
fbshipit-source-id: bf8cf3538
Summary: This diff adds closure symbols to operation/allocation costs, when function pointer is called.
Reviewed By: ezgicicek
Differential Revision: D24308550
fbshipit-source-id: 6c5889d41
Summary:
This diff extended the polynomial domain to include symbols for closure calls.
When the closure symbol is added to the polynomial? Unknown closure is called inside a function
like,
```
foo() {
self->closure_field();
}
```
Thus, the cost of `foo` becomes `|self->flosure_field|`, rather than unknown. (Note that this
semantics is added only for autoreleasepool size at the moment.)
When the symbol is instantiated? `foo` is called with correct closure contexts.
```
goo() {
self->closure_field = ^(){ ... };
foo();
}
```
The summary of `goo` will have instantiated summary of the closure.
Reviewed By: ezgicicek
Differential Revision: D23992590
fbshipit-source-id: d1d228403
Summary:
Another step in the refactoring of the starvation domain:
- Main purpose is to mediate access to the set of critical pairs in a summary through a fold function (`fold_critical_pairs_of_summary`) and not through direct field access to that set. This will allow eliding storage of critical pairs entirely and dynamically generating those when folding.
- Remove optional arguments as much as possible, as this led to unused arguments not being caught.
- Helper functions distributed more logically among modules.
Reviewed By: skcho
Differential Revision: D24275399
fbshipit-source-id: d23123a48
Summary: As part of a refactor, push `thread` from the enclosing type (`CriticalPairElement`) into `Event.t`.
Reviewed By: jvillard
Differential Revision: D24161709
fbshipit-source-id: bd812f3fd
Summary:
In ObjC, `NSObject.copy` returns the object returned by `copyWithZone:` on the given class. This method must be implemented if the class complies with `NSCopying` protocol. Since we don't have access to `NSObject`'s code, to follow calls into `copyWithZone:`, we replace such `copy` calls with calls to `copyWithZone:` when a) such a method exists in the class and b) the class conforms to `NSCopying` protocol.
This is done in the preanalysis because
- we need to know if there is a `copyWithZone:` method in the class.
- so that other analyses also benefit (as opposed to doing this in cost and inferbo models).
Note that `NSObject` doesn't itself conform to `NSCopying` but all its subclasses must confrom to the protocol and support the same behavior as above.
https://developer.apple.com/documentation/objectivec/nsobject/1418807-copy
Similarly for `mutableCopy` -> `mutableCopyWithZone:` for classes implementing `NSMutableCopying` protocol.
Reviewed By: skcho
Differential Revision: D24218102
fbshipit-source-id: 42900760e
Summary:
`NonBlocking` methods have starvation errors silenced (but not deadlock ones). This is implemented by summarising as usual and then filtering out such events when the summary is finalised, if the method is annotated as such.
It's better to not record the events in the first place.
Reviewed By: ezgicicek
Differential Revision: D24237465
fbshipit-source-id: 1b24a26f0
Summary: This will be needed in the next diff so that we can find all classes that conform to `NSCopying` protocol.
Reviewed By: skcho
Differential Revision: D24216549
fbshipit-source-id: 297b527a6
Summary:
- rename the checker "Uninitialized Variable" to "Uninitialized Value"
as this is the name of the issue type
- delete timestamp XML comment from the man pages to avoid future git
churn when updating the website
- counting is hard
Reviewed By: martintrojer
Differential Revision: D24219165
fbshipit-source-id: cf3057373
Summary:
I wanted to change the default to "callgraph" but that created issues in
our tests, introducing flaky behaviours and even a failure due to trying
to run the pre-analysis multiple times (not 100% sure it was related).
Instead, document the various options and put the option in the analysis
manual so users can choose.
Reviewed By: martintrojer
Differential Revision: D24193751
fbshipit-source-id: 4b7c33a79
Summary: Model it similar to `NSArray.initWithArray` as copying from the given dictionary elements. Removes a FP as expected.
Reviewed By: ngorogiannis
Differential Revision: D24136868
fbshipit-source-id: ed31c3c8f
Summary:
This diff is a preparation to extend the polynomial domain. What I will do in the following diff is
to extend the polynomial domain to include a symbol representing "cost of function pointer call".
Then, the symbol will be instantiated to another polynomial cost at call sites.
The polynomial domain is defined as a sum of
* non negative insteger
* map from `bound` to polynomail domain
```
type poly = {const: NonNegativeInt.t; terms: poly M.t}
```
The problem is all `bound`s are adderessed as integer values, rather than polynomial, thus it
does not fit to include the symbol for the "cost of function pointer call".
In this diff, it introduces a `Key` module for the map `M`, the type of `Key.t` is the same to the previous key of `M`. The actual extension of the key type will be in the following diff.
Reviewed By: ezgicicek
Differential Revision: D23991401
fbshipit-source-id: cec64347f
Summary: Subsequent diff will push information down into `Event.t` so as preparation, turn all variant values into records.
Reviewed By: jvillard
Differential Revision: D24115201
fbshipit-source-id: d2126dd49
Summary:
`std::lock(x,y,z)` simultaneously acquires locks `x,y,z` in a deadlock free manner (essentially an unspecified fixed order).
Starvation currently deals with it by exploiting properties of the state domain. It's a map from locks to number of times the lock is held, so the count of many locks can be increased at the same time without recording any particular lock order.
In upcoming diffs the domain will be refactored into a tree of nested lock acquisitions (for other reasons) and that domain necessarily records lock order. The obvious way of doing this correctly is to allow `std::lock` as an atomic even (ie, without trying to break it into multiple acquisitions).
This diff does exactly that, by changing the `Event.LockAcquire` variant to take a list of locks.
Reviewed By: ezgicicek
Differential Revision: D24052304
fbshipit-source-id: 410c812d7
Summary:
This diff avoids some usages of functors when they are applied only once in `polynomials.ml`. While
functor is in general helpful to abstract data and make code cleaner, it makes us hard to understand
code, eg `merlin-locate` does not give an actual definition point of terms when it is from a module
parameter.
Reviewed By: ngorogiannis
Differential Revision: D23991164
fbshipit-source-id: c61289e84
Summary:
This diff extends inferbo's domain to include closure values. The goal of this extension is to
follow missing semantics where closures are handled as values, for example, a closure is assigned to
an object field, then it is got later to call.
Due to the bottom-up nature of the analyzer, sometimes we don't know which values are written in a
field, which is the same for the other non-closure values.
Reviewed By: ezgicicek
Differential Revision: D23932186
fbshipit-source-id: 4a575d0de
Summary: Dispatch & function call mechanism was so jumbled up together. Let's refactor it to be cleaner.
Reviewed By: skcho
Differential Revision: D24049889
fbshipit-source-id: 42a218016
Summary:
This makes sure we call `AbductiveDomain.summary_of_post` exactly once
per post-condition. Notice in particular in the diff:
- in Pulse.ml we remove a now-certified-useless "is_unsat_expensive"
call
- in PulseOperations.ml we add a previously-missing call to
`summary_of_post` (it's needed to remove local variables from the
symbolic state + normalize)
The price to pay is ugly type annotations and down-casting peppered in a
few places, in reasonable number.
Reviewed By: da319
Differential Revision: D24078564
fbshipit-source-id: 3102cacf0
Summary:
Take another page from the Incorrectness Logic book and refrain from reporting issues on paths unless we know for sure that this path will be taken.
Previously, we would report on paths that are merely *not impossible*. This goes very far in the other direction, so it's possible we'll want to go back to some sort of middle ground. Or maybe not. See the changes in the tests to get a sense of what we're missing.
Reviewed By: ezgicicek
Differential Revision: D24014719
fbshipit-source-id: d451faf02
Summary: We add a naive model for `forEach` idiom for Java's Iterable and Maps. The model is naive because it doesn't take the cost of the lambda into account. This will be fixed later.
Reviewed By: da319
Differential Revision: D23868203
fbshipit-source-id: 37d169c6f
Summary: Gradle produces a number of compilation units which are currently captured sequentially. This diff parallelizes this step.
Reviewed By: jvillard
Differential Revision: D23930978
fbshipit-source-id: d71c22ba3
Jules Villard
Daiva Naudziuniene
Nikos Gorogiannis
Sungkeun Cho
Mitya Lyubarskiy
Ezgi Çiçek