| 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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
- 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)
|
|
|
|
|
|
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.
|
|
|
|
Comment out some interpreter tests that go into infinite loops because
those will cause issues for Jenkins.
|
|
|
|
|
|
Disabled by default because it's fairly resource heavy.
Currently two failures: a minor bug affecting divmod.sail, and undefined
values aren't set up for set_slice_bits.sail.
|
|
|
|
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.
|
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
Prevents some type variables that came from unpacking existentials
leaking into generated Coq types.
|
|
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to
target !opt_target ast env
This allows us to implement a :compile <target> command in the
interactive toplevel
Also implement a :rewrites <target> command which performs all the
rewrites for a specific target, so rather than doing e.g.
> sail -c -O -o out $FILES
one could instead interactively do
> sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit
for the same result.
To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
|
|
inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
|
|
Most such patterns are re-written away by various re-writing steps,
but for those that arn't they are fairly easy to handle by just having
as patterns directly in the ANF-patterns.
Fixes #39
|
|
Add a test case to ensure variable types in l-expressions remain the
same with flow-sensitive constraints.
|
|
In particular, spot variable shadowing and handle (n as 'm) patterns.
|
|
- add dummy print_bits function
- support int(1) like types in axioms
|
|
- skip a few more that aren't supported yet
- produce better debugging information (in particular, in the right order)
- avoid some autocasts that aren't supported yet and are usually
unnecessary
- Handle more constraints like `8 * n = 8 * ?Goal`
|
|
|
|
Rewrite <> true/false in goals.
Correct implicits in record and variant types.
Use expanded valspecs from the type checker in axioms.
Allow list notations in type definitions.
Skip some not-yet-supported tests.
|
|
|
