Summary: In the pointer arithmetics, it returns top, if we cannot precisely follow the physical memory model, e.g., (&x + 1).
Reviewed By: mbouaziz
Differential Revision: D7453510
fbshipit-source-id: db8738e
Summary:
Report nullable inconsistencies by relying on the bytecode, and not on the presence of analysis summary on disk.
This use the `--external-java-packages` to avoid reporting inconsistencies outside of the codebase.
Reviewed By: sblackshear
Differential Revision: D7481101
fbshipit-source-id: 281135d
Summary:
If an aggregate `a` has a field `f` whose type has a constructor (e.g., `std::string`), we translate creating a local aggregate `A { "hi" }` as `string(&(a.f), "hi")`.
This diff makes sure that we recognize this as initializing `a`.
Reviewed By: jeremydubreil
Differential Revision: D7404624
fbshipit-source-id: 0ba90a7
Summary:
Show where the invalidation occurred in the trace.
Should make things easier to understand.
Reviewed By: jeremydubreil
Differential Revision: D7312182
fbshipit-source-id: 44ba9cc
Summary: This was causing false positives when returning the constant integer 0.
Reviewed By: sblackshear
Differential Revision: D7330143
fbshipit-source-id: 45d19dd
Summary: It adds an issue type, `BUFFER_OVERRUN_U5`, for alarms involving unknown values, i.e., when the trace set includes an unknown function call.
Reviewed By: mbouaziz
Differential Revision: D7178841
fbshipit-source-id: bfe857b
Summary:
At the moment, Java and Clang sources/sinks live in the same inferconfig entry.
If we try to parse a Java procedure that happens to be an invalid Clang qualified name (e.g., `MyClass.<init>`),
parsing will crash.
As a temporary fix, throw an exception and catch it instead.
In the future, we can avoid this by requiring that JSON source/sink specifications to indicate the language.
Reviewed By: mbouaziz
Differential Revision: D7291880
fbshipit-source-id: f8f4502
Summary:
Aggregate initialization (e.g., `S s{1, 2}`) doesn't invoke a contructor.
Our frontend translates aggregation initialization as assigning to each field in the struct.
To avoid the appearance of the struct being uninitialized, count any assignment to a field of an aggregate struct as initializing the struct.
Reviewed By: jeremydubreil
Differential Revision: D7189671
fbshipit-source-id: ace02fc
Summary: It corrects a precision bug in the interval domain, with adding some test cases.
Reviewed By: mbouaziz
Differential Revision: D7230918
fbshipit-source-id: 3ec641a
Summary:
:
Previously, we did not have information about type of `exp` in `sizeof exp` from clang plugin which led to `Bad_footprint` errors. Infer did not understand `sizeof *p` in `struct Person* p = malloc(sizeof *p);` and used some default type.
This resulted in `Bad_footprint` error when trying to assign to a field `age` in `p->age=42;`.
This diff uses the version of clang plugin which exports the appropriate type information.
update-submodule: facebook-clang-plugins
Reviewed By: dulmarod
Differential Revision: D7179870
fbshipit-source-id: 4104f10
Summary:
Show some `SymAssign`s (corresponding to parameters) in the trace.
Depends on D7194448
Reviewed By: skcho
Differential Revision: D7194479
fbshipit-source-id: 0deff6c
Summary: It corrects a bug that `&(x.f[n])` was evaluated to `&(x.f[0])`.
Reviewed By: mbouaziz
Differential Revision: D7179620
fbshipit-source-id: 04cbaa7
Summary: It simply resizes the target structure instead of allocating new heap memories and copying values.
Reviewed By: mbouaziz
Differential Revision: D7179353
fbshipit-source-id: 9c20f64
Summary: If a `Closure` expression `e` captures variable `x`, consider `e` as borrowing from `x`. When the closure is invoked via `operator()`, check that the borrow is still valid.
Reviewed By: jeremydubreil
Differential Revision: D7071839
fbshipit-source-id: d923a6a
Summary: It avoids that locations of array fields are evaluated to the `unknown` location incorrectly by addressing the case in the `eval_lindex` function.
Reviewed By: mbouaziz
Differential Revision: D7152736
fbshipit-source-id: 2dc825e
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: 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:
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:
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:
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 `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:
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:
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:
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:
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:
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:
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:
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: 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:
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:
- Combine two fields from ProcAttributes.t into a single field `method_kind` with more information
- New field details whether the procedure is an `OBJC_INSTANCE`, `CPP_INSTANCE`, `OBJ_CLASS`, `CPP_CLASS`, `BLOCK`, or `C_FUNCTION`
- `is_objc_instance_method` and `is_cpp_instance_method` fields no longer necessary
- Changed `is_instance` field in CMethod_signature to `method_kind` field of type ProcAttributes.method_kind
Reviewed By: dulmarod
Differential Revision: D6884402
fbshipit-source-id: 4b916c3
Summary:
The boolean lock domain is simple and surprisingly effective.
But it's starting to cause false positives in the case where locks are nested.
Releasing the inner lock also releases the outer lock.
This diff introduces a new locks domain: a map of locks (access paths) to a bounded count representing an underapproximation of the number of times the lock has been acquired.
For now, we just use a single dummy access path to represent all locks (and thus a count actually would have been sufficiently expressive; we don't need the map yet).
But I'm planning to remove this limitation in a follow-up by refactoring the lock models to give us an access path.
Knowing the names of locks could be useful for error messages and suggesting fixes.
Reviewed By: jberdine
Differential Revision: D6182006
fbshipit-source-id: 6624971
Summary:
Previously, we could understand than an access was safe either because it was possibly owned or protected by a thread/lock, but not both. If an access was both protected by a lock and rooted in a paramer (i.e., possibly owned), we would forget the ownership part of the precondition and remember only the lock bit. This leads to false positives in cases where an access protected by a lock is owned, but another unowned access to the same memory is not protected by a lock (see the new `unownedLockedWriteOk` E2E test for an example).
This diff makes access safety conditions disjunctive so we can simultaneously track whether an access is owned and whether an access is protected by a thread/lock. This will fix false positives like the one explained in T24015160.
Reviewed By: jberdine
Differential Revision: D6671489
fbshipit-source-id: d17715f
Summary:
We already knew not to warn when non-resource `Closeable`'s like `ByteArrayOutputStream` weren't closed, but we still warned on their subtypes.
This diff fixes that problem by checking subclasses in the frontend.
This also removes the need for Java source code models of non-resource types, so I removed them.
Reviewed By: jeremydubreil
Differential Revision: D6843413
fbshipit-source-id: 60fe7fb
Summary: The heuristics to determine the end of a block/procedure was too brittle, the new one ignores non significant instructions.
Reviewed By: jvillard
Differential Revision: D6845380
fbshipit-source-id: feab557
Summary:
This diff fixes the translation of `new` and `placement new` with one argument. If `placement new` has more than one argument it means that it is user-defined (this will be addressed in another diff).
update-submodule: facebook-clang-plugins
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6807751
fbshipit-source-id: 7cf0290
Summary: This should allow to report several occurences of the an issue appearing several times within the same method.
Reviewed By: jvillard
Differential Revision: D6783298
fbshipit-source-id: 5555906
Summary:
This lets us fix the limitation of reporting false positives when a `private` function calls `build()` on a parameter without passing all of the required props.
We will now report such issues in the caller only if it fails to pass the required props.
An unfortunate consequence of this change is that we lose track of where the actual call to `build` occurs--we now report on the declaration of the caller function rather than on the call site of `build`.
I'll work on addressing that in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D6764153
fbshipit-source-id: 3b173e5
Summary:
The captured variables of a closure are tuples (id, var, typ) with the implicit assumption
that &var -> id holds in the heap. This is true when the closure is created, but is not enforce otherwise.
This becomes a problem when the closure is stored in the heap, goes passed a bi-abduction, and then it's executed
(see new test). This was failing before this diff and now succeeds.
We add the verification of this constraint to the normalization of sigma.
At the moment I expect Precondition_not_met to be removed, but also later, we will be able to compute retain cycles
over the closures, as the correct captured variable info is kept through the execution.
Reviewed By: jvillard
Differential Revision: D6796525
fbshipit-source-id: a8a7655
Summary:
Not sure what an "iCFG" is but the dotty is only about CFGs anyway.
Diff obtained by mass-`sed`.
Reviewed By: sblackshear
Differential Revision: D6324280
fbshipit-source-id: b7603bb
Summary: At each call to `Component$Builder.build()`, checks that the required props for `Component` have been set via prior calls to the `Builder`. Does not yet handle `Prop(optional = true)`, but will address that in a follow-up.
Reviewed By: jeremydubreil
Differential Revision: D6735524
fbshipit-source-id: 0c812fd
Summary:
Previously imports with relative filenames would not get resolved so the result
would depend on where infer had been run from. Usually this was the project
root. Now, resolve path names of imports relative to the file doing the
`#IMPORT`. This changes behaviour most of the time.
Reviewed By: dulmarod
Differential Revision: D6784740
fbshipit-source-id: 4ccb7bf
Summary:
This changes the syntax for AL imports from `#IMPORT <file>` to `#IMPORT
"file"`. As a side-effect, the `file` part is now lex'd more permissively too.
Reviewed By: dulmarod
Differential Revision: D6784669
fbshipit-source-id: cc1bb73
Summary:
In Java, static variables are distinguished by package/class:
the file where they are defined doesn't matter.
Fixes#831.
Closes https://github.com/facebook/infer/pull/833
Reviewed By: jeremydubreil
Differential Revision: D6661240
Pulled By: sblackshear
fbshipit-source-id: beeb2f9
Summary:
Some commands (mostly `infer report`) would attempt to run the initialisation
code of infer from the default results directory instead of the one used by the
test. This is mostly harmless because we do not actually use anything from the
directory (typically, we pass `--from-json-results foo.json` and only foo.json
matters). However, this can trip the initialisation code, eg on db schema
changes.
Reviewed By: mbouaziz
Differential Revision: D6711641
fbshipit-source-id: f04b4c7
Summary: Previously we had a single sanitizer kind for escaping, but this isn't quite right. A function that escapes a URL doesn't necessarily make a string safe to execute in SQL, for example.
Reviewed By: the-st0rm
Differential Revision: D6656376
fbshipit-source-id: 572944e
Summary: The checker should only propagate the nullablility on the lhs when of pointer type.
Reviewed By: sblackshear
Differential Revision: D6630294
fbshipit-source-id: 07fe3d6
Summary: This subdirectory was only containing tests related to nullable on Objective C.
Reviewed By: sblackshear
Differential Revision: D6657654
fbshipit-source-id: 11003f2
Summary:
Model for `folly::split` that handles the representation in the cpp model.
Depends on D6544992
Reviewed By: jvillard
Differential Revision: D6545006
fbshipit-source-id: 2b7a139
Summary:
Before this diff, the nullable checker would not be able to find annotations involving methods annotated in the protocols
update-submodule: facebook-clang-plugins
Reviewed By: sblackshear
Differential Revision: D6534893
fbshipit-source-id: 39bd3dd
Summary: This is to allow the bi-abduction analysis and the nullable checker for Clang languages to run together without stepping on each other toes.
Reviewed By: sblackshear
Differential Revision: D6567934
fbshipit-source-id: a318c33
Summary: There was a back and forth conversion between `string` and `IssueType.t` which was not necessary.
Reviewed By: sblackshear
Differential Revision: D6562747
fbshipit-source-id: 70b57a2
Sungkeun Cho
Jeremy Dubreil
Daiva Naudziuniene
Dulma Churchill
Nikos Gorogiannis
Sam Blackshear
Ezgi Çiçek
Dino Distefano
Mehdi Bouaziz
Tony Hu
Jérémie Marguerie
Jules Villard
Varun Arora
Radu Grigore