summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2018-02-20Bump up case split limit for nowBrian Campbell
2018-02-20Simplifying nexp division, since the type checker can introduce itBrian Campbell
(otherwise you end up with div(64,8) in output sizes!)
2018-02-20Report unsupported nexps properly in Lem backendBrian Campbell
2018-02-20Rework atom-to-itself transformation to check for equivalent size nexpsBrian Campbell
2018-02-20Look for alternative size annotations when pretty printing LemBrian Campbell
(so that we get enough type annotations for bitvectors)
2018-02-20Allow overlapping bitfield field namesAlasdair Armstrong
Allows bitfields to share field names by generating accessors as _get/set_name_field where name is the type name and field is the field name rather than _get/set_field. They are still accessed and set using just register.field() and register.field() = value. Fixes #1
2018-02-19Have generic vectors working in C backendAlasdair Armstrong
2018-02-17Merge branch sail2Thomas Bauereiss
2018-02-17Merge master branch into sail2 for OCaml 4.06 compatibilityThomas Bauereiss
2018-02-17Add a note detailing hopefully up-to-date install processAlasdair Armstrong
2018-02-16Avoid nested explicit type annotationsThomas Bauereiss
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
2018-02-16Don't generate undefined functions for generated register typesThomas Bauereiss
2018-02-16Add __TakeColdReset function to aarch64_no_vectorAlasdair Armstrong
Turns out the __TakeColdReset function is actually in the v8.3 XML. I went and looked for it, and it's there, it just wasn't being picked up by ASL parser because it's not called from any instructions. I added a new field to the json config files for ASL parser that can tell it about any such special functions that it should guarantee to include. Also fixed a bug in C loop compilation
2018-02-16Add alternative definitions of aarch64 functions for monomorphisationBrian Campbell
2018-02-16Can now compile aarch64/duopod to CAlasdair Armstrong
Goes through the C compiler without any errors, but as we still don't have all the requisite builtins it won't actually produce an executable. There are still a few things that don't work properly, such as vectors of non-bit types - but once those are fixed and the Sail library is implemented fully it should work.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:27:14 +0000