summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Collapse)Author
2015-11-07fixes, no more uncessary variables, pp progressChristopher Pulte
2015-11-06fixesChristopher Pulte
2015-11-06fixesChristopher Pulte
2015-11-05some progress on lem backend: rewrite away mutable variable assignments, ↵Christopher Pulte
rewrite for-loops, if/case-expressions to return updated variables
2015-11-04Add a new module for writing queries/analyses that aren't type checking but ↵Kathy Gray
could be useful Define in that a function for determining a default direction for vectors
2015-10-29Ocaml generation now just needing big int/little int issues resolved ↵Kathy Gray
(probably) at least for Power.
2015-10-28progress on lem backend: auto-generate read_register and write_register ↵Christopher Pulte
functions, and state definition
2015-10-26Switch name set to name map to include type and expression dataKathy Gray
2015-10-26Add variable set to rewritersKathy Gray
2015-10-26Begin if variable introduction rewritingKathy Gray
2015-10-20fix a-normalisation bugChristopher Pulte
2015-10-19progress on lem backendChristopher Pulte
2015-10-17clean up, more readabilityChristopher Pulte
2015-10-17a-normalisation for lem backendChristopher Pulte
2015-10-13some progress on sequentialise_effectsChristopher Pulte
2015-10-12fixesChristopher Pulte
2015-10-12apply rewriter changes to master as wellChristopher Pulte
2015-10-07adapted pretty_print and rewriter to new tannot typeChristopher Pulte
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher Pulte
2015-10-06Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-06fixesChristopher Pulte
2015-10-06make let and case actually call pattern rewriterKathy Gray
2015-10-05made vector_concat pass remove typ annotation expression inside ↵Christopher Pulte
vector_concat patterns, fixed a pp missing newline
2015-10-05some fixesChristopher Pulte
2015-10-05Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-05added pattern rewriting for DEF_val expressionsChristopher Pulte
2015-10-05More library functionsKathy Gray
Tweak to rewriter to actually rewrite function patterns
2015-10-05added funcl pattern rewriting to remove vector concat patternsChristopher Pulte
2015-10-04add 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-29ml output passing simple test suite, except for register aliasesKathy 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-29Boiler plate to generate an ml file from a sail spec. Now debugging the ↵Kathy Gray
output of such
2015-09-28added rewriter rewrite_defs_remove_vector_concat that should get rid of ↵Christopher Pulte
vector-concat patterns. Not tested.
2015-09-25added 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-25added 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-25building version of last change, removing stray )Kathy Gray
2015-09-25Rewrite expressions for ocaml, lifting assignment introductions into a ↵Kathy Gray
special let form to set the scope
2015-09-24Beginning of expression rewriter for ocamlKathy Gray
2015-09-24basic pattern rewriterKathy Gray
2015-09-24Parameterise the rewriter's for multiple different rewritingsKathy Gray
Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope
2015-09-24added 'remove_vector_string_patterns and .._expressions functionsChristopher Pulte
2015-09-17Type checker checking on case splits properly, and dependency ↵Kathy Gray
transformations restored :)
2015-09-06Improved type system, so that it catches int where there should be natKathy 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-06-30Change 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-30Fix updating dec vector start bugsKathy Gray
2015-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
Events are eamem to signal the memory address to write to and wmv to pass the value to write
2015-06-10Put missing cases into nexp_eq_checkKathy Gray
2015-06-04reduce number of unknown identifiers and get one step closer to actually ↵Kathy Gray
decoding an ARM instruction. (Note: may fix issue #2, haven't checked yet)
2015-05-01Fix pattern match bug with enumerated valuesKathy Gray
2015-05-01Change interpreter interface to support ppcmem2's view of vectors as always ↵Kathy Gray
increasing while supporting inc and dec views to the interpreter and in printing Fix bugs exposed by running idlarm several instructions (after fixing above)
2015-03-26Add subtraction to nexp grammar (removing the need to do a + (-1 * b))Kathy Gray
Fix up parsing on 2** precedence Fix errors on type variables in function definition
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 00:52:20 +0000