| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-05 | added funcl pattern rewriting to remove vector concat patterns | Christopher Pulte | |
| 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 | |||
| 2015-09-28 | Add initial support for register fields | Kathy Gray | |
| 2015-09-28 | tweak what the output expects | Kathy Gray | |
| 2015-09-28 | added rewriter rewrite_defs_remove_vector_concat that should get rid of ↵ | Christopher Pulte | |
| vector-concat patterns. Not tested. | |||
| 2015-09-25 | added something for remove_vector_string_patterns that for a give ↵ | Christopher Pulte | |
| pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet | |||
| 2015-09-25 | added something for remove_vector_string_patterns that for a give ↵ | Christopher Pulte | |
| pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet | |||
| 2015-09-25 | Potentially working ocaml mode, minus registers with fields, awaiting ↵ | Kathy Gray | |
| pattern-match rewriting | |||
| 2015-09-25 | building version of last change, removing stray ) | Kathy Gray | |
| 2015-09-25 | Rewrite expressions for ocaml, lifting assignment introductions into a ↵ | Kathy Gray | |
| special let form to set the scope | |||
| 2015-09-24 | Beginning of expression rewriter for ocaml | Kathy Gray | |
| 2015-09-24 | basic pattern rewriter | Kathy Gray | |
| 2015-09-24 | Parameterise the rewriter's for multiple different rewritings | Kathy Gray | |
| Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope | |||
| 2015-09-24 | added 'remove_vector_string_patterns and .._expressions functions | Christopher Pulte | |
| 2015-09-23 | More pretty printing | Kathy Gray | |
| A few more expressive tags for introducing mutable variables and for tracking local mutations A new pred for detecting bit vectors | |||
| 2015-09-22 | Start pretty printing ocaml for sequential | Kathy Gray | |
| 2015-09-17 | Type checker checking on case splits properly, and dependency ↵ | Kathy Gray | |
| transformations restored :) | |||
| 2015-09-06 | Turn off debug print outs | Kathy Gray | |
| 2015-09-06 | Improved type system, so that it catches int where there should be nat | Kathy Gray | |
| Note: the resulting Lem file generated may or may not actually work properly with the interpreter (i.e. it might have too many unknowns); still in the process of debugging some changes there. | |||
| 2015-08-18 | Make register fields with concatenated ranges compile now | Kathy Gray | |
| 2015-08-14 | Steps towards making constraint solver smarter | Kathy Gray | |
| 2015-08-06 | Update analysis to merge states and values after branches taken due to ↵ | Kathy Gray | |
| unknown conditions. Does not merge if one path has resulted in an exit | |||
| 2015-07-24 | Turn back off new analysis style until it works | Kathy Gray | |
| 2015-07-24 | Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 | Shaked Flur | |
| 2015-07-24 | added signed_integer | Shaked Flur | |
| 2015-07-24 | Begin doing better analysis on case splits over unknowns | Kathy Gray | |
| 2015-07-20 | minor fixes | Kathy Gray | |
| 2015-07-19 | abbreviate printing of memory values <=9 | Peter Sewell | |
| 2015-07-02 | fix match_pattern reverse bug | Kathy Gray | |
| 2015-07-01 | fix equality comparison | Kathy Gray | |
| 2015-07-01 | Use set instead of list for tainted values | Kathy Gray | |
| 2015-07-01 | Go on despite the presence of an exit in exhaustive mode | Kathy Gray | |
| 2015-06-30 | Change rewriter to better reset dec vectors to count from (length - 1) ↵ | Kathy Gray | |
| instead of whatever random spot they might be in, where functions expect length-n to 0 | |||
| 2015-06-30 | Fix updating dec vector start bugs | Kathy Gray | |
| 2015-06-29 | Fix pattern match error | Kathy Gray | |
| 2015-06-29 | Return unknown for a == unknown or unknown == a. Fixes issue #15 | Kathy Gray | |
| 2015-06-28 | Tag enumeration variables properly when introducing them | Kathy Gray | |
| 2015-06-26 | Better handling of literal true and false (turn them into the expected bit0 ↵ | Kathy Gray | |
| and bit1); also fix some handling of wmv and eamem. | |||
| 2015-06-24 | Support new write memory events | Kathy Gray | |
| 2015-06-24 | Support new memory write events in the sail front end and pretty printer | Kathy Gray | |
| Events are eamem to signal the memory address to write to and wmv to pass the value to write | |||
| 2015-06-24 | Add new outcomes/events separating effective address and value for memory writes | Kathy Gray | |
| 2015-06-22 | Fixes issue #12 | Kathy Gray | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |