| Age | Commit message (Collapse) | Author |
|---|
|
Added a regression test in test/ocaml/string_of_struct
|
|
|
|
Also updated some of the documentation in the sail source code
|
|
|
|
Fixed test cases for ocaml backend and interpreter
|
|
|
|
New testcase for bitfield syntax
Updated to work with latest lem and linksem
|
|
|
|
|
|
Works with the vector branch of asl_parser
|
|
Add the ast.sed script we need to build sail. Currently we just need
this to fix up the locations in the AST but it will be removed once we
can share locations between ocaml and lem.
|
|
|
|
Improved handling of try/catch
Better handling of unprovable constraints when the environment contains
false
|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
Added a test case for this behavior
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
|
For example:
val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit
val main : unit -> unit
function main () = {
test ();
}
for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.
Also fixed some bugs in the ocaml backend.
|
|
|
|
|
|
|
|
Cleaned up the option list in sail.ml
|
|
Fixed an issue in ast.ml with uneccessary type variables
|
|
|
|
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
|
|
|
|
|
|
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
syntactically correct ocaml
|
|
files into runable executable.
|
|
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
|
