| 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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Generates much better SMT that assigning each field one-by-one
starting with an undefined struct.
|
|
|
|
Change specialisation so we only specialize integer parameters when
they are constant. This makes ensures that the integer-specialised
code is always type-correct.
|
|
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
|
|
Add some tests for arithmetic operations. Some tests fail in either Z3
or CVC4 currently, due to how overflow is handled.
|
|
Rather than generating SMT from a function called check_sat, now find
any function with a $property directive and generate SMT for it, e.g.
$property
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
$property
function prop_base_lteq_top(capbits: bits(128)) -> bool = {
let c = capBitsToCapability(true, capbits);
let (base, top) = getCapBounds(c);
let e = unsigned(c.E);
e >= 51 | base <= top
}
The file property.ml has a function for gathering all the properties
in a file, as well as a rewrite-pass for properties with type
quantifiers, which allows us to handle properties like
function prop forall 'n, 'n <= 100. (bv: bits('n)) -> bool = exp
by rewriting to (conceptually)
function prop(bv: bits(MAX_BIT_WIDTH)) -> bool =
if length(bv) > 100 then true else exp
The function return is now automatically negated (i.e. always true =
unsat, sometimes false = sat), which makes sense for quickcheck-type
properties.
|
|
|
|
|
|
Make sure struct fields can overlap each other, and function names
|
|
Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
is always true.
|
|
Currently only works with CVC4, test cases are in test/smt. Can prove
that RISC-V add instruction actually adds values in registers and
that's about it for now.
|
|
- Rename DeIid to Operator. It corresponds to operator <string> in the
syntax. The previous name is from when it was called deinfix in
sail1.
- Removed things that weren't actually common from
pretty_print_common.ml, e.g. printing identifiers is backend
specific. The doc_id function here was only used for a very specific
use case in pretty_print_lem, so I simplified it and renamed it to
doc_sia_id, as it is always used for a SIA.Id whatever that is.
- There is some support for anonymous records in constructors, e.g.
union Foo ('a : Type) = {
MkFoo : { field1 : 'a, field2 : int }
}
somewhat similar to the enum syntax in Rust. I'm not sure when this
was added, but there were a few odd things about it. It was
desugared in the preprocessor, rather than initial_check, and the
desugaring generated incorrect code for polymorphic anonymous
records as above.
I moved the code to initial_check, so the pre-processor now just
deals with pre-processor things and not generating types, and I
fixed the code to work with polymorphic types. This revealed some
issues in the C backend w.r.t. polymorphic structs, which is the
bulk of this commit. I also added some tests for this feature.
- OCaml backend can now generate a valid string_of function for
polymorphic structs, previously this would cause the ocaml to fail
to compile.
- Some cleanup in the Sail ott definition
- Add support for E_var in interpreter previously this would just
cause the interpreter to fail
|
|
Previously the specialization would remove any polymorphic union
constructor that was never created anywhere in the
specification. While this wasn't usually problematic, it does leave an
edge case where such a constructor could be matched upon in a pattern,
and then the resulting match would fail to compile as it would be
matching on a constructor kind that doesn't exists.
This should fix that issue by chaging the V_ctor_kind value into an
F_ctor_kind fragment. Previously a polymorphic constructor-kind would
have been represented by its mangled name, e.g.
V_ctor_kind "zSome_unit"
would now be represented as
V_ctor_kind ("Some", unifiers, ty)
where ty is a monomorphic version of the original constructor's type
such that
ctyp_unify original_ty ty = unifiers
and the mangled name we generate is
zencode_string ("Some_" ^ string_of_list "_" string_of_ctyp unifiers)
|
|
|
|
Allows us to track the last version of the return variable when the AST
in in SSA form.
|
