| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-01 | Remove some hardcoded calls to obsolete Lem library functions | Thomas Bauereiss | |
| 2017-07-26 | Merge remote-tracking branch 'origin/master' into sail_new_tc | Alasdair Armstrong | |
| 2017-07-06 | substitute all uses of mod_big_int and div_big_int for Z.rem and Z.div which ↵ | Robert Norton | |
| have correct rounding behaviour. Missed these when changing quot and mod functions. | |||
| 2017-07-06 | implement abs function correctly for ocaml shallow embedding. | Robert Norton | |
| 2017-07-06 | fix dodgy get_min/max_representable functions. Looks like an attempt at ↵ | Robert Norton | |
| optimisation went wrong. | |||
| 2017-06-30 | add more tests for sail library. Can't compile entire file due to sail ↵ | Robert Norton | |
| performance bug or infinite loop. Add some missing shallow embedding funcitons. | |||
| 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-06-21 | Merge | Thomas Bauereiss | |
| 2017-06-21 | Pretty-print bitvector expressions | Thomas Bauereiss | |
| - Add case distinctions between bitvector types and vectors of other element types (e.g. registers) and use the corresponding operations (i.e. "bvslice", "bvaccess", etc for the former, and "slice", "access", etc for the latter) when pretty-printing expressions - Add type annotations to expressions when the type includes bitvectors with concretely known length - Update state.lem to use bitvectors (in the interface, at least; internally, bitvectors are still stored as bit lists for now, since that makes it easier to support storing different registers with different lengths) This has been tested with the CHERI-MIPS model with some success, but some things are still missing: - Bitvector patterns are not handled yet - Some bitvector length monomorphisation is needed in a few places of the model - Some type annotations are missing, because the (old) Sail type checker does not infer bitvector lengths in some instances where one would hope it to do that; this should be checked with the new type checker | |||
| 2017-06-19 | Fix Show on Lem bitvector | Brian Campbell | |
| 2017-06-16 | Some Isabelle fixes for word version of sail_values | Brian Campbell | |
| 2017-06-15 | Replace sail_values.lem with Brian's machine word version | Thomas Bauereiss | |
| 2017-06-14 | Add a work-in-progress version of sail_values.lem | Brian Campbell | |
| that uses the new Lem machine words library. | |||
| 2017-06-02 | Add tag memory to Lem shallow embedding | Thomas Bauereiss | |
| 2017-05-24 | fixed missing _tag bits | Shaked Flur | |
| 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 | it turns out that Zarith has a divide function which does truncation towards ↵ | Robert Norton | |
| zero but it is not exposed via Bit_int_Z. Use it instead of rolling our own. Also ocaml / and mod already do the right thing. | |||
| 2017-05-08 | add some missing things in sail_values and make big_int version the default ↵ | Robert Norton | |
| for set_vector_subrange_bit. | |||
| 2017-04-27 | add command line argument for setting undef values to all zero or all one. ↵ | Robert Norton | |
| Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work. | |||
| 2017-04-25 | optimise to_vec_int because it is used by MEMr to convert each byte to vector. | Robert Norton | |
| 2017-04-25 | replace memory representation with map of 1MB pages rather than map of ↵ | Robert Norton | |
| bytes. This makes loading binaries much quicker but doesn't seem to make a big difference to execution speed. | |||
| 2017-04-25 | remove unused function. | Robert Norton | |
| 2017-04-21 | define some big_int literals in sail_values.ml to avoid lots of calls to ↵ | Robert Norton | |
| bit_int_of_int. Likely very little performance benefit but slightly more readable. | |||
| 2017-04-21 | implement to_vec_big using zarith extract for some speedup. | Robert Norton | |
| 2017-04-21 | suppress register field tracing if not enabled (missed in previous commit) | Robert Norton | |
| 2017-04-20 | more library optimisation. Implement int_of_bit_array using shift, avoiding ↵ | Robert Norton | |
| need to use power. | |||
| 2017-04-20 | implement vector subrange using Array.sub for approx 10% speedup. | Robert Norton | |
| 2017-04-20 | attempt to optimise performance if not tracing writes. | Robert Norton | |
| 2017-04-20 | add missing min and max functions, overriding built-in ocaml ones. Also ↵ | Robert Norton | |
| neq_range. | |||
| 2017-04-20 | add name to register representation and print it on write. | Robert Norton | |
| 2017-04-18 | fix definition of mask -- Vregister and VvectorR were swapped. | Robert Norton | |
| 2017-04-18 | Implement return using an exception caught in the function body. Polymorphic ↵ | Robert Norton | |
| exceptions are not permitted so a local mutable variable, ret, is used in ocaml to store the return value. This avoids having to define a new exception type for each function. Ocaml infers the type of the option when it is assigned at the return site. | |||
| 2017-04-07 | fix error in generated ocaml where writing single bit of register was not ↵ | Robert Norton | |
| taking account of register direction. | |||
| 2017-04-07 | implement quot and mod with truncation towards zero which is not the ocaml ↵ | Robert Norton | |
| way but standard for C and most hw. | |||
| 2017-04-07 | simplify xor using ocaml <> operator which also has the advantage of being ↵ | Robert Norton | |
| more correct | |||
| 2017-04-06 | minor changes in sail_values.ml to aid debugging | Robert Norton | |
| 2017-04-06 | fix incorrect use of == in eq | Robert Norton | |
| 2017-04-06 | implement exts and extz as manipulations on bit vectors rather than ↵ | Robert Norton | |
| converting to integers, allowing them to work on vectors containing undef. | |||
| 2017-04-06 | Implement exit by raising Sail_exit exception | Robert Norton | |
| 2017-03-30 | Make length function return big_int | Robert Norton | |
| 2017-03-28 | temporary fix for problem duplicate (lack of direction) -- assume decreasing ↵ | Robert Norton | |
| for mips compatibility. | |||
| 2017-03-28 | Fix erroneous bitwise xor. | Robert Norton | |
| 2017-03-27 | fix bitshift operators. I think these should be independent of vector order... | Robert Norton | |
| 2017-03-27 | Fix broken to_vec of negative values. Old code was a bit confused. Probably ↵ | Robert Norton | |
| possible to rewrite using arithmetic on big_int which might be faster. | |||
| 2017-03-24 | Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵ | Robert Norton | |
| embedding. | |||
| 2017-03-24 | changes to ocaml pp to allow mips->ocaml to compile | Robert Norton | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |