summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-11Merge branch 'mappings' into sail2Jon French
2018-06-11actually fix exist_pattern testJon French
2018-06-11fix test exist_pattern.sail -- lem needed much more of the stdlib to be importedJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-11Add string.sail file to libAlasdair Armstrong
2018-06-11Merge branch 'sail2' into mappingsJon French
(involved some manual tinkering with gitignore, type_check, riscv)
2018-06-11change double-caret for string-append-pattern to single caret, since that ↵Jon French
wouldn't be legal in a pattern anyway
2018-06-11ocaml test prelude: option is now in stdlibJon French
2018-06-11drop now-unnecessary type annotation clutter from riscv decode mappingsJon French
2018-06-11better type inference of union-constructors and mappingsJon French
2018-06-09Increment minstret on instruction retires, and handle the case when the ↵Prashanth Mundkur
minstret CSR is explicitly written to.
2018-06-09Some fixes to counteren handling.Prashanth Mundkur
2018-06-09Fix issue in C_backend, and run C tests with undefined behavior sanitizerAlasdair
2018-06-09Fix issue with catch block return values not being compiled correctlyAlasdair
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
2018-06-08Fix mmio address matching for clint device.Prashanth Mundkur
2018-06-08Add counteren registers.Prashanth Mundkur
2018-06-08Slightly condense execution trace log.Prashanth Mundkur
2018-06-08Update initialization of misa.Prashanth Mundkur
2018-06-08Make the simulation loop use the platform interface to detect exits via htif.Prashanth Mundkur
2018-06-08Add mem and mmio access tracing.Prashanth Mundkur
2018-06-08Fix use of non-tail-recursive calls in elf_loader.Prashanth Mundkur
2018-06-08type checking mappings: allow inferring based on the other side's id inferencesJon French
2018-06-08Coq: some handling of existential types as function return typesBrian Campbell
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
Plus test case, broken builtin name
2018-06-08Coq: track add_typquant changeBrian Campbell
2018-06-08Correct dependencies of bytecode sailBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
- add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving
2018-06-08Coq: some very basic existential supportBrian Campbell
Only single variable in places, only packed at literals and variables, no unpacking
2018-06-08Coq: fix axiom generationBrian Campbell
2018-06-08Coq: ignore some currently unsupported testsBrian Campbell
2018-06-08Coq: update foreach handling, correct field accessesBrian Campbell
2018-06-08Fill in most Coq built-insBrian Campbell
2018-06-08Coq: skip two tests with redundant pattern matchesBrian Campbell
2018-06-08Coq: correct failure on unsupported undefined valuesBrian Campbell
2018-06-08Coq: use record update syntax (only single fields work for now)Brian Campbell
2018-06-08Coq: correct implicitness of type arguments in unionsBrian Campbell
2018-06-08Add missing Coq builtin info to vector_incBrian Campbell
2018-06-08add sail as dependency of mips targets.Robert Norton
2018-06-07Slight refactor to keep platform handling localized to the _platform file.Prashanth Mundkur
2018-06-07Fix width guards on htif accesses.Prashanth Mundkur
2018-06-07Update physical memory and address translation for MMIO.Prashanth Mundkur
- Assume for now that atomic accesses are only to memory regions, to leave their effects unchanged. - The top-level mem_read and mem_write functions for physical memory now have rreg and wreg effects due to MMIO (due to reads/writes to device registers). It would be nice to have a separate construct for non-CPU-register state to avoid polluting the footprint. - Assume for now that page-table walks access physical memory regions only, and not MMIO regions. Leave a fixme note there to address this later, perhaps when PMP/PMA is added.
2018-06-07More definitions for the physical memory map.Prashanth Mundkur
2018-06-07Remove unused file.Prashanth Mundkur
2018-06-07Add terminal output to riscv platform, with incomplete handling of input.Prashanth Mundkur
2018-06-07Fix bug in add_bits optimizationAlasdair Armstrong
2018-06-07Refactor mips main a little to work around apparent bug in c generation. ↵Robert Norton
Generated c Works with no gcc optimisation but fails when optimisation is on, implying undefined behaviour. Probably due to control reaching end of non-void function in exception case.
2018-06-07Use the vector_dec standard library for mips. This means we get all the c ↵Robert Norton
functions ready to go.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:52:06 +0000