summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-07-13Monomorphisation size limitsBrian Campbell
2017-07-13Monomorphisation now splits vectorsBrian Campbell
2017-07-13Make new-tc monomorphisation actually workBrian Campbell
2017-07-13Couple of fixes for old-tc monomorphisationBrian Campbell
2017-07-13Add basic translation of monomorphisation to the new type checkerBrian Campbell
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-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-12Remove old interface fileBrian Campbell
2017-07-12Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
sail_new_tc
2017-07-12Removed inital_check_full_astAlasdair 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-12Add annotations to raw bitvector slicesThomas Bauereiss
2017-07-12MergeThomas Bauereiss
2017-07-12Add checks for variable identifiers in pattern subsumptionThomas Bauereiss
2017-07-12Added vector range l-expressions and additional testsAlasdair Armstrong
2017-07-11Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
sail_new_tc
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-11Fix missing vector append constraints in old type checkerBrian Campbell
2017-07-10Bugfixes and testing new checker on the MIPS specAlasdair Armstrong
2017-07-10Added tests for union constructor matchingAlasdair Armstrong
2017-07-10Merge remote-tracking branch 'origin/word' into sail_new_tcAlasdair Armstrong
2017-07-10Adder pattern matching for union typesAlasdair Armstrong
2017-07-10Further performance improvements to typecheckerAlasdair Armstrong
Added code to solve basic constraints without passing them to Z3. This results in roughly another 5x speedup.
2017-07-10Performance improvements to type checkerAlasdair Armstrong
Filter the possible casts by only attempting those which reasonably match the surrounding type environment. This results in about a 5x performance improvement.
2017-07-10Reduce functions during constant propagation under reasonable circumstancesBrian Campbell
2017-07-10Support some variable patterns in monomorphisationBrian Campbell
2017-07-07Warn when we can't monomorphise a constructor applicationBrian Campbell
2017-07-07Correct variable mapping when splitting constructor patterns for ↵Brian Campbell
monomorphisation
2017-07-07Implement basic monomorphisation of constructorsBrian Campbell
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
2017-07-05Added split_on_char as a utility function in Util.ml, and replaced usage in ↵Alasdair Armstrong
sail.ml Current REMS install script and Jenkins CI server is on an older ocaml which doesn't have this function in String.
2017-07-05Merge remote-tracking branch 'origin/word' into sail_new_tcAlasdair Armstrong
2017-07-05Re-factored and cleaned up type-checkerAlasdair Armstrong
2017-07-04Added effect system to new type checkerAlasdair Armstrong
2017-07-04Added documentation to type_check_new.mliAlasdair Armstrong
2017-07-03Cleanup, and add support for variable bindings in bitvector patternsThomas Bauereiss
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-30Split bit patterns for monomorphisation, do equality checksBrian Campbell
(e.g., for some ARM decoding functions)
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-29Rewrite bitvector patternsThomas Bauereiss
Seems to work for CHERI-MIPS, but still a few things to be done, e.g. collecting let bindings for variables bound in bitvector patterns
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-29Propagate type information from reducing case expressionsBrian Campbell
2017-06-29Ocamlbuild targets should always be remadeBrian Campbell
2017-06-29Added support for set constraintsAlasdair Armstrong
Also added some additional tests in test/typecheck
2017-06-29Various improvements to typecheckerAlasdair Armstrong
Added vector concatenation patterns. Currently slightly more restrictive than before as each subvector's length must be inferrable from just that particular subvector - this may require additional type annotations in certain vector patterns. How exactly weird vector patterns, such as incrementing and decrementing vectors appearing in the same pattern, as well as patterns with funny start indexes should be dealt with correctly is unclear. It's probably best to be as restrictive as possible to avoid unsoundness bugs. Added a new option -ddump_tc_ast which dumps the (new) typechecked AST to stdout. Also added a new option -dno_cast which disables implicit casting in the typechecker. These options can be used in conjunction to dump the typechecked ast (which has all implicit casts resolved), and then re-typecheck it as a way to check that the typechecker is indeed resolving all casts correctly, and is reconstructing a fully type correct AST. The run_tests.sh script in test/typecheck has been modified to do this. Removed the dependency on Type_internal.ml from pretty_print_sail.ml. This means that we can no longer pretty print certain internal constructs produced by the old typechecker, but on the plus side it means that the sail pretty printer is type system agnostic and works with any annotation AST, irregardless of the type of annotations. Also fixed a few bugs where certain constructs would be pretty printed incorrectly.
2017-06-28User defined overloaded operatorsAlasdair Armstrong
New typechecker has no builtin overloaded operators - instead can now write something in SAIL like: overload (deinfix +) [id1; id2; id3] to set up functions id1, id2, and id3 as overloadings for the + operator. Any identifier can be overloaded, not just infix ones. This is done in a backwards compatible way, so the old typechecker removes the DEF_overload nodes from the ast so the various backends never see it.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 11:23:10 +0000