| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-24 | Begin refactoring Sail library | Thomas 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-24 | Avoid re-typechecking after rewriting passes | Thomas Bauereiss | |
| Rewriting of sizeofs and constraints seems to lose or hide some information that the typechecker needs | |||
| 2017-08-24 | Add some missing type annotations | Thomas Bauereiss | |
| 2017-08-23 | Started work on an undefined literal removal pass for the ocaml | Alasdair Armstrong | |
| backed. Ocaml doesn't support undefined values, so we need a way to remove them from the specification in order to generate good ocaml code. There are more subtle issues to - like if we initialize a mutable variable with an undefined list, then the ocaml runtime has no way of telling what it's length should be (as this information is removed by the simple_types pass). We therefore rewrite undefined literals with calls to functions that create undefined types, e.g. (bool) undefined becomes undefined_bool () (vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ()) We therefore have to generate undefined_X functions for any user defined datatype X. initial_check seems to be the logical place for this. This is straightforward provided the user defined types are not-recursive (and it shouldn't be too bad even if they are). | |||
| 2017-08-22 | Type quantification elimination working for hexapod spec | Alasdair Armstrong | |
| 2017-08-22 | Added debugging output for E_record and E_record_update in ast_util | Alasdair Armstrong | |
| 2017-08-22 | Added basic support for pure record definitions and functional record | Alasdair Armstrong | |
| updates to the new typechecker | |||
| 2017-08-22 | More work on quantifier elimination | Alasdair Armstrong | |
| 2017-08-21 | More work on quantifier elimination pass | Alasdair Armstrong | |
| Also added a rewriting pass that removes the cast annotations and operator overloading declarations from the AST because they arn't supported by the interpreter. | |||
| 2017-08-21 | Modified sizeof rewriting pass so it can correctly deal with existentials. | Alasdair Armstrong | |
| Basically we needed to make the rewriting step for E_sizeof and E_constraint more aggressively try to rewrite those expressions from variables in scope, without adding new parameters to pass the type variables at runtime, as this can break in the presence of existential quantification. Still some cleanup to do in this code, but tests on the arm spec show that it now introduces the minimal amount of new parameters. | |||
| 2017-08-18 | Fixed a bug where sizeof re-writing fail for aliased type arguments | Alasdair Armstrong | |
| Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments | |||
| 2017-08-17 | Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal pass | Alasdair Armstrong | |
| 2017-08-17 | Add E_constraint support to re-writer | Alasdair Armstrong | |
| 2017-08-17 | Add support for register types other than bitvector to state monad | Thomas Bauereiss | |
| Make state monad parametric in register state, and generate a record with registers from the Sail spec | |||
| 2017-08-17 | Various sail fixes for ASL hexapod | Alasdair Armstrong | |
| 2017-08-16 | Added the feature to bind type variables in patterns. | Alasdair Armstrong | |
| The reason you want this is to do something like (note new parser only): ********* default Order dec type bits 'n:Int = vector('n - 1, 'n, dec, bit) val zeros : forall 'n. atom('n) -> bits('n) val decode : bool -> unit function decode b = { let 'datasize: {|32, 64|} = if b then 32 else 64; let imm: bits('datasize) = zeros(datasize); () } ********* for the ASL decode functions, where the typechecker now knows that the datasize variable and the length of imm are the same. | |||
| 2017-08-15 | Merge remote-tracking branch 'origin/mono-experiments' into experiments | Alasdair Armstrong | |
| 2017-08-15 | Removed Typ_arg_effect - nobody used it and it isn't supported by the backends. | Alasdair Armstrong | |
| 2017-08-15 | Export existential destructuring function in type_check.mli. | Alasdair Armstrong | |
| Also rename some functions for consistency. | |||
| 2017-08-15 | Export utility functions from type_check.ml | Alasdair Armstrong | |
| 2017-08-15 | Menhir parser support for try/catch | Alasdair Armstrong | |
| 2017-08-15 | Improve and simplify handling of mutable local variables | Thomas Bauereiss | |
| 2017-08-15 | Added exceptions and try/catch blocks to AST and typechecker in order | Alasdair Armstrong | |
| to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail. | |||
| 2017-08-14 | Existentials in free type var functions | Brian Campbell | |
| 2017-08-14 | Some overloaded equality support in monomorphisation | Brian Campbell | |
| 2017-08-14 | Merge remote-tracking branch 'origin/master' into experiments | Alasdair Armstrong | |
| 2017-08-14 | Merge remote-tracking branch 'origin/mono-experiments' into experiments | Alasdair Armstrong | |
| 2017-08-14 | More constructs in menhir parser, plus support for both left and right infix ↵ | Alasdair Armstrong | |
| operators. | |||
| 2017-08-14 | Keep all asserts in the program during type checking | Brian Campbell | |
| 2017-08-14 | Don't reverse lexp tuple during type checking | Brian Campbell | |
| 2017-08-12 | Resolve ambiguity between negation of integers and bools | Thomas Bauereiss | |
| 2017-08-12 | Fix compilation issue for 32-bit systems | Thomas Bauereiss | |
| 2017-08-11 | Menhir for new parser, ocamlyacc for old | Brian Campbell | |
| 2017-08-11 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-11 | Make type checking just clever enough to solve 8*n = constant | Brian Campbell | |
| 2017-08-10 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| Conflicts: src/pretty_print_common.ml | |||
| 2017-08-10 | Fix bug with subtyping in let bindings | Alasdair Armstrong | |
| 2017-08-10 | Improved operator support for test menhir parser | Alasdair Armstrong | |
| 2017-08-10 | Experimenting with alternate parser | Alasdair Armstrong | |
| 2017-08-10 | Add support for early return to Lem backend | Thomas Bauereiss | |
| Implemented using the exception monad, by throwing and catching the return value | |||
| 2017-08-10 | Disable menhir on this branch | Brian Campbell | |
| (until location information is updated) | |||
| 2017-08-10 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-10 | Existentials in Lem AST output | Brian Campbell | |
| 2017-08-10 | Experimental removal of existentials | Brian Campbell | |
| 2017-08-10 | Improved existentials and type synonyms | Alasdair Armstrong | |
| 2017-08-09 | Pretty-print some more type annotations | Thomas Bauereiss | |
| 2017-08-08 | Add infrastructure to play with new menhir parsers. | Alasdair Armstrong | |
| Added a copy of the current parser/lexer in parser2.mly and lexer2.mll. They can be used with the -new_parser flag. Currently they are just copies of the existing files. | |||
| 2017-08-08 | Switch to using menhir for sail parser in experiments branch | Alasdair Armstrong | |
| 2017-08-08 | Fix Lem bindings in test cases | Thomas 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-08 | Glue together Sail prelude and Lem library | Thomas Bauereiss | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |