| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
|
|
|
|
Generate addresses, kinds, and values separately for read and write
events.
Add an mli interface for jib_smt.ml
|
|
|
|
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.
|
|
|
|
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.
|
