Changeset 1135


Ignore:
Timestamp:
Aug 29, 2011, 5:45:04 PM (8 years ago)
Author:
campbell
Message:

Add invariants to Cminor semantics to rule out some failures.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r1102 r1135  
    1111definition genv ≝ (genv_t Genv) (fundef internal_function).
    1212
     13definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
     14  stmt_P (λs.stmt_vars (present ?? en) s ∧
     15             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.
     16
     17lemma stmt_inv_update : ∀f,en,s,l,v.
     18  stmt_inv f en s →
     19  ∀H:present ?? en l.
     20  stmt_inv f (update_present ?? en l H v) s.
     21#f #en #s #l #v #Inv #H
     22@(stmt_P_mp … Inv)
     23#s * #H1 #H2 %
     24[ @(stmt_vars_mp … H1)
     25  #l #H @update_still_present @H
     26| @H2
     27] qed.
     28
     29(* continuations within a function. *)
    1330inductive cont : Type[0] ≝
    14 | Kstop : cont
     31| Kend : cont
    1532| Kseq : stmt → cont → cont
    16 | Kblock : cont → cont
    17 | Kcall : option ident → internal_function → block (* sp *) → env → cont → cont.
     33| Kblock : cont → cont.
     34
     35let rec cont_inv (f:internal_function) (en:env) (k:cont) on k : Prop ≝
     36match k with
     37[ Kend ⇒ True
     38| Kseq s k' ⇒ stmt_inv f en s ∧ cont_inv f en k'
     39| Kblock k' ⇒ cont_inv f en k'
     40].
     41
     42lemma cont_inv_update : ∀f,en,k,l,v.
     43  cont_inv f en k →
     44  ∀H:present ?? en l.
     45  cont_inv f (update_present ?? en l H v) k.
     46#f #en #k elim k /2/
     47#s #k #IH #l #v #Inv #H whd %
     48[ @stmt_inv_update @(π1 Inv)
     49| @IH @(π2 Inv)
     50] qed.
     51
     52(* a stack of function calls *)
     53inductive stack : Type[0] ≝
     54| SStop : stack
     55| Scall : ∀dest:option ident. ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some id ⇒ present ?? en id] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
    1856
    1957inductive state : Type[0] ≝
     
    2260    ∀    s: stmt.
    2361    ∀   en: env.
     62    ∀ fInv: stmt_inv f en (f_body f).
     63    ∀  Inv: stmt_inv f en s.
    2464    ∀    m: mem.
    2565    ∀   sp: block.
    2666    ∀    k: cont.
     67    ∀ kInv: cont_inv f en k.
     68    ∀   st: stack.
    2769            state
    2870| Callstate:
     
    3072    ∀ args: list val.
    3173    ∀    m: mem.
    32     ∀    k: cont.
     74    ∀   st: stack.
    3375            state
    3476| Returnstate:
    3577    ∀    v: option val.
    3678    ∀    m: mem.
    37     ∀    k: cont.
     79    ∀   st: stack.
    3880            state.
    3981
    4082definition mem_of_state : state → mem ≝
    4183λst. match st with
    42 [ State _ _ _ m _ _ ⇒ m
     84[ State _ _ _ _ _ m _ _ _ _ ⇒ m
    4385| Callstate _ _ m _ ⇒ m
    4486| Returnstate _ m _ ⇒ m
     
    5092axiom FailedLoad : String.
    5193
    52 let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
    53 match e with
    54 [ Id _ i ⇒
    55     do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
     94let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (present ?? en)) (sp:block) (m:mem) on e : res (trace × val) ≝
     95match e return λt,e.expr_vars t e (present ?? en) → res (trace × val) with
     96[ Id _ i ⇒ λEnv.
     97    let r ≝ lookup_present ?? en i ? in
    5698    OK ? 〈E0, r〉
    57 | Cst _ c ⇒
     99| Cst _ c ⇒ λEnv.
    58100    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    59101    OK ? 〈E0, r〉
    60 | Op1 ty ty' op e' ⇒
    61     do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
     102| Op1 ty ty' op e' ⇒ λEnv.
     103    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    62104    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    63105    OK ? 〈tr, r〉
    64 | Op2 ty1 ty2 ty' op e1 e2 ⇒
    65     do 〈tr1,v1〉 ← eval_expr ge ? e1 en sp m;
    66     do 〈tr2,v2〉 ← eval_expr ge ? e2 en sp m;
     106| Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv.
     107    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
     108    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
    67109    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    68110    OK ? 〈tr1 ⧺ tr2, r〉
    69 | Mem rg ty chunk e ⇒
    70     do 〈tr,v〉 ← eval_expr ge ? e en sp m;
     111| Mem rg ty chunk e ⇒ λEnv.
     112    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    71113    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    72114    OK ? 〈tr, r〉
    73 | Cond sz sg ty e' e1 e2 ⇒
    74     do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
     115| Cond sz sg ty e' e1 e2 ⇒ λEnv.
     116    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    75117    do b ← eval_bool_of_val v;
    76     do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en sp m;
     118    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en ? sp m;
    77119    OK ? 〈tr ⧺ tr', r〉
    78 | Ecost ty l e' ⇒
    79     do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
     120| Ecost ty l e' ⇒ λEnv.
     121    do 〈tr,r〉 ← eval_expr ge ty e' en ? sp m;
    80122    OK ? 〈Echarge l ⧺ tr, r〉
    81 ].
     123] Env.
     124try @Env
     125try @(π1 Env)
     126try @(π2 Env)
     127try @(π1 (π1 Env))
     128cases b
     129try @(π2 (π1 Env))
     130try @(π2 Env)
     131qed.
    82132
    83133axiom BadState : String.
    84134
    85 let rec k_exit (n:nat) (k:cont) on k : res cont ≝
    86 match k with
    87 [ Kstop ⇒ Error ? (msg BadState)
    88 | Kseq _ k' ⇒ k_exit n k'
    89 | Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
    90 | Kcall _ _ _ _ _ ⇒ Error ? (msg BadState)
    91 ].
     135let rec k_exit (n:nat) (k:cont) f en (kInv:cont_inv f en k) on k : res (Σk':cont. cont_inv f en k') ≝
     136match k return λk.cont_inv f en k → ? with
     137[ Kend ⇒ λ_. Error ? (msg BadState)
     138| Kseq _ k' ⇒ λkInv. k_exit n k' f en ?
     139| Kblock k' ⇒ λkInv. match n with [ O ⇒ OK ? «k',?» | S m ⇒ k_exit m k' f en ? ]
     140] kInv.
     141[ @(π2 kInv) | @kInv | @kInv ]
     142qed.
    92143
    93144let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
     
    99150].
    100151
    101 let rec call_cont (k:cont) : cont ≝
    102 match k with
    103 [ Kseq _ k' ⇒ call_cont k'
    104 | Kblock k' ⇒ call_cont k'
    105 | _ ⇒ k
    106 ].
    107 
    108 let rec find_label (l:identifier Label) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
    109 match s with
    110 [ St_seq s1 s2 ⇒
    111     match find_label l s1 (Kseq s2 k) with
    112     [ None ⇒ find_label l s2 k
     152let rec find_label (l:identifier Label) (s:stmt) (k:cont) f en (Inv:stmt_inv f en s) (kInv:cont_inv f en k) on s : option (Σsk:(stmt × cont). stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk)) ≝
     153match s return λs. stmt_inv f en s → ? with
     154[ St_seq s1 s2 ⇒ λInv.
     155    match find_label l s1 (Kseq s2 k) f en ?? with
     156    [ None ⇒ find_label l s2 k f en ??
    113157    | Some sk ⇒ Some ? sk
    114158    ]
    115 | St_ifthenelse _ _ _ s1 s2 ⇒
    116     match find_label l s1 k with
    117     [ None ⇒ find_label l s2 k
     159| St_ifthenelse _ _ _ s1 s2 ⇒ λInv.
     160    match find_label l s1 k f en ?? with
     161    [ None ⇒ find_label l s2 k f en ??
    118162    | Some sk ⇒ Some ? sk
    119163    ]
    120 | St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k)
    121 | St_block s' ⇒ find_label l s' (Kblock k)
    122 | St_label l' s' ⇒
     164| St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
     165| St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
     166| St_label l' s' ⇒ λInv.
    123167    match identifier_eq ? l l' with
    124168    [ inl _ ⇒ Some ? 〈s',k〉
    125     | inr _ ⇒ find_label l s' k
    126     ]
    127 | St_cost _ s' ⇒ find_label l s' k
    128 | _ ⇒ None ?
    129 ].
     169    | inr _ ⇒ find_label l s' k f en ??
     170    ]
     171| St_cost _ s' ⇒ λInv. find_label l s' k f en ??
     172| _ ⇒ λ_. None ?
     173] Inv.
     174//
     175try @(π2 Inv)
     176try @(π2 (π1 Inv))
     177[ % [ @(π2 Inv) | @kInv ]
     178| % [ @Inv | @kInv ]
     179| % [ @(π2 Inv) | @kInv ]
     180] qed.
     181
     182lemma find_label_none : ∀l,s,k,f,en,Inv,kInv.
     183  find_label l s k f en Inv kInv = None ? →
     184  ¬Exists ? (λl'.l' = l) (labels_of s).
     185#l #s elim s
     186try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) )
     187[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     188  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
     189  cases (find_label l s1 (Kseq s2 k) f en ??)
     190  [ #H1 whd in ⊢ (??%? → ?)
     191    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
     192    [ #H2 #_ % #H cases (Exists_append … H)
     193      [ #H' cases (H1 (refl ??)) /2/
     194      | #H' cases (H2 (refl ??)) /2/
     195      ]
     196    | #sk #_ #E destruct
     197    ]
     198  | #sk #_ #E whd in E:(??%?); destruct
     199  ]
     200| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     201  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
     202  cases (find_label l s1 k f en ??)
     203  [ #H1 whd in ⊢ (??%? → ?)
     204    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
     205    [ #H2 #_ % #H cases (Exists_append … H)
     206      [ #H' cases (H1 (refl ??)) /2/
     207      | #H' cases (H2 (refl ??)) /2/
     208      ]
     209    | #sk #_ #E destruct
     210    ]
     211  | #sk #_ #E whd in E:(??%?); destruct
     212  ]
     213| #s1 #IH #k #f #en #Inv #kInv @IH
     214| #s1 #IH #k #f #en #Inv #kInv @IH
     215| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
     216  whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
     217| whd in i:(??%?); cases (identifier_eq Label l a) in i;
     218  whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
     219| #cl #s1 #IH #k #f #en #Inv #kInv @IH
     220] qed.
     221
     222definition find_label_always : ∀l,s,k. Exists ? (λl'.l' = l) (labels_of s) →
     223  ∀f,en. stmt_inv f en s → cont_inv f en k →
     224  Σsk:stmt × cont. stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk) ≝
     225λl,s,k,H,f,en,Inv,kInv.
     226  match find_label l s k f en Inv kInv return λx.find_label l s k f en Inv kInv = x → ? with
     227  [ Some sk ⇒ λ_. sk
     228  | None ⇒ λE. ⊥
     229  ] (refl ? (find_label l s k f en Inv kInv)).
     230cases (find_label_none … E)
     231#H1 @(H1 H)
     232qed.
    130233
    131234axiom WrongNumberOfParameters : String.
    132235
    133236(* TODO: perhaps should do a little type checking? *)
    134 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env
     237let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids)
    135238match vs with
    136 [ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
     239[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
    137240| cons v vt ⇒
    138     match ids with
     241    match ids return λids.res (Σen. All ?? ids) with
    139242    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    140243    | cons idh idt ⇒
    141244        let 〈id,ty〉 ≝ idh in
    142245        do en ← bind_params vt idt;
    143         OK ? (add ?? en id v)
    144     ]
    145 ].
     246        OK ? «add ?? en (\fst idh) v, ?»
     247    ]
     248].
     249[ @I
     250| % [ whd >lookup_add_hit % #E destruct
     251    | @(All_mp … (use_sig ?? en)) #a #H whd @lookup_add_oblivious @H
     252    ]
     253] qed.
    146254
    147255(* TODO: perhaps should do a little type checking? *)
    148256definition init_locals : env → list (ident×typ) → env ≝
    149257foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
     258
     259lemma init_locals_preserves : ∀en,vars,l.
     260  present ?? en l →
     261  present ?? (init_locals en vars) l.
     262#en #vars elim vars
     263[ #l #H @H
     264| #idt #tl #IH #l #H whd
     265  @lookup_add_oblivious @IH @H
     266] qed.
     267
     268lemma init_locals_env : ∀en,vars.
     269  All ? (λidt. present ?? (init_locals en vars) (\fst idt)) vars.
     270#en #vars elim vars
     271[ @I
     272| #idt #tl #IH %
     273  [ whd >lookup_add_hit % #E destruct
     274  | @(All_mp … IH) #a #H @lookup_add_oblivious @H
     275  ]
     276] qed.
     277
     278let rec trace_map_inv (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → res (trace × B))
     279                  (l:list A) (p:All A P l) on l : res (trace × (list B)) ≝
     280match l return λl. All A P l → ? with
     281[ nil ⇒ λ_. OK ? 〈E0, [ ]〉
     282| cons h t ⇒ λp.
     283    do 〈tr,h'〉 ← f h ?;
     284    do 〈tr',t'〉 ← trace_map_inv … f t ?;
     285    OK ? 〈tr ⧺ tr',h'::t'〉
     286] p.
     287[ @(π1 p) | @(π2 p) ] qed.
    150288
    151289axiom FailedStore : String.
     
    155293axiom ReturnMismatch : String.
    156294
     295lemma Exists_exists : ∀A,P,l.
     296  Exists A P l →
     297  ∃x. P x.
     298#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
     299qed.
     300
     301lemma Exists_All : ∀A,P,Q,l.
     302  Exists A P l →
     303  All A Q l →
     304  ∃x. P x ∧ Q x.
     305#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
     306qed.
     307
    157308definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    158309λge,st.
    159310match st with
    160 [ State f s en m sp k ⇒
    161     match s with
    162     [ St_skip ⇒
    163         match k with
    164         [ Kstop ⇒ Wrong ??? (msg BadState)
    165         | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
    166         | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
     311[ State f s en fInv Inv m sp k kInv st ⇒
     312    match s return λs. stmt_inv f en s → ? with
     313    [ St_skip ⇒ λInv.
     314        match k return λk. cont_inv f en k → ? with
     315        [ Kseq s' k' ⇒ λkInv. ret ? 〈E0, State f s' en fInv ? m sp k' ? st〉
     316        | Kblock k' ⇒ λkInv. ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    167317          (* cminor allows functions without an explicit return statement *)
    168         | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k
    169         ]
    170     | St_assign _ id e ⇒
    171         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    172         ! en' ← update ?? en id v;
    173         ret ? 〈tr, State f St_skip en' m sp k
    174     | St_store _ _ chunk edst e ⇒
    175         ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
    176         ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
     318        | Kend ⇒ λkInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st
     319        ] kInv
     320    | St_assign _ id e ⇒ λInv.
     321        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     322        let en' ≝ update_present ?? en id ? v in
     323        ret ? 〈tr, State f St_skip en' ? ? m sp k ? st
     324    | St_store _ _ chunk edst e ⇒ λInv.
     325        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
     326        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
    177327        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    178         ret ? 〈tr ⧺ tr', State f St_skip en m' sp k
    179 
    180     | St_call dst ef args ⇒
    181         ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
     328        ret ? 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st
     329
     330    | St_call dst ef args ⇒ λInv.
     331        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    182332        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    183         ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    184         ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    185     | St_tailcall ef args ⇒
    186         ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
     333        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     334        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     335    | St_tailcall ef args ⇒ λInv.
     336        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    187337        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    188         ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    189         ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)
     338        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     339        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st
    190340       
    191     | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)
    192     | St_ifthenelse _ _ e strue sfalse ⇒
    193         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     341    | St_seq s1 s2 ⇒ λInv. ret ? 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st
     342    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
     343        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    194344        ! b ← eval_bool_of_val v;
    195         ret ? 〈tr, State f (if b then strue else sfalse) en m sp k
    196     | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)
    197     | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)
    198     | St_exit n ⇒
    199         ! k' ← k_exit n k;
    200         ret ? 〈E0, State f St_skip en m sp k'
    201     | St_switch sz _ e cs default ⇒
    202         ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     345        ret ? 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st
     346    | St_loop s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st
     347    | St_block s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kblock k) ? st
     348    | St_exit n ⇒ λInv.
     349        ! k' ← k_exit n k ?? kInv;
     350        ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st
     351    | St_switch sz _ e cs default ⇒ λInv.
     352        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    203353        match v with
    204354        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
    205             ! k' ← k_exit (find_case ?? i cs default) k;
    206             ret ? 〈tr, State f St_skip en m sp k'〉)
     355            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
     356            ret ? 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
    207357            (Wrong ??? (msg BadSwitchValue))
    208358        | _ ⇒ Wrong ??? (msg BadSwitchValue)
    209359        ]
    210360    | St_return eo ⇒
    211         match eo with
    212         [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)
     361        match eo return λeo. stmt_inv f en (St_return eo) → ? with
     362        [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st
    213363        | Some e ⇒
    214             match e with [ dp ty e ⇒
    215               ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    216               ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)
     364            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ dp ty e ⇒ λInv.
     365              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     366              ret ? 〈tr, Returnstate (Some ? v) (free m sp) st
    217367            ]
    218368        ]
    219     | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
    220     | St_goto l ⇒
    221         ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
    222         ret ? 〈E0, State f s' en m sp k'〉
    223     | St_cost l s' ⇒
    224         ret ? 〈Echarge l, State f s' en m sp k〉
    225     ]
    226 | Callstate fd args m k ⇒
     369    | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
     370    | St_goto l ⇒ λInv.
     371        match find_label_always l (f_body f) Kend ? f en ?? with [ dp sk Inv' ⇒
     372          ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
     373        ]
     374    | St_cost l s' ⇒ λInv.
     375        ret ? 〈Echarge l, State f s' en fInv ? m sp k ? st〉
     376    ] Inv
     377| Callstate fd args m st ⇒
    227378    match fd with
    228379    [ Internal f ⇒
    229380        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    230381        ! en ← bind_params args (f_params f);
    231         ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k
     382        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st
    232383    | External fn ⇒
    233384        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
    234385        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    235386        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
    236         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
    237     ]
    238 | Returnstate res m k ⇒
    239     match k with
    240     [ Kcall dst f sp en k' ⇒
    241         ! en' ← match res with
    242                 [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
    243                 | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
    244                                           | Some id ⇒ update ?? en id v ]
    245                 ];
    246         ret ? 〈E0, State f St_skip en' m sp k'〉
     387        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
     388    ]
     389| Returnstate res m st ⇒
     390    match st with
     391    [ Scall dst f sp en dstP fInv k Inv st' ⇒
     392        match res with
     393        [ None ⇒ match dst with
     394                 [ None ⇒ ret ? 〈E0, State f St_skip en ? ? m sp k ? st'〉
     395                 | Some _ ⇒ Wrong ??? (msg ReturnMismatch)]
     396        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
     397                   [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
     398                   | Some id ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en id dstP v) ? ? m sp k ? st'〉
     399                   ] dstP
     400        ]
    247401    | _ ⇒ Wrong ??? (msg BadState)
    248402    ]
    249403].
     404try @(π1 kInv)
     405try @(π2 kInv)
     406try @(conj ?? I I)
     407try @kInv
     408try @(π2 (π1 Inv))
     409try @kInv
     410try @(π1 (π1 Inv))
     411try (@cont_inv_update @kInv)
     412try @(π2 (π1 (π1 Inv)))
     413try @(π1 (π1 (π1 Inv)))
     414try @(π1 Inv)
     415try @(π2 Inv)
     416[ @stmt_inv_update @fInv
     417| % [ @(π2 Inv) | @kInv ]
     418| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
     419| % [ @Inv | @kInv ]
     420| @(use_sig … k')
     421| @(use_sig … k')
     422| @(π1 Inv')
     423| @(π2 Inv')
     424| @fInv
     425| @I
     426| 11,12:
     427  @(stmt_P_mp … (f_inv f))
     428  #s * #V #L %
     429  [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
     430    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (use_sig … en))
     431      * #id' #ty * #E1 #H <E1 @H
     432    | *: #H cases (Exists_All … H (init_locals_env … en …))
     433      * #id' #ty * #E1 #H <E1 @H
     434    ]
     435  | 2,4: @L
     436  ]
     437| @fInv
     438| @Inv
     439| @stmt_inv_update @fInv
     440| @cont_inv_update @Inv
     441] qed.
    250442
    251443definition is_final : state → option int ≝
    252444λs. match s with
    253 [ Returnstate res m k
    254     match k with
    255     [ Kstop ⇒
     445[ Returnstate res m st
     446    match st with
     447    [ SStop ⇒
    256448        match res with
    257449        [ None ⇒ None ?
     
    278470  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    279471  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    280   OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     472  OK ? 〈ge, Callstate f (nil ?) m SStop〉.
    281473
    282474definition Cminor_fullexec : fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.