| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-31 | add very stripped down 2-instruction RISCV example with add and load. | Robert Norton | |
| 2018-01-31 | add some elf files from riscv test suite and run them on riscv model. | Robert Norton | |
| 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 | riscv prelude: add a to_bits function for converting ints to bits of given ↵ | Robert Norton | |
| length. | |||
| 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 | Fix Lem generation for RISC-V | Thomas Bauereiss | |
| 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 | Add a fixme for unhandled fences but allow them to execute. | Prashanth Mundkur | |
| 2018-01-29 | Initial handling of CSR reads/writes. | Prashanth Mundkur | |
| 2018-01-29 | Add satp to CSR dummy implemented predicate. Also direct the illegal ↵ | Prashanth Mundkur | |
| instruction exception through the exception handler. | |||
| 2018-01-29 | use check target in makefile when checking riscv spec. | Robert Norton | |
| 2018-01-29 | riscv: fix warnings about incomplete patterns. Add a check target in ↵ | Robert Norton | |
| Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings. | |||
| 2018-01-29 | Sync mono rewrites definitions with library | Brian Campbell | |
| 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 | riscv: remove break from main loop and place val spec in prelude. | Robert Norton | |
| 2018-01-29 | riscv: add tracing of register writes. | 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 | Added ecall/mret and exception support. | Prashanth Mundkur | |
| 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 | Shaked removing generation of now-uncessary uint dependency | Peter Sewell | |
| 2018-01-29 | Linksem does not use uint anymore | Shaked Flur | |
| 2018-01-29 | Fix error in RISCV: SLLI and SRLI were swapped... | Robert Norton | |
| 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-27 | Add Makefile for RISC-V | Thomas Bauereiss | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |