| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-26 | fix run_with builds after build_context gained an extra argument. | Robert Norton | |
| 2017-05-26 | add cmovz and cmovn conditional capability move instructions new in ISAv6. | Robert Norton | |
| 2017-05-26 | Update ctoptr instruction to check that all of ct is within bounds of cb and ↵ | Robert Norton | |
| that cb is not sealed as per ISAv6. | |||
| 2017-05-26 | in ISAv6 cjr and cjalr are permitted on local capabilities. | Robert Norton | |
| 2017-05-26 | add support for the new ccall selector 1 implementation that directly ↵ | Robert Norton | |
| unseals capabilities. | |||
| 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 | Fix type error in CGetLen | Thomas Bauereiss | |
| For some reason, Lem did not like the call to "min" when exporting to Isabelle. Replacing "min" with an if-then-else expression solves this. This is also in line with the CHERI spec, which actually uses an if block. | |||
| 2017-05-10 | Further to Thomas's commit remove the duplicate declarations of max_otype ↵ | Robert Norton | |
| and have_cp2. | |||
| 2017-05-10 | Add stubs for TAGw | Thomas Bauereiss | |
| Tagged memory seems to be currently missing in the Lem shallow embedding of (CHERI-)MIPS. | |||
| 2017-05-10 | Comment out duplicate definitions in cheri_types.sail | Thomas Bauereiss | |
| They are already defined in cheri_prelude_common.sail | |||
| 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 target for building ocaml shallow embed for arm. | 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 | avoid out of bounds indicies in cheri128 decompression functions. | Robert Norton | |
| 2017-04-27 | also trace memory writes. | Robert Norton | |
| 2017-04-27 | remove undefined value from cheri 128 spec. The ocaml shallow embedding ↵ | Robert Norton | |
| cannot handle undef structs and the value should not be used (could be option type but wanted a similar interface to incCapOffset and setCapOffset). | |||
| 2017-04-27 | fix incorrect vector index in cheri128 spec. Should ideally have been caught ↵ | Robert Norton | |
| by type checker... | |||
| 2017-04-27 | fix cheri128 model referring to wrong registers and not capreg printing. | Robert Norton | |
| 2017-04-27 | need brackets around try ... with expression. | Robert Norton | |
| 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-27 | reverse endianness of data when writing UART. Altera jtag uart is ↵ | Robert Norton | |
| little-endian and this change allows it to work when writing using store word (as done by FreeBSD driver) or sb (as done by cheri helloworld program). | |||
| 2017-04-25 | extend the try around call to select to avoid gprof crashing with EINTR. | Robert Norton | |
| 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 | Don't die if stdin gets closed (e.g. when running unit tests). | Robert Norton | |
| 2017-04-25 | support loading more than one raw file as anonymous arguments so that we can ↵ | Robert Norton | |
| load simboot + kernel. | |||
| 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 | remove unnecessary cast in incrementCP0Count (run every instruction) for ↵ | Robert Norton | |
| potential speedup. | |||
| 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 | |
| 2017-04-20 | work around ocaml shallow embedding problem with matching on big_ints by ↵ | Robert Norton | |
| restructuing switch as if | |||
| 2017-04-20 | add support for cheri128 ocaml shallow embedding | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |