Summary:
All tests were redirecting `stderr` into duplicates.txt which made it much harder to see other error messages in stderr (such as uncaught exceptions).
To mitigate it, write duplicates to separate file and don't redirect `stderr` to another file.
Reviewed By: jvillard
Differential Revision: D4728938
fbshipit-source-id: 8ad2fc8
Summary:
One limitation of Eradicate is that certain nullability patterns are not expressible using simply the `Nullable` annotation.
One such pattern is using the knowledge that a function returns null when passed null, but returns an object otherwise.
The annotation `PropagatesNullable` is a variant of `Nullable` applied to parameters when their value propagates to the return value.
A method annotated
```
B m(PropagatesNullable A x) { return x == null ? x : B(x); }
```
indicates that `m` returns null if `x` is null, or an object of class `B` if the argument is not null.
Examples with multiple parameters are in the test cases.
This diff builds some infrastructure for annotation transformers: the example above represents the identity function on nullability annotations.
Reviewed By: jvillard
Differential Revision: D4705938
fbshipit-source-id: 9f6194e
Summary:
Before, `trace_of_pname` only grabbed unprotected writes from the summary, so the traces ending in an unprotected read were truncated.
We now look at reads too when appropriate.
Reviewed By: peterogithub
Differential Revision: D4719740
fbshipit-source-id: 28f6e63
Summary: Now, running `infer -a checkers -- ...` will also run the ThreadSafety checker
Reviewed By: sblackshear
Differential Revision: D4691330
fbshipit-source-id: 04fc781
Summary: Run all the checkers one after each other, which allows the Infer AI framework to run several checkers together, including the possibility for them to collaborate.
Reviewed By: sblackshear
Differential Revision: D4621838
fbshipit-source-id: e264d67
Summary:
This makes sure that one can run `./build-infer.sh` then `make`. Otherwise it's
not always clear what one should do to recompile infer, eg when `make` will
work and when `./build-infer.sh` should be used instead, in particular when the
user doesn't have opam configured for her terminal.
Reviewed By: jberdine
Differential Revision: D4698159
fbshipit-source-id: 5df8059
Summary:
We were including hex of empty string if mangled name was not empty (so for all C++ functions).
Instead, include hex of a source file only if it's not empty
Reviewed By: mbouaziz
Differential Revision: D4705388
fbshipit-source-id: 55b6587
Summary:
Procnames files are now reversed qualifier lists with `#` as separator (instead of `::` which needs to be escaped in bash).
Because of the mechanism that is used to obtain qualifiers, it also affects naming for ObjC classes.
Examples:
```
std::unique_ptr<int>::get -> get#unique_ptr<int>#std#__MANGLED,...__ // C++ method
folly::split -> split#folly#__MANGLED,..._ // function within namespace
NSNumber numberWithBool: -> numberWithBool:#NSNumber#class // ObjC method
```
Reviewed By: jvillard
Differential Revision: D4689701
fbshipit-source-id: c3acfc6
Summary:
We want to stop supporting '-multiletter' options altogether in the future as
they are not standard.
For boolean switches, we used to have '-short' for true and '-nshort' for
false, but that second form is necessarily > 1 letters, which doesn't work in
this scheme. Replace these by '-s' for true and '-S' for false.
Reviewed By: jberdine
Differential Revision: D4674079
fbshipit-source-id: 95bacfe
Summary:
When both an unprotected write and a read/write race emanate from the same line,
undoubtedly because of interprocedurality, strip the read/write report (for now).
Perhaps report the info in more succinct form later, but keep to one report/line.
Reviewed By: sblackshear
Differential Revision: D4685102
fbshipit-source-id: 291cf20
Summary:
There was a bug where we allowed ourselves to project local variables from the callee summary into an access path in the caller.
We should only be able to project callee variables that are in the footprint.
Reviewed By: jeremydubreil
Differential Revision: D4684868
fbshipit-source-id: 53a2b9d
Summary:
Updated version of the plugin exports some missing `VarDecls`. To make sure it doesn't break again,
add a test that didn't work before.
Reviewed By: dulmarod
Differential Revision: D4674123
fbshipit-source-id: 0c1677a
Summary:
Eradicate detects circular field initializations (e.g. a field initialized with itself)
by checking in the typestate at the end of the constructor whether the origin
of the field is a field name in the current class.
This has the problem that the following initialization pattern is not recognized as correct:
C(C x) { this.field = x.field }
To fix the issue, the origin information for field accesses x.f is extended
with the origin information of the inner object x.
Circularities are detected if the origin of x is "this".
Reviewed By: jberdine
Differential Revision: D4672472
fbshipit-source-id: 9277bdd
Summary: Previously, we wouldn't report races where the write was under synchronization.
Reviewed By: peterogithub
Differential Revision: D4658850
fbshipit-source-id: e9f4c41
Summary: I encountered cases where the class name part of the method name was passed as `(None, "package.Class")` instead of `("package", "Class")` and therefore incorrectly failing some inequality checks
Reviewed By: sblackshear
Differential Revision: D4662617
fbshipit-source-id: 98ee3e3
Summary:
Stop multiple reports per line happening. These come about
because of interprocedural access to multiple fields. Present one trace,
and summary information about other accesses.
Reviewed By: sblackshear
Differential Revision: D4636232
fbshipit-source-id: 9039fea
Summary:
All intermediate `.exp` files used for tests can be generated with custom info, based on what is needed for the tests purposes.
This customisation happens via command-line argument `--issues-fields`.
Reviewed By: cristianoc, jvillard
Differential Revision: D4628062
fbshipit-source-id: feaa382
Summary:
- The package declaration was wrong
- There was a leftover copy-pasted resource leak test from `CursorLeak.java`.
Reviewed By: sblackshear
Differential Revision: D4612687
fbshipit-source-id: 42c1a35
Summary: Rather than having three separate annotations related to checking/assuming thread-safety, let's just have one annotation instead.
Reviewed By: peterogithub
Differential Revision: D4605258
fbshipit-source-id: 17c935b
Summary: distinguish writes via method calls (e.g., add) from writes via assignment in the error messages
Reviewed By: sblackshear
Differential Revision: D4611748
fbshipit-source-id: 7594d3b
Summary: Report at most one read/write race or unprotected write per access path per method
Reviewed By: sblackshear, jvillard
Differential Revision: D4590815
fbshipit-source-id: 3c3a9d9
Summary:
To address a common source of false positives observed in D4494901.
We don't do anything with `release` yet, but can model it as releasing ownership in the future if we want to enforce correct usage of `SynchronizedPool`'s.
Reviewed By: peterogithub
Differential Revision: D4593635
fbshipit-source-id: 621e937
Summary: Reports on reads that have one or more conflicting writes. When you report, say which other methods race with it.
Reviewed By: sblackshear
Differential Revision: D4538793
fbshipit-source-id: 47ce700
Summary: Thread-local variables can't be shared between threads, so it's safe to mutate them outside of synchronization
Reviewed By: jeremydubreil
Differential Revision: D4568316
fbshipit-source-id: 0634cad
Summary:
Enrich the domain of SIOF to contain, as well as the globals needed by a
procedure, the globals that the procedure initializes. Also add the possibility
to model some procedures as initializing some variables. Use that mechanism to
teach the checker about `std::ios_base::Init`.
Reviewed By: mbouaziz
Differential Revision: D4588284
fbshipit-source-id: d72fc87
Summary:
This gives a way for users to flag safe methods regarding SIOF, for instance if
the problematic paths in the method cannot happen before `main()` has started.
Reviewed By: akotulski
Differential Revision: D4578700
fbshipit-source-id: 6542dcf
Summary:
I couldn't figure out why, but from within an infer release the traces we get
for this test are different than the expected ones. This is even consistent
across osx and linux.
In order to restore sanity, let's just hide this incomprehensible fact. Let's
come back to it if more tests exhibit this, maybe traces are not guaranteed to
be exactly the same across runs.
Reviewed By: sblackshear
Differential Revision: D4559405
fbshipit-source-id: dd88c59
Summary: Should stop us from reporting on benign races of fields that are caching resources.
Reviewed By: peterogithub
Differential Revision: D4538037
fbshipit-source-id: 15236b4
Summary: This annotation can then be used to suppress the warnings on non-android Java projects.
Reviewed By: sblackshear
Differential Revision: D4544858
fbshipit-source-id: 8a0b8fa
Summary:
The Java models for resources are way to complex. The main issue I am facing with these models is that small changes in the analysis can affect the generation of the models in some weird ways. For instance, I get different specs for some of the models between my devserver and my devvm, which seems to be mostly related with the backend treatment of `instanceof`.
The objective here is to simplify the models as much as possible in order to:
1) make debugging regressions easier
2) get simpler specs and less modeled methods shipped in `models.jar`
Reviewed By: sblackshear
Differential Revision: D4536115
fbshipit-source-id: 577183a
Summary: Better documentation, and could perhaps be checked instead of trusted later if the analysis understands threads better.
Reviewed By: jaegs
Differential Revision: D4537463
fbshipit-source-id: 4323c78
Summary: In some cases where a function is called directly on a formal (e.g, `def foo(o) { callSomething(o) }`, we were failing to propagate the footprint trace to the caller.
Reviewed By: jeremydubreil
Differential Revision: D4502404
fbshipit-source-id: d4d632f
Summary: This case was already working but there was no tests for it
Reviewed By: sblackshear
Differential Revision: D4529473
fbshipit-source-id: ca3ff02
Summary: This will be important for maintaining ownership of `View`'s, which involve a lot of casting.
Reviewed By: peterogithub
Differential Revision: D4520441
fbshipit-source-id: fdef226
Summary:
Previously, we would lose track of ownership in code like
```
Obj owned = new Obj();
Obj stillOwned = id(owned); // would lose ownership here
stillOwned.f = ... // would report false alarm here
```
This diff partially addresses the problem by adding a notion of "unconditional" (always owned) or "conditional" (owned if some formal at index i is owned) ownership.
Now we can handle simple examples like the one above.
I say "partially" because we still can't handle cases where there are different reasons for conditional ownership, such as
```
oneOrTwo(Obj o1, Obj o2) { if (*) return o1; else return o2; } // we won't understand that this maintains ownership if both formals are owned
Obj stillOwned = oneOrTwo(owned1, owned2);
stillOwned.f = ... // we'll report a false alarm here
```
This can be addressed in the future, but will require slightly more work
Reviewed By: peterogithub
Differential Revision: D4520069
fbshipit-source-id: 99c7418
Summary: This fixes a wrong level of indirection when performing the type substitution.
Reviewed By: sblackshear
Differential Revision: D4521008
fbshipit-source-id: 7324ea6
Summary:
This fixes false positives we had in fields written by callees of a constructor (see new E2E test).
This is also a bit cleaner than what we did before; instead of special-casing constructors, we just use the existing ownership concept.
Reviewed By: peterogithub
Differential Revision: D4505161
fbshipit-source-id: a739ebc
Summary:
Constants are always "owned" in the sense that no one can mutate them.
In code like
```
Obj getX(boolean b) {
if (b) {
return null;
}
return new Obj();
}
```
, we need to understand this in order to infer that the returned value is owned.
This should fix a few FP's that I've seen.
Reviewed By: peterogithub
Differential Revision: D4485452
fbshipit-source-id: beae15b
Summary:
Infer used to report null dereference when field was accessed later:
```
vector<int> v;
int& a = v[0]; // should be EMPTY_VECTOR_ACCESS here, but it wasn't reported
int b = a; // was NULL_DEREFERENCE here
```
To avoid this problem, model all accesses to vector as dereference of its internal `beginPtr` field.
Reviewed By: jberdine
Differential Revision: D4481942
fbshipit-source-id: 2142894
Summary: This should fix the issue with broken invariants when the method specialization on pointer ends up doing a substitution on non pointer types
Reviewed By: sblackshear
Differential Revision: D4487232
fbshipit-source-id: f3fce84
Summary: The method `junit.framework.TestCase.setUp()` is always run before the other methods by the JUnit testing framework. So the method act as a class initializer.
Reviewed By: sblackshear
Differential Revision: D4487371
fbshipit-source-id: 1998801
Summary: Just adding some more test cases on how Infer handles dynamic dispatch.
Reviewed By: jberdine
Differential Revision: D4486529
fbshipit-source-id: d90ef42
Summary:
This modifies `CTrans_utils.dereference_value_from_result` function. Reasons:
1. Type in Sil.Load tuple is supposed to be the type of Ident.t field (result), not Exp.t (source)
2. Inside `dereference_value_from_result` we used wrong type when `~strip_pointer:true` - it used original type instead of the resulting one
3. Fixing (2), uncovered similar issue in `CTrans_utils.cast_operation` - it should have used resulting type, not original one
Changed tests are expected:
1. `deprecated_hack.cpp` test was how I discovered this issue (it was very wrong)
2. the other test also had issues, now it's correct
Sadly, there was no logic I followed when writing this change - I stuffed changes in a way that fits, but it may be breaking something somewhere else.
Reviewed By: jberdine
Differential Revision: D4481895
fbshipit-source-id: b139c59
Summary:
This diff adds a set of access paths holding a value returned from a method annotated with Functional to the domain.
If a "functional" value is written to a field, we won't count that right as an unprotected access.
The idea is to be able to use the Functional annotation to get rid of benign race false positive, such as:
```
Functional T iAlwaysReturnTheSameThing();
T mCache;
T memoizedGetter() {
if (mCache == null) {
mCache = iAlwaysReturnTheSameThing();
}
return mCache;
}
```
Although there is a write-write race on `mCache`, we don't care because it will be assigned to the same value regardless of which writer wins.
Reviewed By: peterogithub
Differential Revision: D4476492
fbshipit-source-id: cfa5dfc
Summary:
We warn on unsafe accesses to fields that occur in a public method (or are reachable from a public method).
We ought not to consider VisibleForTesting methods as public, since they are only public for testing purposes.
Reviewed By: peterogithub
Differential Revision: D4477648
fbshipit-source-id: 5f58914
Summary: Simple model for List methods that write to the collection.
Reviewed By: peterogithub
Differential Revision: D4453381
fbshipit-source-id: 19edc51
Summary:
Sometimes some instructions were never part of any CFG node and were not written to CFG at all. Add a mechanism that will create node and add them to CFG when they reach compoundStmt translation.
This is step forward to make `*x;` instruction actualy dereference x (it works in C already in C++ AST looks different though)
Reviewed By: dulmarod
Differential Revision: D4469139
fbshipit-source-id: b03b11c
Mehdi Bouaziz
Jeremy Dubreil
Andrzej Kotulski
Sam Blackshear
Martino Luca
Dulma Churchill
Peter O'Hearn
Cristiano Calcagno
Dino Distefano
Jules Villard
Kihong Heo