Timeline


and

Mar 26, 2013:

7:13 PM Changeset [2970] by tranquil
now joint_if_entry can change when a preamble is added, so code points …
7:09 PM Changeset [2969] by sacerdot
Dead axiom removed :-)
7:07 PM Changeset [2968] by sacerdot
The initial status memory was not really initialized. Now it is.
6:54 PM Changeset [2967] by sacerdot
Semantics changed so that a terminating joint program that returns an …
6:35 PM Changeset [2966] by sacerdot
Modified by hand files (to improve a little bit the performance).
6:35 PM Changeset [2965] by sacerdot
Code performance improved a bit by hand.
6:33 PM Changeset [2964] by sacerdot
Debugging code removed.
6:32 PM Changeset [2963] by sacerdot
Bug fixed: the pre-main for the final code is now COST k1 …
5:36 PM Changeset [2962] by sacerdot
Most performant algorithm restored.
5:02 PM Changeset [2961] by sacerdot
Bug fixed (stupid typo in pre-main code made the compiler diverge on …
4:51 PM Changeset [2960] by sacerdot
New extraction, it diverges in RTL execution now.
4:46 PM Changeset [2959] by sacerdot
Typo
4:45 PM Changeset [2958] by sacerdot
Error message implemented.
4:41 PM Changeset [2957] by tranquil
fixed semantics_blocks
4:31 PM Changeset [2956] by tranquil
fixed LTL/LIN semantics
4:11 PM Changeset [2955] by tranquil
corrected stupid typo
3:52 PM Changeset [2954] by tranquil
resolved circular dependency for ERTLptr's semantics
3:34 PM Changeset [2953] by campbell
Fix silly label handling bug I realised was there during my talk…
2:01 PM Changeset [2952] by tranquil
* corrected all back-end premains to not pass any arguments to the …

Mar 25, 2013:

11:30 PM Changeset [2951] by sacerdot
New extraction. Novely: a pre-main is used in the back-end. …
10:39 PM Changeset [2950] by sacerdot
linearise repaired (did I do the right thing???)
9:48 PM Changeset [2949] by sacerdot
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …

Mar 24, 2013:

9:17 PM Changeset [2948] by campbell
Finish up measurable to structured proof, exposing the prefix and …
9:17 PM Changeset [2947] by campbell
Init change in measurable to structured file.
11:29 AM Changeset [2946] by tranquil
main novelties: * there is an in-built stack_usage nat in joint …

Mar 23, 2013:

8:43 AM Changeset [2945] by campbell
Minor tweak.
2:31 AM Changeset [2944] by sacerdot
Some progress.
2:07 AM Changeset [2943] by sacerdot
Mauro, I have put a daemon in place of the proof obligation that used …
1:37 AM Changeset [2942] by sacerdot
Many changes: 1. Coloured graphs are now specified in terms of …

Mar 22, 2013:

9:46 PM Changeset [2941] by campbell
Update proof slides.
7:16 PM Changeset [2940] by sacerdot
1. StatusSimulationHelper? changed to allow to use status_rel that …
10:11 AM Changeset [2939] by sacerdot
Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
2:11 AM Changeset [2938] by sacerdot
1. proof of "all eliminable are eliminable" completed 2. the notion of …

Mar 21, 2013:

9:45 PM Changeset [2937] by campbell
Speed up checking of RTLabs/CostInj.ma.
9:45 PM Changeset [2936] by campbell
Disable initialisation code generation in Cminor, propogate init data …
9:37 PM Changeset [2935] by tranquil
separation of RTL semantics in three different versions, and …
8:34 PM Changeset [2934] by sacerdot
Patch to obtain more easily comparable traces.
8:11 PM Changeset [2933] by sacerdot
New extraction, several bug fixed. RTL_semantics fixed by hand, will …
7:58 PM Changeset [2932] by sacerdot
Same comment as previous commit on this file: the previous commit was …
7:31 PM Changeset [2931] by sacerdot
Partial back-track from Paolo's commit, that was partial.
7:14 PM Changeset [2930] by sacerdot
More progress. Some useless parameters have been removed from the …
7:13 PM Changeset [2929] by sacerdot
Bug fixed: the coercion mechanism made you think that the CALL case …
6:26 PM Changeset [2928] by tranquil
some sketches about correctness proof
5:17 PM Changeset [2927] by tranquil
stupid bug in bool_of_beval
4:06 PM Changeset [2926] by tranquil
corrected bug in executing Sub
3:39 PM Changeset [2925] by tranquil
corrected bug in toggle_bool
8:39 AM Changeset [2924] by campbell
Make calls to a known identifier actually use a direct call.
8:38 AM Changeset [2923] by campbell
Remove some leftovers.
2:12 AM Changeset [2922] by sacerdot
Progress: proof of "eliminable statements can be eliminated" almost …
12:56 AM Changeset [2921] by sacerdot
Extracted again.
12:53 AM Changeset [2920] by sacerdot
dos2unix-ed

Mar 20, 2013:

7:21 PM Changeset [2919] by fguidi
"MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
5:10 PM Changeset [2918] by tranquil
erased stupid accidental paste at the start of file (happened when …
1:20 PM Changeset [2917] by tranquil
made it so that a 0 offset does not generate adding ops when accessing …
12:33 PM Changeset [2916] by tranquil
corrected yet another endianness bug in load and store
9:37 AM Changeset [2915] by sacerdot
Dead code removed.
8:39 AM Changeset [2914] by campbell
Use single definition for stack measurement.
12:24 AM Changeset [2913] by sacerdot
Bug corrected by hand. It will be corrected automatically by next …
12:21 AM Changeset [2912] by sacerdot
Ouch, another bug in the very same function. Fixed too, on an example …
12:12 AM Changeset [2911] by sacerdot
Bug fixed in the translation of casts.

Mar 19, 2013:

11:19 PM Changeset [2910] by sacerdot
Abstract statuses for ASM and OC completed. A simple test program can …
10:21 PM Changeset [2909] by sacerdot
New extraction.
8:00 PM Changeset [2908] by sacerdot
Bug fixed by hand, they will be fixed automatically by the new extraction.
7:48 PM Changeset [2907] by sacerdot
1. a few bugs fixed 2. as_return implemented for ASM & OC
9:54 AM Changeset [2906] by sacerdot
Bug fixed.
8:42 AM Changeset [2905] by sacerdot
Semantics of ASM in place (up to return values and function call …
1:27 AM Changeset [2904] by sacerdot
1. Algorithm modified by hand to make it run faster. The trusted …
1:25 AM Changeset [2903] by sacerdot
Extracted again.
1:24 AM Changeset [2902] by sacerdot
Quick hack to allow printing of OC code. It will be automatically …
1:22 AM Changeset [2901] by sacerdot
1. backendPrinter renamed to printer 2. Clight printing branched into …
1:20 AM Changeset [2900] by sacerdot
Flushing to understand where it is slow.
12:33 AM Changeset [2899] by sacerdot
1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …

Mar 18, 2013:

10:03 AM Changeset [2898] by piccolo
1) simplification of cond and seq case for StatusSimulationHelper?

Mar 16, 2013:

9:08 PM Changeset [2897] by campbell
Minor tidying.
9:08 PM Changeset [2896] by campbell
Complete part of measurable to structured subtraces proof that shows …
9:08 PM Changeset [2895] by campbell
Match up function id from RTLabs Callstate with shadow stack, use in …
9:08 PM Changeset [2894] by campbell
Some progress on showing that the change to structured traces …
9:08 PM Changeset [2893] by campbell
Add tlr_unrepeating.
9:08 PM Changeset [2892] by campbell
Add cost hypotheses.
10:42 AM Changeset [2891] by piccolo
added precondition on seq statement and tested correct in the …

Mar 15, 2013:

11:11 PM Changeset [2890] by sacerdot
Exported again, now the execution is correct up to LIN for a simple …
7:36 PM Changeset [2889] by sacerdot
It works very nice!
7:31 PM Changeset [2888] by tranquil
backtracked some partial changes
7:22 PM Changeset [2887] by tranquil
Corrected bug where eliminable statements where not eliminated. …
7:19 PM Changeset [2886] by piccolo
partial commit
7:06 PM Changeset [2885] by sacerdot
Hint at how to change everything.
6:37 PM Changeset [2884] by sacerdot
Debugging print added.
6:33 PM Changeset [2883] by piccolo
partial commit
5:52 PM Changeset [2882] by sacerdot
5:51 PM Changeset [2881] by sacerdot
5:51 PM Changeset [2880] by sacerdot
12:16 PM Changeset [2879] by tranquil
changed coercion from list of joint_seq to blocks to a more efficient one
11:32 AM Changeset [2878] by tranquil
backtracked some changes that were not ready for commit
11:29 AM Changeset [2877] by garnier
Correction of a bug in my former bug correction.
10:58 AM Changeset [2876] by tranquil
corrected another endianess bug in joint_semantics. Switched some …
1:32 AM Changeset [2875] by sacerdot
Pretty printing of object code integrated too. A couple of axioms make …

Mar 14, 2013:

10:46 PM Changeset [2874] by sacerdot
Syntax fixed: ./cerco [-exec] filename annotationoption
10:37 PM Changeset [2873] by sacerdot
Extracted again.
7:26 PM Changeset [2872] by tassi
Fix list of distributed files so that the debian package can be built
5:34 PM Changeset [2871] by tranquil
op2 evaluation on beval's rendered oblivious to carry bit when …
4:26 PM Changeset [2870] by sacerdot
Proof fixed.
3:40 PM Changeset [2869] by tranquil
some reorganization of definitions, and a new taaf_append_taaf
12:04 AM Changeset [2868] by sacerdot
Pretty printing of ERTL and ERTLptr code.

Mar 13, 2013:

11:12 PM Changeset [2867] by sacerdot
New extraction after indianess bug fixes by Paolo.
4:21 PM Changeset [2866] by tranquil
corrected two bugs of the translation: constant translation used wrong …
2:38 PM Changeset [2865] by sacerdot
2:27 PM Changeset [2864] by sacerdot
I must have drunk yesterday: all RTL passes are printed correctly; the …
2:22 PM Changeset [2863] by piccolo
Added new invariant to good_if Generalized version of cond case for …
2:07 PM Changeset [2862] by sacerdot
Repaired, a reverse was enough.
1:15 PM Changeset [2861] by mckinna
PROVISIONAL commit: Unintentional list reversal cause final step of …
2:02 AM Changeset [2860] by sacerdot
RTL printing, core dumps ATM
1:19 AM Changeset [2859] by sacerdot
Pretty printing improved (now it always starts the visit from lbl 1).
12:52 AM Changeset [2858] by sacerdot
Trying to pretty print the code graph in visit order. Slightly bugged …

Mar 12, 2013:

8:03 PM Changeset [2857] by garnier
CL to CM: some invariants strengthened.
7:11 PM Changeset [2856] by sacerdot
Pretty printing of LTL almost finished.
6:51 PM Changeset [2855] by piccolo
little bug fixed in TranslateUtils?.
5:53 PM Changeset [2854] by sacerdot
Pretty printing of the LTL program.
5:53 PM Changeset [2853] by sacerdot
Pretty printing of line/label numbers.
4:37 PM Changeset [2852] by mckinna
Interim commit to re-establish well-typedness after all the recent …
4:13 PM Changeset [2851] by piccolo
partial commit
3:54 PM Changeset [2850] by garnier
Progress on CL to CM. Some more cases closed modulo some critical …
1:41 PM Changeset [2849] by piccolo
partial commit
10:56 AM Changeset [2848] by sacerdot
The pretty printer for LTL.
10:20 AM Changeset [2847] by sacerdot
2:28 AM Changeset [2846] by sacerdot
Pretty printing of joint programs.

Mar 11, 2013:

6:50 PM Changeset [2845] by piccolo
ERTLptr to LTL correctness proof started
1:28 PM Changeset [2844] by piccolo
Stupid bug fixed
1:02 PM Changeset [2843] by piccolo
1) Fixed a litte bug in Joint.ma 2) ERTL to ERTLptr correctness proof …
12:41 PM Changeset [2842] by sacerdot
The compiler can now show all back-end traces too (assembly and object …
12:40 PM Changeset [2841] by sacerdot
The compiler now computes also the stack cost for every intermediate …
12:18 PM Changeset [2840] by campbell
Remove irrelevant stuff from RTLabs_partial_traces
12:18 PM Changeset [2839] by campbell
Basic structure of RTLabs measurable to structured traces results.

Mar 10, 2013:

1:21 PM Changeset [2838] by garnier
Closing some more cases

Mar 9, 2013:

12:19 PM Changeset [2837] by tranquil
* filled in evaluation of LTL/LIN's extended instrucitons

Mar 8, 2013:

11:55 PM Changeset [2836] by sacerdot
11:54 PM Changeset [2835] by sacerdot
Included Uses.ma which is required by the untrusted code. The …
11:45 PM Changeset [2834] by sacerdot
Execution integrated in the compiler, as it was in the prototype. …
11:40 PM Changeset [2833] by sacerdot
11:40 PM Changeset [2832] by sacerdot
Added abstraction in front of cases daemon for code extraction.
11:38 PM Changeset [2831] by sacerdot
11:37 PM Changeset [2830] by sacerdot
Added abstractions in front of cases daemon for code extraction.
11:18 PM Changeset [2829] by sacerdot
Semantics files committed.
11:17 PM Changeset [2828] by sacerdot
1. New semantics.ma file that puts together all semantics. It …
9:07 PM Changeset [2827] by sacerdot
Everything extracted again.
9:07 PM Changeset [2826] by sacerdot
New error messages.
8:36 PM Changeset [2825] by garnier
Progress, Clight to Cminor
5:37 PM Changeset [2824] by tranquil
* moved sum on lists notation to extranat * used sum on lists to …
3:51 PM Changeset [2823] by tranquil
* corrected bug in ERTL semantics (both delframe and newframe did the …
12:48 PM Changeset [2822] by garnier
A consitent proof state for Clight to Cminor, with some progress (and …
11:44 AM Changeset [2821] by tranquil
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
12:26 AM Changeset [2820] by sacerdot
Proof obligation closed.
12:14 AM Changeset [2819] by sacerdot
Proof obligation closed.

Mar 7, 2013:

11:43 PM Changeset [2818] by sacerdot
"Repaired", using non computational daemons.
10:31 PM Changeset [2817] by sacerdot
Repaired after Paolo's commit.
10:20 PM Changeset [2816] by sacerdot
Repaired after Paolo's commit.
9:41 PM Changeset [2815] by sacerdot
exec superseded by exec_all
9:39 PM Changeset [2814] by sacerdot
frontend superseded by execute_all
9:34 PM Changeset [2813] by sacerdot
RTLabs now printed too
9:23 PM Changeset [2812] by sacerdot
Pre-classified system for RTLabs.
9:22 PM Changeset [2811] by sacerdot
Pre-classified system for RTLabs.
6:36 PM Changeset [2810] by sacerdot
Cminor semantics exported.
6:33 PM Changeset [2809] by sacerdot
6:03 PM Changeset [2808] by tranquil
added local_stacksize to joint internal functions to accomodate for …
5:43 PM Changeset [2807] by mckinna
Yet another ErrorMessage? Removed corresponding axiom in …
2:51 PM Changeset [2806] by tranquil
new b_graph_translate obligations
2:01 PM Changeset [2805] by sacerdot
Now also prints the trace for the labelled Clight.
1:55 PM Changeset [2804] by sacerdot
New executable exec_all. It contains a function to run and print all …
1:54 PM Changeset [2803] by sacerdot
More code extracted, used to debug the compiler.
1:53 PM Changeset [2802] by sacerdot
New file Clight_classified_system with the classified system for …
1:29 PM Changeset [2801] by piccolo
Partial commit not yet finished
1:07 PM Changeset [2800] by campbell
Tidy up Measurable.ma a little, get rid of obsolete comments.
1:04 PM Changeset [2799] by tranquil
* added taaf_to_taa, conversion from trace_any_any_free to …
12:56 PM Changeset [2798] by sacerdot
New error message.
12:55 PM Changeset [2797] by sacerdot
Extracted again after James's cleanup and the implementation of the …
12:10 PM Changeset [2796] by tranquil
* added global notation for existence in Type[1] (\exists[1] x.P) * in …
9:31 AM Changeset [2795] by sacerdot
Added new function Measurable.observe_all_in_measurable to be used to …
7:47 AM Changeset [2794] by mckinna
Minor tweaks/tidying up

Mar 6, 2013:

7:23 PM Changeset [2793] by campbell
Oops, gave fields wrong order during initialisation.
4:50 PM Changeset [2792] by campbell
Make instrumented output a little easier to read.
4:50 PM Changeset [2791] by campbell
Remove dead code in driver.
3:48 PM Changeset [2790] by campbell
Some null handling in conversion from CIL.
3:48 PM Changeset [2789] by campbell
Some changes to the driver to aid debugging.
3:48 PM Changeset [2788] by campbell
Report compiler error
3:48 PM Changeset [2787] by campbell
Output stack costs in driver.
2:59 PM Changeset [2786] by piccolo
Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
2:58 PM Changeset [2785] by piccolo
Traces.ma repaired
2:35 PM Changeset [2784] by sacerdot
Repaired after Mauro's commit.
12:09 PM Changeset [2783] by piccolo
modified joint_closed_internal_function definition (added condition on …
3:03 AM Changeset [2782] by sacerdot
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
3:00 AM Changeset [2781] by sacerdot
One more computational daemon closed.
2:59 AM Changeset [2780] by sacerdot
Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …

Mar 5, 2013:

11:50 PM Changeset [2779] by sacerdot
1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
11:34 PM Changeset [2778] by sacerdot
Code to pretty-print the IntelHex? output. At the moment the glue code …
10:03 PM Changeset [2777] by sacerdot
One computational daemon closed.
9:53 PM Changeset [2776] by sacerdot
The compiler now extracts also the stack cost model.
9:52 PM Changeset [2775] by sacerdot
The compiler now computes also the stack cost model.
6:15 PM Changeset [2774] by sacerdot
1. the compiler now outputs both the stack cost model and the max …

Mar 4, 2013:

10:03 AM Changeset [2773] by sacerdot
1. everything extracted again after all bugs in Matita's extraction …
9:55 AM Changeset [2772] by sacerdot
Useless code removed.

Mar 3, 2013:

11:46 PM Changeset [2771] by sacerdot
Some speed up in Policy.ma.
9:58 PM Changeset [2770] by mckinna
WARNING: another big commit, touching many files in ASM/*.ma This …
2:59 PM Changeset [2769] by mckinna
Mistakenly commented out both as_cost_get_label (needed; OK) as well …
2:44 PM Changeset [2768] by mckinna
Nightmare: file no longer typechecks, because defn as_cost_get_labels …
2:03 PM Changeset [2767] by mckinna
WARNING: BIG commit, which pushes code_size_opt check into …
10:39 AM Changeset [2766] by mckinna
pruned redundant dependency on Clight/Cexec?.ma
12:23 AM Changeset [2765] by sacerdot
1. correctness.ma repaired 2. we used the OC_preclassified_system to …

Mar 2, 2013:

11:59 PM Changeset [2764] by sacerdot
preclassified_system for object code
11:42 AM Changeset [2763] by sacerdot
All daemons in compiler.ma closed (i.e. proof obligations added to the …
2:37 AM Changeset [2762] by sacerdot
All repaired up to compiler.ma. Note: one daemon is left for one …
1:50 AM Changeset [2761] by sacerdot
Unused (but not useless) code commented out.
1:29 AM Changeset [2760] by sacerdot
1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …

Mar 1, 2013:

7:56 PM Changeset [2759] by campbell
Print out costs, with choice of style. Note small anti-assertion patch …
7:55 PM Changeset [2758] by campbell
Adapt prototype's Clight printer. Doesn't use cost map yet.
7:13 PM Changeset [2757] by tranquil
many things are still broken, but there is a partial backtrack on …
1:05 PM Changeset [2756] by sacerdot
WARNING: this commit breaks things, sorry, Paolo is going to fix …
11:06 AM Changeset [2755] by tranquil
* changed primitives of abstract status (with stuf that is probably …
10:26 AM Changeset [2754] by sacerdot
1. WARNING: I commented out one of James's function used in …

Feb 28, 2013:

5:56 PM Changeset [2753] by mckinna
Further tidying up thanks to Claudio's strong_decidable intervention; …
2:36 PM Changeset [2752] by mckinna
Fixed TODO regarding length of list_instr Added ASM/CodeMemory.ma to …
2:29 PM Changeset [2751] by mckinna
Added | AssemblyTooLarge? : ErrorMessage? to complete compiler.ma
2:27 PM Changeset [2750] by mckinna
Miscellany on 216 bounds, memory, lemmas+definitions. Completes …
2:12 PM Changeset [2749] by regisgia
* Updated version of the Frama-C plugin.
2:12 PM Changeset [2748] by regisgia
* Remove the old version of the plugin.

Feb 27, 2013:

10:48 PM Changeset [2747] by sacerdot
The compiler (frontend + backend)
10:46 PM Changeset [2746] by sacerdot
1. debugging code in glue 2. updated version
10:46 PM Changeset [2745] by sacerdot
1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
10:45 PM Changeset [2744] by sacerdot
Build no longer fails.
9:27 PM Changeset [2743] by sacerdot
Latest version of the compiler, extracted with the latest version of …
5:42 PM Changeset [2742] by sacerdot
Untrusted register colouring fully branched.
5:16 PM Changeset [2741] by sacerdot
File used only by untrusted code. Implemented in Matita to exploit …
4:59 PM Changeset [2740] by sacerdot
Graph colouring terminated up to Uses that will be implemented in Matita.
4:37 PM Changeset [2739] by sacerdot
The graph colouring algorithm takes in input also the function.
2:03 PM Changeset [2738] by sacerdot
Porting the graph colouring stuff from the untrusted prototype to the …

Feb 26, 2013:

7:37 PM Changeset [2737] by garnier
Commit of current proof state for Clight to Cminor translation.
6:18 PM Changeset [2736] by sacerdot
Untrusted fixpoint computation branched in.
3:35 PM Changeset [2735] by campbell
Note about loose end in FEMeasurable.
3:31 PM Changeset [2734] by mckinna
yet another puzzling automation failure, in the repaired case: "" …

Feb 25, 2013:

11:04 PM Changeset [2733] by sacerdot
All axioms in set_adt implemented by hand.
11:03 PM Changeset [2732] by sacerdot
Unused code removed.
10:17 PM Changeset [2731] by sacerdot
Minimal set of axioms implemented to make the driver run.
9:54 PM Changeset [2730] by sacerdot
Exported again.
9:51 PM Changeset [2729] by sacerdot
More errors recognized
9:42 PM Changeset [2728] by sacerdot
listb.ma => listb_extra.ma for extraction
6:43 PM Changeset [2727] by campbell
Remove a couple of redundant hypotheses.
12:11 PM Changeset [2726] by campbell
Show max stack preserved in FEMeasurable.
11:45 AM Changeset [2725] by campbell
Add observables to FEMeasurable proof; fix silly typo.

Feb 24, 2013:

8:39 PM Changeset [2724] by campbell
Add RTLabs cost labelling checks to compiler.ma.
Note: See TracTimeline for information about the timeline view.