Ignore:
Timestamp:
Apr 15, 2011, 4:26:23 PM (9 years ago)
Author:
campbell
Message:

An experimental branch of the Cminor semantics.

Location:
Deliverables/D3.3
Files:
2 added
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/Cminor-experiment/semantics.ma

    r754 r755  
    1111definition genv ≝ (genv_t Genv) (fundef internal_function).
    1212
    13 inductive cont : Type[0] ≝
    14 | Kstop : cont
    15 | Kseq : stmt → cont → cont
    16 | Kblock : cont → cont
    17 | Kcall : option ident → internal_function → block (* sp *) → env → cont → cont.
     13inductive cont : nat → Type[0] ≝
     14| Kstop : cont O
     15| Kseq : ∀n. stmt n → cont n → cont n
     16| Kblock : ∀n. cont n → cont (S n)
     17| Kcall : option ident → internal_function → block (* sp *) → env → ∀n. cont n → cont O.
    1818
    1919inductive state : Type[0] ≝
    2020| State:
    2121    ∀    f: internal_function.
    22     ∀    s: stmt.
     22    ∀    n: nat.
     23    ∀    s: stmt n.
    2324    ∀   en: env.
    2425    ∀    m: mem.
    2526    ∀   sp: block.
    26     ∀    k: cont.
     27    ∀    k: cont n.
    2728            state
    2829| Callstate:
     
    3031    ∀ args: list val.
    3132    ∀    m: mem.
    32     ∀    k: cont.
     33    ∀    k: cont O.
    3334            state
    3435| Returnstate:
    3536    ∀    v: option val.
    3637    ∀    m: mem.
    37     ∀    k: cont.
     38    ∀    k: cont O.
    3839            state.
    3940
    4041definition mem_of_state : state → mem ≝
    4142λst. match st with
    42 [ State _ _ _ m _ _ ⇒ m
     43[ State _ _ _ _ m _ _ ⇒ m
    4344| Callstate _ _ m _ ⇒ m
    4445| Returnstate _ m _ ⇒ m
     
    7677].
    7778
    78 let rec k_exit (n:nat) (k:cont) on k : res cont ≝
    79 match k with
    80 [ Kstop ⇒ Error ?
    81 | Kseq _ k' ⇒ k_exit n k'
    82 | Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
    83 | Kcall _ _ _ _ _ ⇒ Error ?
    84 ].
     79let rec k_exit (n:nat) (m:Fin n) (k:cont n) on k : Sig nat cont ≝
     80(match k return λx.λ_.Fin x → Sig nat cont with
     81[ Kstop ⇒ λm.?
     82| Kseq n' _ k' ⇒ λm. k_exit ? m k'
     83| Kblock n' k' ⇒ λm.match m return λx.λ_.match x with [ O ⇒ True | S y ⇒ (Fin y → Sig nat cont) → Sig nat cont ] with [ FO _ ⇒ λ_.dp ??? k' | FS n' m' ⇒ λr.r m' ] (λm'. k_exit ? m' k')
     84| Kcall _ _ _ _ _ _ ⇒ λm.?
     85]) m.
     86@(match m return λx.λ_.match x return λ_.Type[0] with [ O ⇒ Sig nat cont | S _ ⇒ True] with [ FO x ⇒ I | FS x y ⇒ I ])
     87qed.
     88
    8589
    8690let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
     
    9296].
    9397
    94 let rec call_cont (k:cont) : cont ≝
    95 match k with
    96 [ Kseq _ k' ⇒ call_cont k'
    97 | Kblock k' ⇒ call_cont k'
    98 | _ ⇒ k
    99 ].
    100 
    101 let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
    102 match s with
    103 [ St_seq s1 s2 ⇒
    104     match find_label l s1 (Kseq s2 k) with
    105     [ None ⇒ find_label l s2 k
     98let rec call_cont (n:nat) (k:cont n) on k : cont O ≝
     99match k return λ_.λ_.cont O with
     100[ Kseq _ _ k' ⇒ call_cont ? k'
     101| Kblock _ k' ⇒ call_cont ? k'
     102| Kstop ⇒ Kstop
     103| Kcall a b c d e f ⇒ Kcall a b c d e f
     104].
     105
     106let rec find_label (l:ident) (n:nat) (s:stmt n) (k:cont n) on s : option (Sig nat (λn.stmt n × (cont n))) ≝
     107(match s with
     108[ St_seq _ s1 s2 ⇒ λk.
     109    match find_label l ? s1 (Kseq ? s2 k) with
     110    [ None ⇒ find_label l ? s2 k
    106111    | Some sk ⇒ Some ? sk
    107112    ]
    108 | St_ifthenelse _ s1 s2 ⇒
    109     match find_label l s1 k with
    110     [ None ⇒ find_label l s2 k
     113| St_ifthenelse _ _ s1 s2 ⇒ λk.
     114    match find_label l ? s1 k with
     115    [ None ⇒ find_label l ? s2 k
    111116    | Some sk ⇒ Some ? sk
    112117    ]
    113 | St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k)
    114 | St_block s' ⇒ find_label l s' (Kblock k)
    115 | St_label l' s' ⇒
     118| St_loop _ s' ⇒ λk. find_label l ? s' (Kseq ? (St_loop ? s') k)
     119| St_block _ s' ⇒ λk. find_label l ? s' (Kblock ? k)
     120| St_label l' _ s' ⇒ λk.
    116121    match ident_eq l l' with
    117     [ inl _ ⇒ Some ? 〈s',k〉
    118     | inr _ ⇒ find_label l s' k
    119     ]
    120 | St_cost _ s' ⇒ find_label l s' k
    121 | _ ⇒ None ?
    122 ].
     122    [ inl _ ⇒ Some ? (dp … 〈s',k〉)
     123    | inr _ ⇒ find_label l ? s' k
     124    ]
     125| St_cost _ _ s' ⇒ λk. find_label l ? s' k
     126| _ ⇒ λk. None ?
     127]) k.
    123128
    124129let rec bind_params (vs:list val) (ids:list ident) : res env ≝
     
    137142λge,st.
    138143match st with
    139 [ State f s en m sp k ⇒
    140     match s with
    141     [ St_skip
     144[ State f n0 s en m sp k ⇒
     145    (match s return λx.λ_. cont x → IO io_out io_in (trace × state) with
     146    [ St_skip n ⇒ λk.
    142147        match k with
    143148        [ Kstop ⇒ Wrong ???
    144         | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
    145         | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
     149        | Kseq n' s' k' ⇒ ret ? 〈E0, State f n' s' en m sp k'〉
     150        | Kblock n' k' ⇒ ret ? 〈E0, State f n' (St_skip ?) en m sp k'〉
    146151          (* cminor allows functions without an explicit return statement *)
    147         | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k
    148         ]
    149     | St_assign id e
     152        | Kcall a b c d e f ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (Kcall a b c d e f)
     153        ]
     154    | St_assign id e n ⇒ λk.
    150155        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    151         ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉
    152     | St_store chunk edst e
     156        ret ? 〈tr, State f n (St_skip ?) (add ?? en id v) m sp k〉
     157    | St_store chunk edst e n ⇒ λk.
    153158        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
    154159        ! 〈tr',v〉 ← eval_expr ge e en sp m;
    155160        ! m' ← opt_to_res … (storev chunk m vdst v);
    156         ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    157 
    158     | St_call dst ef args sig (* XXX sig unused? *)
     161        ret ? 〈tr ⧺ tr', State f n (St_skip ?) en m' sp k〉
     162
     163    | St_call dst ef args sig n ⇒ λk. (* XXX sig unused? *)
    159164        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    160165        ! fd ← opt_to_res … (find_funct ?? ge vf);
    161166        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    162         ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    163     | St_tailcall ef args sig
     167        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en n k)〉
     168    | St_tailcall ef args sig n ⇒ λk.
    164169        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    165170        ! fd ← opt_to_res … (find_funct ?? ge vf);
    166171        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    167         ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) k
     172        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont ? k)
    168173       
    169     | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
    170     | St_ifthenelse e strue sfalse ⇒
     174    | St_seq n s1 s2 ⇒ λk. ret ? 〈E0, State f n s1 en m sp (Kseq ? s2 k)〉
     175    | St_ifthenelse e n strue sfalse ⇒ λk.
    171176        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    172177        ! b ← eval_bool_of_val v;
    173         ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
    174     | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉
    175     | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉
    176     | St_exit n ⇒
    177         ! k' ← k_exit n k;
    178         ret ? 〈E0, State f St_skip en m sp k'〉
    179     | St_switch e cs default ⇒
     178        ret ? 〈tr, State f n (if b then strue else sfalse) en m sp k〉
     179    | St_loop n s ⇒ λk. ret ? 〈E0, State f n s en m sp (Kseq ? (St_loop ? s) k)〉
     180    | St_block n s ⇒ λk. ret ? 〈E0, State f ? s en m sp (Kblock ? k)〉
     181    | St_exit n x ⇒ λk.
     182        match k_exit n x k with
     183        [ dp n' k' ⇒
     184            ret ? 〈E0, State f ? (St_skip ?) en m sp k'〉
     185        ]
     186    | St_switch e n cs default ⇒ λk.
    180187        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    181188        match v with
    182189        [ Vint i ⇒
    183             ! k' ← k_exit (find_case ? i cs default) k;
    184             ret ? 〈tr, State f St_skip en m sp k'〉
     190            match k_exit ? (find_case ? i cs default) k with
     191            [ dp n k' ⇒
     192                ret ? 〈tr, State f n (St_skip ?) en m sp k'〉
     193            ]
    185194        | _ ⇒ Wrong ???
    186195        ]
    187     | St_return eo
     196    | St_return eo n ⇒ λk.
    188197        match eo with
    189         [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
     198        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont ? k)〉
    190199        | Some e ⇒
    191200            ! 〈tr,v〉 ← eval_expr ge e en sp m;
    192             ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
    193         ]
    194     | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
    195     | St_goto l ⇒
    196         ! 〈s', k'〉 ← opt_to_res … (find_label l (f_body f) (call_cont k));
    197         ret ? 〈E0, State f s' en m sp k'〉
    198     | St_cost l s' ⇒
    199         ret ? 〈Echarge l, State f s' en m sp k〉
    200     ]
     201            ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont ? k)〉
     202        ]
     203    | St_label l n s' ⇒ λk. ret ? 〈E0, State f ? s' en m sp k〉
     204    | St_goto l n ⇒ λk.
     205        ! x ← opt_to_res … (find_label l ? (f_body f) (call_cont ? k));
     206        match x with [ dp n' x' ⇒ let 〈s', k'〉 ≝ x' in
     207          ret ? 〈E0, State f ? s' en m sp k'〉
     208        ]
     209    | St_cost l n s' ⇒ λk.
     210        ret ? 〈Echarge l, State f n s' en m sp k〉
     211    ]) k
    201212| Callstate fd args m k ⇒
    202213    match fd with
     
    204215        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    205216        ! en ← bind_params args (f_params f);
    206         ret ? 〈E0, State f (f_body f) en m' sp k〉
     217        ret ? 〈E0, State f O (f_body f) en m' sp k〉
    207218    | External fn ⇒
    208219        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     
    213224| Returnstate res m k ⇒
    214225    match k with
    215     [ Kcall dst f sp en k' ⇒
     226    [ Kcall dst f sp en n k' ⇒
    216227        ! en' ← match res with
    217228                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
     
    219230                                          | Some id ⇒ OK ? (add ?? en id v) ]
    220231                ];
    221         ret ? 〈E0, State f St_skip en' m sp k'〉
     232        ret ? 〈E0, State f n (St_skip ?) en' m sp k'〉
    222233    | _ ⇒ Wrong ???
    223234    ]
Note: See TracChangeset for help on using the changeset viewer.