Summary: This diff adds TryEntry and TryExit statements to the entry and exit of C++ `try` block, in order to handle exceptional control flow better in analyses.
Reviewed By: da319, jvillard
Differential Revision: D26946188
fbshipit-source-id: 33f4ae9e7
Summary:
Update Infer to LLVM (clang) 11.1.0.
Infer/clang now uses the LLVM 'monorepo' release, simplifying the download script.
Some changes done to how/when ASTExporter mangles names, this to avoid the
plugin hitting asserts in the clang code when mangling names.
Reviewed By: jvillard
Differential Revision: D27006986
fbshipit-source-id: 4d4b6ba05
Summary:
We use `procedure_name` which is coming from `Procname.get_method` in explanation of cost issues. For blocks, procedure name includes a prefix `objc_block` and a suffix with `_x` where x is the block counter. However, displaying this name to the user is not pretty. Especially when we have nested blocks, procedure name looks like `objc_blockobjc_blockdirectUIMessageFromContentAndMetadata_10_23`.
This diff drops the block index suffix and replaces `objc_block` with a prettier version `^`(signifying block).
so instead, in the cost report, we will have `^^blockdirectUIMessageFromContentAndMetadata`.
Reviewed By: skcho
Differential Revision: D26945333
fbshipit-source-id: 9d135423c
Summary: Variables captured by reference do not have correct type in objc blocks. They are missing one reference. This diff sets the correct type of captured reference variables inside procdesc, similarly as we already have for cpp lambdas. The translation of block's body will then take into account the type of captured variable from procdesc.
Reviewed By: ezgicicek
Differential Revision: D26945575
fbshipit-source-id: 06a9d9cc6
Summary: This diff adds a test replicating the issue fixed in D26975222 (7110c1ca3f) in [commit 7110c1c](7110c1ca3f)
Reviewed By: ngorogiannis
Differential Revision: D26978562
fbshipit-source-id: 41e41df8c
Summary: We shouldn't report a complexity increase here because `existing_block_here` is a removed function (that doesn't exist in current version)!
Reviewed By: skcho
Differential Revision: D26947439
fbshipit-source-id: 6620804be
Summary: Adding option to suppress errors involving unknown code. If `--pulse-report-ignore-unknown-java-methods-patterns` is provided, reports containing skipped functions not matching at least one of the given regexps are suppressed.
Reviewed By: jvillard
Differential Revision: D26820575
fbshipit-source-id: b6e1df7b2
Summary:
Adapting error messages in Pulse so that they become more intuitive for
developers.
Reviewed By: jvillard
Differential Revision: D26887140
fbshipit-source-id: 896970ba2
Summary:
RacerD needs to analyse the class initialiser in order to establish field properties in its post, such as that certain static fields are synchronized containers.
There was a bug where class initializers were not analysed at all, from the time where there was no analysis of field properties in the post.
We still don't want to report on the class initialiser since it cannot possibly race with itself (JVM guarantees that) and it cannot race with any of the other methods in its class (because it must finish before any other method can be called).
Reviewed By: da319
Differential Revision: D26887151
fbshipit-source-id: 570aff370
Summary: The `NonBlocking` annotation should zero out all domain elements that represent blocking calls. The current implementation only really removes such elements when they are generated by the current method under analysis, leaving such elements from callees unaffected. This diff fixes that.
Reviewed By: jvillard
Differential Revision: D26874704
fbshipit-source-id: 2d4859b30
Summary:
This changes the results. I think it's because we cut short paths to
ISL errors sooner now, before they are duplicated and moved. I could not
really assess what was going on though so could be wrong.
On OpenSSL 1.0.2d:
Before: 106 issues
After: 90 issues
Reviewed By: ezgicicek
Differential Revision: D26822331
fbshipit-source-id: e861e7fc2
Summary:
This will enable further improvements: basically we want to be able to
abort the symbolic execution of a single disjunct whenever an error is
detected. Right now there is only one kind of error, which is now
explicitly called `ReportableError`.
The next diff refactors Pulse.ISL to add its own error type so that we
are able to get rid of the isl_status field (ISLOk/ISLError) inside
abductive states. ISLError states are really `Error _` states but
previously it would have been too much of an API change to expose that.
Now it's all going to be part of `AccessResult.t`.
A further change will add another error type for when a value is found
to be 0 after the fact by the arithmetic.
Reviewed By: ezgicicek
Differential Revision: D26821178
fbshipit-source-id: 2923db8e7
Summary:
It makes more sense to return a list of results than a result of lists:
the latter stops the execution on *all* the disjuncts that would have
been in the list as soon as *one* of them fails. This is the same issue
we solved for non-ISL pulse models earlier.
Reviewed By: skcho
Differential Revision: D26818409
fbshipit-source-id: 7cc1d8b39
Summary: In ObjC, when a method is called on nil, there is no NPE, the method is actually not called and the return value is 0/false/nil. There is an exception in the case where the return type is non-POD. In that case it's UB and we want to report an error.
Reviewed By: jvillard
Differential Revision: D26815687
fbshipit-source-id: 8126414ab
Summary: We were missing a part of the trace if it was going through a nil summary as the invalidation was set in the nil summary. Instead of creating a fresh value for return in the nil summary {self=0}{return=0}, we return self {self=0}{return=self}. This way we keep all the information about invalidation in the trace.
Reviewed By: jvillard
Differential Revision: D26871098
fbshipit-source-id: 6eb175e68
Summary:
Providing model for the android function TextUtils.isEmpty(). For now,
this always returns false assuming that the given value is not null.
Reviewed By: jvillard
Differential Revision: D26779619
fbshipit-source-id: 3d8e26813
Summary: Adding support for the Java instanceof operator in Pulse.
Reviewed By: jvillard
Differential Revision: D26275046
fbshipit-source-id: 8ba608cca
Summary:
This diff runs `infer reportdiff` on config impact results, ie previous and current
`config-impact-report.json`s. Ungated and added/removed callees are reported at `introduced.json`.
Reviewed By: ezgicicek
Differential Revision: D26723054
fbshipit-source-id: efabd0d5f
Summary: Adding temporary model for Collections/Map isEmpty() as an attempt to reduce false positives before we provide a full model for Collections.
Reviewed By: ezgicicek
Differential Revision: D26724085
fbshipit-source-id: d3418c173
Summary: `STARVATION` is currently used as a catch-all for several blocking events. This diff splits out `IPC_ON_UI_THREAD`.
Reviewed By: skcho
Differential Revision: D26691868
fbshipit-source-id: 618423793
Summary:
Only register biabduction-style timeouts the first time the function
exe_timeout is called. This avoid getting timeouts in other
long-running analyses. (Especially on windows, where the wall clock is
used.)
Pull Request resolved: https://github.com/facebook/infer/pull/1391
Reviewed By: skcho
Differential Revision: D26780445
Pulled By: jvillard
fbshipit-source-id: 19631b702
Summary:
gcc warnings are more strict starting from gcc10. Not having the const
qualifier triggers an error.
Pull Request resolved: https://github.com/facebook/infer/pull/1393
Reviewed By: skcho
Differential Revision: D26780417
Pulled By: jvillard
fbshipit-source-id: 4507c55eb
Summary:
It removed the result directory without check due to a bug. This diff fixes it to do the check and more careful removement of files.
* Before removing a result directory, it checks
* if the directory is empty: This is ok.
* if the directory is non-empty, but has `results.db`: This is ok, because the directory seems to be an infer's result directory.
* if the directory is non-empty and no `results.db`: This is not ok, so it does not remove the directory.
Reviewed By: jvillard
Differential Revision: D26635059
fbshipit-source-id: fa808265f
Summary:
This diff uses config-impact-issues.exp instead of issues.exp, like in
the cost checker.
Reviewed By: ezgicicek
Differential Revision: D26723761
fbshipit-source-id: 9c6779479
Summary:
Adapting existing model for `new` used in ObjC to Java.
This allows to compute dynamic type information and will facilitate
handling `instanceof`, for instance.
Changing attribute value type from Typ.Name.t to Typ.t to handle arrays.
Reviewed By: da319
Differential Revision: D26687839
fbshipit-source-id: 2cfcd0625
Summary:
Difficult to repro as most of the time other simplifactions catch this
before we actually get to dividing by zero. Nonetheless...
shamecube
Reviewed By: da319
Differential Revision: D26758187
fbshipit-source-id: b8718c515
Summary: Instead of accumulating all reports for a location in a list and then partitioning that list by issue type, just use a map from issue types to report lists.
Reviewed By: ezgicicek
Differential Revision: D26748929
fbshipit-source-id: 81c35cd4e
Summary: Now that all reports are deduplicated using the same criterion (trace length), use that to simplify deduplication functions.
Reviewed By: skcho
Differential Revision: D26726239
fbshipit-source-id: 77e3b319a
Summary:
A "severity" level was used for keeping the highest severity issue when deduplicating across many issues on the same location. This was used for only one of the issue types reported by the analysis.
It turned out this isn't very useful and it complicates significantly the reporting code.
This diff removes the type and uses trace depth to sort all the issue types in the same way all other issue types than `starvation` used.
Next diff will remove now unnecessary stuff.
Reviewed By: skcho
Differential Revision: D26725569
fbshipit-source-id: f9287dcd1
Summary:
The config impact checker prints ungated callees in a separate file config-impact-report.json,
because its results should be compared before actual reporting as the cost checker does.
Reviewed By: ezgicicek
Differential Revision: D26665097
fbshipit-source-id: 0c6e13403
Summary:
The javax.crypto.Mac classes behaves like a container
and can lead to race conditions when used in a concurrent context.
This adds Mac operations as container writes/reads in RacerD's models.
Pull Request resolved: https://github.com/facebook/infer/pull/1395
Test Plan: CI
Reviewed By: skcho
Differential Revision: D26722737
Pulled By: ngorogiannis
fbshipit-source-id: 74f03e9a5
Summary: This diff changes the compare function of `UncheckedCallee` not to distinguish direct/indirect call.
Reviewed By: ngorogiannis
Differential Revision: D26722968
fbshipit-source-id: f83f4de10
Summary: When a method is called in ObjC on nil, there is no NPE, the method is actually not called and the return value is 0/false/nil. (There is an exception in the case where the return type is non-POD. In that case it's UB. This will be addressed later). To implement this behaviour we add additional summary to ObjC instance methods {self = 0} {return = 0}. We also want to make sure that inferred summary will not be used in we call a method on nil, hence, we add a path condition {self > 0} to get a contradiction when needed.
Reviewed By: jvillard
Differential Revision: D26664187
fbshipit-source-id: cdac2a5bb
Summary:
In the following diff, we will add `JsonConfigImpactPrinter` that will share some common code base
with `JsonCostsPrinter`. This diff prepares the sharing.
Reviewed By: jvillard
Differential Revision: D26665070
fbshipit-source-id: 5032e0611
Summary:
In some corner cases where there are a lot of sequential statements, it raised stack overflow. To
avoid the issue, this diff changes the function as tail recursive by passing a callback function.
Reviewed By: ngorogiannis
Differential Revision: D26668338
fbshipit-source-id: 822d9a5f8
Summary:
Currently, we report on all functions that are not config checked. However, the aim of the analysis is to only report on these for specific functions. Moreover, this has performance implications in practice.
This diff instead reports on functions that occur on a json file that is passed by the command line option `config-data-file`.
Reviewed By: skcho
Differential Revision: D26666336
fbshipit-source-id: 290cd3ada
Summary:
As a first step to support the Java `instanceof`
operator, this change allows the path condition to be appended with
`IsInstanceOf(var, typ)`.
Reviewed By: jvillard
Differential Revision: D26664009
fbshipit-source-id: cd19dce83
Summary:
See added tests. Passing a variable by reference to a function `foo` can
cause the variable to be added to the global state so any stores after
that might be live as long as there is another function call after the
store (since the global state shouldn't outlive the scope of the
function). Currently we don't check that the latter is true; to report
these we would need to extend the abstract domain to remember which
stores have been made without a subsequent call.
Also change Blacklisted -> Dangerous everywhere since the corresponding
option is called "liveness_dangerous_classes".
Reviewed By: skcho
Differential Revision: D26606151
fbshipit-source-id: e869e5df1
Summary:
Providing model for Java `instanceof` operator that
avoids to return true when given object is null. This is a temporary
solution that will reduce FPs while we do not provide the correct
semantics for `instanceof`.
Reviewed By: jvillard
Differential Revision: D26608043
fbshipit-source-id: 87c82b906
Summary: If we record all callees with empty summary, we end up with FPs. This diff instead only records leaf calls. for non-leaf calls, we just load the summary.
Reviewed By: skcho
Differential Revision: D26606228
fbshipit-source-id: 77e76ee9e
Summary: This diff finds a declared variable name or declared field names from trace, then constructs an error message including access paths.
Reviewed By: jvillard
Differential Revision: D26544275
fbshipit-source-id: 135c90a1b
Summary:
This diff makes the analysis inter-procedural.
* If a callee is called in a config check branch, it does nothing.
* if a callee is called outside config check branches,
* If callee's summary is empty, add the callee's name to the set of unchecked callees.
* If callee's summary is not empty, join the summary to the set of unchecked callees. (We intentionally don't add the callee's name here.)
Reviewed By: ezgicicek
Differential Revision: D26465235
fbshipit-source-id: ac3ad3543
Summary:
`add_edge_on_src` is to prepare a stack location for a local variable. Before this diff, it was
called several times for each fields.
Reviewed By: jvillard
Differential Revision: D26543715
fbshipit-source-id: 49ebf2b65
Summary:
The impurity checker assumed that in pulse summary, all key addresses of PRE state should exist in
POST state. However, the assumption is not always true. For example,
```
void foo(int x) {
int y = x;
// HERE
}
```
At `HERE`, pulse's summary is
```
POST={
roots={ &x=v1 };
mem ={ v1 -> { * -> v4 } };
}
PRE={
roots={ &x=v1 };
mem ={ v1 -> { * -> v4 },
v4 -> { } };
}
```
The `v4` entry exists only at `PRE`. Although the `v4` entry is luckily removed in the summary by
the canonicalization in this example, basically there is no guarantee about the entry sets of PRE and POST.
Reviewed By: jvillard
Differential Revision: D26550338
fbshipit-source-id: 99a31cd43
Summary:
This resolves a few instances of false negatives; typically:
```
if (x == y) {
// HERE
*x = 10;
*y = 44;
// THERE
}
```
We used to get
```
HERE: &x->v * &y ->v' * v == v'
THERE: &x->v * &y ->v' * v == v' * v |-> 10 * v' |-> 44
```
The state at THERE was thus inconsistent and detected as such (v` and
`v'` are allocated separately in the heap hence cannot be equal).
Now we normalize the state more eagerly and so we get:
```
HERE: &x->v * &y->v
THERE: &x->v * &y->v * v |-> 44
```
Reviewed By: skcho
Differential Revision: D26488377
fbshipit-source-id: 568e685f0
Summary:
There should be no equalities relevant to the precondition to
canonicalize against in the first place: equalities come either from
assignments (hence strictly to the post condition) or from PRUNE
statements, and we don't use the latter to canonicalize states anyway.
Reviewed By: skcho
Differential Revision: D26488378
fbshipit-source-id: 7923f71ea
Summary:
This was a correctness issue as nothing guarantees that bindings are in
a specific order. The following commit violates that assumptions and
made the impurity tests fail without this change.
Reviewed By: ezgicicek
Differential Revision: D26488379
fbshipit-source-id: e9cc41147
Summary:
Pretty minor, it's more convenient to make it return the state and will
be used in a later diff when that function will actually sometimes
modify the state.
Reviewed By: skcho
Differential Revision: D26488376
fbshipit-source-id: a21eaf008
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:
Using more than the "known" part of the arithmetic could accidentally
leak "pruned" information into certain facts.
I noticed this when adding more term equality reasoning to pulse in
another diff. At the moment this has little effect but is still more
correct conceptually.
Reviewed By: ezgicicek
Differential Revision: D26450333
fbshipit-source-id: eb31da344
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:
ClangWrapper.ml was skipping clang commands that didn't capture
by default. It was using the 'skip_analysis_in_path_skips_compilation'
flag to NOT skip commands. This is a confusing use of that flag.
Default should be to run clang (in case it does something useful),
and a new flag to disable this.
Reviewed By: ngorogiannis
Differential Revision: D26459100
fbshipit-source-id: 7f2e9a269
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: As there are no dependencies between procedure and file analyses in RacerD, split them into separate modules.
Reviewed By: ezgicicek
Differential Revision: D26198874
fbshipit-source-id: 032aad9d8
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:
Sometimes purity running failed because it couldn't find inferbo mem. Let's make it print a warning
message, instead of raising an exception.
Reviewed By: ezgicicek
Differential Revision: D26367275
fbshipit-source-id: d2350e855
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:
Change most `t list access_result` to `t access_result list` so that the
Ok/Error is individual to each result in the list instead of having only
a toplevel Ok/Error affecting the whole list.
To make it not horrible to write this introduces new "monadic" operators
`let<*>` and `let<+>`. They are not entirely satisfactory but perhaps
it's just a notation issue as they are not quite bind/map operators
unlike what their notation might suggest. I'd say good enough for now.
The type change induced quite the churn but the new operators simplify
the code overall.
Reviewed By: skcho
Differential Revision: D26150505
fbshipit-source-id: 33764fae3
Summary:
Wrap the TOPL post-processing in the exit node debug wrapper too so that
we can see what it's doing if needed.
Reviewed By: skcho
Differential Revision: D26174365
fbshipit-source-id: dd63905ff
Summary:
When a union type has a member function in C++, it is parsed as `CppClass`. However, sometimes we may want
to distinguish normal cpp classes and union classes. This diff adds a field to the type name.
Reviewed By: jvillard
Differential Revision: D26125619
fbshipit-source-id: 44a6e8192
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:
States would be considered equal when they describe the same heap shape
even though their path conditions were different. Not good.
Reviewed By: skcho
Differential Revision: D26022135
fbshipit-source-id: 510913cde
Summary:
This is all dead code but I had to do this to try something else and I
don't want to have to do that again :)
Reviewed By: skcho
Differential Revision: D26022111
fbshipit-source-id: 622ca10b9
Summary:
It is better for the derived comparison functions to start by comparing
the single offset `Q.t` instead of the map. The order of the pair
doesn't matter so the easiest way to achieve that is by putting the
offset first.
Reviewed By: skcho
Differential Revision: D26022080
fbshipit-source-id: 874ea5c66
Summary:
It's a potentially expensive operation given that it does graph
isomorphism twice on equal values so add a fast path for when they are
the same pointer. Also comparing "skipped calls" doesn't need to care
about traces.
Reviewed By: da319
Differential Revision: D26022022
fbshipit-source-id: 8178df37b
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: In `ClosureSubstSpecializedMethod`, it duplicates a procedure with specialized closure parameters. Since it introduces a new procedure name, its local variables in the procedure body must be replaced to use the new procedure name. (Note that local variable type includes procedure name.) However, in the previous implementation, it missed the translations in some cases: compound expressions and metadata.
Reviewed By: ezgicicek
Differential Revision: D26075490
fbshipit-source-id: 2a5a30cd8
Summary:
In the previous live analysis, it handled class constructor targets as
dead before its calling. For example,
```
// BEFORE live variables {src}
A::A(&tgt, &src)
// AFTER live variables {tgt, src}
```
It *may* be correct if we says the field values written in `tgt` is
dead. However, we cannot says the location of `tgt` is dead.
Because of this bug,
```
A x = y;
```
was translated to
```
VARIABLE_DECLARED(x)
EXIT_SCOPE(x)
// x was dead here
A::A(&x, &y)
```
See that `EXIT_SCOPE(x)` is added right after its declaration, since
the liveness analysis said `x` was dead there.
Reviewed By: ezgicicek
Differential Revision: D26048344
fbshipit-source-id: a172994e2
Summary: This is needed to address GC stalls due to a too small heap.
Reviewed By: jvillard
Differential Revision: D26045530
fbshipit-source-id: 590d1e72c
Summary: The existing code overwrites the `BUCK_EXTRA_JAVA_ARGS` environment var. It's better to extend it with our settings, if present.
Reviewed By: artempyanykh
Differential Revision: D26045398
fbshipit-source-id: 25588488c
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:
- We hoist calculation of `loop_head_to_loop_nodes` to simplify `get_loop_control_map` and also to allow it to be used by inefficient keyset iterator without needing to compute exit maps unnecessarily.
- nit on comments
- `open Control` in `loop_control.ml`
- hoist bound map calculation in `cost.ml`
Reviewed By: ngorogiannis
Differential Revision: D25952592
fbshipit-source-id: ef6103497
Summary:
Clang front-end is confused about exceptional CF. For the following program
```
void throw_positive(int b) {
if (b > 0) {
throw std::length_error("error");
}
}
void foo( std::vector<std::string> traceTokens){
if (traceTokens.size() < 13) {
throw std::invalid_argument("Exception!"); // 1
}
for (int i = 13; i < traceTokens.size(); ++i) {
try {
throw_positive(traceTokens[i].size());
} catch (std::range_error& msg) {
throw(1); // 2
}
try {
throw_positive(traceTokens[7].size());
} catch (std::range_error& msg) {
throw (9); // 3
}
}
}
```
Here, infer thinks that there are edges from 1->2 and 1-> 3. This should not be the case.
This in turn makes control analysis think that there is a back edge from 3->2 and violates the assertion that the exit node (3 in this case) must be a prune node...
Replacing assertion with internal error for now until I fix the clang frontend.
Reviewed By: skcho
Differential Revision: D25947376
fbshipit-source-id: 5c6529647
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 accessing a field or array offset of a pure variable (`Exp.Var`) that does not resolve to an access expression, `HilExp.of_sil` will create an extraneous dereference that causes `HilExp.get_typ` to fail. This pull request wraps variables that are the bases of Lfield or Lindex expressions with AddressOf before they're dereferenced (this is already done for Lvar inside `AccessExpression.of_pvar`) and adds a couple of unit tests that make sure it behaves as expected.
**More details on the bug:**
Given the following code:
```
if (!event_obj->dict)
```
and SIL:
```
n$6=_fun_gdb::ref_ptr<event_object,gdbpy_ref_policy<event_object>>::operator->(&event_obj:gdb::ref_ptr<event_object,gdbpy_ref_policy<event_object>>&) [line 38, column 8];
n$7=*n$6.dict:_object* [line 38, column 8];
PRUNE(!n$7, true); [line 38, column 8];
```
`operator->` has return type `event_object*`, but `n$6.dict` only has access to the type of the struct, `event_object`. `of_sil` [calls](9f98368e49/infer/src/absint/HilExp.ml (L567)) `access_expr_of_lhs_exp` with that type, which [calls](9f98368e49/infer/src/absint/HilExp.ml (L498)) `access_exprs_of_exp` (note that `add_deref` is always true). The Lfield case will then [recurse](9f98368e49/infer/src/absint/HilExp.ml (L469)) to process the Exp.Var, and `AccessExpression.of_id` will return an `AccessPath.base` that is then [dereferenced](9f98368e49/infer/src/absint/HilExp.ml (L440)). When resolving types, `get_typ` will find a non-pointer type wrapped by a `Dereference` and return [None](9f98368e49/infer/src/absint/HilExp.ml (L286)). To fix this, we match what [of_pvar](9f98368e49/infer/src/absint/HilExp.ml (L295)) does and wrap the base in an AddressOf, which is removed by the dereference.
Pull Request resolved: https://github.com/facebook/infer/pull/1372
Reviewed By: ngorogiannis
Differential Revision: D25803049
Pulled By: jvillard
fbshipit-source-id: ceadc8cad
Summary:
Pulse support for C languages ('clang') can now be considered
mature.
Reviewed By: ezgicicek, da319, jvillard
Differential Revision: D25803707
fbshipit-source-id: 5a48eb940
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:
Small model for a couple of StringUtils functions
Pull Request resolved: https://github.com/facebook/infer/pull/1346
Reviewed By: ngorogiannis
Differential Revision: D25638009
Pulled By: jvillard
fbshipit-source-id: 01db6d09e
Summary:
This sometimes happens and brings down all of infer with it. Just log
the error instead.
Fixes https://github.com/facebook/infer/issues/1338
Reviewed By: ezgicicek
Differential Revision: D25637821
fbshipit-source-id: 681207813
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:
In `Config`, the lists generated by `mk_string_list`, `mk_path_list`, `mk_rest_actions` are reversed implicitly, which made it hard for developers to use them correctly. What the previous and this diff will do is to change the list variables of the `Config` to not-reversed one.
* diff1: First diff adds `RevList` to distinguish reversed lists explicitly. All usages of the reversed list should be changed to use `RevList`'s lib calls.
* diff2: Then this diff will change types of `Config` variables to not-reversed, normal list.
Reviewed By: ngorogiannis
Differential Revision: D25562303
fbshipit-source-id: 4cbc6d234
Summary:
In `Config`, the lists generated by `mk_string_list`, `mk_path_list`, `mk_rest_actions` are reversed implicitly, which made it hard for developers to use them correctly. What this and the next diff will do is to change the list variables of the `Config` to not-reversed one.
* diff1: First this diff adds `RevList` to distinguish reversed lists explicitly. All usages of the reversed list should be changed to use `RevList`'s lib calls.
* diff2: Then the next diff will change types of `Config` variables to not-reversed, normal list.
Reviewed By: ngorogiannis
Differential Revision: D25562297
fbshipit-source-id: b96622336
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: As per summary. Note that biabduction will make the results imprecise due to async exceptions from the timeout signal handler, so we warn when both are enabled (https://github.com/janestreet/memtrace/issues/2).
Reviewed By: jvillard
Differential Revision: D25219737
fbshipit-source-id: bdef228fc
Summary:
D25495343 (72a59553d2) mistakenly removed a rev_append and replaced it with @.
Fix that and rename the variable so that it's clearer it needs to be reversed.
Reviewed By: skcho
Differential Revision: D25558030
fbshipit-source-id: c66f477f2
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:
First argument is a boolean and thus is always non-null, rather than
nullable.
Reviewed By: ngorogiannis
Differential Revision: D25532156
fbshipit-source-id: e334e0886
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:
Avoid command-line-too-long for queries where the query expression itself is overly long.
Also, require the temporary filename prefix to ease debugging.
Reviewed By: jvillard
Differential Revision: D25495343
fbshipit-source-id: 0483aac2d
Summary:
First stab at quantifier elimination done poorly but fast :)
Easy one: when we know "x = y", and we want to keep x but not y, then
replace y by x everywhere.
Reviewed By: skcho
Differential Revision: D25432207
fbshipit-source-id: 81b142b96
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:
There was a bug where we forgot to mark these values as reachable. In
particular we would forget their arithmetic value as a result.
For example, now we remember that the array access is at an index equal
to 5 in the summary of this function:
```
foo(int a[]) {
a[5] = 42;
}
```
Reviewed By: skcho
Differential Revision: D25430468
fbshipit-source-id: 4acf09842
Summary:
I... kinda forgot about attributes in D25092158 (ab2813e355), which is probably why
impurity was angry that attributes were sometimes missing. Repare this
by adding together the attributes of all the values that are equal.
Reviewed By: skcho
Differential Revision: D25428405
fbshipit-source-id: e5d55b782
Summary:
Address a long-standing embarassing TODO in a minimal way: array indices
are values and when applying a summary we didn't actually bother
translating callee values to caller values. Fix that in a simple way by
just using the current mapping between callee and caller values and
otherwise freshen callee values to avoid clashes with caller values.
Reviewed By: ezgicicek
Differential Revision: D25424013
fbshipit-source-id: 03ca59b9f
Summary:
I wrote an entire diff trying to fix the "bug" that this wasn't needed
so I think this warrants a comment ;)
Reviewed By: ezgicicek
Differential Revision: D25423958
fbshipit-source-id: 414038e40
Summary: The Ondemand entry point `analyze_proc_desc` exists purely to support specialisation under biabduction. After fixing the storing of specialised `proc_desc`s for java it suffices to use `analyze_proc_name` which will work just fine in its place.
Reviewed By: jvillard
Differential Revision: D25421763
fbshipit-source-id: b162feec3
Summary: Whenever the interface functions are called, there is always an execution environment present, so it is safer and better to get rid of the setter/getter reference thing.
Reviewed By: jvillard
Differential Revision: D25421335
fbshipit-source-id: 7110c932b
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:
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
Sungkeun Cho
Martin Trojer
Ezgi Çiçek
Daiva Naudziuniene
Gabriela Cunha Sampaio
Nikos Gorogiannis
Jules Villard
Boris Yakobowski
Andrey Makeev
Daniel Schoepe
Mitya Lyubarskiy
Adam Ernst
Joshua Selbo
Loc Le
Xiaoyu Liu
Artem Pianykh
Kevin Higgs
Luka Rahne
Franco Raimondi