| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | |
| 2017-02-03 | fix headers | Peter Sewell | |
| 2017-01-27 | fix right shift | Kathy Gray | |
| 2017-01-26 | c128: xor E with 48 when storing in memory so that null cap is all zeros but ↵ | Robert Norton | |
| has non-zero E (latest spec.) | |||
| 2017-01-26 | christopher, kathy, peter: hacky experiment on nias_of_instruction | Peter Sewell | |
| 2017-01-25 | Make interpreter a little more flexible on the format of a register type to ↵ | Kathy Gray | |
| match ASL; add missing functions/cases to library | |||
| 2017-01-25 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail | Kathy Gray | |
| 2017-01-25 | Make vector equality remember about the possibility of unknown values | Kathy Gray | |
| 2017-01-24 | functionality for comparing handwritten analysis function with exhaustive ↵ | Christopher Pulte | |
| interpreter | |||
| 2017-01-24 | Remember to pass through collapse argument in else case in bit_lifteds_to_string | Robert Norton | |
| 2017-01-23 | remove taint printing | Kathy Gray | |
| 2017-01-23 | Extend lib with min and max | Kathy Gray | |
| 2017-01-14 | changes to enable interpreter exhaustive analysis in ppcmem again | Christopher Pulte | |
| 2016-12-09 | sail changes for making lem embedding Isabelle-friendlier | Christopher Pulte | |
| 2016-12-02 | fix interpreter build following refactoring | Robert Norton | |
| 2016-12-01 | move interpreter-specific types from Sail_impl_base to Interp_interface | Christopher Pulte | |
| 2016-11-30 | add new barrier kind for MIPS (only one for now). | Robert Norton | |
| 2016-11-27 | make outcome_s contain the instruction state pretty print rather than the ↵ | Christopher Pulte | |
| instruction state, factor out interpreter/shallow embedding value conversion | |||
| 2016-11-23 | Add new type checking file. Small changes to type inference, temporary ↵ | Kathy Gray | |
| change to printing | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |