| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-26 | move closer to power.sail -> power.ml output | Kathy Gray | |
| 2016-01-06 | Add new assert expression to Sail | Kathy Gray | |
| This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified. | |||
| 2015-12-21 | fixes, pp progress | Christopher | |
| 2015-12-16 | rewriter and pp changes for generating ARM output | Christopher | |
| 2015-12-15 | better location information | Christopher | |
| 2015-12-09 | adapted for Kathy's lexp effect typing changes: register writes should be ↵ | Christopher | |
| correct now, fixes, pp | |||
| 2015-12-07 | adapted pp for Kathy's effect type changes | Christopher | |
| 2015-12-03 | added prompt.lem for connecting to concurrency model and ↵ | Christopher Pulte | |
| {power,armv8}_extras.lem; fixes | |||
| 2015-11-25 | fixes, pp | Christopher Pulte | |
| 2015-11-24 | Add BE_escape effect when an E_exit is seen | Kathy Gray | |
| Close #20 | |||
| 2015-11-20 | no more unecessary variables from removing vector-concatenation pattern ↵ | Christopher Pulte | |
| matches, reset variable name counter for each function clause, fixes | |||
| 2015-11-19 | fixes for cumulative effect anotations | Christopher Pulte | |
| 2015-11-13 | fixes, more pp | Christopher Pulte | |
| 2015-11-10 | rewriting fixes, syntactically correct lem syntax, number type errors remaining | Christopher Pulte | |
| 2015-11-07 | fixes, no more uncessary variables, pp progress | Christopher Pulte | |
| 2015-11-06 | progress on generating function for read/writing register fields | Christopher Pulte | |
| 2015-11-06 | fixes | Christopher Pulte | |
| 2015-11-05 | some progress on lem backend: rewrite away mutable variable assignments, ↵ | Christopher Pulte | |
| rewrite for-loops, if/case-expressions to return updated variables | |||
| 2015-10-29 | Ocaml generation now just needing big int/little int issues resolved ↵ | Kathy Gray | |
| (probably) at least for Power. | |||
| 2015-10-28 | progress on lem backend: auto-generate read_register and write_register ↵ | Christopher Pulte | |
| functions, and state definition | |||
| 2015-10-26 | fix | Christopher Pulte | |
| 2015-10-26 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-26 | add preliminary Sail_values.lem, adapt lem pp to recent Ocaml pp changes | Christopher Pulte | |
| 2015-10-23 | More of sail correctly generating ocaml; including using polymorphic ↵ | Kathy Gray | |
| variants when there are more than 246 constructors | |||
| 2015-10-20 | add copies of ocaml-pp functions for lem-pp | Christopher Pulte | |
| 2015-10-20 | ocaml output now produces parsing power.sail | Kathy Gray | |
| 2015-10-20 | more fixes | Kathy Gray | |
| 2015-10-20 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-20 | compiling prettyprinter | Kathy Gray | |
| 2015-10-20 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-20 | fix a-normalisation bug | Christopher Pulte | |
| 2015-10-20 | Fixing bugs in pretty printer to ocaml | Kathy Gray | |
| 2015-10-19 | progress on lem backend | Christopher Pulte | |
| 2015-10-13 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-13 | some progress on sequentialise_effects | Christopher Pulte | |
| 2015-10-13 | Refine local vs cumulative effects for lexp | Kathy Gray | |
| More ocaml output, better treatment of registers. | |||
| 2015-10-07 | Compiling again after refactoring. Haven't pushed to interpreter and lem yet | Kathy Gray | |
| 2015-10-07 | adapted pretty_print and rewriter to new tannot type | Christopher Pulte | |
| 2015-10-07 | start changing representation of registers for ocaml | Kathy Gray | |
| 2015-10-06 | better printing for register writing, whole register (maybe not "right" yet) | Kathy Gray | |
| more library | |||
| 2015-10-05 | made vector_concat pass remove typ annotation expression inside ↵ | Christopher Pulte | |
| vector_concat patterns, fixed a pp missing newline | |||
| 2015-10-04 | add find_updated_vars to support for-loops for lem or prover backend, add ↵ | Christopher Pulte | |
| normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested | |||
| 2015-09-30 | Alias support for ocaml mode | Kathy Gray | |
| 2015-09-29 | capitalise and uncapitalise according to ocaml requirements | Kathy Gray | |
| 2015-09-29 | ml output passing simple test suite, except for register aliases | Kathy Gray | |
| Known todo: Write library functions in ocaml Properly upper-case/lower-case the first letter of names to conform to ocaml requirements Handle register aliases Turn id reads to dereferences for local ref variables | |||
| 2015-09-29 | Boiler plate to generate an ml file from a sail spec. Now debugging the ↵ | Kathy Gray | |
| output of such | |||
| 2015-09-28 | for loop variant without closure required | Kathy Gray | |
| 2015-09-28 | basic untested ocaml boiler plate | Kathy Gray | |
| 2015-09-28 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-09-28 | completed pp for E_for expressions, necessary OCaml foreach_inc and ↵ | Christopher Pulte | |
| foreach_dec declarations in comment | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |