| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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. | |||
| 2017-05-02 | doc | Peter Sewell | |
| 2017-04-24 | added register_value_for_reg | Shaked Flur | |
| 2017-04-18 | added transactional memory support | Shaked Flur | |
| 2017-04-03 | Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵ | Robert Norton | |
| it is only ever used for translating the PC. | |||
| 2017-03-29 | change reqiured to work with little endian interpreter. | Robert Norton | |
| 2017-03-25 | endianness fix | Shaked Flur | |
| 2017-03-24 | fixed endianness | Shaked Flur | |
| 2017-03-24 | Christopher, Peter: make "run_interp_model.ml" build again (endianness) | Peter Sewell | |
| 2017-03-24 | Print tracking information for V_track, hopefully fix extern_vector_value, ↵ | Christopher Pulte | |
| fix sail_values bug. | |||
| 2017-03-23 | the interpreter/shallow expects little-endian memory-values | Shaked Flur | |
| 2017-03-02 | tweak comments | Peter Sewell | |
| 2017-02-08 | put back the header into Sail_impl_base | Christopher Pulte | |
| 2017-02-08 | pull in Shaked's type class instance changes, fix Ord and Eq instances | Christopher Pulte | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |