summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-07-20add new CNEXEQ instruction.Robert Norton
2017-07-19split library tests into separate files to avoid risk of sail compiler stack ↵Robert Norton
overflow.
2017-07-19borrow some of aa's bash code to convert library test suite output to junit ↵Robert Norton
xml for jenkins.
2017-07-06Tests for (almost) all sail builtins. Many interesting things discovered. ↵Robert Norton
Library in need of rationalisation.
2017-07-06fix off by one in type of add_vec builtin function. There are many more ↵Robert Norton
dubious types but will wait for library rationalisation to fix.
2017-07-06fix 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-06fix interpreter lteq/gteq for range/vec.Robert Norton
2017-07-06fix interpreter version of != which was broken for vector/range comparisons.Robert Norton
2017-07-06substitute 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-06implement abs function correctly for ocaml shallow embedding.Robert Norton
2017-07-06fix dodgy get_min/max_representable functions. Looks like an attempt at ↵Robert Norton
optimisation went wrong.
2017-07-04further testing of sail library.Robert Norton
2017-07-04change to cgettype -- returns -1 if not sealed instead of 0.Robert Norton
2017-07-03Update to copytype and ccseal -- now use belt and braces approach when ↵Robert Norton
handling unsealed capabilities by clearing tag and setting cursor to -1. Also CCSeal got an encoding.
2017-06-30add 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-29beginnings of a sail library test suite.Robert Norton
2017-06-22fix 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-22add a 'print' built-in function handy for writing sail tests.Robert Norton
2017-06-22fix a typo spotted in CPtrCmp instruction -- CLEU was using signed ↵Robert Norton
comparison instead of unsigned.
2017-06-22revised ccopytype with check for offset being in bounds and clearing tag ↵Robert Norton
instead of using magic value if unsealed. Also corresponding CCSeal instruction which degrades to a cmove if ct.tag is unset.
2017-06-16prefer arithmetic on integers followed by cast to bit[64] in CCopyType.Robert Norton
2017-06-16remove unnecessary local variable definitions copy and pasted from cbuildcap.Robert Norton
2017-06-16fix previous commit so that it builds.Robert Norton
2017-06-16implement new CBuildCap and CCopyType instrucitons for ISAv6.Robert Norton
2017-06-14Add a work-in-progress version of sail_values.lemBrian Campbell
that uses the new Lem machine words library.
2017-06-13Add Makefile and ROOT for Isabelle libraryThomas Bauereiss
2017-06-05Attempt to make Lem-prettyprinting of function clauses more robustThomas 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-05Fix pretty-printing of function clauses with wildcards for LemThomas 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-02Add tag memory to Lem shallow embeddingThomas Bauereiss
2017-05-28fixed exmemShaked Flur
2017-05-26fix run_with builds after build_context gained an extra argument.Robert Norton
2017-05-26add cmovz and cmovn conditional capability move instructions new in ISAv6.Robert Norton
2017-05-26Update 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-26in ISAv6 cjr and cjalr are permitted on local capabilities.Robert Norton
2017-05-26add support for the new ccall selector 1 implementation that directly ↵Robert Norton
unseals capabilities.
2017-05-24fixed missing _tag bitsShaked Flur
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked 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-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change 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-24it 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-10Fix type error in CGetLenThomas 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-10Further to Thomas's commit remove the duplicate declarations of max_otype ↵Robert Norton
and have_cp2.
2017-05-10Add stubs for TAGwThomas Bauereiss
Tagged memory seems to be currently missing in the Lem shallow embedding of (CHERI-)MIPS.
2017-05-10Comment out duplicate definitions in cheri_types.sailThomas Bauereiss
They are already defined in cheri_prelude_common.sail
2017-05-10Build Cheri_embed_types.thy together with Cheri_embed_sequential.thyThomas Bauereiss
2017-05-08add make rules to (attempt to) build arm and power ml.Robert Norton
2017-05-08add target for building ocaml shallow embed for arm.Robert Norton
2017-05-08add some missing things in sail_values and make big_int version the default ↵Robert Norton
for set_vector_subrange_bit.
2017-05-08add error messages for unhandled pattern match nodes in ocaml pretty printer.Robert Norton
2017-05-08put failwith in brackets to avoid parse error.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:08:17 +0000