| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2017-11-27 | Split rewriter into separate rewriting library and rewrite passes | Alasdair Armstrong | |
| As discussed previously, we wanted to start refactoring the re-writer to make it a bit less monolithic, and in the future potentially break it into separate files for backend-specific rewrites and stuff. - rewriter.ml now contains the generic re-writing code - rewrites.ml contains the rewriting passes themselves It would be nice if the generic rewriting code didn't depend on the typechecker, because then it could be used in ASL parser on untyped code. | |||
| 2017-11-27 | Use guards from when patterns when typing cases | Brian Campbell | |
| 2017-11-27 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-11-27 | Compile assertions into OCaml | Alasdair Armstrong | |
| and_bool and or_bool now are treated specially in the ocaml backend, so that they have the correct short-circuiting behaviour. This is required so that assertions don't fail for the ARM spec for predicates that shouldn't be tested in certain circumstances, for example things like: IsAArch32() && AArch32_specific_predicate Also fixed an issue in the sail library for ocaml where greater than or equal to was being mapped to greater than. | |||
| 2017-11-27 | Fix bitvector pattern removal typo | Brian Campbell | |
| 2017-11-27 | Replace bad generic comparisons in mono | Brian Campbell | |
| 2017-11-27 | Case splitting on bools | Brian Campbell | |
| (mostly to make test cases easier) | |||
| 2017-11-24 | Use unbound precision big_ints throughout sail. | Alasdair Armstrong | |
| Alastair's test cases revealed that using regular ints causes issues throughout sail, where all kinds of things can internally overflow in edge cases. This either causes crashes (e.g. int_of_string fails for big ints) or bizarre inexplicable behaviour. This patch switches the sail AST to use big_int rather than int, and updates everything accordingly. This touches everything and there may be bugs where I mistranslated things, and also n = m will still typecheck with big_ints but fail at runtime (ocaml seems to have decided that static typing is unnecessary for equality...), as it needs to be changed to eq_big_int. I also got rid of the old unused ocaml backend while I was updating things, so as to not have to fix it. | |||
| 2017-11-24 | Attempt to document intermediate language used by Sail in ott. | Alasdair Armstrong | |
| 2017-11-23 | renaming | Shaked Flur | |
| 2017-11-23 | added RISCV_ prefix to some values to stop Lem from renaming them | Shaked Flur | |
| 2017-11-21 | Expose entry point in elf_loader for Sail model | Alasdair Armstrong | |
| 2017-11-21 | Check non-constraint liftable assertions in blocks correctly | Alasdair Armstrong | |
| 2017-11-21 | Merge Thomas' suggested changes | Brian Campbell | |
| Use overloading to find eq/neq Track range/atom split Missing type expansion | |||
| 2017-11-20 | Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| experiments | |||
| 2017-11-20 | Fix a bug with constraint generation in flow typing. | Alasdair Armstrong | |
| This bug manifested as the ARM example elf executable printing the wrong characters... but otherwise doing not failing and exiting cleanly. It didn't trigger the test suite at all. I tracked it down to this line using git-bisect, and while returning nc_true is a bit suspect I'm still not 100% sure how this caused such a subtle and annoying bug in the generated ocaml code - it took several hours to track down the breakage to this line. | |||
| 2017-11-20 | Tidy last up | Brian Campbell | |
| 2017-11-20 | Constant propagation in guards | Brian Campbell | |
| 2017-11-20 | Basic handling of recursive calls in monomorphisation analysis | Brian Campbell | |
| 2017-11-20 | Look up the right type variables in monomorphisation analysis | Brian Campbell | |
| 2017-11-20 | Support new nexp in mono | Brian Campbell | |
| 2017-11-17 | Fix Makefile for interpreter and update instruction_extractor | Alasdair Armstrong | |
| Instruction extractor code that I commented out in this commit seems buggy anyway - it will claim that the length of all bitvectors is 64?! | |||
| 2017-11-17 | Fix interpreter to work with new typechecker | Alasdair Armstrong | |
| Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard. | |||
| 2017-11-16 | Make the generation of the lem_ast numeric constants automatic for all ↵ | Alasdair Armstrong | |
| numbers below 129 | |||
| 2017-11-16 | Made l2.ott generate an ast.lem which is is valid w.r.t. -lem_ast output. | Alasdair Armstrong | |
| This is the first step towards getting the interpreter working on this branch | |||
| 2017-11-16 | Remove unused Typ_wild constructor | Alasdair Armstrong | |
| 2017-11-16 | Fixed some longstanding issues regarding constraints on type constructors. | Alasdair Armstrong | |
| Now constraints on type constructors are checked correctly when checking that types are well formed using Env.wf_typ. The arity and kind of type constructor arguments are also checked in the same way. Also some general cleanups to the type checker code, with some auxillary functions being moved to more appropriate files. | |||
| 2017-11-15 | Additional test case for OCaml backend | Alasdair Armstrong | |
| 2017-11-15 | Simplify flow typing code in typechecker | Alasdair Armstrong | |
| 2017-11-15 | Merge branch 'smt' into experiments | Alasdair Armstrong | |
| 2017-11-15 | Fix atom - range unification again | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |