summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-14Update mono testsBrian Campbell
2018-03-14Machine words extract/update operations arguments are the other way aroundBrian Campbell
2018-03-14Remove unnecessary size_itself_int uses in guards (for Lem)Brian Campbell
2018-03-14Fix compilation for OCaml 4.02Thomas Bauereiss
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add rewriting step for moving execute clauses into auxiliary functionsThomas Bauereiss
2018-03-14Disallow impure global let bindingsThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
2018-03-14fix riscv build: missing eq_bit implementation.Robert Norton
2018-03-14riscv: disable failing lrsc test for now to make sail2 green.Robert Norton
2018-03-14minor cleanup of load -- we no longer need to separate out by access size bec...Robert Norton
2018-03-14add extract of ccseal instruction.Robert Norton
2018-03-14Add extract of some new instructions for including into CHERI documentation.Robert Norton
2018-03-13Polymorphic option types now compile to CAlasdair Armstrong
2018-03-13Add test for mutual recursion and monomorphisationBrian Campbell
2018-03-13Support a few more set constraints in monoBrian Campbell
2018-03-13Merge funcls for Lem output, making it suitable for testing with OCamlBrian Campbell
2018-03-13A couple of mono test tweaksBrian Campbell
2018-03-12ELF loading for C backendAlasdair Armstrong
2018-03-12lem_interp: expose disable color flag in Printing_functions interfaceJon French
2018-03-09Specialise constructors for polymorphic unionsAlasdair Armstrong
2018-03-09Sort mono test cases, add missing filesBrian Campbell
2018-03-08rename mips_new_tc to mipsRobert Norton
2018-03-08Remove files in mips directory prior to copying in files from mips_new_tc. Ho...Robert Norton
2018-03-08make HighestSetBit return option now that it can type check.Robert Norton
2018-03-07Fix cheri and mips following 1fe8f33fce5aaaaea82fc54b6d198ffc9d7e1eeb which r...Robert Norton
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-03-06Add missing checks for permit_load and permit_store in capability load/store ...Robert Norton
2018-03-06Check tag of pcc in TranslatePC. This could happen after an ERET with untagge...Robert Norton
2018-03-06overload shift operators so they can be used with integer shifts in cheri128 ...Robert Norton
2018-03-06finish port of cheri128 spec. to sail2.Robert Norton
2018-03-06add atom versions of val declaration for min and max.Robert Norton
2018-03-05Fix specialisation pass to handle polymorphic substitutionsAlasdair Armstrong
2018-03-05Add Print outcome to prompt monad for debugging and tracingThomas Bauereiss
2018-03-05Add support for undefined bit oracle to Lem shallow embeddingThomas Bauereiss
2018-03-02Use sail_lib.lem values in C backendAlasdair Armstrong
2018-03-02Fix a bug in rewriting of loops for Lem backendThomas Bauereiss
2018-03-02Add full aarch64_no_vector monomorphisation demoBrian Campbell
2018-03-02remove workaround for #8 now that it is fixed.Robert Norton
2018-03-02Fix off-by-one error in OCaml for loop compilationAlasdair Armstrong
2018-03-02work around bug in ocaml foreach generation -- end point not included in loop...Robert Norton
2018-03-02add a cp2_next_pc function to update cheri state in fde loop and a stub versi...Robert Norton
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 intial...Robert Norton
2018-03-01fix typo in flow.sailRobert Norton
2018-03-01cheri wip.Robert Norton