Timeline
Apr 16, 2013:
- 5:31 PM Changeset [3153] by
- More data.
- 2:46 PM Changeset [3152] by
- r
- 11:33 AM Changeset [3151] by
- More data flowing in.
- 11:30 AM Changeset [3150] by
- Integrated all data I received so far.
- 11:09 AM Changeset [3149] by
- More data from Roberto integrated.
- 11:00 AM Changeset [3148] by
- Infos by Roberto integrated.
Apr 15, 2013:
- 6:57 PM Changeset [3147] by
- More work on Part 4.
- 6:29 PM Changeset [3146] by
- Most of the "scientific" work required for Part4. I still need to …
- 4:31 PM Changeset [3145] by
- * removed sigma types from traces of intensional events * completed …
- 3:43 PM Changeset [3144] by
- Initial work on D1.3. Part 1 and Part 2 have been fixed already.
- 2:27 PM Changeset [3143] by
- More papers pulled into the report.
- 10:51 AM Changeset [3142] by
- Sketch out a bit more of 3.4.
Apr 12, 2013:
- 7:23 PM Changeset [3141] by
- Rephrase Tullio's contribution... more work needed?
- 7:22 PM Changeset [3140] by
- Diagram illustrating nested function calls in structured traces.
- 7:11 PM Changeset [3139] by
- English tweaks
- 7:03 PM Changeset [3138] by
- Sketch up-to-labelling bit.
- 6:53 PM Changeset [3137] by
- Tweaks
- 6:47 PM Changeset [3136] by
- Updates: form and content, incorporating comments from Brian, and from …
- 6:34 PM Changeset [3135] by
- Discussion with Kevin at HiPEAC workshop.
- 6:27 PM Changeset [3134] by
- Opps uncommitted edits!
- 6:18 PM Changeset [3133] by
- Underscores!
- 6:17 PM Changeset [3132] by
- 1st version of workshop s reports. Comments/amendments welcome!
- 6:10 PM Changeset [3131] by
- Add rest of correctness.
- 6:10 PM Changeset [3130] by
- Tweak diagram spacing.
- 6:10 PM Changeset [3129] by
- Right version of the diagram.
- 5:00 PM Changeset [3128] by
- Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
- 4:03 PM Changeset [3127] by
- report on general proof
- 1:00 AM Changeset [3126] by
- Splitted into empty report + "stand alone" paper. The paper needs to …
Apr 11, 2013:
- 7:10 PM Changeset [3125] by
- …
- 6:34 PM Changeset [3124] by
- …
- 6:22 PM Changeset [3123] by
- …
- 3:55 PM Changeset [3122] by
- …
- 3:08 PM Changeset [3121] by
- …
- 2:04 PM Changeset [3120] by
- …
Apr 10, 2013:
- 7:15 PM Changeset [3119] by
- …
- 6:45 PM Changeset [3118] by
- 1) finished return case in StatusSimulationHelper? 2) started to write …
- 6:25 PM Changeset [3117] by
- …
- 5:07 PM Changeset [3116] by
- …
- 1:28 PM Changeset [3115] by
- Clean up some left-over lemmas and move comment back into place.
- 9:48 AM Changeset [3114] by
- Some progress on pipelines/caches.
Apr 9, 2013:
- 7:00 PM Changeset [3113] by
- Some work on control flow analysis.
- 6:05 PM Changeset [3112] by
- added invariant that costlabels are only assigned to NOPs (not proved …
- 6:05 PM Changeset [3111] by
- Skeleton
- 6:02 PM Changeset [3110] by
- …
- 5:28 PM Changeset [3109] by
- New version.
Apr 8, 2013:
- 11:50 PM Changeset [3108] by
- Towards D5.2.
- 1:17 PM Changeset [3107] by
- * External tools to compile the plugin.
Apr 6, 2013:
- 7:35 PM Changeset [3106] by
- New extraction.
- 6:38 PM Changeset [3105] by
- Pretty printing changed. There is still an inefficiency left: activate …
- 6:37 PM Changeset [3104] by
- Performance improvement.
- 4:19 PM Changeset [3103] by
- Simplified "include" dependencies
- 4:11 PM Changeset [3102] by
- Removed redundant refs to current_instruction0, which itself has been …
- 4:08 PM Changeset [3101] by
- Removed redundant lemma execute_1_technical, which is covered by …
- 4:05 PM Changeset [3100] by
- Removed redundant defn of current_instruction0, which only appears in …
- 4:02 PM Changeset [3099] by
- Simplified preliminaries: inefficient_address_of_word_labels, and …
- 11:44 AM Changeset [3098] by
- Performance improvement.
Apr 5, 2013:
- 9:53 PM Changeset [3097] by
- Performance improvement in policy computation.
- 6:04 PM Changeset [3096] by
- preliminary work on closing correctness.ma
Apr 4, 2013:
- 9:53 PM Changeset [3095] by
- Some performance improvement: an heavy computation was done again and …
- 12:04 PM Changeset [3094] by
- Makefile with targets: byte opt clean
- 11:52 AM Changeset [3093] by
- Makefile replaces build, targets: byte, opt, clean
- 11:36 AM Changeset [3092] by
- No more references to Lustre stuff.
- 11:31 AM Changeset [3091] by
- …
- 11:26 AM Changeset [3090] by
- dist: take into account symlink
- 11:18 AM Changeset [3089] by
- Symbolic link to the cparser
- 11:16 AM Changeset [3088] by
- We now also generate the package for native code.
- 11:06 AM Changeset [3087] by
- script to build tarpall
- 10:53 AM Changeset [3086] by
- extracted is now in driver
- 10:46 AM Changeset [3085] by
- extracted directory moved into driver to make debian packages more …
- 10:19 AM Changeset [3084] by
- 9:58 AM Changeset [3083] by
- The cost and stack* variables are now initialized with the cost of …
- 9:31 AM Changeset [3082] by
- Tidying up: the long comment about preamble/renamed_symbols in the …
Apr 3, 2013:
- 5:54 PM Changeset [3081] by
- Tidy up recent work a little.
- 5:27 PM Changeset [3080] by
- New extraction.
- 5:03 PM Changeset [3079] by
- added printing of ERTL, LTL and LIN's ext_seq's.
- 3:01 PM Changeset [3078] by
- fixed change of Mov
- 11:49 AM Changeset [3077] by
- New extraction.
- 10:13 AM Changeset [3076] by
- simplified include dependencies
Apr 2, 2013:
- 7:59 PM Changeset [3075] by
- Apologies for late folding in of old changes which were left over from …
- 7:25 PM Changeset [3074] by
- Put some kind of high level proof in for front-end.
- 6:44 PM Changeset [3073] by
- New extraction, all tests pass.
- 6:39 PM Changeset [3072] by
- corrected a bug (translate_store was wrong)
- 4:49 PM Changeset [3071] by
- …
- 4:49 PM Changeset [3070] by
- Ext case of RTL implemented.
- 2:09 PM Changeset [3069] by
- New extraction.
- 1:51 PM Changeset [3068] by
- Debugging code removed.
- 1:49 PM Changeset [3067] by
- New test that fails too.
- 1:48 PM Changeset [3066] by
- * implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
- 1:37 PM Changeset [3065] by
- Efficiency of semantics of assembled improved: ticks_of was …
- 1:02 PM Changeset [3064] by
- Efficiency of the semantics of assembly improved by avoiding the …
- 12:16 PM Changeset [3063] by
- Remove measure function from FEMeasurable because we're not using it …
- 11:59 AM Changeset [3062] by
- Bug fixed in the semantics of Mov: the offset was ignored. Now all …
- 11:32 AM Changeset [3061] by
- New extraction.
- 11:11 AM Changeset [3060] by
- Bug fixed in the semantics of JMP. The bug was due to a bug in the …
- 1:25 AM Changeset [3059] by
- New extraction
Apr 1, 2013:
- 9:14 PM Changeset [3058] by
- …
- 9:14 PM Changeset [3057] by
- lookup of function identifiers was not corrected with sigma
- 7:17 PM Changeset [3056] by
- fixed a merge gone wrong
- 7:04 PM Changeset [3055] by
- Start getting partial Clight to Cminor proof in shape for …
- 7:04 PM Changeset [3054] by
- Put missing typ check in; adjust proof because I did it a little …
- 7:04 PM Changeset [3053] by
- Cast simplification preserves measurable subtraces.
- 6:31 PM Changeset [3052] by
- …
- 6:28 PM Changeset [3051] by
- fixed order of global initialization in LINToASM. For the moment …
- 5:18 PM Changeset [3050] by
- 1) Added general commutation theorem for monads. 2) Added some …
- 12:06 AM Changeset [3049] by
- Globalenvs and initial states for cast simplification.
- 12:06 AM Changeset [3048] by
- Improve dependency for cast simplification.
Mar 31, 2013:
- 10:01 PM Changeset [3047] by
- Switch removal and labelling combined.
Mar 30, 2013:
- 1:11 AM Changeset [3046] by
- Main part of combined switch removal and labelling proof.
Mar 29, 2013:
- 10:15 PM Changeset [3045] by
- fixed what made test3 fail. However it involves a different notion of …
- 8:16 PM Changeset [3044] by
- Start showing combination of switch removal and labelling is OK. Fix …
- 6:38 PM Changeset [3043] by
- New major extraction that should have solved all remaining issues. As …
- 6:27 PM Changeset [3042] by
- Repaired.
- 6:18 PM Changeset [3041] by
- Repaired
- 5:51 PM Changeset [3040] by
- fixed LINToASM
- 5:45 PM Changeset [3039] by
- * merged and extended MovSuccessor? and Mov in one instruction (Mov dst …
- 5:27 PM Changeset [3038] by
- Bug fixed: the stack_cost* variables must be declared before the …
- 5:19 PM Changeset [3037] by
- * ADDRESS joint instruction now has also an offset * corrected call to …
- 5:12 PM Changeset [3036] by
- Fixing some problems, progress, etc
- 3:21 PM Changeset [3035] by
- Tweak: tidied up ?/\ldots Conceptual: better monadic threading of …
- 2:39 PM Changeset [3034] by
- Bug fixed: COST instructions are now assembled as NOP to prevent the …
- 12:53 PM Changeset [3033] by
- Bug fixed: sign_extension was extending according to the _second_ bit, …
- 12:51 PM Changeset [3032] by
- Remind myself why ms_rel_normal is reasonable.
- 12:38 PM Changeset [3031] by
- Tidy up RTLabs preclassified_system definitions.
- 12:09 PM Changeset [3030] by
- Break up front-end for correctness proof. Use let rec to prevent …
- 9:47 AM Changeset [3029] by
- New extraction after DPH/DPL bug fixing.
- 9:42 AM Changeset [3028] by
- Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
- 12:03 AM Changeset [3027] by
- Another output used by the plug-in.
Mar 28, 2013:
- 11:58 PM Changeset [3026] by
- With -a we now produce also the .cerco file required by the plug-in.
- 11:21 PM Changeset [3025] by
- 1. two syntax errors in instrumented files fixed 2. the compiler now …
- 10:53 PM Changeset [3024] by
- Bug fixed: set_flags was ignoring the cy and ov flags.
- 9:58 PM Changeset [3023] by
- Typo fixed. It made all GOTOs jump to random positions in the ASM code.
- 7:49 PM Changeset [3022] by
- Make a couple of tests monadic for easier inversion.
- 7:11 PM Changeset [3021] by
- Replace clight_clock_after with a more sensible definition that uses …
- 5:28 PM Changeset [3020] by
- - Options not used removed from the help/interface. - More compliance …
- 5:27 PM Changeset [3019] by
- New extraction after ERTLptr abortion.
- 5:27 PM Changeset [3018] by
- 1) some files repaired 2) all stuff related to the aborted pass …
- 5:05 PM Changeset [3017] by
- Repaired.
- 5:04 PM Changeset [3016] by
- fixed after previous commit
- 4:58 PM Changeset [3015] by
- Comment removed
- 4:58 PM Changeset [3014] by
- ERTL to ERTLptr pass suppressed (it introduced a bug in the later …
- 4:56 PM Changeset [3013] by
- Temporary parsing files removed.
- 3:51 PM Changeset [3012] by
- Debugging code removed after bug fixing.
- 3:47 PM Changeset [3011] by
- New extraction.
- 3:46 PM Changeset [3010] by
- same bug as was in liveness is now fixed
- 3:09 PM Changeset [3009] by
- New extraction.
- 3:07 PM Changeset [3008] by
- corrected bug where the address of pointer calls was not defined as used
- 2:59 PM Changeset [3007] by
- Sketch out how Cminor to RTLabs correctness would fit into the …
- 1:50 PM Changeset [3006] by
- New extraction, bugs fixed.
- 1:49 PM Changeset [3005] by
- Beginning of making it fully compatible with untrusted one.
- 1:48 PM Changeset [3004] by
- fixed a bug where when doing an asymetrical op, cast initialization …
- 1:08 PM Changeset [3003] by
- Correctness.ma "repaired"
- 1:05 PM Changeset [3002] by
- fixed previous commit
- 1:02 PM Changeset [3001] by
- New extraction.
- 1:01 PM Changeset [3000] by
- added RTLabs printer
- 12:47 PM Changeset [2999] by
- code_memory added to labelled_object_code to avoid recomputing it …
- 12:12 PM Changeset [2998] by
- Test on conditional execution. Fails atm.
- 10:27 AM Changeset [2997] by
- New extraction.
- 10:22 AM Changeset [2996] by
- Printing of graphs now starts from the entry point.
- 10:03 AM Changeset [2995] by
- The lIN_printer extracted.
- 10:02 AM Changeset [2994] by
- The LIN printer.
- 9:56 AM Changeset [2993] by
- 1. performance improved: the type inference was inferring …
- 12:07 AM Changeset [2992] by
- Add "only one return" invariant to RTLabs functions.
Mar 27, 2013:
- 9:57 PM Changeset [2991] by
- Fixed cond and seq case in StatusSimulationHelper? Added cost case in …
- 7:49 PM Changeset [2990] by
- Replace dodgy hypothesis by nice ones, clean up a little.
- 7:00 PM Changeset [2989] by
- Make front-end measurability preservation proof cope with moving the …
- 6:45 PM Changeset [2988] by
- Some easy tests.
- 6:32 PM Changeset [2987] by
- And again.. :(
- 6:32 PM Changeset [2986] by
- New extraction.
- 6:31 PM Changeset [2985] by
- Order of printing of lines in LIN fixed again, truly this time. But I …
- 6:17 PM Changeset [2984] by
- better LINToASM initialization of globals (to be tested!)
- 6:17 PM Changeset [2983] by
- LIN code was printed in reverse order. But I have not really …
- 6:05 PM Changeset [2982] by
- Pretty priting of LIN implemented.
- 4:53 PM Changeset [2981] by
- New extraction after code simplification.
- 4:50 PM Changeset [2980] by
- fixed b_graph_translate
- 4:34 PM Changeset [2979] by
- 1. LINToASM: new extraction (fix deletion backtracked) 2. …
- 4:33 PM Changeset [2978] by
- merged accidentally backtracked changes
- 4:09 PM Changeset [2977] by
- New extraction after several bug fixes.
- 4:09 PM Changeset [2976] by
- * a dangling trivial proof obligation is now closed
- 4:07 PM Changeset [2975] by
- * RTL premain fixed * fixed bug in back end ops (subtracting to a …
- 4:03 PM Changeset [2974] by
- New extraction.
- 1:11 PM Changeset [2973] by
- semanticUtils adapted to changes in TranslateUtils?
- 11:42 AM Changeset [2972] by
- Remove init from a testcase.
- 11:41 AM Changeset [2971] by
- Single RTLabs return statement.
Mar 26, 2013:
- 7:13 PM Changeset [2970] by
- now joint_if_entry can change when a preamble is added, so code points …
- 7:09 PM Changeset [2969] by
- Dead axiom removed :-)
- 7:07 PM Changeset [2968] by
- The initial status memory was not really initialized. Now it is.
- 6:54 PM Changeset [2967] by
- Semantics changed so that a terminating joint program that returns an …
- 6:35 PM Changeset [2966] by
- Modified by hand files (to improve a little bit the performance).
- 6:35 PM Changeset [2965] by
- Code performance improved a bit by hand.
- 6:33 PM Changeset [2964] by
- Debugging code removed.
- 6:32 PM Changeset [2963] by
- Bug fixed: the pre-main for the final code is now COST k1 …
- 5:36 PM Changeset [2962] by
- Most performant algorithm restored.
- 5:02 PM Changeset [2961] by
- Bug fixed (stupid typo in pre-main code made the compiler diverge on …
- 4:51 PM Changeset [2960] by
- New extraction, it diverges in RTL execution now.
- 4:46 PM Changeset [2959] by
- Typo
- 4:45 PM Changeset [2958] by
- Error message implemented.
- 4:41 PM Changeset [2957] by
- fixed semantics_blocks
- 4:31 PM Changeset [2956] by
- fixed LTL/LIN semantics
- 4:11 PM Changeset [2955] by
- corrected stupid typo
- 3:52 PM Changeset [2954] by
- resolved circular dependency for ERTLptr's semantics
- 3:34 PM Changeset [2953] by
- Fix silly label handling bug I realised was there during my talk…
- 2:01 PM Changeset [2952] by
- * corrected all back-end premains to not pass any arguments to the …
Mar 25, 2013:
- 11:30 PM Changeset [2951] by
- New extraction. Novely: a pre-main is used in the back-end. …
- 10:39 PM Changeset [2950] by
- linearise repaired (did I do the right thing???)
- 9:48 PM Changeset [2949] by
- Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
Mar 24, 2013:
- 9:17 PM Changeset [2948] by
- Finish up measurable to structured proof, exposing the prefix and …
- 9:17 PM Changeset [2947] by
- Init change in measurable to structured file.
- 11:29 AM Changeset [2946] by
- main novelties: * there is an in-built stack_usage nat in joint …
Mar 23, 2013:
- 8:43 AM Changeset [2945] by
- Minor tweak.
- 2:31 AM Changeset [2944] by
- Some progress.
- 2:07 AM Changeset [2943] by
- Mauro, I have put a daemon in place of the proof obligation that used …
- 1:37 AM Changeset [2942] by
- Many changes: 1. Coloured graphs are now specified in terms of …
Mar 22, 2013:
- 9:46 PM Changeset [2941] by
- Update proof slides.
- 7:16 PM Changeset [2940] by
- 1. StatusSimulationHelper? changed to allow to use status_rel that …
- 10:11 AM Changeset [2939] by
- Major problem: in order to accomodate the ERTLptrToLTL proof pass, the …
- 2:11 AM Changeset [2938] by
- 1. proof of "all eliminable are eliminable" completed 2. the notion of …
Mar 21, 2013:
- 9:45 PM Changeset [2937] by
- Speed up checking of RTLabs/CostInj.ma.
- 9:45 PM Changeset [2936] by
- Disable initialisation code generation in Cminor, propogate init data …
- 9:37 PM Changeset [2935] by
- separation of RTL semantics in three different versions, and …
- 8:34 PM Changeset [2934] by
- Patch to obtain more easily comparable traces.
- 8:11 PM Changeset [2933] by
- New extraction, several bug fixed. RTL_semantics fixed by hand, will …
- 7:58 PM Changeset [2932] by
- Same comment as previous commit on this file: the previous commit was …
- 7:31 PM Changeset [2931] by
- Partial back-track from Paolo's commit, that was partial.
- 7:14 PM Changeset [2930] by
- More progress. Some useless parameters have been removed from the …
- 7:13 PM Changeset [2929] by
- Bug fixed: the coercion mechanism made you think that the CALL case …
- 6:26 PM Changeset [2928] by
- some sketches about correctness proof
- 5:17 PM Changeset [2927] by
- stupid bug in bool_of_beval
- 4:06 PM Changeset [2926] by
- corrected bug in executing Sub
- 3:39 PM Changeset [2925] by
- corrected bug in toggle_bool
- 8:39 AM Changeset [2924] by
- Make calls to a known identifier actually use a direct call.
- 8:38 AM Changeset [2923] by
- Remove some leftovers.
- 2:12 AM Changeset [2922] by
- Progress: proof of "eliminable statements can be eliminated" almost …
- 12:56 AM Changeset [2921] by
- Extracted again.
- 12:53 AM Changeset [2920] by
- dos2unix-ed
Mar 20, 2013:
- 7:21 PM Changeset [2919] by
- "MATITA_COMPONENTS=/path/to/matita/components/ make deps" outputs …
- 5:10 PM Changeset [2918] by
- erased stupid accidental paste at the start of file (happened when …
- 1:20 PM Changeset [2917] by
- made it so that a 0 offset does not generate adding ops when accessing …
- 12:33 PM Changeset [2916] by
- corrected yet another endianness bug in load and store
- 9:37 AM Changeset [2915] by
- Dead code removed.
- 8:39 AM Changeset [2914] by
- Use single definition for stack measurement.
- 12:24 AM Changeset [2913] by
- Bug corrected by hand. It will be corrected automatically by next …
- 12:21 AM Changeset [2912] by
- Ouch, another bug in the very same function. Fixed too, on an example …
- 12:12 AM Changeset [2911] by
- Bug fixed in the translation of casts.
Mar 19, 2013:
- 11:19 PM Changeset [2910] by
- Abstract statuses for ASM and OC completed. A simple test program can …
- 10:21 PM Changeset [2909] by
- New extraction.
- 8:00 PM Changeset [2908] by
- Bug fixed by hand, they will be fixed automatically by the new extraction.
- 7:48 PM Changeset [2907] by
- 1. a few bugs fixed 2. as_return implemented for ASM & OC
- 9:54 AM Changeset [2906] by
- Bug fixed.
- 8:42 AM Changeset [2905] by
- Semantics of ASM in place (up to return values and function call …
- 1:27 AM Changeset [2904] by
- 1. Algorithm modified by hand to make it run faster. The trusted …
- 1:25 AM Changeset [2903] by
- Extracted again.
- 1:24 AM Changeset [2902] by
- Quick hack to allow printing of OC code. It will be automatically …
- 1:22 AM Changeset [2901] by
- 1. backendPrinter renamed to printer 2. Clight printing branched into …
- 1:20 AM Changeset [2900] by
- Flushing to understand where it is slow.
- 12:33 AM Changeset [2899] by
- 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
Mar 18, 2013:
- 10:03 AM Changeset [2898] by
- 1) simplification of cond and seq case for StatusSimulationHelper? …
Note: See TracTimeline
for information about the timeline view.
