| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-05 | Update license headers for Sail source | Alasdair Armstrong | |
| 2017-11-30 | Merge branch 'master' into experiments | Alasdair Armstrong | |
| 2017-11-29 | Better lem_ast tagging and interpreter tweaks | Alasdair Armstrong | |
| 2017-11-29 | Switched to bytecode compiler for executing interpreter to avoid stack overflow | Alasdair Armstrong | |
| 2017-11-17 | Fix Makefile for interpreter and update instruction_extractor | Alasdair Armstrong | |
| Instruction extractor code that I commented out in this commit seems buggy anyway - it will claim that the length of all bitvectors is 64?! | |||
| 2017-11-17 | Fix interpreter to work with new typechecker | Alasdair Armstrong | |
| Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard. | |||
| 2017-11-02 | remove a lot of dead code form run_with_elf_cheri* | Robert Norton | |
| 2017-11-02 | reset inCCallDelay in code that is not dead. | Robert Norton | |
| 2017-11-01 | added RISC-V "fence r,r" | Shaked Flur | |
| 2017-10-31 | cheri: throw an exception if there is an attempt to access C26/IDC in the ↵ | Robert Norton | |
| delay slot of a ccall selector 1 call. | |||
| 2017-10-25 | Alternative low-memory version of barrier_kindCompare | Brian Campbell | |
| 2017-10-24 | fix default cap value on cheri128 following previous changes -- E stored in ↵ | Robert Norton | |
| registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length. | |||
| 2017-10-09 | add translations for missing read/write kinds. | Robert Norton | |
| 2017-10-09 | add translation of IK_mem_rmw interp_inter_imp. TODO: could we get rid of ↵ | Robert Norton | |
| this and use shallow embedding conversion? | |||
| 2017-10-06 | move nias_of_instruction into RMEM so that it can use shallow embedding ast ↵ | Robert Norton | |
| and not obsolete interp_interface one. | |||
| 2017-09-29 | fix those build errors | Christopher Pulte | |
| 2017-09-29 | fix deep_shallow_convert, stop using interp_interface.instruction for most ↵ | Christopher Pulte | |
| things, SF and CP bugfixing | |||
| 2017-09-21 | added a comment to the x86 lock'd read and write | Shaked Flur | |
| 2017-09-20 | add support for x86 lock prefix (also remove unused Read/Write_tag kind in ↵ | Robert Norton | |
| etc/regfp.sail. | |||
| 2017-09-15 | x86: implement regfp analysis function (no control flow yet) | Robert Norton | |
| 2017-09-15 | reinstate deep/shallow conversion | Christopher Pulte | |
| 2017-09-03 | added RISC-V strong-acquire/release | Shaked Flur | |
| 2017-08-31 | add EnumerationType type class: if a type is a member you get Ord membership ↵ | Christopher Pulte | |
| and Set membership for free | |||
| 2017-08-31 | added RISC-V AMOs | Shaked Flur | |
| 2017-08-30 | typeclass instance Ord(opcode) | Christopher Pulte | |
| 2017-08-28 | Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵ | Brian Campbell | |
| mono-experiments # Conflicts: # src/gen_lib/sail_values.lem | |||
| 2017-08-24 | Begin refactoring Sail library | Thomas Bauereiss | |
| - Add back support for bit list representation of bit vectors, for backwards compatibility in order to ease integration with the interpreter. For this purpose, split out a file sail_operators.lem from sail_values.lem, and add a variant sail_operators_mwords.lem for the machine word representation of bitvectors. Currently, Sail is hardcoded to use machine words for the sequential state monad, and bit lists for the free monad, but this could be turned into a command line flag. - Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem library. The wrappers make use of sizeof expressions to extract type information from bitvectors (length, start index) in order to pass it to the Lem functions. - Add early return support to the free monad, using a new constructor "Return of 'r". As with the sequential monad, functions with early return are wrapped into "catch_early_return", which extracts the return value at the end of the function execution. | |||
| 2017-08-24 | typo | Shaked Flur | |
| 2017-08-24 | typo | Shaked Flur | |
| 2017-08-24 | added barrier-kind for x86 MFENCE; | Shaked Flur | |
| fixed some compare functions; | |||
| 2017-08-22 | added RISC-V "fence w,w" and "fence.i"; | Shaked Flur | |
| fixed the interpreter nias analysis; | |||
| 2017-08-19 | RISC-V store-release | Shaked Flur | |
| 2017-08-17 | added RISC-V load-acquire | Shaked Flur | |
| 2017-08-17 | fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w") | Shaked Flur | |
| 2017-08-16 | lem_interp: remove broken val_to_string_internal functions, replace with ↵ | Jon French | |
| string_of_value as used everywhere else | |||
| 2017-08-02 | fix sail library test interpreter glue for API change. Also fix ↵ | Robert Norton | |
| build_context val spec which was out of dated although lem did not complain for some reason... | |||
| 2017-08-02 | fix run_with_elf*.ml with changed lem_interp api | Jon French | |
| 2017-07-24 | interpreter: optionally print debugging traces | Jon French | |
| 2017-07-24 | vector parts of interpreter now evaluate all arguments of expression before ↵ | Jon French | |
| exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints | |||
| 2017-07-24 | move value type definitions to ott, and introduce new E_internal_value ast ↵ | Jon French | |
| node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node | |||
| 2017-07-06 | fix interpreter version of get_min/max_representable which similarly broken ↵ | Robert Norton | |
| to ocaml version. TODO: also fix copies in sail_values.lem and sail_values_word.lem. | |||
| 2017-07-06 | fix interpreter lteq/gteq for range/vec. | Robert Norton | |
| 2017-07-06 | fix interpreter version of != which was broken for vector/range comparisons. | Robert Norton | |
| 2017-06-22 | fix three different copies of the hardware_quot function to do proper ↵ | Robert Norton | |
| trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0. | |||
| 2017-06-22 | add a 'print' built-in function handy for writing sail tests. | Robert Norton | |
| 2017-05-28 | fixed exmem | Shaked Flur | |
| 2017-05-26 | fix run_with builds after build_context gained an extra argument. | Robert Norton | |
| 2017-05-24 | Merge branch 'master' of bitbucket.org:Peter_Sewell/sail | Shaked Flur | |
| # Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml | |||
| 2017-05-24 | added the exmem effect for AArch64 store-exclusive | Shaked Flur | |
| 2017-05-24 | Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵ | Robert Norton | |
| data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |