summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2017-09-14Fix some more test casesThomas Bauereiss
2017-09-13Work on improving Sail error messagesAlasdair Armstrong
- Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases
2017-09-07Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-09-07Add ocaml run-time and updates to sail for ocaml backendAlasdair Armstrong
2017-09-02Add command line flags to toggle sequential monad and native machine wordsThomas Bauereiss
2017-09-01Testing typedef generation for ocamlAlasdair Armstrong
2017-09-01More test cases for ocaml backendAlasdair Armstrong
2017-09-01Started work on test suite 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-22Added basic support for pure record definitions and functional recordAlasdair Armstrong
updates to the new typechecker
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-17Fix two more test casesThomas Bauereiss
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-15Added exceptions and try/catch blocks to AST and typechecker in orderAlasdair Armstrong
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
2017-08-10Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
Conflicts: src/pretty_print_common.ml
2017-08-10Fix bug with subtyping in let bindingsAlasdair Armstrong
2017-08-10Improved existentials and type synonymsAlasdair Armstrong
2017-08-08Fix Lem bindings in test casesThomas Bauereiss
Add a test case with the MIPS spec using the TLB stub. Use the sequential monad for Lem testing for now; the free monad (in "prompt.lem") has not been updated for machine words yet.
2017-08-07Fixed various issues regarding typechecking lists.Alasdair Armstrong
2017-08-02Test for overloaded function with varying aritiesAlasdair Armstrong
2017-08-02Fix run_tests.sh so it cleans up generated ml files when testing ocaml backendAlasdair Armstrong
2017-08-02Tune vector_subrangeThomas Bauereiss
2017-08-02Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
2017-08-01Added ocaml generation to run_tests.shAlasdair Armstrong
2017-08-01Fixed a bug where type_synonyms were not being expanded properly when ↵Alasdair Armstrong
considering possible casts
2017-08-01Fixed a bug where as patterns weren't binding their variable correctlyAlasdair Armstrong
2017-08-01Added additional test for existentialsAlasdair Armstrong
2017-07-31Changed behavior of return to better match ASLAlasdair Armstrong
2017-07-28Mips TLB existential exampleAlasdair Armstrong
2017-07-28Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
2017-07-27Some more test casesAlasdair Armstrong
2017-07-27Add test cases for overlapping record field namesAlasdair Armstrong
2017-07-27Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
2017-07-27Fixed bug with pattern synonyms in Cons and List patternsAlasdair Armstrong
2017-07-27Fixed some bugs with existentials, and added test casesAlasdair Armstrong
2017-07-26Improve rewriting of sizeof expressionsThomas Bauereiss
If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly
2017-07-25Improved l-expressionsAlasdair Armstrong
- Fixed a bug where some l-expressions which wrote registers wern't picking up register writes. - Can now write to registers with record types. e.g. ARM's ProcState record from ASL.
2017-07-24Added cons patterns to sailAlasdair Armstrong
See test/typecheck/pass/cons_pattern.sail for an example. Also cleaned up the propagating effects code by making some of the variable names less verbose
2017-07-18Added real number literals to sail, to better support full ASL translationAlasdair Armstrong
2017-07-17Added pattern guards to sailAlasdair Armstrong
Introduces a when keyword for case statements, as the Pat_when constructor for pexp's in the AST. This allows us to write things like: typedef T = const union { int C1; int C2 } function int test ((int) x, (T) y) = switch y { case (C1(z)) when z == 0 -> 0 case (C1(z)) when z != 0 -> x quot z case (C2(z)) -> z } this should make translation from ASL's patterns much more straightforward
2017-07-13Typechecker now inserts val specs into AST when it infers themAlasdair Armstrong
2017-07-13Modified MIPS model so it typechecks with the new typecheckerAlasdair Armstrong
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-11Various typechecker improvements:Alasdair Armstrong
* Fixed a bug where non-polymorphic function return types could be incorrect * Added support for LEXP_memory AST node * Flow typing constraint generation for all inequality operators * Better support for increasing vector indices in field access expressions
2017-07-10Bugfixes and testing new checker on the MIPS specAlasdair Armstrong
2017-07-10Added tests for union constructor matchingAlasdair 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-04Added effect system to new type checkerAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 09:19:33 +0000