| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Fix SMT mem_builtin test case
|
|
|
|
|
|
These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.
|
|
If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.
|
|
In particular, bitvector subrange updates work with this version.
|
|
for 'exception.sail' test that deliberately exits with uncaught exception.
|
|
- additional rewrites (signed extend of subrange@zeros, subrange assignment,
variants with casts)
- drop # from new top-level type variables (e.g., n_times_8) so that the
rewriter knows that they're safe to include in casts
- add casts in else-branches when only one possible value for a size is left
- add casts when assertions force a size to be a particular value
- don't use types to detect set constraints in analysis because we won't
know which part of the assertion should be replaced
- also use non-top-level type variables when simplifying sizes in analysis
(useful when it can from pattern matching on an ast)
- cope with repeated int('n) in a pattern match (!)
|
|
|
|
|
|
|
|
slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends.
|
|
Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).
|
|
|
|
|
|
|
|
Add a test case for this
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Allow conversion between int(n) and int in smt_conversion
|
|
|
|
|
|
|
|
We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
|
|
Usually we do this at function applications and casts, but occasionally
a variable is used at a different type.
|
|
|
|
Generate addresses, kinds, and values separately for read and write
events.
Add an mli interface for jib_smt.ml
|
|
Previous commit changed the bitfield desugaring very slightly which
this test case relied upon.
|
|
Since we have __deref to desugar *x in this file (as it's the one file
everything includes) we might as well add a __bitfield_deref here too,
for the bitfield setters.
Make sure undefined_nat can be used in C
Both -memo_z3 and -no_memo_z3 were listed as default options, now only
-no_memo_z3 is listed as the default.
|
|
|
|
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
|
|
Generate SMT where the memory reads and writes are totally
unconstrained, allowing additional constraints to be added that
restrict the possible reads and writes based on some memory model.
|
|
|
|
|
|
Previously path conditionals for a node were defined as the path
conditional of the immediate dominator (+ a guard for explicit guard
nodes after conditional branches), whereas now they are the path
conditional of the immediate dominator plus an expression
encapsulating all the guards between the immediate dominator and the
node. This is needed as the previous method was incorrect for certain
control flow graphs.
This slows down the generated SMT massively, because it causes the
path conditionals to become huge when the immediate dominator is far
away from the node in question. It also changes computing path
conditionals from O(n) to O(n^2) which is not ideal as our inlined
graphs can become massive. Need to figure out a better way to generate
minimal path conditionals between the immediate dominator and the
node.
I upped the timeout for the SMT tests from 20s to 300s each but this
may still cause a failure in Jenkins because that machine is slow.
|
|
|
|
Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.
Strings are likewise encoded as SMTLIB strings, for similar reasons.
Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.
|
|
|
|
|
|
Also handle any type variables from assignments and degrade gracefully
during constant propagation when unification is not possible.
|
|
Fixes C backend optimizations that were disabled due to changes in the
IR while working on the SMT generation.
Also add a -Oaarch64_fast option that optimizes any integer within a
struct to be an int64_t, which is safe for the ARM v8.5 spec and
improves performance significantly (reduces Linux boot times by 4-5
minutes). Eventually this should probably be a directive that can be
attached to any arbitrary struct/type.
Fixes the -c_specialize option for ARM v8.5. However this only gives a
very small performance improvment for a very large increase in
compilation time however.
|
|
As an example:
$counterexample :query exist match_failure
function prop(xs: bits(4)) -> unit = {
match xs {
_ : bits(3) @ 0b0 => ()
}
}
Will return
Solver found counterexample: ok
xs -> 0x1
as we are asking for an input such that a match failure occurs,
meanwhile
$counterexample :query ~(exist match_failure)
function prop(xs: bits(4)) -> unit = {
match xs {
_ : bits(3) @ 0b0 => ()
}
}
will return 0x0 as we are asking for an input such that no match
failure occurs. Note that we can now support properties for
non-boolean functions by not including the return event in the query.
|
|
SMT query now expressed as a logical expression over events, so e.g.
let default_query =
Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow]
Checks either an overflow occurred, or the function returned true,
while all assertions held, and no match failures occurred. Currently
there is only the default query but the plan is to make this
user-specifiable in the $property/$counterexample directives.
|
|
Have assert events for assertions and overflow events for potential
integer overflow. Unclear how these should interact... The order in
which such events are applied to the final assertion is potentially
quite important.
Overflow checks and assertions are now path sensitive, as they should
be.
|
|
|
