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:
Let's collect the list of all skipped functions with a `proc_name` but no summary in Pulse's memory. This will be useful for the impurity analysis later (next diff).
Concretely, we extend Pulse's domain with a map from skipped calls to their respective traces. For efficiency, we only keep a single trace per skipped call.
For impurity analysis, tracking skipped calls in Pulse allows us to rely on Pulse's strong memory model to get rid of infeasible paths as opposed to creating an independent checker which wouldn't be able to do that.
Reviewed By: jvillard
Differential Revision: D19428426
fbshipit-source-id: 3c5e482c5
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:
This diff revises the generation of unknown value. If the type of the unknown value generating is
int, it does not add the "Unknown" pointer/array value.
Reviewed By: ngorogiannis
Differential Revision: D19392696
fbshipit-source-id: e1b3c9a3a
Summary: In impurity analysis, pick up the pulse summary rather than re-analyzing. Re-order the checkers so that we first analyze pulse.
Reviewed By: jvillard
Differential Revision: D19448296
fbshipit-source-id: 2987fa848
Summary:
This diffs does: (1) move `get_formals` to `BufferOverrunUtils` (2) use separate `get_formals` in
`BufferOverrunChecker`, in order to simplify the following diff.
Reviewed By: jvillard
Differential Revision: D19432280
fbshipit-source-id: bfb4df118
Summary:
The restart scheduler will now have two phases:
1. Analyze all the procs obtained from the sources.
2. Run the FileScheduler on the sources.
The second step aims to analyze only the File level analyzers
requirements.
Reviewed By: ngorogiannis
Differential Revision: D19430244
fbshipit-source-id: b4f9ee69b
Summary: `dune build check` will compile all the ml files much quicker than `dune build`
Reviewed By: jvillard
Differential Revision: D19427864
fbshipit-source-id: 5221d32bc
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
Ezgi Çiçek
Mitya Lyubarskiy
Sungkeun Cho
Jules Villard
Fernando Gasperi Jabalera
Nikos Gorogiannis
Josh Berdine
Radu Grigore
Artem Pianykh
David Pichardie