| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Bind loop bounds to type variables, and don't pull existential variables
out of context
|
|
|
|
We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
Remove unused name schemes and DEF_kind
|
|
|
|
|
|
|
|
With the new comment syntax, Isabelle seems to barf on that comment,
apparently due to the backslashes.
|
|
|
|
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.
|
|
Remove redundant variables in boolean existentials. A situation can occur
during re-writing when patterns are re-written into simpler guarded
patterns, with the guard containing a large conjunction. Often those
individual conjuncts have no meaning for flow typing, but we'll still
generate a large conjunct bool('p & 'q & 'r & 's ...) for the guard. Now
we can simplify that return type by combining all the type variables
that don't give us any information into a single one, which improves
performance as we can avoid passing all those variables to the
constraint solver.
|
|
This ensures that mappings round-trip through the pretty-printer and
parser unchanged
Remove guarded_pats rewrite from C compilation. It causes a large
increase in compilation time due to how it interacts with flow
typing/pattern literal re-writing/and sizeof-rewriting
|
|
|
|
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.
|
|
(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.
|
|
Fixes some re-writer issues that was preventing RISC-V from building
with new flow-typing constraints. Unfortunately because the flow
typing now understands slightly more about boolean variables, the very
large nested case statements with matches predicates produced by the
string-matching end up causing a huge blowup in the overall
compilation time.
|
|
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".
|
|
have to recompute it, which can be very expensive for very large
specifications
Also additional flow typing and fixes for boolean type variables
|
|
|
|
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.
|
|
|
|
|
