Summary:
We update the type of captured variables to include information about capture mode (`ByReference` or `ByValue`) both for procdesc attributes and the closure expression.
For lambda: closure expression now contains correct capture mode for capture variables. Procdesc still does not contain information about captured variables which we will address in the next diff.
For objc blocks: at the moment all captured variables have mode `ByReference`. Added TODOs to fix this.
Reviewed By: jvillard
Differential Revision: D22572054
fbshipit-source-id: 4c88678ee
Summary:
As title
Model `NSString` as `JavaString`.
Since `NSArray` does not contain information about its type of element, we do not use associate string with collection as in Java and C++. In Java, String model is implemented using java collection, and for C++, string model is implemented using vector.
So instead, we use existing `JavaString` model.
Reviewed By: skcho
Differential Revision: D22431949
fbshipit-source-id: 7cdde1ad7
Summary: To avoid NULLPTR_DEREFERENCE false positives we want to model some functions as returning non-null. A new flag --pulse-model-return-nonnull allows us to provide a list of such functions.
Reviewed By: ezgicicek
Differential Revision: D22431564
fbshipit-source-id: 9944c7382
Summary: `addAll` adds elements one by one and hence takes linear time. We didn't have a model for this and considered it O(1).
Reviewed By: skcho
Differential Revision: D22375157
fbshipit-source-id: 65b82bfae
Summary: This diff prevents printing line numbers of loop in the trace description, which helps to keep the same descriptions even when the line number of a function is changed in tests.
Reviewed By: ezgicicek
Differential Revision: D22375584
fbshipit-source-id: 676d1a7cc
Summary:
Keyword `thread_local` in cpp allows us to create a variable with thread storage duration, meaning that the object's lifetime begins when the thread begins and ends when the thread ends.
We get `NULLPTR_DEREFERENCE` false positive for `thread_local` variable since we reallocate it in the `VariableLifetimeBegins` metadata instruction and we do not see further updates to the variable. To solve the issue we special case `VariableLifetimeBegins` instruction for global variables.
Reviewed By: jvillard
Differential Revision: D22284135
fbshipit-source-id: 13c14ef90
Summary: Create test for the most common unmodeled function in inferbo that acts as control variable.
Reviewed By: skcho
Differential Revision: D22331168
fbshipit-source-id: 1913682db
Summary: Add objc test for customized class and blocks. Mostly sanity test.
Reviewed By: ezgicicek
Differential Revision: D22043918
fbshipit-source-id: 917deeea7
Summary:
This diff adds a model of `File.listFiles` as returning an array with
a symbolic length.
Reviewed By: ezgicicek
Differential Revision: D22332258
fbshipit-source-id: 6ca593b8b
Summary: This diff adds support for `com.facebook.litho.sections.Section` which mimics the behavior for `com.facebook.litho.Component`.
Reviewed By: skcho
Differential Revision: D22309039
fbshipit-source-id: 3510441a8
Summary:
We already had a heuristic to deal with assignment expressions, but it
relied on the very previous CFG node to have a non-empty list of instrs.
In some cases, however, this previous node is a Join_node with no instrs,
so we need to take one more step back to find what we're looking for.
I've also added a bit more logging around this functionality, so it's
easier to debug/tune in future.
Reviewed By: ngorogiannis
Differential Revision: D22282930
fbshipit-source-id: 024eec145
Summary:
This model is very important in the analysis of ObjC classes because the pattern
```
- (instancetype)init {
if (self = [super init]) {
...
}
return self;
}
```
is very common, so we need to know that if the super class is `NSObject`, the implementation of `init` is returning `self`, otherwise it's a skip function and we don't get the correct spec for the function. We fix some memory leak FP with this model, see test.
Reviewed By: ezgicicek
Differential Revision: D22259281
fbshipit-source-id: 3ee48c827
Summary:
We need to check if `folly::Optional` is not `folly::none` if we want to retrieve the value, otherwise a runtime exception is thrown:
```
folly::Optional<int> foo{folly::none};
return foo.value(); // bad
```
```
folly::Optional<int> foo{folly::none};
if (foo) {
return foo.value(); // ok
}
```
This diff adds a new issue type that reports if we try to access `folly::Optional` value when it is known to be `folly::none`.
Reviewed By: ezgicicek
Differential Revision: D22053352
fbshipit-source-id: 32cb00a99
Summary: This linters were not used much anymore, so we can delete them.
Reviewed By: ngorogiannis
Differential Revision: D22233895
fbshipit-source-id: f31180a05
Summary: There is now a compilation check for UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK so this check is less useful. Also the check REGISTERED_OBSERVER_BEING_DEALLOCATED is useful only in an old version of iOS.
Reviewed By: ngorogiannis
Differential Revision: D22231851
fbshipit-source-id: 72151fef5
Summary:
This diff tries to support a specific form of linked list iteration in Java.
```
while (p != null) {
p = p.getNext();
}
```
This example was a constant cost before because the cost checker could not detect that it is an iteration on a linked list.
The heuristic this diff implemented is:
(1) `p = p.getNext()`: It tries to find this specific form of assignment. Then, it increments `p.linked_list_index` by 1. Note that `linked_list_index` is a virtual field for keeping an index in the linked list. Its initial value is always 0.
(2) At `p != null`, it tries to prune the value of `p.linked_list_index`: the upper-bound of `p.linked_list_index` is pruned by `<= p.linked_list_length`. Here again, `p.linked_list_length` is also a virtual field to denote the length of the linked list.
Reviewed By: ezgicicek
Differential Revision: D22234892
fbshipit-source-id: 2fee176bb
Summary: These models for Memory Leaks have been ported to Pulse, so we can remove the models in biabduction and corresponding tests.
Reviewed By: skcho
Differential Revision: D22206287
fbshipit-source-id: e17499ad3
Summary:
Move the implementation of implicit getters and setters from the biabduction to the clang frontend so these methods are accessible to all the checkers.
*Background*: In Objective-C when properties are created in the interface of a class, the compiler creates automatically the instance variable for it and also the getter and setter in the implementation of the class. In the frontend we collect the information about which method is the implicit getter and setter of which instance variable (we get the method declaration but not the implementation), and here we add the implicit implementation.
Reviewed By: skcho
Differential Revision: D22187238
fbshipit-source-id: 76e0508ed
Summary: Let's make package name match the directory name to follow Java's file lookup conventions
Reviewed By: skcho
Differential Revision: D22183964
fbshipit-source-id: b9958b975
Summary:
Document FP due to imprecision in tracking outer lock release. In a nested `synchronized` block the outer release is not registered by the abstract domain. The reason is that HIL is not resolving what `$bcvarX` is pointing to (in this case to `lockE`).
Reported by Andreea Costea.
Reviewed By: ezgicicek
Differential Revision: D22186240
fbshipit-source-id: 84e5e72b1
Summary:
Nullability of the assignment result is not refined in code snippets
like:
```
while ((a = foo.getA()) != null) {
nonNullableVal = a;
}
```
Let's add a test for this.
Reviewed By: jvillard
Differential Revision: D22136218
fbshipit-source-id: 206c368d6
Summary:
A bug in docusaurus makes relative URLs fail depending on how the page
was accessed, because the URL of a page in docs/ will end in / if
accessed directly or via hyperlink, but that / will be omitted when
clicking on the sidebar. The final / makes all the difference when
interpreting relative URLs so relative URLs are essentially broken.
See https://github.com/facebook/docusaurus/issues/2832 for more details.
This changes URL generation to generate URLs /docs/next/..., and
manually substitute relative URLs that had been written by hand.
Also fix a few other things about outdated links/comments.
Finally, `make doc-publish`.
Reviewed By: dulmarod
Differential Revision: D22117187
fbshipit-source-id: 32e2ba7e1
Summary:
Add objc test for ```NSArray``` and ```NSMutableArray```.
```NSMutableArray``` is a subclass of ```NSArray```.
For documentation of ```NSArray```, https://developer.apple.com/documentation/foundation/nsarray?language=objc
For documentation of ```NSMutableArray```, https://developer.apple.com/documentation/foundation/nsmutablearray?language=objc
The underlying mechanism for ```NSMutableArray``` is quite complicated. It changes the underlying data structure during runtime, so it is possible to have say O(log n) complexity for accessing element in array. (See here https://opensource.apple.com/source/CF/CF-855.11/CFArray.h) However, this is unlikely to happen if the engineer does not abuse the usage of the class ```NSMutableArray``` according to at least two ios engineers. So here the complexity is set to match the normal expectation of the complexity.
Reviewed By: ezgicicek
Differential Revision: D22041277
fbshipit-source-id: c27f43167
Summary:
This diff adds a prototype of a new checker that collects config checkings between markers.
Basically, what the checker is doing is a taint analysis.
* Taint source: function calls of "marker start"
* Taint sink: function calls of config checking
* Taint remove: function calls of "marker end"
By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending.
I am separating the diff into three steps:
(1/3) Add basic abstract semantics
(2/3) Add trace information
(3/3) Add reporting with test examples
Reviewed By: jvillard
Differential Revision: D21998170
fbshipit-source-id: e7759f62f
Summary: Pulse has now a better version of this check, so let's delete it.
Reviewed By: ngorogiannis
Differential Revision: D22019247
fbshipit-source-id: 344678225
Summary:
This issue type was not giving good results and can be replaced by
Pulse's version.
Reviewed By: ngorogiannis
Differential Revision: D22019551
fbshipit-source-id: 5cf3db46d
Summary:
Add objc test case for ```NSInteger``` and ```NSString```.
The test cases are adapted from java test case: ```IntTest.java```, ```StringBuilder.java```, and ```StringTest.java```.
Inspection of the record will be done later.
Reviewed By: ezgicicek
Differential Revision: D21994620
fbshipit-source-id: 0c1d7b34e
Summary: To avoid NULLPTR_DEREFERENCE false positives we want to treat some functions as `abort`. A new flag `--pulse-model-abort` allows us to provide a list of such functions.
Reviewed By: ezgicicek
Differential Revision: D21962555
fbshipit-source-id: d46b93c99
Summary: The new memory leaks analysis is now ready to be enabled by default and turned on in production. This also replaces the biabduction one which is now disabled.
Reviewed By: jvillard
Differential Revision: D21998666
fbshipit-source-id: 9cd95e894
Summary:
Turns out it was useful, so it is now reborn in OCaml.
Fixes https://github.com/facebook/infer/issues/1262.
Reviewed By: skcho
Differential Revision: D22016185
fbshipit-source-id: 31ccb7540
Summary:
This models ARC implementation of dealloc, see https://clang.llvm.org/docs/AutomaticReferenceCounting.html#dealloc. Dealloc methods can be added to ObjC classes to free C memory for example, but the deallocation of the ObjC instance variables of the object is done automatically. So here we add this explicitly to Infer:
1. First, we add an empty dealloc method when it is not written explicitly.
2. For each dealloc method (including the implicitly added ones) we add calls to dealloc of the ObjC instance variables.
Reviewed By: jvillard
Differential Revision: D21883546
fbshipit-source-id: f5d4930f2
Summary:
This diff avoids `infer report`s run parallel. If they do, there may be race for writing
`infer-out/.infer_runstate.json`, which result in `make test` failure in the next time.
Reviewed By: jvillard
Differential Revision: D21999073
fbshipit-source-id: 64df79cb6
Summary: We don't rely on `external-java-packages` in the inferconfig anymore. Let's remove it altogether.
Reviewed By: jvillard
Differential Revision: D21997962
fbshipit-source-id: 7a2e13cfe
Summary:
Similarly as for issue types, we want to generate the website
documentation from infer itself so we can easily cross-reference
checkers and the issue types they report.
This imports the website documentation written for some (very few) of
the checkers. I wrote some cursory one-liners for the rest.
Reviewed By: dulmarod
Differential Revision: D21934375
fbshipit-source-id: 8c9dc2b08
Summary:
This diff gives an order on running `test1`, `test2`, and `test3`. If they run parallel, they may
have a data race on writing `infer-out/.infer_runstate.json`.
Another minor fix is the object file path to remove.
Reviewed By: jvillard
Differential Revision: D21995671
fbshipit-source-id: eb9950cae
Summary:
There was an issue on `make build_ant_test` that newly generated `issues.exp.test` is empty. When
infer runs with `-- ant`, if there is already built objects in `ant_out`, infer analyzes nothing,
which result in the empty `issues.exp.test`. For example,
```
~/infer/infer/tests/build_systems/ant$ make test
[11:26:49][36924] Testing ant integration...
[ 2s][36924] SUCCESS Testing ant integration
~/infer/infer/tests/build_systems/ant$ touch `which infer`
```
The makefile tries to reanalyze ant targets because `infer` binary has been changed. However, there
is nothing to build/analyze, since `ant_out` still exists as the same.
```
~/infer/infer/tests/build_systems/ant$ make test
[11:26:57][37078] Testing ant integration...
[ 1s][37078] SUCCESS Testing ant integration
diff --git a/Users/scho/infer/infer/tests/build_systems/ant/issues.exp b/Users/scho/infer/infer/tests/build_systems/ant/issues.exp.test
index 376146b5f..e69de29bb 100644
--- a/Users/scho/infer/infer/tests/build_systems/ant/issues.exp
+++ b/Users/scho/infer/infer/tests/build_systems/ant/issues.exp.test
@@ -1 +0,0 @@
[-build_systems/ant/src/Hello.java, Hello.test():int, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure test()]-]
Test output (build_systems/ant/issues.exp.test) differs from expected test output build_systems/ant/issues.exp
Run the following command to replace the expected test output with the new output:
make -C build_systems/ant replace
make: *** [test] Error 1
```
To handle this issue, this cleans `ant_out` before running infer.
Reviewed By: jvillard
Differential Revision: D21950916
fbshipit-source-id: f57056f6e
Summary:
See previous diff: issues are always reported with the same severity so
recognise that and just use their default severity in "modern" checkers.
Reviewed By: ngorogiannis
Differential Revision: D21904591
fbshipit-source-id: fb5387e35
Summary:
This diff implements part of the memory management for Objective-C classes in ARC, namely that `dealloc` is called when the objects become unreachable. In reality the semantics of ARC says that this happens when their reference count becomes 0, but we are not modelling this yet in Pulse. However, we could in the future.
This fixes false positives memory leaks when the memory is freed in dealloc.
`dealloc` is often implicit in Objective-C, it also calls the dealloc of instance variables and superclass. None of this is implemented yet, and will be done in a future diff. This will be added in the frontend probably, similarly to how it's done for C++ destructors.
This is an important part of modelling Objective-C semantics in Infer, I looked at whether this should be a preanalysis to be used by all analyses but this needs Pulse. So the idea is that any analysis that needs to understand Objective-C memory model well, should have Pulse as a preanalysis.
Reviewed By: jvillard
Differential Revision: D21762292
fbshipit-source-id: ced014324
Summary:
Since Java8, interfaces mays contain implementations
(default methods). We modify the resolve algorith in the Java frontend
to take care of that.
Reviewed By: jvillard
Differential Revision: D21785182
fbshipit-source-id: ffab8124c
Summary: We do not use an arbitrary threshold to test cost results anymore but instead rely on `cost-issues` which do not have any trace attached. This diff adds traces to `costs-report.json` so that we can test cost issues with traces.
Reviewed By: skcho
Differential Revision: D21858846
fbshipit-source-id: e73321a92
Summary:
Now that we have a way to write cost issues, let's not rely on some arbitrary threshold (and also get rid of `EXPENSIVE_EXECUTION_TIME` issues in tests).
One consequence of this is that we will loose the cost traces in tests since `costs-report.json` doesn't have any traces. Next diff fixes that.
Reviewed By: skcho
Differential Revision: D21837574
fbshipit-source-id: 86b4d028d
Summary:
The model returns an array the length of which is the same to that of enum entries.
It takes the length of enum entries from the summary of `Enum.values` because it is not written in `tenv`. In order to do that, the model semantics should be able to request the summary of the function with `get_summary`, so I extended `model_env` to include the functionality.
Reviewed By: ezgicicek
Differential Revision: D21843319
fbshipit-source-id: d6f10eb91
Summary:
The model returns an array the length of which is the number of known
fields in `tenv`.
Reviewed By: ezgicicek
Differential Revision: D21840375
fbshipit-source-id: 891517c6e
Summary: D21816312 forgot to add the new cost testing mechanism to `fb-performance` and `performance-exlusive` directories. This diff fixes that.
Reviewed By: skcho
Differential Revision: D21837912
fbshipit-source-id: 407dafcd3
Summary: The models were too naive before since they invalidated the underlying array completely (copying C++'s push_back model), causing spurious vector invalidation issues in Java. This diff adds more reasonable models.
Reviewed By: skcho
Differential Revision: D21787543
fbshipit-source-id: a5a59ff69
Summary:
In order to test cost analysis results, currently we rely on having an arbitrary cost threshold (200) and report issues that exceed this cost. For instance, a cost of 201 is considered expensive and reported as `EXPENSIVE_EXECUTION_TIME` issue in cost tests.
This means, if we change the cost analysis in a slight way that results in some constant cost increase under 200, we wouldn't able to detect it. I find this unsatisfactory and somewhat hacky.
This diff adds the ability to write the result of `costs-report.json` into a separate `cost-issues.exp` and then compare the actual costs (not only than relying on this arbitrary threshold reporting mechanism).
Reviewed By: skcho
Differential Revision: D21816312
fbshipit-source-id: 93b531928
Summary: Add models for `View` methods that schedule on the UI thread.
Reviewed By: skcho
Differential Revision: D21767954
fbshipit-source-id: 015441ea7
Summary:
Android OS calls certain overridden class methods always on the UI thread. The function changed here attempted to build a list of all these methods, one by one. It's much more complete to simply consider a method as callable on the UI thread if it's an override of an Android library method, and it starts with "on". Only a single instance is known not to obey this pattern, so it's easier to blacklist than to whitelist.
Also clarify the name to `is_android_lifecycle_method`.
Reviewed By: ezgicicek
Differential Revision: D21703365
fbshipit-source-id: 41ca3e998
Summary:
I think `Analysis_stops` ought to achieve roughly the same thing (except
that weird filtering logic which I removed).
Reviewed By: dulmarod
Differential Revision: D21686562
fbshipit-source-id: 53d40729f
Summary: Assigning `nullptr` to `std::function` was causing `NULLPTR_DEREFERENCE` as our model was expecting to get an object in the right hand side of the assignment (`std::function::operator=`) and was dereferencing that object. Assigning `nullptr` to `std::function` removes callable object from it. We model this special case by creating a fresh value.
Reviewed By: skcho
Differential Revision: D21685318
fbshipit-source-id: 2d4af1933
Summary:
Introduce BIABD_ prefixes for a few issue types that were duplicated
between analyses, and also prefix the lab exercise issue type to avoid
sharing with biabduction.
Reviewed By: ngorogiannis
Differential Revision: D21660226
fbshipit-source-id: 3435916e6
Summary:
A buck integration for capturing simultaneously clang and java targets.
Just like the java-specific `JavaGenruleCapture` integration, it relies on
dummy targets that depend on the flavoured clang versions.
For example, a `cxx_library` target named `//clang:hello` will have an associated target
called `//clang:hello_infer` that depends on `//clang:hello#infer-capture-all`,
and whose output is a text file containing the output path of the dependency.
Reviewed By: jvillard
Differential Revision: D21620458
fbshipit-source-id: 23919387b
Summary:
This seems to make sense as it's a separate analysis (that depends on
biabduction). This introduces unpleasant `|| is_checker_enabled TOPL`
whenever we try to figure out if biabduction will run. I think this is a
more general problem that deserves a more general solution to express
the fact that checkers can depend on others, so that, eg,
`is_checker_enabled Purity` is true when we pass `--loop-hoisting`. Will
address in another diff.
Reviewed By: ngorogiannis
Differential Revision: D21618460
fbshipit-source-id: 8b0c9a015
Summary: Later on, this can be changed again or made customizable.
Reviewed By: artempyanykh
Differential Revision: D21618730
fbshipit-source-id: fe517c766
Summary:
We stopped relying on an external perf data file to determine which functions are on the cold start. Let's remove this issue now.
NB: Keeping the `--perf-profiler-data-file` as deprecated to prevent issues on the CI and prod.
Reviewed By: skcho
Differential Revision: D21594150
fbshipit-source-id: faa58782d
Summary:
Start with tests about dynamic dispatch to test the upcoming
pre-analysis.
Reviewed By: ezgicicek
Differential Revision: D21594496
fbshipit-source-id: 1771ea968
Summary:
This function had been computing the name for ObjC methods wrong, with only the class name. This was causing wrong error messages in Pulse.
The main issue was that `Procname.to_simplified_string` was writing `Classname::methodname` for ObjC methods, which is not the convention. This confused the `hashable_name` funtion. So changing the method name to `Classname.methodname` which is more standard, and this also fixes `hashable_name`.
Reviewed By: ngorogiannis, jvillard
Differential Revision: D21570880
fbshipit-source-id: 13ed62cf8
Summary: In an intra-procedural analysis, we assume that parameters passed by reference to a function will be initialized inside that function. To do that we use the type information of a formal parameter to initialize the fields of the struct. This was causing false positives if the formal parameter in function signature had type `void*`. To solve this, we used type information from local variables instead. However, we also get false positives for any kind of pointer if we use cast. We fix this by using type information of local variables as in `void*` case.
Reviewed By: jvillard
Differential Revision: D21522979
fbshipit-source-id: 4222ff134
Summary:
Previous translation of enum constants were wrong since they assumed that the enum constant didn't include any global variable (hence they just looked up the enum exp from the map, forgetting to tie the respective instructions into the cfg).
```
const int gvar = 0;
enum {
evar = gvar,
};
int dangling() {
return evar;
}
```
as a result, the CFG was missing the instruction for the load of the `gvar`.
{F237004587}
This diff fixes this issue by hooking up the instructions that load the enum constant in to the CFG. Note that in this example, it is only a load instruction but there could be more instructions (e.g. if we had `gvar > 1`, we would have prune +join).
{F237004493}
Reviewed By: ezgicicek
Differential Revision: D21549781
fbshipit-source-id: 525534fb2
Summary:
Just like `CFBridgingRelease` we want to be able to model functions that are specific to a given codebase that make a transfer of memory ownership so that developers don't need to worry about releasing that memory anymore, and hence, we don't want to report leaks on that memory.
Things get a little more complicated, because some of the functions we want to model are in a specific namespace, so with this flag we take both cases into account, when we are dealing with namespaces or not.
Reviewed By: jvillard
Differential Revision: D21404409
fbshipit-source-id: c36bd7afc
Summary: Currently we get false positive if we apply `operator--` to the `end()` iterator. To solve this, we model iterator `operator--` not to raise an error for the `EndIterator` invalidation, but to create a fresh element in the underlying array.
Reviewed By: ezgicicek
Differential Revision: D21476353
fbshipit-source-id: 5c722372e
Summary:
It is undefined behavior to dereference end iterator.
To catch end iterator dereferencing issues we change iterator model: instead of having `internal pointer` storing the current index, we model it as a pointer to a current index. This allows us to model `end()` iterator as having an invalid pointer and there is no need to create an invalidated element in the vector itself.
Reviewed By: ezgicicek
Differential Revision: D21178441
fbshipit-source-id: fd6a94b0b
Summary: We mistakenly invalidated the set element which causes spurious vector invalidation errors. Instead, we should modify it without any invalidation.
Reviewed By: jvillard
Differential Revision: D21521943
fbshipit-source-id: 67963967e
Summary:
This diff adds semantics of assume null, heuristics. When `assume(x == null)`, it removes the
methods called on the builder `*x` from the abstract state.
```
x -> {p}
p -> {method1 called}
assume(x == null)
x -> {p}
```
This heuristics is unsound: Even though `x` (a pointer to builder object) points-to an builder
object, which cannot imply that the object `p` does not exist in the concrete semantics. The
unsoundness may appear when there is an alias (see the FP test added).
Reviewed By: ezgicicek
Differential Revision: D21502923
fbshipit-source-id: 2e392bd89
Summary: Java's iterator models were wrong. This causes `VECTOR_INVALIDATION` errors in fbandroid projects. This diff aims to fix it by modeling Java iterators with a current pointer and an underlying collection array.
Reviewed By: skcho
Differential Revision: D21448322
fbshipit-source-id: 7d44354b5
Summary:
These 2 methods are automatically supplied for all enums, with
predefined behavior and nullability: https://www.geeksforgeeks.org/enum-in-java/
(Note that they are not part of java.lang.Enum class).
This will allow using them in unvetted third part and under strict mode.
Reviewed By: artempyanykh
Differential Revision: D21501716
fbshipit-source-id: 104082d15
Summary:
Because in the real semantics CFRelease can be used more than once, and also the variables can be used after CFRelease in general, modelling this as `free` causes many `USE_AFTER_FREE` errors. Now we change the model to not add the `Invalid CFree` attribute, but to just remove the `Allocated` attribute. So we can model memory leaks in the simple case of `Create` and not `CFRelease` before going out of scope, but we avoid the `USE_AFTER_FREE`.
Since the model for CFRelease now diverges from free, changed the command line option for modelling to `pulse-model-release-pattern`.
Reviewed By: jvillard
Differential Revision: D21324895
fbshipit-source-id: ab323d981
Summary: The contract for reporting races in C++ is to flag races between writes under lock with reads without a lock. This diff restores that contract which had been violated by recent changes.
Reviewed By: jberdine
Differential Revision: D21383876
fbshipit-source-id: 6a84e1506
Summary:
This diff changes way we treat classes w.r.t. to Nullsafe modes when
issuing meta-issues.
Previously, we considered nested class independently of the outer one.
This was leading to a tricky case: when the class is clean but nested
class needs fixing, meta-info told that class can be Nullsafe.
This is counter-intutive and lead to problems when users tried to follow
wrong nullsafe suggestions for this case.
After this diff we:
1. Start calculating meta-issues only on the outermost level. This will simplify
reasoning about nullsafe stats.
2. Aggregate all nested issues counters to corresponding outer-level class.
Among others, CLASS_CAN_BE_NULLSAFE Advice will finally become
actionable in all known cases.
Reviewed By: artempyanykh
Differential Revision: D21353607
fbshipit-source-id: a17c6958a
Summary:
List of things happening in this unreviewable diff:
- moved PulsePathCondition to PulseSledge
- renamed --pulse-path-conditions to --pudge
- PulsePathCondition now contains all the arithmetic of pulse
(inferbo+concrete intervals+pudge). In particular, moved arithmetic
attributes into PulsePathCondition.t. PulsePathCondition plays the
role of PulseArithmetic (combining all domains).
- added tests for a false positive involving free()
- PulseArithmetic is now just a thin wrapper around PulsePathCondition
to operate on states directly (instead of on path conditions).
- The rest is mostly moving code into PulsePathCondition (eg, from
PulseInterproc) and adjusting it.
Reviewed By: jberdine
Differential Revision: D21332073
fbshipit-source-id: 184c8e0a9
Summary:
We have a common entry point where we skip analysis in nullsafe.
This logic is copied from `Reporting.log_issue_from_summary`.
I believe this should not exist in Reporting: it is not the right place
to decide whether to suppress issues: we should not try to report it in
first place.
Because of that we falsely report "needs improvement" meta-issue while
we don't issue any (they were suppressed but participated in needs
improvement count calculations).
Now this change will make meta-issue to be synced with what the user
actually sees.
Down the line we should have a more reliable fix for that.
So far I reviewed suppressing code and looks like we should not suppress
anything else (unless explicitly SuppressLint-ed, which is fine).
Reviewed By: artempyanykh
Differential Revision: D21328634
fbshipit-source-id: 120ce06d1
Summary:
Add a new data structure and use it for the map of memory accesses to
limit the number of destinations reachable from a given address. This
avoids remembering details of each index in large arrays, or even each
field in large structs.
Reviewed By: skcho
Differential Revision: D18246091
fbshipit-source-id: 5d3974d9c
Summary:
It suppresses cost reports of access methods, anonymous class methods, and auto-generated methods.
For those methods, this diff blocks reporting both expensive
issue (`EXPENSIVE_COLD_START/_UI_THREAD`) and complexity increase issue (`COMPLEXITY_INCREASE`).
Reviewed By: jvillard
Differential Revision: D21303068
fbshipit-source-id: 1c9533956
Summary:
The C++ tests were a bit of a mess. This diff tries to enforce the following principles:
- mark every function with `_ok` or `_bad` so that when a function appears in `issues.exp` it's easy to figure out the intention;
- mark every false negative and positive with `FP_` and `FN_` to document expectations;
- make every function access one field and participate in at most one issue report so that it's easier to assess changes.
Reviewed By: jvillard
Differential Revision: D21278627
fbshipit-source-id: 9698f716f
Summary:
We were invalidating "*(vec.__infer_backing_array)" instead of the
address of the field itself.
Reviewed By: ezgicicek
Differential Revision: D21280357
fbshipit-source-id: 48b984800
Summary:
The directory was created to have several sets of nullsafe tests but
there is only one in the end. Remove the redundant "-default".
Reviewed By: mityal
Differential Revision: D21300205
fbshipit-source-id: 46ed8b032
Summary:
The directory names had some interesting variety due to historical
reasons.
- {c,cpp,objc,objcpp}/errors/ date from the time when infer was only
biabduction
- java/infer/ dates from the time when we had an "--analyzer" option and
"infer" was one of them (sic), and eg another was "eradicate".
- c/biabduction/ dates from the time when the biabduction analysis was
being migrated to the "checkers" (AI) framework. For some reasons the
tests there are not a subset of c/infer/ but seem to be entirely new
tests.
The convention now dictates that we should name all of these
*/biabduction/. This diff moves the existing tests from c/biabduction/
into c/biabduction/misc/.
Reviewed By: mityal
Differential Revision: D21300147
fbshipit-source-id: 516d1cb15
Summary:
The test for the ant integration used to import all of biabduction tests
via a symlink. This is extremely annoying: whenever the biabduction
tests change, so do the ant tests.
Replace the ant tests with a simple single file project.
Reviewed By: ngorogiannis
Differential Revision: D21301450
fbshipit-source-id: 0d67d71d7
Summary: We currently don't support abducing the spec that we need to delete an attribute, that makes the model for `CFBridgingRelease` work les well when it is, for instance, wrapped in a method. We show examples of how this doesn't work at the moment.
Reviewed By: jvillard
Differential Revision: D21176108
fbshipit-source-id: 79aed7a5d
Summary:
We model `malloc` in Objective-C as `malloc_not_fail` I think because the null case is not normally handled in iOS apps because the OS will just killed the app after giving some memory warnings.
So adding `malloc_not_fail` model to Pulse.
Reviewed By: jvillard
Differential Revision: D21278527
fbshipit-source-id: 17a5008fe
Summary:
This translates the construct `ObjCBridgedCastExpr` when the cast_kind is `OBC_BridgeTransfer`, or in syntax, the cast (`__bridge_transfer`).
This cast means that the object is passed from manual memory management to ARC, so one doesn't need to call `release` manually. It is important to model this to avoid false positives.
It translates it as a builtin that we then model in Pulse, the same way we modelled `CFBridgingRelease` which does the same thing.
The name of the builtin is `__free_cf` which is not ideal but I left it like that for compatibility with biabduction. We can change it once we remove this check from biabduction.
update-submodule: facebook-clang-plugins
Reviewed By: jvillard
Differential Revision: D21176337
fbshipit-source-id: 736ceeb9b
Summary:
Good night, sweet prince. This was never used and hasn't seen progress
in a while.
Reviewed By: jberdine
Differential Revision: D21201932
fbshipit-source-id: e6f537b30
Summary:
In the previous diffs, nullsafe behavior was changed to the following:
nested class mode is inherited from the outer class mode.
Though it is possible to e.g. make nested class Nullsafe and outer not,
or make nested class STRICT and outer just LOCAL, this is an edge case
and we don't want to recommend annotating nested classes by default. The
right way is to make outer class Nullsafe instead.
In this decision, we take into account user experience and codebase
readability.
Reviewed By: ngorogiannis
Differential Revision: D21255806
fbshipit-source-id: 0200cb555
Summary:
With this change, set of possibilities will be more actionable. Most
importantly, this will also educate users and make them realize how
Nullsafe trust works.
NOTE: yes, parenthesis are bit clumsy, but it was the easiest way to
make this change and let the phrase remain grammatically correct.
Reviewed By: artempyanykh
Differential Revision: D21231468
fbshipit-source-id: 4b5349fb5
Summary:
In the previous diff we changed the semantics of nested classes w.r.t.
to Nullsafe.
Let's make it clear if users will attempt to misuse it.
Reviewed By: artempyanykh
Differential Revision: D21230717
fbshipit-source-id: 0ecc0dd06
Summary: Similarly to Enum.name, we model Class.getCanonicalName as returning an arbitrary non-empty string.
Reviewed By: ngorogiannis
Differential Revision: D21207120
fbshipit-source-id: 1e2dbd1fd
Summary:
From the user perspective, the current behavior is confusing.
The users intutitively expect the inner class to inherit Nullsafe mode
from the outer one.
Having a class that is Nullsafe but the inner is not is hence dangerous
and misleading.
For the sake of completeness and to support gradual strictification, we
allow the nested class to improse additional strictness. Particularly,
the inner class can be Nullsafe but the outer can be not.
A follow up to this diff will include warnings telling about redundant and wrong usages of nested annotations.
Reviewed By: artempyanykh
Differential Revision: D21228055
fbshipit-source-id: 75755ad1d
Summary: Iterator invalidation traces were based on vector rather than iterator itself.
Reviewed By: ezgicicek
Differential Revision: D21202047
fbshipit-source-id: 62ce8a488
Summary:
We model Enum.name as returing a constant name, rather than getting real field names. We did this
because we couldn't think of any big gains, in terms of analysis precision/performance, from getting
the real names.
Reviewed By: ezgicicek
Differential Revision: D21201730
fbshipit-source-id: a2dc01a44
Summary: This diff revises the models of Collection.set and get to handle its elements.
Reviewed By: ezgicicek
Differential Revision: D21201242
fbshipit-source-id: 9c248453d
Summary:
We ignored allocator models for vectors, and were not able to initialize vectors properly. This diff fixes this issue.
It also adds a test which was a FN before.
Reviewed By: skcho, jvillard
Differential Revision: D21089492
fbshipit-source-id: 6906cd1d1
Summary: D21155014 replaced `skip` call with a Load but this was not right. Instead, let's add a new builtin function (rather than skip) so that other analyses can freely model it as they want.
Reviewed By: jvillard
Differential Revision: D21178286
fbshipit-source-id: c214ccfb0
Summary: Java has this pattern of wrapping non-thread-safe containers in factory methods producing identically-typed results, but wrapped in a synchronised shell. This diff teaches RacerD about some common factory methods and uses the attribute domain to track the dynamic type of their results.
Reviewed By: ezgicicek
Differential Revision: D21155538
fbshipit-source-id: 42ebe6251
Summary: Complete the set of models for java containers that Infer should not report thread safety violations.
Reviewed By: ezgicicek
Differential Revision: D21138280
fbshipit-source-id: 01e1944b6
Summary: Models were partial and/or simply missing (`Map` writes!). Now the modelled containers use inheritance for conciseness (`List` reads are only those not caught by the `Collection` matcher, etc). Also, add URLs to documentation sources.
Reviewed By: ezgicicek
Differential Revision: D21132069
fbshipit-source-id: fefb360f0
Summary: `CFBridgingRelease` and `__bridge_transfer` which I'll model later, transfer the memory model from manual memory ref count to ARC (automatic ref count), so to avoid false positives this needs to be modelled. We can simply remove the Allocated attribute from the state, which means we won't try to track that memory anymore.
Reviewed By: skcho
Differential Revision: D21088218
fbshipit-source-id: 3520a0d59
Summary: This diff suppresses cost issues on lambda and auto-generated procedures, since they were too noisy.
Reviewed By: ezgicicek
Differential Revision: D21153619
fbshipit-source-id: 65ad6dcc3
Summary:
Replace horrible hack with ok hack.
The main difficulty in implementing the disjunctive domain is to avoid
the quadratic time complexity of executing the same disjuncts over and
over again when going around loops:
First time around a loop, assuming for example a single disjunct `d`:
```
[d]
loop body
[d1' \/ d2']
```
Second time around the same loop: the new pre will be the join of the
posts of predecessor nodes, so `old_pre \/ post(loop,old_pre)`, i.e.
`d \/ d1' \/ d2'`. Now we need to execute `loop body` again
*without running the symbolic execution of `d` again* (and the time after
that we'll want to not execute `d`, `d1'`, or `d2'`).
Horrible hack (before): Disjuncts have a boolean "visited" attached
that does its best to keep track of whether a given disjunct is old or
new. When executing a single *instruction* look at the flag and skip the
state if it's old. Of course we have no way to know for sure so it turns
out it was often wrongly re-executing old disjuncts. This was also
producing the wrong results over even simple loops: only the last
iteration would make it outside the loop for some reason. Overall, the
semantics were pretty untractable and shady at best.
New hack (this diff): only run instructions of a given *node* on
disjuncts that are not physically equal to the "pre" ones already in the
invariant map for the current node.
This gives the correct result over simple loops and a nice performance
improvement in general (probably the old heuristic was hitting the
quadratic bad case more often).
Reviewed By: skcho
Differential Revision: D21154063
fbshipit-source-id: 5ee38c68c
Summary:
We translated the expression `CXXStdInitializerListExpr` naively in D3058895 as a call to
a skip function, with the hope that it would be translated better in the future. However, the naive means that we lose access to the initialized list/array because we are simply skipping it. So, even if we want to model the initializer properly, we have to deal with the skip specially.
This diff tries to solve this problem by removing the skip call whenever
possible. Instead, we translate the underlying array/list as a Load, so
that when it is passed to the constructor, we can pick it up.
For the following initialization:
``` std::vector<int*> vec = {nullptr};
```
Before, we translated it as
```
*&0$?%__sil_tmpSIL_materialize_temp__n$7[0]:int* const =null
n$8=_fun___infer_skip_function(&0$?%__sil_tmpSIL_materialize_temp__n$7:int* const [1*8] const )
n$9=_fun_std::vector<int*,std::allocator<int*>>::vector(&vec:std::vector<int*,std::allocator<int*>>*,n$8:std::initializer_list<int*>)
```
However, this means, `n$8` would be result of something skipped which we can't reason about. Instead, we just pass the underlying initialized array now, so we get the following translation:
```
*&0$?%__sil_tmpSIL_materialize_temp__n$7[0]:int* const =null
n$8=*&0$?%__sil_tmpSIL_materialize_temp__n$7:int* const [1*8] const
n$9=_fun_std::vector<int*,std::allocator<int*>>::vector(&vec:std::vector<int*,std::allocator<int*>>*,n$8:std::initializer_list<int*>)
```
Reviewed By: jvillard
Differential Revision: D21155014
fbshipit-source-id: 75850b1e6
Summary:
When encountering a constant, pulse creates an abstract value (a
variable) to represent it, and remembers that it's equal to it. The
problem is that pulse doesn't yet know how to deal with the fact that
some variables are going to be equal to each other.
This hacks around this issue in the case of constants, within the same
procedure, by remembering which constants have been assigned to which
place-holder variables, and serving those variables again when the same
constant is translated again.
Limitation: this doesn't work across procedure calls as the "constant
maps" are not saved in summaries.
Something to look out for: we don't want to make `if (p == NULL)` create
a path where `p` is invalid (we only make null invalid when we see an
assignment from 0, i.e. `p = NULL;`).
Reviewed By: ezgicicek
Differential Revision: D21089961
fbshipit-source-id: 5ebb85d0a
Summary:
1. Package will make the error too verbose.
2. We don't even need to say it is "class" because we say it in the error
description ("Class has 0 issues and can be marked Nullsafe").
Reviewed By: artempyanykh
Differential Revision: D21131998
fbshipit-source-id: 6ccca7615
Summary:
One source of false positives on container races is when the container member field is initialised to a concurrent version in a constructor, but the static type of the field doesn't reflect the thread safety of it.
This solution
- tracks flows from constructors of safe data structures to abstract addresses;
- initialises the initial attribute state when analysing a non-constructor method to that achieved by all constructors/class-initializers.
- checks for that attribute when recording container accesses.
Reviewed By: jvillard
Differential Revision: D21089428
fbshipit-source-id: 02a88f6e8
Summary: Modeling vector iterator with two internal fields: an internal array and an internal pointer. The internal array field points to the internal array field of a vector; the internal pointer field represents the current element of the array. For now `operator++` creates a fresh element inside the array.
Reviewed By: ezgicicek
Differential Revision: D21043304
fbshipit-source-id: db3be49ce
Summary:
Add a path condition to each symbolic state, represented in sledge's arithmetic domain. This gives a precise account of arithmetic constraints. In particular, it is relation and thus is more robust in the face of inter-procedural analysis.
This is gated behind a flag for now as there are performance issues with the new arithmetic.
Reviewed By: jberdine
Differential Revision: D20393947
fbshipit-source-id: b780de22a
Summary:
There are two types of anonymous classes (not user defined classes):
- classic anonymous classes (defined as $<int> suffixes)
- lambda classes (corresponding to lambda expressions). Experimentally,
they all have form `$Lambda$_<int>_<int>`, but the code just uses
`$Lambda$` as a heuristic so it is potentially more robust.
# Problem this diff solves
When generate meta-issues for nullsafe, we are interested only in
user-defined classes, so we merge all nested anonymous stuff to
corresponding user-defined classes and hence aggregate the issues.
Without this diff, for each lambda in the code, we would report this as
a separate meta-issue, which would both screw up stats and be confusing
for the user (when we start reporting mode promo suggestions!).
Reviewed By: artempyanykh
Differential Revision: D21042928
fbshipit-source-id: a7be266af
Summary:
This diff revises how to handle the unknown location in inferbo in two ways:
* stop appending field to the `Unknown` location, e.g. `Unknown.x.a` is evaluated to `Unknown`
* redesign the abstract of multiple locations, like `Bottom` < `Unknown` < `Known` locations
I am doing them in one diff since applying only one of them showed bad results.
Background: `Unknown` was adopted for abstracting all unknown concrete locations, so we could avoid missing semantics of assignments to unknown locations. We tried to keep soundness. However, it brought some other problems related to precision and performance.
1. Sometimes especially when Inferbo failed to reason precise pointer values, `Unknown` may point to many other abstract locations.
2. At that time, value assignments to `*Unknown` makes the situation worse: many abstract locations are updated with imprecise values.
This problem harmed not only its precision, but also its performance since it introduced more location entries in the abstract memory.
Reviewed By: jvillard
Differential Revision: D21017789
fbshipit-source-id: 0bb6bd8b5
Summary: The flags `--biabduction-fallback-model-alloc-pattern` and `--biabduction-fallback-model-free-pattern` were unused because we removed the models from .inferconfig a while ago because of too many false positives. We are implementing a better memory leak check based on Pulse, and are adding the similar flags `--pulse-model-alloc-pattern` and `--pulse-model-free-pattern`.
Reviewed By: jvillard
Differential Revision: D21061511
fbshipit-source-id: 1b3476c22
Summary:
See the code comment re: why don't we also recommend "strict" at this
stage. We can always change it later when we think users are happy with
strict.
Reviewed By: artempyanykh
Differential Revision: D21039553
fbshipit-source-id: 758ccf32c
Summary:
This diff is a step forward to the state when the list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes a case when we incorrectly defined possible promo mode (see
the test payload)
Reviewed By: artempyanykh
Differential Revision: D20948897
fbshipit-source-id: 616b96f96
Summary:
See the comments in the code why it makes logical sense.
This diff is a step forward the state when list of type violations is
independent of the mode (and we use mode solely to decide re: whether to
report or not).
This fixes majority of cases in ModePromotions.java
Reviewed By: artempyanykh
Differential Revision: D20948656
fbshipit-source-id: 82c0d530b
Summary:
Currently we exlude only if the method is based on deprecated config
packages.
Lets use the proper method, which covers both cases (config +
user-defined third party repo).
Reviewed By: artempyanykh
Differential Revision: D20946506
fbshipit-source-id: c3332667f
Summary:
Previously, we learned to detect if Default mode class can be made
Nullsafe(LOCAL).
Lets generalize it and calculate the precise mode.
NOTE 1: We don't distinct shades of "Trust some". We also don't
recommend trust some and recommend "Trust all" instead.
NOTE 2: As you can see from the test payload (see ModePromotions.java),
the precise calculation is not working as expected. This is due to a bug
in nullsafe implementation/design. See follow up diffs that will fix
this test.
Reviewed By: artempyanykh
Differential Revision: D20941345
fbshipit-source-id: 2255359ba
Summary: Unify the models of malloc and for the Create and Copy functions for Core Graphics. This add the null case from the malloc model to the Core Graphics models.
Reviewed By: jvillard
Differential Revision: D20890956
fbshipit-source-id: 278ac9d2f
Summary:
As soon as pulse detects an error, it completely stops the analysis and loses the state where the error occurred. This makes it difficult to debug and understand the state the program failed. Moreover, other analyses that might build on pulse (e.g. impurity), cannot access the error state.
This diff aims to restore and display the state at the time of the error in `PulseExecutionState` along with the diagnostic by extending it as follows:
```
type exec_state =
| represents the state at the program point that caused an error *)
```
As a result, since we don't immediately stop the analysis as soon as we find an error, we detect both errors in conditional branches simultaneously (see test result changes for examples).
NOTE: We need to extend `PulseOperations.access_result` to keep track of the failed state as follows:
```
type 'a access_result = ('a, Diagnostic.t * t [denoting the exit state] ) result
```
Reviewed By: jvillard
Differential Revision: D20918920
fbshipit-source-id: 432ac68d6
Summary: Consider functions that simply exit as impure by extending the impurity domain with `AbstractDomain.BooleanOr` that signifies whether the program exited.
Reviewed By: skcho
Differential Revision: D20941628
fbshipit-source-id: 19bc90e66
Summary:
This information can be useful for tooling responsible for further
processing (e.g. metric calculation and logging)
Reviewed By: artempyanykh
Differential Revision: D20914583
fbshipit-source-id: 61804d88f
Summary: The heuristics is to find a method in non-abstract sub-classes. See D20647101.
Reviewed By: jvillard
Differential Revision: D20491461
fbshipit-source-id: 759713ef4
Summary:
This diff distinguishes array declaration and size-setting in trace. For example, when there is an
assume statement on an array size, the array size can be pruned to another value. In which case, we
want to see "Set array size" in the trace, instead of "Array declaration".
Reviewed By: jvillard
Differential Revision: D20914930
fbshipit-source-id: 0253fb69e
Summary:
This diff lifts the `PulseAbductiveDomain.t` in `PulseExecutionState` by tracking whether the program continues the analysis normally or exits unusually (e.g. by calling `exit` or `throw`):
```
type exec_state =
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *)
| ExitProgram of PulseAbductiveDomain.t
(** represents the state originating at exit/divergence. *)
```
Now, Pulse's actual domain is tracked by `PulseExecutionState` and as soon as we try to analyze an instruction at `ExitProgram`, we simply return its state.
The aim is to recover the state at the time of the exit, rather than simply ignoring them (i.e. returning empty disjuncts). This allows us to get rid of some FNs that we were not able to detect before. Moreover, it also allows the impurity analysis to be more precise since we will know how the state changed up to exit.
TODO:
- Impurity analysis needs to be improved to consider functions that simply exit as impure.
- The next goal is to handle error state similarly so that when pulse finds an error, we recover the state at the error location (and potentially continue to analyze?).
Disclaimer: currently, we handle throw statements like exit (as was the case before). However, this is not correct. Ideally, control flow from throw nodes follows catch nodes rather than exiting the program entirely.
Reviewed By: jvillard
Differential Revision: D20791747
fbshipit-source-id: df9e5445a
Summary:
Malloc returns either an allocated object or a null pointer if there is no memory available. Modelling that.
This has always been a bit contentious because this leads to NPEs that people often ignores because they don't care. But if we don't model this, then we have FPs when people do take this into account when freeing the memory.
Reviewed By: jvillard
Differential Revision: D20791692
fbshipit-source-id: 6fd259f12
Summary:
This diff limits the depth of abstract location by a constant.
problem: Inferbo generated too many of abstract locations, especially when struct types had many pointer fields and Inferbo was not able to analyze the objects precisely. Since the number of generated abstract locations were exponential to the number of fields, it resulted in OOM in the end.
(reported by zyh1121 in https://github.com/facebook/infer/issues/1246)
Reviewed By: jvillard
Differential Revision: D20818471
fbshipit-source-id: f8af27e5c
Summary:
Currenlty the cost issue is printed at the first node of a function, which is usually the first
statment of the function. This may give a wrong impression that the cost of the statement is
changed.
This diff re-locate where to print issues with heuristics. Going backward from the first node
lines, it looks up a line satisfying,
1. A line should start with <fname> or should include " <fname>".
2. The <fname> found in 1 should be followed by a space, '<', '(', or end of line.
Reviewed By: jvillard
Differential Revision: D20766876
fbshipit-source-id: b4fee3180
Summary:
It's easy to create large arrays in code, eg `int x[1UL << 16];`, but
these can generate huge nodes in SIL because zero-initialization is
translated by zero-ing structures element by element. Introduce a
builtin to use instead. Keep the naive method for small structures (with
a configurable limit on "small").
Reviewed By: dulmarod
Differential Revision: D20836836
fbshipit-source-id: 6bf5410f8
Summary: Modelling `CG.*Release ` and `CFRelease` as `free`. This is what we were doing in biabduction.
Reviewed By: skcho
Differential Revision: D20767174
fbshipit-source-id: c77c1cdc6
Summary:
This models all the Create and Copy functions from CoreGraphics, examples in the tests.
These functions all allocate memory that needs to be manually released.
The modelling of the release functions will happen in a following diff. Until then, we have some false positives in the tests.
This check is currently in biabduction, and we aim to move it to Pulse.
Reviewed By: jvillard
Differential Revision: D20626395
fbshipit-source-id: b39eae2d9
Summary:
- Add `no_return` models for Java's `exit(...)` methods (can be extended further later on)
- handle throw-catch better by short-cutting throw nodes to not exit node but to all **catch nodes** that are reachable by the node. If there is no catch node, we short-cut to the exit node as before.
This removes a FP from deadstore tests because before we simply were not able to handle CF from throw-> catch nodes at all.
Reviewed By: skcho
Differential Revision: D20769039
fbshipit-source-id: e978f6cdb
Summary:
To find a method in non-abstract sub-classes, this diff applies the
same heuristics of inferbo.
* If the class is an interface: Find its unique sub-class and apply the heuristics recursively.
* If the class is an abstract class: Find/use its own summary if possible. If not found, find
one (arbitrary but deterministic) summary from its sub-classes.
* Otherwise: Find its own summary.
Reviewed By: ezgicicek
Differential Revision: D20647101
fbshipit-source-id: 2f8f3ff81
Summary: When looking at some reports I realised that adding the place where the memory becomes unreachable to the trace makes it more readable.
Reviewed By: skcho
Differential Revision: D20790277
fbshipit-source-id: d5df69e68
Summary:
The attribute `[no_return]` signifies that a function doesn't return. Previously, pre-analysis had cut the links to successor nodes of such no-return function nodes. This was intended to help with suppressing reporting on unreachable paths for some analyses. However, this results in having these nodes as dangling, with no connection to exit nodes.
This diff additionally shortcuts these no-return function nodes to exit node. This would allow us to enhance inter-procedural analyses like pulse to kepp track of paths that do not return since we will be keeping their connections at exit node rather than completely cutting them of as before. It would also allow us to assume that all paths start at the one start node and end at the one exit node (at least syntactically in the CFG).
Reviewed By: skcho
Differential Revision: D20736043
fbshipit-source-id: 0eace1bdb
Summary:
Used `2to3` but had to (poorly, sorry!) fix byte -> string output of processes.
update-submodule: facebook-clang-plugins
Reviewed By: ngorogiannis
Differential Revision: D20672767
fbshipit-source-id: 852c7e973
Summary:
Re-implement the generation of an HTML report (with bug traces) in
OCaml.
Kills the --only-show as a side-effect, it is of dubious use since there
is already infer-out/report.txt to get the report list as text. A
follow-up diff adds numbers to the list in infer-out/report.txt for easy
cross-referencing with `infer explore --select 123`.
Reviewed By: skcho
Differential Revision: D20672769
fbshipit-source-id: 39b3a299d
Summary:
Morally, INTERFACE_NOT_THREAD_SAFE is issued when an interface method is invoked from `ThreadSafe`-annotated code on an interface that is not known to be thread-safe or annotated so.
However, the ultimate purpose is to prevent races. Thus it should never be issued on an owned object or on objects we would not report races on for any reason (local variables, non-source variables, etc).
This diff equips interface call records with the abstract address they are invoked on, and uses the same rules for maintaining those records or not.
Reviewed By: skcho
Differential Revision: D20669259
fbshipit-source-id: 6c7841e6a
Summary: In an intra-procedural analysis we assume that parameters passed by reference to a function will be initialized inside that function. We use the type information of an actual parameter to initialize the fields of the struct. This does not work if a function has a parameter of type void* as the actual parameters also has type void*. To solve this issue, we use type information from local variables.
Reviewed By: jvillard
Differential Revision: D20670253
fbshipit-source-id: dc9f051ef
Summary:
This diff adds a procedure name to the head of the trace in order to distinguish issues in the same line.
"Updated Cost is ..." is changed to "Updated Cost of <proc name> is ..."
Reviewed By: ezgicicek
Differential Revision: D20672214
fbshipit-source-id: 303b4492f
Summary:
- Model `System.exit()` as early_exit and add a test
- Tweak message of methods that are impure due to having no pulse summary (and add a test)
Reviewed By: skcho
Differential Revision: D20668979
fbshipit-source-id: 6b5589aae
Summary: This diff avoids that an invalid interval value, e.g. [0, -1], is genrated by interval pruning.
Reviewed By: ezgicicek
Differential Revision: D20645488
fbshipit-source-id: 6516c75d1
Summary:
Hopefully no one uses this. This is in Python and we'd like to get rid
of it. Easy enough to either re-implement if needed or to be
re-implemented by a third party.
Reviewed By: ngorogiannis
Differential Revision: D20626344
fbshipit-source-id: 484022482
Summary: The current message is recommending to change `View.findViewById()` to `View.requireViewById()`, but the latter method is not supported in all API, so might lead to a crash in runtime.
Differential Revision: D20619361
fbshipit-source-id: 542746c79
Summary:
- the order of call state was wrong when printing contradiction for CItv
- add a test for impurity
Reviewed By: jvillard
Differential Revision: D20646181
fbshipit-source-id: 1c86fd0a4
Summary: There are no plans currently to track which lock protects each access, so reduce to the functional equivalent of having a singleton lock domain.
Reviewed By: skcho
Differential Revision: D20595013
fbshipit-source-id: d5100ac49
Summary:
As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by:
- discovering aliasing in memory
- widening limited number of times in loops and concluding that loop exit conditions are never taken
However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts:
```
Pulse: 1 pre/post(s)
#0: PRE:
{ roots={ };
mem ={ };
attrs={ };}
POST:
{ roots={ };
mem ={ };
attrs={ };}
SKIPPED_CALLS: { }
```
The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure.
Reviewed By: skcho
Differential Revision: D20619504
fbshipit-source-id: 3a8502c90
Summary:
Although try-with-resource is supported by nullsafe this code pattern
throws it off and make nullsafe report on a virtual **b**yte-**c**ode
variable.
Check out debug output from `TryWithResource` (or attached
visualisation of CFG):
0. node14: $bcvar2=null (on entry to try-with-resource).
1. node16: n$14=$bcvar2, but **also** PRUNE(!(n$14 == null), true). Then we go to
2. node18: do something here and in case of exception go to
3. node25->node23->node19->node20: and here we do
$bcvar2->addSuppressed(...).
Because on step 1 we refined nullability of n$14, but didn't refine
nullability of $bcvar20, on step 3 we are sure that $bcvar is null and
therefore issue an error.
Reviewed By: mityal
Differential Revision: D20558343
fbshipit-source-id: 520505039
Summary:
This is likely not the final refinement, rather one step forward.
We classify all classes by 3 categories:
- Nullsafe and 0 issues
- can add Nullsafe and will be 0 issues
- the rest (class needs improvement)
Each class will fall into exactly one category.
Error messaging is WIP, they are not intended to be surfaced to the user
just yet.
Note how this diff uses the result of the previous refactoring.
Reviewed By: artempyanykh
Differential Revision: D20512999
fbshipit-source-id: 7f462d29d
Summary: Add a flag `is-inclusive-cost` (`true` by default) which computes inclusive cost for each function. Setting the flag to `false` computes exclusive cost of the function where the cost of the callees are assumed to be `0`.
Reviewed By: skcho
Differential Revision: D20558275
fbshipit-source-id: 6b5798916
Summary:
# Problem
Consider
```
some_method(Object a) { a.deref(); }
```
What is nullability of `a` when we dereference it?
Logically, things like "LocallyCheckedNonnull" etc are not applicable
here.
This would be applicable if we called some_method() outside! But not
inside. Inside the function, it can freely treat params as non-null, as
long they are declared as non-nullable.
The best we can capture it is via StrictNonnull nullability.
Reviewed By: artempyanykh
Differential Revision: D20536586
fbshipit-source-id: 5c2ba7f0d
Summary:
`make test` failed in some test directories, because we were getting warnings
```
Foo.java uses unchecked or unsafe operations.
```
This diff fixes or suppresses these warnings.
Reviewed By: skcho
Differential Revision: D20557572
fbshipit-source-id: 63ecd3dfa
Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.
Reviewed By: jvillard
Differential Revision: D20444097
fbshipit-source-id: 33b6b25a2
Summary:
- Add more naive pulse models for:
- `System.arraycopy`
- `StringBuilder.setLength`
- `StringBuilder.delete`
- Model the following as pure
- `SparseArrayCompat.valueAt`
- `File.get...`
- Add a nice test
Reviewed By: jvillard
Differential Revision: D20513397
fbshipit-source-id: 6d412d13a
Summary:
This diff continues work in D20491716.
This time for Inheritance Rule.
Reviewed By: jvillard
Differential Revision: D20492889
fbshipit-source-id: c4dfd95c3
Summary:
This diff continues work in D20491716.
This time for Dereference Rule.
Reviewed By: jvillard
Differential Revision: D20492296
fbshipit-source-id: ff7f824f9
Summary:
# Problem
In current design, Rules (assignment rule, dereference rule, inheritance
rule) decide, depending on the mode, wether the issue is legit or not.
If the issue is not actionable for the given mode, it won't be created
and registered.
For meta-issues, we want to be able to do smart things like:
- Identify if we can raise strictness of the mode without
introducing new issues
- Classify classes on "clean" vs "broken", taking into account issues
that are currently invisible.
# Solution
In the new design:
1. Rules are issuing violations independently of mode. This makes sense
semantically. Mode is "level of trust we have for suspicious things",
but the thing does not cease to be suspicious in any mode.
2. Each Rule decides if it is reportable or not in a given mode.
3. `nullsafe_mode` is passed to the function `register_error`, that 1)
adds error so it can be recorded in summary for file-level analysis
phase 2) reports some of them to the user.
# This diff
This diff converts only AssignmentRule, follow up will include
conversion of other rules, so no issue encapsutes the mode.
Reviewed By: jvillard
Differential Revision: D20491716
fbshipit-source-id: af17dd66d
Summary:
Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals. However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes.
For instance, for the following functions
```
public static boolean is_null(Byte a) {
return a == null;
}
public static boolean call_is_null(Byte a) {
return is_null(a);
}
```
We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts):
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null,
BoItv ([max(0, v2), min(0, v2)]),
WrittenTo-----------WRONG },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1),
WrittenTo-----------WRONG },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1) },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
Reviewed By: skcho
Differential Revision: D20490102
fbshipit-source-id: 253d8ef64
Summary: These tests fail when seemingly unrelated changes are made to infer. In particular, it seems timeout limits have to be increased by 10x or more to make them succeed again. Disabling until we have a more stable replacement.
Reviewed By: ezgicicek
Differential Revision: D20489647
fbshipit-source-id: 9706b0807
Summary:
This diff naively models the following as `StdVector.push_back`:
- `StringBuilder.append`
- `String.replace`
- `Queue.poll`
It also adds a FN test for `Iterator.next`.
Reviewed By: skcho
Differential Revision: D20469786
fbshipit-source-id: 2d8e8d117
Summary:
This diff is doing three things:
1. Finishes work paved in D20115024, and applies it to nullsafe. In that diff, we hardened API for
file level analysis. Here we use this API in nullsafe, so now we can
analyze things on file-level, not only in proc-level like it was before!
2. Introduces a class-level analysis. For Nullsafe purposes, file is not
an interesting granularity, but we want to analyze a lot of things on
file level. Interesting part here is anonymous classes and how we link
them to their corresponding user-defined classes.
3. Introduces a first (yet to be improved) implementation of class-level
analysis. Namely it is "meta-issues" that tell what is going with class
on high level. For now these are two primitive issues, and we will
refine them in follow up diffs. They are disabled by default.
Follow ups include:
1. Refining semantics of meta-issues.
2. Adding other issues that we could not analyze before or analyzed not
user friendly. Most importantly, we will use it to improve reporting for
FIELD NOT INITIALIZED, which is not very user friendly exactly because
of lack of class-level aggregation.
Reviewed By: artempyanykh
Differential Revision: D20417841
fbshipit-source-id: 59ba7d2e3
Summary: The `FN_loop2` was not actually FN because infer analyzes its complexity as degree 1 correctly.
Reviewed By: dulmarod
Differential Revision: D20468367
fbshipit-source-id: 9e4c19415
Summary: The `iterate_over_mycollection_quad_FN` was not actually FN because infer analyzes its complexity as degree 2 correctly. So, this diff removed `_FN` from there.
Reviewed By: ezgicicek
Differential Revision: D20467398
fbshipit-source-id: b10340612
Summary: There has never been a sufficient formal basis for soundness nor completeness of reports on locals. This diff changes the domain to effectively concern only expressions rooted at formals or globals.
Reviewed By: ezgicicek
Differential Revision: D19769201
fbshipit-source-id: 36ae04d8c
Summary: `Object.clone` modeled as pure until the analysis can distinguish returning a fresh object vs. having no side-effects.
Reviewed By: skcho
Differential Revision: D20439998
fbshipit-source-id: 421054cfb
Summary:
`JavaSplitName` is used to represent Java types (in `Procname` in particular). The type itself is a pair of string (an optional package qualifier) and a "type name" (the quotes are there because it may contain array qualifiers).
For example `java.lang.Object[][]` should be represented as
```
{package=Some "java.lang"; typename="Object[][]"}
```
The constructor `make` was misused to construct instead types such as
```
{package=None; typename="java.lang.Object[][]"}`
```
This is evident when we print the return type of a `Procname` non-verbosely (the default), but we still see the package qualifier.
Obviously this is not just a pretty-printing bug, the values were themselves wrong.
The fix is to use the `of_string` constructor which will parse the package and separate it correctly. Another bug (in response to this one) had to be fixed in `Procname.is_vararg` to maintain behaviour in Nullsafe and Quandary.
Reviewed By: mityal
Differential Revision: D20394146
fbshipit-source-id: 4633902eb
Summary:
Impurity domain was tracking all changes to variables (with a list of traces that containing all write/invalid accesses). This results in having long traces with multiple access events for the same variable. For instance,
```
void swap_impure(int[] array, int i, int j) {
int tmp = array[i];
array[i] = array[j]; \\ included in the trace
array[j] = tmp; \\ included in the trace
}
```
here we recorded both array accesses.
This diff changes the domain to include accesses so that we only keep track of a single trace per access. Array accesses are only recorded once.
Note that we want to record all unique accesses, not just the first one, because impurity will be used for hoisting/cost where we will invalidate impure arguments and consider all the rest as not changing.
Reviewed By: jvillard
Differential Revision: D20385745
fbshipit-source-id: d3647dad3
Summary:
D20362149 missed
- to pass the optional argument `include_value_history` to the recursive call in `PulseTrace.add_to_errlog`.
- to set `include_value_history=false` for skipped calls.
This diff fixes these issues.
Reviewed By: skcho
Differential Revision: D20385604
fbshipit-source-id: 176e4d010
Summary:
Main changes are:
1. Dune can promote targets into the source tree as a part of build. This
allows us to **remove custom promotion/installation logic in src/Makefile**.
2. Dune promotion only works for path within workspace. This required
**moving dune-workspace one folder up**: from infer/infer/src to infer/infer.
But this is not bad, since it makes it possible to migrate tests under dune at some point.
3. `checkCopyright` now also promoted into `infer/infer/bin` instead of
`infer/scripts` partly for consistency and partly because of the
dune-workspace location.
4. `byte` mode was replaced with `byte_complete`. The latter takes
similar amount of time to build compared to `byte`, but produces
standalone binaries that don't require InferCStubs to be
installed. This allowed to remove `dune_exec_shim` and custom logic
around `dune build InferCStubs.install` when dealing with byte
targets.
All in all, `infer/src/Makefile` is not about 2/3 its previous size
with less custom logic in Makefiles/scripts and more encoded in dune
build files.
Reviewed By: jvillard
Differential Revision: D20303902
fbshipit-source-id: 9e4c65bd0
Summary:
With profiles and `(env ...)` stanza it's possible to consolidate
various ocamlc/ocamlopt/etc setups in a single place.
Where previously we needed to append `dune.common` to every dune file
and specify `flags` and `ocamlopt_flags` now the flags are specified
in `env` and applied accross the board.
This allows to
1. simplify build definitions,
2. avoid the need to generate dune files,
3. use plain sexps instead of OCaml and JBuilder plugin in build
files.
(I'll try to address 2 and 3 in the followup patches).
Existing `make` targets should continue working as before. Also, we
can use dune CLI like so:
```
infer/src$ dune printenv --profile opt # <- very useful for introspection
infer/src$ dune build check
infer/src$ dune build check --profile test
infer/src$ dune build infer.exe --profile dev
infer/src$ dune build infer.exe --profile opt
```
Also, with just 1 context something like `dune runtest` will run unit
tests only once instead of N times, where N is the number of contexts.
Now, there's one difference compared to the previous setup with
contexts:
- Previously, each context had its own build folder, and building infer
in opt context didn't invalidate any of the build artifacts in default
context. Therefore, alternating between `make` and `make opt` had low
overhead at the expense of having N copies of all build artifacts (1
for every context).
- Now, there's just 1 build folder and switching between profiles does
invalidate some artifacts (but not all) and rebuild takes a bit more
time.
So, if you're alternating like crazy between profiles your experience
may get worse (but not necessarily, more on that below). If you want
to trigger an opt build occasionally, you shouldn't notice much
difference.
For those who are concerned about slower build times when alternating
between different build profiles, there's a solution: [dune
cache](https://dune.readthedocs.io/en/stable/caching.html).
You can enable it by creating a file `~/.config/dune/config` with the
following contents:
```
(lang dune 2.0)
(cache enabled)
```
With cache enabled switching between different build profiles (but
also branches and commits) has ~0 overhead.
Dune cache works fine on Linux, but unfortunately there are [certain
problems with
MacOS](https://github.com/ocaml/dune/issues/3233) (hopefully, those
will be fixed soon and then there will be no downsides to using
profiles compared to contexts for our case).
Reviewed By: jvillard
Differential Revision: D20247864
fbshipit-source-id: 5f8afa0db
Summary:
This was never quite finished and inferbo has a new way to do sort of
the same thing.
Reviewed By: skcho, ngorogiannis
Differential Revision: D20362619
fbshipit-source-id: 7c7935d47
Summary:
Make <infer-out>/report.json the default value for this option, as this
is what is used 99% of the time. Clean up test options using this.
Reviewed By: ngorogiannis
Differential Revision: D20362644
fbshipit-source-id: a1bb18757
Summary:
Adding a model for malloc: we add an attribute "Allocated". This can be used for implementing memory leaks: whenever the variables get out of scope, we can check that if the variable has an attribute Allocated, it also has an attribute Invalid CFree.
Possibly we will need more details in the Allocated attribute, to know if it's malloc, or other allocation function, but we can add that later when we know how it should look like.
Reviewed By: jvillard
Differential Revision: D20364541
fbshipit-source-id: 5e667a8c3
Summary: Impurity traces are quite big due to recording values histories. Let's simplify the traces by removing pulse's value histories.
Reviewed By: skcho
Differential Revision: D20362149
fbshipit-source-id: 8a2a6115e
Summary: Type is not enough to say a function call of `Provider.get` is expensive or not.
Reviewed By: jvillard
Differential Revision: D20366206
fbshipit-source-id: 83d3e8741
Summary:
This diff uses a type parameter of `Provider.get` to decide whether assigning expensive cost to the
function call or not. For example, if the type is small one like `Provider<Integer>`, it be
evaluated to have a unit cost, otherwise a linear cost.
To get the return type of `Provider.get`, I added a simple analyzer that collects "casted" types
backwards. In Sil, while the function call statement loses the return type, e.g,
```
n$5=_fun_Object Provider.get()(n$3:javax.inject.Provider*);
```
the `n$5`'s value is usually casted to a specific type at some point later.
```
*&$irvar0:java.lang.Object*=n$5
n$8=*&$irvar0:java.lang.Object*
n$9=_fun___cast(n$8:java.lang.Object*,sizeof(t=java.lang.Integer;sub_t=( sub )(cast)):void)
```
So, the analyzer starts from the cast statements backward, collecting the types to cast for each
variables.
Reviewed By: ezgicicek
Differential Revision: D20345268
fbshipit-source-id: 704b42ec1
Summary: This diff adds a model for Java's `Object.clone()` method (similar to existing shallow_copy).
Reviewed By: jvillard
Differential Revision: D20341073
fbshipit-source-id: 30ae40fe7
Summary:
Some (all?) of this is already tested in other tests, but this feature
is important enough (and the implementation is scattered accross the
whole code), so I found it useful to have a small test that ensures the
very basic things are working as expected.
See `NestedFieldAccess.java` that tests far more advances things, but
here we focus only very basic things: conditions, local variable
assignments, and explicit assignments.
Reviewed By: jvillard
Differential Revision: D20339056
fbshipit-source-id: a6cfd0043
Summary: We forgot to take skipped calls into account for state comparison. This diff fixes that.
Reviewed By: skcho
Differential Revision: D20282739
fbshipit-source-id: 7b4d84bb0
Summary:
These were not used (and were actually activated byt the same config
param). They both are in experimental stage that never reached maturity.
Since the team does not have immediate plans to work on ObjC nullability
checker; and since "eradicate" (now known as nullsafe) is the main
solution for Java, removing it is sensible.
Reviewed By: jvillard
Differential Revision: D20279866
fbshipit-source-id: 79e64992b
Summary:
This is the kind of property for which the previous syntax forced one to
use spurious registers.
Reviewed By: ngorogiannis
Differential Revision: D20118863
fbshipit-source-id: b49740d33
Summary: When reporting CapturedStrongSelf we shouldn't report it when the block is "no escaping", as this won't lead to a retain cycle, so capturing strongSelf is ok.
Reviewed By: jvillard
Differential Revision: D20224359
fbshipit-source-id: c60dae333
Summary:
Update handling of `OffsetOfExpr` based on the new type definition
from updated version of clang-plugin.
Together with the change to clang-plugin, this essentially fixes hard
crash while analysing C/C++ files with non-literal `offsetof`
expression.
Fixes GH issues [#1178](https://github.com/facebook/infer/issues/1178), [#1212](https://github.com/facebook/infer/issues/1212)
Reviewed By: jvillard
Differential Revision: D20159173
fbshipit-source-id: 65fc228a4
Summary:
This diff renames `ZERO_XXX` issues to more appropriately named and descriptive
`XXX_UNREACHABLE_AT_EXIT` and replaces bottom with
unreachable in cost kinds and issues.
Reviewed By: skcho
Differential Revision: D20140301
fbshipit-source-id: eb6076b30
Summary:
1. It is convenient to stick with the policy "ERROR if and only if it is
enforced". Among other, it makes CI integration much easier to implement
(enforcemend, UI and messaging is decided based on severity).
2. Since Nullsafe annotation is an idiomatic way to indicate classes
with enforced nullability checking, we want it to be the only way to
enforce issues.
3. This means we decrease the priority of GraphQL violation issues.
(In practice they were not enforced so we have plenty of violations in
codebase to reflect reality). The proper way dealing with GraphQL will
be detecting such issues as a special issue type and prioritizing fixing
and Nullsafe-ifying corresponding classes.
4. Among other, we downgrade severity of field overannotated to advice
to keep it consistent with condition redundant.
Reviewed By: artempyanykh
Differential Revision: D20141420
fbshipit-source-id: e2f12835a
Summary:
The issue type `ZERO_EXECUTION_TIME` actually corresponds to bottom state but has been mistakenly used to mean
- unreachable nodes (program never reaching exit state)
- having zero cost (e.g. for allocations).
Note that, for execution costs, the latter doesn't make sense since we always incur a unit cost for the start node. Hence, a function with empty body will have unit cost. For allocations or IO however, we only incur costs for specific primitives, so a function with no allocations/IO could have a zero cost. However, there is no point reporting functions with zero cost as a specific issue type. Instead, what we want to track is the former, i.e. functions whose cost becomes 0 due to program never reaching exit state.
This diff aims to split these cases into two by only reporting on the latter and adds traces to bottom/unreachable cost by creating a special category in polynomials.
Next diff will rename `ZERO_XXX` to `XXX_UNREACHABLE_AT_EXIT`.
Reviewed By: skcho
Differential Revision: D20005774
fbshipit-source-id: 46b9abd5a
Summary:
For Mode.Local this is kind of obvious decision.
But this diff does the same for strict mode as well.
See comment in [ExplicitNonnullThirdParty] for the detailed explanation.
Reviewed By: artempyanykh
Differential Revision: D20140056
fbshipit-source-id: 13c66df81
Summary:
In the previos diff we restructured error rendering utils for
TypeOrigin.MethodCall.
In this diff we do the same with TypeOrigin field: lets make the code
consistent.
We also clearly distinct third party from all other possible cases in
this branch.
This changes messaging and reported errors for strict modes (see test cases), and I believe this is a net improvement.
Reviewed By: artempyanykh
Differential Revision: D20139741
fbshipit-source-id: 84f502553
Summary:
> We don't report when the cost is Top as it corresponds to subsequent 'don't know's. Instead, we
> report Top cost only at the top level per function
The previous code just ignored top costed nodes, so it was able to report a non-top cost that was
from another node. For example,
```
void foo() {
linear-cost();
top-cost();
}
```
It reported inconsistent reports: `EXPENSIVE_EXECUTION_TIME` with a linear cost and
`INFINITE_EXECUTION_TIME` at the same time.
This diff fixes it not to report `EXPENSIVE_EXECUTION_TIME` when there is a node with the top cost.
Reviewed By: ezgicicek
Differential Revision: D20139408
fbshipit-source-id: 9fedd4aec
Summary:
In the previous report, it reported the first cost of node that exceeds a threshold. However, this
may hide a bigger cost of node that appears later. This diff changes this to report the biggest
cost of node among the costs exceeding the threshold.
Reviewed By: ezgicicek
Differential Revision: D20116162
fbshipit-source-id: 06199fb46
Summary:
Current domain of Inferbo cannot handle float values. This diff evaluates float constants to the top
interval.
Reviewed By: ezgicicek
Differential Revision: D20116361
fbshipit-source-id: e6e398bbd
Summary:
This syntax
- is less confusing (according to several people who are not me);
objectively, there's less magic under the hood
- gives fine control over register number (because condition/action are separated)
- lets one compare values of different arguments of the same call
(e.g., one could have a transition that is taken only if two
arguments of a method call are equal)
Reviewed By: ngorogiannis
Differential Revision: D20005403
fbshipit-source-id: fad8f3b3d
Summary:
The test shows what that TOPL can express, in addition to bugs,
efficiency properties. However, there seems to be an underlying problem
in biabdaction that prevents this particular problem from being caught.
Reviewed By: ngorogiannis
Differential Revision: D20005404
fbshipit-source-id: 466f79050
Summary: The semantics of the `values` function of Java enum class was missing, when it is called outside the class initializer. This diff gets the size of the enum elements from the summary of class initializer function, `<clinit>`.
Reviewed By: ezgicicek
Differential Revision: D20094880
fbshipit-source-id: 7362bba1c
Summary: We had no tests that resulted in `ZERO_EXECUTION_COST`. Let's fix that.
Reviewed By: skcho
Differential Revision: D20097504
fbshipit-source-id: 56c23fea0
Summary:
Now when typechecking a class `A` marked with `Nullsafe(LOCAL)`,
classes from trusted list are properly recognized and nullability of
method params and return value are refined to `LocallyCheckedNonnull`
in a context of class `A`.
NOTE: refininng nullability when **accessing fields** on trusted classes
is **not implemented yet**, because the whole business of handling fields
in nullsafe is somewhat convoluted. This should not be a huge issue
though, since in Java fields are commonly accessed via getters any
way.
Reviewed By: mityal
Differential Revision: D20056158
fbshipit-source-id: 496433d90
Summary:
This will help making error reporting more actionable.
Often methods that are nullable in general (like View.findViewById) are used as not-nullable due to app-invariants. In such cases suggesting a non-nullable alternative that does an assertion under the hood makes the error report more actionable and provides necessary guidance with respect to coding best practices
Follow up will include adding more methods to models.
If this goes well, we might support it in user-defined area (nullability
repository)
Reviewed By: artempyanykh
Differential Revision: D20001416
fbshipit-source-id: 46f03467c
Summary:
Introduction of `ThirdPartyNonnull` nullability broke nullability
refinement heuristic for enums. This diff fixes it and also adds tests
so that we hopefully avoid such issues in future.
Reviewed By: mityal
Differential Revision: D19975810
fbshipit-source-id: f9245f305
Summary:
We need to be able to differentiate `UncheckedNonnull`s in internal vs
third-party code. Previously, those were under one `UncheckedNonnull`
nullability which led to hacks for optmistic third-party parameter
checks in `eradicateChecks.ml` and lack of third-party enforcement in
`Nullsafe(LOCAL, trust=all)` mode (i.e. we want to trust internal
unchecked code, but don't want to trust unvetted third-party).
Now such values are properly modelled and can be accounted for
regularly within rules.
Also, various whitelists are refactored using
`Nullability.is_considered_nonnull ~nullsafe_mode nullability`.
`ErrorRenderingUtils` became a tad more convoluted, but oh well, one
step at a time.
Reviewed By: mityal
Differential Revision: D19977086
fbshipit-source-id: 8337a47b9
Summary:
Add support for nullsafe mode with `trust=all` and `trust=none` a case
with a specific trust list is not supported yet and needs to be
implemented separately.
Tests introduce one unexpected
`ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION` issue which
complains about `this` having incorrect nullability; it is a bug and
needs to be fixed separately.
Reviewed By: mityal
Differential Revision: D19662708
fbshipit-source-id: 3bc1e3952
Summary: Was broken by previous diff: I forgot to update issues.exp
Reviewed By: artempyanykh
Differential Revision: D20001233
fbshipit-source-id: 67f534349
Summary: In all other cases we have period at the end, which is inconsistent.
Reviewed By: artempyanykh
Differential Revision: D20001065
fbshipit-source-id: 85ec6d751
Summary:
Use a record of package, class name to store (qualified) Java class names. This saves the round trip of concatenating then splitting again, etc, as well as saves some memory in the type environment as now the package paths can be shared across classes of the same package (about 10% in tests).
Also remove some unfortunate APIs.
Reviewed By: jvillard
Differential Revision: D19969325
fbshipit-source-id: f7b7f5a55
Summary: The way `Mangled.t` is used in `JavaClassName` means that it's always a plain string (we never have a "mangled" part). Remove the indirection and extra allocation. Also, simplify the API by throwing away one function that was used just once and wastefully.
Reviewed By: artempyanykh
Differential Revision: D19950672
fbshipit-source-id: b61fcba6e
Summary: This diff suppresses integer overflow issues in functions that includes "hash" in its name.
Reviewed By: jvillard
Differential Revision: D19942654
fbshipit-source-id: d86fa4f00
Summary: In line with changes to loom query in D19903057, let's adjust Infer's processing of the results.
Reviewed By: martintrojer
Differential Revision: D19902933
fbshipit-source-id: 200b3a03e
Summary: Not needed any more as infer's concurrency isn't controlled via make.
Reviewed By: jvillard
Differential Revision: D19905712
fbshipit-source-id: f97ef4421
Summary: Once we identify a weakSelf variable that is being used in a Noescape block, we want to report only the first occurrence.
Reviewed By: skcho
Differential Revision: D19941502
fbshipit-source-id: 2b6d4648b
Summary: For each variable that we identify as a captured strong self, we want to report only the first occurrence.
Reviewed By: skcho
Differential Revision: D19940031
fbshipit-source-id: f38f642c9
Summary: When we discovered that a strongSelf var was not checked for null, we then report in each occurrence which is spammy. Now we report only the first occurrence. To achieve that, we store a `reported` flag in the domain that gets set to true after we report once, and we only report if it's false.
Reviewed By: jvillard
Differential Revision: D19877218
fbshipit-source-id: c44109ae9
Summary:
This adds a violation of baos.topl found in github/seata/seata. However,
it is not a bug (see comment in commit).
Reviewed By: ngorogiannis
Differential Revision: D19518641
fbshipit-source-id: e219245ee
Summary:
Since Javalib 3.2, a new feature allows to rewrite
methods that contain (some specific form of) closures. Infer
now uses it. When loading each class we rewrite them and
new classes generated by Javalib to implements closures
(i.e. Java interfaces)<
Reviewed By: ngorogiannis
Differential Revision: D19389227
fbshipit-source-id: 245dd4404
Summary:
When finding a proper constructor for `std::make_shared`, the given parameter types are sometimes
slightly different, e.g., const int vs int. This diff loosens the condition of the types on finding
constructors.
Reviewed By: ngorogiannis
Differential Revision: D19743198
fbshipit-source-id: f90213109
Summary:
This diff fixes the clang translation for switch statement. It assumed that `default:` comes always
at last, which introduced some unreachable nodes inadvertently, e.g. when `default:` comes at first.
Reviewed By: dulmarod
Differential Revision: D19793138
fbshipit-source-id: 1e8b52c0d
Summary:
We already warn about lack of nullable annotations in `equals()`, and even have a specialized error message for that.
But lack of an annotation is not as severe as direct dereference: the
latter is a plain bug which is also a time bomb: it will lead to an NPE not immediately.
This is widespread enough to be reported separately.
Reviewed By: dulmarod
Differential Revision: D19719598
fbshipit-source-id: a535d43ea
Summary:
Since we fixed a bug in implementation of FalseOnNull (see stack below),
we can finally ship this change.
Side note: this change is essential for the follow up diff (which adds extra check
for user-defined implementations of equal()), without it the follow
up change would introduce a lot of false positives.
Reviewed By: ngorogiannis
Differential Revision: D19771057
fbshipit-source-id: 7d7cf1ef7
Summary:
If we managed to whitelist a function as TrueOnNull, we should teach
nullsafe the nullability of its arguments, otherwise it will ask not to
pass null here.
This fixes a silly FP warning, see the test.
Reviewed By: dulmarod
Differential Revision: D19770341
fbshipit-source-id: 0f861fae1
Summary:
Yay, the previous refactoring finally makes it possible to do some actual
changes to the code in `TypeCheck.ml`!
Changes in this diff:
1. Fixes the bug: TrueOnNull and FalseOnNull were working only for
static methods. Surpsingly nobody noticed that. It is because the first
argument for non-static method was `this`.
2. Behavior change: TrueOnNull/FalseOnNull were not working correctly
where there are several argumens. See the task attached for the example
of the legit usecase. Now the behavior is the following: if there are
several Nullable arguments infer nullability for all of them.
Reviewed By: skcho
Differential Revision: D19770219
fbshipit-source-id: 7dffe42cd
Summary:
This refactoring unblocks the changes in follow up diffs (plus fixes a
bug).
So what was happening?
Each comparison with null leads to CFG being splitted into two branches, one branch
is PRUNE(a == null) and another is PRUNE(a != null).
PRUNE(a != null) is where most of logic happens, it is the place where
we infer non-null nullability for a, and this is a natural place to
leave a check for redundancy.
Before this diff we effectively checked the same thing twice, and used
`true_branch` (only one of 2 instruction will have it set to true) as a symmetry breaker.
This diff removes the `true_branch` checks, but leaves only one call out
of two, hence breaking symmetry in a different way.
## Bug fix
The code around the removed check was (crazily) doing two things at
once: it processed results of (returning booleans!)
TrueOnNull-annotated functions AND
results of (returning Objects!) other functions, using the fact that all
of them are encoded as zero literals (sic!).
Not surprisingly that lead to a bug where we accidentally call the check
for non intended places (arguments of trueOnNull functions), which lead
to really weird FP.
This diff fixes it.
Reviewed By: dulmarod
Differential Revision: D19744604
fbshipit-source-id: fe4e65a8f
Summary:
The goals are:
- Increase precision in C-languages by ditching access paths.
- Help with eventually sharing the abstract address module with RacerD.
- Reports are now language-mode specific (eg `->` in clang vs `.` in Java).
It's not exactly access expressions used here. Instead the pattern `(base, access list)` is used where `access` is `HilExp.Access.t`. This is done to ease the way `deriving` is used for creating two comparison functions, one that cares about the root variable and one that doesn't; and also because the main function that recurses over accesses (`normalise_access_list`) visits the accesses from innermost to outermost.
Also, kill some dead code.
Reviewed By: skcho
Differential Revision: D19741545
fbshipit-source-id: 013bf1a89
Summary: We don't use allocation costs in prod at the moment. There is no plan to do so in the near future. Let's not report them anymore and also save some space in `costs-report.json`.
Reviewed By: skcho
Differential Revision: D19766828
fbshipit-source-id: 06dffa61d
Summary:
This diff adds a taint domain in Inferbo. The taint value will be used to find vulnerable array
accesses in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D19391028
fbshipit-source-id: 566b4c0fe
Summary:
This test tests PropagatesNullable and TrueOnNull/FalseOnNull
annotations.
Both tests suites grew big so it is hard to observe them at glance and
make changes.
I could not figure out better name for TrueFalseOnNull.java, it is sort
of silly but I optimized for searchability, "FalseOnNull" will be
directly searched and "TrueOnNull" will be searched in IDEs that are
smart enough.
Reviewed By: skcho
Differential Revision: D19724512
fbshipit-source-id: 703961342
Summary: This diff returns non-symbolic value (top) for unknown external function calls because the symbolic values sometimes make it hard to understand costs.
Reviewed By: ezgicicek
Differential Revision: D18685715
fbshipit-source-id: 1b39c718b
Summary:
Pulse has an extra invalidation mechanism (introduced in D18726203) to prevent something invalid (e.g. `null`) to be passed by reference to an initialisation function. Therefore, it havocs formals passed by reference to skipped functions. However, I don't think this makes sense in Java. So, let's turn it off.
A nice consequence of this is that in impurity analysis, we do not consider functions that call skipped library calls with object arguments as writing to their formals.
Reviewed By: skcho
Differential Revision: D19697110
fbshipit-source-id: 6e3a71f2a
Summary:
To emulate the `ThreadSafe` contract in C++/ObjC, reporting was gated behind a check that ensured a C++/ObjC class has a `std::mutex` member (plus other filters). This is reasonable, but it has some drawbacks
- other locks may be used, and therefore must be added to the member check;
- locking mechanisms that use the object itself as a monitor cannot be modelled (`synchronized` in ObjC)
RacerD already has `ThreadsDomain` which models our guess on whether a method is expected to run in a concurrent context, and which in C++/ObjC boils down to whether the method non-transitively acquires a lock. This should be a good enough indicator that the class should be checked regardless of whether the locks are member fields. This diff gates the C++/ObjC check on that abstract property.
Reviewed By: dulmarod
Differential Revision: D19558355
fbshipit-source-id: 229d7ff82
Summary:
Revert incomplete/incorrect translation of `synchronized` in ObjC.
The current translation is incomplete because
```
syncrhonized(foo){
return;
}
```
should be translated as
```
__set_locked_attribute(foo);
__delete_locked_attribute(foo);
return;
__delete_locked_attribute(foo);
```
but instead we get
```
__set_locked_attribute(foo);
return;
__delete_locked_attribute(foo);
```
The same applies for `break`/`continue` etc
Reviewed By: skcho
Differential Revision: D19718882
fbshipit-source-id: fc49ef529
Summary:
- Thread the two types into one instead of having a record where the `path` field doesn't always make sense (`Class` case).
- Improved pretty printing of class objects (java only).
- Move starvation-specific stuff out of `AbstractAddress` (eg `make_java_synchronized`).
- Slight optimisation of `apply_subst` for when a parameter is used without additional accesses inside a method (then, the substitution need not modify the term substituted for the parameter in any way).
Reviewed By: ezgicicek
Differential Revision: D19639922
fbshipit-source-id: 1cebecf5d
Summary:
`String` and `StringBuilder` both implement `CharSequence`. Let's generalize the model for `String` to `CharSequence` wherever possible and add missing models for
- `StringBuilder.append`
- `StringBuilder.toString`
Reviewed By: skcho
Differential Revision: D19558009
fbshipit-source-id: 0dfdb21af
Summary:
Java's String models were broken for
- initializing a String object with a locally defined constant string (which is an `Object*` in SIL).
- initializing a String object with a `char`/`byte` array
This diff fixes them and also adds models for `new String ()`.
Reviewed By: skcho
Differential Revision: D19662180
fbshipit-source-id: 23968d0aa
Summary: This diff fixes the array access checking function for nested global arrays. We had assumed that RHS of `store` statement in SIL does not include array access expression, but that is not true: for global arrays, SIL can have statements like `*LHS = GlobalArray[n][m]`.
Reviewed By: ezgicicek
Differential Revision: D19300153
fbshipit-source-id: 256325642
Summary:
This diff gives semantics of `std::make_shared` as simple constructor, i.e., it changes function
call of `std::make_chared<C>(i)` to the constructor `C(i)`.
Reviewed By: ngorogiannis
Differential Revision: D19432338
fbshipit-source-id: 0d838e555
Summary: This adds a check for when developers use weakSelf (and maybe strongSelf) in a block, when there is no need for it, because it won't cause a retain cycle. In general there is an annotation in Objective-C for methods that take blocks, NS_NOESCAPE, that means that the passed block won't leave the scope, i.e. is "no escaping". So we report when weakSelf is used and the block has the annotation.
Reviewed By: ngorogiannis
Differential Revision: D19662468
fbshipit-source-id: f5ac695aa
Summary:
Prevent returning a negative cost bound when calling `substring(begin_index, end_index)` when either is possible
- `begin_index < 0`
- `begin_index > end_index`
Instead, return unit cost since such cases either throw `IndexOutOfBoundsException ` at runtime or correspond to having two symbolic bounds that cannot be semantically compared.
Reviewed By: dulmarod
Differential Revision: D19619410
fbshipit-source-id: cf5e8cb7b
Summary:
The "access path" memory model (equal access paths iff equal object addresses) is suited to when aliasing occurs only at the roots (i.e. variables). When there is intentional aliasing in the middle of an access path, this model will miss the aliasing. For instance if `[x.f] == [y.g]`, then also `[x.f.h] == [y.g.h]`, but the latter access paths are unequal.
In Java, non-static inner classes consistently alias `this.this$0` inside an inner class, which points to the "parent" outer-class object. So if two inner-class objects (belonging to different inner classes) access `this(type:InnerClassA).this$0.f` and `this(type:InnerClassB).this$0.f` the equality will be missed (many other combinations exist). This isn't strictly due to the memory model -- any alias analysis would have to do some class invariant inference to detect this.
For this purpose `AccessPath.inner_class_normalize` exists (it replaces `this.this$0` with `this` of the appropriate type), but this breaks the invariant that we know which formal parameter is at the root (there may not even exist a `this` parameter if the method is static). So this was buggy.
Here we simply recursively remove the synthetic field prefix of the accesses list, while computing forwards the object type. This is only applied when we check aliasing across threads. This will also allow actuals/parameters substitutions (stacked diff) which normalisation was breaking.
Reviewed By: jberdine
Differential Revision: D19601455
fbshipit-source-id: 7e42667b6
Summary: The translation of closures includes a load instruction for the captured variable, then we add that corresponding id to the closure. This doesn't correspond to an actual "use" of the captured variable in the source program though, and causes false positives. Here we remove the ids from the domain when that id is being added to a closure.
Reviewed By: ngorogiannis
Differential Revision: D19557352
fbshipit-source-id: 52b426011
Summary:
- Add `Nullsafe` annotation as a general mechanism to specify
type-checking behaviour for nullsafe.
- Document annotation params and provide usage examples with
explanations.
- Add tests to demonstrate the behaviour with different type-checking
modes.
No implementation is added. This diff serves as an RFC to hash out the
details before I dive into code.
Reviewed By: ngorogiannis
Differential Revision: D19578329
fbshipit-source-id: b1a9f6162
Summary: `String.split(regexp)` returns an array that is split by the given regexp. If the regexp doesn't match, the original string is returned. Hence, the resulting array's length must be in `[1, max(1, n_u -1)]` where`n_u` is the upper bound of the string's length.
Reviewed By: dulmarod
Differential Revision: D19578318
fbshipit-source-id: 675af7376
Summary:
Adding a new check as part of the SelfInBlock checker, for cases when a strong pointer to self, that is not self, is captured in the block.
This will cover the following wrong scenarios:
1. strongSelf is a local variable in a block as it should be, and then it's used in a sub-block, in which case it's a captured variable.
2. weakSelf is defined without the weak attribute by mistake.
Reviewed By: ngorogiannis
Differential Revision: D19538036
fbshipit-source-id: 151871745
Summary:
In practice, condition redundant is extremely noisy and low-signal
warning (hence it is turned off by default).
This diff does minor tweaks, without the intention to change anything
substantially:
1/ Change severity to advice
2/ Change "is" to "might be"
3/ Describe the reason in case the origin comes from a method.
The short term motivation is to use 3/ for specific use-case: running nullsafe on codebase and
identify most suspicious functions (that are not annotated by often
compared with null).
Reviewed By: artempyanykh
Differential Revision: D19553571
fbshipit-source-id: 2b43ea0af
Summary: We were reporting strongSelf Not Checked when the variable was checked in a conditional, this diff fixes that.
Reviewed By: jvillard
Differential Revision: D19535943
fbshipit-source-id: f8e64e1b7
Summary: I noticed when looking into a false positive of strongSelf Not Checked, that there were some inconsistencies in the translation of if statements with an and, with an extra redundant join only if using a method in the condition that returned an object. So I could repro the problem and investigate and found the place of the inconsistency in the translation. This diff fixes it without changing things too much.
Reviewed By: jvillard
Differential Revision: D19518368
fbshipit-source-id: 47a6a778c
Summary:
The order by which the scheduler visits odd and even methods here
will determine if there is any report at all. This is a bad test
so remove.
Reviewed By: fgasperij
Differential Revision: D19535537
fbshipit-source-id: 6b64b0de9
Summary: Adding reporting to strongSelf Not Checked when strongSelf is passed to a method in a not explicitly nullable position.
Reviewed By: ezgicicek
Differential Revision: D19330872
fbshipit-source-id: 95871a70a
Summary: After receiving feedback about this, I'm changing the reporting of strongSelf Not Checked to only in cases where it can cause a crash. Here I'm adding reporting for field access, and removing general reporting. In a next diff, I'll also add reporting for passing strongSelf to methods in not explicitly nullable positions.
Reviewed By: skcho
Differential Revision: D19329842
fbshipit-source-id: 35beb2aa3
Summary:
1. One should use either a writer or a stream to send a response, but not both.
2. A response should be forwarded only if it was commited.
Both properties are extracted from API comments on classes in the servlet API.
Reviewed By: jvillard
Differential Revision: D19514568
fbshipit-source-id: 79f0257ed
Summary:
If data comes from an outer OutputStream, then this outer OutputStream
needs to be flushed before getting the byte array.
Reviewed By: jvillard
Differential Revision: D19514569
fbshipit-source-id: e3e025394
Summary: We were lacking this kind of test where one interface refines the nullability of the other.
Reviewed By: ngorogiannis
Differential Revision: D19514245
fbshipit-source-id: fa3e781f3
Summary:
This is a common enough case to make error message specific.
Also let's ensure it's modelled.
Reviewed By: artempyanykh
Differential Revision: D19431899
fbshipit-source-id: f34459cb3
Summary:
The previous diff changes the message for params case, this one handles
return.
Reviewed By: artempyanykh
Differential Revision: D19430706
fbshipit-source-id: f897f0e56
Summary:
This diff gets global constant array values from their initializers. The `find_global_array` function is
added to memory domain, which finds values of global array locations during the ondemand value
generation.
Reviewed By: ngorogiannis
Differential Revision: D19300143
fbshipit-source-id: 7b0b84c42
Summary: Use more informative method names, and add comments explaining the logic behind each test. Correct two cases which are FPs instead of legitimate reports.
Reviewed By: artempyanykh
Differential Revision: D19465227
fbshipit-source-id: 29332e2b9
Summary:
If a race exists in two or more overloads of the same method and we use only the class and method name in the report text, then the current bug hashing algorithm will identify the two reports as duplicates.
To avoid this, the report had the class, method and list of type parameters. This is unreadable, however, and redundant (the report is already located within the method in question). So at the risk of duplicates, use only class+method names.
Also, fix a bug in `Procname.pp_simplified ~withclass` where `withclass` was ignored for C++/ObjC methods.
Now:
> Read/Write race. Non-private method `FrescoVitoImageSpec.onCreateInitialState(...)` indirectly reads with synchronization from `factory.AnimatedFactoryProvider.sImpl`. Potentially races with unsynchronized write in method `FrescoVitoImageSpec.onEnteredWorkingRange(...)`.@ [Litho components are required to be thread safe because of multi-threaded layout](https://fburl.com/background-layout). Reporting because current class is annotated `MountSpec`, so we assume that this method can run in parallel with other non-private methods in the class (including itself).
Before
> Read/Write race. Non-private method `void FrescoVitoImageSpec.onCreateInitialState(ComponentContext,StateValue,StateValue,Uri,MultiUri,ImageOptions,FrescoContext,Object,ImageListener)` indirectly reads with synchronization from `factory.AnimatedFactoryProvider.sImpl`. Potentially races with unsynchronized write in method `FrescoVitoImageSpec.onEnteredWorkingRange(...)`.@ [Litho components are required to be thread safe because of multi-threaded layout](https://fburl.com/background-layout). Reporting because current class is annotated `MountSpec`, so we assume that this method can run in parallel with other non-private methods in the class (including itself).
Reviewed By: artempyanykh
Differential Revision: D19462277
fbshipit-source-id: aebc20d89
Summary:
Currently, impurity analysis is oblivious to skipped functions which might e.g. return a non-deterministic value, write to memory or have some other side-effect. This diff fixes that by relying on Pulse's skipped functions to determine impurity. Any unknown function which is not modeled to be pure is assumed to be impure.
This is a heuristic. We could have assumed them to be pure by default as well.
Reviewed By: jvillard
Differential Revision: D19428514
fbshipit-source-id: 82efe04f9
Summary:
As suggested by Ilya, the current message can be improved in a way that
it can contain more clear action. I also added artempyanykh's explanation at the
end of message to provide an additional justification from common sense
perspective.
But most importantly, the previous message was missing a space which is
eye bleeding, how come haven't I noticed this before, I can't stand it
OMG.
Reviewed By: artempyanykh
Differential Revision: D19430271
fbshipit-source-id: dd31f7adb
Summary:
Inferbo analyzed some program points unreachable incorrectly, because of unsound semantics of band
operator, which did not handle the case when given parameters are pointer values.
Reviewed By: ngorogiannis
Differential Revision: D19392705
fbshipit-source-id: dd590508c
Summary:
Introduce a new notion of equality for comparing abstract addresses in distinct threads:
```
(** Abstract address for a lock. There are two notions of equality:
- Equality for comparing two addresses within the same thread/process/trace. Under this,
identical globals and identical class objects compare equal. Locks represented by access paths
rooted at method parameters must have equal access paths to compare equal. Paths rooted at
locals are ignored.
- Equality for comparing two addresses in two distinct threads/traces. Globals and class objects
are compared in the same way, but locks represented by access paths rooted at parameters need
only have equal access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing
parameters in *distinct* threads. This relation is used in [may_deadlock]. *)
```
Reviewed By: skcho
Differential Revision: D19347307
fbshipit-source-id: 9f338731b
Summary:
This diff avoids that `array_sizeof` returns bottom value when given Java enum values, which
introduced unreachable code inadvertently.
Reviewed By: ngorogiannis
Differential Revision: D19409077
fbshipit-source-id: 2816fd995
Summary:
The property SkipAfterRemove already had a test, but not for
intra-procedural violations. This adds a test for that case.
Reviewed By: ngorogiannis
Differential Revision: D19330471
fbshipit-source-id: 1dd1c3ad7
Summary: This diff implements this for Field Not Initialized check
Reviewed By: artempyanykh
Differential Revision: D19393989
fbshipit-source-id: cf60e8d53
Summary: add subdirectories so that we can run each java file against its own topl properties
Reviewed By: rgrig
Differential Revision: D19347302
fbshipit-source-id: 562830774
Summary:
This diff does it for nullable dereference and assignment violations
rules which happen under NullsafeStrict case.
Follow up are to make the same for inheritance and field initializer
violations.
Possible follow up includes making error message more specific and
articulare this this is a nullsafe strict mode.
Reviewed By: artempyanykh
Differential Revision: D19392916
fbshipit-source-id: 2554ac7a7
Summary:
Previously, _override resolution_ considered only the number of
arguments. This led to many FPs in nullsafe's _Inconsistent Subclass
Annotation_ check.
Current version also checks that argument types match. However, we
still don't handle type parameters and erasure, so in this sense the
rules are incomplete.
Reviewed By: ngorogiannis, mityal
Differential Revision: D19393201
fbshipit-source-id: a0c75b8dd
Summary:
`diff` by default doesn't colorize its output, while `git diff`
does. Since we already depend on git it seems like a safe change and
brings some quality of life improvement while working with tests.
Reviewed By: ngorogiannis
Differential Revision: D19374691
fbshipit-source-id: 8872b527c
Summary:
`infer/tests/infer.make` unconditionally runs
```
$(call check_no_duplicates,$(INFER_OUT)/duplicates.txt)
```
as a part of `test` target. This requires the flag to be set to
produce `duplicates.txt`.
`clang.make` does this, but `java.make` was missing the flag which led
to an error on running `make tests` within
e.g. `tests/codetoanalyze/java/nullsafe-default`:
```
grep: infer-out/duplicates.txt: No such file or directory
```
Reviewed By: mityal
Differential Revision: D19373857
fbshipit-source-id: c2fcbe9dd
Summary:
This diff avoids that null-retuned path's abstract value ruins that of non-null-returned path.
What this diff does is: when joining two abstract states, one is null-return-path and the other is
non-null-return-path (`return obj;`), it keeps the method calls of `obj` from the
non-null-return-path.
While this design is unsound, I think it should work in practice.
Reviewed By: ezgicicek
Differential Revision: D19348313
fbshipit-source-id: cf5d0f3ff
Summary: This diff captures global initializers ondemand, like we do for functions defined in headers.
Reviewed By: ezgicicek
Differential Revision: D19346947
fbshipit-source-id: 05174e6a4
Summary:
Java treats switch on nullables in a non-obvious way (throws an NPE
surprise) so lets have a decidated test exactly for this.
Reviewed By: ngorogiannis
Differential Revision: D19371280
fbshipit-source-id: d9867b6d6
Summary:
Demonstrate that the per-file type environments don't prevent
the deadlock report here. The fear was that when the analyser
tries to locate the methods of the endpoint class, it might fail to
do so because the types might be stored in different type
environments (per file).
Reviewed By: mityal
Differential Revision: D19225908
fbshipit-source-id: 097e4aeea
Summary: This diff use actuall call path in the cost results instead of `class name + method name`.
Reviewed By: ngorogiannis
Differential Revision: D19194969
fbshipit-source-id: b72018586
Summary:
Model array length in Java as returning an unknown interval [0, +inf] for now.
Ideally, we can deal with the size in a more precise manner in the future like in InferBo.
Reviewed By: skcho
Differential Revision: D19312123
fbshipit-source-id: 8c51059a4
Summary: Pulse doesn't care about exceptions yet. With Exceptional CFG, java analysis takes a lot of time due to having many disjuncts. Let's use Normal CFG for now.
Reviewed By: jvillard
Differential Revision: D19194479
fbshipit-source-id: f94bb6078
Summary:
Kill these tests as that mode is not supported anymore.
Note that :
- "buck_cross_module" was effectively already dead since it's not hooked up to `make test`
- "buck" is actually another copy of "genrule" so wasn't testing anything
Reviewed By: ngorogiannis
Differential Revision: D19176166
fbshipit-source-id: b5bb90448
Summary:
This changes how we select amongst our (currently) 4 Buck integrations
for Java and clang, as well as how the user's choice is reflected by the
Config module.
The old command line interface is still supported but is now deprecated.
The changes in how to select each integration are:
- clang via "flavors", activated with `--flavors`, now with `--buck-clang`
- clang via "compilation DB", activated with `--buck-compilation-database`, unchanged
- Java via "genrule", activated with `--genrule-master-mode`, now with `--buck-java`
- Java "without genrules", used to be activated by *not specifying any other Buck mode*, unchanged
Instead of various `Config` flags corresponding to the previous CLI that
are allowed in any combination of `flavors`,
`buck_compilation_database`, `genrule_master_mode`, `Config` now exposes
a single `buck_mode` datatype. This allows, eg, `flavors` to override
`buck_compilation_database` if needed. It will also make it easier to
get rid of the old "Java without genrules" integration in a later diff
(see inline comments).
Reviewed By: ngorogiannis
Differential Revision: D19175686
fbshipit-source-id: 29b3831be
Summary:
In order to improve the impurity analysis, this diff adds models for
- `hasNext()` and - `Object.equals()` modeled as returning a non-deterministic value (havoc_id)
- `next()` modeled as `StdVector.get` with a fresh index
- `iterator` modeled as just returning the underlying list
Reviewed By: jvillard
Differential Revision: D19177392
fbshipit-source-id: 0babb037a
Summary:
This diff updates the relation between iterator (offset) and integer value not only at
assignments (`x += 1`), but also at function calls (`foo()`) that increase integer values by one in
their side effects.
Reviewed By: ezgicicek
Differential Revision: D19163214
fbshipit-source-id: 47e52f939
Summary: This diff extends the domain to express the relation between iterator's offset and integer value.
Reviewed By: ezgicicek
Differential Revision: D19143670
fbshipit-source-id: 6223bc934
Summary:
Old versions of sawja/javalib got the line numbers slightly wrong. The workaround was to do a regexp search in the source file for the right line.
My understanding is that this is no longer necessary. This diff removes it.
Reviewed By: jvillard
Differential Revision: D19033415
fbshipit-source-id: 2da19d66d
Summary:
This is an optimization. We ask the user to tell us which states are nondeterministic, and we
generate code that handle nondeterminism only for those states. It is common for only one state per
TOPL property to be nondeterministic. This speeds up the biabduction-analysis of the monitor by a
factor of ~10. But, using the monitor is only a little faster.
Facebook
Reviewed By: jvillard
Differential Revision: D19160286
fbshipit-source-id: 4dd39769a
Summary:
In the previous code, it removed non-build-called method calls. For example, it was like
```
{non-build-called: {prop1, prop3}}
{build-called: {}}
b.build();
{non-build-called: {}}
{build-called: {prop1, prop3}}
```
However, this behavior introduced a false positive when there is multiple builders that point to the
same abstract object and `build` is called one by one.
This diff changes the semantics to keep the method calls of non-build-called at `build` calls.
Reviewed By: ezgicicek
Differential Revision: D19144525
fbshipit-source-id: e2ace127f
Summary:
This applies some simplifications that were previously
done after footprint (and therefore lost), and some
simplifications that require looking at both pre and
post.
Reviewed By: ngorogiannis
Differential Revision: D19035494
fbshipit-source-id: bad79534a
Summary:
This havocs event data, so that biabduction doesn't try to
track what was the last event processed by the monitor
(which is redundant as long as the state of the monitor
is tracked).
Reviewed By: ngorogiannis
Differential Revision: D19035491
fbshipit-source-id: a1c75daae
Summary:
Don't instrument SIL when we can determine statically that
biabduction symexec would be a no-op.
Reviewed By: ngorogiannis
Differential Revision: D19116849
fbshipit-source-id: 4d25462a3
Summary: It is confusing to report missing props at the the beginning of the method (especially when there are many components created or when the method has many lines). Let's report them at create methods to better contextualize. Also, make the missing prop bold.
Reviewed By: skcho
Differential Revision: D19141135
fbshipit-source-id: a23d2e7c9
Summary:
In addition to
state1 -> state2: pattern
one can now also write
state1 -> state2: pattern if condition
where "condition" is some conjunction of comparisons (==,<,>) that
involve variables bound by "pattern", registers of the automaton, and
constants.
Reviewed By: ngorogiannis
Differential Revision: D19035496
fbshipit-source-id: 6f6e6a9be
Summary:
According to Java semantics, they are always non-null.
Internally they are represented as static fields, so they have
DeclaredNonnull nullability, which means NullsafeStrict mode would
refuse to use them without strictification.
Lets teach nullsafe that these guys are non-nullables.
See also FN in test case.
Reviewed By: ngorogiannis
Differential Revision: D19024547
fbshipit-source-id: 8c120fa50
Summary:
We do not have the create method in the trace which makes it difficult to understand
- inter-procedural issues where create and prop setting are in different methods
- there are multiple create-build chains in a method
Let's add the create to the beginning of the trace. Moreover, let's simplify the prop printing to make traces easier to understand.
Reviewed By: ngorogiannis
Differential Revision: D19020213
fbshipit-source-id: 7f8a5d4ec
Summary: The new domain is much better than the old one. Let's kill the old one (along with old litho tests) and simplify things.
Reviewed By: skcho
Differential Revision: D18959627
fbshipit-source-id: df77ae20e
Summary:
In order to handle the example added:
changed domain of `MethodCalled`
from `CreatedLocation -> (IsBuildCalled X IsChecked X Set(MethodCall))`
to `(CreatedLocation X IsBuildCalled) -> (IsChecked X Set(MethodCall))`
This avoids joining of two method calls where one is build-called and the other is not, e.g.,
```
if(b) {
o.build();
} else {
// no build call
}
```
changed domain of `NewDomain`
from `Created X MethodCalled`
to `(Created X MethodCalled) X (Created X MethodCalled)`
One is for no returned memory and the other is returned memory. This keeps precision some join
points of branches, e.g.,
```
if(b) {
return;
} else {
// no return
}
```
Reviewed By: ezgicicek
Differential Revision: D18909768
fbshipit-source-id: c39d1a1ef
Summary:
A plus is a plus, no need to give up when +/- is about pointers. This
gets rid of some false positives involving pointer arithmetic.
However, the problem remains if we make things a bit more
inter-procedural. This is documented in an added test.
Reviewed By: ezgicicek
Differential Revision: D18932877
fbshipit-source-id: 4ad1cfe72
Summary: It is not used anywhere and there are no plans to revive it. Kill it!
Reviewed By: skcho
Differential Revision: D18934719
fbshipit-source-id: b9b069b96
Summary:
The `Typ.FIeldname` module has many issues. Among those:
- It has 5 different string/printing functions and most of them do radically different things in Java and in Clang.
- There is no type safety: creating a Clang field and calling a Java function on it will lead to a crash (`rindex_exn` etc, there are usually no dots in Clang fields).
- It uses a single string for Java fields, containing the package, the class and the field, e.g., `java.lang.Object.field`. This is wasteful, because
- there is no sharing of strings for packages/classes, and,
- string operations need to be performed every time we need the field or the class or the package alone.
This diff preserves the behaviour of the module's interface, so the API problems remain.
However, by using a saner representation for Java fields we can get small performance and large memory gains (the type environment in Java is much smaller, about 30-40%).
In addition, many functions on clang fields would previously do string manipulations (look for `.` and split on it) before returning the final field unchanged -- now they use the type of the field for that.
Reviewed By: jvillard
Differential Revision: D18908864
fbshipit-source-id: a72d847cc
Summary:
- Do most of the work of `solve_arithmetic_constraints` inside `subst_attribute` instead, since we need to re-use the latter function for post-conditions where the first function is not appropriate.
- When substituting arithmetic constraints, we refine arithmetic information (both concrete intervals and inferbo), which can lead to inconsistent states. Instead of recording the new arithmetic facts by returning a new current state, just act as a map on attributes. This is to enable doing the point above.
- All this lead to a somewhat messy refactoring...
- Rename `CannotApplyPre` to `Contradiction` since it's used for post-conditions as well now
Reviewed By: skcho
Differential Revision: D18889120
fbshipit-source-id: d81647143
Summary: Guava uses assertions to ensure a future can be gotten without blocking (this means that if the future is not done, the app will crash). This diff teaches the starvation analyser about a number of such assertions, by treating them as assumes (since we don't care about exceptions).
Reviewed By: jvillard
Differential Revision: D18893427
fbshipit-source-id: 4d26a202b
Summary: A future is guaranteed not to block if `isDone()` has returned true first. Add logic for supporting that by remembering the objects that we have called `isDone` on and by making `assume` do the right thing with that knowledge. All this is achieved with the attribute domain.
Reviewed By: ezgicicek
Differential Revision: D18833901
fbshipit-source-id: 7f4ea0cd1
Summary:
When retrieving a value from a container, we previously had an arbitrary hack which would
- In java, give no ownership to the returned object (trying to be sound)
- In C++ give conditional ownership to the current method's first argument (trying to be complete, but doing it badly, as the first argument may not be the `this` object in a static method, or we might be accessing it through another parameter altogether).
Harmonise both by using the existing ownership of the container as ownership value for the returned object (leaning towards completeness).
Reviewed By: jvillard
Differential Revision: D18882800
fbshipit-source-id: f98f8d315
Summary:
Pointers are hard... The previous test had no chance of doing
initialisation of the pointer by reference and was in fact a false
negative (and still is, fix incoming). Renamed functions to stress the
false negative and added a test that is really (potentially) doing
pointer initialisation by reference.
Reviewed By: skcho
Differential Revision: D18888008
fbshipit-source-id: 1e72408c7
Summary:
This reverts commit 4fd6165d190bab32544f9f040b777565432c15b2.
We don't need to check for reporting each node anymore. It suffices to just check per function.
Reviewed By: skcho
Differential Revision: D18883833
fbshipit-source-id: 2591b3af3
Summary:
Making `MethodCalled` an inverted map from created location to method calls results in not being able to track a builder that is created in two different branches of a conditional with different types. Instead, we can make `MethodCalled` simply a map and also change `Created` to be a map from access paths to a set of created locations.
To deal with the case of setting a prop only in one branch, we need to ensure that whenever we call a create method, we add a binding to `MethodCalled` with an empty list of methods so that its intersection with a non-empty one is empty.
Reviewed By: skcho
Differential Revision: D18883097
fbshipit-source-id: b3464ca20
Summary: As long as the types match, it should be possible to call build on two components that are created at different locations.
Reviewed By: skcho
Differential Revision: D18881740
fbshipit-source-id: 356f9e168
Summary:
Finally use information from the inferbo intervals in pulse's domain to
make decisions about whether conditionals are feasible or not.
Reviewed By: skcho
Differential Revision: D18811193
fbshipit-source-id: d80a28657
Summary: Add a FN that is detected by the old domain but not the new one
Reviewed By: ngorogiannis
Differential Revision: D18854389
fbshipit-source-id: 9bdc90a6b
Summary: The map from `CreatedLocation` to `MethodCalls` already takes care of the association from create methods to their set props. `MethodCall` comparison should be oblivious the the receiver, otherwise, we risk mistakenly considering two props set at different locations as different.
Reviewed By: skcho
Differential Revision: D18829388
fbshipit-source-id: b5a0d628d
Summary: This diff check and report on every nodes. Problem of the previous design is that it has to report alarms only with the abstract memory of the exit node. However, the new abstract value becomes imprecise at every join points on the path to the exit node, since it is using inverted map, i.e., under-approximation on collecting called methods. As a solution, this diff report on every nodes where `.build` is called with the abstract memory at that node.
Reviewed By: ezgicicek
Differential Revision: D18809449
fbshipit-source-id: 4fd6165d1
Summary: Current method call comparison is too strong. As exemplified with the new test, one can also set the required prop by calling a version which contains the suffixes. The domain should take care of such cases now.
Reviewed By: skcho
Differential Revision: D18808869
fbshipit-source-id: 9f7672e75
Summary:
Sometimes clang9 does not return a boxing method (a name of function to apply), e.g., [@("str")].
To solve the issue, this diff uses "unknownSelector:" instead of giving up the translation.
Reviewed By: dulmarod
Differential Revision: D18831844
fbshipit-source-id: b9324ba39
Summary: This diff checks litho condition on the new abstract value. This is triggered with `--new-litho-domain`, but it is intra-procedural as of now.
Reviewed By: ezgicicek
Differential Revision: D18783203
fbshipit-source-id: 98570104e
Summary:
Also add logic for recognising excessive timeouts. Refactor the code
around timeouts a little.
Reviewed By: artempyanykh
Differential Revision: D18807836
fbshipit-source-id: df5a1b566
Summary:
`Object.wait()` must be called on a locked monitor and it releases the
lock immediately, as far as other threads are concerned
(it also magically re-takes the lock when the monitor is `notified`).
Starvation can only occur if the UI thread is waiting
a lock that is distinct to that being waited on.
The check present was over-approximate in that it was checking that there exists a lock held by the UI thread and the thread issuing the `wait`, but did not make sure that lock was *not* the one waited on.
Amusingly, the e2e test was correct, but the reporting code wasn't.
Reviewed By: dulmarod
Differential Revision: D18782919
fbshipit-source-id: b3b98239e
Summary: The clang plugin exports C++ mangled names in hashed form for perf reasons, so we need to hash the incoming mangled names in the profiler samples, so that we can compare them.
Reviewed By: skcho
Differential Revision: D18761842
fbshipit-source-id: 3072b5e33
Summary: Similar to constructor established attributes, we do the same here for static initializers. That is, attributes of static properties are injected into the initial state of every method.
Reviewed By: ezgicicek
Differential Revision: D18763192
fbshipit-source-id: 3879a27c5
Summary: Raises an error when weakSelf is used multiple times in a block. The issue is that there could be unexpected behaviour. Even if `weakSelf` is not nil in the first use, it could be nil in the following uses since the object that `weakSelf` points to could be freed anytime.
Reviewed By: skcho
Differential Revision: D18765493
fbshipit-source-id: 37fc652e3
Summary: This diff extends the bound domain to express multiplication of bounds in some simple cases.
Reviewed By: ezgicicek
Differential Revision: D18745246
fbshipit-source-id: 4f2dcb42c
Summary:
One standard way to schedule work is by starting a thread. We treat this by
- Treating invocations of `start` on a receiver with the `Runnable _` attribute as scheduling that runnable for parallel execution in the background (as opposed to on the UI thread).
- If `start` is used on an object of a subclass of `Thread` everything already works thanks to the `get_exp_attributes` function which will implicitly ascribe to an expression the attribute `Runnable _` if the expression points to an object with a known `run` method. This will even take care of some degree of dynamic dispatch, yay!
- If `start` is used on a `Thread` object which has been created with a constructor call provided with a `Runnable` argument, we have to appropriately model that constructor call, which is what is done in `do_call`.
Reviewed By: jvillard
Differential Revision: D18726676
fbshipit-source-id: 0bd83c28e
Summary:
A current blind spot is when object construction stores specific executors / runnables to object fields, which are then never mutated and accessed from normal methods. IOW the attributes established in the constructor are necessary to report properly inside a normal method (assuming these attributes are not invalidated by method code).
To achieve this, first we retain a subset of the final state attributes in the summary (only those that affect instance variables, in constructor methods). Then, when we analyse a non-constructor method:
- we analyse all constructors
- remove all attributes from the attribute map whose key is not an expression of the form `this.x. ...`
- re-localise all remaining keys so that they appear as rooted in the `this` local variable of the current procedure
- join (intersect) all such attribute maps
- use the result in place of initial state as far as the attribute map is concerned for the analysis of the current procedure, which can now start.
This means we can catch idioms that use side-effectful initialisation for configuring certain object fields like executors or runnables.
Reviewed By: jvillard
Differential Revision: D18707890
fbshipit-source-id: 42ac6108f
Summary: Another way to schedule work in android is by posting it to a `Handler`. A handler can be constructed out of the main looper, which forces it to schedule work on the UI thread. To model all this, we add syntactic models for getting the main looper and for creating handlers, and dataflow attributes for tracking that an expression is a looper/the main looper, or a handler constructed out of a looper.
Reviewed By: skcho
Differential Revision: D18706768
fbshipit-source-id: 7c46e6913
Summary:
New syntax f1 AND-WITH-WITNESSES f2 : predicate_on_both_witnesses()
This is needed for a linter to check that a macro is present, see the test.
Reviewed By: skcho
Differential Revision: D18735988
fbshipit-source-id: a3be75c5e
Summary:
This gets rid of false positives when something invalid (eg null) is
passed by reference to an initialisation function. Havoc'ing what the
contents of the pointer to results in being optimistic about said
contents in the future.
Also surprisingly gets rid of some FNs (which means it can also
introduce FPs) in the `std::atomic` tests because a path condition
becomes feasible with havoc'ing.
There's a slight refinement possible where we don't havoc pointers to
const but that's more involved and left as future work.
Reviewed By: skcho
Differential Revision: D18726203
fbshipit-source-id: 264b5daeb
Summary:
It's a well-known fact that pulse should know too. To avoid splitting
the abstract state systematically, only act if we know the pointer is
exactly 0 to avoid reporting a nullptr dereference on `free(x)`.
Reviewed By: ezgicicek
Differential Revision: D18708575
fbshipit-source-id: 1cc3f6908
Summary:
Turns out code uses atomics in important places, modelling it removes
FPs.
The tests are copied from biabduction and adapted and extended a bit. I
didn't implement compare_exchange primitives for now (plus, giving them
a sequential semantics like in biabduction is probably a bit cheeky).
Reviewed By: skcho
Differential Revision: D18708576
fbshipit-source-id: a3581b8a4
Daiva Naudziuniene
Qianyi Shu
Ezgi Çiçek
Sungkeun Cho
David Pichardie
Artem Pianykh
Dulma Churchill
Nikos Gorogiannis
Jules Villard
Mitya Lyubarskiy
Radu Grigore
Kfir Schindelhaim
Martin Trojer