summaryrefslogtreecommitdiff
path: root/src/gen_lib
AgeCommit message (Collapse)Author
2017-09-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments
2017-09-02Remove dependency of state.lem on bitvector operationsThomas Bauereiss
2017-08-29Make Lem export of CHERI(-256) typecheckThomas Bauereiss
Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS).
2017-08-28Eta expand lem for OCaml generationBrian Campbell
2017-08-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-28Correct indexing and equality for bitvectorsBrian Campbell
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments # Conflicts: # src/gen_lib/sail_values.lem
2017-08-24Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-24Begin refactoring Sail libraryThomas 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-23Update monomorphisation test scriptBrian Campbell
2017-08-21Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-18Correct indexing and equality for bitvectorsBrian Campbell
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
Make state monad parametric in register state, and generate a record with registers from the Sail spec
2017-08-17Merge remote-tracking branch 'origin' into mono-experimentsBrian Campbell
# Conflicts: # src/type_internal.ml
2017-08-16Eta-expansion in sail_values to make OCaml happyBrian Campbell
2017-08-15Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-14Merge remote-tracking branch 'origin/master' into experimentsAlasdair Armstrong
2017-08-12Resolve ambiguity between negation of integers and boolsThomas Bauereiss
2017-08-10Add support for early return to Lem backendThomas Bauereiss
Implemented using the exception monad, by throwing and catching the return value
2017-08-08Glue together Sail prelude and Lem libraryThomas Bauereiss
2017-08-01Remove some hardcoded calls to obsolete Lem library functionsThomas Bauereiss
2017-07-26Merge remote-tracking branch 'origin/master' into sail_new_tcAlasdair Armstrong
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-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-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-21MergeThomas Bauereiss
2017-06-21Pretty-print bitvector expressionsThomas 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-19Fix Show on Lem bitvectorBrian Campbell
2017-06-16Some Isabelle fixes for word version of sail_valuesBrian Campbell
2017-06-15Replace sail_values.lem with Brian's machine word versionThomas Bauereiss
2017-06-14Add a work-in-progress version of sail_values.lemBrian Campbell
that uses the new Lem machine words library.
2017-06-02Add tag memory to Lem shallow embeddingThomas Bauereiss
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-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-08add some missing things in sail_values and make big_int version the default ↵Robert Norton
for set_vector_subrange_bit.
2017-04-27add 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-25optimise to_vec_int because it is used by MEMr to convert each byte to vector.Robert Norton
2017-04-25replace 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-25remove unused function.Robert Norton
2017-04-21define 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-21implement to_vec_big using zarith extract for some speedup.Robert Norton
2017-04-21suppress register field tracing if not enabled (missed in previous commit)Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:42:23 +0000