| Age | Commit message (Collapse) | Author |
|---|
|
The have_exception flag wasn't being cleared until after the handler,
resulting in false exception reporting.
|
|
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
|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
Was being overly conservative with nested structs and used an incorrect location for the error message
|
|
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
|
|
|
|
(plus test, as it wasn't covered before)
|
|
|
|
|
|
|
|
|
|
The following is therefore always forbidden
```
scattered union U
enum E = A | B | C
union clause U = Ctor : E
```
We attempt to detect when this occurs and include a hint indicating the
likely reason why a 'Undefined type E' error might occur in this
circumstance
|
|
|
|
Ensure we give a nice error message that explains that recursive types are forbidden
```
Type error:
[struct_rec.sail]:3:10-11
3 | field : S
| ^
| Undefined type S
| This error was caused by:
| [struct_rec.sail]:2:0-4:1
| 2 |struct S = {
| |^-----------
| 4 |}
| |^
| | Recursive types are not allowed
```
The theorem prover backends create a special register_value union that
can be recursive, so we make sure to special case that.
|
|
|
|
|
|
- in particular at monadic interfaces (i.e., sufficient for instruction
ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)
|
|
|
|
|
|
|
|
|
|
Mostly in the Coq backend, plus a few testcases that use bitvector
builtins on poly-vectors (which works on some backends, but not Coq).
Also handle some additional list inclusion proofs in Coq.
|
|
|
|
Fixes #53
|
|
|
|
|
|
Fix SMT mem_builtin test case
|
|
|
|
|
|
|
|
|
|
Do this by making sure that generic pattern literal re-writing gets
applied to top-level function clauses. This requires re-ordering the
rewrites for most backends otherwise they break, which hopefully wo
anything.
After doing this re-ordering I had to turn off casting when rewriting
bitvector patterns, otherwise insane things can happen.
|
|
|
|
|
|
These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.
|
|
If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.
|
|
In particular, bitvector subrange updates work with this version.
|
|
for 'exception.sail' test that deliberately exits with uncaught exception.
|
|
- additional rewrites (signed extend of subrange@zeros, subrange assignment,
variants with casts)
- drop # from new top-level type variables (e.g., n_times_8) so that the
rewriter knows that they're safe to include in casts
- add casts in else-branches when only one possible value for a size is left
- add casts when assertions force a size to be a particular value
- don't use types to detect set constraints in analysis because we won't
know which part of the assertion should be replaced
- also use non-top-level type variables when simplifying sizes in analysis
(useful when it can from pattern matching on an ast)
- cope with repeated int('n) in a pattern match (!)
|
|
|
|
|
