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:
The infer results directories in buck-out/ are "cleaned up" to avoid polluting
the Buck cache with too much data or non-deterministic data. In particular, the
runstate is deleted, which confused subsequent infer processes trying to read
the pre-existing results directory.
Add a special case in infer to delete pre-existing results directories in
buck-out instead of trying to load their state.
Reviewed By: mbouaziz
Differential Revision: D6845128
fbshipit-source-id: 5c716aa
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:
Record the db schema, infer version, and run dates into
infer-out/.infer_runstate.json. This allows us to check on startup whether the
results directory was generated using a compatible version of infer or not, and
give a better error message in the latter case than some SQLite error about
mismatching tables.
This will be used in a follow-up diff to record capture phases too, and avoid
relying on filesystem timestamps of the infer-out/capture/foo/ directories for
reactive analysis.
Had to change some tests Makefiles to make sure they do not attempt to re-use
stale infer-out directories, which would now fail the run.
The stale infer-out directory gets deleted if `--force-delete-results-dir` is
passed (but a warning still gets printed).
Reviewed By: mbouaziz
Differential Revision: D6760787
fbshipit-source-id: f36f7df
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
Summary: As Dulma pointed out, adding or removing paramters in a method in Objective C is changing the name of the method. Such changes should not make pre-exisiting issues reported as introduced. This diff is to prevent this by only keeping in the bug hash the part of the name that is before the first colon.
Reviewed By: dulmarod
Differential Revision: D6491215
fbshipit-source-id: 3c00fae
Summary:
Our model of unique_ptr and shared_ptr relied on the fact that we could C-style cast a pointer to the internal pointer type used in the smart pointer.
This is wrong when the smart pointer is used with a custom deleter that declares its own pointer type whose is not constructible from just a single pointer.
Reviewed By: dulmarod
Differential Revision: D6496203
fbshipit-source-id: 1305137
Summary: Local `CKComponentScope`'s are often created purely for their side effects, so it's fine for them to be unread.
Reviewed By: jeremydubreil
Differential Revision: D6475475
fbshipit-source-id: 17e869a
Summary: This would allow the checker to detect indirect nullable violations, i.e. violations that are involving intermediate method calls on potentially `nil` values.
Reviewed By: sblackshear
Differential Revision: D6464900
fbshipit-source-id: 3663729
Summary: NSDictionary initialization will crash when using `nil` as a key or as a value
Reviewed By: dulmarod
Differential Revision: D6466349
fbshipit-source-id: 57bb012
Summary: This will avoid collisions when the inner classes are implementing the same methods. For example, the previous version of the bug hash could conflate the issues when several annonymous inner classes are implementing the same method, e.g. a annonymous subclass of `Runnable` implementing `run()`.
Reviewed By: sblackshear
Differential Revision: D6461594
fbshipit-source-id: 2bb8545
Summary:
Simpler bug hash that is more independent of the underlying analysis. This now computes the hash based on:
- the bug type.
- the base filename: i.e for my/source/File.java, just keep File.java. So the hash will not change when moving files around.
- the simple method name: i.e. without package information and list of parameters. So changing the list of parameters will not affect the bug hash.
- the error message were the line numbers have been removed. So moving code or reformatting will not affect the hash.
Reviewed By: jberdine
Differential Revision: D6445639
fbshipit-source-id: 82e3cbe
Summary: To avoid false positives, we treat `operator[]` in cpp as container read. Moreover, if a container `c` is owned, we make all accesses `c[i]` to be also owned.
Reviewed By: sblackshear
Differential Revision: D6396574
fbshipit-source-id: 94aabff
Summary:
It seems that the abstraction instructions were not previously added the the CFG.
This is a functional changes to make sure that the abstraction state is always added. We can simplify the code later and just run this step before storing the CFG instead of after loading them.
Reviewed By: sblackshear, jvillard
Differential Revision: D6383672
fbshipit-source-id: cedcb8a
Summary:
As da319 points out, we did not handle this case correctly before. There were a few reasons why:
(1) An assignment like `struct S s = mk_s()` gets translated as `tmp = mk_s(); S(&s, tmp)`, so we didn't see the write to `s`.
(2) We counted uses of variables in destructors and dummy `_ = *s` assignments as reads, which meant that any struct values were considered as live.
This diff fixes these limitations so we can report on dead stores of struct values.
Reviewed By: da319
Differential Revision: D6327564
fbshipit-source-id: 2ead4be
Summary:
The diff is very big but it's mostly removing code. It was inspired by the fact that we were getting Dead Store FPs because we were modeling some functions from CoreFoundation and CoreGraphics directly as alloc in the frontend, which caused the parameters of the function to be seen as dead. See the new test.
To deal with this, if we are going to skip the function, we model it as malloc instead. Given how many models we had for those "model as malloc" functions, I removed them to rely solely on the new mechanism.
The modeling of malloc and release was still based on the old retain count implementation, even though all we do here is a malloc/free kind of analysis. I also changed
that to be actually malloc/free which removed many Assert false in the tests. CFRelease is not exactly free though, and it's possible to use the variable afterwards. So used a custom free builtin that only cares about removing the Memory attribute and focuses on minimizing Memory Leaks FPs.
Otherwise we were translating CFBridgingRelease as a special cast, and this wasn't working. To simplify this as well, I removed all the code for the special cast, and just modeled CFBridgingRelease and CFAutorelease also as free_cf, to avoid Memory Leak false positives. I also treated the cast __bridge_transfer as a free_cf model. This means we stopped trying to report Memory Leaks on those objects.
The modeling of CoreGraph release functions was done in the frontend, but seemed simpler to also simplify that code and model all the relevant functions.
Reviewed By: sblackshear
Differential Revision: D6397150
fbshipit-source-id: b1dc636
Summary:
- Plug model checkers
- Add alloc size safety condition on alloc of negative, zero or big size
Reviewed By: sblackshear
Differential Revision: D6375144
fbshipit-source-id: bbea6f3
Summary: This option was for compatibility with the command line options of the previous, but is no longer used. This diff removes the option and the deprecated code.
Reviewed By: sblackshear, mbouaziz
Differential Revision: D6351097
fbshipit-source-id: 0e4cfc5
Summary: Adding a null key or a null value will cause a runtime exception.
Reviewed By: sblackshear
Differential Revision: D6378618
fbshipit-source-id: 8bd27c6
Summary:
This resolves#796 . Effectively it adds file specific suffix to name of all global initializers (so initializersof two global variable of the same name will have unique Typ.Procname). which is the same rule as currently used by constructing Procname for the static functions. However this change applies to initializers of all global variables and not just static (arguably it's a right thing. since GCC used to allow multiple global variables with the same name).
Consequences of this change that it becomes impossible to know name of generated initialization function of global ('extern') variables. However get_initializer_pname function is only referenced by the frontend (when creating initializer for the defined global variables) and by the SIOF checker.
Closes https://github.com/facebook/infer/pull/801
Reviewed By: jvillard
Differential Revision: D6335034
Pulled By: dulmarod
fbshipit-source-id: 1a92c08
Summary: Adding a nil object to an NSArray will crash. Adding this case to the checker.
Reviewed By: sblackshear
Differential Revision: D6346241
fbshipit-source-id: 3fe6f20
Summary: The clang compiler introduces a materialized temporary expression which should be treated similarly to the Infer internal temporary variables.
Reviewed By: sblackshear
Differential Revision: D6331237
fbshipit-source-id: 81d8196
Summary:
We would previously skip any function that had one of these.
A no-op translation is sufficient to fix this issue (see new E2E test).
Reviewed By: mbouaziz
Differential Revision: D6317323
fbshipit-source-id: 0855bd8
Summary: Just changing ClangTrace to actually look at the different sanitizer kinds.
Reviewed By: jeremydubreil
Differential Revision: D6325086
fbshipit-source-id: 5da236d
Summary: In a thread safety report we used the access path from the final sink. This diffs change the report to include the expanded access path from the initial sink.
Reviewed By: sblackshear
Differential Revision: D6297848
fbshipit-source-id: 2386063
Summary:
This diff adds a new way of executing blocks when they are passed as parameters to a method. So far we just skipped the block in this case.
Now we can execute it. Let's demonstrate with an example. Say we have
//foo has a block parameter that it executes in its body
foo (Block block) { block();}
// bar calls foo with a concrete block
bar() {
foo (^(){
self->x = 10;
});
};
Now, when we call the method foo with a concrete block, we create a copy of foo instantiated with the concrete block, which in itself is translated as a method with a made-up name.
The copy of foo will get a name that is foo extended with the name of the block parameter, the call to the block parameter will be replaced to a call to the concrete block, and the captured variables
of the concrete block (self in this case), will be added to the formals of the specialized method foo_block_name.
This is turned on at the moment for ObjC methods with ObjC blocks as parameters, and called with concrete blocks. Later on we can extend it to other types of methods, and to C++ lambdas, that are handled similarly to blocks.
Another extension is to check when the block has been called with nil instead of an actual block, and raise an error in that case.
After this diff, we can also model various methods and functions from the standard library that take blocks as parameters, and remove frontend hacks to deal with that.
Reviewed By: ddino
Differential Revision: D6260792
fbshipit-source-id: 0b6f22e
Summary: The checker should not report unitinialzed values on the throw branch.
Reviewed By: ddino
Differential Revision: D6267019
fbshipit-source-id: 05768f1
Summary: We were conflating reads/writes with container reads/writes that created false positives.
Reviewed By: sblackshear
Differential Revision: D6232768
fbshipit-source-id: 39159cb
Summary: This is a hack to removes most of the false positives of this checker in Objective C.
Reviewed By: sblackshear
Differential Revision: D6239914
fbshipit-source-id: 1cf05de
Summary:
This confuses the SIOF checker and causes false positives. This dummy deref is
generated for constructors of classes that are modeled as being pointer types
instead of the actual class in infer, typically for smart pointers. I do not
understand how this works.
The biabduction also analyses this code, so might now get confused itself.
Reviewed By: jberdine
Differential Revision: D6221817
fbshipit-source-id: 050c5a9
Summary:
The issue is with classes defining static data members:
```
$ cat foo.h
struct A {
static int foo;
};
$ cat foo.cpp
#include "foo.h"
int A::foo = 12;
int f() { return A::foo; // should see A::foo as defined in this translation unit
$ cat bar.cpp
#include "foo.h"
void g() { return A::foo; // should see A::foo defined externally
```
Previously, both foo.cpp and bar.cpp would see `A::foo` as defined within their
translation unit, because it comes from the header. This is wrong, and static
data members should be treated as extern unless they're defined in the same
file.
This doesn't change much except for frontend tests. SIOF FP fix in the next diff.
update-submodule: facebook-clang-plugins
Reviewed By: da319
Differential Revision: D6221744
fbshipit-source-id: bef88fd
Summary: This only works for Java at the moment but we can re-organise the code later to add the Objective C equivalent of these assertion methods.
Reviewed By: mbouaziz
Differential Revision: D6230588
fbshipit-source-id: 46ee98e
Summary: The checker should not report nullable violations on repeated calls
Reviewed By: sblackshear
Differential Revision: D6195471
fbshipit-source-id: 16ff76d
Summary: The Java bytecode does not contain information about the location of abstract of interface methods. Before this diff, the analysis trace was tuncated and the file where the abstract or interface method was not included in the trace, which makes it harder to understand the Infer report, especially when the method is on a generated file that is not checked in the repository.
Reviewed By: sblackshear
Differential Revision: D6223612
fbshipit-source-id: c80c6f2
Summary: More general version of the fix in D6138749. This diff moves RacerD's lock modeling into a separate module and uses the module in the HIL translation to check when a function has lock/unlock semantics.
Reviewed By: jberdine, da319
Differential Revision: D6191886
fbshipit-source-id: 6e1fdc3
Summary: Functions that do not belong to a class or a struct are translated to c-style functions even in the context of cpp. We need to add ownership to locals for c-style functions too.
Reviewed By: sblackshear
Differential Revision: D6196882
fbshipit-source-id: 715f129
Summary:
vector::data returns a pointer to the first value of the vector.
- The size of the (array) pointer should be the same with the vector.
- The pointer should point to the same abstract value with the vector.
Reviewed By: mbouaziz
Differential Revision: D6196592
fbshipit-source-id: cc17096
Summary: `std::unique_lock` constructor allows to create a unique lock without locking the mutex. `std::unique_lock::try_lock` returns true if mutex has been acquired successfully, and false otherwise. It could be that an exception is being thrown while trying to acquire mutex, which is not modeled.
Reviewed By: jberdine
Differential Revision: D6185568
fbshipit-source-id: 192bf10
Summary:
Code often uses std::unique_lock::owns_lock to test if a deferred lock
using the 2-arg std::unique_lock constructor actually acquired the
lock.
Reviewed By: sblackshear
Differential Revision: D6181631
fbshipit-source-id: 11e9df2
Summary:
Use a distinct issue type for the Java and C++ concurrency analyses,
as the properties they are checking are significantly different.
Reviewed By: sblackshear
Differential Revision: D6151682
fbshipit-source-id: 00e00eb
Summary:
In a summary, you never want to see a trace where non-footprint sources flow to a sink.
Such a trace is useless because nothing the caller does can make more data flow into that sink.
Reviewed By: jeremydubreil
Differential Revision: D5779983
fbshipit-source-id: d06778a
Summary:
Due to limitations in our Buck integration, the thread-safety analysis cannot create a trace that bottoms out in a Buck target that is not a direct dependency of the current target.
These truncated traces are confusing and tough to act on.
Until we can address these limitations, let's avoid reporting on truncated traces.
Reviewed By: jeremydubreil
Differential Revision: D5969840
fbshipit-source-id: 877b9de
Summary:
:
Make both buck capture and compilation database handle buck command line arguments and invoke buck query the same way.
Plus allow:
- target patterns `//some/dir:` and `//some/dir/...`. However since `//some/dir:#flavor` and `//some/dir/...#flavor` are not supported, they need to be expanded before adding the infer flavor.
- target aliases (defined in `.buckconfig`)
- shortcuts `//some/dir` rewritten to `//some/dir:dir`
- relative path `some/dir:name` rewritten to `//some/dir:name`
Reviewed By: jvillard
Differential Revision: D5321087
fbshipit-source-id: 48876d4
Summary:
If you write
```
boolean readUnderLockOk() {
synchronized (mLock) {
return mField;
}
}
```
it will be turned into
```
lock()
irvar0 = mField
unlock()
return irvar0
```
in the bytecode. Since HIL eliminates reads/writes to temporaries, it will make the above code appear to perform a read of `mField` outside of the lock.
This diff fixes the problem by forcing HIL to perform all pending reads/writes before you exit a critical section.
Reviewed By: jberdine
Differential Revision: D6138749
fbshipit-source-id: e8ad9a0
Summary: In HIL, allow deref'ing a magic address like `0xdeadbeef` for debugging purposes. Previously, we would crash on code like this.
Reviewed By: mbouaziz
Differential Revision: D6143802
fbshipit-source-id: 4151924
Summary: This check is deprecated and will be replaced by a dedicated checker to detect unitialized values.
Reviewed By: mbouaziz
Differential Revision: D6133108
fbshipit-source-id: 1c0e9ac
Summary: Previously, this would incorrectly classify types like `map<std::string, int>` as a buffer
Reviewed By: mbouaziz
Differential Revision: D6125530
fbshipit-source-id: c8564de
Summary:
This is in the spec for clang compilation databases.
Also improves error messages when we fail to parse the compilation database.
closes#771
Reviewed By: dulmarod
Differential Revision: D6123832
fbshipit-source-id: 070f70f
Summary: In preparation for making `-a checkers` the default (when no analyzer is specified), let's test `-a checkers` by default.
Reviewed By: mbouaziz
Differential Revision: D6051177
fbshipit-source-id: d8ef611
Summary:
Refactor `RegisterCheckers` to give a record type to checkers instead of a tuple type.
Print active checkers with their per-language information.
Improve the manual entries slightly.
Reviewed By: sblackshear
Differential Revision: D6051167
fbshipit-source-id: 90bcb61
Summary:
Whenever we see a use of a lock, infer that the current method can run in a multithreaded context. But only report when there's a write under a lock that can be read or written without synchronization elsewhere.
For now, we only infer this based on the direct usage of a lock; we don't assume a caller runs in a multithreaded context just because its (transitive) callee can.
We can work on that trickier case later, and we can work on smarter inference that takes reads under sync into account. But for now, warning on unprotected writes of reads that occur under sync appears to be too noisy.
Reviewed By: jberdine
Differential Revision: D5918801
fbshipit-source-id: 2450cf2
Summary: This commit adds unsigned symbol for preciser analysis results with less number of uses of min/max operators.
Reviewed By: mbouaziz
Differential Revision: D6040437
fbshipit-source-id: 999ca4c
Summary:
This was a crutch from the days before ownership analysis.
We shouldn't need it anymore, and it was actually causing FP's because we were skipping analysis of `ImmutableList.builder()` and not understanding that the return value is owned.
Reviewed By: jeremydubreil
Differential Revision: D6035631
fbshipit-source-id: afa0ade
Summary:
This generates `--resource-leak-only` automatically, and make the other
checkers' `-only` option work as expected with respect to `--resource-leak` too
(eg, `--resource-leak --biabduction-only` disables resource leak).
Reviewed By: jeremydubreil
Differential Revision: D6051134
fbshipit-source-id: 2d4a2ba
Summary:
1. Mark some Makefile targets as depending on `MAKEFILE_LIST` so they get rebuilt on Makefile changes
2. Do not show boolean options with no documentation in the man pages (like we do for other option types).
3. Default to Lazy dynamic dispatch for the checkers.
4. In the tests, use `--<checker>-only` instead of relying on `--no-default-checkers`
5. `--no-filtering` is redundant if `--debug-exceptions` is passed
Reviewed By: jeremydubreil
Differential Revision: D6030578
fbshipit-source-id: 3320f0a
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: 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:
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:
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:
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
Sam Blackshear
Dulma Churchill
Mehdi Bouaziz
Jules Villard
Daiva Naudziuniene
Jeremy Dubreil
Tony Hu
Radu Grigore
Dino Distefano
Peter O'Hearn
Sungkeun Cho
Vivek Dhiman
Dominic Cooney
Josh Berdine
Anders Papitto
Kyriakos Nikolaos Gkorogiannis