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
Summary:
Match the `x` suffix naming convention of Term pp functions that take
a classification function.
Reviewed By: ngorogiannis
Differential Revision: D19282639
fbshipit-source-id: fc340e4bc
Summary:
Equality relies on the result of solving an equation to be a "solution
substitution". In constrast to unconstrained Map's, solution
substitutions are idempotent and have constraints on the terms that
may appear in their domain (they must be "maximal solvables", that is,
variables or uninterpreted function applications, which would be
variables if explicit "variable abstraction" was done).
This diff factors out the manipulation of concrete Map's into a
Equality.Subst module, and uses these for the result of `solve`.
Reviewed By: ngorogiannis
Differential Revision: D19282637
fbshipit-source-id: 4fc825e59
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:
Trace.infok is like Trace.info but accepts a polymorphic printf
continuation instead of directly taking a format string and its
args. This is useful to write wrappers such as:
```
let trace k = [%Trace.infok k]
```
Reviewed By: ngorogiannis
Differential Revision: D19221883
fbshipit-source-id: 88e939b26
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:
Equality.classes was assuming a simpler representation, and was
incomplete as a result.
The 'representative' map is not kept in a normalized form, where
subterms are necessarily representatives. Therefore, applying the
representative map to subterms of terms in a class can reveal new
elements of the class. This mirrors how the `lookup` function in
`normalize` works.
Reviewed By: ngorogiannis
Differential Revision: D19221868
fbshipit-source-id: 4a2ed6d3f
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: It is easier to understand the order of args with diff_inter.
Reviewed By: ngorogiannis
Differential Revision: D19221869
fbshipit-source-id: b29ac83c8
Summary:
Add some test cases from Reuss and Shankar for equality that are
mishandled by Shostak's original algorithm.
Reviewed By: ngorogiannis
Differential Revision: D19221880
fbshipit-source-id: a6f9d51e3
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:
OCaml 4.08 has a new warning (66) on unused `open!` statements. This
has a suboptimal interaction with `ppx_let`'s `let%map_open` which
leads to triggering the warning if any of a group of such let bindings
does not need the open.
In this case, the refactor is easy.
But, warning 66 is very dubious, so also just switch it off.
Reviewed By: jvillard
Differential Revision: D18708466
fbshipit-source-id: 77618ab6e
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
Summary:
Equality.or_ assumed a simpler representation of equality relations,
and was incomplete as a result.
Reviewed By: jvillard
Differential Revision: D18298138
fbshipit-source-id: cf91229f6
Summary:
The treatment of type conversions is too complicated, non-uniform,
etc. This diff attempts to simplify things by separating integer to
integer conversions, which are interpreted, from others, which are
essentially just uninterpreted functions. Integer conversions are now
handled using two expression and term forms: Signed and
Unsigned. These each interpret their argument as either a signed or
unsigned number of a given bitwidth:
```
| Signed of {bits: int}
(** [Ap1 (Signed {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit signed integer and injected into the [dst] type. That is,
it two's-complement--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth at least
[n]. *)
| Unsigned of {bits: int}
(** [Ap1 (Unsigned {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit unsigned integer and injected into the [dst] type. That
is, it unsigned-binary--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth greater than
[n]. *)
| Convert of {src: Typ.t}
(** [Ap1 (Convert {src}, dst, arg)] is [arg] converted from type [src]
to type [dst], possibly with loss of information. The [src] and
[dst] types must be [Typ.convertible] and must not both be
[Integer] types. *)
```
Reviewed By: ngorogiannis
Differential Revision: D18298140
fbshipit-source-id: 690f065b4
Summary:
Extend the APRON-backed interval analysis to handle a wider range
of LLAIR expressions.
Reviewed By: jvillard
Differential Revision: D17858072
fbshipit-source-id: c50f5bf20
Summary:
In some cases the result of an integer conversion needs to be
truncated by a bit.
Differential Revision: D18271179
fbshipit-source-id: e80740045
Summary:
Add a new interval abstract domain. This domain uses the APRON
numerical analysis library to keep track of the range of values held
by llair variables where possible. This works by translating LLAIR
expressions into APRON tree expressions, so only handles the
subset of the LLAIR expression language that can be embedded.
Note also that function summarization is not yet implemented.
Future commits will add summarization and improve coverage of
LLAIR's expression language.
Reviewed By: jberdine
Differential Revision: D17763517
fbshipit-source-id: 826ce4cc5
Summary:
The Used globals (pre-)analysis produces results queried by
Control. This diff adds a type definition for these and moves the
query into the Used_globals module.
Reviewed By: bennostein
Differential Revision: D17856879
fbshipit-source-id: 0211b82d7
Summary:
To avoid code explosion, the frontend emits move instructions for
expressions with more than one use. This diff relaxes this slightly by
allowing duplication of casts.
Reviewed By: bennostein
Differential Revision: D17856384
fbshipit-source-id: 6f6c496ef
Summary:
The frontend translation of exceptional control flow is untrusted
enough that it makes sense to disable it by default.
Reviewed By: bennostein
Differential Revision: D16061018
fbshipit-source-id: 65dca36ae
Summary:
The CFG of a function is implicit in the blocks themselves, so it is
possible to remove the explicit represention as a vector of
blocks. The only uses are fold or iter, and since the cycles are
detected during construction, these can be simple depth-first
traversals.
Reviewed By: bennostein
Differential Revision: D17821845
fbshipit-source-id: fc7a02151
Summary:
Fix a bug where the actual return variable was not scoped correctly in
cases where its name clashed with a local or formal of the
callee. Also comment and simplify to attempt to make more
understandable.
Reviewed By: bennostein
Differential Revision: D17801944
fbshipit-source-id: 286739241
Summary:
Some code that is otherwise benignly scalar still uses the
ExtractElement and InsertElement vector operations, so translate them
as if they were array operations.
Reviewed By: ngorogiannis
Differential Revision: D17801949
fbshipit-source-id: 89f3666bd
Summary:
By some unfortunate logic, OCaml often decides to use
`sexp_list`/`sexp_option` instead of just `list`/`option`. Sometimes
these get copy/pasted in interface files.
It would be good to tell OCaml not to do that in the first place but in
the meantime: this diff.
Reviewed By: ngorogiannis
Differential Revision: D17907938
fbshipit-source-id: 7546834a2
Summary:
For test scripting purposes, when the analysis finishes successfully,
report the number of alarms.
Reviewed By: ngorogiannis
Differential Revision: D17801947
fbshipit-source-id: 1660866df
Summary:
In a spec, it currently may be that foot.us does not contain xs. So
exec_specs needs to extend the vocabulary of foot before existentially
quantifying out xs.
Reviewed By: ngorogiannis
Differential Revision: D17801933
fbshipit-source-id: 7b4b9262a
Summary:
Previously it was added to the locals before calling Dom.call, but
this results in the scope of freturn ending too early.
Reviewed By: ngorogiannis
Differential Revision: D17801939
fbshipit-source-id: 739ec8981
Summary:
Some globals have 'appending' linkage, where linking modules results
in appending the arrays from each module. These can appear even when
empty, leading to useless and somewhat troublesome 0-length arrays. So
drop them.
Reviewed By: ngorogiannis
Differential Revision: D17801927
fbshipit-source-id: d2dc180d7
Summary:
While BitCasts are the identity function on the bitwise
representation, they are not necessarily so in the semantics or the
logical representation. So be more conservative about eliding them in
the Exp language. Those that are actually semantic identities are
still omitted in the Term language.
Reviewed By: ngorogiannis
Differential Revision: D17801950
fbshipit-source-id: bf9ae57b5
Summary:
The analyzer (currently) hard-codes some assumptions about sizes of
basic types such as Typ.bool, Typ.siz, etc. Check that these
assumptions are satisfied by the input llvm datalayout, and give
reasonable error messages otherwise.
Reviewed By: ngorogiannis
Differential Revision: D17801941
fbshipit-source-id: 4fe484ee0
Summary:
Now that expression types and type sizes can be computed, it is not
necessary to store the sizes of globals separately.
Reviewed By: ngorogiannis
Differential Revision: D17801932
fbshipit-source-id: f746e506b
Summary:
- The `Llvm_target.DataLayout.size_in_bits` needs to be used for checking casts
e.g. it is ok to `bitcast <16 x i1> to i16`: they both have 16 bits, but they have sizes 16 vs 2 bytes
- The `Llvm_target.DataLayout.abi_size` needs to be used for the size of memory blocks containing values
e.g. for the size of memory segments containing the initial values of globals
- The example above shows that we can't compute the byte size from the bit size without knowing the target specific datalayout
- So we need both in each sized type
- Also add checks that Convert exps and terms are not no-ops
- Simplifications of size manipulating code
Reviewed By: ngorogiannis
Differential Revision: D17801928
fbshipit-source-id: 8c8ce6128
Summary:
In order to type-check casts, it is necessary to have the size of each
sized type. This size information is also useful in a few other places.
Reviewed By: bennostein
Differential Revision: D17801931
fbshipit-source-id: f8ef53276
Summary:
This is needed since expressions distinguish between the integer or
pointer zero value and zero-initialized array/tuple/struct aggregates
based on type, and the backend distinguishes them semantically.
Reviewed By: bennostein
Differential Revision: D17801938
fbshipit-source-id: ac8665e65
Summary:
Linking can lead to opaque types becoming identified with a known
types. Assertions in various places that types should be sized can be
triggered by such opaque types. Until there is a distinction between
processing fully-linked versus incomplete code, these checks need to
be relaxed to permit opaque types where sized ones are expected.
Reviewed By: bennostein
Differential Revision: D17801929
fbshipit-source-id: c5e62f7c8
Summary: Integer terms need to compare higher than any monomial.
Reviewed By: bennostein
Differential Revision: D17725607
fbshipit-source-id: c64fd52d5
Summary:
Also weaken definition of Typ.castable to permit casting between
floats and ints of the same size.
Reviewed By: bennostein
Differential Revision: D17725611
fbshipit-source-id: 5e8114e26
Summary:
Typ.equivalent is currently defined the same as Typ.castable, but
conceptually they are different and castable needs to be
weakened. They are different since for example it is possible to cast
from an i64 to a f64, but those types denote different sets of values
in the semantics, and the bitcast is modeled using a conversion
function.
Reviewed By: bennostein
Differential Revision: D17725615
fbshipit-source-id: 973574f2a
Summary:
For function calls where the callee is a cast expression, previous the
wrong type would be used for the callee. This could lead to crashes in
llvm, or asserting in sledge.
Reviewed By: bennostein
Differential Revision: D17725610
fbshipit-source-id: 938b49a49
Summary:
Some called functions are represented in llvm as a global variable
with e.g. external linkage, and so they do not appear as
'functions'. It is still valid to call such functions, though the
analyzer does not know their definitions.
Reviewed By: bennostein
Differential Revision: D17725609
fbshipit-source-id: 333d19c0d
Summary:
Improve Trace.fail to log the error and raise informative exceptions.
Eliminate the confusion between Import.fail and Trace.fail by removing
Import.fail.
Reviewed By: bennostein
Differential Revision: D17725608
fbshipit-source-id: 79fdfbd86
Summary:
By default all functions except those specified as entry points in the
config file are "internalized". Internal functions are removed if they
are not called. It is sometimes necessary to disable internalization,
e.g. to analyze the llvm tests.
Reviewed By: bennostein
Differential Revision: D17725614
fbshipit-source-id: 4b13501f5
Summary:
Sometimes the models for the C/C++ runtime and standard libraries are
not needed. Furthermore, sometimes, e.g. when analyzing llvm tests,
trying to link them fails.
Reviewed By: bennostein
Differential Revision: D17725616
fbshipit-source-id: 76a4bcf90
Summary:
The `(t, unit) result` type is no more informative than `t option` and
less convenient.
Reviewed By: bennostein
Differential Revision: D17665244
fbshipit-source-id: fa969d8b7
Summary:
This puts the mediation between Exp and Term together in Sh_domain
rather than being spread across the two.
Reviewed By: bennostein
Differential Revision: D17665235
fbshipit-source-id: edf277d45
Summary:
The move instruction takes a vector of assignments to perform in
parallel, so generalize exec_move from one to a vector.
Reviewed By: bennostein
Differential Revision: D17665248
fbshipit-source-id: 52aae5ff9
Summary:
Extend the encoding using `id` from 0 indicating a program variable to
also -1 indicating a global program variable.
Reviewed By: bennostein
Differential Revision: D17665229
fbshipit-source-id: 848b8a31e
Summary:
The sorting of heap blocks when printing formulas was broken by the
change to the direct representation of polynomials.
Reviewed By: bennostein
Differential Revision: D17665246
fbshipit-source-id: 4ebea9f20
Summary: It is not necessary to have both < and >=, and similarly for <= and >.
Reviewed By: bennostein
Differential Revision: D17665232
fbshipit-source-id: 01b3511f5
Summary:
Now that terms operate over unbounded, signed, integers rather than
bounded integers, and Boolean operations are treated uniformly with
bitwise operations, it is not necessary to propagate types throughout
arithmetic term manipulation.
Reviewed By: bennostein
Differential Revision: D17665257
fbshipit-source-id: 5236b101d
Summary:
Z.numbits ignores the sign, which allows 2^(N - 1) as representable
within N bits, while it is not. So check explicitly.
Reviewed By: bennostein
Differential Revision: D17665231
fbshipit-source-id: 0d3940517
Summary:
Instead of having separate signed and unsigned operations, use the
signed operations applied to explicit conversion of the arguments
using an unsigned integer interpretation.
Reviewed By: bennostein
Differential Revision: D17665267
fbshipit-source-id: 0b3271e71
Summary:
Add an Extract term form to interpret an integer with given signedness
and bitwidth.
Reviewed By: bennostein
Differential Revision: D17665263
fbshipit-source-id: 1d8917f3c
Summary:
Be more explicit about semantics of unsigned vs. signed conversions,
and fix a few related corner cases.
Reviewed By: bennostein
Differential Revision: D17665268
fbshipit-source-id: 67fecdf34
Summary:
With terms using unbounded two's complement arithmetic, it is not
necessary to special-case 1-bit integers as Booleans.
Reviewed By: ngorogiannis
Differential Revision: D17665228
fbshipit-source-id: a2f280fc3
Summary:
Remove the guards that prevent normalizing in some cases where the
corresponding instruction in LLVM would produce a poison
value. Usefully tracking poison values will be more involved.
Reviewed By: ngorogiannis
Differential Revision: D17665230
fbshipit-source-id: 59fb25042
Summary:
Revise program expressions based on the changed constraints now that
Term is separate from Exp. In particular:
- Add types to all application, indicating how the operation
interprets its arguments
- Change to a simpler uncurried form
- Remove now-unneeded normalizations
Reviewed By: bennostein
Differential Revision: D17665236
fbshipit-source-id: 1bcf2efd6
Summary:
Boolean and bitwise negation of `e` is represented using `-1 xor
e`. Since Equality can only maintain and propagate equality
constraints, Boolean negation `-1 xor b` is normalized to `b =
false`. This diff delays this normalization from being part of
expression construction to part of symbolic heap formula
construction. This makes the normalization done as part of expression
construction independent of the distinction between bitwise and
boolean operations.
Reviewed By: bennostein
Differential Revision: D17665254
fbshipit-source-id: 0a0722865
Summary:
Splat, Memory, and Concat expressions are never used. Only the term
forms are needed.
Reviewed By: bennostein
Differential Revision: D17665259
fbshipit-source-id: cbfd7650d
Josh Berdine
Benno Stein
Jules Villard