| Age | Commit message (Collapse) | Author |
|---|
|
Some SMT goals in unification would generate problems with missing
variables. Turns out the SMT solver would happily ignore this and
return the correct unsat/sat result anyway. However, this does affect
the error code from the solver so if we now check the return code we
must make sure that we don't generate any smtlib files that generate
warnings or errors.
Now that kopts_of_X functions exist in ast_util we can just use those
to get well-kinded variables from the constraint itself rather than
relying on the typechecker to pass in a list of variables which makes
things simpler to boot!
|
|
When adding a constraint such as `x <= 2^n-1` to an environment
containing e.g. `n in {32, 64}` or similar, we can enumerate all
values of n and add `n == 32 & x <= 2^32-1 | n == 64 & x <= 2^64-1`
instead. The exponentials then get simplified away, which means that
we stay on the SMT solver's happy path.
This is enabled by the (experimental, name subject to change) flag
-smt_linearize, as this both allows some things to typecheck that
didn't before (see pow_32_64.sail in test/typecheck/pass), but also
may potentially cause some things that typecheck to no longer
typecheck for SMT solvers like z3 that have some support for reasoning
with power functions, or where we could simply treat the exponential
as a uninterpreted function.
Also make the -dsmt_verbose option print the smtlib2 files for the
solve functions in constraint.ml. We currently ignore the -smt_solver
option for these, because smtlib does not guarantee a standard format
for the output of get-model, so we always use z3 in this case.
Following the last commit where solve got renamed solve_unique, there
are now 3 functions for solving constraints:
* Constraint.solve_smt, which finds a solution if one exists
* Constraint.solve_all_smt, which returns all possible
solutions. Currently there's no bound, so this could loop forever if
there are infinite solutions.
* Constraint.solve_unique, which returns a unique solution if one exists
Fix a bug where $option pragmas were dropped unnecessarily.
|
|
|
|
Useful to see what constraints we are generating that are particularly
hard, and which of our specs work with different solvers.
Refactor code to use smt in names rather than specifically z3
|
|
Simply constraints further before calling Z3 to improve performance of
sizeof re-writing.
|
|
On a new branch because it's completely broken everything for now
|
|
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.
|
|
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)
|
