source: src/RTLabs

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2728   8 years sacerdot listb.ma => listb_extra.ma for extraction
(edit) @2724   8 years campbell Add RTLabs cost labelling checks to compiler.ma.
(edit) @2722   8 years campbell It's easier to keep the real function identifier in front-end …
(edit) @2716   8 years sacerdot utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
(edit) @2689   8 years tranquil * fixed passes up to linearisation
(edit) @2677   8 years campbell Retain the pointer for the function called in front-end call states so …
(edit) @2674   8 years tranquil * another change in block definition * RTLabs -> RTL and ERTL -> …
(edit) @2645   8 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
(edit) @2640   8 years tranquil updated RTL and RTLabs to RTL translation
(edit) @2608   8 years garnier Regions are no more stored in blocks. block_region now tests the id, …
(edit) @2601   8 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
(edit) @2571   8 years campbell Lots of little changes for cl_tailcall and classifier change.
(edit) @2511   8 years campbell Conjecture main Cminor/RTLabs simulation results. Add a few notes …
(edit) @2505   8 years mckinna Cleaned up compiler.ma; some refactoring/additional code needed in …
(edit) @2502   8 years campbell Sketch a little about how measurable traces might work with RTLabs and …
(edit) @2499   8 years campbell Separate out the RTLabs abstract status record from the proofs about …
(edit) @2493   8 years mckinna Change in cst_well_defd to fix previously broken defn of …
(edit) @2490   8 years tranquil switched back to Byte immediate (instead of beval ones) propagated …
(edit) @2475   8 years campbell Get compiler.ma and correctness.ma checking again. Note that the …
(edit) @2439   8 years campbell Get a proper reverse mapping of function blocks to identifiers by …
(edit) @2420   8 years campbell Tidy away generic results about folds on positive/identifier maps.
(edit) @2418   8 years campbell Add a checking function for the uniqueness of cost labels in RTLabs …
(edit) @2395   8 years campbell Proper handling of comparison of pointers off-the-end of an object. We …
(edit) @2384   8 years campbell Move Matita pretty printers into place.
(edit) @2315   9 years campbell Add some more commentary.
(edit) @2314   9 years campbell Move generic definitions from recent commit to appropriate places.
(edit) @2313   9 years campbell RTLabs cost checker correct.
(edit) @2308   9 years campbell More proof (and corrections) on cost checking.
(edit) @2307   9 years campbell Half the proofs for sound cost labelling check.
(edit) @2305   9 years campbell RTLabs cost spec checking function implemented (lacks proof, or much …
(edit) @2303   9 years campbell Some preliminary checking of cost labelling properties in RTLabs.
(edit) @2300   9 years campbell Cut out some dead ends and add some comments to the last commit.
(edit) @2299   9 years campbell Soundly labelled RTLabs structured traces are "unrepeating".
(edit) @2297   9 years campbell Nicer form of steps until cost label bound in RTLabs.
(edit) @2296   9 years campbell Tidy up some ill-placed definitions.
(edit) @2295   9 years campbell Start on showing unrepeating property of RTLabs structured traces: …
(edit) @2294   9 years campbell Make RTLabs cost spec deterministic.
(edit) @2293   9 years campbell Add instruction pointer for call states in RTLabs.
(edit) @2292   9 years campbell More RTLabs invariants.
(edit) @2290   9 years campbell Remove jump tables from RTLabs -> RTL.
(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   9 years campbell Provide a combined type for terminating and non-terminating structured …
(edit) @1808   9 years campbell Create a Prop version of the non-terminating structured traces so that …
(edit) @1806   9 years campbell Show that we could construct RTLabs non-terminating structured traces …
(edit) @1805   9 years campbell RTLabs structured traces: package up some of the properties we need …
(edit) @1784   9 years campbell Start on proof of existence of nonterminating RTLabs structured traces.
(edit) @1782   9 years campbell Correct bad inversion.
(edit) @1765   9 years campbell Rule out final states in non-terminating executions chunks (RTLabs …
(edit) @1764   9 years campbell Terminating function preserve the property that the execution does not …
(edit) @1736   9 years campbell Show that the bound on the number of instructions until a cost label …
(edit) @1719   9 years campbell Show that non-termination survives a terminating function call.
(edit) @1713   9 years campbell Add a distinguished final state to the front-end languages to match up …
(edit) @1712   9 years campbell Show that constructing an RTLabs structure trace really does use a …
(edit) @1707   9 years campbell Progress on finite segments of infinite RTLabs structured trace.
(edit) @1706   9 years campbell Checkpoint RTLabs structured traces.
(edit) @1705   9 years campbell Checkpoint RTLabs labelling soundness work.
(edit) @1682   9 years campbell Complete proof for as_after_return for RTLabs.
(edit) @1681   9 years campbell Checkpoint of stack preservation work in RTLabs.
(edit) @1680   9 years campbell Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
(edit) @1675   9 years campbell Some work on sound labelled for RTLabs.
(edit) @1671   9 years campbell A little more on RTLabs infinite traces.
(edit) @1670   9 years campbell Snapshot of non-terminating RTLabs structured traces work.
(edit) @1656   9 years campbell Minor fixups to RTLabs/Traces due to syntax changes.
(edit) @1655   9 years campbell Update Cminor and RTLabs semantics to use new monad definitions.
(edit) @1654   9 years campbell Corrections to structured trace definitions (see the mailing list). …
(edit) @1653   9 years campbell Start on building finite sections of non-terminating structured traces.
(edit) @1651   9 years campbell Start looking at non-terminating structured traces by defining …
(edit) @1644   9 years tranquil minor changes
(edit) @1643   9 years tranquil * some changes in everything * separated extensions in sequential and …
(edit) @1640   9 years tranquil * finished fork of semantics.ma * unification of Errors under the …
(edit) @1638   9 years campbell Tidy up RTLabs structured traces code a little.
Note: See TracRevisionLog for help on using the revision log.