source: src/RTLabs

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2288   9 years campbell Remove jumptables from RTLabs. :(
(edit) @2287   9 years campbell RTLabs typing for loads and stores.
(edit) @2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(edit) @2226   9 years campbell Whole program proof.
(edit) @2224   9 years campbell Proper whole program result in RTLabs/Traces
(edit) @2223   9 years campbell Simplify RTLabs structure traces proofs by getting rid of wrong …
(edit) @2218   9 years campbell Separate out cost properties required of RTLabs programs from the …
(edit) @2217   9 years tranquil * collapsed step_params, unserialized_params, funct_params and …
(edit) @2214   9 years tranquil * changed order of parameters of joint_internal_function and genv in …
(edit) @2208   9 years tranquil * moving some code around * changed immediates to hold beval in …
(edit) @2184   9 years campbell Minor fix ups.
(edit) @2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @2162   9 years tranquil * yet another correction to joint * added functions adding prologues …
(edit) @2155   9 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2103   9 years campbell Make transform_*program take a more general transformation to make …
(edit) @2044   9 years campbell PCs for RTLabs structured traces.
(edit) @2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2025   9 years campbell Silly typo and old comment.
(edit) @1999   9 years campbell Make back-end use the main global envs.
(edit) @1995   9 years campbell Overall compiler definition; bits and pieces to make everything happy(ish).
(edit) @1988   9 years campbell Abstraction of the memory contents in the memory models is no longer …
(edit) @1986   9 years campbell Get rid of unused abstraction of Globalenvs.
(edit) @1960   9 years campbell Update RTLabs structured traces to make minor changes in definitions.
(edit) @1920   9 years campbell Most of the labelling simulation. Still need to sort out switch …
(edit) @1882   9 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1880   9 years campbell Show that RTLabs flat traces are determined by their starting state, …
(edit) @1878   9 years campbell Enforce typing of constants in front-end, plus binops for RTLabs.
(edit) @1877   9 years campbell Update RTLabs structured traces for typed binops and new memory model.
(edit) @1874   9 years campbell First cut at using back-end memory model throughout. Note the …
(edit) @1872   9 years campbell Make binary operations in Cminor/RTLabs properly typed. A few extra …
(edit) @1812   10 years campbell Provide a combined type for terminating and non-terminating structured …
(edit) @1808   10 years campbell Create a Prop version of the non-terminating structured traces so that …
(edit) @1806   10 years campbell Show that we could construct RTLabs non-terminating structured traces …
(edit) @1805   10 years campbell RTLabs structured traces: package up some of the properties we need …
(edit) @1784   10 years campbell Start on proof of existence of nonterminating RTLabs structured traces.
(edit) @1782   10 years campbell Correct bad inversion.
(edit) @1765   10 years campbell Rule out final states in non-terminating executions chunks (RTLabs …
(edit) @1764   10 years campbell Terminating function preserve the property that the execution does not …
(edit) @1736   10 years campbell Show that the bound on the number of instructions until a cost label …
(edit) @1719   10 years campbell Show that non-termination survives a terminating function call.
(edit) @1713   10 years campbell Add a distinguished final state to the front-end languages to match up …
(edit) @1712   10 years campbell Show that constructing an RTLabs structure trace really does use a …
(edit) @1707   10 years campbell Progress on finite segments of infinite RTLabs structured trace.
(edit) @1706   10 years campbell Checkpoint RTLabs structured traces.
(edit) @1705   10 years campbell Checkpoint RTLabs labelling soundness work.
(edit) @1682   10 years campbell Complete proof for as_after_return for RTLabs.
(edit) @1681   10 years campbell Checkpoint of stack preservation work in RTLabs.
(edit) @1680   10 years campbell Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
(edit) @1675   10 years campbell Some work on sound labelled for RTLabs.
(edit) @1671   10 years campbell A little more on RTLabs infinite traces.
(edit) @1670   10 years campbell Snapshot of non-terminating RTLabs structured traces work.
(edit) @1656   10 years campbell Minor fixups to RTLabs/Traces due to syntax changes.
(edit) @1655   10 years campbell Update Cminor and RTLabs semantics to use new monad definitions.
(edit) @1654   10 years campbell Corrections to structured trace definitions (see the mailing list). …
(edit) @1653   10 years campbell Start on building finite sections of non-terminating structured traces.
(edit) @1651   10 years campbell Start looking at non-terminating structured traces by defining …
(edit) @1644   10 years tranquil minor changes
(edit) @1643   10 years tranquil * some changes in everything * separated extensions in sequential and …
(edit) @1640   10 years tranquil * finished fork of semantics.ma * unification of Errors under the …
(edit) @1638   10 years campbell Tidy up RTLabs structured traces code a little.
(edit) @1637   10 years campbell RTLabs structured traces: Add a termination measure to satisfy …
(edit) @1636   10 years tranquil * added coercions to arguments (in RTL) and notation for ops (for the …
(edit) @1635   10 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1633   10 years campbell Update Cminor pretty printer and examples.
(edit) @1626   10 years campbell Add extra type safety in front end. NB: critical freshness parts …
(edit) @1617   10 years campbell Note stuff to do on structured traces.
(edit) @1612   10 years sacerdot All library ported to new Matita lib (finally).
(edit) @1601   10 years sacerdot Files ported to new version of the standard library.
(edit) @1596   10 years campbell RTLabs structured traces: sort out passing of termination proofs around.
(edit) @1595   10 years campbell We don't need an explicit termination count when building traces.
(edit) @1594   10 years campbell Rework handling of termination information in RTLabs structured traces …
(edit) @1586   10 years campbell RTLabs structured traces: cost labels after jumps.
(edit) @1583   10 years campbell More on RTLabs structured traces. Fixed mistake in structure trace …
(edit) @1574   10 years campbell A little more progress on traces on RTLabs.
(edit) @1565   10 years campbell Note that RTLabs ought to classify branches as "jumps" (in the …
(edit) @1563   10 years campbell A little progress on constructing RTLabs structured traces.
(edit) @1559   10 years campbell Add a notion of flat traces with evidence for RTLabs.
(edit) @1552   10 years campbell Update RTLabs structured trace definition.
(edit) @1537   10 years campbell A preliminary definition of the abstract status record for RTLabs.
(edit) @1535   10 years campbell Make RTLabs semantics use knowledge that the next instruction always …
(edit) @1529   10 years campbell Update RTLabs to RTL with unary operation types.
(edit) @1521   10 years sacerdot Syntax change in Matita: change what where => change where what.
(edit) @1515   10 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1408   10 years sacerdot 1. Added joint/BEGlobalenvs that is a modification of …
(edit) @1369   10 years campbell Put type information into front-end unary ops. Slight change to …
(edit) @1358   10 years mulligan got rtlabs to rtl compiling, foldi_strong needs examining
(edit) @1356   10 years mulligan deleted redundant directory. added outlines for both reports, and …
(edit) @1354   10 years sacerdot One axiom closed.
(edit) @1352   10 years sacerdot This commit is made necessary by the last Matita change. Inclusion is …
(edit) @1343   10 years mulligan fixed some bugs in the translation
(edit) @1331   10 years mulligan some changes, but i now have two contradictory proof obligations.
(edit) @1325   10 years mulligan finished implementing the translate constant function
(edit) @1316   10 years campbell Merge in id-lookup-branch to trunk.
(edit) @1315   10 years mulligan another move for the same reason. got rtlabs > rtl compiling again by …
(edit) @1314   10 years mulligan name changes so that bash tab completion actually works with some …
(edit) @1308   10 years mulligan changes to translate_cst
(edit) @1307   10 years mulligan adding translate_cst
(edit) @1306   10 years mulligan small changes to rtlabs. what axioms remain look hard to close. need …
(edit) @1296   10 years mulligan changes
(edit) @1293   10 years mulligan finished rtl abs to rtl transformation subject to closing some axioms …
Note: See TracRevisionLog for help on using the revision log.