| Age | Commit message (Collapse) | Author |
|---|
|
|
|
(probably still some pattern matching to do, but I don't think the models
use that)
|
|
|
|
|
|
|
|
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.
|
|
cleanly
|
|
|
|
Prevents partial unfolding of Z.pow.
|
|
Fixes handling of Replicate(x, 0).
|
|
Added assertions to check that length of bit operations
is sensible (i.e., consistent with type system).
|
|
vector_update_subrange wasn't setting its return length correctly
|
|
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, ...)
|
|
|
|
|
|
targets using this.
|
|
Every Unix is subtly different.
|
|
|
|
|
|
|
|
The Arm spec uses the value 2.0^1000000 to represent infinity
so it is worth making real_power take logarithmic time.
|
|
graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation.
|
|
Implement square root function for rationals up to an arbitrary
precision, currently 30 decimal places. May need to increase this for
ARM tests.
|
|
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
|
|
|
|
Also fix the constraints in the standard prelude files,
add a couple of useful cast rewriting lemmas.
|
|
|
|
|
|
|
|
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.
|
|
|
