| Age | Commit message (Collapse) | Author |
|---|
|
|
|
boot time by reducing TLB misses but an apparent reduction in IPS counteracts this. Makes use of foreach and return to implement tlbSearch.
|
|
|
|
|
|
to sequential simulation. This is needed for booting FreeBSD where a minimal bootloader (simboot.elf) runs before jumping into the kernel loaded in memory.
|
|
|
|
|
|
|
|
|
|
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
|
Add type refinement to arm spec
|
|
|
|
checker
|
|
|
|
Interp: trying to add some debugging to isolate bug
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
requires some clean up (currently one huge function).
|
|
|
|
decode/translate_address/exhaustive. (Was previously correct for full register reads)
|
|
Attempt to get correct behaviour wrt nextpC on instruction fetch exception (prob. still wrong).
|
|
|
|
fix bug in interp_to_value_helper
|
|
(although decode isn't pushed through yet).
Note: this will break all builds
|
|
then reconvert delayedPC
|
|
|
|
|
|
implementation for now and exceptions not properly handled.
|
|
|
|
|
|
This is not yet connected to any model and not yet tested.
Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ).
|
|
undefined unless we actually access memory which is uninitialised.
|
|
assignment expression
|
|
|
|
version. Temporary 'solution' to building mips and cheri builds until proper factorising can take place.
|
|
|
|
|
|
interp_lib, interp_inter_imp, and printing_functions.
|
|
|
|
|
|
|
|
|
