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:
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:
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
Dulma Churchill
Nikos Gorogiannis
Radu Grigore
Artem Pianykh
Mitya Lyubarskiy
Sungkeun Cho
Ezgi Çiçek
Jules Villard
Kfir Schindelhaim