| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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)
|
|
Can now handle nexps such as (2**65 - 1). Uses big_ints for comparisons, and
keeps original nexps in the AST.
|
|
Also generate a function which initializes all the registers in a spec to undefined. This gives us the information we need post-rewriting to generate registers of any arbitrary type.
|
|
|
|
Rewriting of sizeofs and constraints seems to lose or hide some information
that the typechecker needs
|
|
|
