Summary:
This diff adds uninitialized value check in pulse. For now, it supports only simple cases,
- declared variables with a type of integer, float, void, and pointer
- malloced pointer variables that points to integer, float, void, and pointer
TODOs: I will add more cases in the following diffs.
- declared/malloced array
- declared/malloced struct
- inter-procedural checking
Reviewed By: jvillard
Differential Revision: D25269073
fbshipit-source-id: 317df9a85
Summary:
This diff adds the ability to skip translation with `... && neg ( pattern)` logic so that we can skip translation of some files if the source does not contain a pattern.
Note that `skip-translation` expects a list of patterns as disjunctions:
https://www.internalfb.com/intern/diffusion/INFER/browse/master/infer/src/IR/inferconfig.ml?commit=76ae5fa0d3376573f6d04814e47ff6b5a9dd9746&lines=74
whereas we want the ability to have conjuctions inside.
## Context
Immutability analysis requires analyzing generated code which might have `Immutable` annotations. When analysing fbandroid, we skip all generated code:
```
"skip-translation": [
{
"source_contains": "generated",
"language": "Java"
}
],
```
However, rather than analyzing all generated code (which might be expensive across all targets) by removing the above, with this diff, we only analyze generated code that doesn't contain e.g. `Immutable` and skip all other generated code as before:
```
"skip-translation": [
{
"source_contains": "generated",
"source_not_contains": "Immutable",
"language": "Java"
}
],
```
Reviewed By: ngorogiannis
Differential Revision: D25328931
fbshipit-source-id: 3ae6ae92a
Summary:
D17710123 (ec62fbefb2) introduced locking to protect the shared pipe to the
originator of the process pool.
D20158845 (a154c8c328) changed the situation by creating a private pipe to the
originator for each worker, so should have removed the locks.
Reviewed By: ezgicicek
Differential Revision: D25370445
fbshipit-source-id: e5f3e4b00
Summary:
See comments added in the code: there's always a chance some unsat
states make it to the end of the execution of an instructions. Before
this diff they would get propagated and executed until some code path
actually bothers to check their satifiability. After this diff we throw
them out at the end of the execution of the first instruction they get
generated in.
An alternative design would be to return Unsat explicitly everywhere we
currently might return `false_`. This would be good too but there's
still a chance we'd generate `false_` and so even if we did that more
significant refactoring, the detection in this diff would still be a
good last line of defense.
Reviewed By: ezgicicek
Differential Revision: D25336042
fbshipit-source-id: a24693596
Summary: When using the restart scheduler incrementing the analyzed count before the analysis itself gives wrong results.
Reviewed By: jvillard
Differential Revision: D25367787
fbshipit-source-id: aed22cc68
Summary:
The frontend of ObjC regarding to captured variable was incorrect: it set capturing mode as
by-reference always, but it actually translaged as if all captured variables were passed with
by-value. This diff fixes this based on the document.
https://developer.apple.com/library/archive/documentation/Cocoa/Conceptual/Blocks/Articles/bxVariables.html
* global variable: by reference
* local variable: by value
* `static` local variable: by reference
* `__block` local variable: by reference
* parameter: by value
Reviewed By: jvillard
Differential Revision: D25306122
fbshipit-source-id: ec499d705
Summary:
When we know `v1 = v2`, canonicalize `v2 -> v1 * v3 -> v2` to
`v1 -> v1 * v3 -> v1`. Only do this when creating summaries
(and so also when reporting errors) for now.
This only takes into account the equality relation between variables
for now. It needs to be extended to take into account other ways
variables can be equal, eg when two variables are equal to the same
constant or the same term.
Reviewed By: skcho
Differential Revision: D25092158
fbshipit-source-id: 9e589b631
Summary:
Made `AbductiveDomain.summary_of_post` return a Sat/Unsat to make sure
callers filter unsat summaries. Also made `ExitProgram` take a summary
instead of a non-normalized abstract state, which was wrong (mostly
could litter the disjuncts with infeasible paths).
Reviewed By: skcho
Differential Revision: D25277565
fbshipit-source-id: 72dacb944
Summary:
Use the new module to represent both Sat/Unsat from Pulse formulas, and
FeasiblePath/InfeasiblePath from PulseReport.
Reviewed By: jberdine
Differential Revision: D25277566
fbshipit-source-id: 9f8412ca9
Summary:
Until then we mostly ignored aliasing constraints added by callees,
except some of the cases where the aliasing was incompatible with the
current heap. But, we should add `v_caller = v_caller'` any time both
of these (caller) variables are equal to the same callee variable.
These situations are hard to create at the moment since all values in
the pre-condition heap are created distinct and never change. The next
diff introduces canonicalisation of states and merges equal variables,
thus needs this change.
Reviewed By: skcho
Differential Revision: D25092213
fbshipit-source-id: 9fa7b8b53
Summary:
This diff uses Pvar.t in CapturedVar.t, so that
* it can include additional info in Pvar.t
* it can avoid some `Pvar.mk` calls when using the captured variables
Reviewed By: jvillard
Differential Revision: D25331763
fbshipit-source-id: 4e0c2ab4a
Summary:
- Eliminate dead `source` field in `field_data` record.
- Use a 2-level hashtable structure (`procname` -> `source_file` and `source_file` -> `file_data`) to help potentially using an LRU cache for layer 1.
- Use laziness instead of mutability.
- Fixed stale comments
Reviewed By: jvillard
Differential Revision: D25303360
fbshipit-source-id: 68a22d299
Summary:
Models are currently not specialised*. Remove the ability entirely, to allow further changes.
*this is proved by the fact that Infer doesn't crash, which it would if it tried to specialise models, because their procdesc is the already pre-analysed one, and pre-analysing twice a procdesc will crash.
Reviewed By: jvillard
Differential Revision: D25027698
fbshipit-source-id: 76ae5fa0d
Summary:
The code related to "pruned" Topl constraints was scattered in
PulseTopl. Now it's grouped in PulseTopl.Constraint.
Reviewed By: jvillard
Differential Revision: D25273820
fbshipit-source-id: 5d2d0765b
Summary:
When extracting summaries, ask PulseFormula to work harder to prove that
path-conditions are unsat. This reduces the number of false positives.
Reviewed By: jvillard
Differential Revision: D25270609
fbshipit-source-id: 61ef5e8ac
Summary:
Added a topl-max-disjuncts, which is analogous to pulse-max-disjuncts.
Note, however, that the maximum number of states tracked will be the
product of the two limits.
Added also topl-max-conjuncts, which drops Topl states that became too
complex.
Reviewed By: jvillard
Differential Revision: D25240386
fbshipit-source-id: 588c90390
Summary: Tests for the LRU cache now expect a fixed order of key-value pairs in the cache where previously only the set of key-value pairs was considered.
Reviewed By: jvillard
Differential Revision: D25301133
fbshipit-source-id: 0d8077950
Summary: In Java, public class name should be the same to file name.
Reviewed By: ezgicicek
Differential Revision: D25245194
fbshipit-source-id: 49fd16748
Summary:
This diff adds a new issue type for reporting modifications to immutable fields (when `report-immutable-modifications` is enabled).
The underlying analysis depends on impurity analysis which itself is based on post-processing of pulse's summaries.
Reviewed By: skcho
Differential Revision: D25216637
fbshipit-source-id: 42e843793
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
Nikos Gorogiannis
Sungkeun Cho
Ezgi Çiçek
Joshua Selbo
Jules Villard
Radu Grigore
Daiva Naudziuniene
Mitya Lyubarskiy
David Pichardie
Joscha Benz