| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
(which allows us to avoid a Coq bug where the proof isn't recorded
correctly)
|
|
With the new comment syntax, Isabelle seems to barf on that comment,
apparently due to the backslashes.
|
|
|
|
and tests.
|
|
(Needed for current CHERI.)
|
|
|
|
|
|
Annotating non-recursive functions as recursive in Lem output is
allowed, but will make Lem use "fun"/"function" commands when generating
Isabelle output, which is much slower to process than "definiton".
|
|
Also output termination measures in Sail printer
|
|
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
|
|
|
|
bool_of_bit and bit_of_bool in sail_lib
|
|
|
|
|
|
|
|
subrange_subrange_concat does a zero extension internally, so another
zero extension of its result is redundant and can lead to a type error
in Lem (because Lem's type system cannot calculate the length of the
intermediate result of subrange_subrange_concat).
|
|
Sizeof-rewriting could introduce extra arguments to functions that
instantiate_simple_equations could fill in with overly complicated
types, causing unification to fail when building lem.
|
|
|
|
|
|
|
|
|
|
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).
|
|
It now includes updating the effects so that morally pure recursive
functions can be turned into this impure termination-by-assertion form.
|
|
|
|
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
|
|
|
|
|
|
We should infer type variable kinds better in initial_check.ml, but we really don't want to have to deal
with that everywhere, especially when we can no longer easily cheat and assume KOpt_none implies K_int.
|
|
Remove some dead code in Pretty_print_common
Start thinking a bit about Minisail-esque syntactic sugar in initial_check
|
|
|
|
This only applies to recursive functions and uses the termination measure
merely as a limit to the recursive call depth, rather than proving the
measure correct.
|
|
|
|
* 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
|
