summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-02add a cp2_next_pc function to update cheri state in fde loop and a stub ↵Robert Norton
version for mips.
2018-03-02add space in cap dump format to match that expected by test framework.Robert Norton
2018-03-02cheri tests expect reserved permission bits to be initialised to one.Robert Norton
2018-03-01Cleanup intermediate bytecode representation in C backendAlasdair Armstrong
2018-03-01Add support for read_tag and write_tag in sail_lib.ml. and support for ↵Robert Norton
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
2018-03-01fix typo in flow.sailRobert Norton
2018-03-01cheri wip.Robert Norton
2018-03-01Fix polymorphic functions annotations in OCaml compilationAlasdair Armstrong
One caveat still: Won't work if the polymorphic definition consists of multiple function clauses, but this seems unlikely - and I added an error message if this is the case. Also fix a small flow typing bug Fixes #7
2018-02-28Add check for if a function is redefining a val-specAlasdair Armstrong
Previously this did not result in an error, but would cause issues with generated code. Fixes #5
2018-02-28Use topological sorting for OCaml backendThomas Bauereiss
Fixes #6
2018-02-27Fix some bugs in C compilation, and optimise struct updatesAlasdair Armstrong
Fix some issues where some early returns in functions would cause memory leaks, and optimize struct updates so the struct is not copied uneccesarily. Also make C print_bits match ocaml version output, and update tests.
2018-02-27Get MIPS translated to LemThomas Bauereiss
2018-02-27Make constant propagation of slicing more generalBrian Campbell
2018-02-27Lem/OCaml compatibility fixesBrian Campbell
2018-02-26Add some obvious optimisations to C backend.Alasdair Armstrong
With these optimisations on, now get about 10x performance over OCaml.
2018-02-26Last of the aarch64_no_vector monomorphisation replacementsBrian Campbell
2018-02-26work around linksem crashing when trying to print an elf file where ↵Robert Norton
entry_point overflows an ocaml int.
2018-02-26working sail2 mips spec (passes BERI tests).Robert Norton
2018-02-26ADDU should sign extend 32-bit result.Robert Norton
2018-02-26workaround sail2 not liking type synonyms as arguments to constructors (see #2).Robert Norton
2018-02-26Fix SLTIU: note that immediate must be sign extended before unsigned comparison!Robert Norton
2018-02-26Fix missing case in pattern completeness checkAlasdair Armstrong
Fixes #4
2018-02-26Rename some Isabelle theoriesThomas Bauereiss
The suffix _lemmas is more descriptive than _extras.
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
Architecture-specific lemmas about concrete registers and types are generated and written to a file <prefix>_lemmas.thy, generic lemmas are in the theories *_extras.thy in lib/isabelle. In particular, State_extras contains simplification lemmas about the lifting from prompt to state monad.
2018-02-24Fix C builtinsAlasdair Armstrong
2018-02-23Change links in README to point to githubAlasdair Armstrong
Closes #3
2018-02-23Fix some bugs in C compilationAlasdair Armstrong
Fixed an issue with pattern matching on enums Fixed an issue whereby fix_early_returns would cause memory leaks Added optimizations for some of the builtins used in the decode function. Optimizations are turned on with the -O flag.
2018-02-23Make mono test harness nicerBrian Campbell
2018-02-23Allow guarded patterns rewrite to merge P_var patternsBrian Campbell
2018-02-23Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
2018-02-23Some tidy up of sail library - use extract_num from Big_int to implement ↵Robert Norton
to_get_slice_int in less confusing way. Add arithmetic shift right.
2018-02-23Change monomorphisation tests to proper outputBrian Campbell
2018-02-23test commitPeter Sewell
2018-02-23Update more monomorphisation testsBrian Campbell
2018-02-22More updates to C backendAlasdair Armstrong
Add support for short-ciruiting and/or. I forgot about this in the original ANF specification and not having it causes problems for the ARM spec.
2018-02-22Curtail at more false assertionsBrian Campbell
(plus some adjustments for the test case)
2018-02-22Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
2018-02-22wipRobert Norton
2018-02-22Start resurrecting monomorphisation testsBrian Campbell
2018-02-22Some Lem/OCaml compatibility fixesBrian Campbell
2018-02-22Point merlin at pprint buildBrian Campbell
2018-02-21Can now compile aarch64/no_vector into CAlasdair Armstrong
Now compiles to C and builds a working executable. Just need to correctly implement all the library builtins (some are still stubs), and it should work.
2018-02-21More aarch64 changes used in monomorphisationBrian Campbell
2018-02-21Add more bitvector sizes for aarch64Brian Campbell
2018-02-21Implement more builtins in constant propagationBrian Campbell
2018-02-21Cut out dead if branches according to the type environment during monoBrian Campbell
const progagation. Needed to avoid negative bitvector sizes on aarch64 Also propagate values found from "if var = const ...", which is needed in aarch64
2018-02-21Create an update_field function for each field in a bitfield definitionAlasdair Armstrong
2018-02-21Have aarch64/no_vector compiling to CAlasdair Armstrong
Just need to implement builtins, fix-up a few re-write passes, and integrate some kind of elf-loading and it should work.
2018-02-21clean LICENCEPeter Sewell
2018-02-20Remove temporary debugging messageBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:28:23 +0000