| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Added support for:
* Register type declarations
* Undefined literals
* Exit statement
* Toplevel let statements
* Vector literals i.e. [a, b, c]
* Binary bitvector literals
* Hex bitvector literals
Patched the parser so you can actually write 2**'n - 1 in a nexp. The
parser rules for nexps are a bit strange, and there didn't seem to be
anyway to write this before without it causing a parse error.
Can now typecheck up to line 332 of mips_prelude in mips/, but need to
add support for the implict passing of registers by names to go any
further, which should be fun...
|
|
|
|
|
|
|
|
Can now properly typecheck register declarations and assignments. Also
better support for assignments to mutable variables. Assignment to
immutable let bound variables is disallowed as it should be, and casts
when assiging to existing bound variables should be handled properly.
Added additional tests for these new features, and a new option
-just_check that allows the new checker to be run without the old.
|
|
Added basic support for vector types, and fixed various bugs. Also
added some basic tests for these features in test/typecheck.
|
|
|
|
|
|
Started work on a bi-directional type checking algorithm for sail
based on Mark and Neel's typechecker for minisail in idl
repository. It's a bit different though, because we are working with
the unmodified sail AST, and not in let normal-form.
Currently, we can check a fragment of sail that includes pattern
matching (in both function clauses and switch statements), numeric
constraints (but not set constraints), function application, casts
between numeric types, assignments to local mutable variables,
sequential blocks, and (implicit) let expressions.
For example, we can correctly typecheck the following program:
val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id
val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
{
switch x {
case ([|10:30|]) y -> y
case ([:31:]) _ -> sizeof 'N
case ([|31:40|]) _ -> plus(60,3)
}
}
and branch (([|51:63|]) _) = ten_id(sizeof 'N)
The typechecker has been set up so it can produce derivation trees for
the typing judgements and constraints, so for the above program we
have:
Checking function branch
Adding local binding x :: range<10, 'N>
| Check { switch x { case (range<10, 30>) y -> y case (atom<31>) _ -> sizeof 'N case (range<31, 40>) _ -> plus(60, 3)} } <= range<10, 'N>
| | Check switch x { case (range<10, 30>) y -> y case (atom<31>) _ -> sizeof 'N case (range<31, 40>) _ -> plus(60, 3)} <= range<10, 'N>
| | | Infer x => range<10, 'N>
| | Subset 'N >= 63 |- {'fv1 | 10 <= 'fv1 & 'fv1 <= 30} {'fv0 | 10 <= 'fv0 & 'fv0 <= 'N}
| | Adding local binding y :: range<10, 30>
| | | Check y <= range<10, 'N>
| | | | Infer y => range<10, 30>
| | | Subset 'N >= 63 |- {'fv4 | 10 <= 'fv4 & 'fv4 <= 30} {'fv3 | 10 <= 'fv3 & 'fv3 <= 'N}
| | Subset 'N >= 63 |- {'fv7 | 31 <= 'fv7 & 'fv7 <= 31} {'fv6 | 10 <= 'fv6 & 'fv6 <= 'N}
| | | Check sizeof 'N <= range<10, 'N>
| | | | Infer sizeof 'N => atom<'N>
| | | Subset 'N >= 63 |- {'fv10 | 'N <= 'fv10 & 'fv10 <= 'N} {'fv9 | 10 <= 'fv9 & 'fv9 <= 'N}
| | Subset 'N >= 63 |- {'fv13 | 31 <= 'fv13 & 'fv13 <= 40} {'fv12 | 10 <= 'fv12 & 'fv12 <= 'N}
| | | Check plus(60, 3) <= range<10, 'N>
| | | | | Infer 60 => atom<60>
| | | | | Infer 3 => atom<3>
| | | | Infer plus(60, 3) => atom<((60 - 20) + (20 + 3))>
| | | Subset 'N >= 63 |- {'fv20 | ((60 - 20) + (20 + 3)) <= 'fv20 & 'fv20 <= ((60 - 20) + (20 + 3))} {'fv19 | 10 <= 'fv19 & 'fv19 <= 'N}
Subset 'N >= 63 |- {'fv23 | 51 <= 'fv23 & 'fv23 <= 63} {'fv22 | 10 <= 'fv22 & 'fv22 <= 'N}
| Check ten_id(sizeof 'N) <= range<10, 'N>
| | | Infer sizeof 'N => atom<'N>
| | Prove 'N >= 63 |- 'N >= 10
| | Infer ten_id(sizeof 'N) => atom<'N>
| Subset 'N >= 63 |- {'fv28 | 'N <= 'fv28 & 'fv28 <= 'N} {'fv27 | 10 <= 'fv27 & 'fv27 <= 'N}
Judgements are displayed in the order they occur - inference steps go
inwards bottom up, while checking steps go outwards top-down. The
subtyping rules from Mark and Neel's check_sub rule all are verified
using the Z3 constraint solver.
I have been a set of tests in test/typecheck which aim to exhaustively
test all the code paths in the typechecker, adding new tests everytime
I add support for a new construct.
The new checker is turned on using the -new_typecheck option, and can
be tested (from the toplevel sail directory) by running:
test/typecheck/run_tests.sh -new_typecheck
(currently passes 32/32)
and compared to the old typechecker by
test/typecheck/run_tests.sh
(currently passes 21/32)
|
|
that uses the new Lem machine words library.
|
|
Instead of abusing patterns as expressions, bind patterns to names (if they are
more complex than an identifier or literal and don't have a name already) and
generate expressions referring to those names (which we then pass as arguments
to the auxiliary functions).
|
|
Before, wildcards sometimes ended up in the arguments to the function call on
the RHS, in particular when using vector patterns (which implicitly introduce
wildcards for the order and index parameters).
|
|
|
|
|
|
|
|
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
zero but it is not exposed via Bit_int_Z. Use it instead of rolling our own. Also ocaml / and mod already do the right thing.
|
|
|
|
|
|
for set_vector_subrange_bit.
|
|
|
|
|
|
|
|
Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work.
|
|
|
|
bytes. This makes loading binaries much quicker but doesn't seem to make a big difference to execution speed.
|
|
|
|
neater access to registers of single bit.
|
|
|
|
dependency on ocaml uint library by using it.
|
|
bit_int_of_int. Likely very little performance benefit but slightly more readable.
|
|
|
|
Also makes the check function in type_check tail recursive.
|
|
|
|
|
|
enable gprof profiling)
|
|
need to use power.
|
|
|
|
|
|
|
|
doesn't mistake the - for minus operator
|
|
between them using a command line switch.
|
|
|
|
neq_range.
|
|
|
|
|
