| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
|
|
If, for example, we have a bidirectional encoding-decoding mapping as in
sail-riscv, but want to translate only the decoder to a theorem prover,
this commit allows us to stub out the the encoder by splicing in dummy
definitions.
|
|
|
|
The val spec generation for partially evaluated function copies did not
pick up type variables originally declared using the new "constant"
syntax, as well as some implicit existential variables (e.g. in "bool")
that were not declared originally but appear and get bound during
instantiation. Change the code to just recreate the list of type
variables from scratch from the new type. This will lose "constant"
annotations, but the new list of type variables should be correct.
|
|
When considering whether to add a cast, now also consider the updated
environment within an if branch / match clause to compare against the
outer environment. This picks up not only constraints on type variables
added by an if condition or pattern guard (e.g. "if (size == 16) ..."),
but also constraints depending on those (e.g. in "bits('width)" where
"'width == 'size * 8"). Fixes a type error observed when generating Lem
for sail-arm (in aget__Mem).
|
|
... with one field per register *type*, instead of one field per
register. The fields store functions from register name to value.
This leads to dramatically reduced processing time for the register
state record in HOL4.
|
|
|
|
Means we can avoid the use of -undefined_gen for Sail->SMT
|
|
|
