| Age | Commit message (Collapse) | Author |
|---|
|
The have_exception flag wasn't being cleared until after the handler,
resulting in false exception reporting.
|
|
Callable as either :f or :step_function
Allow // to be used as a comment in the interactive toplevel
|
|
sail -i now starts an interactive toplevel with a few additional
options set by default:
- It applies the "interpreter" rewrites to any files passed on the command
line.
- It also applies those rewrites after the :l/:load command
- Registers previously started in a disabled state, as the interactive shell
made no default decision as to how to handle undefined (which is the initial
value for all registers). Now -i implies -undefined_gen
- Better help text for :fix_registers
- Nullary interactive actions generate Sail functions that round-trip through pretty
printing and parsing (bugfix)
The -interact_custom flag has the same behavior as the previous -i flag
This commit also improves the c/ocaml/interpreter test harness so it
cleans up temporary files which could cause issues with stale files
when switching ocaml versions
|
|
Allows clients of sail as a library to define custom symbols for $ifdef
and $ifndef
Iterate vector concat assignment and tuple assignment to handle unusual
nesting cases when compiling to C. These rewrites should really be one
rewrite anyway though!
Don't add type annotations when introducing tuple patterns during
rewriting. I guess not adding them could also cause an error in some
circumstances, but if that's the case it could probably be fixed by
tweaking some rules in the type-checker.
|
|
|
|
|
|
|
|
From:
No type variable 'ex14#
to:
Type error:
[../and_let_bool.sail]:6:19-50
6 | and_bool(let y : bool = x in not_bool(y), x)
| ^-----------------------------^
| The type variable 'ex14# would leak into an outer scope.
|
| Try adding a type annotation to this expression.
| This error was caused by:
| [../and_let_bool.sail]:6:23-24
| 6 | and_bool(let y : bool = x in not_bool(y), x)
| | ^
| | Type variable 'ex14# was introduced here
|
|
|
Allows ASL-to-Sail translation to automatically patch lexp bounds check
errors.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #61
|
|
|
|
|
|
Tells the typechecker that, for example, in a block after
if (i < 0) then {
return ();
} else {
...
}
the constraint not(i < 0) holds. This is a useful pattern when
type-checking code generated from ASL.
|
|
|
|
|
|
Also uncovered a few other issues w.r.t lists
|
|
|
|
When returning a type from a letbinding we need to be careful that the
type it returns does not refer to any type variable that only exists for
the lifetime of the letbinding (because it was bound by it). Normally
this fails because any type variable bound in the inner letbinding won't
exist in the outer scope, but if it is shadowed this can cause an issue.
|
|
OCaml library
|
|
|
|
|
|
|
|
|
|
Also be more careful to avoid pattern bindings with identifiers to avoid
parsing clashes, eg `let 'bytes := ...` which is confused with the
notation for binary literals.
|
|
|
|
|
|
Useful for tracking down non-determinism
|
|
|
|
Was being overly conservative with nested structs and used an incorrect location for the error message
|
|
This is useful because an arbitrary vector of a fixed size N can be represented symbolically as a
vector of N symbolic values, whereas an arbitrary vector of arbitrary size cannot be easily
represented.
|
|
|
|
Instead handle it specially in c_backend, leaving the type information in the IR available for other consumers
|
|
(using match rather than let-and-projections because the latter would
be reduced by tactics like unfold)
|
|
|
|
execution
|
|
|
|
|
|
|
|
Now we less desugared ASL we'd like to translate some notions more idiomatically, such as bitfields
with names. However the current bitfield implementation in Sail is really ugly (entirely my fault)
This commit introduces a new flag -new_bitfields which changes the behavior of bitfields as follows
bitfield B : bits(32) = {
Field: 7..0
}
Is now treated as a struct with a single field called `bits`
register R : B
function main() -> unit = {
R[Field] = 0xFF;
assert(R[Field] == 0xFF)
}
then desugars as
R.bits[7..0] = 0xFF
and
assert(R.bits[7..0] == 0xFF)
which is much simpler, matches ASL and is probably how it should have worked all along
|
|
|
|
... not just in type abbreviations.
Fixes an error in the RV32 build of CHERI-RISC-V.
|
|
(plus test, as it wasn't covered before)
|
|
|
|
Don't include length and indexing order in Regval_vector constructor, as
these can get in the way of proofs without providing any value.
|
