summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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
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-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-08Glue together Sail prelude and Lem libraryThomas Bauereiss
2017-08-02Tune vector_subrangeThomas Bauereiss
2017-07-26Add right shift to lib/prelude.sail, and add case for E_exit in ↵Alasdair Armstrong
Ast_util.string_of_exp
2017-07-17Fixed multiply for MIPS in prelude so it correctly doubles bitvectorAlasdair Armstrong
length, and removed redundant calls to extension functions.
2017-07-14Correct signedness bugs in mips_new_tc.Brian Campbell
2017-07-13Modified MIPS model so it typechecks with the new typecheckerAlasdair Armstrong
2017-07-13Improved type inference for let statements and assignments with type ↵Alasdair Armstrong
annotated patterns and lexps Added get_enum to type checker interface
2017-07-12Various small changesAlasdair Armstrong
* Experimented with using list<bit> to clean up manually monomorphised code in MIPS tlb * Added option -dtc_verbose to control verbosity of new typechecker * Allowed functions with val specs to omit their type declarations
2017-07-12Fixed parser to parse 2** nexp expressions properlyAlasdair Armstrong
This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.
2017-07-12Added vector range l-expressions and additional testsAlasdair Armstrong
2017-07-06Testing new typechecker on MIPS specAlasdair Armstrong
Also: - Added support for foreach loops - Started work on type unions - Flow typing can now generate constraints, in addition to restricting range-typed variables - Various bugfixes - Better unification for nexps with multiplication
2017-07-05Fixed several unification bugsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 11:17:26 +0000