| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Currently uses the -c2 option
Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.
For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.
The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.
Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.
|
|
|
|
8 bytes or less to avoid cost of using GMP integers (including free/malloc).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
C: Don't print usage message and quit when called with no arguments,
as this is used for testing C output
OCaml: Fix generation of datatypes with multiple type arguments
OCaml: Generate P_cons pattern correctly
C: Fix constant propagation to not propagate letbindings with type
annotations. This behaviour could cause type errors due to how type
variables are introduced. Now we only propagate letbindings when the
type of the propagated variable is guaranteed to be the same as the
inferred type of the binding.
Tests: Add OCaml tests to the C end-to-end tests (which really
shouldn't be in test/c/ any more, something like test/compile might be
better). Currently some issues with reals there like interpreter.
Tests: Rename list.sail -> list_test.sail because ocaml doesn't want
to compile files called list.ml.
|
|
|
|
This allows debug messages to include the current cycle count
which can be useful for debugging.
|
|
interpreter implementations of same.
|
|
Making the message more like archex messages simplifies tooling.
Plus, it is a better message.
|
|
|
|
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, ...)
|
|
|
|
|
|
|
|
graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation.
|
|
Use -DHAVE_SETCONFIG to enable __SetConfig support
|
|
|
|
This is now directly supported from SAIL so we can call the SAIL __SetConfig function
instead.
|
|
triggered by generated code (probably false positives). Fix some warnings in rts.c
|
|
Note that an alternative implementation choice is just to implement
them as SAIL functions manipulating a global variable.
Not sure which is better.
|
|
|
|
Also further tweaks to Sail library for C and include sail lib files for tracing
|
|
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.
|
|
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.
|
|
|
