summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2018-01-30Fix failing Lem testsAlasdair Armstrong
2018-01-29Sync mono rewrites definitions with libraryBrian Campbell
2018-01-29Shaked removing generation of now-uncessary uint dependencyPeter Sewell
2018-01-26Fixed loading ARM elf filesAlasdair Armstrong
Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib
2018-01-26One more mono rewriteBrian Campbell
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.
2018-01-22Update and fix test suiteAlasdair Armstrong
2018-01-19Update monomorphisation for sail2Brian Campbell
(no vector type start position, comment syntax)
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-18Modified ocaml backend to use ocamlfind for linksem and lemAlasdair Armstrong
Fixed test cases for ocaml backend and interpreter
2018-01-16Another useful monomorphisation rewriteBrian Campbell
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-09More monomorphisation rewrites for aarch64Brian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2017-12-14An experimental version of sail without bitvector start indexes.Alasdair Armstrong
Works with the vector branch of asl_parser
2017-12-14Merge remote-tracking branch 'origin/experiments' into interactiveAlasdair Armstrong
2017-12-13Cleanup code by fixing compiler warnings, and fix ocaml compilationAlasdair Armstrong
Add the ast.sed script we need to build sail. Currently we just need this to fix up the locations in the AST but it will be removed once we can share locations between ocaml and lem.
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-07Support monomorphisation with set constrained integersBrian Campbell
Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude
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-28Small update to trivial sizeof rewrites so we can handle all cases inAlasdair Armstrong
aarch64 vector instructions. There's maybe a better more general way to do this but I'm not sure what that would be.
2017-11-27Compile assertions into OCamlAlasdair Armstrong
and_bool and or_bool now are treated specially in the ocaml backend, so that they have the correct short-circuiting behaviour. This is required so that assertions don't fail for the ARM spec for predicates that shouldn't be tested in certain circumstances, for example things like: IsAArch32() && AArch32_specific_predicate Also fixed an issue in the sail library for ocaml where greater than or equal to was being mapped to greater than.
2017-11-21Expose entry point in elf_loader for Sail modelAlasdair Armstrong
2017-11-15Additional test case for OCaml backendAlasdair Armstrong
2017-11-15Simplify flow typing code in typecheckerAlasdair Armstrong
2017-11-10Fixed ocaml backend so it correctly compiles registers passed by name.Alasdair Armstrong
Added a test case for this behavior
2017-11-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
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-03Fix ocaml test suiteAlasdair Armstrong
2017-10-31Improvements to register read tracing in ocaml backendAlasdair Armstrong
2017-10-27Fixed some ocaml backend related bugsAlasdair Armstrong
2017-10-26Fix a bug in Sail OCaml libraryAlasdair Armstrong
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
Cleaned up the option list in sail.ml
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Avoid name clash in generated LemBrian Campbell
(complains due to added val spec)
2017-10-23Added support for better tracing in ocaml backendAlasdair Armstrong
Fixed an issue in ast.ml with uneccessary type variables
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-18Mark more prelude functions externBrian 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-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-29Move Isabelle libraryThomas Bauereiss
2017-09-26Added while-do and repeat-until loops to sail for translating ASLAlasdair Armstrong
2017-09-18Added additional utility functions in ast_utilAlasdair Armstrong
Also fixed basic ocaml test suite
2017-09-14Fix some more test casesThomas Bauereiss
2017-09-07Add ocaml run-time and updates to sail for ocaml backendAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 22:07:44 +0000