Summary:
- Use Logging for logging
- Add a few extra debug (not ON by default)
- No space before colon
Depends on D4961957
Reviewed By: KihongHeo
Differential Revision: D4961989
fbshipit-source-id: 7c8697d
Summary: The purpose of the annotation reachability analysis is to report when a method annotated with `X` never calls, directly or indirectly, another method annotated with `Y`. However, there can be different call stacks following different execution paths from `X` to `Y`. Reporting more than one call stack ending with the same annotated procedure does not bring more signal to the end user. So the purpose of this diff is to avoid those duplicated reports and report at most one annotation reachability issue per end of call stack.
Reviewed By: sblackshear
Differential Revision: D4942765
fbshipit-source-id: 46325a7
Summary:
- Bottom-lift abstract memory domain to express unreachable node
- Two cases to make a node unreachable
+ constant: when an evaluation result of condition expression is
bottom or false, e.g., "prune(0)".
+ alias: when the same structure e is compared to itself with "<",
">", and "!=", e.g., "prune(e < e)".
- Add test for the new prune (prune_constant.c, prune_alias.c)
- Debug the semantics of comparison
Reviewed By: mbouaziz
Differential Revision: D4938055
fbshipit-source-id: d0fadf0
Summary:
As an interprocedural checker, SIOF should not run unless explicitly required.
Make it a new type of analyzer like other similar checkers.
Reviewed By: mbouaziz
Differential Revision: D4937820
fbshipit-source-id: a9e2d38
Summary: `bufferoverrun` is not part of `checkers` yet so bufferoverrun tests require their own Makefile
Reviewed By: jvillard
Differential Revision: D4937558
fbshipit-source-id: 20380f1
Summary: Sawja assigns them on multiple control-flow paths, so they're not SSA.
Reviewed By: peterogithub
Differential Revision: D4896745
fbshipit-source-id: c805216
Summary:
There are false positives in the current analysis due to the
use of conjunction in the treatment of threaded. Changing conjunction to disjunction
removes these false positives. Some new false negatives arise, but all the old tests pass.
This is a stopgap towards a better solution being planned.
Reviewed By: sblackshear
Differential Revision: D4883280
fbshipit-source-id: c2a7e6e
Summary: The flakiness is exercised by upgrading the OCaml compiler to 4.04.0.
Reviewed By: jberdine
Differential Revision: D4859904
fbshipit-source-id: 0dd7ff6
Summary:
If we couldn't project the callee access path into the caller during summary application, we still added the corresponding trace to the caller state.
This was wasteful; it just bloats the caller with state it will never look at.
Fixed it by making `get_caller_ap_node` return `None` when the state won't be visible in the caller.
Reviewed By: jeremydubreil
Differential Revision: D4727937
fbshipit-source-id: 87665e9
Summary: This should make the reports much easier to understand. We can generalize to reporting a stack trace for all of the writes in the future if we wish.
Reviewed By: peterogithub
Differential Revision: D4845641
fbshipit-source-id: 589fdbc
Summary:
Make it possible to write one model which will be used by all template instantiations.
There is one big missing piece: infer never tries to do template instantiation by itself. With current code, it's possible to use generic models
as long as header contains `__infer_generic_model` annotation (see the test as an example).
This is not viable to modify all headers with this annotation hence infer will try to do template instantiation for generic models in later diffs.
Reviewed By: jberdine
Differential Revision: D4826365
fbshipit-source-id: 2233e42
Summary: If two public methods touch the same state and only one is marked `ThreadSafe`, it's reasonable to report unsafe accesses on both of them.
Reviewed By: peterogithub
Differential Revision: D4785038
fbshipit-source-id: 5a80da4
Summary: `__attribute__((annotate("")))` is better way of passing information to the frontend
Reviewed By: jberdine
Differential Revision: D4818805
fbshipit-source-id: 6e8add2
Summary:
*Unless* the unprotected write runs on the main thread and the read doesn't.
Otherwise, we'll already report on the unprotected write, and we don't want to duplicate.
Reviewed By: peterogithub
Differential Revision: D4798357
fbshipit-source-id: 5de06a0
Summary:
This is step further simplify the code to avoid cases where the summary of the procedure being analyzed can exist in two different versions:
# one version is the summary passed as parameter to every checker
# the other is a copy of the summary in the in-memory specs table
This diff implements:
# the analysis always run through the `Ondemand` module (was already the case before)
# the summary of the procedure being analyzed is created at the beginning of the on-demand analysis call
# all the checkers run in sequence, update their respective part of the payload and log errors to the error table
# the summary is store at the end of the on-demand analysis call
Reviewed By: sblackshear
Differential Revision: D4787414
fbshipit-source-id: 2d115c9
Summary:
Adds a new type and branching for a missing path of execution.
closes#575
Reviewed By: jvillard
Differential Revision: D4738681
fbshipit-source-id: f72344c
Summary:
It can be useful when debugging infer or the Makefiles themselves to see what
`make` is doing. Instead of editing Makefiles to remove `@` now you can `make
VERBOSE=1`.
This is just `git ls-files | grep -e Makefile -e '.*\.make' | xargs sed -e 's/^\t@/\t$(QUIET)/' -i`, and adding the definition of `QUIET` to Makefile.config.
Reviewed By: jeremydubreil
Differential Revision: D4779115
fbshipit-source-id: e6e4642
Summary:
No new functionality here; mostly `FN_` tests documenting our current limitations.
Will start chipping away at the false negatives in follow-up diffs.
Reviewed By: peterogithub
Differential Revision: D4780013
fbshipit-source-id: 7a0c821
Summary: Bringing the logic back to where it was before the big refactoring of the reporting logic.
Reviewed By: peterogithub
Differential Revision: D4774541
fbshipit-source-id: afeaaf8
Summary:
Move all of the reporting on top of the aggregation functionality.
This lets us delete lots of code
Reviewed By: peterogithub
Differential Revision: D4772223
fbshipit-source-id: 47cc51a
Summary:
This was the one type of races we were not yet reporting (besides ones that use the wrong synchronization :)).
Wrote new utility function to aggregate all accesses by the memory they access.
This makes it easy to say which accesses we should report and what their conflicts are.
Eventually, we can simplify the reporting of other kinds of unsafe accesses using this structure.
Reviewed By: peterogithub
Differential Revision: D4770542
fbshipit-source-id: 96d948e
Summary:
For collections whose type does not express that the collection is thread-safe (e.g., `Collections.syncrhonizedMap` and friends).
If you annotate a field holding one of these collections, we won't warn when you mutate the collection.
Reviewed By: jeremydubreil
Differential Revision: D4763565
fbshipit-source-id: 58b487a
Summary: It seems that we were not really using the `Bottom` part of the domain as a pair of (empty call map, empty tracking var map) was already acting as bottom.
Reviewed By: sblackshear
Differential Revision: D4759757
fbshipit-source-id: 53dedfe
Summary:
Most of our tests work by comparing the output of some command to a baseline
expected output. It's often needed to update that baseline.
Previously, that was crudely done by attempting to move every foo.exp.test file
to foo.exp. This does not work terribly well, in particular because
foo.exp.test might be stale.
Instead, add a `replace` target to every test that knows how to update the
baseline. This allows custom behaviours too, eg in the differential tests.
Most of the tests include base.make or differential.make, so add a replace target
there. A few tests are completely custom, add a replace target to them too.
Reviewed By: jeremydubreil
Differential Revision: D4754279
fbshipit-source-id: ec34273
Summary:
This issue was spotted in the wild. There may be more of those, unfortunately it's hard to predict
More general problem is that types in infer frontend diverge from clang's types for DerivedToBase cast.
Then, infer uses types from clang anyway and that confuses backend. Getting it always right is very hard
Reviewed By: jvillard
Differential Revision: D4754081
fbshipit-source-id: 5fb7069
Summary:
If I read off the main thread and write on the main we
could have a race. (Writes off main are already reported.)
Reviewed By: sblackshear
Differential Revision: D4746138
fbshipit-source-id: 8b6e9c5
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
Summary:
Previously, we would correctly be silent on code like `x = new T(); x.f = ...`, but would wrongly warn on code like `x = makeT(); x.f = ...`.
The reason is that we only allowed ownership through direct allocation.
This diff adds a boolean that specifies whether the return value is owned as part of the summary.
This allows us to correctly handle many common cases of (transitively) returning a freshly allocated object, but still won't work for understanding that ownership is maintained in examples like
`x = new T(); y = id(x); y.f = ...`.
Reviewed By: jvillard
Differential Revision: D4456864
fbshipit-source-id: b5eec02
Summary:
Eradicate currently considers a field initialized if it's simply accessed (not written to),
or initialized with another initialized field.
This fixes the issue.
Reviewed By: jvillard
Differential Revision: D4449541
fbshipit-source-id: 06265a8
Summary:
If we have code like
```
o.setF(source())
sink(o)
```
and `setF` is an unknown method, we probably want to report.
Reviewed By: jeremydubreil, mburman
Differential Revision: D4438896
fbshipit-source-id: 5edd204
Summary:
In code like
```
foo(o) {
iWriteToF(o)
}
```
, the condtional write to `f` in `iWriteToF` should become a conditional write for `foo`.
Reviewed By: peterogithub
Differential Revision: D4429160
fbshipit-source-id: f111ac4
Summary:
In code like
```
foo() {
Object local = new Object();
iWriteToAField(local);
}
```
, we don't want to warn because the object pointed to by `local` is owned by the caller, then ownership is transferred to the callee.
This diff supports this by introducing a notion of "conditional" and "unconditional" writes.
Conditional writes are writes that are rooted in a formal of the current procedure, and they are safe only if the actual bound to that formal is owned at the call site (as in the `foo` example above).
Unconditional writes are rooted in a local, and they are only safe if a lock is held in the caller.
Reviewed By: peterogithub
Differential Revision: D4429131
fbshipit-source-id: 2c6112b
Summary:
Races on volatile fields are less concerning than races on non-volatile fields because at least the read/write won't result in garbage.
For now, let's de-prioritize these writes by ignoring them.
Reviewed By: peterogithub
Differential Revision: D4434023
fbshipit-source-id: 05043ba
Summary:
Also make sure we don't introduce deprecated options in our repo, eg when
calling infer from infer.
Reviewed By: jeremydubreil
Differential Revision: D4430379
fbshipit-source-id: 77ea7fd
Summary: Just cleanup; gives us slightly less test code to maintain.
Reviewed By: jeremydubreil
Differential Revision: D4429265
fbshipit-source-id: d43c308
Summary:
Similar to marking classes ThreadConfined, we want to support marking fields as well.
The intended semantics are: don't warn on writes to the marked field outside of syncrhonization, but continue to warn on accesses to subfields.
Reviewed By: peterogithub
Differential Revision: D4406890
fbshipit-source-id: af8a114
Summary: Generalized the CppTrace into a Clang trace because we don't currently have separate checkers for Obj-C and Cpp. Happy to separate them later if there is a good reason
Reviewed By: akotulski
Differential Revision: D4394952
fbshipit-source-id: e288761
Summary:
Adding models that allow us to warn on unguarded accesses to subclasses of `Map`, but not on accesses of threadsafe containers like `ConcurrentMap`.
Lots more containers to model later, but stopping at `Map`s for now to make sure the approach looks ok.
Reviewed By: jvillard
Differential Revision: D4385306
fbshipit-source-id: d791eee
Summary: Need to upgrade in order to specify some taint properties on a more recent `WebView` API.
Reviewed By: cristianoc
Differential Revision: D4382590
fbshipit-source-id: 0925742
Summary: These methods should only be called from other methods that also run on the UI thread, and they should not be starting new threads.
Reviewed By: peterogithub
Differential Revision: D4383133
fbshipit-source-id: 6cb2e40
Summary: Use the lazy dynamic dispatch by default in prod for the Java analysis
Reviewed By: sblackshear
Differential Revision: D4356872
fbshipit-source-id: 491e92e
Summary:
Without this it's not always obvious which test fails. It also makes it easier
to mass-patch test failures from the CI jobs to replace expected outputs with
actual outputs (eg, when debugging osx frontend tests from linux).
Reviewed By: jberdine
Differential Revision: D4352205
fbshipit-source-id: 8887d7b
Summary:
We currently can only model the return values of functions as sources.
In order to model inputs of endpoints as sources, we need the capability to treat the formals of certain functions as sources too.
This diff adds that capability by adding a function for getting the tainted sources to the source module, then using that info in the analysis.
Reviewed By: jeremydubreil
Differential Revision: D4314738
fbshipit-source-id: dd7d423
Summary: Access to std::vector shouldn't be treated as SKIP. Implementation is simple enough to use one from std:: headers
Reviewed By: jvillard
Differential Revision: D4339577
fbshipit-source-id: d1fbbee
Summary:
Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces.
This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary.
One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible.
Under the old summary system, we would do it at most once for each "function" in the summary list.
Now, we'll do it at most once for each node in the access tree summary.
This will be a smaller number of calls, since each node can summarize many input/output relationships.
Reviewed By: jeremydubreil
Differential Revision: D4271579
fbshipit-source-id: 34e407a
Summary: Don't warn on NotThreadSafe class, particularly when super is ThreadSafe
Reviewed By: sblackshear
Differential Revision: D4334417
fbshipit-source-id: 0df3b9d
Summary:
SuppressWarnings annotations are hardly used and add considerable
complexity due to requiring recompilation with an annotation processor.
Reviewed By: jvillard
Differential Revision: D4312193
fbshipit-source-id: c4fc07e
Summary:
Change the domain of SIOF to be based on sets of pvar * location instead of
single pvars. This allows us to group several accesses together. However, we
still get different trace elems for different instructions in a proc. We do two
things to get around this limitation and get a trace where all accesses within
the same proc are grouped together, instead of one trace for each access:
1. A post-processing phase at the end of the analysis of one proc collects all
the globals directly accessed in the proc into a single trace elem.
2. When creating the error trace, unpack this set into several trace elements
to see each access (at its correct location) separately in the trace.
This is a bit hacky and another way would be to extend the API of traces to
handle in-procedure accesses natively instead of shoe-horning them. However
since SIOF is the only one to use this, it introduces less boilerplate to do it
that way for now.
Also, a few .mlis for good measure.
Reviewed By: sblackshear
Differential Revision: D4299070
fbshipit-source-id: 3bbb5c2
Summary: These direct tests were still mostly relying on PHONY targets.
Reviewed By: jberdine
Differential Revision: D4326469
fbshipit-source-id: 37b2d0a
Summary:
If these collections don't encapsulate their state properly, there are bigger problems than thread safety issues :).
Plus, these warnings are less-than-actionable for non-Guava maintainers.
Reviewed By: peterogithub
Differential Revision: D4324277
fbshipit-source-id: cacfbf0
Summary:
Maintain an "ownership" set of access paths that hold locally allocated memory that has not escaped.
This memory is owned by the current procedure, so modifying it outside of synchronization is safe.
If an owned access path does escape to another procedure, we remove it from the ownership set.
Reviewed By: peterogithub
Differential Revision: D4320034
fbshipit-source-id: 64f9169
Summary:
In particular, the method for retrieving an element from the array, this should never be nil. Also added a model for count
similar to the one for NSString length.
Reviewed By: ddino
Differential Revision: D4306655
fbshipit-source-id: 0ecb25a
Summary: Our C++ model magic didn't work when instantiating smart pointers with volatile types. Fix it
Reviewed By: jvillard
Differential Revision: D4313271
fbshipit-source-id: 55ffb98
Summary: Rename the intermediate .exp.test files to .exp.test.noreplace so that they don't match the regexp used by `make test-replace`. Otherwise they can accidentally become .exp files that will show up in `git status`.
Reviewed By: cristianoc
Differential Revision: D4319436
fbshipit-source-id: df2ef21
Summary:
Before the diff, the code was considering as Nullable any annotation ending with `...Nullable`, including `SuppressParameterNotNullable`.
Closes#533
Reviewed By: jberdine
Differential Revision: D4317356
fbshipit-source-id: 6091c0f
Summary: Adding Buck `DEFS` macros for generating Infer genrules. The generated genrules can be used to run the analysis on any existing `java_library` targets.
Reviewed By: sblackshear
Differential Revision: D4291234
fbshipit-source-id: 6430e2e
Summary:
The Java frontend translates exceptions by assigning them to the return value.
This leads to weird behavior when the return type of the function is void.
Already handled one case of this in Quandary (ignoring assignments of exceptions to return value), but was missing the case where null is assigned to the return value.
The frontend does this to "clear" the value of previously assigned exceptions.
Reviewed By: jeremydubreil
Differential Revision: D4294060
fbshipit-source-id: 6bef5ef
Summary: Globals that are constexpr-initializable do not participate in SIOF.
Reviewed By: sblackshear
Differential Revision: D4277216
fbshipit-source-id: fd601c8
Summary:
Although the Builder pattern is not actually thread-safe, Builder's are not expected to be shared between threads.
Handle this by ignoring all unprotected accesses in classes the end with "Builder".
We might be able to soften this heuristic in the future by ensuring rather than assuming that Builder are not shared between methods (or, ideally, between threads).
Reviewed By: peterogithub
Differential Revision: D4280761
fbshipit-source-id: a4e6738
Summary:
When calling function g_realloc(gpointer mem,gsize n_bytes) one of the spec considers the case
whereby n_bytes is zero. In that case g_realloc would return null.
If we call with sizeof(int), infer would compare sizeof(int) with zero. But the prover would fail to
understand that sizeof(int) != 0.
This diff fix this. We try to convert expression to constant when they can be converted (eg in case of sizeof).
The method currently make a partial set of conversion. This could be extended.
Reviewed By: jberdine
Differential Revision: D4166944
fbshipit-source-id: 3ec4fd7
Summary:
Remember which globals are static locals.
It's useful to distinguish those from global variables in objc and in the SIOF
checker. Previously in ObjC we would accomplish that by looking at the name of
the variable, but that wouldn't work reliably in C++. Keep the old method around for
now as the way we deal with static locals in ObjC needs some fixing.
Reviewed By: akotulski
Differential Revision: D4198993
fbshipit-source-id: 357dd11
Summary: This should no work even when Infer is not setup in the PATH
Reviewed By: jvillard
Differential Revision: D4262356
fbshipit-source-id: e3fa779
Summary: `ReentrantReadWriteLock.ReadLock` and `ReentrantReadWriteLock.WriteLock` are commonly used lock types that were not previously modeled.
Reviewed By: peterogithub
Differential Revision: D4262032
fbshipit-source-id: 4ff81a7
Summary:
`o.<init>` cannot be called in parallel with other methods of `o` from outside, so it's less likely to have thread safety violations in `o.<init>`.
This diff suppresses reporting of thread safety violations for fields touched (transitively) by a constructor.
We can do better than this in the future (t14842325).
Reviewed By: peterogithub
Differential Revision: D4259719
fbshipit-source-id: 20db71f
Summary: Originially, there was a missing package declaration meaning that the generated class was ending in a different place. I also added a test for equality of Integer to complement the test of no equality, which could be always true.
Reviewed By: sblackshear
Differential Revision: D4263676
fbshipit-source-id: 86ab0d3
Summary:
We only ought to report a source-sink flow at the call site where the sink is introduced.
Otherwise, we will report silly false positives.
Reviewed By: jeremydubreil
Differential Revision: D4234766
fbshipit-source-id: 118051f
Summary: This should make it easier to understand complex error reports.
Reviewed By: peterogithub
Differential Revision: D4254341
fbshipit-source-id: fb32d73
Summary: We'll eventually want fancy interprocedural traces. This diff adds the required boilerplate for this and adds the line number of each access to the error message. Real traces will come in a follow-up
Reviewed By: peterogithub
Differential Revision: D4251985
fbshipit-source-id: c9d9823
Summary: Adding this so we can test interprocedural trace-based reporting in a subsequent diff.
Reviewed By: peterogithub
Differential Revision: D4243046
fbshipit-source-id: 7d07f20
Summary: We're at risk for some silly false positives without these models.
Reviewed By: peterogithub
Differential Revision: D4244795
fbshipit-source-id: b0367e6
Summary:
Currently cfg nodes are written into dot files in whatever order they
appear in a hash table. This seems unnecessarily sensitive, so this
diff sorts the nodes.
Reviewed By: dulmarod
Differential Revision: D4232377
fbshipit-source-id: a907cc6
Summary: Add some basic command line API to run Infer using Buck genrules. Remains to fix issues with absolute vs relative paths and to see how to create these genrules on the fly for a given java or android library.
Reviewed By: sblackshear
Differential Revision: D4245622
fbshipit-source-id: 1cda4ee
Summary:
Dealing with symbolic links in project root is tricky. To avoid it, always normalize all paths to sources with `realpath`.
Changes to tests are expected - infer started to resolve symbolic links which screws up with our testing mechanism.
Reviewed By: jberdine
Differential Revision: D4237587
fbshipit-source-id: fe1cb01
Summary:
Before, we were using a set domain of strings to model a boolean domain.
An explicit boolean domain makes it a bit clear what's going on.
There are two things to note here:
(1) This actually changed the semantics from the old set domain. The set domain wouldn't warn if the lock is held on only one side of a branch, which isn't what we want.
(2) We can't actually test this because the modeling for `Lock.lock()` etc doesn't work :(.
The reason is that the models (which do things like adding attributes for `Lock.lock`) are analyzed for Infer, but not for the checkers.
We'll have to add separate models for thread safety.
Reviewed By: peterogithub
Differential Revision: D4242487
fbshipit-source-id: 9fc599d
Summary:
In Java, we handle unknown code by propagating behavior from the parameters of the unknown function call to the return value (or constructed object, in the case of a constructor). But we do this in a somewhat silly way--generating a new summary with these semantics at each unknown call site. Instead, this diff introduces these two options as predefined behaviors and adds specialized code for them.
As a side effect of this approach, unknown functions are no longer counted as passthroughs. This is ok; the original behavior was less of a reasoned decision and more of an unintended consequence of the way we decided to handle unknown code.
This new approach ought to be more efficient than the old one, and as a virtuous side effect it will be easier to specify how to handle unknown code in other languages like C++.
Reviewed By: jeremydubreil
Differential Revision: D4205624
fbshipit-source-id: bf97445
Summary: Run all java tests with project-root at `infer/tests`. Do it to keep things consistent between clang and java tests
Reviewed By: sblackshear
Differential Revision: D4233236
fbshipit-source-id: c3f24fd
Summary:
Run all clang tests with project-root at `infer/tests`. I need it because we'll start resolving symbolic links
soon and some tests would lead outside of project root which means we'd start seeing absolute paths in recorded tests.
Diff that does same thing for java tests: D4233236
Reviewed By: jberdine
Differential Revision: D4233194
fbshipit-source-id: c261a2b
Summary:
Let's introduce some concepts. A "known unknown" function is one for which no Java code exists (e.g., `native`, `abstract`, and `interface methods`). An "unknown unknown" function is one for which Java code may or may not exist, but we don't have the code or we choose not to analyze it (e.g., non-modeled methods from the core Java or Android libraries).
Previously, Quandary handled both known unknowns and unknown unknowns by propagating taint from the parameters of the unknown function to its return value. It turns out that it is really expensive to do this for known unknown functions. D4142697 was the diff that starting handling known unknown functions in this way, and bisecting shows that it was the start of the recent performance problems for Quandary.
This diff essentially reverts D4142697 by handling known unknowns as skips instead. Pragmatically, doing the propagation trick for Java/Android library functions (e.g., `String` functions!) matters much more, so i'm not too worried about the missed behaviors from this. Ideally, we will go back to the old handling once performance has improved (have lots of ideas there). But I need this to unblock me in the meantime.
Reviewed By: jeremydubreil
Differential Revision: D4205507
fbshipit-source-id: 79cb9c8
Summary:
Developers will sometimes write GuardedBy("T.f") with the intended semantics: "guarded by the field f of the object with type T in the current state".
We want to support this to avoid false positives.
Reviewed By: peterogithub
Differential Revision: D4197476
fbshipit-source-id: acd00d9
Summary:
The way interfaces are dealt with led to a false positive,
where tryLock() works OK for a Lock but not for a ReentrantLock.
The solution is just to provide the model.
While I am at it I am adding some more standard tests for Lock and ReentrantLock, which were not present.
Reviewed By: sblackshear
Differential Revision: D4204551
fbshipit-source-id: 9b6de28
Summary: These are dangerous if you are trying to compare a type to a string, and they're also unsightly.
Reviewed By: jvillard
Differential Revision: D4189956
fbshipit-source-id: 14ce127
Summary:
SIOF is only for interactions between objects of non-POD types. Previously the
checker was also reporting for POD types.
Reviewed By: akotulski
Differential Revision: D4197620
fbshipit-source-id: 7c56571
Summary:
Record an abstraction of the bug traces in the tests. The abstraction of a
trace is the sequence of descriptions. In practice, descriptions are either
empty, or of the form "start/end/return from/call to procedure X". They seem
pretty stable.
Motivation: there is nothing testing the traces reported by Infer right now,
even though they are surfaced to developers. For instance, Quandary uses
--issues-txt instead of --issues-tests to make sure the traces do not regress.
This change would make this approach more widespread.
Reviewed By: sblackshear
Differential Revision: D4159597
fbshipit-source-id: 9c83952
Summary:
`make` doesn't delay variable evaluation in targets' dependencies, so
`$(OBJECTS)` was always empty. Including clang.make after having defined
`OBJECTS` fixes it.
Reviewed By: jberdine
Differential Revision: D4159522
fbshipit-source-id: 6925f8a
Mehdi Bouaziz
Jeremy Dubreil
Sam Blackshear
Sungkeun Cho
Jules Villard
Kihong Heo
Peter O'Hearn
Dino Distefano
Andrzej Kotulski
Paco Estevez Garcia
Martino Luca
Dulma Churchill
Cristiano Calcagno
Kihong Heo
Josh Berdine
Ryan Rhee