| Age | Commit message (Collapse) | Author |
|---|
|
The monomorphisation analysis decides whether to split function
arguments in the callee or in callers. The code previously used a
datastructure that can hold results of either the one case or the other,
but there might be functions that are called in different contexts
leading to different decisions. This patch changes the datastructure to
support storing all instances of either case.
|
|
If we call a function where some arguments need to be rewritten, we
might need to rewrite those parameters in the caller as well.
|
|
For example, in
let datasize = e in ...
the typechecker will generate a kid '_datasize if e has an existential
type (with one kid), and in
let 'datasize = e in ...
the typechecker will bind both 'datasize and '_datasize. If we
substitute one as part of constant propagation, this patch will make
constant propagation also substitute the other.
|
|
... and try to resolve them using constant propagation.
|
|
Split the variable (tuple) type into an input and output type. They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it). The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.
|
|
|
|
Check that indices are within bounds, not just in the right
(increasing/decreasing) order.
|
|
|
|
Asserting constraints from the loop condition in the body is fine for
while-loops, but doesn't make sense for until-loops.
|
|
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.
|
|
|
|
|
