Summary:
Previously, impurity analysis only collected one access for a single modification but not all other modifying accesses. This diff
- changes the impurity domain to collect all modifying accesses
- tracks and prints all the accesses seen to reach the modification, improving readability&debugging
Recording all accesses are needed in the next diff to determine if a method modifies any immutable fields. To determine that, we need to know all modifications, not just a single one.
Reviewed By: skcho
Differential Revision: D25186516
fbshipit-source-id: 43ceb3cd8
Summary: The main point here is to ignore owned interfaces when considering whether to warn about non-thread-safe calls.
Reviewed By: ezgicicek
Differential Revision: D25187775
fbshipit-source-id: c2a7ce89c
Summary: There are no users of this, and it stands in the way of refactoring.
Reviewed By: ezgicicek
Differential Revision: D25241940
fbshipit-source-id: 5e653341a
Summary: To look for captured variable address escape we should only check the validity of the addresses captured by reference. Checking the validity of the address captured by value can cause nullptr dereference false positives.
Reviewed By: jvillard
Differential Revision: D25219347
fbshipit-source-id: faf6f2b00
Summary:
For a long sequence of calls nop();...;nop() the runtime was quadratic
because formals and actuals were bound via equalities. Now,
substitutions are used, when easy.
Reviewed By: jvillard
Differential Revision: D25211504
fbshipit-source-id: 696e3dcdf
Summary:
If f() calls g() and g() violates a property, there used to be two
traces (one for f() and one for g()) even if all that f() has to do with
the property is that it calls g(). Now the error is reported only in
g().
Reviewed By: jvillard
Differential Revision: D25210007
fbshipit-source-id: 68ea57e71
Summary:
A "large step" is a call, and it is "trivial" if it does not affect the
automaton state; i.e., if it is irrelevant to the property being
tracked.
Reviewed By: jvillard
Differential Revision: D25209670
fbshipit-source-id: bf3e594b3
Summary:
Makes sure that topl summaries don't repeat. Previously this happened
when two posts led to the same summary when procedure-local variables
were killed. Such repeated summaries quickly lead to exponential
explosion. (For example, the added test -- `ManyLoops.java` -- didn't
finish in any reasonable time.)
Reviewed By: jvillard
Differential Revision: D25209623
fbshipit-source-id: 04b1a3e12
Summary:
Now one can use the pattern #ArrayWrite(A,I) to match on a write at
index I in array A. This only works in the Pulse variant of Topl (not in
the one based on SIL instrumentation).
Reviewed By: jvillard
Differential Revision: D25202768
fbshipit-source-id: 479f434e3
Summary:
PulseTopl.large_step is now implemented
All active tests are migrated now to topl-in-pulse.
Reviewed By: jvillard
Differential Revision: D25179556
fbshipit-source-id: dc1136bab
Summary:
When running the deep-Pulse version of Topl, it now produces and reports
traces.
Reviewed By: jvillard
Differential Revision: D25177139
fbshipit-source-id: 6955ee0cd
Summary:
A Topl "small step" is a call to a method that is of interest to the
automaton. When such a call of interest is made, the topl component of
PulseAbductiveDomain.t is updated. This means that intra-procedural
Topl should now work entirely inside Pulse, without instrumenting Sil.
Main TODOs:
- add error extraction
- implement inter-procedural (PulseTopl.large_step)
Reviewed By: jvillard
Differential Revision: D25028286
fbshipit-source-id: e31a96d13
Summary:
When a procedure is called, we must evolve the topl component of the
PulseAbductiveDomain. This commit just inserts a call to a dummy
PulseTopl.large_step in the right place. The [large_step] function still
needs to be done.
Reviewed By: jvillard
Differential Revision: D24980825
fbshipit-source-id: 0eb280145
Summary:
Put hooks into Pulse for a faster Topl:
- done: PulseAbductiveDomain now tracks a Topl state
- todo: PulseTopl needs some transfer function (now they're dummies)
Reviewed By: jvillard
Differential Revision: D23815497
fbshipit-source-id: f3f0cf9ef
Summary: Ocaml doesn't have extensible records so the workaround I have found is to wrap the inferbo model env into another record.
Reviewed By: skcho
Differential Revision: D25244745
fbshipit-source-id: 87f53d5e5
Summary: We always add Pvars to impurity domain. So let's simplify the domain to make it explicit.
Reviewed By: ngorogiannis
Differential Revision: D25220214
fbshipit-source-id: 4dc9bce4c
Summary:
Currently, we don't issue warnings for third party return value in
non-@Nullsafe modes.
For some integrations, this feature is useful.
This diff repurposes the existing param to suit this goal.
Reviewed By: artempyanykh
Differential Revision: D25186043
fbshipit-source-id: 308101841
Summary:
This diff makes the issue to be rendered more clearly. Before, we used to report
weirdly looking unconventional mode names like NullsafeLocal, even when
exact mode name was irrelevant.
Reviewed By: artempyanykh
Differential Revision: D25186041
fbshipit-source-id: 2619bcbd2
Summary:
Similar to the `tar` command, append `sudo` to the `ln` command since it fails due to 'Permission Denied' errors on Linux
Pull Request resolved: https://github.com/facebook/infer/pull/1344
Reviewed By: skcho
Differential Revision: D24917642
Pulled By: jvillard
fbshipit-source-id: d593d12b8
Summary:
This diff adds trace of closure in autoreleasepool checker. We introduce a symbolic trace value for closure variable.
* It is added to the trace when closure variable is called
* and is substituted to concrete one when actual closure is given later.
Reviewed By: ezgicicek
Differential Revision: D25025883
fbshipit-source-id: a6e246be7
Summary: At a function call, an access performed by a callee must be processed in various ways before it's added to the accesses of the caller, and several of these steps may throw away the access. Previously, this was done by effectively doing a bit of transformation, creating a new set of accesses, then folding over that to add to the caller's. This is inefficient and somewhat confusing, as this can be done with one fold and a sequence of `Option.map`s.
Reviewed By: skcho
Differential Revision: D24885117
fbshipit-source-id: 4ab61eab9
Summary:
Existing closure substitution only supported direct block calls to formals.
The following didn't work since the domain was only keeping track of loads/calls from formals, but didn't support stores.
```
void foo(dispatch_block_t block1){
dispatch_block_t local_block = block1;
local_block(); // we don't substitute the call here
}
```
This diff adds support for assigning a block to a local variable so that we can specialize the above example.
We now have a pair domain
- existing mapping from ids to block vars
- a new mapping from mangled to block specializations
the latter allows us to update the mapping in local block assignment (via store).
Reviewed By: skcho
Differential Revision: D25030234
fbshipit-source-id: 3f172341c
Summary:
Specialized closure substitution was broken for conditionals:
```
void foo(dispatch_block_t block1){
if (x){
block1(); // not replaced with specialized implementation
}
}
```
The problem was that when substituting function calls, it only used memory state at the exit node, rather than at each program point.
We could solve this by
- reverting the domain change in D24418560 (c47911359a), i.e. collecting all possible mappings conservatively (e.g. switch the domain back to `Map`)
- pass the `invariant_map` for substitutions at each program point.
We go with the second option here.
The closure substitution is still somewhat broken as exemplified by the following example:
```
void foo(dispatch_block_t block1){
dispatch_block_t local_block = block1;
local_block(); // we don't substitute the call here
}
```
Reviewed By: skcho
Differential Revision: D24993962
fbshipit-source-id: ebadddb58
Summary:
A minor but persistent annoyance: named argument of a non-ambiguous type
of almost the same name. No.
Reviewed By: skcho
Differential Revision: D24991673
fbshipit-source-id: c806f9cec
Summary:
This was left as a TODO before: where to place calls to destructors for
C++ temporaries that are only conditionally creating when evaluating an
expression. This can happen inside the branches of a conditional
operation `b?e:f` or in potentially-short-circuited conditions on the
righ-hand side of `&&` and `||` operators.
Following the compilation scheme of clang (observed by looking at the
generated LLVM bitcode), we instrument the program with "marker"
variables, so that for instance `X x = true?X():y;` becomes (following
the execution on the true branch):
```
marker1 = 0; // initialize all markers to 0
PRUNE(true) // entering true branch
X::X(&temporary); // create temporary...
marker1 = 1; // ...triggers setting its marker to 1
X::X(&x, &temporary); // finish expression
if (marker1) {
X::~X(&temporary); // conditionally destroy the temporary
}
```
In this diff, you'll find code for:
- associating markers to temporaries that need them
- code to initialize markers to 0 before full-expressions
- code to conditionally destroy temporaries based on the values of the
markers once the full-expression has finished evaluating
Reviewed By: da319
Differential Revision: D24954070
fbshipit-source-id: cf15df7f7
Summary:
The translation of `switch` cases needs to insert nodes around the
translation of each `case` sub-statement, so we need to force node
creation in these sub-statements so the nodes around it can be connected
to the translation of the sub-statements.
Also added more logging I found useful when debugging that.
Reviewed By: da319
Differential Revision: D24991455
fbshipit-source-id: d3a622142
Summary:
The current source parser is based on ocamllex only.
In order to track field declaration locations, we propose a
new parser using ocamllex/menhir. This is a more ambitious
project that closely follows the official Java syntax.
Reviewed By: jvillard
Differential Revision: D24858280
fbshipit-source-id: 22d6766e5
Summary:
These are not simply handled by `@deriving` since:
- These types are recursive and so some fields need to be ignored
- Some are uniquely identified by one of their fields
- Some fields are mutable, but set only during construction, and need
to be considered by compare, equal, hash, but ppx_hash refuses.
Reviewed By: jvillard
Differential Revision: D24989064
fbshipit-source-id: 7f8d699e5
Summary:
The use of realpath on paths obtained from debug info and the current
working directory is application-usage-specific behavior that does not
belong in the backend library. This diff moves these uses to the
frontend and cli, respectively. Also, the use of realpath in the
frontend is memoized along the same lines as the other frontend
translation functions.
This was also the last use of `core` in the `sledge` library, so the
dependency is moved to `sledge_cli` and `sledge_report`.
Reviewed By: ngorogiannis
Differential Revision: D24989070
fbshipit-source-id: c21b275f5
Summary:
Currently __llair_choice is left undefined, and so executed as skip.
This has the correct behavior, but makes it hard to distinguish from
calls to unintentionally-undefined procedures.
Reviewed By: ngorogiannis
Differential Revision: D24989068
fbshipit-source-id: f62981857
Summary:
Use B/K/M/G/... units for memory quantities, round percentages to 2
decimal places, and robustly detect deltas of close to zero.
Reviewed By: ngorogiannis
Differential Revision: D24989063
fbshipit-source-id: 35f0bccfb
Summary:
Instructions that have multiple specs sometimes have inconsistent
footprints for one or more of their specifications. In such cases, the
handling of the existential and universal vocabularies was sometimes
incorrect before this diff. In particular, the ghosts of a spec need
not appear in the pure approximation of the footprint, which the
previous code incorrectly assumed. Also, the unit of disjunction is
`false` with an empty vocabulary, not the precondition's vocabulary as
the previous code incorrectly used.
Reviewed By: ngorogiannis
Differential Revision: D24989067
fbshipit-source-id: eca3bff55
Summary:
Change `-llair-output` to `-output`, for binary form, and
`-llair-txt-output` to `-llair-output`, for textual form. Also
correspondingly change `.llair` to `.bllair`, for binary, and
`.llair.txt` to `.llair` for text.
This improves command line argument completion, and makes `.llair` the
extension of the files most commonly interacted with.
Reviewed By: ngorogiannis
Differential Revision: D24951506
fbshipit-source-id: ad4c73ca2
Summary:
The `seq` name of this field refers to the expected sort of it's
value, where the others refer to the role they play. So rename
seq (for sequence) to cnt (for contents).
Reviewed By: ngorogiannis
Differential Revision: D24951507
fbshipit-source-id: fd6640517
Ezgi Çiçek
Nikos Gorogiannis
Daiva Naudziuniene
Radu Grigore
Mitya Lyubarskiy
David Pichardie
Joscha Benz
Edwin Kofler
Sungkeun Cho
Martin Trojer
Jules Villard
Joshua Selbo
Josh Berdine