| Age | Commit message (Collapse) | Author |
|---|
|
Makes the generated undefined functions smaller, easier to read, and
avoids excessive memory usage in Coq (e.g., for large AST types).
|
|
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
|
|
|
|
|
|
(should really make the Lem pretty printer use the solver properly,
but this is a useful stopgap)
|
|
|
|
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.
2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.
The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.
3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.
4. Include a newly generated version of aarch64_no_vector
5. Update the Ocaml test suite to use builtins in lib/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Take into account existential types when determining bounds for the loop
variable
|
|
|
|
This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in
```
val f : nat -> nat
let x = f(3)
```
whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.
Also:
- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
pass didn't add type paramemters for newly added type variables in
generated function parameters.
- Updated string_of_ functions in ast_util to reflect syntax changes
- Fixed a C compilation issue where elements of union type
constructors were not being coerced between big integers and 64-bit
integers where appropriate
- Type annotations in patterns now generalise, rather than restrict
the type of the pattern. This should be safer and easier to handle
in the various backends. I don't think any code we had was relying
on this behaviour anyway.
- Add inequality operator to lib/flow.sail
- Fix an issue whereby top-level let bindings with annotations were
checked incorrectly
|
|
Now it just returns the actual arguments and a separate function
calculates the start index when required.
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits. Undefined
cases can be handled in different ways:
- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
default so far),
- return an option type,
- raise a failure in the monad, or
- use a bitstream oracle to resolve undefined bits.
This patch adds different versions of partial functions corresponding to those
options. The desired behaviour can be selected by choosing a binding in the
Sail prelude. The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.
|
|
For example, generates an auxiliary function execute_ADD (rs, rt, rd) for the
clause execute (ADD (rs,rt,rd)) = ...
Without this rewriting, the execute function easily becomes too large to be
handled by Isabelle (e.g., for CHERI-MIPS; for MIPS alone, it seems to be just
about small enough).
This used to be implemented in the pretty-printer, but that code was commented
out recently in order to support a recursive execute function for RISC-V
compressed instructions.
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
The rewriter ignored loops that were not contained within some let-binding,
which later caused the Lem pretty-printer to fail (see #8).
|
|
One caveat still: Won't work if the polymorphic definition consists of
multiple function clauses, but this seems unlikely - and I added an
error message if this is the case.
Also fix a small flow typing bug
Fixes #7
|
|
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)
|
