Summary:
It is pointless to track membership of atomic exps in the congruence
relation, as they cannot have any subexps which might later become
equal to something else.
Reviewed By: jvillard
Differential Revision: D15424820
fbshipit-source-id: 048dbc9e1
Summary:
For some Exp forms, Exp.solve is not complete, and this is necessary
since the result of solve is a substitution that needs to encode the
input equation as a conjunction of equations each between a variable
and an exp. This is tantamount to, stronger even than, the theory
being convex. So Exp.solve is not complete for some exps, and some of
those have constructors that perform some simplification. For example,
`(1 ≠ 0)` simplifies to `-1` (i.e. true). To enable deductions such as
`((x ≠ 0) = b) && x = 1 |- b = -1` needs the equality solver to
substitute through subexps of simplifiable exps like = and ≠, as it
does for interpreted exps like + and ×. At the same time, since
Exp.solve for non-interpreted exps cannot be complete, to enable
deductions such as `((x ≠ 0) = (y ≠ 0)) && x = 1 |- y ≠ 0` needs the
equality solver to congruence-close over subexps of simplifiable exps
such as = and ≠, as it does for uninterpreted exps.
To strengthen the equality solver in these sorts of cases, this diff
adds a new class of exps for = and ≠, and revises the equality solver
to handle them in a hybrid fashion between interpreted and
uninterpreted.
I am not currently sure whether or not this breaks the termination
proof, but I have also not managed to adapt usual divergent cases to
break this. One notable point is that simplifying = and ≠ exps always
produces genuinely simpler and smaller exps, in contrast to
e.g. polynomial simplification and gaussian elimination.
Note that the real solution to this problem is likely to be to
eliminate the i1 type in favor or a genuine boolean type, and
translate all integer operations on i1 to boolean/logical ones. Then
the disjunction implicit in e.g. equations between disequations would
appear as actual disjunction, and could be dealt with as such.
Reviewed By: jvillard
Differential Revision: D15424823
fbshipit-source-id: 67d62df1f
Summary:
* Adds compilation of cxxabi.bc
* Includes the cxxabi.bc into the sledge executable via opam-crunch
* Links cxxabi.bc in sledge frontend
Reviewed By: jberdine
Differential Revision: D15415190
fbshipit-source-id: cc42f09fb
Summary:
There are two motivations for this:
1. Distinguish between `Unreachable`, which silently terminates
execution a la `assume false`; and `Abort`, which vocally
terminates execution a la `assert false`.
2. Distinguish between undefined functions, which have `Unreachable`
bodies, and bomb functions such as:
```
define void bomb() {
tail call void llvm.trap()
unreachable
}
```
Reviewed By: ngorogiannis
Differential Revision: D15408246
fbshipit-source-id: b64354cdb
Summary:
Require a final `()` argument to explicitly indicate the end of the
arguments to the printf-like functions. For `warn` this is not
any safer because the return type is `unit` anyhow, but for `fail` the
return type is polymorphic so the final `()` prevents unintentionally
forgetting an argument.
Reviewed By: ngorogiannis
Differential Revision: D15403367
fbshipit-source-id: ce3fe4035
Summary:
llvm.trap is noreturn nounwind so calls to it are always succeeded by
Unreachable, therefore unless an alarm is desired for reaching it,
translating it as nop suffices.
Reviewed By: ngorogiannis
Differential Revision: D15328302
fbshipit-source-id: 54efe6c21
Summary:
A previous rebase fumble sometimes led to the wrong arguments being
passed to retpolines of Invoke instructions.
Reviewed By: ngorogiannis
Differential Revision: D15323950
fbshipit-source-id: f6eb6fbe2
Summary:
It is (now?) the case that `[%sexp_of: type_name]` generates just
`sexp_of_type_name`, rather than expanding `type_name` to its
definition and generating a conversion function for that. Hence, when
such cases appear within `let rec sexp_of_type_name`, they get
captured, sometimes leading to divergence.
This diff fixes this by manually expanding such types into their
definitions.
Reviewed By: ngorogiannis
Differential Revision: D15314736
fbshipit-source-id: 716fff7cc
Summary: There was a missing case for singleton monomials of degree > 1.
Reviewed By: mbouaziz
Differential Revision: D15098810
fbshipit-source-id: e6d17d899
Summary:
Boolean Xor expressions are treated directly by the solver, so the 'no
new subexps' invariant for congruence closure is not needed.
Reviewed By: mbouaziz
Differential Revision: D15098817
fbshipit-source-id: d118c5881
Summary: Shifting by too many bits is undefined, so do not normalize them.
Reviewed By: mbouaziz
Differential Revision: D15098812
fbshipit-source-id: 96f4606d7
Summary:
When constructing division expressions from rational coefficients of
polynomials, the constant numerator and denominator should be clamped
to the number of bits in the result type.
Reviewed By: mbouaziz
Differential Revision: D15098825
fbshipit-source-id: fa448c39a
Summary:
Some constants are used during Exp normalization, to encode
subtraction using addition, units of addition and multiplication,
etc. Previously these were unconditionally integers, but need to be
floats for float arithmetic.
Reviewed By: mbouaziz
Differential Revision: D15098815
fbshipit-source-id: 13d1be142
Summary:
The frontend would implicitly assume there was (at least) one argument
to calls to operator new. If code declares operator new with the wrong
type, this can lead to crashing trying to access a missing arg.
Reviewed By: mbouaziz
Differential Revision: D15098820
fbshipit-source-id: 539281a83
Summary: These relaxations are needed for some of the llvm test suite.
Reviewed By: mbouaziz
Differential Revision: D15098813
fbshipit-source-id: 702d3ffd9
Summary:
Some globals have initializers which refer to the global
itself (e.g. for program counter relative offsets). Memoizing
translation of globals gives enough machinery to detect and handle
this situation.
Reviewed By: mbouaziz
Differential Revision: D15098819
fbshipit-source-id: ecc9dce92
Summary:
In some cases there were extra metadata operands (such as alignment of
an alloc) which would cause the debug locations to not be recorded.
Reviewed By: mbouaziz
Differential Revision: D15098816
fbshipit-source-id: a7e83f590
Summary:
This reverts commit e4f7a0dc8d439561a0be7e8b33ad924195a6c441.
No longer needed due to ocamlformat fix.
Reviewed By: mbouaziz
Differential Revision: D15098826
fbshipit-source-id: 2a4dc0f55
Summary:
When comparing stacks as part of a control-flow edge, treat each as a
code location in a hypothetical expansion of the program where all
non-recursive functions have been completely inlined. In particular,
this means to compare stacks as if all Locals frames or Return frames
for recursive calls had been removed. Additionally, the from_call info
in Return frames is ignored.
Reviewed By: jvillard
Differential Revision: D14657601
fbshipit-source-id: b8a42d3fa
Summary:
- Ensure that popping Throw or Return does not leave stale Throw or
Return frames
- Add a module for Control.stack
- Add invariant to enforce that a Throw frame can appear only
immediately above a Return frame
Reviewed By: jvillard
Differential Revision: D14547263
fbshipit-source-id: deb31b8af
Summary:
The backend does not generally interpret conditional expressions
specially. Therefore it is logically stronger to hoist them over other
boolean exps, for example normalizing
`e = (c ? t : f)` to `(c ? e = t : e =f)`
This enables the treatment of top-level conditional expressions in
terms of disjunction, conjunction and negation.
Reviewed By: mbouaziz
Differential Revision: D14495815
fbshipit-source-id: 4f2e8053f
Summary:
Eq and Dq expressions are interpreted by Equality and Exp, rather than
being considered uninterpreted functions. Classifying them as
interpreted results in stronger Equality normalization.
Reviewed By: mbouaziz
Differential Revision: D14495817
fbshipit-source-id: 44bb376c0
Summary: Also fix the spec for posix_memalign, and minor cleanup.
Reviewed By: ngorogiannis
Differential Revision: D14403648
fbshipit-source-id: 6b1cb3e3a
Summary:
The SL solver is currently not always able to append segments which
have been split symbolically, that is, at an internal point expressed
using a variable, rather than merely a constant.
Also, existential instantiation, that is, the choice of witnesses
during proof search, is currently sensitive to the order of
subformulas. This can lead to fragile incompleteness.
Reviewed By: mbouaziz
Differential Revision: D14481991
fbshipit-source-id: 80fe2f0a8
Summary:
Strengthen the Sh.seg constructor and Sh.is_false test to account for
the axiom that `null -[_;_)-> ⟨_,_⟩` is inconsistent.
Reviewed By: ngorogiannis
Differential Revision: D14481986
fbshipit-source-id: 7016e7451
Summary:
The dnf implementation dates to before nested existentials were
added. Updating it was overlooked, and it is just wrong.
Reviewed By: ngorogiannis
Differential Revision: D14481988
fbshipit-source-id: 9bba570f0
Summary:
P ∨ (∃x. Q ∨ R) could be simplified to (∃x. P ∨ Q ∨ R) and capture
occurrences of x in P.
Reviewed By: ngorogiannis
Differential Revision: D14481990
fbshipit-source-id: 92b474d59
Josh Berdine
Timotej Kapus