source: src/RTLabs

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2674   7 years tranquil * another change in block definition * RTLabs -> RTL and ERTL -> …
(edit) @2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
(edit) @2640   7 years tranquil updated RTL and RTLabs to RTL translation
(edit) @2608   7 years garnier Regions are no more stored in blocks. block_region now tests the id, …
(edit) @2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
(edit) @2571   7 years campbell Lots of little changes for cl_tailcall and classifier change.
(edit) @2511   7 years campbell Conjecture main Cminor/RTLabs simulation results. Add a few notes …
(edit) @2505   7 years mckinna Cleaned up compiler.ma; some refactoring/additional code needed in …
(edit) @2502   7 years campbell Sketch a little about how measurable traces might work with RTLabs and …
(edit) @2499   7 years campbell Separate out the RTLabs abstract status record from the proofs about …
(edit) @2493   7 years mckinna Change in cst_well_defd to fix previously broken defn of …
(edit) @2490   7 years tranquil switched back to Byte immediate (instead of beval ones) propagated …
(edit) @2475   7 years campbell Get compiler.ma and correctness.ma checking again. Note that the …
(edit) @2439   7 years campbell Get a proper reverse mapping of function blocks to identifiers by …
(edit) @2420   7 years campbell Tidy away generic results about folds on positive/identifier maps.
(edit) @2418   7 years campbell Add a checking function for the uniqueness of cost labels in RTLabs …
(edit) @2395   7 years campbell Proper handling of comparison of pointers off-the-end of an object. We …
(edit) @2384   7 years campbell Move Matita pretty printers into place.
(edit) @2315   7 years campbell Add some more commentary.
(edit) @2314   7 years campbell Move generic definitions from recent commit to appropriate places.
(edit) @2313   7 years campbell RTLabs cost checker correct.
(edit) @2308   7 years campbell More proof (and corrections) on cost checking.
(edit) @2307   7 years campbell Half the proofs for sound cost labelling check.
(edit) @2305   7 years campbell RTLabs cost spec checking function implemented (lacks proof, or much …
(edit) @2303   7 years campbell Some preliminary checking of cost labelling properties in RTLabs.
(edit) @2300   7 years campbell Cut out some dead ends and add some comments to the last commit.
(edit) @2299   7 years campbell Soundly labelled RTLabs structured traces are "unrepeating".
(edit) @2297   7 years campbell Nicer form of steps until cost label bound in RTLabs.
(edit) @2296   7 years campbell Tidy up some ill-placed definitions.
(edit) @2295   7 years campbell Start on showing unrepeating property of RTLabs structured traces: …
(edit) @2294   7 years campbell Make RTLabs cost spec deterministic.
(edit) @2293   7 years campbell Add instruction pointer for call states in RTLabs.
(edit) @2292   7 years campbell More RTLabs invariants.
(edit) @2290   7 years campbell Remove jump tables from RTLabs -> RTL.
(edit) @2288   7 years campbell Remove jumptables from RTLabs. :(
(edit) @2287   7 years campbell RTLabs typing for loads and stores.
(edit) @2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(edit) @2226   7 years campbell Whole program proof.
(edit) @2224   7 years campbell Proper whole program result in RTLabs/Traces
(edit) @2223   7 years campbell Simplify RTLabs structure traces proofs by getting rid of wrong …
(edit) @2218   7 years campbell Separate out cost properties required of RTLabs programs from the …
(edit) @2217   7 years tranquil * collapsed step_params, unserialized_params, funct_params and …
(edit) @2214   7 years tranquil * changed order of parameters of joint_internal_function and genv in …
(edit) @2208   7 years tranquil * moving some code around * changed immediates to hold beval in …
(edit) @2184   7 years campbell Minor fix ups.
(edit) @2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @2162   7 years tranquil * yet another correction to joint * added functions adding prologues …
(edit) @2155   7 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2103   7 years campbell Make transform_*program take a more general transformation to make …
(edit) @2044   7 years campbell PCs for RTLabs structured traces.
(edit) @2032   7 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2025   7 years campbell Silly typo and old comment.
(edit) @1999   7 years campbell Make back-end use the main global envs.
(edit) @1995   7 years campbell Overall compiler definition; bits and pieces to make everything happy(ish).
(edit) @1988   7 years campbell Abstraction of the memory contents in the memory models is no longer …
(edit) @1986   7 years campbell Get rid of unused abstraction of Globalenvs.
(edit) @1960   7 years campbell Update RTLabs structured traces to make minor changes in definitions.
(edit) @1920   7 years campbell Most of the labelling simulation. Still need to sort out switch …
(edit) @1882   8 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1880   8 years campbell Show that RTLabs flat traces are determined by their starting state, …
(edit) @1878   8 years campbell Enforce typing of constants in front-end, plus binops for RTLabs.
(edit) @1877   8 years campbell Update RTLabs structured traces for typed binops and new memory model.
(edit) @1874   8 years campbell First cut at using back-end memory model throughout. Note the …
(edit) @1872   8 years campbell Make binary operations in Cminor/RTLabs properly typed. A few extra …
(edit) @1812   8 years campbell Provide a combined type for terminating and non-terminating structured …
(edit) @1808   8 years campbell Create a Prop version of the non-terminating structured traces so that …
(edit) @1806   8 years campbell Show that we could construct RTLabs non-terminating structured traces …
(edit) @1805   8 years campbell RTLabs structured traces: package up some of the properties we need …
(edit) @1784   8 years campbell Start on proof of existence of nonterminating RTLabs structured traces.
(edit) @1782   8 years campbell Correct bad inversion.
(edit) @1765   8 years campbell Rule out final states in non-terminating executions chunks (RTLabs …
(edit) @1764   8 years campbell Terminating function preserve the property that the execution does not …
(edit) @1736   8 years campbell Show that the bound on the number of instructions until a cost label …
(edit) @1719   8 years campbell Show that non-termination survives a terminating function call.
(edit) @1713   8 years campbell Add a distinguished final state to the front-end languages to match up …
(edit) @1712   8 years campbell Show that constructing an RTLabs structure trace really does use a …
(edit) @1707   8 years campbell Progress on finite segments of infinite RTLabs structured trace.
(edit) @1706   8 years campbell Checkpoint RTLabs structured traces.
(edit) @1705   8 years campbell Checkpoint RTLabs labelling soundness work.
(edit) @1682   8 years campbell Complete proof for as_after_return for RTLabs.
(edit) @1681   8 years campbell Checkpoint of stack preservation work in RTLabs.
(edit) @1680   8 years campbell Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
(edit) @1675   8 years campbell Some work on sound labelled for RTLabs.
(edit) @1671   8 years campbell A little more on RTLabs infinite traces.
(edit) @1670   8 years campbell Snapshot of non-terminating RTLabs structured traces work.
(edit) @1656   8 years campbell Minor fixups to RTLabs/Traces due to syntax changes.
(edit) @1655   8 years campbell Update Cminor and RTLabs semantics to use new monad definitions.
(edit) @1654   8 years campbell Corrections to structured trace definitions (see the mailing list). …
(edit) @1653   8 years campbell Start on building finite sections of non-terminating structured traces.
(edit) @1651   8 years campbell Start looking at non-terminating structured traces by defining …
(edit) @1644   8 years tranquil minor changes
(edit) @1643   8 years tranquil * some changes in everything * separated extensions in sequential and …
(edit) @1640   8 years tranquil * finished fork of semantics.ma * unification of Errors under the …
(edit) @1638   8 years campbell Tidy up RTLabs structured traces code a little.
(edit) @1637   8 years campbell RTLabs structured traces: Add a termination measure to satisfy …
(edit) @1636   8 years tranquil * added coercions to arguments (in RTL) and notation for ops (for the …
(edit) @1635   8 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1633   8 years campbell Update Cminor pretty printer and examples.
(edit) @1626   8 years campbell Add extra type safety in front end. NB: critical freshness parts …
(edit) @1617   8 years campbell Note stuff to do on structured traces.
Note: See TracRevisionLog for help on using the revision log.