| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-09 | Increment minstret on instruction retires, and handle the case when the ↵ | Prashanth Mundkur | |
| minstret CSR is explicitly written to. | |||
| 2018-06-09 | Some fixes to counteren handling. | Prashanth Mundkur | |
| 2018-06-09 | Fix issue in C_backend, and run C tests with undefined behavior sanitizer | Alasdair | |
| 2018-06-09 | Fix issue with catch block return values not being compiled correctly | Alasdair | |
| 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-08 | Fix mmio address matching for clint device. | Prashanth Mundkur | |
| 2018-06-08 | Add counteren registers. | Prashanth Mundkur | |
| 2018-06-08 | Slightly condense execution trace log. | Prashanth Mundkur | |
| 2018-06-08 | Update initialization of misa. | Prashanth Mundkur | |
| 2018-06-08 | Make the simulation loop use the platform interface to detect exits via htif. | Prashanth Mundkur | |
| 2018-06-08 | Add mem and mmio access tracing. | Prashanth Mundkur | |
| 2018-06-08 | Fix use of non-tail-recursive calls in elf_loader. | Prashanth Mundkur | |
| 2018-06-08 | Coq: some handling of existential types as function return types | Brian Campbell | |
| 2018-06-08 | Coq: add destructuring of atom existentials in patterns | Brian Campbell | |
| Plus test case, broken builtin name | |||
| 2018-06-08 | Coq: track add_typquant change | Brian Campbell | |
| 2018-06-08 | Correct dependencies of bytecode sail | Brian Campbell | |
| 2018-06-08 | Coq: existential and constraint solving work | Brian 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-08 | Coq: some very basic existential support | Brian Campbell | |
| Only single variable in places, only packed at literals and variables, no unpacking | |||
| 2018-06-08 | Coq: fix axiom generation | Brian Campbell | |
| 2018-06-08 | Coq: ignore some currently unsupported tests | Brian Campbell | |
| 2018-06-08 | Coq: update foreach handling, correct field accesses | Brian Campbell | |
| 2018-06-08 | Fill in most Coq built-ins | Brian Campbell | |
| 2018-06-08 | Coq: skip two tests with redundant pattern matches | Brian Campbell | |
| 2018-06-08 | Coq: correct failure on unsupported undefined values | Brian Campbell | |
| 2018-06-08 | Coq: use record update syntax (only single fields work for now) | Brian Campbell | |
| 2018-06-08 | Coq: correct implicitness of type arguments in unions | Brian Campbell | |
| 2018-06-08 | Add missing Coq builtin info to vector_inc | Brian Campbell | |
| 2018-06-08 | add sail as dependency of mips targets. | Robert Norton | |
| 2018-06-07 | Slight refactor to keep platform handling localized to the _platform file. | Prashanth Mundkur | |
| 2018-06-07 | Fix width guards on htif accesses. | Prashanth Mundkur | |
| 2018-06-07 | Update 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-07 | More definitions for the physical memory map. | Prashanth Mundkur | |
| 2018-06-07 | Remove unused file. | Prashanth Mundkur | |
| 2018-06-07 | Add terminal output to riscv platform, with incomplete handling of input. | Prashanth Mundkur | |
| 2018-06-07 | Fix bug in add_bits optimization | Alasdair Armstrong | |
| 2018-06-07 | Refactor 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-07 | Use the vector_dec standard library for mips. This means we get all the c ↵ | Robert Norton | |
| functions ready to go. | |||
| 2018-06-07 | add mips_c target. | Robert Norton | |
| 2018-06-07 | Rename some functions in vector_dec library file to avoid clashes with ↵ | Robert Norton | |
| functions in mips spec in prepartion for using this file in mips prelude. Also modify tests that use this header. We should consider prefixing library builtins to avoid name clashes. overload can then be used to provide aliases if desired. | |||
| 2018-06-07 | Fixes and additions to c builtins needed to pass mips test suite. bv_ts ↵ | Robert Norton | |
| should be kept in normal form i.e. a positive mpz_t with no bits higher than len set. | |||
| 2018-06-07 | Fix a small bug in monomorphisation | Thomas Bauereiss | |
| 2018-06-07 | Fix Lem build of RISC-V | Thomas Bauereiss | |
| 2018-06-07 | Merge pull request #14 from lastland/sail2 | Alasdair Armstrong | |
| Fix a typo. | |||
| 2018-06-06 | Fix a typo. | Yao Li | |
| 2018-06-07 | Add a constant folding optimization pass | Alasdair | |
| 2018-06-06 | Factor utility functions for IR into separate file and struct update ↵ | Alasdair Armstrong | |
| 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). | |||
| 2018-06-06 | Some additional fixes to C backend. Re-enable primitive optimizations. | Alasdair Armstrong | |
| 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. | |||
| 2018-06-06 | Some work on improving error messages | Alasdair Armstrong | |
| We now store the location where type variables were bound, so we can use this information when printing error messages. Factor type errors out into type_error.ml. This means that Type_check.check is now Type_error.check, as it previously it handled wrapping the type_errors into reporting_basic errors. Type_check.check' has therefore been renamed to Type_check.check. | |||
| 2018-06-04 | Add the htif exit command, a top-level function to initialize the riscv ↵ | Prashanth Mundkur | |
| platform, and document the artificial wreg effect due to using registers for device state. | |||
| 2018-06-04 | Uncomment the clint implementation in riscv_platform. | Prashanth Mundkur | |
| 2018-06-04 | Update sail C library | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |