Summary: We will then be able to merge the tests for the other checkers without affecting these lab tests
Reviewed By: jvillard
Differential Revision: D6039433
fbshipit-source-id: e575ce9
Summary:
Another step toward running the biabduction analysis as a checker.
Depends on D6038210
Reviewed By: jvillard
Differential Revision: D6038682
fbshipit-source-id: fed45bf
Summary:
The previous version of the code was trying to lookup from disk the procedure description of the procedure to analyze, which was in fact already loaded in memory.
This diff fixes one of the issues preventing the bi-abduction to run as a checker when using the lazy dynamic dispatch algorithm.
Reviewed By: sblackshear
Differential Revision: D6038210
fbshipit-source-id: 10a98ee
Summary:
9c7fc65 introduced a large performance regression, this diff eliminates it and a bit more.
Instead of constructing the quotiented access list map in a two-step process of first constructing a map of all accesses and then quotienting it, the quotiented map is constructed directly by using a coarser comparison function on keys. Partitioning the access map O(number of access paths) times, using an apparently expensive partition predicate, seems to be causing trouble based on rough profile data.
Reviewed By: da319
Differential Revision: D6005262
fbshipit-source-id: 077846c
Summary: Stack-allocated variables cannot be raced on in cpp as every thread has its own stack. At the beginning of the analysis we add ownership to the local variables.
Reviewed By: jberdine
Differential Revision: D6020506
fbshipit-source-id: 0a90a97
Summary: Now that we report write-write races involving more than one write, we need to improve the traces accordingly.
Reviewed By: jberdine
Differential Revision: D6026845
fbshipit-source-id: b1366dd
Summary:
This is to avoid getting BUSY from sqlite when the machine is busy (not
necessarily busy because of infer).
Reviewed By: jberdine
Differential Revision: D6020022
fbshipit-source-id: ca0f913
Summary:
Next step to issue deduplication: do not keep safety conditions that are subsumed by others.
Only do it if they do not have infinite bound: replacing `0 < size` by `1 < size` is ok, but replacing it by `+oo < size` is not because it looks much more like a lack of precision.
Reviewed By: skcho
Differential Revision: D5978455
fbshipit-source-id: acc2384
Summary:
A specific type of alias is added for the vector::empty() result and it is used at pruning.
Now, there are two types of aliases:
- "simple" alias: x=y
- "empty" alias: x=v.empty() and y=v.size
So, if x!=0, y is pruned by (y=0). Otherwise, i.e., x==0, y is pruned by (y>=1).
Reviewed By: mbouaziz
Differential Revision: D6004968
fbshipit-source-id: bb8d50d
Summary:
`pp_instr_list` was not tailrec causing a stack overflow on big code.
Also simplified a few things
Reviewed By: jvillard
Differential Revision: D5995451
fbshipit-source-id: 40a4911
Summary: The may alias analysis relation that the thread safety analysis uses is very specific to Java and causes many false alarms for C++ code. This diff disables it when analyzing C++ code. Improving it to avoid false negatives is left for later.
Reviewed By: sblackshear
Differential Revision: D5974182
fbshipit-source-id: 9c7fc65
Summary:
The analyzer currently does not understand the control flow of
Singletons, which leads to false alarms. This diff is an unsound hack
that simply ignores any read or write accesses made when computing the
value of a singleton.
Reviewed By: sblackshear
Differential Revision: D5979639
fbshipit-source-id: 34caecb
Summary:
Model folly::SharedMutex lock and unlock operations, some
apache::thrift::concurrency::ReadWriteMutex operations, some
folly::RWSpinLock operations, and folly::MicroSpinLock operations.
Reviewed By: sblackshear
Differential Revision: D5974225
fbshipit-source-id: 19e2816
Summary:
The biabduction backend can raise exceptions that will be caught when triggered
from within the biabduction backend itself (eg, `analyze_procedure` called from
Symexec as a result of an ondemand analysis, because Symexec will catch these),
but not caught when called as the result of an ondemand analysis emanating from
another analyzer (eg ThreadSafety).
Make the biabduction more self-contained by wrapping the analysis of a
procedure inside a `try/with` with similar properties as the one of Symexec.
Reviewed By: jeremydubreil
Differential Revision: D5986335
fbshipit-source-id: 36a5d32
Summary:
Attempting to translate these will not go well as the declaration still depends
on some template arguments. Added a test that was previously crashing the
frontend.
Also extend the catching of "Unimplemented" and other errors to `translate_one_decl` as it was useful to debug this issue. In particular, reraise all exceptions and log some additional context when doing so.
update-submodule: facebook-clang-plugins
Reviewed By: mbouaziz
Differential Revision: D5976357
fbshipit-source-id: fca8e38
Summary:
Previously, annotating something ThreadSafe meant "check that it is safe to run all of this procedure's methods in parallel with each other" (including self-parallelization).
This makes sense, but it means that if the user writes no annotations, we do no checking.
I'm moving toward a model of inferring when an access might happen on a thread that can run concurrently with other threads, then automatically checking that it is thread-safe w.r.t to all other accesses to the same memory (on or off the current thread thread).
This will let us report even when there are no `ThreadSafe` annotations.
Any method that is known to run on a new thread (e.g., `Runnable.run`) will be modeled as running on a thread that can run in parallel with other threads, and so will any method that is `synchronized` or acquires a lock.
In this setup, adding `ThreadSafe` to a method just means: "assume that the current method can run in parallel with any thread, including another thread that includes a different invocation of the same method (a self race) unless you see evidence to the contrary" (e.g., calling `assertMainThread` or annotating with `UiThread`).
The key step in this diff is changing the threads domain to abstract *what threads the current thread may run in parallel with* rather than *what the current thread* is. This makes things much simpler.
Reviewed By: jberdine
Differential Revision: D5895242
fbshipit-source-id: 2e23d1e
Summary:
Indicate if read or write is protected, and do not print only the
field but also the object involved in the race.
Reviewed By: sblackshear
Differential Revision: D5974250
fbshipit-source-id: 351a576
Summary:
Expanding traces currently works in the following way:
Given a `TraceElem.Kind` `k` we want to report in `foo`, we look for a callee `C` of `foo` that has a `TraceElem.Kind` equal to `k` in its summary, grab the summary for `C`, then repeat until we bottom out.
This isn't very flexible: it insists on equality between `TraceElem.Kind`'s as the criteria for expanding a trace.
This diff introduces a new `matches` function for deciding when to expand a trace from a caller into a callee.
Clients that don't want strict equality can implement a fuzzier kind of equality inside this function.
I've gone ahead and done this for the trace elemes of thread-safety.
In the near future, equivalent access paths won't always compare equal from caller to callee, so we want to match their suffixes instead.
Reviewed By: jvillard
Differential Revision: D5914118
fbshipit-source-id: 233c603
Summary:
Move Inferbo safety conditions to their own file.
Split the old `Condition.t` to a condition together with a trace.
This will ease having: different kind of condition and several traces for the same condition (see following diff)
Reviewed By: jvillard
Differential Revision: D5942030
fbshipit-source-id: d74a612
Summary: Not using this for now, and it seems good to simplify the complex domain as much as we can.
Reviewed By: jberdine
Differential Revision: D5970233
fbshipit-source-id: a451503
Jeremy Dubreil
Sungkeun Cho
Josh Berdine
Daiva Naudziuniene
Sam Blackshear
Dulma Churchill
Jules Villard
Dino Distefano
Mehdi Bouaziz
Kyriakos Nikolaos Gkorogiannis
Martino Luca