Summary:
An invariant of `And` and `Or` formulas is that they are flattened,
that is, `And` formulas do not have positive immediate subformulas of
form `And` nor negative immediate subformulas of form `Or`, and
similarly for `Or`. This invariant is ensured by the formula
constructors, which scan the immediate subformulas for cases that need
to be flattened.
When mapping over formulas, this repeated scanning is a performance
bottleneck. Most of the work of flattening is wasted since the input
formulas are necessarily already in flattened form, and the common
case is that the transformation preserves the flattened form. This
diff optimizes this case by detecting violations of flattening during
the transformation, performing the needed flattening, and avoiding the
general constructor that scans for flattening violations.
Reviewed By: jvillard
Differential Revision: D26338014
fbshipit-source-id: 9f15cca58
Summary:
Update the first-order equality solver for the sequence theory to
avoid searching the whole representation now that the super-term index
is maintained.
Reviewed By: jvillard
Differential Revision: D26338015
fbshipit-source-id: 24a9a19b6
Summary:
Similarly to terms, use the Comparar interface of Sets to defined
formulas using recursive types instead of recursive modules.
Reviewed By: jvillard
Differential Revision: D26250512
fbshipit-source-id: 84f0ae8c0
Summary: No functional change, just to make the interface easier to read
Reviewed By: jvillard
Differential Revision: D26250513
fbshipit-source-id: f3b07bccc
Summary:
Terms include Arithmetic terms, which are polynomials over terms
themselves. Monomials are represented as maps from
terms (multiplicative factors) to integers (their powers). Polynomials
are represented as maps from monomials (indeterminates) to
rationals (coefficients). In particular, terms are represented using
maps whose keys are terms themselves. This is currently implemented
using recursive modules.
This diff uses the Comparer-based interface of Maps to express this
cycle as recursive *types* rather than recursive *modules*, see the
very beginning of trm.ml. The rest of the changes are driven by the
need to expose the Arithmetic.t type at toplevel, outside the functor
that defines the arithmetic operations, and changes to stage the
definition of term and polynomial operations to remove unnecessary
recursion.
One might hope that these changes are just moving code around, but due
to how recursive modules are implemented, this refactoring is
motivated by performance profiling. In every cycle between recursive
modules, at least one of the modules must be "safe". A "safe" module
is one where all exposed values have function type. This allows the
compiler to initialize that module with functions that immediately
raise an exception, define the other modules using it, and then tie
the recursive knot by backpatching the safe module with the actual
functions at the end. This implementation works, but has the
consequence that the compiler must treat calls to functions of safe
recursive modules as indirect calls to unknown functions. This means
that they are not inlined or even called by symbol, and instead
calling them involves spilling registers if needed, loading their
address from memory, calling them by address, and restoring any
spilled registers. For operations like Trm.compare that are a handful
of instructions on the hot path, this is a significant
difference. Since terms are the keys of maps and sets in the core of
the first-order equality solver, those map operations are very very
hot.
Reviewed By: jvillard
Differential Revision: D26250533
fbshipit-source-id: f79334c68
Summary:
No functional change, apart from a minor change in invariant checking
for core constructors. Only to reduce diffs of upcoming changes.
Reviewed By: jvillard
Differential Revision: D26250518
fbshipit-source-id: a731e4fd6
Summary:
Inline functor applications, principally those involved in the
representation of (arithmetic) terms. This enables direct calls to
functions in the result of functor applications, instead of indirect
via an offset from the start of the module block resulting from the
functor appication. This also then enables further inlining
opportunities.
Reviewed By: jvillard
Differential Revision: D26338016
fbshipit-source-id: 27b770fa3
Summary: Also add support for deriving compare, equal, and sexp.
Reviewed By: ngorogiannis
Differential Revision: D26250524
fbshipit-source-id: b47787a9c
Summary:
A comparer `('a, 'compare_a) t` for type `'a` is a "compare" function
of type `'a -> 'a -> int` tagged with a phantom type `'compare_a`
acting as a singleton type denoting an individual compare function.
The point of these is to enable writing type definitions of containers
that depend on a compare function prior to applying a functor. For
example, a type of sorted lists could be exposed as:
```
type elt
type (elt, 'compare_elt) t = private elt list
```
and the operations manipulating sorted lists would be defined by a
functor that accepts a `Comparer.S` and implements the operations
using
```
let compare = (comparer :> elt -> elt -> int)
```
Reviewed By: ngorogiannis
Differential Revision: D26250528
fbshipit-source-id: ea61844ec
Summary: `make debug` should not be the same as `make release`
Reviewed By: ngorogiannis
Differential Revision: D26451307
fbshipit-source-id: 1bf924f92
Summary: No functional change, just to reduce diffs of upcoming changes.
Reviewed By: ngorogiannis
Differential Revision: D26250543
fbshipit-source-id: a14b6f4b0
Summary:
These links have changed it seems. Also delete the mini-table of
contents at the top of the Hello, World! page as docusaurus now produces
a nice (and up to date!) one automatically.
Reviewed By: skcho
Differential Revision: D26544300
fbshipit-source-id: 664a0eea1
Summary:
These pages are not referenced from anywhere and are stale, oops! We
even linked to checker-bug-types from our footer on all pages... These
pages are stale and replaced with auto-generated ones now.
Reviewed By: skcho
Differential Revision: D26544298
fbshipit-source-id: c3b7742b8
Summary: No need to keep more than one version + next version around.
Reviewed By: skcho
Differential Revision: D26544299
fbshipit-source-id: 1aff562cf
Summary:
Links to pages in static resources have been broken for a while it
seems: Docusaurus generates a Page not Found error for them, then
refreshing the URL loads the page properly... This is because of wrong
routing from the Docusaurus Single-Page App.
See https://github.com/facebook/docusaurus/issues/3309
A suggested workaround is to prepend `pathname://` in front of each link
not managed by docusaurus. This makes the page open in a new tab, which
is actually quite ok for our use cases: OCaml API docs and man pages.
Reviewed By: skcho
Differential Revision: D26544273
fbshipit-source-id: 2ed86ca4f
Summary:
This resolves a few instances of false negatives; typically:
```
if (x == y) {
// HERE
*x = 10;
*y = 44;
// THERE
}
```
We used to get
```
HERE: &x->v * &y ->v' * v == v'
THERE: &x->v * &y ->v' * v == v' * v |-> 10 * v' |-> 44
```
The state at THERE was thus inconsistent and detected as such (v` and
`v'` are allocated separately in the heap hence cannot be equal).
Now we normalize the state more eagerly and so we get:
```
HERE: &x->v * &y->v
THERE: &x->v * &y->v * v |-> 44
```
Reviewed By: skcho
Differential Revision: D26488377
fbshipit-source-id: 568e685f0
Summary:
There should be no equalities relevant to the precondition to
canonicalize against in the first place: equalities come either from
assignments (hence strictly to the post condition) or from PRUNE
statements, and we don't use the latter to canonicalize states anyway.
Reviewed By: skcho
Differential Revision: D26488378
fbshipit-source-id: 7923f71ea
Summary:
This was a correctness issue as nothing guarantees that bindings are in
a specific order. The following commit violates that assumptions and
made the impurity tests fail without this change.
Reviewed By: ezgicicek
Differential Revision: D26488379
fbshipit-source-id: e9cc41147
Summary:
Pretty minor, it's more convenient to make it return the state and will
be used in a later diff when that function will actually sometimes
modify the state.
Reviewed By: skcho
Differential Revision: D26488376
fbshipit-source-id: a21eaf008
Summary:
Instead of recording some facts as "known" (i.e., observed assignments),
record them as "pruned". This should be done any time the fact is not an
assignment, for instance when path-splitting on "is the argument =0?" as
in the model of `free()`.
Reviewed By: ezgicicek
Differential Revision: D26450362
fbshipit-source-id: 4fc980f90
Summary:
Using more than the "known" part of the arithmetic could accidentally
leak "pruned" information into certain facts.
I noticed this when adding more term equality reasoning to pulse in
another diff. At the moment this has little effect but is still more
correct conceptually.
Reviewed By: ezgicicek
Differential Revision: D26450333
fbshipit-source-id: eb31da344
Summary:
These were present for `std::optional` but not `folly::Optional` for
some reason.
Reviewed By: da319
Differential Revision: D26450400
fbshipit-source-id: 45051e828
Summary:
ClangWrapper.ml was skipping clang commands that didn't capture
by default. It was using the 'skip_analysis_in_path_skips_compilation'
flag to NOT skip commands. This is a confusing use of that flag.
Default should be to run clang (in case it does something useful),
and a new flag to disable this.
Reviewed By: ngorogiannis
Differential Revision: D26459100
fbshipit-source-id: 7f2e9a269
Summary: In Objective-C, `static const int var = ..` is not recognized as ICE (integral constant expression) unlike C++. To handle such loads better, this diff adds a check for `constant_global_array` as a workaround.
Reviewed By: skcho
Differential Revision: D26369461
fbshipit-source-id: e2dae11f1
Summary:
Races in Nullsafe classes can undermine NPE safety despite the class passing the type checks.
This diff adds to the report text of THREAD_SAFETY_VIOLATION and GUARDEDBY_VIOLATION the following trailer:
> Data races in `Nullsafe` classes may still cause NPEs.
This only happens if the race is directly on a non-primitively-typed member field of the class.
It also uses distinct bug types (adds the suffix _NULLSAFE to the bug types above) for easier accounting.
Reviewed By: ezgicicek
Differential Revision: D26403274
fbshipit-source-id: 3cd6ca082
Summary: As there are no dependencies between procedure and file analyses in RacerD, split them into separate modules.
Reviewed By: ezgicicek
Differential Revision: D26198874
fbshipit-source-id: 032aad9d8
Summary:
The `--pulse-model-return-nonnull` config option currently works for C++. Now we
will be using it also for Java. Changing type from string list to regexp to
make it more general.
Reviewed By: ezgicicek
Differential Revision: D26367888
fbshipit-source-id: 9a06b9b32
Summary:
Modeling Java instanceof operator in Pulse. This
implementation does not yet provide the proper semantics for instanceof.
For now, it will always return true. This is temporary and should reduce the false positive rate.
Reviewed By: da319
Differential Revision: D26317089
fbshipit-source-id: 494e3dec5
Josh Berdine
Jules Villard
Sungkeun Cho
Mitya Lyubarskiy
Gabriela Cunha Sampaio
Adam Ernst
Martin Trojer
Ezgi Çiçek
Nikos Gorogiannis
Joshua Selbo
Loc Le