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
Daiva Naudziuniene
Loc Le
Kevin Higgs
Luka Rahne
Gabriela Cunha Sampaio
Jules Villard
Sungkeun Cho
Franco Raimondi
Artem Pianykh
Nikos Gorogiannis
Martin Trojer
Ezgi Çiçek
Joshua Selbo