summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Collapse)Author
2017-03-24Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵Robert Norton
embedding.
2017-03-24changes to ocaml pp to allow mips->ocaml to compileRobert Norton
2017-02-03fix headersPeter Sewell
2016-11-08fixesChristopher Pulte
2016-10-27more shallow embedding fixesChristopher Pulte
2016-10-26shallow embedding fixesChristopher Pulte
2016-10-13make sail-to-lem rewriting passes use dependency analysis, make dependency ↵Christopher Pulte
analysis include type information, small pp fix
2016-10-10changed the way registers/register fields work, fixes, nicer names for new ↵Christopher Pulte
letbound variables
2016-09-26nicer lem output: fewer unnecessary letbinds, monad binds and returnsChristopher Pulte
2016-09-25nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵Christopher Pulte
for-loops or case-expressions also return updated variables
2016-09-24nicer lem output: fewer unecessary 'return'sChristopher Pulte
2016-09-19sail-to-lem progressChristopher Pulte
2016-09-16fixChristopher Pulte
2016-09-16make vector concatenation pattern removal deal with vector patterns of ↵Christopher Pulte
unknown length (in the last item)
2016-09-07push some lem pp changesChristopher Pulte
2016-08-14Start adding form for (a,b,c) := foo()Kathy Gray
Not working yet
2016-08-10Fix sizeof code generation to look at parameter boundsKathy Gray
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-07-20Make rewriter understand type abbreviations for removing internal_exp instancesKathy Gray
2016-05-27Add sizeof to sail. Documentation to followKathy Gray
2016-03-02Add new language feature to permit definitions of items of kind Nat, etc as ↵Kathy Gray
well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required.
2016-01-26move closer to power.sail -> power.ml outputKathy Gray
2016-01-21Start splitting values/etc into int/big_int for ocaml generationKathy Gray
2016-01-14small edit to previous commitKathy Gray
2016-01-14Fix cumulative effects for circumstance when lifting variable introductions ↵Kathy Gray
out of an if Note: this fixes the local cumulative effects for the e_assign and e_if, it may not properly propagate them to the context of the surrounding block
2016-01-12Fix undefined nvar occurrences that were impacting ARMKathy Gray
2016-01-07Add E_assert to basic rewritersKathy Gray
2015-12-21fixes, pp progressChristopher
2015-12-16rewriter and pp changes for generating ARM outputChristopher
2015-12-15better location informationChristopher
2015-12-10fixChristopher
2015-12-09adapted for Kathy's lexp effect typing changes: register writes should be ↵Christopher
correct now, fixes, pp
2015-11-25fixes, ppChristopher Pulte
2015-11-22do effect annotation updates more systematically, fix dedupChristopher Pulte
2015-11-20no more unecessary variables from removing vector-concatenation pattern ↵Christopher Pulte
matches, reset variable name counter for each function clause, fixes
2015-11-19fixes for cumulative effect anotationsChristopher Pulte
2015-11-13fixes, more ppChristopher Pulte
2015-11-10fix case-expressions' newreturnChristopher Pulte
2015-11-10rewriting fixes, syntactically correct lem syntax, number type errors remainingChristopher Pulte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 18:31:31 +0000