Summary:
The eventual aim is for the conversion of Llair to Fol to be external
to Fol. Fol should not need to depend on Llair, nor vice versa. This
is not yet possible, but a step forward is to move the conversion
functions into separate modules outside the core Fol modules.
Reviewed By: ngorogiannis
Differential Revision: D22170522
fbshipit-source-id: 4860b4c07
Summary:
The `Subst` module is not used by `Ses`, so move it out of the
Ses-internal APIs.
Reviewed By: ngorogiannis
Differential Revision: D22170513
fbshipit-source-id: a189a1440
Summary:
Change Term and Equality rename functions to accept a partial
application of Var.Subst.apply to the renaming substitution.
Reviewed By: ngorogiannis
Differential Revision: D22170520
fbshipit-source-id: 003d8b27e
Summary:
The convention is for modules that are intended to be `open`ed, that
define syntax and infix operations, are named `Import`. This diff
combines the `Option.Monad_infix` and `Option.Monad_syntax` modules
into `Option.Import` to follow this convention.
Reviewed By: ngorogiannis
Differential Revision: D22170507
fbshipit-source-id: 44378fd56
Summary:
Exponents in polynomials are represented by rationals for code reuse
purposes, but only integral exponents are supported. Strengthen the
invariant check to clarify this.
Reviewed By: ngorogiannis
Differential Revision: D22170517
fbshipit-source-id: 81ae38f4e
Summary:
Refactor `Equality.ppx_classes_diff` into `diff_classes` to construct
the difference between classes maps explicitly, and change
`ppx_classes` to accept such a difference instead of computing it
internally.
This more flexibly composable interface allows elimination of extra
calls to `Equality.entails` to check if the difference is empty.
Reviewed By: jvillard
Differential Revision: D22038488
fbshipit-source-id: c19c18fc8
Summary:
The list interpreted as a conjunction of individual terms in `Sh.pure`
is now redundant with `Term.And`. This patch removes the redundant
list.
Reviewed By: jvillard
Differential Revision: D22035852
fbshipit-source-id: 49c01a078
Summary:
With the current handling of fresh variable generation during symbolic
execution, it is now possible to delay generating fresh variables in
individual small axioms until the precondition is known. In
particular, the existential variables of the precondition formula can
be bound, and then the small axiom can be generated with variables
fresh with respect to them. Previously, the small axioms were
generated with fresh variables that could later clash with the
precondition's existentials, necessitating renaming. This
double-freshening is now eliminated.
Reviewed By: jvillard
Differential Revision: D21974022
fbshipit-source-id: f217bfb9f
Summary:
When fresh variables are generated to name the overwritten value in an
assignment, they should be included in the ghost variables of the
resulting small axiom. This change should have been included in the
elimination of SSA.
Also strengthen assertion checking of small specs during symbolic
execution.
Reviewed By: jvillard
Differential Revision: D21974019
fbshipit-source-id: a66d8dac6
Summary:
Currently the symbolic execution code in `Exec` manually threads
universal and existential variable contexts through virtually every
function. It is easy to mistakenly pass on a context that is not the
latest-extended one, or to forget to add generated variables to the
contexts.
This patch adds a state monad, `Fresh`, to manage the generation of
fresh variables in `Exec`. This is a standard state monad where the
state is two sets of variables: those to which fresh variables must be
chosen fresh, and those which have been generated. This yields an
abstraction where an `'a Fresh.t` value represents a value of type
`'a` which may contain as-yet-unnamed variables, and `Fresh.gen ~wrt
a` generates names that are fresh with respect to `wrt` for all
unnamed variables in `a`, and yields the set of generated variables
together with `a` expressed in terms of those variables.
Reviewed By: jvillard
Differential Revision: D21974018
fbshipit-source-id: 1917e82c0
Summary: Minor code simplification and optimization of `extend_us` in no-op case.
Reviewed By: jvillard
Differential Revision: D21974021
fbshipit-source-id: a8b12b564
Summary:
Change the `Var.Subst` `freshen` and `restrict` constructors to return
the domain and range of the substitution explicitly. Clients generally
need to compute them immediately, and they are at least partially
constructed during the initial substitution construction anyhow. This
may be an incidental minor optimization.
This allows removing the `apply_set` operation, as it's use can be
handled directly from the domain and range sets.
This also allows `Sh.rename` to be split into a function that assumes
that the substitution is restricted to the vocabulary of the formula,
and a wrapper that does this restriction and calls through. This
allows `Sh.freshen_xs` to be simplified slightly, and avoids some
redundant restriction, domain, and range computations.
Reviewed By: jvillard
Differential Revision: D21974017
fbshipit-source-id: aa8b3db24
Summary:
`Domain_sh.from_call.subst` is a substitution that replaces shadowed
variables with fresh ones, which is constructed by `Domain_sh.call`
and used by `Domain_sh.retn`, after inverting it. This patch changes
the stored substitution to the inverted one, and renames it to
`unshadow` for clarity.
After this change, the stored substitutions have the property that
they map variables to program variables. This is desirable since it
avoids the question about the uninverted substitution of whether the
variables in the range of the uninverted substitution are "fresh".
Reviewed By: jvillard
Differential Revision: D21974020
fbshipit-source-id: d469c89f9
Summary:
Logically there is nothing specific to memory contents (as
byte-arrays) or aggregate (struct/array) values, the theory is for
sequences of non-fixed sized elements.
Reviewed By: jvillard
Differential Revision: D21721019
fbshipit-source-id: b2b730a50
Summary:
`Term.eq_concat` is not primitive and complicates the `Term`
interface. Move it to a couple clients as a convenience wrapper.
Reviewed By: jvillard
Differential Revision: D21721026
fbshipit-source-id: 0d74aa251
Summary:
Previously `null` and `zero` had different sorts/types, but now they
are equivalent.
Reviewed By: jvillard
Differential Revision: D21721023
fbshipit-source-id: 485219f6a
Summary:
Multiplication by a constant is primitive in the linear arithmetic
solver, while general multiplication is not, so for clarity and
predictability, use constants where possible.
Reviewed By: jvillard
Differential Revision: D21721020
fbshipit-source-id: 3497d06c9
Summary:
It is suboptimal for `Sh` to destruct terms with detailed knowledge of
their representation. So add `Term.const_of` to obtain the constant
summand of a polynomial term.
Reviewed By: jvillard
Differential Revision: D21721022
fbshipit-source-id: 4af858896
Summary:
It is suboptimal for `Sh` to destruct terms with detailed knowledge of
their representation. So add `Term.d_int` to destruct an integer term.
Reviewed By: jvillard
Differential Revision: D21721024
fbshipit-source-id: 5f13794b6
Summary:
It is suboptimal for `Sh` to destruct terms with detailed knowledge of
their representation. So add `Term.disjuncts` to obtain the toplevel
disjuncts of a term.
Reviewed By: jvillard
Differential Revision: D21721016
fbshipit-source-id: 809da9b1b
Summary:
It has no dependencies on the rest of the sledge codebase and might be
more generally useful.
Reviewed By: jvillard
Differential Revision: D21720980
fbshipit-source-id: b4f061e73
Summary:
Now that the frontend translates LLVM's undef to nondet instructions,
not expressions, Nondet in Exp and Term are not needed.
Reviewed By: jvillard
Differential Revision: D21720969
fbshipit-source-id: e8acaf432
Summary:
Refer to Llair modules using `Llair.` qualifier, except for in
`Frontend`, which makes so much use of `Llair` that it is now opened
(`Llair` only contains types and modules, so `open` is safe).
Reviewed By: jvillard
Differential Revision: D21720979
fbshipit-source-id: dd42075d9
Summary:
The term representing an exp should not rely on more info than is
carried by the exp.
Reviewed By: jvillard
Differential Revision: D21720989
fbshipit-source-id: b65bf3678
Summary:
It is now possible to not spew dune files all over the repo, and opam
files aren't needed either.
Reviewed By: jvillard
Differential Revision: D21720978
fbshipit-source-id: 553e1d154
Summary:
```
val ( let@ ) : ('a -> 'b) -> 'a -> 'b
(** [let@ x = e in b] is equivalent to [e @@ fun x -> b], that is,
[e (fun x -> b)] *)
```
Reviewed By: jvillard
Differential Revision: D21721025
fbshipit-source-id: d8efdebbe
Summary:
Rather than compute the size of the llair type of the llair
initializer expression, compute the size of the llvm initializer
directly.
Reviewed By: ngorogiannis
Differential Revision: D21720982
fbshipit-source-id: 4364baf38
Summary:
In LLVM it is possible for struct constant values to be directly
recursive, with no pointer dereference to close the cycle. These
appear for example as the values of vtables from C++ code.
Currently such recursive records in the Exp and Term languages are
represented as genuinely cyclic values. Compared to a standard term
representation, the presence of cyclic values is a significant
complication everywhere. Since the backend solver does not do anything
such as induction over these, they have to be treated as essentially
atomic.
This patch changes the representation to a standard non-recursive tree
term structure. Instead of cyclic references, an explicit constructor
is added for the "non-tree edges", which simply indicates which
ancestor record value to which the recursive reference points.
There is a potential issue with this representation, since for
mutually recursive records, the representation is not canonical: it
chooses one of the records in the cycle to start from and expresses
the cycles relative to that. Currently the choice of representation is
dictated by the frontend. For the case of vtables, the frontend
translates globals in the same order they appear in the LLVM IR, so
the representation choice is fixed.
It may turn out that other potential uses require more reasoning
support in the backend solver, which would involve a theory of
equality of record values induced by equating the representations
resulting from different rotations of the cycle of records.
Reviewed By: jvillard
Differential Revision: D21441533
fbshipit-source-id: 0c5a11378
Summary:
Having `val size_of : Typ.t -> t` in the signature of `Term` and `val
size_of : t -> t` in the signature of `Exp` gives the impression that
`Term` and `Exp` know something about `Typ`. But they don't, those
functions are only trivial convenience wrappers, and only have a few
uses, so just inline them to clarify that it is `Typ` that knows about
the sizes of types.
Reviewed By: jvillard
Differential Revision: D21441535
fbshipit-source-id: 09b135a8c
Summary:
Move files, adjust build system, etc.
This also separates out the ppx_trace conditional compilation debug
tracing machinery into an independent package and library.
Reviewed By: jvillard
Differential Revision: D20322876
fbshipit-source-id: a50522462
Summary:
`Reg.demangle` is implemented by calling the `_cxa_demangle` C++
runtime system function. This will be linked into the sledge binary,
due to being linked with llvm, but will not necessarily be available
in the sledge library. So make it a dynamically-set function to avoid
calling an undefined function from the library.
Reviewed By: jvillard
Differential Revision: D20323791
fbshipit-source-id: bda9afd37
Summary:
Formulate the canonizer for Extract from Concat terms uniformly as a
concatenation of extracts.
Reviewed By: jvillard
Differential Revision: D20303064
fbshipit-source-id: a45bc45dd
Summary:
Change constructor for solver goals to enforce variable context
conditions, and simplify other context manipulations that are now
unneeded.
Reviewed By: jvillard
Differential Revision: D20248543
fbshipit-source-id: a255c792b
Summary:
In a few places, implicitly witnessed existential variables could
remain in the existential context. This led to weakness in the solver,
where occurrences bound by the existential context would be not known
to be constrained by their witnesses.
Reviewed By: jvillard
Differential Revision: D20248542
fbshipit-source-id: 44f62839c
Summary: In preparation for enforcing invariants in the constructor.
Reviewed By: jvillard
Differential Revision: D20248541
fbshipit-source-id: 41f7d36e5
Summary:
Program (and global) variables are only distinct when considering
their string names, but logical variables need only their ids.
Reviewed By: jvillard
Differential Revision: D20214528
fbshipit-source-id: f7892c3ad
Summary:
When extracting from a concatenation, drop a prefix of the concat with
length equal to the offset of the extraction:
```
(α₀^…^αᵢ^…) [0+n₀+…+nᵢ₋₁, l) ==> (αᵢ^…)[0,l) where nₓ ≡ |αₓ|
```
Reviewed By: jvillard
Differential Revision: D20192874
fbshipit-source-id: cd015aa36
Summary:
Fix unstated assumptions Sh.or_ made on the universal and existential
contexts of disjuncts.
Reviewed By: jvillard
Differential Revision: D20192873
fbshipit-source-id: 945623e57
Summary:
This diff changes `Sh.simplify` from a logically-weakening syntactic
simplification to an equivalence-preserving rewrite. The
implementation is based on `Equality.solve_for_vars` which is also
used by `Solver` to witness existential variables.
Reviewed By: jvillard
Differential Revision: D20120274
fbshipit-source-id: 5e11659ea
Summary:
Just fix accumulated mis-formatting that is swallowed by the
inline-test promotion implementation.
Reviewed By: ngorogiannis
Differential Revision: D20120262
fbshipit-source-id: 0e387dc55
Summary:
Add `Sh.pp_raw` which is closer to the representation, for use when
tracing `Sh` operations.
Reviewed By: ngorogiannis
Differential Revision: D20120281
fbshipit-source-id: e3b1b531a
Summary:
Due to strengthened existential witnessing, the incomplete ad hoc
witness guessing is no longer needed.
Reviewed By: ngorogiannis
Differential Revision: D20120277
fbshipit-source-id: 8ee1656dd
Summary:
Strengthen computation of solution substitutions used for existential
witnessing by using the solver for the memory contents theory. This
uses a generalization of the equation solver implementation which
accepts a predicate used as a filter for equations added to the
solution substitution. When used for solving for a given set of
variables, this filter excludes equations which do not meet the
desired variable conditions.
Reviewed By: jvillard
Differential Revision: D20120275
fbshipit-source-id: 4203d5e41
Summary:
Strengthen existential quantifier witnessing to enable witnessing an
existential with a term containing another existential if no universal
witness is available. Additionally, strengthen existential witnessing
to enable terms of interpreted theories to witness existential
variables.
Also strengthen and simplify the representation invariant checking for
existential witnessing code.
Reviewed By: jvillard
Differential Revision: D20120271
fbshipit-source-id: 4c44fe9ef
Summary:
Handle the case the universal context of a goal does not stay in sync
with that of the minuend.
The need for this indicates that there is some problematic redundancy
in the representation of solver goals.
Reviewed By: ngorogiannis
Differential Revision: D20120268
fbshipit-source-id: 44a4d6260
Summary:
It can happen that canonizing subterms can change the classification
of a term e.g. to the literal true. In such cases, it is not useful or
correct use `Equality.lookup` (which expects to only be used on
uninterpreted applications) to search for some other equation equal to
the literal and use its representative instead.
Reviewed By: ngorogiannis
Differential Revision: D20120279
fbshipit-source-id: 3e2160233
Summary: When equating Concat terms, drop any common prefix or suffix.
Reviewed By: ngorogiannis
Differential Revision: D20120264
fbshipit-source-id: afdeb990e
Summary: No code change, only reordering definitions in prep for later changes.
Reviewed By: ngorogiannis
Differential Revision: D20120263
fbshipit-source-id: b312dfc9a
Summary: Add `Equality.and_term` and replace most of `Sh.pure` with it.
Reviewed By: ngorogiannis
Differential Revision: D20029742
fbshipit-source-id: 07c2f1fe6
Summary:
Replace `Equality.Subst.trim` with `partition_valid` which has a
logical specification (and unsurprisingly fixes some corner case
bugs):
```
val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
(** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks and ν
are maximal where ∃ks. ν is universally valid, xs ⊇ ks and ks ∩
fv(τ) = ∅. *)
```
Reviewed By: ngorogiannis
Differential Revision: D20004974
fbshipit-source-id: 5cb3b3835
Summary:
Sh.var_strength determines, in part, if an existential variable has
only a single occurrence. The objective of this is to determine that a
variable is merely a placeholder and not used to express additional
constraints. For this, it suffices to check the weaker condition that
there is a single occurrence in each branch of a DNF expansion.
Reviewed By: ngorogiannis
Differential Revision: D19973779
fbshipit-source-id: 2c90c61f4
Josh Berdine