| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
(monomorphisation uses them to decide where to case split)
|
|
Also handle any type variables from assignments and degrade gracefully
during constant propagation when unification is not possible.
|
|
|
|
Note that we might need to do both in future.
Also report more information when constructor refinement fails.
|
|
Needed for constructor monomorphisation
|
|
|
|
|
|
Avoids having to handle unexpected undefined values during constant
propagation.
|
|
|
|
Only requires a very small change to c_backend.ml. Most of this commit
is duplication of the builtins and runtime in lib/int128. But the
actual differences in those files is also fairly minor could be
handled by some simple ifdefs for the integer builtins.
|
|
|
|
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.
|
|
Need to get these working again before we can thing about merging back
into sail2
|
|
Get rid of separate V_op and V_unary constructors. jib.ott now defines
the valid operations for V_call including zero/sign extension, in such
a way that the operation ctyp can be inferred. Overall this makes the
IR less ad-hoc, and means we can share more code between SMT and C.
string_of_cval no longer used by c_backend, which now uses sgen_cval
following other sgen_ functions in the code generator, meaning
string_of_cval doesn't have to produce valid C code anymore and so can
be used for backend-agnostic debug and error messages.
|
|
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.
|
|
Add an Assumption event that is true whenever a property's type
quantifier is true, rather than wrapping body in a if-statement that
ends up creating a dead branch.
|
|
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.
|
|
|
|
|
|
|
|
|
|
- handle multiple bitvector length variables
- more fine-grained unnecessary cast insertion checks
- add tuple matching support to constant propagation (for the test)
|
|
|
|
|
|
- updates for type checking changes
- handle a little more pattern matching in constant propagation
- fix bug where false positive warnings were produced
- ensure bitvectors in tuples are always monomorphised (to catch the case
where the bitvectors only appear alone with a constant size)
|
|
|
|
|
|
as in other places
|
|
|
|
|
|
Probably need to clean-up the implementation and merge new_interpreter into
this branch before supporting re-checking counterexamples with more things.
|
|
|
|
|
|
Simple parser-combinator style parser for generated models. It's
actually quite tricky to reconstruct the models because we can have:
let x = something
$counterexample
function prop(x: bits(32)) -> bool = ...
where the function argument becomes zx/1 rather than zx/0, which is what
we'd expect for the argument of a property. Might need to do something
smarter with encoding locations into smt names to figure out what SMT
variables correspond to which souce variables exactly. The above
also previously generated incorrect SMT, which has now been fixed.
|
|
|
|
Add a new AE_write_ref constructor in the ANF representation to
make writes to register references explicit in Jib_compile
|
|
With the new interpreter changes computing the initial state for the
interpreter does some significant work. The existing code was
re-computing the initial state for every subexpression in the
specification (not even just the ones due to be constant-folded away).
Now we just compute the initial state once and use it for all constant
folds.
Also reduce the time taken for the simple_assignments rewrite from 20s
to under 1s for ARMv8.5, by skipping l-expressions that are already in
the simplest form.
|
|
(in particular, to cope with Type_check.simp_typ)
|
|
|
|
|
|
|
|
If we have e.g.
$property
val prop : ...
let X = 0
function prop(...) = X == ...
then we need to ensure that let X is included when we generate the
property.
|
|
|
