| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Cleanup some debugging output
|
|
|
|
We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional
sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist
at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator
changes.
|
|
lifted types
Add a test case for nested variant constructors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
types
|
|
|
|
Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
|
|
|
|
|
|
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
|
|
Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing
variants. Also make sure that struct equality works for structs containing other structs.
|
|
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any
builtin type in sail.h.
|
|
|
|
Non bitvector literals for decreasing vectors were not being reversed
correctly, so the list of capability registers was effectively in
reverse order.
Added a test case to test/c/ based on this aspect of CHERI
|
|
to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed.
|
|
We should test before the first iteration in case 'to' starts out as
less than 'from'.
|
|
The code to do this is rather ugly. It would be nice to have a generic
callgraph representation we could just query and not use the rewriter
in a weird way to extract this info.
|
|
|
|
|
|
|
|
This is now directly supported from SAIL so we can call the SAIL __SetConfig function
instead.
|
|
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
|
|
Also further tweaks to Sail library for C and include sail lib files for tracing
|
|
Refactor the C compilation process by moving out the conversion to
A-normal form into its own file. Also make the A-normal form AST
parameterised by the type of the types annotating it. The idea being we
can have a typ aexp -> ctyp aexp translation, converting to low-level
types at a slightly higher level before mapping into our low-level IR.
This would fix some issues we have where the type of variables change
due to flow typing, because we could map the sail types to low-level
types in the ANF ast where we still have some knowledge about the
structure of the original Sail.
|
|
For example, the MIPS model can boot FreeBSD as
./mips_c --binary=0x100000,/path/to/kernel --image=/path/to/simboot.sailbin
Or with short options as
./mips_c -b 0x100000,/path/to/kernel -i /path/to/simboot.sailbin
The current options are:
-e, --elf, which loads an elf file directly
-n, --entry, which sets the entry point
-i, --image, which loads an image file compiled by "sail -elf" using Linksem
-b, --binary, which loads a plain binary image into memory at a specific address
-l, --cyclelimit, which means the (new) cycle_count() builtin exits the model after a certain number of calls
Also there are the default -? --help and --usage options.
|
|
|
|
This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.
|
|
Previously the ANF->IR translation cared too much about how things
were allocated in C, so it had to constantly check whether things
needed to be allocated on the stack or heap, and generate different
cequences of IR instructions depending on either. This change removes
the ialloc IR instruction, and changes iinit and idecl so that the
code generator now generates different C for the same IR instructions
based on the variable types involved.
The next change in this vein would be to merge icopy and iconvert at
the IR level so that conversions between uint64_t and large-bitvectors
are inserted by the code generator. This would be good because it
would make the ANF->IR translation more robust to changes in the types
of variables caused by flow-typing, and optimization passes could
convert large bitvectors to uint64_t as local changes.
|
|
|
|
|
|
Fix a bug involving indentifers on the left hand side of assignment
statements not being shadowed correctly within foreach loops.
Make the different between different types of integer division
explicit in at least the C compilation for now. fdiv_int is division
rounding towards -infinity (floor). while tdiv_int is truncating
towards zero. Same for fmod_int and tmod_int.
|
|
|
|
|
|
|
|
|
|
|
|
This should fix the issue raised in commit 45554f
Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations
|
|
|
|
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.
|
