| Age | Commit message (Collapse) | Author |
|---|
|
|
|
If a SEE exception is not caught within the decoder, it is
an error in the Sail implementation or in the instruction set spec.
This change ensures that we promptly detect and unambiguously report
such errors.
|
|
This change causes execution of AArch32 code or ASIMD code
to fail with an easily diagnosed error message of the form
UNIMPLEMENTED: xxx support
where xxx is either AArch32 or ASIMD.
Having a clear error message allows these to be detected by triaging
scripts.
To make the AArch32 detection part work, you also need to change
HaveAnyAArch32 to read like this instead of just returning false.
function HaveAnyAArch32 () =
return ((CFG_ID_AA64PFR0_EL1_EL0 == 0x2)
|| (CFG_ID_AA64PFR0_EL1_EL1 == 0x2)
|| (CFG_ID_AA64PFR0_EL1_EL2 == 0x2)
|| (CFG_ID_AA64PFR0_EL1_EL3 == 0x2))
|
|
read/maintain
|
|
While trying to track down some strange behaviour, I added a lot
more try-catch blocks that I think will be useful in the future.
Also dropped spurious escape effects on primops.
Also, only advance PC if we executed an instruction.
|
|
It appears that primops that have the escape effect are required to
write to the have_exception flag so I am dropping the effect from
primops that don't actually escape.
|
|
This is interpreted as a set of bits that control various bits of output.
Bit 0 is print the PC on every cycle.
(It would probably be useful to standardise a few of these flags across
all models. Other candidates are accesses to physical memory, throwing
SAIL exceptions, current privilege level, ...)
|
|
|
|
- Initialise fault typ field of result record to avoid an unitialised read that
can lead to an early return with a fault. This looks like a bug in the ASL
specification (the ASL tests probably assume that this field is initialised
with Fault_None).
- In ZeroExtend_slice_append (one of the helper functions for monomorphisation
rewrites), use extzv instead of ZeroExtend. It allows not only extension,
but also truncation, and in AArch64_TranslationTableWalk the
ZeroExtend_slice_append function is used to construct a 52 bit physical address
using parts of the 64 bit input address.
- Use the Lem library function for reversing endianness
|
|
If you don't exit immediately, the test will probably just jump off into the
weeds and stay there until it times out. So better to exit early.
But note that this is not all IMPDEF behaviour.
Most IMPDEF such as 'Are SHA3 crypto instructions available?' are already
being handled and either TRUE or FALSE is being returned.
So this is just for the stuff where we don't have a good answer at all.
|
|
|
|
No functional change
|
|
|
|
Mostly improving error messages
|
|
|
|
|
|
Note that an alternative implementation choice is just to implement
them as SAIL functions manipulating a global variable.
Not sure which is better.
|
|
|
|
|
|
|
|
optimizations.
Move the utility functions for graph generation and pretty printing of
intermediate representation instructions into a separate file,
bytecode_util.ml, by analogy with ast_util.ml.
Add an optimization pass that searches for specific patterns of struct
updates and removes uncessary copying of the structs involved. With
this optimisation pass the time taken for u-boot to run approx
57,000,000 instructions goes down from about 11-12 minutes to 8
minutes (about 120,000 IPS).
|
|
Also add an additional -Oz3 flag that uses z3 to optimize some
additional types. This is currently very experimental and doesn't
fully work yet.
|
|
|
|
|
|
Worked around problem with the model where it tries to use bound variables
in patterns
|
|
|
|
|
|
Move mono_rewrites into lib
|
|
|
|
Mostly introducing type variables for regsize in valspecs
|
|
|
|
|
|
|
|
|
|
|
|
Typechecking for-loops failed after the Lem rewriting passes in some cases: if
the lower bound for the loop may be greater than the upper bound, the loop
variable's type might be empty, and it cannot be initialised. This patch adds
a guard "lower <= upper" around the loop body, and removes it again during
pretty-printing.
|
|
+ add additional lexp
+ update aarch64 mono demo source
- still needs support for tyvars from assignments in dependency analysis
|
|
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.
2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.
The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.
3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.
4. Include a newly generated version of aarch64_no_vector
5. Update the Ocaml test suite to use builtins in lib/
|
|
|
|
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
They are used in various specs and test cases.
|
|
(note that they're already declared in lib/arith.sail)
|
|
|
|
This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in
```
val f : nat -> nat
let x = f(3)
```
whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.
Also:
- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
pass didn't add type paramemters for newly added type variables in
generated function parameters.
- Updated string_of_ functions in ast_util to reflect syntax changes
- Fixed a C compilation issue where elements of union type
constructors were not being coerced between big integers and 64-bit
integers where appropriate
- Type annotations in patterns now generalise, rather than restrict
the type of the pattern. This should be safer and easier to handle
in the various backends. I don't think any code we had was relying
on this behaviour anyway.
- Add inequality operator to lib/flow.sail
- Fix an issue whereby top-level let bindings with annotations were
checked incorrectly
|
|
More work on Latex output
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
(used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
|
