| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-15 | Experimenting with interactive mode | Alasdair Armstrong | |
| 2017-12-14 | Merge remote-tracking branch 'origin/experiments' into interactive | Alasdair Armstrong | |
| 2017-12-14 | Fix all compiler warning except in lem pretty printer and monomorphisation | Alasdair Armstrong | |
| 2017-12-13 | Cleanup code by fixing compiler warnings, and fix ocaml compilation | Alasdair Armstrong | |
| Add the ast.sed script we need to build sail. Currently we just need this to fix up the locations in the AST but it will be removed once we can share locations between ocaml and lem. | |||
| 2017-12-13 | Merge remote-tracking branch 'origin/master' into interactive | Alasdair Armstrong | |
| 2017-12-13 | Use big_nums from Lem | Alasdair Armstrong | |
| 2017-12-13 | find zarith using ocamlfind instead of using the one in ocaml-lib which is ↵ | Shaked Flur | |
| no longer there | |||
| 2017-12-12 | Add a few helper functions for bit lists | Thomas Bauereiss | |
| 2017-12-12 | Make mono analysis fail properly on effectful functions | Brian Campbell | |
| 2017-12-12 | moved the Power patch (shallow embedding) to ppcmem2 | Shaked Flur | |
| 2017-12-11 | Allow stepping through code when evaluating | Alasdair Armstrong | |
| 2017-12-11 | Prototype interactive mode for sail. | Alasdair Armstrong | |
| Requires linenoise library (opam install linenoise) for readline support. Use 'make isail' to build sail with interactive support. Plain 'make sail' should work as before with no additional dependencies. Use 'sail -i <commands>' to run sail interactively, e.g. sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail then try some commands for typechecking and evaluation sail> :t main sail> main () Doesn't use the lem interpreter right now, instead has a small operational semantics in src/interpreter.ml, but this is not very complete and will be changed/removed. | |||
| 2017-12-11 | Remove some duplication from monomorphisation analysis failure reports | Brian Campbell | |
| 2017-12-07 | More OCaml test cases | Alasdair Armstrong | |
| Improved handling of try/catch Better handling of unprovable constraints when the environment contains false | |||
| 2017-12-07 | Fix boolean literal constraints | Alasdair Armstrong | |
| 2017-12-07 | Fix regressions in OCaml output | Alasdair Armstrong | |
| Recent patches have made the rewriter more strict about performing type correct rewrites. This is mostly a good thing but did cause some problems with the ocaml backend. Currently the sizeof rewriter doesn't seem to preserve type correctness - I suspect this is because when it resolves the sizeofs, it generates constraints that are true, but not in a form where the typechecker can see that they are true. I disabled the re-check after the sizeof rewriting pass to fix this. Maybe we don't want to do this anyway because it's slow. Changes to function clauses with guards + monomorphisation changed how the typechecker handles literal patterns. I added a rewriting pass to rewrite literals to guarded equality checks, which is run before generating ocaml. The rewriter currently uses Env.empty in a view places. This can cause bugs because Env.empty is a totally unitialised environment that doesn't satisfy invariants we expect of an environment. This should be changed to initial_env and it shouldn't be exported, I fixed a few cases where this caused things to go wrong, but it should probably not be exported from Type_check.ml. | |||
| 2017-12-07 | Support monomorphisation with set constrained integers | Brian Campbell | |
| Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude | |||
| 2017-12-07 | Resolve function clause guard parsing ambiguity by requiring parentheses | Brian Campbell | |
| 2017-12-07 | Functions with guards changes in rewrites | Brian Campbell | |
| 2017-12-06 | Add parsing for guards in function clauses | Brian Campbell | |
| Breaks parsing ambiguities by removing = as an identifier in the old parser and requiring parentheses for some expressions in the new parser | |||
| 2017-12-06 | Remove filename mangling in monomorphisation | Brian Campbell | |
| Broke analysis a little | |||
| 2017-12-06 | Rework case checking to only introduce guards when necessary | Brian Campbell | |
| 2017-12-06 | Add top-level pattern match guards internally | Brian Campbell | |
| Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next. | |||
| 2017-12-06 | Make CHERI spec type-check again | Thomas Bauereiss | |
| 2017-12-06 | Merge remote branch 'experiments' into experiments | Thomas Bauereiss | |
| 2017-12-06 | Make AST after rewriting for Lem backend type-checkable | Thomas Bauereiss | |
| - Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now | |||
| 2017-12-05 | Better support for exceptions in sail for ASL specs that need them. | Alasdair Armstrong | |
| 2017-12-05 | add Ed | Peter Sewell | |
| 2017-12-05 | Merge branch 'master' into experiments | Alasdair Armstrong | |
| 2017-12-05 | Update header files on master | Alasdair Armstrong | |
| 2017-12-05 | Update license headers for Sail source | Alasdair Armstrong | |
| 2017-12-05 | Pretty printer now prints operator precedence correctly. | Alasdair Armstrong | |
| Also some simple rules to try to format if statements better based on contents while pretty printing. | |||
| 2017-12-04 | Fix warnings in test suite | Alasdair Armstrong | |
| 2017-12-04 | Merge remote-tracking branch 'origin/master' into experiments | Alasdair Armstrong | |
| 2017-12-04 | added the Power model | Shaked Flur | |
| 2017-12-04 | match what rmem expects from sail/arm | Shaked Flur | |
| 2017-12-04 | renamed hgen to gen | Shaked Flur | |
| 2017-11-30 | Use doc_typdef_lem from experiments | Alasdair Armstrong | |
| 2017-11-30 | Merge branch 'master' into experiments | Alasdair Armstrong | |
| 2017-11-30 | Improvements to enable parsing and checking intermediate rewriting | Alasdair Armstrong | |
| steps Parser now has syntax for mutual recusion blocks mutual { ... fundefs ... } which is used for parsing and pretty printing DEF_internal_mutrec. It's stripped away by the initial_check, so the typechecker never sees DEF_internal_mutrec. Maybe this could change, as forcing mutual recursion to be explicit would probably be a good thing. Added record syntax to the new parser New option -dmagic_hash is similar to GHC's -XMagicHash in that it allows for identifiers to contain the special hash character, which is used to introduce new autogenerated variables in a way that doesn't clash with existing names. Option -sil compiles sail down to the intermediate language defined in sil.ott (not complete yet). | |||
| 2017-11-30 | match what rmem (ppcmem2) expects from ISA Makefiles | Shaked Flur | |
| 2017-11-29 | Better lem_ast tagging and interpreter tweaks | Alasdair Armstrong | |
| 2017-11-29 | Switched to bytecode compiler for executing interpreter to avoid stack overflow | Alasdair Armstrong | |
| 2017-11-29 | Fix lem_ast output bugs | Alasdair Armstrong | |
| 2017-11-29 | Added location information for fixity and overloads in ast_util.ml | Alasdair Armstrong | |
| 2017-11-28 | Make pretty printer able to print several internal constructs for debugging | Alasdair Armstrong | |
| 2017-11-28 | Small update to trivial sizeof rewrites so we can handle all cases in | Alasdair Armstrong | |
| aarch64 vector instructions. There's maybe a better more general way to do this but I'm not sure what that would be. | |||
| 2017-11-28 | Fix issue where statements in blocks had incorrect environments | Alasdair Armstrong | |
| 2017-11-27 | Utility functions in ast_util for asl_parser | Alasdair Armstrong | |
| 2017-11-27 | Added test for short-circuiting of boolean operations | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |