Summary:
At one point I thought we'd want to have lots of different schedulers for things like exploring loops in different orders, but that hasn't materialized.
Let's make the common use-case simpler by hiding the `Scheduler` parameter inside the `AbstractInterpreter` module.
We can always expose `MakeWithScheduler` later if we want to.
Reviewed By: jberdine
Differential Revision: D4508095
fbshipit-source-id: 726e051
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:
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:
The thread-safety and annotation reachibility analyses were defining ugly custom versions of override_exists with refs.
Let's give them a canonical, ref-free version instead.
Reviewed By: jberdine
Differential Revision: D4475777
fbshipit-source-id: 0bb45fc
Summary: Simple model for List methods that write to the collection.
Reviewed By: peterogithub
Differential Revision: D4453381
fbshipit-source-id: 19edc51
Summary:
One of the things that confuses me about the current annotations API is that there's a lot of ways to do the same thing.
Some of the concepts like `annotated_signature` are only really needed by Eradicate.
This diff removes usages of `annotated_signature` outside of Eradicate (everyone else was just using `get_annotated_signature` as a roundabout way to get the return annotation of a procedure).
In the future, I'll move `get_annotated_signature` and other Eradicate-specific functionality into its own module inside the Eradicate directory.
Reviewed By: jberdine
Differential Revision: D4472058
fbshipit-source-id: 5bb0846
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:
Remove the remaining uses of polymorphic equality `=`.
In case of basic types, this is replaced by String.equal or Int.equal.
In case of `= []`, this is replaced by `List.is_empty`.
In case of `= None`, this is replaced by `is_none`.
In case of a datatype definition such as `type a = A | B`,
a `compare_a` function is defined by adding `type a = A | B [@deriving compare]`
and a `equal_a` function is defined as `let equal_a = [%compare.equal : a]`.
In case of comparison with a polymorphic variant `= `Yes`, the equality
defined in `PVariant.(=)` is used. Typically, `open! Pvariant` is added
at the beginning of the file to cover all the uses.
Reviewed By: jberdine
Differential Revision: D4456129
fbshipit-source-id: f31c433
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:
If an access path rooted in some parameter `p` is accessed outside of synchronizaton, but `p` is owned by the caller, then we should not warn.
We will implement this by separating writes into "conditional" (safe if a certain parameter is owned by the caller" and "unconditional" (safe only if the caller synchronizes appropriately).
This diff just introduces the map type for conditional writes and changes the transfer functions accordingly.
We'll actually use the map in a follow-up.
Reviewed By: peterogithub
Differential Revision: D4400987
fbshipit-source-id: d2b8af8
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:
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: 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:
A domain should not definite its initial state, since distinct users of the domain may want to choose different initial values.
For example, one user might want to bind all of the formals to some special values, and one user might want the initial domain to be an empty map
This diff makes this distinction clear in the types by (a) requiring the initial state to be passed to the abstract interpreter and (b) lifting the requirement that abstract domains define `initial`.
Reviewed By: jberdine
Differential Revision: D4359629
fbshipit-source-id: cbcee28
Summary: Don't warn on NotThreadSafe class, particularly when super is ThreadSafe
Reviewed By: sblackshear
Differential Revision: D4334417
fbshipit-source-id: 0df3b9d
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: This is required to maintain a set of owned access paths in a subsequent diff.
Reviewed By: jberdine
Differential Revision: D4318859
fbshipit-source-id: bd1a9fa
Summary:
Before, the Interprocedural functor was a bit inflexible. You couldn't do custom postprocessing like normalizing the post state or coverting the post from an astate type to a summary type.
Now, you can do whatever you want by passing a custom `~compute_post` function.
Since `AbstractInterpreter.compute_post` can be used by clients who don't care to do anything custom, this doesn't create too much boilerplate.
Reviewed By: jvillard
Differential Revision: D4309877
fbshipit-source-id: 8d1d85d
Summary: We're about to add another element to the abstract domain, and a 4-tuple is a bit too cumbersome to work with.
Reviewed By: jberdine
Differential Revision: D4315292
fbshipit-source-id: d04699f
Summary:
Utils contains definitions intended to be in the global namespace for
all of the infer code-base, as well as pretty-printing functions, and
assorted utility functions mostly for dealing with files and processes.
This diff changes the module opened into the global namespace to
IStd (Std conflict with extlib), and moves the pretty-printing
definitions from Utils to Pp.
Reviewed By: jvillard
Differential Revision: D4232457
fbshipit-source-id: 1e070e0
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: `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: 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: Noticed this when I was writing the documentation for the abstract interpretation framework and was curious about why `Ondemand.analyze_proc` needs the type environment. It turns out that the type environment is only used to transform/normalize Infer bi-abduction specs before storing them to disk, but this can be done elsewhere. Doing this normalization elsewhere simplifies the on-demand API, which is a win for all of its clients.
Reviewed By: cristianoc
Differential Revision: D4241279
fbshipit-source-id: 957b243
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:
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: Currently the thread safety checker neglects to analyze and files methods we don't want to report on. Like constructors and private methods, and classes where no superclass is marked ThreadSafe. For interprocedural analysis we want to analyze all these to get summaries, even if we don't report on them.
Reviewed By: jberdine
Differential Revision: D4226515
fbshipit-source-id: 7571573
Summary: Refactoring to make thread safety checker interpocedural. This should not change funcitonality, and will only set things up for making the interprocedural part more serious.
Reviewed By: sblackshear
Differential Revision: D4124316
fbshipit-source-id: 6721953
Summary: The thread safety checker is run independently of other analyses, using the command "infer -a threadsafety -- <build-command>".
Reviewed By: sblackshear
Differential Revision: D4148553
fbshipit-source-id: bc7b3f9
Summary:
this makes frontends no longer depend on SymExec.ml. `ModelBuiltins` was split into two modules:
- `BuiltinDecl` with procnames for builtins (used to determine whether some function is a builtin)
- `BuiltinDefn` with implementations used by `SymExec`
- they both have similar type defined in `BUILTINS.S` which makes sure that new builtin gets added into both modules.
During the refactor I ran some scripts:
`BuiltinDecl.ml`:
let X = create_procname "X"
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,$4,"\42"$2"\42"} '
then manually confirm string match. Exceptions:
"__exit" -> "_exit"
"objc_cpp_throw" -> "__infer_objc_cpp_throw"
__objc_dictionary_literal
nsArray_arrayWithObjects
nsArray_arrayWithObjectsCount
`BuiltinDefn.ml`:
let X = Builtin.register BuiltinDecl.X execute_X
cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,"Builtin.register BuiltinDecl."$2,"execute_"$2} '
then, fix all compilation problems
Reviewed By: jberdine
Differential Revision: D3951035
fbshipit-source-id: f059602
Summary:
We issue a thread safety warning on a class not
marked ThreadSafe, when it has a super that is. This makes some sense. But,
it will be nice to remind that a super is so maeked, else the mesg could
seem out of context or surprising
Reviewed By: sblackshear
Differential Revision: D4075145
fbshipit-source-id: ebc2b83
Summary: when a method has writes to a field outside of synchrnoization, issue an appropriate error message identifying the fields
Reviewed By: sblackshear
Differential Revision: D4015612
fbshipit-source-id: 4f697fc
Sam Blackshear
Cristiano Calcagno
Peter O'Hearn
Josh Berdine
Andrzej Kotulski