| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues
|
|
Simply constraints further before calling Z3 to improve performance of
sizeof re-writing.
|
|
Now all ARM, RISC-V, and CHERI-MIPS all build successfully with
type-checking changes. All typechecker/c/ocaml/lem/builtin/riscv/arm
tests are now working as well.
Now the python test scripts can run sequentially with TEST_PAR=1 there's
no reason to keep the old shell versions around anymore.
|
|
|
|
Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of
uvar as the result of unify. Plus A_ could either stand for argument, or
Any/A type which is quite appropriate in most use cases.
Restore instantiation info in infer_funapp'. Ideally we would save this
instead of recomputing it ever time we need it. However I checked and
there are over 300 places in the code that would need to be changed to add
an extra argument to E_app. Still some issues causing specialisation to
fail however.
Improve the error message when we swap how we infer/check an l-expression,
as this could previously cause the actual cause of a type-checking failure
to be effectively hidden.
|
|
On a new branch because it's completely broken everything for now
|
|
|
|
This should make subtyping work better for tuples containing
constrained types. Removes the intermediate type-normal-form
representation from the subtyping check, and replaces it with
Env.canonicalize from the canonical branch.
|
|
New function Type_check.solve : Env.t -> nexp -> Big_int.num option.
Takes an environment and an n-expression (nexp), and returns either
Some u, where u is a unique solution such that nexp = u, or None which
indicates that either no unique solution could be found. It is
technically possible that a unique solution could exist, but Z3 may
not find it.
Involves two calls to Z3, one of which cannot be memoised, so should
be used carefully, as over-reliance could lead to performance issues.
|
|
|
|
|
|
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...
|
|
|
|
New option -memo_z3 memoizes calls to the Z3 solver, and saves these
results between calls to sail. This greatly increases the performance
of sail when re-checking large specifications by about an order of
magnitude. For example:
time sail -no_effects prelude.sail aarch64_no_vector.sail
real 0m4.391s
user 0m0.856s
sys 0m0.464s
After running with -memo_z3 once, running again gives:
time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail
real 0m0.457s
user 0m0.448s
sys 0m0.008s
Both the old and the new parser should now have better error messages
where the location of the parse error is displayed visually in the
error message and highlighted.
|
|
- Correctly pass exponentials to Z3
- Infer types of functional record updates
- Support "def Nat"
|
|
Other things:
* Cleaned up several files a bit
* Fixed a bug in the parser where (deinfix |) got parsed as (definfix ||)
* Turned of the irritating auto-indent in sail-mode.el
|
|
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)
|
