| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The initial implementation tries to optimize for simulator execution, especially for OS boots.
|
|
This is now split into instructions, regs, memory and platform, each
controlled individually. Currently all are enabled and not connected to
any command-line options, so a recompile is needed for trace tuning.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(except without the accidentally committed aarch64 files from the branch)
|
|
Essentially all we have to do to make this work is introduce a member of
the Value type, V_attempted_read <reg>, which is returned whenever we
try to read a register value with allow_registers disabled. This defers
the failure from reading the register to the point where the register
value is used (simply because nothing knows how to deal with
V_attempted_read). However, if V_attempted_read is returned directly as
the result of evaluating an expression, then we can replace the
expression with a single direct register read. This optimises some
indirection in the ARM specification.
|
|
Should hopefully fix memory leak in RISC-V.
Also adds an optimization pass that removes copying structs and allows
some structs to simply alias each other and avoid copying their
contents. This requires knowing certain things about the lifetimes of
the structs involved, as can't free the struct if another variable is
referencing it - therefore we conservatively only apply this
optimization for variables that are lifted outside function
definitions, and should therefore never get freed until the model
exits - however this may cause issues outside ARMv8, as there may be
cases where a struct can exist within a variant type (which are not
yet subject to this lifting optimisation), that would break these
assumptions - therefore this optimisation is only enabled with the
-Oexperimental flag.
|
|
This optimisation re-uses variables if possible, rather than
allocating new ones.
|
|
|
|
|
|
Bitvectors that aren't fixed size, but can still be shown to fit
within 64-bits, now have a specialised representation. Still need to
introduce more optimized functions, as right now we mostly have to
convert them into large bitvectors to pass them into most
functions. Nevertheless, this doubles the performance of the TLBLookup
function in ARMv8.
|
|
- Propagate types more accurately to improve optimization on ANF
representation.
- Add a generic optimization pass to remove redundant variables that
simply alias other variables.
- Modify Sail interactive mode, so it can compile a specification with
the :compile command, view generated intermediate representation via
the :ir <function> command, and step-through the IR with :exec <exp>
(although this is very incomplete)
- Introduce a third bitvector representation, between fast
fixed-precision bitvectors, and variable length large
bitvectors. The bitvector types are now from most efficient to least
* CT_fbits for fixed precision, 64-bit or less bitvectors
* CT_sbits for 64-bit or less, variable length bitvectors
* CT_lbits for arbitrary variable length bitvectors
- Support for generating C code using CT_sbits is currently
incomplete, it just exists in the intermediate representation right
now.
- Include ctyp in AV_C_fragment, so we don't have to recompute it
|
|
|
|
because >100 field records slow everything down
|
|
|
|
|
|
71020c2f460e6031776df17cf8f2f71df5bb9730 introduced assert error messages containing " revealing unescaped string literals in generated lem and prompting review of other backends.
|
|
|
|
|
|
Also fix some C optimisations
|
|
|
|
Also fix a test with an insufficient constraint
|
|
Fixes CHERI Lem build
|
|
This was _really_ slow - about 50secs for ARM. If this changes causes
breakages we should fix them in some other way.
Also using Reporting.err_unreachable in ANF translation, and fix slice
optimization when creating slices larger than 64-bits in C translation
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This brings Sail closer to MiniSail, and means that
type my_range 'n 'm = {'o, 'n <= 'o <= 'm. int('o)}
will work on the left hand side of a function type in the same way as
a regular built-in range type. This means that in principle neither
range nor int need be built-in types, as both can be implemented in
terms of int('n) (atom internally). It also means we can easily
identify type variables that need to be made into implict arguments,
with the criterion for that being simply any type variable that
doesn't appear in a base type on the LHS of the function, or only
appears on the RHS.
|
|
|
|
|
|
|
|
details (TODO make this optional).
|
|
|
|
|
|
|
|
|
|
usere more flexibility about formatting generated latex.
|
|
Also add a special case for shift-left when we are shifting 8 by a two
bit opcode, or 32 by a one bit opcode.
|
|
This fixes another case we often have to patch manually in translated ASL
code where a function returns a (result, Constraint)-pair.
Also (slightly) improve the error message for when we fail to infer a
l-expression, as we are going to hit this case more often now.
|
|
Previously the following would fail:
```
default Order dec
$include <prelude.sail>
register V : vector(1, dec, vector(32, dec, bit))
val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit)
function main() : unit -> unit = {
V[0] = zeros()
}
```
Since the type-checker wouldn't see that zeros() must have type
`vector(32, dec, bit)` from the type of `V[0]`. It now tries both to
infer the expression, and use that to check the assignment, and if
that fails we infer the lexp to check the assignment. This pattern
occurs a lot in ASL, and we often had to patch zeros() to zeros(32) or
similar there.
|
|
|
|
|
