Changeset 2449


Ignore:
Timestamp:
Nov 9, 2012, 6:01:01 PM (7 years ago)
Author:
garnier
Message:

Documentation added.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2448 r2449  
    27022702
    27032703
    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
    27052766theorem switch_removal_correction :
    27062767  ∀ge,ge'.
Note: See TracChangeset for help on using the changeset viewer.