Summary: Rework the intrinsic name detection to detect e.g. llvm.memset.*
Reviewed By: jvillard
Differential Revision: D25146150
fbshipit-source-id: 85ebcfb7a
Summary:
Rename the existing exec_intrinsic that works for calls to intrinsic
functions to exec_intrinsic_func to make room for an exec_intrinsic
that works on intrinsic instructions.
Reviewed By: jvillard
Differential Revision: D25146166
fbshipit-source-id: 80ae3aac9
Summary:
The translation of instruction intrinsics that are `Invoke`d is almost
the same as those that are `Call`ed. The same Llair instruction is
produced, but it is wired into the CFG differently. This diff uses the
translation of instruction intrinsics used for `Call`s for `Invoke`s
as well.
Reviewed By: jvillard
Differential Revision: D25146159
fbshipit-source-id: 85a93d915
Summary:
The code that computes the number of actuals is largely duplicated
between the Call and Invoke cases. But some issues have been fixed in
each that ought to be applied to the other. This factors out and
unifies this computation.
Reviewed By: jvillard
Differential Revision: D25146149
fbshipit-source-id: 78552327a
Summary:
Move the translation of Calls to intrinsics that map to instructions
into a separat function.
No functional change.
Reviewed By: jvillard
Differential Revision: D25146169
fbshipit-source-id: 79c640344
Summary:
Currently intrinsics are treated as functions, with Call instructions
to possibly-undefined functions with known names. This diff adds an
Intrinsic instruction form to express these more directly and:
- avoid the overhead of intrinsics needing to end blocks
- avoid the overhead of the function call machiery
- avoid the complexity of doing the string name lookup to find their
specs, repeatedly
This diff only adds the backend support, the added Intrinsic
instructions are not yet generated by the frontend.
Reviewed By: jvillard
Differential Revision: D25146155
fbshipit-source-id: f24024183
Summary:
Previously, when LLAIR was in SSA form, blocks took parameters just
like functions, and it was sometimes necessary to partially apply a
block to some of the parameters. For example, blocks to which function
calls return would need to accept the return value as an argument, and
sometimes immediately jump to another block passing the rest of the
arguments as well. These "trampoline" blocks were partial applications
of the eventual block to all but the final, return value,
argument.
This partial application mechanism meant that function parameters and
arguments were represented as a stack, with the first argument at the
bottom, that is, in reverse order.
Now that LLAIR is free of SSA, this confusion is no longer needed, and
this diff changes the representation of function formal parameters and
actual arguments to be in the natural order. This also brings Call
instructions in line with Intrinsic instructions, which will make
changing the handling of intrinsics from Calls to Intrinsic less
error-prone.
Reviewed By: jvillard
Differential Revision: D25146163
fbshipit-source-id: d3ed07a45
Summary:
Overwritten variables in move instructions are not impossible. Since
Domain_itv does not handle them, the check should be a `todo` rather
than an `assert false`.
Reviewed By: jvillard
Differential Revision: D25146168
fbshipit-source-id: 13d8587c7
Summary:
It was possible for the scope of a local to be incorrectly restored
when entering it for the first time in a caller after is was shadowed
by a callee. This could happen because scope management in the
analysis relies on renaming variables to adjust the vocabulary of
symbolic states. This was usually done, but optimizations of renaming
with a substitution whose domain is disjoint from the vocabulary of a
formula inadvertantly violated this vocabulary-adjustment
assumption. (Yes, this is too easy to get wrong.)
Reviewed By: jvillard
Differential Revision: D25146162
fbshipit-source-id: 30f2d657f
Summary:
These are not simply handled by `@deriving` since:
- These types are recursive and so some fields need to be ignored
- Some are uniquely identified by one of their fields
- Some fields are mutable, but set only during construction, and need
to be considered by compare, equal, hash, but ppx_hash refuses.
Reviewed By: jvillard
Differential Revision: D24989064
fbshipit-source-id: 7f8d699e5
Summary:
The use of realpath on paths obtained from debug info and the current
working directory is application-usage-specific behavior that does not
belong in the backend library. This diff moves these uses to the
frontend and cli, respectively. Also, the use of realpath in the
frontend is memoized along the same lines as the other frontend
translation functions.
This was also the last use of `core` in the `sledge` library, so the
dependency is moved to `sledge_cli` and `sledge_report`.
Reviewed By: ngorogiannis
Differential Revision: D24989070
fbshipit-source-id: c21b275f5
Summary:
Currently __llair_choice is left undefined, and so executed as skip.
This has the correct behavior, but makes it hard to distinguish from
calls to unintentionally-undefined procedures.
Reviewed By: ngorogiannis
Differential Revision: D24989068
fbshipit-source-id: f62981857
Summary:
Use B/K/M/G/... units for memory quantities, round percentages to 2
decimal places, and robustly detect deltas of close to zero.
Reviewed By: ngorogiannis
Differential Revision: D24989063
fbshipit-source-id: 35f0bccfb
Summary:
Instructions that have multiple specs sometimes have inconsistent
footprints for one or more of their specifications. In such cases, the
handling of the existential and universal vocabularies was sometimes
incorrect before this diff. In particular, the ghosts of a spec need
not appear in the pure approximation of the footprint, which the
previous code incorrectly assumed. Also, the unit of disjunction is
`false` with an empty vocabulary, not the precondition's vocabulary as
the previous code incorrectly used.
Reviewed By: ngorogiannis
Differential Revision: D24989067
fbshipit-source-id: eca3bff55
Summary:
Change `-llair-output` to `-output`, for binary form, and
`-llair-txt-output` to `-llair-output`, for textual form. Also
correspondingly change `.llair` to `.bllair`, for binary, and
`.llair.txt` to `.llair` for text.
This improves command line argument completion, and makes `.llair` the
extension of the files most commonly interacted with.
Reviewed By: ngorogiannis
Differential Revision: D24951506
fbshipit-source-id: ad4c73ca2
Summary:
The `seq` name of this field refers to the expected sort of it's
value, where the others refer to the role they play. So rename
seq (for sequence) to cnt (for contents).
Reviewed By: ngorogiannis
Differential Revision: D24951507
fbshipit-source-id: fd6640517
Summary: It is too easy to mix up multiple arguments of the same type.
Reviewed By: jvillard
Differential Revision: D24934116
fbshipit-source-id: 6e595b26e
Summary:
Global constants have reliable types, and their sizes can be used
instead of storing the size of the initializer separately.
Reviewed By: jvillard
Differential Revision: D24934114
fbshipit-source-id: 2426ab5be
Summary:
In practice this has not been observed to matter so far, since
treating `Splat N` as interpreted or uninterpreted does not matter
when `N` is a literal constant, and code seen so far only uses `Splat`
for zero initializers or memset with literal constant bytes.
Reviewed By: jvillard
Differential Revision: D24934118
fbshipit-source-id: 213e9724e
Summary:
0 and Splat 0 need to be treated the same since code relies on knowing
that 0 consists of all-0 bytes, and extracting a subsequence of a
Splat 0 yields 0. For example, initializing a struct to all-zeros and
then reading a member of pointer type out of it needs to produce the
null pointer. Therefore 0 and Splat 0 are redundant representations,
and all uses of Splat need to be updated to also handle 0.
This unfortunately leads to some near code duplication that seems to
be necessary. The issue is that 0 and Splat 0 are, from the backend's
perspective, constants in two distinct theories. Since 0 is chosen
over Splat 0 as the representation, the sequence theory solver needs
to treat 0 as if it was Splat 0, which duplicates some code handling
the general Splat cases.
Reviewed By: jvillard
Differential Revision: D24920758
fbshipit-source-id: 7c02be62b
Summary:
Global variables and function names in LLAIR are constant and so do
not need to be handled like normal assignable or shadowable
variables. This diff does this by changing the translation from LLAIR
to FOL to map globals and functions to uninterpreted constants instead
of variables.
Reviewed By: jvillard
Differential Revision: D24886571
fbshipit-source-id: efb8c9f49
Summary:
Localizing the entry of a procedure needs the globals (that the
procedure uses), but later creating a summary does not.
Reviewed By: jvillard
Differential Revision: D24886570
fbshipit-source-id: 8a7b18c58
Summary:
The computation of provable reachability through the heap currently
uses a set of variables whose values are either determined by the
desired roots or by the heap constraints. This requires globals to be
treated as variables. In preparation for distinguishing globals from
variables, this diff changes the reachability computation to use a set
of atomic terms instead of variables.
Reviewed By: jvillard
Differential Revision: D24886573
fbshipit-source-id: c0e6763b6
Summary:
No functional change, only simplifiying and making easier to
generalize.
Reviewed By: jvillard
Differential Revision: D24886572
fbshipit-source-id: e487b815d
Summary:
The general xlate_value function can be used in place of
xlate_func_name.
Reviewed By: jvillard
Differential Revision: D24846677
fbshipit-source-id: 603ebd388
Summary:
Calling an inline asm function that might raise is not currently
supported.
Reviewed By: jvillard
Differential Revision: D24846675
fbshipit-source-id: a7cfe6050
Summary:
Mangled names start with _Z, so only demangle those names. This leaves
unmangled C names alone.
Reviewed By: jvillard
Differential Revision: D24846674
fbshipit-source-id: d239a61aa
Summary:
Distinguish expressions that name globals from registers. This leads
to clearer code, and globals are semantically distinct from general
registers. In particular, they are constant, so any machinery for
handling assignment does not need to consider them. This diff only
adds the distinction to LLAIR, it is not pushed through to FOL, which
will come later.
Reviewed By: jvillard
Differential Revision: D24846676
fbshipit-source-id: 3aca025bf
Summary:
This module represents the definition of a global constant, rather
than the global itself.
Reviewed By: jvillard
Differential Revision: D24846673
fbshipit-source-id: d47e67984
Summary:
Distinguish expressions that name functions from registers. This leads
to clearer code, and function names are semantically distinct from
general registers. In particular, they are constant, so any machinery
for handling assignment does not need to consider them. Unlike general
globals, they never have initializer expressions, and in particular
not recursive initializers. This diff only adds the distinction to
LLAIR, it is not pushed through to FOL, which will come later.
Reviewed By: jvillard
Differential Revision: D24846672
fbshipit-source-id: 2101f353f
Summary:
LLVM and Llair use a form of records, in particular for values of
constant structs and arrays. In Llair, these use standard `select` and
`update` operations a la McCarthy's theory of functional arrays, with
a compact `record` operation for constructing complete records. This
is fine and logically well-understood. The issue is that once
constructed, these values are accessed using instructions that (may)
operate over byte-ranges, rather than struct member indices. The
backend uses a theory of sequences to represent such values (the
contents of memory). So some code depends on high fidelity
interoperation between these two views.
This diff resolves this by removing the record theory from the backend
and instead encoding them using the sequence theory. The approach
taken keeps records in Llair and translates them to sequences in
Llair_to_Fol. This choice is made since the encoding into the sequence
theory involves terms that do not have types that are expressible in
terms of the source types. In particular, `(update r i e)`, is encoded
as the concatenation of the prefix of `r` up to the offset of index
`i`, followed by `e` (possibly with padding), and then the suffix of
`r` from index `i+1` on. The prefix and suffix sequences do not
necessarily have source-expressible types.
Reviewed By: jvillard
Differential Revision: D24800866
fbshipit-source-id: e7238c558
Summary:
The support for recursive references to globals from within their
initializers is enough to handle all the cases of recursive structs
that have been encountered so far. Therefore this diff removes the
complication of recursive records entirely.
Reviewed By: jvillard
Differential Revision: D24772955
fbshipit-source-id: f59f06257
Summary:
It happens so seldomly that it is not worth it to optimistically
assume that linking will make opaque types sized. In particular, it is
incongruent for `Typ.is_sized` to hold and then `Typ.size_of` to
raise.
Reviewed By: jvillard
Differential Revision: D24772956
fbshipit-source-id: 96a72a5cf
Summary:
This information is needed to mediate between index-based
operations (such as on records) and offset-based operations (such as
load/store). Since it is fragile to recompute, the approach here is to
query llvm during translation and store the result.
Reviewed By: jvillard
Differential Revision: D24772954
fbshipit-source-id: ad22c3ecf
Summary:
If these failures are observed in real code of interest, they will
need to be resolved, so they are `todo` rather than an internal
`fail`ure.
Reviewed By: jvillard
Differential Revision: D24746222
fbshipit-source-id: 6b924be58
Summary:
While vector types can be translated, vector operations are not
currently handled. Translating type can lead to later failures (such
as bogus Convert expressions) that are not clearly identifiable as
originating from vector types. So fail eagerly when a vector type is
seen. Note that the only vectors that the frontend sees are due to
incompleteness of the LLVM vectorizer pass.
Reviewed By: jvillard
Differential Revision: D24746224
fbshipit-source-id: 30c0715eb
Summary: Do not fail when resolving the realpath of a debug info path.
Reviewed By: jvillard
Differential Revision: D24746237
fbshipit-source-id: b9dc35176
Summary:
Applicative command line argument interpretation fail: using map
instead of compose meant that the type of the ignored arg was the
action function.
Reviewed By: jvillard
Differential Revision: D24746226
fbshipit-source-id: f1dd67067
Summary:
Change Arith.map to not descend through non-interpreted arithmetic
operators. For example, in `2×(x × y) + 3×z + 4`, `map ~f` will apply
`f` to the subterms `x × y` and `z`, but not `x` or `y`.
The logical notion of "subterm" that is needed by the solver does not
coincide with the representation. This is essentially due to not
"flattening" or "purifying" terms. That is, traditionally `x × y`
would not be permitted as an indeterminate of a polynomial. Instead, a
new variable would need to be introduced: `v = x × y` and then the
polynomial would be expressed as `2×v + 3×z + 4`. Taking maximal
non-interpreted subterms as the definition of "subterm" results in
subterms in the non-flattened representation that are equivalent to
those that would result from flattening the representation.
Reviewed By: jvillard
Differential Revision: D24746235
fbshipit-source-id: d8fcf46a1
Summary:
The implementation of Arithmetic relies on the partial projection from
terms to polynomials. This diff enables it to also embed polynomials
back into terms.
Reviewed By: jvillard
Differential Revision: D24746223
fbshipit-source-id: b6010e7b7
Summary:
Add a distinction between interpreted and uninterpreted arithmetic
terms, and use it in Context.classify. This enables correctly
classifying non-linear terms such as `x × y` as uninterpreted.
Reviewed By: ngorogiannis
Differential Revision: D24746228
fbshipit-source-id: 1a4b0e3bd
Summary:
It was possible for the scope of existentials to be violated. In
particular, before this diff the order of re-quantifying the
existentials and conjoining the non-eliminated equations from the
solution of solving for existentials was wrong.
Reviewed By: ngorogiannis
Differential Revision: D24746231
fbshipit-source-id: d96cc60a6
Summary:
In the process of computing `Context.solve`, fresh variables can be
generated. Not all of these end up in the final solution
substitution. Currently all of the freshly generated variables are
returned to the client, which leads to extraneous existentials. This
diff trims the returned fresh variables to only those that appear in
the final solution.
Reviewed By: ngorogiannis
Differential Revision: D24746241
fbshipit-source-id: 59a2f221b
Summary:
Since floats of any width are interpreted the same (as exact rationals
where possible and uninterpreted constants otherwise), this does not
introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746225
fbshipit-source-id: bc8e7bdb9
Summary:
Since non-integral address spaces are not currently supported anyhow,
this does not introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746234
fbshipit-source-id: 1f6887a78
Summary: Just to make the source and destination types of the conversion more clear.
Reviewed By: da319
Differential Revision: D24746239
fbshipit-source-id: 592c7d0f1
Summary:
Since Context treats only equality directly, formulas involving other
literals can normalize to false when the context is not unsat. This
diff changes Sh.star to check this case, and return the canonical
false symbolic heap.
Reviewed By: da319
Differential Revision: D24746227
fbshipit-source-id: 50a51b8a6
Summary:
- Treat missing baseline files as if empty
- Only filter unchanged results if a baseline file is given
- Minor optimization
- Sort multiple statuses
- Fix total computation
- List tests with failing statues first
- Do not use `Format.formatter_of_out_channel` since it sometimes does
not work for some unknown reason, e.g. when the output should have
only one line, none are emitted.
Reviewed By: da319
Differential Revision: D24746236
fbshipit-source-id: f4ead1531
Summary:
When exceptions are used due to the lack of goto, use `raise_notrace`
instead of `raise` to avoid the overhead of populating the backtrace.
Reviewed By: ngorogiannis
Differential Revision: D24630525
fbshipit-source-id: c5051d9c4
Summary:
Adding quotes is needed only to avoid clashes between LLVM integer
literals and anonmous value names.
Reviewed By: ngorogiannis
Differential Revision: D24630527
fbshipit-source-id: 97339740c
Summary:
The implementation in Context, in terms of Fol.Term and Fol.Formula,
can now be used instead of Ses.Equality, implemented using
Ses.Term. The Ses modules can now be removed.
Reviewed By: jvillard
Differential Revision: D24532362
fbshipit-source-id: cee9791b7
Summary:
Adapt the solver implementation from Ses.Equality to Context, and use
the interface of Fol.Context.
Reviewed By: jvillard
Differential Revision: D24532348
fbshipit-source-id: 2c6d41669
Summary:
Apply normalization to conditional terms similar to conditional
formulas: evaluate terms with literal conditions, equal branches, and
ensure the condition is not negative.
Reviewed By: jvillard
Differential Revision: D24532344
fbshipit-source-id: 7818dc496
Summary:
Operations over the core representation are more useful in the core
representation modules.
Reviewed By: ngorogiannis
Differential Revision: D24532340
fbshipit-source-id: f1eab822d
Summary:
The Fol.Term and Fol.Formula provide an interface which supports
if-then-else terms and formulas, while the underlying representation
in Trm does not and Fml only supports if-then-else over formulas, not
terms. The implementation of the rest of the first-order solver needs
to use the underlying, normalized, representation. This diff exports
Trm and Fml to separate modules for this purpose. Later, they will be
packed into a library for the first-order solver, and only used from
within.
Reviewed By: ngorogiannis
Differential Revision: D24532351
fbshipit-source-id: 7310827da
Summary:
And add Monad.Make to implement the full interface from return and
bind.
Reviewed By: ngorogiannis
Differential Revision: D24532341
fbshipit-source-id: 5740ba1c2
Summary:
The iterator is simpler to define and all the traversals are then
available through Iter.
Reviewed By: jvillard
Differential Revision: D24401743
fbshipit-source-id: 81f0653d9
Summary:
It is redundant to include the unit of conjunction in conjunction
formulas (resp., disjunction).
Reviewed By: jvillard
Differential Revision: D24371084
fbshipit-source-id: 6edc151e5
Summary: Simplify output of arithmetic terms, and omit trivial pure part of Sh.
Reviewed By: jvillard
Differential Revision: D24371082
fbshipit-source-id: 91f2117d3
Summary:
Normalization of literal formulas is determined by their term
arguments. Logically, this is part of the theories, so move this code
out of the Propositional module which is theory-independent and into
Fol, which is theory-sensitive.
Reviewed By: jvillard
Differential Revision: D24371081
fbshipit-source-id: f80a19ab8
Summary:
Change the type of `fold` functions to enable them to compose
better. The guiding reasoning behind using types such as:
```
val fold : 'a t -> 's -> f:('a -> 's -> 's) -> 's
```
is:
1. The function argument should be labeled. This is so that it can be
reordered relative to the others, since it is often a multi-line
`fun` expression.
2. The function argument should come last. This enables its
arguments (which are often polymorphic) to benefit from type-based
disambiguation information determined by the types of the other
arguments at the call sites.
3. The function argument's type should produce an
accumulator-transformer when partially-applied. That is,
`f x : 's -> 's`. This composes well with other functions designed
to produce transformers/endofunctions when partially applied, and
in particular improves the common case of composing folds into
"state-passing style" code.
4. The fold function itself should produce an accumulator-transformer
when partially applied. So `'a t -> 's -> f:_ -> 's` rather than
`'s -> 'a t -> f:_ -> 's` or `'a t -> init:'s -> f:_ -> 's` etc.
Reviewed By: jvillard
Differential Revision: D24306063
fbshipit-source-id: 13bd8bbee
Summary:
The changes in set_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306089
fbshipit-source-id: 00a09f486
Summary:
Preceding commit reversed Map.to_iter to match the previous behavior
of to_list.
Reviewed By: jvillard
Differential Revision: D24306051
fbshipit-source-id: aad12e434
Summary:
The changes in map_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306050
fbshipit-source-id: 71e286d4e
Summary:
Remove `-error-style short` from the compilation flags since it causes
merlin to complain, see https://github.com/ocaml/merlin/issues/1176.
After this diff, developers will need to set `OCAML_ERROR_STYLE=short`
in their environment.
Reviewed By: jvillard
Differential Revision: D24306066
fbshipit-source-id: 9c4f26393
Summary:
The usage of equal_or_opposite boils down to evaluating formulas on
propositional constants, which seems clearer.
Reviewed By: jvillard
Differential Revision: D24306104
fbshipit-source-id: df5d07628
Summary:
Represent And and Or formulas as pairs of sets of formulas. One set is
interpreted as positive and the other as negative. This results in
normalization with respect to associativity, commutativity, and unit
laws. This does not normalize distributivity laws, e.g. formulas are
not expanded to disjunctive-normal form or conjunctive-normal
form. Additionally, "zero" laws P ∧ ¬P iff ⊥ and P ∨ ¬P iff ⊤ are
cheaply detected and normalized. Note that formulas are already in
negation-normal form.
Reviewed By: jvillard
Differential Revision: D24306072
fbshipit-source-id: e52265a44
Summary:
Some Iter and Containers functions take optional arguments that
default to polymorphic comparison. This diff wraps all of these making
the argument non-optional to avoid silently using polymorphic compare.
Reviewed By: ngorogiannis
Differential Revision: D24306074
fbshipit-source-id: 34772ee86
Summary:
Expressing the sort of short-circuit evaluation in the changed code is
conceptually more direct using iterators.
Also, when using With_return, getting usable backtraces relies on the
compiler recognizing that the `raise` in the implementation of
`Base.Exn.raise_without_backtrace` should be a `reraise`. Using
iterators avoids this potential fragility.
Reviewed By: jvillard
Differential Revision: D24306094
fbshipit-source-id: b1abe04fb
Summary:
Change implementation of IArray from a wrapper of
Core_kernel.Array.Permissioned to NS.Array, and remove magic. Also
add operations to Array and Iter in order to ensure that IArray is an
extremely thin wrapper of Array: only defining conversions to/from
arrays as well as adding hashing support.
Reviewed By: jvillard
Differential Revision: D24306095
fbshipit-source-id: 97b9187be
Summary:
Term.const_of is misleading as it is easy to expect it checks if a
term is a constant, or to expect that it returns the constant part of
a term. Instead, Term.split_const is clearer:
```
val split_const : t -> t * Q.t
(** Splits a term into the sum of its constant and non-constant parts.
That is, [split_const a] is [(b, c)] such that [a = b + c] and the
absolute value of [c] is maximal. *)
```
Reviewed By: ngorogiannis
Differential Revision: D24306065
fbshipit-source-id: ba15958ad
Summary:
The treatment of comparison and exceptions in Core/Core_kernel/Base
makes them questionable as the default. This diff changes nonstdlib so
that Core is no longer opened in the global namespace, and makes a few
changes to handle the resulting minor API changes. This leads to a
lighter-touch nonstdlib, which makes a few definitions of its own, and
selects and extends modules from several libraries, including base,
core_kernel, containers, iter.
Reviewed By: jvillard
Differential Revision: D24306090
fbshipit-source-id: 42c91bd1b
Summary: Now elapsed time and the info in Unix.process_times is treated uniformly.
Reviewed By: jvillard
Differential Revision: D24306049
fbshipit-source-id: 09ab734ea
Summary:
The unary comparison to zero predicates are confusing to read since
whether the 0 is the left or right argument of the naturally infix
comparison is ambiguous. So replace Gt0 with Pos, meaning the argument
is positive, and remove the rest.
Reviewed By: jvillard
Differential Revision: D24306067
fbshipit-source-id: 2bd30dbe4
Summary:
Checking whether a formula is negative now only needs to inspect the
principle connective.
Reviewed By: ngorogiannis
Differential Revision: D24306061
fbshipit-source-id: 1f110e7f1
Summary:
Add a negation formula that will be used on atomic formulas instead of
ensuring the set of literals is closed under negation. This is in
preparation for more efficient negation and negation-normal form
preservation, which explicitly tracks whether literals are positive or
negative.
Reviewed By: ngorogiannis
Differential Revision: D24306055
fbshipit-source-id: 9300d6aee
Summary:
Change the representation of Fol terms to use polynomials for
arithmetic. This is a generalization and simplification of those used
in Ses. In particular, the treatment of division is stronger as it
captures associativity, commutativity, and unit laws, plus being the
inverse of multiplication.
Also, the interface is staged and factored so that the implementation
of polynomials and arithmetic is separate from the rest of terms.
Reviewed By: jvillard
Differential Revision: D24306108
fbshipit-source-id: 78589a8ec
Summary:
Function symbols when applied to literal values can be simplified by
evaluating them. This can be done even for function symbols that are
otherwise uninterpreted. This is not very strong, but is important in
some cases, and can prevent accumulating large complex terms that are
equal to literal constants.
Reviewed By: jvillard
Differential Revision: D24306044
fbshipit-source-id: 8c34d1ef2
Summary: In preparation for generalizing the type of multiplicities.
Reviewed By: jvillard
Differential Revision: D24306052
fbshipit-source-id: ddb71499e
Summary:
The form of the Base containers interface, in particular the way
comparison functions are passed using Comparators, is slower than
standard functors. Also Base.Map is missing some operations, such as
efficient merge and union.
Reviewed By: jvillard
Differential Revision: D24306047
fbshipit-source-id: e1623b693
Summary:
The form of the Base containers interface, in particular the way
comparison functions are passed using Comparators, is slower than
standard functors.
Reviewed By: jvillard
Differential Revision: D24306082
fbshipit-source-id: abf3e0293
Summary: Hopefully only transitional until Fol.Var and Ses.Var are conflated.
Reviewed By: jvillard
Differential Revision: D24306039
fbshipit-source-id: 5c3be8d4d
Summary:
Clarify the translation of 1-bit integer operations to formulas, and
add a few missing cases.
Reviewed By: ngorogiannis
Differential Revision: D24306057
fbshipit-source-id: 626a27997
Summary:
The translation from Llair to Fol can now be implemented using only
the external interface of Fol, so move it to a separate module. This
makes Fol not depend on Llair and vice versa, as appropriate.
Reviewed By: jvillard
Differential Revision: D24306087
fbshipit-source-id: fc68a588b
Summary:
Instead of relying on tuple terms, make function symbol applications
and predicate symbol literals n-ary directly.
Reviewed By: jvillard
Differential Revision: D24306078
fbshipit-source-id: 2863dceb4
Summary:
Move the punting between arrays and lists out of the clients of the
n-ary application normalizing constructors.
Reviewed By: jvillard
Differential Revision: D24306071
fbshipit-source-id: f3d2cb5df
Summary:
References from a record to one of its ancestor records are used to
represent cyclic or recursive record values. While the current
interpretation is weak, these logically are part of the record theory
and should be interpreted with the rest of the record terms.
Reviewed By: jvillard
Differential Revision: D24306091
fbshipit-source-id: 41553741d
Summary:
The empty record term is only used as the base of a sequence of
updates for an interval of indices from 0 to some N. A more direct
representation is to combine such sequences of updates into a flat
record term listing the elements.
Reviewed By: jvillard
Differential Revision: D24306048
fbshipit-source-id: d1b4900c8
Summary:
The uses of record terms only require indices that are literal
integers. This is a significant logical simplification from the
perspective of the backend solver.
Reviewed By: jvillard
Differential Revision: D24306093
fbshipit-source-id: 083dcc6b5
Summary:
Conversions between types are uninterpreted, so use uninterpreted
function symbols for them.
Reviewed By: jvillard
Differential Revision: D24306077
fbshipit-source-id: 49937fdbb
Summary:
Label values are uninterpreted, so use an uninterpreted function
symbol for them.
Reviewed By: jvillard
Differential Revision: D24306097
fbshipit-source-id: e139c70ba
Summary:
Floating point values are uninterpreted, so use an uninterpreted
function symbol for them.
Reviewed By: jvillard
Differential Revision: D24306096
fbshipit-source-id: 8c10dd3fd
Summary:
Convert from Llair.Exp to Fol.Term directly instead of going via
Ses.Term. This is a step on the way to removing Ses.
There are currently some term simplifications done in Ses.Term that
are missing in Fol.Term. This means that converting directly from
Llair.Exp to Fol.Term instead of via Ses.Term is not exactly the same
as the indirect conversion. The missing simplifications will be added
to Fol.Term in upcoming diffs.
Reviewed By: jvillard
Differential Revision: D24306053
fbshipit-source-id: 4ec5620a9
Summary:
Code is expressed using Llair.Exp, which is potentially higher
fidelity than Term. So define the interval analysis directly in terms
of the Llair form.
Reviewed By: jvillard
Differential Revision: D24306085
fbshipit-source-id: f9d876eec
Summary:
Generalize Fol.Predsym to separate Predsym module for arbitrary
uninterpreted predicate symbols.
Add uninterpreted predicate literals to Ses.Term.
Use uninterpreted predicates to represent "ord" and "uno".
Reviewed By: jvillard
Differential Revision: D24306105
fbshipit-source-id: bdd72a8be
Summary: Funsym does not need to be defined as a submodule of Fol.
Reviewed By: jvillard
Differential Revision: D24306092
fbshipit-source-id: 7875f45f0
Summary:
A number of function symbols are not interpreted. This diff adds
generic uninterpreted function symbols, which will be used later to
avoid treating different uninterpreted functions separately.
Reviewed By: jvillard
Differential Revision: D24306076
fbshipit-source-id: b70ed10aa
Summary:
With the implementation of variables defined parametrically over their
representation, the implementation can also be used for Fol.Var.
Reviewed By: ngorogiannis
Differential Revision: D23703054
fbshipit-source-id: d27bdbbe8
Summary:
Variables are represented as a subtype of terms. The implementation of
the operations on variables is largely independent of this. This diff
generalizes the implementation over the concrete representation, and
moves it to a separate module.
Reviewed By: ngorogiannis
Differential Revision: D23660290
fbshipit-source-id: 90d8c3ca4
Summary:
Increase the fidelity of the status in the analysis report slightly by
including the number of analysis steps taken.
Reviewed By: jvillard
Differential Revision: D23648493
fbshipit-source-id: 8050b7829
Summary:
Just to avoid confusion over directories named 'bin' being expected to
contain binaries, rather than the sources of executables.
Reviewed By: jvillard
Differential Revision: D23636372
fbshipit-source-id: 8593380e6
Summary:
Add support to ppx_trace to rewrite `[%trace]` into a call to the
corresponding `Trace` function:
```lang=ocaml
val trace :
?call:(pf -> unit)
-> ?retn:(pf -> 'a -> unit)
-> ?rais:(pf -> exn -> Printexc.raw_backtrace -> unit)
-> string
-> string
-> (unit -> 'a)
-> 'a
(** [trace ~call ~retn ~rais mod_name fun_name k] either simply invokes
[k ()], when not enabled, or else increases the indentation level and
emits the [call] message, then invokes [k ()], then decreases the
indentation level and either emits the [retn] or [rais] message,
depending on whether [k ()] returned normally or exceptionally. *)
```
The main motivation over the existing `Trace.call` and `Trace.retn` is
that by packaging them together, unhandled exceptions can be treated
better.
Reviewed By: jvillard
Differential Revision: D23636200
fbshipit-source-id: f61c267fd
Summary:
Construct the identity function explicitly instead of relying on the
`Stdlib.Fun.id` name, which can be problematic depending on compiler
version and which modules have been `open`ed.
Reviewed By: jvillard
Differential Revision: D23636204
fbshipit-source-id: 2fb644c18
Summary:
Version 0.16 of ppxlib breaks merlin in combination with ppx_trace,
due to https://github.com/ocaml-ppx/ppxlib/issues/175.
Reviewed By: jvillard
Differential Revision: D23636202
fbshipit-source-id: 37a5f36b7
Summary:
The expansion of the `[%debug]` extension point is simple and fits
into the pattern supported by `Ppxlib.Extension`. This diff simplifies
the mapper implementing the rest of the trace expansion by moving the
expansion of debug into a separate
`Ppxlib.Context_free.Rule.extension` rule.
Reviewed By: jvillard
Differential Revision: D23636201
fbshipit-source-id: 847c258fd
Summary:
Use `Ppxlib.Ast_traverse.map` instead of
`Ppxlib.Selected_ast.Ast.Ast_mapper` which is included from
`Migrate_parsetree` since `Ppxlib.Selected_ast.Ast` reexports one of
the `Migrate_parsetree.Versions` modules. This change is needed to be
compatible with (ocaml-migrate-parsetree 2.0 and) ppxlib 0.16 since it
no longer re-exports the `Ast_mapper` module from
`Migrate_parsetree`. This ppxlib change is one of the headline
simplification enablers noted in the (announcement of
ocaml-migrate-parsetree
2.0)[https://discuss.ocaml.org/t/ocaml-migrate-parsetree-2-0-0/5991].
Reviewed By: jvillard
Differential Revision: D23636203
fbshipit-source-id: 71e24b46b
Summary:
When equal_or_separate returns Unknown, it is common to sort the args,
which is wasteful since computing equal_or_separate already had to
test if the args are equal, which is most if not all of the work of
comparing them.
Reviewed By: jvillard
Differential Revision: D23636205
fbshipit-source-id: 5b2bcdd8f
Summary:
The `sledge-help.txt` file is under source control, and should not be
removed by `make clean`.
Reviewed By: ngorogiannis
Differential Revision: D23497893
fbshipit-source-id: 2061160a8
Summary:
`Fol.equal_or_opposite p q` naively constructs the negation of `q` in
most cases, only to test if it is equal to `p`. This is an inefficient
method of computing if one formula is the negation of another. This
diff implements this directly. The drawback is some duplication of the
negation logic from `_Not`.
Reviewed By: ngorogiannis
Differential Revision: D23487500
fbshipit-source-id: 100f95edc
Summary:
Normalize conditional formulas to ensure that their "condition"
formula is not "negative". This avoids redundant formulas such as `(x
= 0 ? p : q)` and `(x ≠ 0 ? q : p)`. The choice of which formulas are
"negative" for this purpose is mostly arbitrary, with the only real
constraint being that negating a negative formula should produce a
positive one.
Note that conditional formulas themselves are considered to be
"positive" since negating them produces another conditional formula
with the same condition formula.
Reviewed By: ngorogiannis
Differential Revision: D23487502
fbshipit-source-id: 63606d89c
Summary:
Sort the subterms or subformulas of binary formulas that are
symmetric. This avoids redundant formulas such as both `x = y` and `y
= x`.
Reviewed By: ngorogiannis
Differential Revision: D23487501
fbshipit-source-id: 7e2295aba
Summary:
To support:
- html report generation via sexp reports (instead of RESULT in stdout)
- smt2 benchmarks
- local and extra-repo tests
- calculation of relative paths to tests
Reviewed By: ngorogiannis
Differential Revision: D23459514
fbshipit-source-id: f44e51c17
Summary:
Add a `sledge-report` executabe to aggregate and report results from
test runs. Results from possibly-many test runs are averaged and
reported in an html file with color-coded indications of performance
improvement or regression.
Reviewed By: ngorogiannis
Differential Revision: D23459521
fbshipit-source-id: 61ca936f4
Summary:
Add a Report.status type to represent the overall status of an
analysis run, and revise handling of backtraces to preserve the trace
of the originally-raised exception in more cases.
Reviewed By: ngorogiannis
Differential Revision: D23459518
fbshipit-source-id: a99fe0d14
Summary:
The SLEdge internal first-order theory solver targets the "word
problem", where a query has the form `C ⊢ L` where `C` is a
conjunction of literals and `L` is a single literal. This can be
abused to implement a naive SMT solver using an expansion to
disjunctive-normal form and checking `C ⊢ false` for each branch `C`
of the DNF. This is not useful as an SMT solver, but can be used for
testing.
Reviewed By: ngorogiannis
Differential Revision: D23459524
fbshipit-source-id: 5483e5a84
Summary: Formula.disjuncts was a quickly written approximation of DNF.
Reviewed By: ngorogiannis
Differential Revision: D23459513
fbshipit-source-id: 79fd60a7b
Summary:
It was incorrect in case any but the first of of the Formula.disjuncts
was inconsistent.
Reviewed By: ngorogiannis
Differential Revision: D23459519
fbshipit-source-id: 394677e38
Summary:
The only use of the ill-specified Sh.with_pure function is to ignore
the pure part when computing free variables. So add an argument to
Sh.fv to achieve that explicitly and remove Sh.with_pure.
Reviewed By: ngorogiannis
Differential Revision: D23459517
fbshipit-source-id: 8767799ca
Summary:
Strengthen normalization performed by Term and Formula constructors to
eliminate literal 0 subterms and true or false subformulas, as well as
cases where subterms or subformulas are either equal or opposite.
This strengthens the ability of Context.implies to prove formulas that
involve embedding or projecting between terms and formulas, as the
added normalization sometimes reduces if-then-else formulas to
literals that are then directly provable.
Reviewed By: ngorogiannis
Differential Revision: D23459512
fbshipit-source-id: 6d4d90399
Summary:
The dune build info embedded into executables is broken with dune <
2.7 and an flambda compiler.
Reviewed By: ngorogiannis
Differential Revision: D23459510
fbshipit-source-id: 18b3e3e15
Summary:
`Sh.norm` relies on `Eq (v, v)` formulas for `v` a variable to be
normalized to `Tt`, which is how eliminated variables are actually
removed from the representation.
Reviewed By: jvillard
Differential Revision: D22571132
fbshipit-source-id: 6d5f3efd7
Summary:
Move normalization that is necessary for `embed_into_fml` to be left
inverse to `embed_into_cnd` into the general `Fml` constructors.
Reviewed By: jvillard
Differential Revision: D22571137
fbshipit-source-id: 575c6bc45
Summary:
In order to ensure that the normalizing constructors are not
circumvented.
Reviewed By: jvillard
Differential Revision: D22571139
fbshipit-source-id: 32032c6fa
Summary:
The default printer is `pp_classes`, while `pp` is for debugging the
internal representation manipulation, so it is renamed to `pp_raw`.
Reviewed By: jvillard
Differential Revision: D22571135
fbshipit-source-id: 2d624e279
Summary:
`Formula.is_true` and `is_false` are now trivial one-line wrappers,
remove them for clarity.
Reviewed By: jvillard
Differential Revision: D22571143
fbshipit-source-id: 3f058eab4
Summary:
It is more confusing than necessary to use logical formula terminology
for the Context interface, considering that Formula represents
formulas and Context represents a (solver state resulting from a) set
of assumptions.
Reviewed By: jvillard
Differential Revision: D22571136
fbshipit-source-id: 087c97a02
Summary:
The unary forms are primitive in ICS, and in uncoming changes which
involve considering the product of a term and an equality relation, it
is more efficient to have unary constructors since the product is then
linear instead of quadratic in the size of the equality relation.
Reviewed By: jvillard
Differential Revision: D22571138
fbshipit-source-id: e0b745cc8
Summary:
Add a Predsym module for uninterpreted (unary) predicate symbols, and
positive and negative literals applying them to a term. As with
uninterpreted functions, tuple terms are used to represent predicates
of other arities.
Using this support, change the Ord and Uno formulas to uninterpreted
literals.
Reviewed By: jvillard
Differential Revision: D22571140
fbshipit-source-id: 5022a91e2
Summary:
`Context.difference` is now just a convenience function that does not
need to be defined internally.
Reviewed By: jvillard
Differential Revision: D22571141
fbshipit-source-id: 58aea9488
Summary: Also, when printing in raw mode, do not print the context.
Reviewed By: jvillard
Differential Revision: D22571145
fbshipit-source-id: b3596d9cc
Summary:
Make the relationship between Sh.is_empty and Sh.pure_approx stronger
and more precise. In particular:
> If [is_empty q], then [pure_approx q] is equivalent to
> [pure (pure_approx q)].
This enables replacing Solver.excise_pure with a simpler pure_entails
function. In particular, the heavy reliance on normalization of pure
formulas to true or false literals is eliminated, and only pure
entailment is needed.
Reviewed By: jvillard
Differential Revision: D22571146
fbshipit-source-id: 2fca64a61
Summary:
Generalize Fol interface to allow checking if a context implies any
formula, rather than restricting to only equalities.
Reviewed By: jvillard
Differential Revision: D22571144
fbshipit-source-id: 726bd87fd
Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.
Reviewed By: jvillard
Differential Revision: D22571150
fbshipit-source-id: 8952f0301
Josh Berdine