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: Access expressions can appear in casts, or sometimes other constructors, inside a `HilExp.t`. Extraction of the access expression can ignore those wrappers. Introduce a single function for doing that throughout the analyser.
Reviewed By: ezgicicek
Differential Revision: D19410673
fbshipit-source-id: a724cb466
Summary:
It is necessary to normalize subterms of Memory and Concat terms or
else Equality.entails_eq is incomplete. They ought to be Interpreted,
but the solver for the byte-array theory is not yet ready for that.
Reviewed By: ngorogiannis
Differential Revision: D19282635
fbshipit-source-id: c06b6ca6d
Summary:
The equality relation is implied by the pure part, so cannot involve
more variables. Also, Sh.invariant checks that the equality relation
does not contain unbound variables.
Reviewed By: ngorogiannis
Differential Revision: D19282641
fbshipit-source-id: 21dd37a3b
Summary:
If `Term.solve_zero_eq` is passed `for_`, then that subterm is solved
for.
Reviewed By: ngorogiannis
Differential Revision: D19282647
fbshipit-source-id: 5d5b76af5
Summary:
Match the `x` suffix naming convention of Term pp functions that take
a classification function.
Reviewed By: ngorogiannis
Differential Revision: D19282639
fbshipit-source-id: fc340e4bc
Summary:
Equality relies on the result of solving an equation to be a "solution
substitution". In constrast to unconstrained Map's, solution
substitutions are idempotent and have constraints on the terms that
may appear in their domain (they must be "maximal solvables", that is,
variables or uninterpreted function applications, which would be
variables if explicit "variable abstraction" was done).
This diff factors out the manipulation of concrete Map's into a
Equality.Subst module, and uses these for the result of `solve`.
Reviewed By: ngorogiannis
Differential Revision: D19282637
fbshipit-source-id: 4fc825e59
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:
Now we can either disable it, or enable it only.
For integrations that disable it, this will allow to enable it for
NullsafeStrict classes without enabled it fully
Reviewed By: artempyanykh
Differential Revision: D19409131
fbshipit-source-id: a2b1fe650
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: In whole-program mode, analysing a method requires analysing first all constructors of the same class. This is not needed in normal mode, so gate that computation under `starvation_whole_program` for efficiency.
Reviewed By: artempyanykh
Differential Revision: D19393412
fbshipit-source-id: 2277e6b5e
Summary:
The RestartScheduler now uses it's own of_list function to build a
ProcessPool.TaskGenerator to be able to use a queue as the underlying
data structure.
Reviewed By: ngorogiannis
Differential Revision: D19390055
fbshipit-source-id: d57b493b7
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:
That was used only by the now-defunct Java Buck integration without
genrules.
Reviewed By: ngorogiannis
Differential Revision: D19176545
fbshipit-source-id: 8253b614a
Summary:
You should use `--buck-java` instead, which uses the new "genrule
master" integration.
This diff makes it impossible to select the previous integration.
Upcoming diffs will clean up the resulting dead code.
This also make infer fail hard when no buck mode is specified in a buck
capture command, eg `infer -- buck build //foo:foo`. The reason is that
we need to choose between 3 incompatible integrations and making any of
them the default will confuse at least one person in the future.
Reviewed By: ngorogiannis
Differential Revision: D19176391
fbshipit-source-id: 707d18b50
Summary:
These changes introduce the RestartScheduler which for now is a copy of the FileScheduler:
- added it as a possible argument to the recently added `--scheduler` option.
- made the necessary changes in `InferAnalyze` to call it if it was chosen.
Reviewed By: ngorogiannis
Differential Revision: D19373505
fbshipit-source-id: 98f065057
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:
Javalib 3.2 brings new features to rewrite
class files and emulate lambdas with regular Java
classes and interfaces. This diff just updates
infer opam depencies.
Reviewed By: ngorogiannis
Differential Revision: D19343539
fbshipit-source-id: d22674ac7
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: The type-name definition for Java can be potentially improved (eg increase sharing, or comparison speed, much like `QualifiedCppName`) by switching away from `Mangled.t` which is essentially a string. First step is to abstract the type.
Reviewed By: jberdine
Differential Revision: D19087508
fbshipit-source-id: 91a81f63b
Summary: Now that we have the kind of lock stored (global/class obj/path rooted at parameter), use it for comparison/equality, while ignoring the root variable of the access path, which is only used for printing.
Reviewed By: skcho
Differential Revision: D19346801
fbshipit-source-id: c65661dc6
Summary:
In preparation for constructing solution substitutions in solve, which
are closely tied to Equality.
Reviewed By: ngorogiannis
Differential Revision: D19282640
fbshipit-source-id: ca0f8ae29
Summary:
Identifying and separating one of the monomials in a polynomial, and
solving an equality for it, is much more dependent on the
representation of polynomial terms than the rest of solve.
Reviewed By: ngorogiannis
Differential Revision: D19282645
fbshipit-source-id: 645191ae0
Summary: Add command line option that directs racerd to treat all return values from unknown code (including abstract methods) as owned objects. This is essentially treating return values with full angelicism
Reviewed By: artempyanykh
Differential Revision: D19368375
fbshipit-source-id: 6a10153fa
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:
This diff changes the build target from `install-with-libs` to `install` since the former has been
removed.
https://github.com/facebook/infer/issues/1207
Reviewed By: ngorogiannis
Differential Revision: D19272627
fbshipit-source-id: be730c1b7
Summary:
The exposed constructors for Memory and Concat Terms are only used in
a very special idiom: to construct an equality between a single Memory
chunk and the Concat of multiple Memory chunks. This diff specializes
and simplifies by exposing a Term.eq_concat constructor for this
idiom, and removes the underlying Term.memory and Term.concat
constructors.
Reviewed By: ngorogiannis
Differential Revision: D19221866
fbshipit-source-id: 4842737d2
Summary:
Trace.infok is like Trace.info but accepts a polymorphic printf
continuation instead of directly taking a format string and its
args. This is useful to write wrappers such as:
```
let trace k = [%Trace.infok k]
```
Reviewed By: ngorogiannis
Differential Revision: D19221883
fbshipit-source-id: 88e939b26
Summary:
The size of Splats is redundant, as they always appear as subterms of
a Memory chunk or a heap segment, both of which are sized.
Reviewed By: ngorogiannis
Differential Revision: D19221870
fbshipit-source-id: 74044d1ad
Nikos Gorogiannis
Sungkeun Cho
Ezgi Çiçek
Josh Berdine
Radu Grigore
Mitya Lyubarskiy
Jules Villard
Fernando Gasperi Jabalera
Artem Pianykh
David Pichardie