summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-16add support for CIncOffsetImmediate and CSetBoundsImmediate.Robert Norton
2017-10-16add support for capability branch null instructions.Robert Norton
2017-10-13Handle bitvector_access in constant propagationBrian Campbell
2017-10-13Make Sail_values.repeat total, and remove duplicateBrian Campbell
2017-10-13Fix some bugs that surfaced in the ASL exportThomas Bauereiss
2017-10-13Add rewriting step for tuple-vector assignmentsThomas Bauereiss
2017-10-13Add rewriting step for function effect propagationThomas Bauereiss
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
2017-10-13Improve debugging outputThomas Bauereiss
2017-10-13Repeat and while loops in menhir parser and pretty printerAlasdair Armstrong
2017-10-13Add support for new cheri instruction encodings. The order of pattern matchin...Robert Norton
2017-10-12Fixes pattern matching exact values ([:'n:]) on integer literalsAlasdair Armstrong
2017-10-12Work around warning in ocaml shallow embedding of mips caused by buggy code g...Robert Norton
2017-10-10More improvements to menhir parserAlasdair Armstrong
2017-10-10Fixes to menhir parser and pretty printerAlasdair Armstrong
2017-10-09Improvements to menhir pretty printer and ocaml backendAlasdair Armstrong
2017-10-09add translations for missing read/write kinds.Robert Norton
2017-10-09add translation of IK_mem_rmw interp_inter_imp. TODO: could we get rid of thi...Robert Norton
2017-10-09X86: Fix bug in register footprint caused by imperative variable update with ...Robert Norton
2017-10-06Remove BK_effect constructorAlasdair Armstrong
2017-10-06Various improvements to menhir parser, and performance improvments for Z3 callsAlasdair Armstrong
2017-10-06move nias_of_instruction into RMEM so that it can use shallow embedding ast a...Robert Norton
2017-10-06Produce type signatures in Lem outputBrian Campbell
2017-10-06Implement replicate_bits for mwordsBrian Campbell
2017-10-06Fix constant propagation on multi-argument functionsBrian Campbell
2017-10-04Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-10-04Fixed a bug in vector concatenation l-expressionsAlasdair Armstrong
2017-10-04Alasdair, Peter: towards new Sail ottPeter Sewell
2017-10-04Add pretty printer for menhir parserAlasdair Armstrong
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-10-04Add pretty printing for while loopsAlasdair Armstrong
2017-10-04Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-10-03Fixes to new parserAlasdair Armstrong
2017-10-03Fixed some loop bugs for ASL parserAlasdair Armstrong
2017-10-02cheri: fix swapped cmovz and cmovn.Robert Norton
2017-10-02Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-02Make undefined constant propagation stop at ex_intBrian Campbell
2017-10-01fixed JALR: do the register write first to allow po-later readsShaked Flur
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29fix those build errorsChristopher Pulte
2017-09-29Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sailChristopher Pulte
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most th...Christopher Pulte
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
2017-09-29Move Isabelle libraryThomas Bauereiss
2017-09-29Add MIPS->Isabelle target to MakefileThomas Bauereiss
2017-09-29x86: add bit set, reset, complement operations.Robert Norton
2017-09-28Use (K)Bindings from ast_util rather than making new onesBrian Campbell
2017-09-28Add loops to monomorphisationBrian Campbell