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:
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:
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:
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:
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:
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: 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:
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:
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:
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:
```
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:
If `Term.solve_zero_eq` is passed `for_`, then that subterm is solved
for.
Reviewed By: ngorogiannis
Differential Revision: D19282647
fbshipit-source-id: 5d5b76af5
Summary:
In preparation for constructing solution substitutions in solve, which
are closely tied to Equality.
Reviewed By: ngorogiannis
Differential Revision: D19282640
fbshipit-source-id: ca0f8ae29
Summary:
Identifying and separating one of the monomials in a polynomial, and
solving an equality for it, is much more dependent on the
representation of polynomial terms than the rest of solve.
Reviewed By: ngorogiannis
Differential Revision: D19282645
fbshipit-source-id: 645191ae0
Summary:
The exposed constructors for Memory and Concat Terms are only used in
a very special idiom: to construct an equality between a single Memory
chunk and the Concat of multiple Memory chunks. This diff specializes
and simplifies by exposing a Term.eq_concat constructor for this
idiom, and removes the underlying Term.memory and Term.concat
constructors.
Reviewed By: ngorogiannis
Differential Revision: D19221866
fbshipit-source-id: 4842737d2
Summary:
The size of Splats is redundant, as they always appear as subterms of
a Memory chunk or a heap segment, both of which are sized.
Reviewed By: ngorogiannis
Differential Revision: D19221870
fbshipit-source-id: 74044d1ad
Summary:
Now that they are uncurried, congruence closure does not need the
order of subterms to be preserved. Sorting them reduces redundancy in
case the same equality in different orders is encountered, and
improved printing.
Reviewed By: ngorogiannis
Differential Revision: D19221875
fbshipit-source-id: c6bf4ccad
Summary:
Reduce redundancy by printing adjacent segments as if they had been
concatenated together.
Reviewed By: ngorogiannis
Differential Revision: D19221881
fbshipit-source-id: 613105864
Summary:
Also, previous code was sometimes inconsistent regarding whether to
enumerate all subterms or only toplevel terms.
Reviewed By: ngorogiannis
Differential Revision: D19221873
fbshipit-source-id: e8644098b
Summary:
This diff enables parsing and auto-formatting documentation
comments (aka docstrings).
I have looked at this entire diff and manually made some changes to
improve the formatting. In some cases it looked like it would take too
much time, or benefit from someone more familiar with the code doing
it, and I instead disabled auto-formatting docstrings in those files.
Also, there are some source files where the docstrings are invalid,
and some where the structure detected by the parser appears not to
match what was intended. Auto-formatting has been disabled for these
files.
Reviewed By: ezgicicek
Differential Revision: D18755888
fbshipit-source-id: 68d72465d
Summary:
OCaml 4.08 supports a form of signature-local bindings, to that a type
can be defined in order to be used in other definitions, without
being part of the signature itself.
Reviewed By: ngorogiannis, jvillard
Differential Revision: D18736380
fbshipit-source-id: 0bb043de6
Summary:
It seems to be effectively unmaintained, as it still doesn't support
4.08.
Reviewed By: jvillard
Differential Revision: D18708467
fbshipit-source-id: dcb3361fc
Summary:
Term.solve makes the assumption that all distinct normalized constants
denote distinct values. This is fragile at best, and it is better to
enumerate the cases where solve discovers inconsistency.
Reviewed By: jvillard
Differential Revision: D18459619
fbshipit-source-id: 71f52557c
Josh Berdine