source: src/RTLabs

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2992   7 years campbell Add "only one return" invariant to RTLabs functions.
(edit) @2948   7 years campbell Finish up measurable to structured proof, exposing the prefix and …
(edit) @2947   7 years campbell Init change in measurable to structured file.
(edit) @2946   7 years tranquil main novelties: * there is an in-built stack_usage nat in joint …
(edit) @2937   7 years campbell Speed up checking of RTLabs/CostInj.ma.
(edit) @2936   7 years campbell Disable initialisation code generation in Cminor, propogate init data …
(edit) @2931   7 years sacerdot Partial back-track from Paolo's commit, that was partial.
(edit) @2925   7 years tranquil corrected bug in toggle_bool
(edit) @2923   7 years campbell Remove some leftovers.
(edit) @2918   7 years tranquil erased stupid accidental paste at the start of file (happened when …
(edit) @2917   7 years tranquil made it so that a 0 offset does not generate adding ops when accessing …
(edit) @2916   7 years tranquil corrected yet another endianness bug in load and store
(edit) @2915   7 years sacerdot Dead code removed.
(edit) @2914   7 years campbell Use single definition for stack measurement.
(edit) @2912   7 years sacerdot Ouch, another bug in the very same function. Fixed too, on an example …
(edit) @2911   7 years sacerdot Bug fixed in the translation of casts.
(edit) @2897   7 years campbell Minor tidying.
(edit) @2896   7 years campbell Complete part of measurable to structured subtraces proof that shows …
(edit) @2895   7 years campbell Match up function id from RTLabs Callstate with shadow stack, use in …
(edit) @2894   7 years campbell Some progress on showing that the change to structured traces …
(edit) @2893   7 years campbell Add tlr_unrepeating.
(edit) @2892   7 years campbell Add cost hypotheses.
(edit) @2866   7 years tranquil corrected two bugs of the translation: constant translation used wrong …
(edit) @2840   7 years campbell Remove irrelevant stuff from RTLabs_partial_traces
(edit) @2839   7 years campbell Basic structure of RTLabs measurable to structured traces results.
(edit) @2823   7 years tranquil * corrected bug in ERTL semantics (both delframe and newframe did the …
(edit) @2811   7 years sacerdot Pre-classified system for RTLabs.
(edit) @2808   7 years tranquil added local_stacksize to joint internal functions to accomodate for …
(edit) @2796   7 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
(edit) @2774   7 years sacerdot 1. the compiler now outputs both the stack cost model and the max …
(edit) @2760   7 years sacerdot 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
(edit) @2757   7 years tranquil many things are still broken, but there is a partial backtrack on …
(edit) @2728   7 years sacerdot listb.ma => listb_extra.ma for extraction
(edit) @2724   7 years campbell Add RTLabs cost labelling checks to compiler.ma.
(edit) @2722   7 years campbell It's easier to keep the real function identifier in front-end …
(edit) @2716   7 years sacerdot utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
(edit) @2689   7 years tranquil * fixed passes up to linearisation
(edit) @2677   7 years campbell Retain the pointer for the function called in front-end call states so …
(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   8 years campbell Whole program proof.
(edit) @2224   8 years campbell Proper whole program result in RTLabs/Traces
(edit) @2223   8 years campbell Simplify RTLabs structure traces proofs by getting rid of wrong …
(edit) @2218   8 years campbell Separate out cost properties required of RTLabs programs from the …
(edit) @2217   8 years tranquil * collapsed step_params, unserialized_params, funct_params and …
(edit) @2214   8 years tranquil * changed order of parameters of joint_internal_function and genv in …
(edit) @2208   8 years tranquil * moving some code around * changed immediates to hold beval in …
(edit) @2184   8 years campbell Minor fix ups.
(edit) @2176   8 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @2162   8 years tranquil * yet another correction to joint * added functions adding prologues …
(edit) @2155   8 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2103   8 years campbell Make transform_*program take a more general transformation to make …
(edit) @2044   8 years campbell PCs for RTLabs structured traces.
(edit) @2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2025   8 years campbell Silly typo and old comment.
(edit) @1999   8 years campbell Make back-end use the main global envs.
(edit) @1995   8 years campbell Overall compiler definition; bits and pieces to make everything happy(ish).
(edit) @1988   8 years campbell Abstraction of the memory contents in the memory models is no longer …
(edit) @1986   8 years campbell Get rid of unused abstraction of Globalenvs.
(edit) @1960   8 years campbell Update RTLabs structured traces to make minor changes in definitions.
(edit) @1920   8 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.
Note: See TracRevisionLog for help on using the revision log.