| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-03 | Cleanup, and add support for variable bindings in bitvector patterns | Thomas Bauereiss | |
| 2017-06-30 | Split bit patterns for monomorphisation, do equality checks | Brian Campbell | |
| (e.g., for some ARM decoding functions) | |||
| 2017-06-29 | Rewrite bitvector patterns | Thomas Bauereiss | |
| Seems to work for CHERI-MIPS, but still a few things to be done, e.g. collecting let bindings for variables bound in bitvector patterns | |||
| 2017-06-29 | Propagate type information from reducing case expressions | Brian Campbell | |
| 2017-06-29 | Ocamlbuild targets should always be remade | Brian Campbell | |
| 2017-06-28 | Reduce simple enumeration cases during monomorphisation | Brian Campbell | |
| 2017-06-28 | Use more plausible type for E_case | Brian Campbell | |
| (Previously it used the last branch's type!) | |||
| 2017-06-23 | Get rid of bogus singleton pattern warnings | Brian Campbell | |
| 2017-06-23 | Add option for monomorphisation splitting | Brian Campbell | |
| 2017-06-23 | Basic constant propagation for partial monomorphisation | Brian Campbell | |
| 2017-06-22 | Initial partial monomorphisation work | Brian Campbell | |
| Splits specified pattern matches on enumerations (other types to be added later); no constant propogation yet. | |||
| 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 | Pretty-print bitvector types | Thomas Bauereiss | |
| Next up: Expressions, patterns | |||
| 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-05 | Attempt to make Lem-prettyprinting of function clauses more robust | Thomas Bauereiss | |
| Instead of abusing patterns as expressions, bind patterns to names (if they are more complex than an identifier or literal and don't have a name already) and generate expressions referring to those names (which we then pass as arguments to the auxiliary functions). | |||
| 2017-06-05 | Fix pretty-printing of function clauses with wildcards for Lem | Thomas Bauereiss | |
| Before, wildcards sometimes ended up in the arguments to the function call on the RHS, in particular when using vector patterns (which implicitly introduce wildcards for the order and index parameters). | |||
| 2017-06-02 | Add tag memory to Lem shallow embedding | Thomas Bauereiss | |
| 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 | 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 | 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-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-10 | Build Cheri_embed_types.thy together with Cheri_embed_sequential.thy | Thomas Bauereiss | |
| 2017-05-08 | add make rules to (attempt to) build arm and power ml. | Robert Norton | |
| 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-05-08 | add error messages for unhandled pattern match nodes in ocaml pretty printer. | Robert Norton | |
| 2017-05-08 | put failwith in brackets to avoid parse error. | Robert Norton | |
| 2017-05-02 | doc | Peter Sewell | |
| 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-25 | Add support for uart terminal. Also add read_bit_reg function for faster and ↵ | Robert Norton | |
| neater access to registers of single bit. | |||
| 2017-04-24 | added register_value_for_reg | Shaked Flur | |
| 2017-04-21 | it turns out zarith has a function for printing big_ints in hex. Remove the ↵ | Robert Norton | |
| dependency on ocaml uint library by using it. | |||
| 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 | Revert change to check in type_check.ml. | Alasdair Armstrong | |
| 2017-04-21 | Fixes stack overflow in sail caused by list append in type_internal.ml. | Alasdair Armstrong | |
| Also makes the check function in type_check tail recursive. | |||
| 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-21 | add make variable for setting ocaml compilation options (e.g. set to -p to ↵ | Robert Norton | |
| enable gprof profiling) | |||
| 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 | remove unnecessary lemlib include in compile. | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |