| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes some bugs found by doing this
|
|
|
|
Also make unifying int against int('n) work as expected for
constructor applications.
|
|
|
|
|
|
|
|
Issues came up with Christophers translation of hand-written ARM into
Sail2 where we were being overly pedantic about the exact position of
existential quantifiers in constructors with multiple arguments. This
commit generalises unify_typ and type_coercion_unify to be more
flexible and support this. Should think at some point if unify_typ can
be generalised further.
This fix should fix the decode side of things, but may be some issues
with the executes that still need looking into when existentials and
multiple argument constructors are mixed.
|
|
|
|
|
|
|
|
Just enough for RISC-V to go through
|
|
Also drop unused implication function
|
|
|
|
|
|
Now generates something vaguely sensible for RISC-V, although the solver
needs a little work.
Adds type annotations around effectful, rich and/or expressions.
|
|
Make internal_plet produce annotations (with code to replace unusable
type variables)
Add mappings for bool kids at bindings
Add version of and_bool that proves a property
|
|
|
|
|
|
|
|
Also make pretty printing more keen on line breaking
|
|
This introduces some simplification of informative booleans, but tries
too hard to eliminate all of the existentials resulting in difficulties
in and/or trees.
|
|
For example:
sail -c_extra_params "CPUMIPSState *env" -c_extra_args env
would pass a QEMU MIPS cpu state to every non-builtin function call.
Also add documentation for each C compilation option in C_backend.mli
|
|
|
|
|
|
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
|
|
|
|
The old check used the wrong part of the AST. It would stop when it
reached the actual effect, anyway, but this should improve performance.
|
|
Add a flag in C backend ctx that allows us to generate arbitrary
precision signed integer types, rather than just int64
|
|
|
|
|
|
|
|
If we want to use our low-level intermediate representation to generate
SMT, then we want to be more precise than just splitting integers into
64-bits and larger. This commit changes CT_int and CT_int64 into CT_lint
for large integers and CT_fint n for (signed) fixed precision integers
that fit within n bits. This follows the convention for bitvectors where
we have CT_fbits for fixed-length bitvectors and CT_lbits for large
arbitrary precision bitvectors.
|
|
|
|
|
|
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.
|
