Changeset 2449 for src/Clight/switchRemoval.ma
 Timestamp:
 Nov 9, 2012, 6:01:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2448 r2449 2702 2702 2703 2703 2704 (* Main theorem. To be ported and completed to memory injections. TODO *) 2704 (* Main theorem. 2705 9th November 2012 2706 We decided to interrupt the development of this particular proof. What follows is a description of what 2707 has to be done in order to finish it. 2708 2709 What has been done up to now is the simulation proof for all "easy" cases, that do not interact with the 2710 switch removal per se, plus a bit of switch. This still implies propagating the memory extension through 2711 each statement (except switch), as well as various invariants that are needed for the switch case. 2712 2713 The proof for the switch case has been started. Here is how I picture the simulation proof. 2714 The simulation proof must be broken down in several steps. The source statement executes as this for the first step : 2715 2716 mem, env, k 2717  2718 switch(e) case_list ===> 2719 e ⇓ Vint i, 2720 case_list' ← select_switch sz n case_list; 2721 Result = State (seq_of_labeled_statement case_list') (Kswitch k) env mem 2722 2723 The resulting statement executes like this. 2724 2725 mem ⊕ writeable, env ⊕ ext, k' 2726 fresh ∈ dom(ext) 2727 ext(fresh) ∈ writeable 2728  2729 fresh = e; 2730 if(e == case0) {  2731 substatement0;  2732 goto next0;  2733 } else { };  2734 if(e == case1) {  = converted_cases 2735 label next0:  2736 substatement1;  2737 goto next1;  2738 } else { };  2739 ... ===> 2740 Result = State (fresh = e) (Kseq converted_cases k) (env ⊕ ext) (mem ⊕ writeable) 2741 ===> 2742 fresh ⇓ Loc l; 2743 e ⇓ Vint i; 2744 m' → store_value_of_type' (typeof a1) m l (Vint i) 2745 Result = State Sskip (Kseq converted_cases k) (env ⊕ ext) (m' ⊕ writeable) 2746 ===> 2747 Result = State converted_cases k (env ⊕ ext) (m' ⊕ writeable) 2748 This has been done. But this state is still not equivalent with the source one. 2749 TODO 1: we must prove that after a finite number of Ssequence in [converted_cases], we 2750 stumble upon a "if(e == casen) { blahblah } else {}; foo" that corresponds to "(seq_of_labeled_statement case_list')" 2751 (remember that "case_list'" has been truncated to the case corresponding to "i"). 2752 TODO 2: the resulting pair of states will not be in the standard simulation relation currently defined in 2753 [switch_state_sim]. We must come up with an additional set of relations with enough informations 2754 to handle the gotos : 2755 1. the gotos from one if to the other avoiding the execution of conditions 2756 2. most importantly, the gotos into which "break"s have been converted ! 2757 This particular subset of the simulation will need some equations allowing to prove that 2758 the current continuation actually contains a label corresponding to the break. 2759 Note that when encountering e.g. a while loop inside a converted case, breaks should stop 2760 beeing converted to gotos and we should go to the 'standard' simulation relation. 2761 TODO 3: some standard cases remain after that, nothing special (halt case ...). 2762 2763 This should be about it. TODO 1 and 2 will probably require some form of induction over switch cases ... 2764 *) 2765 2705 2766 theorem switch_removal_correction : 2706 2767 ∀ge,ge'.
Note: See TracChangeset
for help on using the changeset viewer.