Summary:
Instead of recording some facts as "known" (i.e., observed assignments),
record them as "pruned". This should be done any time the fact is not an
assignment, for instance when path-splitting on "is the argument =0?" as
in the model of `free()`.
Reviewed By: ezgicicek
Differential Revision: D26450362
fbshipit-source-id: 4fc980f90
Summary:
These were present for `std::optional` but not `folly::Optional` for
some reason.
Reviewed By: da319
Differential Revision: D26450400
fbshipit-source-id: 45051e828
Summary: In Objective-C, `static const int var = ..` is not recognized as ICE (integral constant expression) unlike C++. To handle such loads better, this diff adds a check for `constant_global_array` as a workaround.
Reviewed By: skcho
Differential Revision: D26369461
fbshipit-source-id: e2dae11f1
Summary:
Races in Nullsafe classes can undermine NPE safety despite the class passing the type checks.
This diff adds to the report text of THREAD_SAFETY_VIOLATION and GUARDEDBY_VIOLATION the following trailer:
> Data races in `Nullsafe` classes may still cause NPEs.
This only happens if the race is directly on a non-primitively-typed member field of the class.
It also uses distinct bug types (adds the suffix _NULLSAFE to the bug types above) for easier accounting.
Reviewed By: ezgicicek
Differential Revision: D26403274
fbshipit-source-id: 3cd6ca082
Summary:
The `--pulse-model-return-nonnull` config option currently works for C++. Now we
will be using it also for Java. Changing type from string list to regexp to
make it more general.
Reviewed By: ezgicicek
Differential Revision: D26367888
fbshipit-source-id: 9a06b9b32
Summary:
Modeling Java instanceof operator in Pulse. This
implementation does not yet provide the proper semantics for instanceof.
For now, it will always return true. This is temporary and should reduce the false positive rate.
Reviewed By: da319
Differential Revision: D26317089
fbshipit-source-id: 494e3dec5
Summary: D25952894 (1bce54aaf3) changes translation of struct assignments. This diff adopts to this change for loads from global struct arrays.
Reviewed By: skcho
Differential Revision: D26398627
fbshipit-source-id: cc1fb47ab
Summary:
Before this diff:
```
// Summary of const global
// { global -> v }
n$0 =* global
// n$0 -> {global}
x *= n$0
// x -> {global}
```
However, this is incorrect because we expect `x` have `v` instead of the abstract location of `global`.
To fix the issue, this diff lookups the initializer summary when `global` is evaluated as RHS of load statement.
After this diff:
```
// Summary of const global
// { global -> v }
n$0 =* global
// n$0 -> v
x *= n$0
// x -> v
```
Reviewed By: ezgicicek
Differential Revision: D26369645
fbshipit-source-id: 98b1ed085
Summary:
`SettableFuture.set` invokes callbacks registered prior to the call, which may also try to acquire extra locks. If the called of `set` already holds a lock this creates lock dependencies which may lead to deadlocks.
Here we warn whenever `set` is called under a lock taken in a different source file. This avoids reporting when a class internally manages locks and calls `set`, reasoning that developers will be aware this is happening.
Reviewed By: jvillard
Differential Revision: D25562190
fbshipit-source-id: d1b5cb69c
Summary:
This diff resets the id generator before generating ObjC getter/setter, so parsed results are the
same without regard to the generation order. Note that the order may change when we change the type
of Procname.t since their hash values are used for the hash set of procnames.
Reviewed By: ngorogiannis
Differential Revision: D26277348
fbshipit-source-id: a66d77845
Summary:
We are getting lots of FPs due to modeling `Provider.get` as expensive. This is coming from Dependency Injection and Infer cannot statically determine the type of the provider and determine whether that provider is expensive (requires a global analysis and instrumentation).
Instead, we are downgrading this method to the default constant cost.
Reviewed By: skcho
Differential Revision: D26223978
fbshipit-source-id: 79f81c997
Summary:
Dear Infer team,
To contribute to Infer community, I would like to integrate infer#'s language agnostic layer into Infer.
Please help to review, discuss and consider to merge this feature.
Thanks,
Xiaoyu
Pull Request resolved: https://github.com/facebook/infer/pull/1361
Reviewed By: skcho
Differential Revision: D25928458
Pulled By: jvillard
fbshipit-source-id: 7726150b8
Summary: Added some basic examples for Objective-C we want to address next in pulse nullptr dereference analysis. In particular, we should not get a `nil` dereference error when we call a method on `nil`, except if the method returns a non-POD (Plain Old Data) type.
Reviewed By: ezgicicek
Differential Revision: D26053402
fbshipit-source-id: 66f4600c3
Summary:
**Existing heuristic**: If we have a call `foo(n)` that has no model and summary for `foo`, we underestimate its cost as constant[1].
However, if we have a model for `foo` (e.g.with modeled cost O(n)) but applying the model to arguments causes the cost to be Top (e.g if `n` has Top size), then we could have Top-poisoning where all the callers up the call chain will have Top costs [2].
To prevent these unintended Top-poisioning when adding models, this diff applies *the same heuristic* to modeled calls with Top cost and gives them constant cost. This way, when adding models, we wouldn't be introducing more Tops than if we were to have no models in the first place.
[1] This is problematic in itself and causes many FPs at diff time, but otherwise we would be getting Tops everywhere and would not be able to give any meaningful cost. E.g. for fblite, if we were to give unknown calls Top cost, #procedures with Top cost increases form 5% to 38% and #procedures with linear cost reduces by 99.75%.
[2] This was observed for `containsValue` for Instagram where %Tops increased by 88% :(
Reviewed By: skcho
Differential Revision: D26174644
fbshipit-source-id: 232354923
Summary:
In practice, it is not easy to mark all of NOT initialized elements of array, so let's ignore the
array value at the moment.
Reviewed By: jvillard
Differential Revision: D25372449
fbshipit-source-id: 02b2e217c
Summary:
Having different behaviours inter-procedurally and intra-procedurally
sounds like a bad design in retrospect. The model of free() should not
depend on whether we currently know the value is not null as that means
some specs are missing from the summary.
Reviewed By: skcho
Differential Revision: D26019712
fbshipit-source-id: 1ac4316a5
Summary:
When a single field struct is initialized with "type x{v}" form, the translated result is not straightforward. For example,
```
struct t {
int val_;
};
void foo(t x) {
t y{x};
}
```
calls the copy constructor with `x`. This is good.
```
void foo(int n) {
t y{n};
}
```
assigns the integer `n` to `y.val_`. This is good.
```
t get_v();
void foo() {
t y{get_v()};
}
```
assigns return value of `get_v` to `y.val_`, rather than calling the copy constructor. This is not
good, but doesn't matter for actual running; `&y.val_` is the same to `&y` and `t` value is the same
to `int` value.
Reviewed By: jvillard
Differential Revision: D26146578
fbshipit-source-id: 8a81bb1db
Summary:
The test compiled with warnings, not sure how to prevent this in the
future as `infer` will suppress all warnings anyway (I wanted to add
`-Werror` to the test Makefile but that was defeated by infer itself).
Reviewed By: ezgicicek
Differential Revision: D26019682
fbshipit-source-id: d7f8fc2d8
Summary:
providing models for the checkState and checkArgument
functions, both used in Java code.
Reviewed By: da319
Differential Revision: D26101726
fbshipit-source-id: 0cc73d252
Summary: This diff fixes incorrect order of statements on `*p = !b;`.
Reviewed By: jvillard
Differential Revision: D26125069
fbshipit-source-id: 9dcefbd34
Summary:
Now that the buck java flavour is fully deployed, the genrule-based integrations for java can be removed. We also remove the combined (clang+java) integration as this will be reimplemented using flavours in the future.
Also, remove a bunch of deprecated arguments linked to these integrations.
Reviewed By: jvillard
Differential Revision: D26104384
fbshipit-source-id: 6b0059407
Summary: Creating model for the checkNotNull function from the Preconditions class in Pulse (Java). Whenever `checkNotNull(x)` is called, Pulse will assume that `x!= null`.
Reviewed By: ezgicicek
Differential Revision: D26075176
fbshipit-source-id: 40dcd395b
Summary:
This diff fixes incorrect order of statements on assignments.
In the translation of `LHS=RHS;`, if `RHS` is a complicated expression that introduced new nodes, eg a conditional expression, some load statements for `LHS` came after its usage. To avoid the issue, this diff forces it to introduce new nodes for `LHS`.
Reviewed By: jvillard
Differential Revision: D26099782
fbshipit-source-id: 27417cd99
Summary: This diff adds an additional parameter of struct return type in ObjC's methods. The additional parameter had been supported only in C/C++ functions/methods for 5 years (D2865091 (ec80d40bdd)). If there is no specific reason not to do that, let's do it and fix the incorrect frontend translations.
Reviewed By: jvillard
Differential Revision: D26049748
fbshipit-source-id: 414b3011f
Summary: Allowing Pulse NPE reports on Nullsafe classes to be suppressed. This is now possible via the optional argument --pulse-nullsafe-report-npe (default: true).
Reviewed By: da319
Differential Revision: D25997321
fbshipit-source-id: 98465df79
Summary: Copying Java biabduction tests into pulse tests folder. The goal is to check how well Pulse will perform on Java.
Reviewed By: jvillard
Differential Revision: D25901299
fbshipit-source-id: a117b44f5
Summary:
When C and C++ code handle a common struct typed value, the struct
type is handled as a `CStruct` in the C code, but as a `CppClass` in
the C++ code. On the other hand, `Fieldname.t` contains a string of
field and **the struct type**. As a result, even if a same field is
accessed in C and C++ code, the accessed fieldnames are different.
```
void callee_in_c(struct s* x) {
x->a = 3;
}
void caller_in_cpp() {
struct s x;
x.a = 5;
callee_in_c(&x);
// HERE
}
```
For example, in the above code, `caller_in_cpp` sets the field `a` as
5, then calls `callee_in_c`, which sets the field `a` as 3. However,
at `HERE`, the value of `x` in Pulse is `{a -> 5, a -> 3}`, because the two
fieldnames are addressed as different ones.
To avoid the issue, this diff loosens the fieldname comparison in
Pulse.
Reviewed By: jvillard
Differential Revision: D26000812
fbshipit-source-id: 77142ebda
Summary: Renaming biabduction tests in infer/tests/codetoanalyze/java/biabduction/*.java to follow our naming convention: fooOk for tests where no report is expected, fooBad when we expect a report, and FP_ or FN_ prefixes when reality doesn't match the expectation
Reviewed By: jvillard
Differential Revision: D25900575
fbshipit-source-id: ad1370085
Summary:
D20769039 (cec8cbeff2) added a preanalysis step that creates edges from throw nodes to all reachable catch nodes. It intended to fix some deadstore FPs however it caused more damage than the fix itself. In particular, throws were connected irrespective of
- the type of the exception
- whether the try was surrounded by a catch
This in turn caused weird CFGs with dangling and impossible to understand nodes:(
This diff reverts this change for now.
Instead, the fix should probably be done in the frontend where we have more information about try/catch blocks.
Reviewed By: da319
Differential Revision: D25997475
fbshipit-source-id: bbeabfbef
Summary:
When there was an assignment of C struct, `x = y;`, it was translated to the statements of load and store.
```
n$0 = *y
*x = n$0
```
However, this is incorrect in Sil, because a struct is not a value that can be assigned to registers. This diff fixes the translation as assignments of each field values :
```
n$0 = *y.field1
*x.field1 = n$0
n$0 = *y.field2
*x.field2 = n$0
...
```
It copies field values of C structs on:
* assign statement
* return statement
* declarations.
It supports nested structs.
Reviewed By: jvillard
Differential Revision: D25952894
fbshipit-source-id: 355f8db9c
Summary:
Lambdas are essentially private (but are not marked as such in Infer),
so we should only report on their non-private callers.
Meanwhile, add a test to document that access propagation to those
callers is currently broken.
Reviewed By: da319
Differential Revision: D25944811
fbshipit-source-id: ef8ca6d9c
Summary:
This diff fixes a bug in the translation of an empty for-loop. When both initialization and
incrementation statements did not introduce a new node, the frontend generated an incorrect results
where the for-loop was unreachable from the entry node.
Fixes https://github.com/facebook/infer/issues/1374
Reviewed By: jvillard
Differential Revision: D25912142
fbshipit-source-id: 15b65cb84
Summary:
Previously, only names containing '$' were considered synthetic. We need
to extend the logic and look for "_UL_" in the name as well.
Also I deduped 4 different impls of "is_synthetic/generated/autogen".
Reviewed By: ngorogiannis
Differential Revision: D25899232
fbshipit-source-id: 9463eca6b
Summary:
When the body of the loop doesn't created a node then they don't get
wired correctly to the rest of the loop and end up dangling. Force node
creation to fix that.
Fixes https://github.com/facebook/infer/issues/1373
Reviewed By: ezgicicek
Differential Revision: D25804185
fbshipit-source-id: 85108bdd9
Summary:
We need to make sure a node is created to avoid instructions appearing
in the wrong order in the final CFG.
Reviewed By: da319
Differential Revision: D25784405
fbshipit-source-id: 3ef27d712
Summary: Model ` std::__optional_storage_base::has_value` as this is what we see in clang AST when translating `std::optional::has_value` for libc++. For libstdc++, we get `std::optional::has_value` as expected.
Reviewed By: skcho, jvillard
Differential Revision: D25585543
fbshipit-source-id: b8d9d2902
Summary:
The problem is that in `AnnotatedField.special_case_nullability` we
first check the _generic_ nullability and if it is `nonnullish` we
apply refinements for enums, synthetic fields, etc.
The problem is that the definition of `is_nonnullish` changed in
D25186043 (7dcbacf693) to a stricter one `UncheckedNonnull`, but generic
nullability stayed the same `ThirdPartyNonnull`.
Therefore enum elements were not considered `nonnullish` under
`--no-nullsafe-optimistic-third-party-in-default-mode` and the enum
refinements were not applied, which led to bogus errors.
**Example:**
There's a third-party enum
```
enum EnumClass {
ENUM_ELEMENT
}
```
`ENUM_ELEMENT` is represented as a private static field of
`EnumClass`.
Then we have first party code that does
```
EnumClass.ENUM_ELEMENT
```
If this first party class is not `Nullsafe` and the checker is ran
with `--no-nullsafe-optimistic-third-party-in-default-mode`, the user
gets an incorrect warning about `ENUM_ELEMENT` being unvetted third
party.
Reviewed By: ngorogiannis
Differential Revision: D25560119
fbshipit-source-id: 4ad0760c5
Summary: using 'buck clean' rather than 'rm -rf buck-out' makes buck happier, apply to all buck integration tests
Reviewed By: ngorogiannis
Differential Revision: D25558469
fbshipit-source-id: 6c07341d6
Summary:
ndkbuild builds for all supported targets by default, giving errors
for clangs that doesn't support MIPS arch (which isn't relevant for this test).
Reviewed By: da319
Differential Revision: D25533986
fbshipit-source-id: 25c6001ce
Summary:
On centos8 devservers, this test failed on bizarre buck-out/tmp java.nio.file.NoSuch
FileException. I can't tell exactly what going on with rm -rf buck-out, but my guess would be that it puts the running buckd in a bad state.
using 'buck clean' rather than 'rm -rf buck-out' makes buck happier
Reviewed By: jvillard
Differential Revision: D25534471
fbshipit-source-id: 215f993e3
Summary:
Developers complain when a function that used to only throw an exception has complexity increase in the updated revision. Let's suppress such issues by giving those functions 0 cost which is already suppressed by differential reporting.
One common case to the above throw pattern is Java methods that throw an unsupported implementation exception for a functionality that has not been implemented yet. When the developer adds the supported implementation, we don't want to warn them with complexity increase since they are adding new functionality.
This is a design choice/heuristic to prevent noisy results for now.
Reviewed By: skcho
Differential Revision: D25495151
fbshipit-source-id: 94a82b062
Summary: This diff revises the trace generation of the uninitialized value checker, by introducing a new diagnostics for it.
Reviewed By: jvillard
Differential Revision: D25433775
fbshipit-source-id: 1279c0de4
Summary: This diff gives semantics of dispatch_sync to call the closure parameter.
Reviewed By: jvillard
Differential Revision: D25423175
fbshipit-source-id: a45309073
Summary:
This diff supports inter-procedural uninit analysis in pulse.
* Added `MustBeInitialized` attribute to pre state when an address is read
* Remove `Uninitialized` attribute when callee has `WrittenTo` for the
same address
Reviewed By: jvillard
Differential Revision: D25368492
fbshipit-source-id: cbc74d4dc
Summary:
Skipping the analysis of `std::vector::empty()` caused false positives: in the case where `std::vector::empty()` was called several times ("returning" different values each time), we were not able to prune infeasible paths.
Model `std::vector::empty()` as returning the same value every time it is called.
Reviewed By: ezgicicek
Differential Revision: D23904704
fbshipit-source-id: 52e8a2451
Summary:
Since D20736043 (d84fea52ae) is adding edges from the noreturn function node to exit node, analyzers should
handle the state differently to normal states.
Reviewed By: ezgicicek
Differential Revision: D25402576
fbshipit-source-id: a98e41b0c
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:
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 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: 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: 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:
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:
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:
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:
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:
In all other places, we index params from 0, but accidentally recorded
the wrong number in json. It was because of the confusion between index
and user-visible param position that we show for the user message.
This diff fixes it: now we use 0-based indices internally (but of course still
report 1-based ones in the error message).
Reviewed By: artempyanykh
Differential Revision: D24916878
fbshipit-source-id: 45532c5ff
Summary:
Split the translation of return more aggressively between:
1. the instruction that has to happen before the translation of the sub-expr
2. the sub-expr
3. the instruction that has to happen after the sub-expr
This is needed for the next diff which creates potentially large CFGs in
(2).
Reviewed By: da319
Differential Revision: D24954071
fbshipit-source-id: a7e7e2527
Summary: Model `folly::Optional::get_pointer` which returns an address to a value if exists or `nullptr` if empty.
Reviewed By: jvillard
Differential Revision: D24935677
fbshipit-source-id: 9d990fe07
Summary:
We deliberately stopped as soon as an error was detected when applying a
function call. This is not good as other pre/posts of the function may
apply cleanly, which would allow us to cover more behaviours of the
code.
Went on a bit of a refactoring tangeant while fixing this, to clarify
the `Ok None`/`Ok Some _`/`Error _` datatype returned by PulseInterproc.
Now we report errors as soon as we find them during function calls but
continue accumulating specs afterwards.
Reviewed By: da319
Differential Revision: D24888768
fbshipit-source-id: d5f2c29d7
Summary:
Communicate new facts from the arithmetic domain to the memory domain to
detect contradictions between the two.
Reviewed By: jberdine
Differential Revision: D24832079
fbshipit-source-id: 2caf8e9af
Summary:
This is several inter-connected changes together to keep the tests
happy.
The ConditionalOperator `b?t:e` is translated by first creating a
placeholder variable to temporarily store the result of the evaluation
in each branch, then the real thing we want to assign to reads that
variable. But, there are situations where that changes the semantics of
the expression, namely when the value created is a struct on the stack
(eg, a C++ temporary). This is because in SIL we cannot assign the
*address* of a program variable, only its contents, so by the time we're
out of the conditional operator we cannot set the struct value
correctly anymore: we can only set its content, which we did, but that
results in a "shifted" struct value that is one dereference away from
where it should be.
So a batch of changes concern `conditionalOperator_trans`:
- instead of systematically creating a temporary for the conditional,
use the `trans_state.var_exp_typ` provided from above if available
when translating `ConditionalOperator`
- don't even set anything if that variable was already initialized by
merely translating the branch expression, eg when it's a constructor
- fix long-standing TODO to propagate these initialization facts
accurately for ConditionalOperator (used by `init_expr_trans` to also
figure out if it should insert a store to the variable being
initialised or not)
The rest of the changes adapt some relevant other constructs to deal
with conditionalOperator properly now that it can set the current
variable itself, instead of storing stuff inside a temp variable. This
change was a problem because some constructs, eg a variable declaration,
will insert nodes that set up the variable before calling its
initialization, and now the initialization happens *before* that setup,
in the translation of the inner conditional operator, which naturally
creates nodes above the current one.
- add a generic helper to force a sequential order between two
translation results, forcing node creation if necessary
- use that in `init_expr_trans` and `cxxNewExpr_trans`
- adjust many places where `var_exp_typ` was incorrectly not reset when translating sub-expressions
The sequentiality business creates more nodes when used, and the
conditionalOperator business uses fewer temporary variables, so the
frontend results change quite a bit.
Note that biabduction tests were invaluable in debugging this. There
could be other constructs to adjust similarly to cxxNewExpr that were
not covered by the tests though.
Added tests in pulse that exercises the previous bug.
Reviewed By: da319
Differential Revision: D24796282
fbshipit-source-id: 0790c8d17
Summary:
The starvation domain keeps a domain element per distinct pair of lock object and source location. This was used to counteract the imprecision of implicit Quandary-style traces. Starvation has used explicit traces for a long time now, so keeping all these elements is expensive (in fact, in some cases exponential) and of no value. Now, lock object identity is the only distinguishing feature of a domain element.
Also, fix some pretty printing for debugging purposes.
Reviewed By: jvillard
Differential Revision: D24829306
fbshipit-source-id: 22e12f9c1
Summary: We recently introduced a more precise model for constructing an optional from a value by making a shallow copy. However, this introduced Use After Delete false positives. For now, we go back to a less precise model by creating a fresh value. A proper model would be to either make a deep copy or call the copy constructor for a value. We will address this in the following diff.
Reviewed By: jvillard
Differential Revision: D24826749
fbshipit-source-id: 3e5e4edeb
Summary: Refactor `folly::Optional` models to make them easier to reuse for `std::optional`
Reviewed By: jvillard
Differential Revision: D24760053
fbshipit-source-id: f665e84c8
Adam Ernst
Jules Villard
Ezgi Çiçek
Nikos Gorogiannis
Gabriela Cunha Sampaio
Sungkeun Cho
Xiaoyu Liu
Daiva Naudziuniene
Artem Pianykh
Martin Trojer
Loc Le
Radu Grigore
Mitya Lyubarskiy
Joscha Benz
David Pichardie