summaryrefslogtreecommitdiff
path: root/src/gen_lib
AgeCommit message (Collapse)Author
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
- Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
Also, rename a few functions for uniformity, e.g. bool_and -> and_bool
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-11-01added RISC-V "fence r,r"Shaked Flur
2017-11-01Support bitvector-size-parametric functions in Lem outputBrian Campbell
Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
Map to calls to monadic function assert_exp that throws an exception if the assertion is false
2017-10-25Avoid name clash in generated LemBrian Campbell
(complains due to added val spec)
2017-10-24fix default cap value on cheri128 following previous changes -- E stored in ↵Robert Norton
registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length.
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
(and fix up monomorphisation)
2017-10-13Make Sail_values.repeat total, and remove duplicateBrian Campbell
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
Moreover, add support for pretty-printing (to Lem) vector access/update operations for vectors with non-constant, but normalized start index.
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
Requires version of Lem with real number support, currently at https://bitbucket.org/bauereiss/lem/branch/reals
2017-10-06Implement replicate_bits for mwordsBrian Campbell
2017-10-02Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most ↵Christopher Pulte
things, SF and CP bugfixing
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
- Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors.
2017-09-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-26fixesChristopher Pulte
2017-09-21wibShaked Flur
2017-09-19fixChristopher Pulte
2017-09-15reinstate deep/shallow conversionChristopher Pulte
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments
2017-09-03added RISC-V strong-acquire/releaseShaked Flur
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-22and fix that other placesChristopher Pulte
2017-08-22adapt state.lem to RISCV additionsChristopher Pulte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 17:04:52 +0000