| Age | Commit message (Collapse) | Author |
|---|
|
As discussed previously, we wanted to start refactoring the re-writer
to make it a bit less monolithic, and in the future potentially break
it into separate files for backend-specific rewrites and stuff.
- rewriter.ml now contains the generic re-writing code
- rewrites.ml contains the rewriting passes themselves
It would be nice if the generic rewriting code didn't depend on the
typechecker, because then it could be used in ASL parser on untyped
code.
|
|
experiments
|
|
and_bool and or_bool now are treated specially in the ocaml backend,
so that they have the correct short-circuiting behaviour. This is
required so that assertions don't fail for the ARM spec for predicates
that shouldn't be tested in certain circumstances, for example things like:
IsAArch32() && AArch32_specific_predicate
Also fixed an issue in the sail library for ocaml where greater than
or equal to was being mapped to greater than.
|
|
|
|
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
|
|
|
|
|
|
|
|
Also, rename a few functions for uniformity, e.g. bool_and -> and_bool
|
|
|
|
embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
|
|
|
|
Map to calls to monadic function assert_exp that throws an exception if the
assertion is false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes a bug where resolving a type synonym failed in the Lem pretty-printer due
to a missing type environment.
|
|
|
|
- Bitvector pattern rewriting had stopped working due to a line of code being
lost in some merge.
- Fix a bug in early return rewriting that caused returns getting pulled out of
if-statements to disappear.
- There were some variable name clashes with keywords because doc_lem_id was
not always called.
- Ast_util.is_number failed to check for "int" and "nat" built-in types,
causing pattern matching on natural number literals to fail.
|
|
Assignments of the form "(v1, v2, v3) = vector" are common in ASL. They split
the vector on the right-hand side into subvectors and assign those to the
vectors in the tuple. The new rewriting step performs this splitting and
replaces the right-hand side with the tuple of subvectors. The assignment is
then handled by an existing rewriting step for tuple assignments.
|
|
Necessary for the Lem backend if effect checking is turned off in the type
checker: the monad translation needs proper effect annotations.
|
|
With -ddump_rewrite_ast, pretty-print Sail code after each rewriting step in
addition to dumping the AST.
|
|
Menhir pretty printer can now print enough sail to be useful with ASL parser
Fixity declarations are now preserved in the AST
Menhir parser now runs without the Pre-lexer
Ocaml backend now supports variant typedefs, as the machinery to
generate arbitrary instances of variant types has been added to the
-undefined_gen flag
|
|
|
|
|
|
|
|
- Remove start indices and indexing order from bitvector types. Instead add
them as arguments to functions accessing/updating bitvectors. These arguments
are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a
"sizeof" rewriting pass.
- Add a typeclass for bitvectors with a few basic functions (converting to/from
bitlists, converting to an integer, getting and setting bits). Make both
monads use this interface, so that they work with both the bitlist and the
machine word representation of bitvectors.
|
|
|
|
|
|
|
|
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
|
|
as GPR
This was wrongly translated as an update of the vector of references.
|
|
experiments
|
|
- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
term-level variable at the same time)
|
|
|
|
|
|
syntactically correct ocaml
|
|
E_internal_let is only used for introducing local variables, not updating
existing ones.
|
|
experiments
|
|
Works for basic examples with arbitrary register types, so for example we can compile:
val extern string -> unit effect pure print = "print_endline"
val unit -> string effect pure hello_world
function hello_world () = {
return "Hello, World!";
"Unreachable"
}
val unit -> unit effect {wreg, rreg} main
register string REG
function main () = {
REG := "Hello, Sail!";
print(REG);
REG := hello_world ();
print(REG);
return ()
}
into
open Sail_lib;;
let zhello_world () = with_return (fun r ->
begin r.return "Hello, World!"; "Unreachable" end);;
let zREG : (string) ref = ref (undefined_string ());;
let zmain () = with_return (fun r ->
begin
zREG := "Hello, Sail!";
print_endline !zREG;
zREG := zhello_world ();
print_endline !zREG;
r.return ()
end);;
let initialize_registers () = with_return (fun r -> zREG := undefined_string ());;
with the arbitrary register types and early returns being handled
appropriately, given a suitable implementation for Sail_lib
|
|
Don't pull out local variables that are introduced inside a sub-block.
|
|
Also, rewrite expressions in global let bindings (not only function bodies)
|
