| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Also add a $suppress_warnings directive that ensures that no warnings
are generated for a specific file.
|
|
|
|
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.
|
|
Add a new short_loc_to_string function that produces just the file and line number as
a single line. loc_to_string adds a bunch of terminal color codes and other formatting
designed for producing pretty error-messages in the terminal, which isn't ideal when
the string appears in prover output as part of an assert statement. This is should be
purely an aesthetic change.
|
|
|
|
|
|
Work on improving the formatting and quality of error messages
When sail is invoked with sail -i, any type errors now drop the user
down to the interactive prompt, with the interactive environment being
the environment at the point the type error occurred, this means the
typechecker state can be interactively queried in the interpreter to help
diagnose type errors.
|
|
Also fix some C optimisations
|
|
This was _really_ slow - about 50secs for ARM. If this changes causes
breakages we should fix them in some other way.
Also using Reporting.err_unreachable in ANF translation, and fix slice
optimization when creating slices larger than 64-bits in C translation
|
|
Remove Parse_ast.Int (for internal locations) as this was unused. Add
a Parse_ast.Unique constructor to create unique locations. Change
locate_X functions to take a function modifying locations, rather than
just replacing them and add a function unique : l -> l that makes
locations unique, such that `locate unique X` will make a locations in
X unique.
|
|
There is no Reporting_complex, so it's not clear what the basic is
intended to signify anyway.
Add a GitHub issue link to any err_unreachable errors (as they are all
bugs)
|
