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
Summary:
Also minor change to make strlen implementation syntactically closer
to spec.
Reviewed By: ngorogiannis
Differential Revision: D14403647
fbshipit-source-id: 48c771329
Summary:
This diff adds support in symbolic execution for calls to intrinsic
functions, to be used in lieu of adding a separate Llair instruction
for each intrinsic. This involves:
- adding skeleton support in Exec for symbolically execution an
intrinsic function call;
- exposing this in Domain;
- allowing symbolic execution of block terminators (e.g. function
call) to possibly fail; and
- generalizing Report for failing terminators.
Reviewed By: ngorogiannis
Differential Revision: D14403652
fbshipit-source-id: d86d9d1b8
Timotej Kapus
Josh Berdine