| Age | Commit message (Collapse) | Author |
|---|
|
Again use an $ifdef to avoid breaking RMEM. We can't use the same
barrier_kind, because we *really* want a plain enumeration both for
its simple SMT representation and a simple 1 to 1 mapping to the cat
models used by herd.
Technically for Isla, all the read_kind/write_kind/barrier_kind etc
types can be defined separately on a per-architecture basis anyway, so
maybe using this file at all is a bit of an anachronism.
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Allows keeping track of which instructions actually get executed in a trace
|
|
However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because
otherwise the generated lem for RMEM will break.
|
|
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.
|
|
|
|
|
|
Now used in RISC-V model.
|
|
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)
|
|
|
|
- add liftRS support to tactics
- define uint and sint in terms of functions without proof terms
- eq_vec correctness
- lemma that rounding up integers using reals is the obvious integer calculation
- another proof irrelevance tactic
- try lemmas in the sail hintdb both before and after goal processing
|
|
execution
|
|
|
|
|
|
|
|
|
|
Add github actions to build on macOS and ubuntu
|
|
This commit adds two github action to build Sail on macOS and ubuntu (both using the latest version
of each for now). These just build and don't run any tests, as we run those on our own Jenkins
server which is much faster than the github build runners.
I also fixed INSTALL.md to include brew installing pkg-config on macOS as this seems to be required.
From testing on a personal fork it seems quite email happy when it fails. Maybe that's what we want
though.
There's also a windows option but I leave that as future work...
|
|
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
|
|
- break up goals more in unbool
- remove intuition from guess_ex_solver because it can be too expensive
- flip goals around because the side that evars appears on has changed
- generalise the and/or tactics
- make a couple of tactics more specific/robust
|
