summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-06Tests for (almost) all sail builtins. Many interesting things discovered. ↵Robert Norton
Library in need of rationalisation.
2017-07-06fix off by one in type of add_vec builtin function. There are many more ↵Robert Norton
dubious types but will wait for library rationalisation to fix.
2017-07-06fix interpreter version of get_min/max_representable which similarly broken ↵Robert Norton
to ocaml version. TODO: also fix copies in sail_values.lem and sail_values_word.lem.
2017-07-06fix interpreter lteq/gteq for range/vec.Robert Norton
2017-07-06fix interpreter version of != which was broken for vector/range comparisons.Robert Norton
2017-07-06substitute all uses of mod_big_int and div_big_int for Z.rem and Z.div which ↵Robert Norton
have correct rounding behaviour. Missed these when changing quot and mod functions.
2017-07-06implement abs function correctly for ocaml shallow embedding.Robert Norton
2017-07-06fix dodgy get_min/max_representable functions. Looks like an attempt at ↵Robert Norton
optimisation went wrong.
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-04further testing of sail library.Robert Norton
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-30add more tests for sail library. Can't compile entire file due to sail ↵Robert Norton
performance bug or infinite loop. Add some missing shallow embedding funcitons.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-16 01:37:02 +0000