|
|
|
@2992
|
8 years |
campbell |
Add "only one return" invariant to RTLabs functions.
|
|
|
|
@2948
|
8 years |
campbell |
Finish up measurable to structured proof, exposing the prefix and …
|
|
|
|
@2947
|
8 years |
campbell |
Init change in measurable to structured file.
|
|
|
|
@2946
|
8 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
|
@2937
|
8 years |
campbell |
Speed up checking of RTLabs/CostInj.ma.
|
|
|
|
@2936
|
8 years |
campbell |
Disable initialisation code generation in Cminor, propogate init data …
|
|
|
|
@2931
|
8 years |
sacerdot |
Partial back-track from Paolo's commit, that was partial.
|
|
|
|
@2925
|
8 years |
tranquil |
corrected bug in toggle_bool
|
|
|
|
@2923
|
8 years |
campbell |
Remove some leftovers.
|
|
|
|
@2918
|
8 years |
tranquil |
erased stupid accidental paste at the start of file (happened when …
|
|
|
|
@2917
|
8 years |
tranquil |
made it so that a 0 offset does not generate adding ops when accessing …
|
|
|
|
@2916
|
8 years |
tranquil |
corrected yet another endianness bug in load and store
|
|
|
|
@2915
|
8 years |
sacerdot |
Dead code removed.
|
|
|
|
@2914
|
8 years |
campbell |
Use single definition for stack measurement.
|
|
|
|
@2912
|
8 years |
sacerdot |
Ouch, another bug in the very same function.
Fixed too, on an example …
|
|
|
|
@2911
|
8 years |
sacerdot |
Bug fixed in the translation of casts.
|
|
|
|
@2897
|
8 years |
campbell |
Minor tidying.
|
|
|
|
@2896
|
8 years |
campbell |
Complete part of measurable to structured subtraces proof that
shows …
|
|
|
|
@2895
|
8 years |
campbell |
Match up function id from RTLabs Callstate with shadow stack,
use in …
|
|
|
|
@2894
|
8 years |
campbell |
Some progress on showing that the change to structured traces …
|
|
|
|
@2893
|
8 years |
campbell |
Add tlr_unrepeating.
|
|
|
|
@2892
|
8 years |
campbell |
Add cost hypotheses.
|
|
|
|
@2866
|
8 years |
tranquil |
corrected two bugs of the translation: constant translation used wrong …
|
|
|
|
@2840
|
8 years |
campbell |
Remove irrelevant stuff from RTLabs_partial_traces
|
|
|
|
@2839
|
8 years |
campbell |
Basic structure of RTLabs measurable to structured traces results.
|
|
|
|
@2823
|
8 years |
tranquil |
* corrected bug in ERTL semantics (both delframe and newframe did the …
|
|
|
|
@2811
|
8 years |
sacerdot |
Pre-classified system for RTLabs.
|
|
|
|
@2808
|
8 years |
tranquil |
added local_stacksize to joint internal functions to accomodate for …
|
|
|
|
@2796
|
8 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
|
@2774
|
8 years |
sacerdot |
1. the compiler now outputs both the stack cost model and the max …
|
|
|
|
@2760
|
8 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
|
@2757
|
8 years |
tranquil |
many things are still broken, but there is a partial backtrack on …
|
|
|
|
@2728
|
8 years |
sacerdot |
listb.ma => listb_extra.ma for extraction
|
|
|
|
@2724
|
8 years |
campbell |
Add RTLabs cost labelling checks to compiler.ma.
|
|
|
|
@2722
|
8 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
|
@2716
|
8 years |
sacerdot |
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
|
|
|
|
@2689
|
8 years |
tranquil |
* fixed passes up to linearisation
|
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2674
|
8 years |
tranquil |
* another change in block definition
* RTLabs -> RTL and ERTL -> …
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2640
|
8 years |
tranquil |
updated RTL and RTLabs to RTL translation
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2571
|
8 years |
campbell |
Lots of little changes for cl_tailcall and classifier change.
|
|
|
|
@2511
|
8 years |
campbell |
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …
|
|
|
|
@2505
|
8 years |
mckinna |
Cleaned up compiler.ma; some refactoring/additional code needed in …
|
|
|
|
@2502
|
8 years |
campbell |
Sketch a little about how measurable traces might work with RTLabs and …
|
|
|
|
@2499
|
8 years |
campbell |
Separate out the RTLabs abstract status record from the proofs about …
|
|
|
|
@2493
|
8 years |
mckinna |
Change in cst_well_defd to fix previously broken defn of …
|
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
|
@2475
|
8 years |
campbell |
Get compiler.ma and correctness.ma checking again. Note that the …
|
|
|
|
@2439
|
8 years |
campbell |
Get a proper reverse mapping of function blocks to identifiers by …
|
|
|
|
@2420
|
8 years |
campbell |
Tidy away generic results about folds on positive/identifier maps.
|
|
|
|
@2418
|
8 years |
campbell |
Add a checking function for the uniqueness of cost labels in RTLabs …
|
|
|
|
@2395
|
8 years |
campbell |
Proper handling of comparison of pointers off-the-end of an object.
We …
|
|
|
|
@2384
|
8 years |
campbell |
Move Matita pretty printers into place.
|
|
|
|
@2315
|
9 years |
campbell |
Add some more commentary.
|
|
|
|
@2314
|
9 years |
campbell |
Move generic definitions from recent commit to appropriate places.
|
|
|
|
@2313
|
9 years |
campbell |
RTLabs cost checker correct.
|
|
|
|
@2308
|
9 years |
campbell |
More proof (and corrections) on cost checking.
|
|
|
|
@2307
|
9 years |
campbell |
Half the proofs for sound cost labelling check.
|
|
|
|
@2305
|
9 years |
campbell |
RTLabs cost spec checking function implemented (lacks proof, or much …
|
|
|
|
@2303
|
9 years |
campbell |
Some preliminary checking of cost labelling properties in RTLabs.
|
|
|
|
@2300
|
9 years |
campbell |
Cut out some dead ends and add some comments to the last commit.
|
|
|
|
@2299
|
9 years |
campbell |
Soundly labelled RTLabs structured traces are "unrepeating".
|
|
|
|
@2297
|
9 years |
campbell |
Nicer form of steps until cost label bound in RTLabs.
|
|
|
|
@2296
|
9 years |
campbell |
Tidy up some ill-placed definitions.
|
|
|
|
@2295
|
9 years |
campbell |
Start on showing unrepeating property of RTLabs structured traces: …
|
|
|
|
@2294
|
9 years |
campbell |
Make RTLabs cost spec deterministic.
|
|
|
|
@2293
|
9 years |
campbell |
Add instruction pointer for call states in RTLabs.
|
|
|
|
@2292
|
9 years |
campbell |
More RTLabs invariants.
|
|
|
|
@2290
|
9 years |
campbell |
Remove jump tables from RTLabs -> RTL.
|
|
|
|
@2288
|
9 years |
campbell |
Remove jumptables from RTLabs. :(
|
|
|
|
@2287
|
9 years |
campbell |
RTLabs typing for loads and stores.
|
|
|
|
@2286
|
9 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@2226
|
9 years |
campbell |
Whole program proof.
|
|
|
|
@2224
|
9 years |
campbell |
Proper whole program result in RTLabs/Traces
|
|
|
|
@2223
|
9 years |
campbell |
Simplify RTLabs structure traces proofs by getting rid of wrong …
|
|
|
|
@2218
|
9 years |
campbell |
Separate out cost properties required of RTLabs programs from the …
|
|
|
|
@2217
|
9 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
|
@2214
|
9 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
|
@2208
|
9 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
|
@2184
|
9 years |
campbell |
Minor fix ups.
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2162
|
9 years |
tranquil |
* yet another correction to joint
* added functions adding prologues …
|
|
|
|
@2155
|
9 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@2044
|
9 years |
campbell |
PCs for RTLabs structured traces.
|
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@2025
|
9 years |
campbell |
Silly typo and old comment.
|
|
|
|
@1999
|
9 years |
campbell |
Make back-end use the main global envs.
|
|
|
|
@1995
|
9 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1986
|
9 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
|
@1960
|
9 years |
campbell |
Update RTLabs structured traces to make minor changes in definitions.
|
|
|
|
@1920
|
9 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1880
|
9 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1877
|
9 years |
campbell |
Update RTLabs structured traces for typed binops and new memory model.
|
|
|
|
