Summary: It collects array accesses from all sub expressions in commands.
Reviewed By: mbouaziz
Differential Revision: D7165098
fbshipit-source-id: 584dc80
Summary: It does not only malloc a new heap memory, but also copy its contents.
Reviewed By: mbouaziz
Differential Revision: D7152194
fbshipit-source-id: 58cba5e
Summary:
- Add support for floating point values to JsonBuilder
- This allows EventLogger to log fields of type float
Reviewed By: dulmarod
Differential Revision: D7138542
fbshipit-source-id: 8a4e353
Summary: This is to make sure than the analysis produces the same results independently from the order in which the members of a call cycle are analyzed.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6881971
fbshipit-source-id: 23872e1
Summary: Add a new command-line option `--external-java-packages` which allows the user to specify a list of Java package prefixes for external packages. Then the analysis will not report non-actionable warnings on those packages (e.g., inconsistent `Nullable` annotations in external packages).
Reviewed By: jeremydubreil
Differential Revision: D7126960
fbshipit-source-id: c4f3c7c
Summary: When a property was defined in a protocol, we were not translating its attributes which leads to retain cycles false positives. This diff fixes it. It also refactors the code for translating fields a bit.
Reviewed By: mbouaziz
Differential Revision: D7136355
fbshipit-source-id: b5e7445
Summary:
A matcher that matches procnames only.
To be used in bi-abduction.
Depends on D7124877
Reviewed By: skcho
Differential Revision: D7125113
fbshipit-source-id: e44f3a8
Summary:
Because it matches calls (procnames and argument list) and because I will create a `Procname`-only one.
Depends on D7124847
Reviewed By: skcho
Differential Revision: D7124877
fbshipit-source-id: eca7c21
Summary:
Fairly simple approach here:
- If the RHS of an assignment is a frontend-generated temporary variable, assume it transfers ownership to the LHS variable
- If the RHS of an assignment is a program variable, assume that the LHS variable is borrowing from it.
- If we try to access a variable that has borrowed from a variable that is now invalid, complain.
Reviewed By: jeremydubreil
Differential Revision: D7069947
fbshipit-source-id: 99b8ee2
Summary:
Just a bunch of minor changes.
- The mutable field doesn't need to be mutable: it's only mutated once in the code somewhere that doesn't even need to mutate
- Hence the type can be public
- All the `ms_get_*` functions are replaced by field accesses
- `CMethod_signature` -> `CMethodSignature` while I'm at it, although maybe that's bad since other files in clang/ follow the former convention
- `type method_signature` -> `type t`
- `pp` function instead of `to_string`, since it's used with `fprintf`. This gets rid of the only caller of `IList.to_string`.
Reviewed By: dulmarod
Differential Revision: D7123795
fbshipit-source-id: fdfae42
Summary:
`Sequence` API to walk over free variables in expressions, instead of computing lists with uniqueness constraints that make them have linear complexity for insertion.
Switch to a Set representation when we don't care about the order of elements,
otherwise to a `Hash_queue`:
https://ocaml.janestreet.com/ocaml-core/113.33/doc/core/Std/Hash_queue.mod/S.modt/
Often, we don't even need to compute the sequence of free variables, as we are
just testing membership/emptiness/...
Reviewed By: mbouaziz
Differential Revision: D7099294
fbshipit-source-id: e96f84b
Summary:
At function calls, it copies a subset of heap memory that is newly
allocated by callees and is reachable from the return value.
Reviewed By: mbouaziz
Differential Revision: D7081425
fbshipit-source-id: 1ce777a
Summary:
This is to fix the conflicts between Eradicate and the Biabduction when reporting the same kind of errors: when Eradicate is on, the Eradicate warnings will have priority over the null deference reported by the biabduction.
If this approach proved to be successful in prod, I will refactor the reporting mechanism in the analysis itself to simply not report the null dereference in this case at all. For the codebases that aren't yet fully consistently using `Nullable`, this combined approach looks like a good way to deploy Infer toward full null safety.
Reviewed By: mbouaziz
Differential Revision: D7102119
fbshipit-source-id: 35d3add
Summary:
Enrich capability domain with borrowing info. Inline comments explain what the domain is doing.
The analyzer isn't actually using the borrowing functionality yet--that comes in the successor.
Reviewed By: jeremydubreil
Differential Revision: D7067942
fbshipit-source-id: 4c03c69
Summary:
Before D7100561, the frontend translated capture-by-ref and capture-by-value in the same way.
Now we can tell the difference and report bugs in the capture-by-value case.
Reviewed By: jeremydubreil
Differential Revision: D7102214
fbshipit-source-id: e9d3ac7
Summary:
The goal is to allocate less and generally be more efficient than handling
lists with uniqueness constraints.
Reviewed By: mbouaziz, jberdine
Differential Revision: D7098904
fbshipit-source-id: 7111f07
Summary:
The `may_last_field` boolean value in the `decl_sym_val` function presents that the location *may* (not *must*) be a flexible array member.
By the modular analysis nature, it is impossible to determine whether a given argument is a flexible array member or not---because of lack of calling context. For example, there are two function calls of `foo` below: (2) passes a flexible array member as an argument and (1) passes a non-flexible array, however it is hard to notice when analyzing the `foo` function.
```
struct T {
int c[1];
};
struct S {
struct T a;
struct T b;
};
void foo(struct T x) { ... }
void goo () {
struct S* x = (struct S*)malloc(sizeof(struct S) + 10 * sizeof(int));
foo(&(x->a)); // (1)
foo(&(x->b)); // (2)
}
```
We assume that any given arguments may stem from the last field of struct, i.e., flexible array member. (This is why `decl_sym_val` is called with `may_last_field:true` at the first time.) With some tests, we noticed that the assumption does not harm the analysis precision, because whether regarding a parameter as a flexible array member or not is about using a symbolic array size instead of a constant array size written in the type during the analysis of callee. Therefore still it can raise correct alarms if the actual parameter is given in its caller.
Reviewed By: mbouaziz
Differential Revision: D7081295
fbshipit-source-id: a4d57a0
Summary:
Instead of storing the type environment in infer-out/captured/foo.c/foo.c.tenv,
store it in the `source_files` table of the SQLite db. This limits the number
of files we create on disk.
The "file local" type environemnts are specific to the clang integration. For
Java, there is a "global tenv" file. Instead of matching on string names, this
diff also makes the API of `Tenv` reflect this situation.
The global tenv is serialized as a separate file in "infer-out/.global.tenv"
instead of "infer-out/captured/global.tenv", because "infer-out/captured/" will
soon be removed as it now only contains the global tenv (except in debug mode,
where it will still be created).
In the DB, we either store the local tenv for the file, or "global" to indicate
that the global tenv should be consulted.
This diff also moves `Cfg.store` to `SourceFiles.add` because that function
deals with more than just `Cfg.t`.
Reviewed By: jeremydubreil
Differential Revision: D6937945
fbshipit-source-id: 001c10a
Summary:
A list of free variables was computed and passed around, but never used. The
reason OCaml wasn't complaining is that the list is eventually passed to a
recursive function, which passes it to its recursive call, so it looks like
it's used there.
Reviewed By: mbouaziz
Differential Revision: D7098556
fbshipit-source-id: b22a591
Summary:
Switch to the current stable branch for clang.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D7067890
fbshipit-source-id: aedff90
Summary:
You can capture a variable by reference in a lambda, assign to it, and then invoke the lambda.
This looks like a dead store from the perspective of the current analysis.
This diff mitigates the problem by computing an additional analysis that tracks variables captured by ref at each program point.
It refuses to report a dead store on a variable that has already been captured by reference.
Later, we might want to incorporate the results of this analysis directly into the liveness analysis instead of just using it to gate reporting.
Reviewed By: jeremydubreil
Differential Revision: D7090291
fbshipit-source-id: 25eeffa
Summary:
We frequently want to treat such vars differently than true program variables.
Used in only one place now, but will be used in a successor.
Reviewed By: mbouaziz, jvillard
Differential Revision: D7067882
fbshipit-source-id: 90e0348
Summary:
As far as I can tell nothing uses it and it is ignored by the matching engine:
the "parameters" arguments are collected from config options but never actually
used for matching.
Reviewed By: sblackshear
Differential Revision: D6976273
fbshipit-source-id: 6fed5ff
Summary:
Ran into this issue on Debian Testing, in which assert.h is probably different
due to a more recent toolchain. Without this change I get the following CFG
for `assert(e)`:
```
start
|-> prune (e) -> join
|-> prune (!e) -> __infer_fail("ASSERTION_FAILURE") -> exit
```
Notice that the first branch does not get to the exit, so infer must think that
the assertion is *always* violated, and reports `error: ASSERTION_FAILURE`.
This is broken.
Reviewed By: dulmarod
Differential Revision: D7067822
fbshipit-source-id: a2bf5ac
Summary:
- EventLogger no longer depends on ProcAttributes
- This allows for other backend classes which are used by ProcAttributes to log in the future without creating a cyclic dependency structure
Reviewed By: dulmarod
Differential Revision: D7082444
fbshipit-source-id: f32a6e2
Summary: - When a CallTrace result is CR_skip, then a reason for skipping the call will be included in the record
Reviewed By: dulmarod
Differential Revision: D7082572
fbshipit-source-id: 20ed191
Summary:
It supports flexible array member using the following heuristic:
- a memory for a class is allocated by `malloc(sizeof(C) + n * sizeof(T))` format
- the last field of the class is an array
- the static size of the last field is one, i.e., `T field_name[1]`
When allocating and initializing members of classes, it sets the size of flexible array to `n+1` if the above conditions are met.
Reviewed By: mbouaziz
Differential Revision: D7056291
fbshipit-source-id: 31c5868
Summary:
The semantics of "placement new" is defined simply as an assignment.
For example, `C* x = new (y) C();` is analyzed as if `C* x = y;`.
Reviewed By: mbouaziz
Differential Revision: D7054007
fbshipit-source-id: 1c6754f
Summary:
It abstracts the environments required in modeling functions and type
declarations as a record type.
Reviewed By: mbouaziz
Differential Revision: D7065996
fbshipit-source-id: b60cd3c
Summary:
The struct fields in Cil have been sorted for long time, however the
checkers do not seem to depend on the sortedness.
Reviewed By: sblackshear
Differential Revision: D7027858
fbshipit-source-id: 9e7ab96
Summary:
- During the symbolic execution stage of the backend, Infer will log detailed stats about procedure calls
- Logging is accomplished directly within symExec/Tabulation
- call_result type is moved to tabulation.ml
CallStats was a broken module that allocated a lot of useless memory. Now, Specs.CallStats and InferPrint.CallsCsv as well as the Calls report kind in InferPrint no longer exist.
Reviewed By: dulmarod
Differential Revision: D7016439
fbshipit-source-id: 40911ee
Summary:
This commit improves precision of symbol instantiations.
When a return value of a callee is `[s1 + s2, _]` and if we want to
instantiate `s1` to `c3 + max(c4, s5)`, the lower bound was
substituted to `-oo` because our domain cannot express `c3 + max(c4,
s5) + s2`.
However, we can have instantiations that are preciser than `-oo`:
(1) `c3 + c4 + s2`
(2) or `c3 + s5 + s2`
because they are smaller than the ideal instantiation, `c3 + max(c4,
s5) + s2` and it is on the lower bound position.
For now, the implementation instantiates to (1) between the two ones,
because constant values introduced by `assert` or `assume`(`if`)
command are often used as safety conditions, e.g., `assert(index >=
0);` can place before array accesses. (We can change the stratege
later if we find that it doesn't work on some other cases.)
Reviewed By: mbouaziz
Differential Revision: D7020063
fbshipit-source-id: 62fb390
Summary:
- StatsLogs is now its own functional module in InferPrint
- No longer stores events to be logged in a list to be later logged, just immediately logs them
Reviewed By: dulmarod
Differential Revision: D7010559
fbshipit-source-id: 1837ca9
Summary: Just some minor renaming to be more consistent with other modules. I was about to use these modules and was too lazy to type `Ident.IdentSet`.
Reviewed By: da319, avarun42
Differential Revision: D6999808
fbshipit-source-id: c24edef
Summary:
- change a use of clang_method_kind to match directly on the type rather than a brittle check for equality
- make the clang_method_kind field in AnalysisStats an option
- if procedure lang is not clang, then clang_method_kind field gets skipped while logging
Reviewed By: dulmarod
Differential Revision: D7010060
fbshipit-source-id: 077094d
Summary:
- JsonBuilder now has an add_string_opt function that takes a string option instead of a string
- Further alphabetized EventLogger
Reviewed By: dulmarod
Differential Revision: D7011763
fbshipit-source-id: 73f1a4b
Summary:
A simple intraprocedural analysis that tracks when a storage location is read or deleted.
For now, this works only with local variable storage locations; field and array accesses are ignored.
In order to test this, I added a new "use-after-lifetime" warning. It complains when a variable is read or deleted after it has already been deleted.
Reviewed By: jeremydubreil
Differential Revision: D6961314
fbshipit-source-id: 75e95a2
Summary: We do not inject a destructor call if the destructor declaration does not contain a body in AST. We miss all the cases where the destructor is declared in `.h` file and defined in `.cpp` file as other files include `.h` file and do not contain the body of the destructor when destructor calls are being injected based on AST information. After this diff we inject destructor calls even if we do not have body for the destructor in AST.
Reviewed By: sblackshear
Differential Revision: D6796567
fbshipit-source-id: 1c187ec
Summary: More preparation for extending HIL with dereference and address of. We need left hand side of the assignment to also include dereference and address of.
Reviewed By: sblackshear
Differential Revision: D6976150
fbshipit-source-id: 47d1d76
Summary:
It prunes abstract memories on `assert` commands.
Problem: Since the assert command is sometimes translated to two
sequential `if` statments, it was not able to prune the memory
precisely at `assert` commands in Inferbo---the pruned memory at the
first branch was joined before the second branch.
Solution: To avoid losing the pruning information at the first branch,
now, it records which locations are pruned at the first branch and
applies the same pruning at the next branch if they have
semantically the same condition.
Reviewed By: mbouaziz
Differential Revision: D6895919
fbshipit-source-id: 15ac1cb
Summary:
See comment--`Prop(resType = blah) myProp` will generate `.myProp`, `.myPropRes`, and `.myPropAttr`, and any of them can be used to set the prop.
Because our annotation parameter parsing is a bit primitive, handle this by simply checking the `Res` and `Attr` suffixes for every `Prop`.
This shouldn't lead to false negatives because these methods will only exist if the `resType` annotation is specified anyway.
Reviewed By: jeremydubreil
Differential Revision: D6955362
fbshipit-source-id: ec59b21
Summary: InferPrint should not generate StatsLogs format at all unless Config.log_events is set to true
Reviewed By: mbouaziz, dulmarod
Differential Revision: D6976352
fbshipit-source-id: d12005a
Summary: In Obj-C blocks, we explicitly insert reads of the captured vars. This does the same thing for C++. For example, `foo() { int x = 1; [x]() { return x; } }` would previously not contain a read of `x` in `foo`. Now, we'll create a temporary that reads from `x` and pass it to the closure value.
Reviewed By: dulmarod
Differential Revision: D6939997
fbshipit-source-id: f218afc
Summary:
1) Fixes some false negatives when a method annotated with `nullable` in the header is not annotated in the implementation and the attribute lookup returns the implementation. In that case, we should follow the information given in the header.
2) Fixes some false positives when annotations are in the other way around, i.e. annotated in the implementation but not in the headers. For now, there should be no report in this case, but the analysis should be extended to report the inconsistency between the header and the implementation
3) Fixes some cases of weird reports caused by name conflicts where the method in the include has the same name has another method annotated differently.
Reviewed By: jvillard
Differential Revision: D6935379
fbshipit-source-id: 3577eb0
Summary: Preparing to extend HIL with Dereference and AddressOf expressions. Next steps: (1) change SIL -> HIL translation to preserve address of and dereference; (2) adapt analyses based on HIL to make use access expressions.
Reviewed By: jeremydubreil
Differential Revision: D6961928
fbshipit-source-id: 51da919
Summary:
Added a check for recursive calls not to add abduced reference parameters constraints. Abduced reference parameters constraints were causing assertion failure when renaming variables in specs, in particular, when transforming variables into callee variables.
A similar check is already in place for abduced retvals constraints.
Reviewed By: jeremydubreil
Differential Revision: D6856919
fbshipit-source-id: acfe840
Summary:
This allows Eradicate to lookup the annotations from the classpath and without requiring the code in the classpath to have been previously analyzed. The benefit is that source files can be analyzed independently of each other as long as the classpath is known.
The main goal is to run be able to run Eradicate as a linter without losing warnings.
We may have to add some more models of the standard libraries as no `Nullable` on a parameter does not necessarily mean that the method does not accept `null`.
Reviewed By: sblackshear
Differential Revision: D6921720
fbshipit-source-id: f525269
Summary: Some tags like `Bucket` are used, but a lot are just added to the list of tags and never read.
Reviewed By: mbouaziz
Differential Revision: D6886980
fbshipit-source-id: 4474d7f
Sungkeun Cho
Dulma Churchill
Varun Arora
Jeremy Dubreil
Tony Hu
Mehdi Bouaziz
Sam Blackshear
Jules Villard
Jérémie Marguerie
Dino Distefano
Josh Berdine
Nikos Gorogiannis
Ilya Sergey
Daiva Naudziuniene