| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-02 | Also rewrite boolean terms in asserts during monomorphisation | Brian Campbell | |
| (otherwise wildcard cases won't be cut short at the assertion) | |||
| 2018-02-01 | More work on C compilation | Alasdair Armstrong | |
| Can now compile things like early returns. The same approach should work for exception handling as well. Once that's in place, just need to work a bit more on getting union types to work + the library of builtins, then we should be able to compile and run some of our specs via C. Also added some documentation in comments for the general approach taken when compiling (need many more though). | |||
| 2018-02-01 | Fix atom -> itself transformation when clauses feature different set of sizes | Brian Campbell | |
| 2018-02-01 | Curtail function bodies at known-false assertions during mono | Brian Campbell | |
| (preventing non-monomorphised sizes appearing in wildcard cases) | |||
| 2018-02-01 | Proper substitution and propagation of size from last commit | Brian Campbell | |
| 2018-02-01 | Substitute extra size case splits into body in monomorphisation | Brian Campbell | |
| 2018-02-01 | Make mono add case expressions for size tyvars without a corresponding arg | Brian Campbell | |
| 2018-02-01 | Comment out special casing of execute function in Lem pretty-printer | Thomas Bauereiss | |
| It assumes that execute is non-recursive, which is not the case for RISC-V with compressed instructions. Splitting execute into different auxiliary functions for each clause is probably still useful, as Isabelle is likely to parse many small functions faster than one big (potentially recursive) function, but this splitting should be done in the rewriter instead of the pretty-printer, in order to properly deal with recursion. | |||
| 2018-02-01 | Fix a bug where local variables could shadow functions | Alasdair Armstrong | |
| Currently the fix is to disallow this shadowing entirely, because it seems to cause trouble for ocaml. | |||
| 2018-02-01 | More work on running sail tests compiled to C | Alasdair Armstrong | |
| 2018-02-01 | Remove trace viewer application from repository | Alasdair Armstrong | |
| 2018-02-01 | Can now compile some simple sail programs to C | Alasdair Armstrong | |
| 2018-01-31 | Try to make bitvector pattern rewriting more robust | Thomas Bauereiss | |
| Look deep into sub-patterns for identifiers and literals instead of relying on assumptions about possible nestings | |||
| 2018-01-31 | Fix bug in bitvector pattern rewriting | Thomas Bauereiss | |
| Make rewriter look into P_typ patterns instead of throwing them away. | |||
| 2018-01-31 | More updates to C backend - matching and tuples | Alasdair Armstrong | |
| 2018-01-31 | Find buried set constraints in asserts | Brian Campbell | |
| 2018-01-31 | Fix mono continue away option | Brian Campbell | |
| 2018-01-31 | Export arithmetic shift right from Lem library | Thomas Bauereiss | |
| 2018-01-31 | Add Lem operator wrappers for bitlists | Thomas Bauereiss | |
| (accidentally committed the wrong file) | |||
| 2018-01-31 | Add wrappers around Lem operators using bitvector type class | Thomas Bauereiss | |
| Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output. | |||
| 2018-01-31 | Split base definitions of Lem monads and further built-ins (e.g. loop ↵ | Thomas Bauereiss | |
| combinators) Add Isabelle-specific theories imported directly after monad definitions, but before other combinators. These theories contain lemmas that tell the function package how to deal with monadic binds in function definitions. | |||
| 2018-01-30 | Handle 'N == 1 | 'N == 2 | ... style set constraints in mono | Brian Campbell | |
| 2018-01-30 | Optionally give *all* monomorphisation errors at once | Brian Campbell | |
| (and stop afterwards unless asked) | |||
| 2018-01-30 | Fix monomorphisation analysis to detect type variables which need to be | Brian Campbell | |
| concrete but aren't determined by one of the arguments. | |||
| 2018-01-30 | Fix failing Lem tests | Alasdair Armstrong | |
| 2018-01-30 | Updates to C backend | Alasdair Armstrong | |
| 2018-01-30 | Generate functions from enums to numbers and vice versa | Alasdair Armstrong | |
| For an enumeration type T, we can create a function T_of_num and num_of_T which convert from the enum to and from a numeric type. The numeric type is range(0, n) where n is the number of constructors in the enum minus one. This makes sure the conversion is type safe, but maybe this is too much of a hassle. It would be possible to automatically overload all these functions into generic to_enum and from_enum as in Haskell's Enum typeclass, but we don't do this yet. Currently these functions affect a few lem test cases, but I think that is only because they are tested without any prelude functions and pattern rewrites require a few functions to be defined What is really broken is if one tries to generate these functions like enum x = A | B | C function f A = 0 function f B = 1 function f C = 2 the rewriter really doesn't like function clauses like this, and it seems really hard to fix properly (I tried and gave up), this is a shame as the generation code is much more succinct with definitions like above | |||
| 2018-01-29 | Add rreg effect to _reg_deref in fix_val_specs rewrite | Thomas Bauereiss | |
| The internal function _reg_deref is declared as pure, so that bitfield setters can be implemented as read-modify-write, while only having a wreg effect. However, for the Lem shallow embedding, the read step of those setters needs to be embedded into the monad. This could be special-cased in the Lem pretty printer, but then the pretty printer would have to replicate some logic of the letbind_effects rewriting step. It seems simplest to add the effect annotation early in the Lem rewriting pipeline, in the fix_val_specs step. This means that this rewriting step can only be used for other backends if these additional effects are acceptable. | |||
| 2018-01-29 | Output a few more type annotations for Lem | Thomas Bauereiss | |
| Allow pretty-printing of existential types, if the existentially quantified variables do not actually appear in the Lem output. This is useful for the bit list representation of bitvectors, as it will print the type annotation "list bitU" for bitvectors whose length depends on an existentially quantified variable. | |||
| 2018-01-29 | Look through let expressions when constructing nconstraints | Brian Campbell | |
| (needed for handling guards after atom-to-itself transformation in monomorphisation) | |||
| 2018-01-29 | Leave pure if-conditions in place instead of pulling out let-bindings | Brian Campbell | |
| 2018-01-29 | Set maximum split size to work with aarch64 no vector | Brian Campbell | |
| 2018-01-29 | Get typechecking to resolve overriding in remove numeral patterns rewrite | Brian Campbell | |
| 2018-01-29 | Move subst to ast_util, use for guarded clauses rewrite | Brian Campbell | |
| 2018-01-29 | Add some initial exception handling to the riscv execution loop. | Prashanth Mundkur | |
| 2018-01-29 | Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2 | Robert Norton | |
| 2018-01-29 | add tohost to value.ml | Robert Norton | |
| 2018-01-29 | implement shift primitives in sail_lib.ml | Robert Norton | |
| 2018-01-29 | Further updates to C backend | Alasdair Armstrong | |
| 2018-01-29 | Fix a bug where structs containing unions would generate bad to_string functions | Alasdair Armstrong | |
| Added a regression test in test/ocaml/string_of_struct | |||
| 2018-01-29 | Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2 | Alasdair Armstrong | |
| 2018-01-29 | Linksem does not use uint anymore | Shaked Flur | |
| 2018-01-29 | Turn off constraint substitution in mono | Brian Campbell | |
| (Type checker doesn't seem to use false aggressively enough for this) | |||
| 2018-01-29 | Use fresh variables when dealing with (multiple) literal patterns | Brian Campbell | |
| 2018-01-29 | Turn off warnings when rechecking after mono | Brian Campbell | |
| 2018-01-29 | Avoid generating (_ as n) in mono, broke atom type rewriting | Brian Campbell | |
| 2018-01-26 | Fixed loading ARM elf files | Alasdair Armstrong | |
| Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib | |||
| 2018-01-26 | One more mono rewrite | Brian Campbell | |
| 2018-01-26 | Missing -ocamlfind | Brian Campbell | |
| 2018-01-26 | Add replacement of complex nexp sizes by equivalent variables in mono | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |