summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-06-21Remove loading kernel from mips mainAlasdair Armstrong
2018-06-21Merge branch 'sail2' of github.com:rems-project/sail into sail2Alasdair Armstrong
2018-06-21add PMP registers to CSR, fix buildJon French
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
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.
2018-06-21changes to riscv model to support rmemJon French
2018-06-20Coq: Generate MR when appropriate; syntax fixesBrian Campbell
2018-06-20Coq: reverse_endiannessBrian Campbell
2018-06-20Coq: add missing existential projection on simple let expressionsBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: print div/mod/abs in nexps; avoid mod as an identifierBrian Campbell
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-20Coq: a few more opsBrian Campbell
2018-06-19Minor optimization in ocaml_backend to use ints instead of strings for ↵Prashanth Mundkur
Big_int literals. Improves tests/riscv duration by around 2% and size of riscv.o by 15%.
2018-06-19Add more detail to riscv execution trace log.Prashanth Mundkur
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
2018-06-19Add elf parsing from AlastairAlasdair Armstrong
2018-06-19Improvements to Sail C for booting LinuxAlasdair Armstrong
2018-06-18Mono test script updateBrian Campbell
(still need to sort out some string stuff, though)
2018-06-18Add bitvector length constraints to mips inequalitiesBrian Campbell
to match new constraints in prelude
2018-06-18Coq: better handling of identifiers, esp infix onesBrian Campbell
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
(necessary for backends where they're different) Coq uint/sint and related fixes
2018-06-18Coq: fix up some comparison operations in preludeBrian Campbell
2018-06-18Coq: update prompt monad wrt LemBrian Campbell
2018-06-15Fix riscv system register initialization.Prashanth Mundkur
2018-06-15Fixes for C RTS for aarch64 no it's split into multiple filesAlasdair Armstrong
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.
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-14provide impl of int_of_string_opt in Sail_lib to support older Ocaml versionsJon French
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
(The last bit is to declare type aliases as Type so that Coq uses the type scope for notation, so * is prod, not multiplication).
2018-06-12Coq: Handle simple top-level type variable definitionsBrian Campbell
(also another error reporting improvement)
2018-06-12Coq: upgrade some errors to report locationsBrian Campbell
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
Plus - Complete solver support for inequalities - Reduce exponentials in solver
2018-06-12Coq: add more to libraryBrian Campbell
2018-06-12Prove test_raw_add theorem for init_stateRamana Kumar
It can be proved almost entirely by symbolic execution (in <15s) _if_ the right definitions are in the compset. It took a lot of interactive stumbling about to discover that LUPDATE was missing from the standard list compset.
2018-06-12Make progress on HOL4 test_raw_addRamana Kumar
The proof now gets through simulation of the first instruction of the test.
2018-06-12Work on HOL symbolic evaluation of installing codeRamana Kumar
2018-06-12Experimentation with PrePost for test_raw_addRamana Kumar
2018-06-12Speculation on executing a CHERI test in HOL4Ramana Kumar
2018-06-11Use riscv platform insns_per_tick to tick the clock.Prashanth Mundkur
2018-06-11Put the riscv model's output on stderr, leaving stdout for the platform ↵Prashanth Mundkur
terminal.
2018-06-11Update retire semantics for riscv WFI.Prashanth Mundkur
2018-06-11add 'pat as id' mapping-patternsJon French
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-11Merge branch 'mappings' into sail2Jon French
2018-06-11actually fix exist_pattern testJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 03:24:42 +0000