| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-29 | Linksem does not use uint anymore | Shaked Flur | |
| 2018-01-22 | Update Lem shallow embedding to Sail2 | Thomas Bauereiss | |
| - Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators. | |||
| 2017-12-19 | Support user-defined exceptions in Lem shallow embedding | Thomas Bauereiss | |
| The type-checker already supports a user-defined "exception" type that can be used in throw and try-catch expressions. This patch adds support for that to the Lem shallow embedding by adapting the existing exception mechanisms of the state and prompt monads. User-defined exceptions are distinguished from builtin exception cases. For example, the state monad uses type ex 'e = | Exit | Assert of string | Throw of 'e to distinguish between calls to "exit", failed assertions, and user-defined exceptions, respectively. Early return is also handled using the exception mechanism, by lifting to a monad with "either 'r exception" as the exception type, where 'r is the expected return type and "exception" is the user-defined exception type. | |||
| 2017-12-06 | Add top-level pattern match guards internally | Brian Campbell | |
| Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next. | |||
| 2017-12-06 | Merge remote branch 'experiments' into experiments | Thomas Bauereiss | |
| 2017-12-06 | Make AST after rewriting for Lem backend type-checkable | Thomas Bauereiss | |
| - Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now | |||
| 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. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |