| Age | Commit message (Collapse) | Author |
|---|
|
Now compiles to C and builds a working executable. Just need to
correctly implement all the library builtins (some are still stubs),
and it should work.
|
|
|
|
(otherwise you end up with div(64,8) in output sizes!)
|
|
|
|
- Use simplified monad type (e.g., without the with_aux constructors that are
not needed by the shallow embedding).
- Add support for registers with arbitrary types (e.g., records, enumerations,
vectors of vectors). Instead of using bit lists as the common representation
of register values at the monad interface, use a register_value type that is
generated per spec as a union of all register types that occur in the spec.
Conversion functions between register_value and concrete types are generated.
- Use the same representation of register references as the state monad, in
preparation of rebasing the state monad onto the prompt monad.
- Split out those types from sail_impl_base.lem that are used by the shallow
embedding into a new module sail_instr_kinds.lem, and import that. Removing
the dependency on Sail_impl_base from the shallow embedding avoids name clashes
between the different monad types.
Not yet done:
- Support for reading/writing register slices. Currently, a rewriting pass
pushes register slices in l-expressions to the right-hand side, turning a
write to a register slice into a read-modify-write. For interfacing with the
concurreny model, we will want to be more precise than that (in particular
since some specs represent register files as big single registers containing a
vector of bitvectors).
- Lemmas about the conversion functions to/from register_value should be
generated automatically.
|
|
Also update the main aarch64 (no_vector) spec with latest asl_parser
|
|
Solves a problem where generated kids crept into type annotations during
rewriting and caused later typechecking passes to fail.
|
|
|
|
Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:
val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
function test (() : unit) -> unit = {
let matrix as vector('width, _, 'height) = mk_square ();
_prove(constraint('width = 'height));
()
}
where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax
let vector as 'length = ...
or even
let 'vector = ...
still works under this new scheme in a uniform way, so this is backwards compatible
The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.
|
|
|
|
|
|
|
|
For an enumeration type T, we can create a function T_of_num and num_of_T which convert from the enum to and from a numeric type. The numeric type is range(0, n) where n is the number of constructors in the enum minus one. This makes sure the conversion is type safe, but maybe this is too much of a hassle.
It would be possible to automatically overload all these functions into generic to_enum and from_enum as in Haskell's Enum typeclass, but we don't do this yet.
Currently these functions affect a few lem test cases, but I think that is only because they are tested without any prelude functions and pattern rewrites require a few functions to be defined
What is really broken is if one tries to generate these functions like
enum x = A | B | C
function f A = 0
function f B = 1
function f C = 2
the rewriter really doesn't like function clauses like this, and it seems really hard to fix properly (I tried and gave up), this is a shame as the generation code is much more succinct with definitions like above
|
|
|
|
|
|
Gives warnings when pattern matches are incomplete, when matches are
redundant (in certain cases), or when no unguarded patterns exist. For
example the following file:
enum Test = {A, C, D}
val test1 : Test -> string
function test1 x =
match x {
A => "match A",
B => "this will match anything, because B is unbound!",
C => "match C",
D => "match D"
}
val test2 : Test -> string
function test2 x =
match x {
A => "match A",
C => "match C"
/* No match for D */
}
val test3 : Test -> string
function test3 x =
match x {
A if false => "never match A",
C => "match C",
D => "match D"
}
val test4 : Test -> string
function test4 x =
match x {
A if true => "match A",
C if true => "match C",
D if true => "match D"
}
will produce the following warnings
Warning: Possible redundant pattern match at file "test.sail", line 10, character 5 to line 10, character 5
C => "match C",
Warning: Possible redundant pattern match at file "test.sail", line 11, character 5 to line 11, character 5
D => "match D"
Warning: Possible incomplete pattern match at file "test.sail", line 17, character 3 to line 17, character 7
match x {
Most general matched pattern is A_|C_
Warning: Possible incomplete pattern match at file "test.sail", line 26, character 3 to line 26, character 7
match x {
Most general matched pattern is C_|D_
Warning: No non-guarded patterns at file "test.sail", line 35, character 3 to line 35, character 7
match x {
warnings can be turned of with the -no_warn flag.
|
|
(makes some of the monomorphisation case splits smaller)
|
|
- Remove vector start indices
- Library refactoring: Definitions in sail_operators.lem now use Bitvector
type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes
TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.
|
|
This removes all type polymorphism, so we can generate optimized
bitvector code and compile to languages without parametric
polymorphism.
|
|
|
|
This change allows the AST to be type-checked after sizeof
re-writing. It modifies the unification algorithm to better support
checking multiplication in constraints, by using division and modulus
SMT operators if they are defined.
Also made sure the typechecker doesn't re-introduce E_constraint
nodes, otherwise re-checking after sizeof-rewriting will re-introduce
constraint nodes.
|
|
|
|
(rather than for each argument separately)
|
|
|
|
For example:
bitfield cr : vector(8, dec, bit) = {
CR0 : 7 .. 4,
LT : 7,
CR1 : 3 .. 2,
CR2 : 1,
CR3 : 0,
}
The difference this creates a newtype wrapper around the vector type,
then generates getters and setters for all the fields once, rather
than having to handle this construct separately in every backend.
|
|
* Changed comment syntax to C-style /* */ and //
* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.
* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:
X.GET(a, b, c) ==> _mod_GET(X, a, b, c)
X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c)
for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:
X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y)
Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.
* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.
type operator ... ('n : Int) ('m : Int) = slice('n, 'm)
struct cr = {
CR0 : 32 ... 35,
/* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
CR1 : 36 ... 39,
/* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
CR2 : 40 ... 43,
CR3 : 44 ... 47,
CR4 : 48 ... 51,
CR5 : 52 ... 55,
CR6 : 56 ... 59,
CR7 : 60 ... 63,
}
This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.
|
|
Experimenting with porting riscv model to new typechecker
|
|
|
|
The type-checker already supports a user-defined "exception" type that can be
used in throw and try-catch expressions. This patch adds support for that to
the Lem shallow embedding by adapting the existing exception mechanisms of the
state and prompt monads. User-defined exceptions are distinguished from
builtin exception cases. For example, the state monad uses
type ex 'e =
| Exit
| Assert of string
| Throw of 'e
to distinguish between calls to "exit", failed assertions, and user-defined
exceptions, respectively. Early return is also handled using the exception
mechanism, by lifting to a monad with "either 'r exception" as the exception
type, where 'r is the expected return type and "exception" is the user-defined
exception type.
|
|
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.
|
|
|
|
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.
|
|
|
|
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
Now constraints on type constructors are checked correctly when
checking that types are well formed using Env.wf_typ. The arity and
kind of type constructor arguments are also checked in the same way.
Also some general cleanups to the type checker code, with some
auxillary functions being moved to more appropriate files.
|
|
There are several key changes here:
1) This commit allows for user defined operations in n-expressions
using the Nexp_app constructor. These operations are linked to
operators in the SMT solver, by using the smt extern when defining
operations. Notably, this allows integer division and modular
arithmetic to be used in types. This is best demonstrated with an
example:
infixl 7 /
infixl 7 %
val operator / = {
smt: "div",
ocaml: "quotient"
} : forall 'n 'm, 'm != 0. (atom('n), atom('m)) -> {'o, 'o = 'n / 'm. atom('o)}
val mod_atom = {
smt: "mod",
ocaml: "modulus"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod_atom('n, 'm). atom('o)}
val "print_int" : (string, int) -> unit
overload operator % = mod_atom
val main : unit -> unit
function main () = {
let 'm : {'x, 'x % 3 = 1. atom('x)} = 4;
let 'n = m / 3;
_prove(constraint(('m - 1) % 3 = 0));
_prove(constraint('n * 3 + 1 = 'm));
(* let x = 3 / 0; (* Will fail *) *)
print_int("n = ", n);
()
}
As can be seen, these nexp ops can be arbitrary user defined operators
and even operator overloading works (although there are some caveats).
This feature is very experimental, and some things won't work very
well once you use custom operators - notably unification. However,
this not necissarily a downside, because if restrict yourself to the
subset of sail types that correspond to liquid types, then there is
never a need to unify n-expressions. Looking further ahead, if we
switch to a liquid type system a la minisail, then we no longer need
to treat + - and * specially in n-expressions. So possible future
refactorings could involve collapsing the Nexp datatype.
2) The typechecker is stricter about valspecs (and other types) being
well-formed. This is a breaking change because previously we allowed
things like:
val f : atom('n) -> atom('n)
and now this must be
val f : forall 'n. atom('n) -> atom('n)
if we want to allow the first syntax, then initial-check should
desugar it this way - but it must be well-formed by the time it hits
the type-checker, otherwise it's not clear that we do the right
thing. Note we can actually have top-level type variables by using
top-level let bindings with P_var. There's a future line of
refactoring that would make it so that type variables can shadow each
other properly (we should do this) - currently they all have to have
unique names.
3) atom('n) is no longer syntactic sugar for range('n, 'n). The reason
why we want to do this is that if we wanted to be smart about what
sail operations can be translated into SMT operations at the type
level we care very much that they talk about atoms and not
ranges. Why? Because atom is the term level representation of a
specific type variable so it's clear how to map between term level
functions and type level functions, i.e. (atom('n) -> atom('n)) can be
reflected at the type level by a type level function with kind Int ->
Int, but the same is not true for range. Furthermore, both are
interdefinable as
atom('n) -> range('n, 'n)
range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('n)}
and I think the second is actually slightly more elegant. This change
*should* be backwards compatible, as the type-checker knows how to
convert from atom to ranges and unify them with each other, but there
may be bugs introduced here...
|
|
Possibly useful for Brian's monomorphisation code
|
|
|
|
What does this mean? Basically undefined values can't be created for
types that contain free type variables, so for example: undefined :
list(int) is good, but undefined : list('a) is bad. The reason we want
to do this is because we can't compile them away statically, and this
leads to situations where type-checkable code fails in the rewriter
and gives horribly confusing error messages that don't relate to code
the user wrote at all.
As an example the following used to typecheck, but fail in the
rewriter with a confusing error message, whereas now the typechecker
should reject all cases which would trigger that failure in rewriting.
val test : forall ('a:Type). list('a) -> unit effect {wreg, undef}
function test xs = {
xs_mut = xs;
xs_mut = undefined; (* We don't know what kind of undefined 'a is *)
()
}
There's a slight hitch, namely that in the undefined_type functions
created by the -undefined_gen option, we do want to allow functions
that have polymorphic undefined values, so that we can generate
undefined generators for polymorphic datatypes such as:
union option ('a:Type) = {
Some : 'a,
None
}
These functions are always have a specific form that allows the
rewriter to succesfully remove the polymorphic undefined value for the
'a argument for Sone. As such there's a flag in the typechecking
environment for polymorphic undefineds that is enabled when it sees a
function with the undefined_ name prefix.
Also: Fixed some test cases that were broken due to escape effect being added to assert.
|
|
embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
|
|
|
|
|
|
|
