summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
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
2017-07-04Added documentation to type_check_new.mliAlasdair Armstrong
2017-07-03Fixed bug in XML output for jekinsAlasdair Armstrong
2017-07-03Added test suite XML output for jenkinsAlasdair Armstrong
2017-07-03Added tests for lem shallow embeddingAlasdair Armstrong
Now the test suite generates lem for all the typechecker tests, and tests if the generated lem typechecks. For a lot of the cases the answer is currently no.
2017-07-03Added records to checkerAlasdair Armstrong
Added the following constructs to the new type checker: * Added records, and record field accessors * Added assert statements * Added nondet blocks * More simple flow typing tests
2017-06-30Added flow types to new typecheckerAlasdair Armstrong
Added preliminary support for flow types, so we can typecheck things like: default Order inc val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range overload (deinfix +) [add_range] overload (deinfix -) [sub_range] overload (deinfix <) [lt_atom_range; lt_range_atom] function ([|63|]) branch (([|63|]) x) = { y := x; if (y < 32) then { y := 31; y + 32 } else y - 32 } Currently how this works is that the if condition is lifted to a typ modifying function that applies to the type of the variables appearing in the condition provided it satisfies some ad-hoc conditions. As can be seen above, it does require that the initial environment for the typechecker is set up with the correct definitions
2017-06-29Added a large test case to the test-suiteAlasdair Armstrong
Commented out some buggy re-sugaring logic from pretty_print_common where it re-sugared vectors incorrectly Fixed a bug where the type checker forgot to preserve type signatures in top-level letbinds
2017-06-29Created prelude.sail for initial typing environmentAlasdair Armstrong
Other things: * Cleaned up several files a bit * Fixed a bug in the parser where (deinfix |) got parsed as (definfix ||) * Turned of the irritating auto-indent in sail-mode.el
2017-06-29Added support for set constraintsAlasdair Armstrong
Also added some additional tests in test/typecheck
2017-06-29Additional tests for overloading and vector patternsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 22:34:20 +0000