| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
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).
|
|
|
|
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.
|
|
Allows a quick hack where you can give a termination limit rather than a
proper measure for functions with awkward termination 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
|
|
|
|
Separate calling the rewriter from the backend-specific parts of
sail.ml
|
|
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.
|
|
|
|
Rather than each rewrite being an opaque function, with separate lists
of rewrites for each backend, instead put all the rewrites into a
single list then have each backend define which of those rewrites it
wants to use and in what order.
For example, rather than having
let rewrite_defs_ocaml = [
...
("rewrite_undefined", rewrite_undefined_if_gen false);
...
]
we would now have
let all_rewrites = [
...
("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b)));
...
]
let rewriters_ocaml = [
...
("undefined", [Bool_arg false]);
...
]
let rewrite_defs_ocaml =
List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_ocaml
This means we can introspect on the arguments required for each
rewrite, allowing a :rewrite command in the interactive mode which can
parse the arguments required for each rewrite, so we can invoke the
above rewrite as
sail> :rewrite undefined false
with completion for the rewrite name based on all_rewrites, and hints
for any arguments.
The idea behind this is if we want to generate a very custom slice of
a specification, we can set it up as a sequence of interpreter
commands, e.g.
...
:rewrite split execute
:slice_roots execute_LOAD
:slice_cuts rX wX
:slice
:rewrite tuple_assignments
...
where we slice a spec just after splitting the execute function. This
should help in avoiding an endless proliferation of additional options
and flags on the command line.
|
|
|
|
Propagating constants into mutually recursive calls and removing dead branches
might break mutually recursive cycles.
Also make constant propagation use the existing interpreter-based constant
folding to evaluate function calls with only constant arguments (as opposed to
a mixture of inlining and hard-coded rewrite rules).
|
|
|
|
Check in a slightly nicer stylesheet for OCamldoc generated
documentation in etc. Most just add a maximum width and increase the
font size because the default looks absolutely terrible on high-DPI
monitors.
Move val_spec_ids out of initial_check and into ast_util where it
probably belongs. Rename some functions in util.ml to better match the
OCaml stdlib.
|
|
Shouldn't affect anything as this is done by the typechecker now.
Also remove some unfinished tracing code from c_backend.ml
|
|
|
|
(e.g., for the dual 32/64 bit RISC-V model)
Apply this rewrite in Coq backend.
|
|
Rename rewrite_split_fun_constr_pats to rewrite_split_fun_ctor_pats as
constr is commonly used as an abbreviation for constraint rather than
constructor, and add a more descriptive comment.
|
|
Previously any constraints on constructors were just outright dropped
when splitting the execute function in Lem generation. Now we get the
constraints and type signature for each execute clause from the type
given by Env.get_union_constructor, rather than by inferring the type
of the pattern in each function clause.
Currently this can still fail in the case where we have
union U('x: Int), C1('x) = { ctor: {'y. C2('x, 'y), T('x, 'y)} }
and
val execute : forall 'z, C3('z). U('z) -> unit
when C3 implies C1, and the body of an excute clause relies on the
fact that C3 is stronger than C1, as each split function execute_ctor
is only guaranteed to be constrained by some subset of C1. This seems
unlikely to happen in practice though.
Also fix a bug when binding P as int('T) against int('T) and similar
cases, where the new type variable would cause the old type variable
to become shadowed, but the constraint that the bound type variable
and the old type variable are equal would not take this into account.
|
|
|
|
Can now set a prefix for generated C functions with -c_prefix so
-c_prefix sail_ would give sail_execute_CGetPerm over
zexecute_CGetPerm. We still have to use our standard name-mangling
scheme to avoid possible collisions within the name.
Can build C that doesn't expect the standard runtime, which leaves
operations like read_memory, write_memory etc to be stubbed in by
another C program including the generated Sail. Things like
letbindings are still an issue because we rely on a very small runtime
to initialize global letbindings and similar.
-c_separate_execute splits the execute function apart in the generated C
|
|
|
|
Run C tests with -O -Oconstant_fold -auto_mono
|
|
Perhaps suprisingly to some, this did not mean that Sail was
unable to typecheck the identify function.
While doing this rename Effect_opt_pure to Effect_opt_none - as
Effect_opt_pure was the effect equivalent of Typ_annot_opt_none,
and actually means that the function definition lacks an effect
annnotation, not that the function is actually pure, so this was
*extremely* misleading. The effect_opt that actually indicated a
function is pure was (and still is) the succinct:
Effect_opt_aux (Effect_opt_effect (Effect_aux (Effect_set [], _)), _)
In fact because in the grammar we only specify effects on
valspecs (they can always be inferred for fundefs in the absence
of a valspec) effect_opts are basically vestigial and are always
Effect_opt_none.
What might actually be super nice would be to remove rec_opt,
effect_opt and typ_annot_opt from fundefs in ast.ml altogether
and if we want them in the syntax just have them in parse_ast.ml
and pull them into a valspec during the initial check.
|
|
Fixes #34
|
|
This should produce identical Lem and Coq output, but allow dumped Sail
ASTs from the final stages of rewriting to be reread with -dmagic_hash.
|
|
This makes sure we don't do any kind of re-writing or de-scatter any
definitions when loading files into emacs. The difference here is that
normally all files are processed together, but the emacs mode loads
each file one by one. This is probably what we want to be doing
anyway, so location information stays accurate for scattered
functions for things like type-at-cursor commands and similar.
Also fix some warnings.
Fixes #32
|
|
|
|
Also make the rewriter keep failed assertions in output when pruning
blocks.
|
|
For example, in
type xlen : Int = 64
type xlenbits = bits(xlen)
rewrite the 'xlen' in the definition of 'xlenbits' to the constant 64 in
order to simplify Lem generation. In order to facilitate this, pass
through the global typing environment to the rewriting steps (in the AST
itself, type definitions don't carry annotations with environments).
|
|
add_num_def and get_num_def are no longer used. The rewrite pass that
used them would fail on Nexp_ids because of this, but seeing as that
never happened we can probably assume that particular line of code is
simply never touched by any of our models or test suite?
|
|
Various tweaks to the monomorphisation rewrites. Disable old sizeof
rewriting for Lem backend and rely on the type checker rewriting
implicit arguments. Also avoid unifying nexps with sums, as this can
easily fail due to commutativity and associativity.
|
|
|
|
All sizeof expressions now removed by the type-checker, so it's now
properly a type error if they cannot be removed rather than a bizarre
re-write error. This also greatly improves compilation speed overall, at
the expense of the first type-checking pass.
|
|
This reduces the amount of unnecessary complex existentials that appear
during rewriting.
|
|
|
|
|
|
|
|
now that cast insertion can handle RISC-V
Also inserts specs for casts in they're not present
|
|
|
|
|
|
|
|
For example in RISC-V for the translation table walk:
$optimize unroll 2
val walk32 ...
function walk32 ...
would create two extra copies of the walk_32 function,
walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2
being recursive. Currently we only support the case where we have
$optimize unroll, directly followed by a valspec, then a function, but
this should be generalised in future.
This optimization nearly doubles the performance of RISC-V
It is implemented using a new Optimize.recheck rewrite that replaces
the ordinary recheck_defs pass. It uses a new typechecker
check_with_envs function that allows re-writes to utilise intermediate
typechecking environments to minimize the amount of AST checking that
occurs, for performance reasons.
Note that older Sail versions including the current OPAM release will
complain about the optimize pragma, so this cannot be used until they
become up to date with this change.
|
|
Don't wrap effectful expressions in E_internal_return
|
