| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
Make LEXP_deref an inference rule. This should allow strictly more programs to type-check.
|
|
|
|
This supports the following syntax:
type xlen : Int = 64
type ylen : Int = 1
type xlenbits = bits(xlen)
bitfield Mstatus : xlenbits = {
SD : xlen - ylen,
SXL : xlen - ylen - 1 .. xlen - ylen - 3
}
|
|
Tweak colours of monomorphistion test output
|
|
Fix monomorphisation tests
|
|
|
|
|
|
|
|
|
|
Make all backends behave the same when a catch block does not catch a
specific exception.
|
|
|
|
|
|
|
|
It now pushes casts into lets and constructor applications, and so
supports the case needed for RISC-V.
|
|
|
|
|
|
Now supports mutual recursion, configuration registers (in the same way
as Lem), boolean constraints (but produces some ugly stuff that the solver
can't handle).
|
|
|
|
|
|
Since Isabelle 2018, specifying the same directory both on the command
line and persistently in the user's ROOTS file is allowed, so we don't
have to choose between one or the other any more.
|
|
|
|
|
|
There are situations when we really want a more refined expression,
such as 8 * n instead of 64 (when we know n = 8 from a case split), but
we might not be able to generate it. For now we generate an underscore
and let Coq figure it out from the context.
|
|
|
|
|
|
Work on improving the formatting and quality of error messages
When sail is invoked with sail -i, any type errors now drop the user
down to the interactive prompt, with the interactive environment being
the environment at the point the type error occurred, this means the
typechecker state can be interactively queried in the interpreter to help
diagnose type errors.
|
|
Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues
|
|
and tests.
|
|
(Needed for current CHERI.)
|
|
Type variables can now be lexically scoped and shadow each other like normal variables,
rather than being required to be unique. This means we can use identifier names to
choose names for type variables in a way where we can assume they remain consistent
between type-checker runs. This means that re-writer steps can lift types out of
annotations in E_aux constructors and put them directly as syntactic annotations in the
AST - this should enable more robust rewrite steps.
Also fix RISC-V lem build w/ flow typing changes
|
|
This reverts commit 4d8a4078990a00ffdc018bc8f5d4d5e3dcf6527d.
|
|
This results in much better error messages, as we can pick readable
names that make sense, and should hopefully make the re-writer more
robust.
|
|
have to recompute it, which can be very expensive for very large
specifications
Also additional flow typing and fixes for boolean type variables
|
|
|
|
Add a file nl_flow.ml which can analyse a block of Sail expressions
and insert constraints for flow-typing rules which do not follow the
lexical structure of the code (and therefore the syntax-directed
typing rules can't do any flow-typing for). A common case found in ASL
translated Sail would be something like
function decode(Rt: bits(4)) = {
if Rt == 0xF then {
throw(Error_see("instruction"));
};
let t = unsigned(Rt);
execute(t)
}
which would currently fail is execute has a 0 <= t <= 14 constraint
for a register it writes to. However if we spot this pattern and add
an assertion automatically:
let t = unsigned(Rt);
assert(t != 15);
execute(t)
Then everything works, because the assertion is in the correct place
for regular flow typing. Currently it only works for this specific
use-case, and is turned on using the -non_lexical_flow flag
|
|
Some of the output from the tests scripts is odd on Jenkins, try to
fix this by flushing stdout more regularly in the test scripts
|
|
|
|
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.
|
|
Spawning a process for every test and running every test in parallel
is quite RAM intensive (up to about 8gb) especially when running
valgrind on every test in parallel. Now we only run up to TEST_PAR
tests in parallel (default 4).
|
|
|
|
test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.
// de Morgan
_prove(constraint(not('p | 'q) <--> not('p) & not('q)));
_prove(constraint(not('p & 'q) <--> not('p) | not('q)));
introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.
Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.
Also ensure that this test case works correctly in Lem
|
|
|
|
|
|
|
|
* Improve type inference for numeric if statements (if_infer test)
* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)
* Canonicalise all numeric types in function arguments, which
triggers some weird edge cases between parametric polymorphism and
subtyping of numeric arguments
* Because of this eq_int, eq_range, and eq_atom etc become identical
* Avoid duplicating destruct_exist in Env
* Handle some odd subtyping cases better
|
|
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.
|
