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:
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:
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: 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:
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:
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:
`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:
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: 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:
`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
Summary:
In Ses, the constant term of a polynomial is represented as a
redundant multiplication by 1. Fix Fol.of_ses to recognize and
normalize this.
Reviewed By: jvillard
Differential Revision: D22571131
fbshipit-source-id: 3e1a12e5f
Summary:
The Ses constructors might simplify terms when called from
Fol.to_ses. Fix Fol.ses_map to account for this.
Reviewed By: jvillard
Differential Revision: D22571151
fbshipit-source-id: 1d573ac5f
Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.
Reviewed By: jvillard
Differential Revision: D22455725
fbshipit-source-id: 6f0059873
Summary:
In preparation for more smoothly interoperating with ICS's functional
array theory.
Reviewed By: jvillard
Differential Revision: D22401039
fbshipit-source-id: 4de39c38a
Summary:
The first-order context is induced by the pure part, so no need to
compare it.
Reviewed By: jvillard
Differential Revision: D22381645
fbshipit-source-id: 29fff13a3
Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.
The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.
Reviewed By: jvillard
Differential Revision: D22170506
fbshipit-source-id: a014ee7d7
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
Summary:
Currently the free variables of the equality relation of a formula are
contained in the free variables of the rest of the formula, so Sh.fv
ignores them. Propagating equality facts across the star-or structure
of a formula, as necessary for quantifier elimination, breaks this
invariant. Some use cases, such as detecting which variables survive
applying a witness substitution, need to ignore the variables that
appear in the equality relation. This diff adds an argument to
conditionally ignore the variables in the equality relations.
Reviewed By: ngorogiannis
Differential Revision: D19580430
fbshipit-source-id: 2d417d89b
Summary:
In an equation such as `x = ⟨n,a⟩`, `x` is implicitly an aggregate of
size `n` (or else the equation is ill-typed). Make this explicit by
normalizing such equations to e.g. `⟨|⟨n,a⟩|,x⟩ = ⟨n,a⟩`.
Reviewed By: ngorogiannis
Differential Revision: D19358546
fbshipit-source-id: 77f67a0da
Summary:
Strengthen Equality.solve_for_vars so that it will solve cases such as
```
∃ a. ⟨n,a⟩ = ⟨m,b⟩^⟨o,c⟩
```
Reviewed By: ngorogiannis
Differential Revision: D19356324
fbshipit-source-id: a57625ba6
Summary:
Due to paying closer attention to which terms are already normalized
by the accumulated solution substitution.
Reviewed By: ngorogiannis
Differential Revision: D19356323
fbshipit-source-id: e162414a0
Summary:
The function transforming terms passed to Sh.map might produce trivial
constraints, filter them out.
Reviewed By: ngorogiannis
Differential Revision: D19286628
fbshipit-source-id: e3d9926ce
Summary:
In order for Equality.solve to generate fresh variables, it needs to
be passed the universal context with respect to which variables must
be chosen fresh.
Reviewed By: ngorogiannis
Differential Revision: D19286630
fbshipit-source-id: ebbedd954
Summary:
Aggregate args of Extract and Concat must be aggregate terms, in
particular, not variables. This maintains the property that the size
of any aggregate can be computed.
Reviewed By: ngorogiannis
Differential Revision: D19286625
fbshipit-source-id: 1af1e4183
Summary:
The byte-array theory used for the contents of memory is strong
enough to express all the constraints arising during symbolic
execution without the ability to extract a slice out of a byte-array.
However, without Extract, it is not possible to solve some equations
for some variables, for example solving ⟨n,α⟩^⟨m,β⟩ = ⟨l,γ⟩ for α.
Solving such equations is needed for quantifier elimination and to
formulate the byte-array theory as a Shostak theory.
Reviewed By: ngorogiannis
Differential Revision: D19286632
fbshipit-source-id: 07dc112d0
Summary:
Revise the ad hoc treatment to drop tautologous constraints such as
∃x,y. x = y to only apply when x and y do not appear elsewhere.
Reviewed By: ngorogiannis
Differential Revision: D19282633
fbshipit-source-id: 7fb9951ec
Summary:
Equality.solve_for_var_contexts can produce solution substitutions
that witness existentials in more cases than the
single-existential-occurrence heuristic, and is more conservative in
cases where the latter is incomplete.
Reviewed By: ngorogiannis
Differential Revision: D19282634
fbshipit-source-id: f86f0a9cb
Summary:
```
val trim : bound:Var.Set.t -> Var.Set.t -> t -> t
(** [trim bound kills subst] is [subst] without mappings that mention
[kills] or [bound ∩ fv x] for removed entries [x ↦ u] *)
```
To be used for existential witnessing and quantifier elimination.
Reviewed By: ngorogiannis
Differential Revision: D19282644
fbshipit-source-id: d981a1cb4
Summary:
```
val solve_for_vars : Var.Set.t list -> t -> Subst.t
(** [solve_for_vars \[v₁;…\] r] is a solution substitution that is
entailed by [r] and consists of oriented equalities [x ↦ u] such that
[fv x ⊈ vᵢ ⊇ fv u] where [i] is minimal such that [vᵢ]
distinguishes [fv x] and [fv u], if one exists. *)
```
To be used for existential witnessing and quantifier elimination.
Reviewed By: ngorogiannis
Differential Revision: D19282636
fbshipit-source-id: c5b006cea
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
Josh Berdine