source: src/Clight/Cexec.ma @ 1280

Last change on this file since 1280 was 1244, checked in by campbell, 9 years ago

Sort out Clight semantics equivalence proof for new SmallstepExec?.

File size: 21.4 KB
RevLine 
[20]1
2
[700]3include "utilities/extralib.ma".
[731]4include "common/IO.ma".
[700]5include "common/SmallstepExec.ma".
6include "Clight/Csem.ma".
[880]7include "Clight/TypeComparison.ma".
[20]8
[487]9definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
[797]10  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
[250]11
[797]12axiom ValueIsNotABoolean : String.
13
[487]14definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
[20]15  λv,ty. match v in val with
[961]16  [ Vint sz i ⇒ match ty with
17    [ Tint sz' _ ⇒ intsize_eq_elim ? sz sz' ? i
18                   (λi. OK ? (¬eq_bv ? i (zero ?))) (Error ? (msg TypeMismatch))
[797]19    | _ ⇒ Error ? (msg TypeMismatch)
[20]20    ]
21  | Vfloat f ⇒ match ty with
[250]22    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
[797]23    | _ ⇒ Error ? (msg TypeMismatch)
[20]24    ]
[500]25  | Vptr _ _ _ _ ⇒ match ty with
[484]26    [ Tpointer _ _ ⇒ OK ? true
[797]27    | _ ⇒ Error ? (msg TypeMismatch)
[20]28    ]
[484]29  | Vnull _ ⇒ match ty with
30    [ Tpointer _ _ ⇒ OK ? false
[797]31    | _ ⇒ Error ? (msg TypeMismatch)
[484]32    ]
[797]33  | _ ⇒ Error ? (msg ValueIsNotABoolean)
[250]34  ].
35
[487]36lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
37#v #ty #r #H elim H; #v #t #H' elim H';
[961]38  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?) >(eq_bv_false … ne) //
[500]39  | #r #b #pc #i #i0 #s %{ true} % //
[487]40  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
[961]41  | * #sg %{ false} % //
[487]42  | #r #r' #t %{ false} % //;
43  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
44  ]
45qed.
[20]46
47(* Prove a few minor results to make proof obligations easy. *)
48
[487]49lemma bind_OK: ∀A,B,P,e,f.
[797]50  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
51  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
[487]52#A #B #P #e #f elim e; /2/; qed.
[20]53
[487]54lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
[797]55  (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
56  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
[487]57#A #B #P #P' #e #f elim e;
58[ #v0 elim v0; #v #Hv #IH @IH
[797]59| #m #_ @I
[487]60] qed.
[20]61
[487]62lemma bind2_OK: ∀A,B,C,P,e,f.
[797]63  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
64  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
[487]65#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
[20]66
[797]67lemma opt_bind_OK: ∀A,B,P,m,e,f.
68  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
69  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
70#A #B #P #m #e #f elim e; normalize; /2/; qed.
[20]71
72
[797]73axiom BadCast : String. (* TODO: refine into more precise errors? *)
74
[961]75definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
76λm:mem. λsz. λi. λty:type. λty':type.
77match eq_bv ? i (zero ?) with
[124]78[ true ⇒
79  match ty with
[961]80  [ Tint sz' _ ⇒
81    if eq_intsize sz sz' then
82      match ty' with
83      [ Tpointer r _ ⇒ OK ? (Vnull r)
84      | Tarray r _ _ ⇒ OK ? (Vnull r)
85      | Tfunction _ _ ⇒ OK ? (Vnull Code)
86      | _ ⇒ Error ? (msg BadCast)
87      ]
88    else Error ? (msg TypeMismatch)
[797]89  | _ ⇒ Error ? (msg BadCast)
[124]90  ]
[797]91| false ⇒ Error ? (msg BadCast)
[250]92].
[124]93
[487]94definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
[189]95λm:mem. λv:val. λty:type. λty':type.
[20]96match v with
[961]97[ Vint sz i ⇒
[20]98  match ty with
99  [ Tint sz1 si1 ⇒
[961]100    intsize_eq_elim ? sz sz1 ? i
101    (λi.
102      match ty' with
[964]103      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
[961]104      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
105      | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
106      | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
107      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
108      | _ ⇒ Error ? (msg BadCast)
109      ])
110    (Error ? (msg BadCast))
111  | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
112  | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
113  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[797]114  | _ ⇒ Error ? (msg TypeMismatch)
[20]115  ]
116| Vfloat f ⇒
117  match ty with
118  [ Tfloat sz ⇒
119    match ty' with
[961]120    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
[250]121    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
[797]122    | _ ⇒ Error ? (msg BadCast)
[20]123    ]
[797]124  | _ ⇒ Error ? (msg TypeMismatch)
[20]125  ]
[500]126| Vptr r b _ ofs ⇒
[797]127    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
128    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
[189]129    do s' ← match ty' with
[127]130         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
[797]131         | _ ⇒ Error ? (msg BadCast)];
[500]132    match pointer_compat_dec b s' with
133    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
[797]134    | inr _ ⇒ Error ? (msg BadCast)
[500]135    ]
[484]136| Vnull r ⇒
[797]137    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
138    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
[484]139    do s' ← match ty' with
140         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
[797]141         | _ ⇒ Error ? (msg BadCast) ];
[484]142    OK ? (Vnull s')
[797]143| _ ⇒ Error ? (msg BadCast)
[250]144].
145
[487]146definition load_value_of_type' ≝
[498]147λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
[124]148
[797]149axiom BadlyTypedTerm : String.
150axiom UnknownIdentifier : String.
151axiom BadLvalueTerm : String.
152axiom FailedLoad : String.
153axiom FailedOp : String.
154
[1147]155(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
156   a structurally smaller value, we break out the surrounding Expr constructor
157   and use exec_lvalue'. *)
158
[487]159let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
[20]160match e with
161[ Expr e' ty ⇒
162  match e' with
[961]163  [ Econst_int sz i ⇒
164      match ty with
165      [ Tint sz' _ ⇒
166          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
167          else Error ? (msg BadlyTypedTerm)
168      | _ ⇒ Error ? (msg BadlyTypedTerm)
169      ]
[250]170  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
171  | Evar _ ⇒
[189]172      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]173      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]174      OK ? 〈v,tr〉
175  | Ederef _ ⇒
[189]176      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]177      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]178      OK ? 〈v,tr〉
179  | Efield _ _ ⇒
[189]180      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]181      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]182      OK ? 〈v,tr〉
183  | Eaddrof a ⇒
[498]184      do 〈lo,tr〉 ← exec_lvalue ge en m a;
185      match ty with
[500]186      [ Tpointer r _ ⇒
187        match lo with [ pair loc ofs ⇒
188          match pointer_compat_dec loc r with
189          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
[797]190          | inr _ ⇒ Error ? (msg TypeMismatch)
[500]191          ]
192        ]
[797]193      | _ ⇒ Error ? (msg BadlyTypedTerm)
[498]194      ]
[961]195  | Esizeof ty' ⇒
196      match ty with
197      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
198      | _ ⇒ Error ? (msg BadlyTypedTerm)
199      ]
[250]200  | Eunop op a ⇒
[189]201      do 〈v1,tr〉 ← exec_expr ge en m a;
[797]202      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
[250]203      OK ? 〈v,tr〉
204  | Ebinop op a1 a2 ⇒
[189]205      do 〈v1,tr1〉 ← exec_expr ge en m a1;
206      do 〈v2,tr2〉 ← exec_expr ge en m a2;
[797]207      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
[250]208      OK ? 〈v,tr1⧺tr2〉
209  | Econdition a1 a2 a3 ⇒
[189]210      do 〈v,tr1〉 ← exec_expr ge en m a1;
[250]211      do b ← exec_bool_of_val v (typeof a1);
[189]212      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
[175]213                 [ true ⇒ (exec_expr ge en m a2)
[189]214                 | false ⇒ (exec_expr ge en m a3) ];
[250]215      OK ? 〈v',tr1⧺tr2〉
[20]216(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
[250]217  | Eorbool a1 a2 ⇒
[189]218      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]219      do b1 ← exec_bool_of_val v1 (typeof a1);
[175]220      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
[189]221        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]222        do b2 ← exec_bool_of_val v2 (typeof a2);
223        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
224  | Eandbool a1 a2 ⇒
[189]225      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]226      do b1 ← exec_bool_of_val v1 (typeof a1);
[175]227      match b1 return λ_.res (val×trace) with [ true ⇒
[189]228        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]229        do b2 ← exec_bool_of_val v2 (typeof a2);
[175]230        OK ? 〈of_bool b2, tr1⧺tr2〉
[250]231      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
232  | Ecast ty' a ⇒
[189]233      do 〈v,tr〉 ← exec_expr ge en m a;
234      do v' ← exec_cast m v (typeof a) ty';
[250]235      OK ? 〈v',tr〉
236  | Ecost l a ⇒
[189]237      do 〈v,tr〉 ← exec_expr ge en m a;
[250]238      OK ? 〈v,tr⧺(Echarge l)〉
[20]239  ]
240]
[583]241and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
[20]242  match e' with
243  [ Evar id ⇒
[1058]244      match (lookup ?? en id) with
[797]245      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
[583]246      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
[20]247      ]
[250]248  | Ederef a ⇒
[189]249      do 〈v,tr〉 ← exec_expr ge en m a;
[20]250      match v with
[500]251      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
[797]252      | _ ⇒ Error ? (msg TypeMismatch)
[250]253      ]
[20]254  | Efield a i ⇒
255      match (typeof a) with
[250]256      [ Tstruct id fList ⇒
[498]257          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
[189]258          do delta ← field_offset i fList;
[961]259          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
[250]260      | Tunion id fList ⇒
[498]261          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
262          OK ? 〈lofs,tr〉
[797]263      | _ ⇒ Error ? (msg BadlyTypedTerm)
[20]264      ]
[797]265  | _ ⇒ Error ? (msg BadLvalueTerm)
[20]266  ]
[583]267and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
[20]268match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
[250]269
[487]270lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
271#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
[250]272
[251]273(* We define a special induction principle tailored to the recursive definition
274   above. *)
275
[487]276definition is_not_lvalue: expr_descr → Prop ≝
[251]277λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
278
[487]279definition Plvalue ≝ λP:(expr → Prop).λe,ty.
[251]280match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
281
[20]282(* TODO: Can we do this sensibly with a map combinator? *)
[487]283let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
[20]284match l with
[251]285[ nil ⇒ OK ? 〈nil val, E0〉
286| cons e1 es ⇒
[189]287  do 〈v,tr1〉 ← exec_expr ge e m e1;
288  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
[251]289  OK ? 〈cons val v vs, tr1⧺tr2〉
290].
[20]291
[487]292let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
[20]293match l with
[487]294[ nil ⇒ 〈en, m〉
[20]295| cons h vars ⇒
[487]296  match h with [ pair id ty ⇒
297    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
[1058]298      exec_alloc_variables (add ?? en id b1) m1 vars
[487]299]]].
[20]300
[797]301axiom WrongNumberOfParameters : String.
302axiom FailedStore : String.
303
[20]304(* TODO: can we establish that length params = length vs in advance? *)
[487]305let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
[20]306  match params with
[797]307  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
[487]308  | cons idty params' ⇒ match idty with [ pair id ty ⇒
[20]309      match vs with
[797]310      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
[487]311      | cons v1 vl ⇒
[1058]312          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
[797]313          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
[487]314          exec_bind_parameters e m1 params' vl
[20]315      ]
316  ] ].
317
[638]318let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
[388]319match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
320[ Kstop ⇒ ?
321| Kcall _ _ _ _ ⇒ ?
322| _ ⇒ ?
323].
[487]324[ 1,8: %1 ; //
325| *: %2 ; /2/
326] qed.
[20]327
[891]328definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
329λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
[388]330[ Sskip ⇒ inl ?? (refl ??)
331| _ ⇒ inr ?? (nmk ? (λH.?))
[487]332]. destruct
333qed.
[388]334
[20]335
336(* execution *)
337
[487]338definition store_value_of_type' ≝
[124]339λty,m,l,v.
[498]340match l with [ pair loc ofs ⇒
341  store_value_of_type ty m loc ofs v ].
[124]342
[797]343axiom NonsenseState : String.
344axiom ReturnMismatch : String.
345axiom UnknownLabel : String.
346axiom BadFunctionValue : String.
347
[487]348let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
[20]349match st with
350[ State f s k e m ⇒
351  match s with
[252]352  [ Sassign a1 a2 ⇒
[208]353    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
354    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
[797]355    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
[252]356    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
357  | Scall lhs a al ⇒
[208]358    ! 〈vf,tr2〉 ← exec_expr ge e m a;
359    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
[797]360    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
[457]361    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
[388]362(* requires associativity of IOMonad, so rearrange it below
[20]363    ! k' ← match lhs with
364         [ None ⇒ ret ? (Kcall (None ?) f e k)
365         | Some lhs' ⇒
[208]366           ! locofs ← exec_lvalue ge e m lhs';
[498]367           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
[208]368         ];
[20]369    ret ? 〈E0, Callstate fd vargs k' m〉)
370*)
371    match lhs with
[175]372         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
[20]373         | Some lhs' ⇒
[208]374           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
[175]375           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
[252]376         ]
377  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
[20]378  | Sskip ⇒
379      match k with
[252]380      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
[20]381      | Kstop ⇒
382          match fn_return f with
[252]383          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
[797]384          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]385          ]
386      | Kcall _ _ _ _ ⇒
387          match fn_return f with
[252]388          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
[797]389          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]390          ]
[252]391      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
392      | Kdowhile a s' k' ⇒
[208]393          ! 〈v,tr〉 ← exec_expr ge e m a;
[250]394          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[20]395          match b with
[175]396          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
397          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
[252]398          ]
399      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
400      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
401      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[797]402      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]403      ]
404  | Scontinue ⇒
405      match k with
[252]406      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
407      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
408      | Kdowhile a s' k' ⇒
[208]409          ! 〈v,tr〉 ← exec_expr ge e m a;
[250]410          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[20]411          match b with
[175]412          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
413          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
[252]414          ]
415      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
416      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
[797]417      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]418      ]
419  | Sbreak ⇒
420      match k with
[252]421      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
422      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
423      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
424      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
425      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[797]426      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]427      ]
[252]428  | Sifthenelse a s1 s2 ⇒
[208]429      ! 〈v,tr〉 ← exec_expr ge e m a;
[250]430      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[252]431      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
432  | Swhile a s' ⇒
[208]433      ! 〈v,tr〉 ← exec_expr ge e m a;
[250]434      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[175]435      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
[252]436                      else State f Sskip k e m〉
437  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
[20]438  | Sfor a1 a2 a3 s' ⇒
439      match is_Sskip a1 with
[252]440      [ inl _ ⇒
[208]441          ! 〈v,tr〉 ← exec_expr ge e m a2;
[250]442          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
[252]443          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
444      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
[20]445      ]
446  | Sreturn a_opt ⇒
447    match a_opt with
448    [ None ⇒ match fn_return f with
[252]449      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
[797]450      | _ ⇒ Wrong ??? (msg ReturnMismatch)
[20]451      ]
[252]452    | Some a ⇒
[388]453        match type_eq_dec (fn_return f) Tvoid with
[797]454        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
[388]455        | inr _ ⇒
456          ! 〈v,tr〉 ← exec_expr ge e m a;
457          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
458        ]
[20]459    ]
[252]460  | Sswitch a sl ⇒
[208]461      ! 〈v,tr〉 ← exec_expr ge e m a;
[961]462      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
[797]463                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
[252]464  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
[20]465  | Sgoto lbl ⇒
466      match find_label lbl (fn_body f) (call_cont k) with
[487]467      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
[797]468      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
[20]469      ]
[252]470  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
[20]471  ]
472| Callstate f0 vargs k m ⇒
473  match f0 with
[725]474  [ CL_Internal f ⇒
[487]475    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
476      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
[20]477      ret ? 〈E0, State f (fn_body f) k e m2〉
[252]478    ]
[725]479  | CL_External f argtys retty ⇒
[487]480      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
[366]481      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
482      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
[20]483  ]
484| Returnstate res k m ⇒
485  match k with
486  [ Kcall r f e k' ⇒
487    match r with
[389]488    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
[20]489    | Some r' ⇒
[487]490      match r' with [ pair l ty ⇒
[797]491          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
[252]492          ret ? 〈E0, (State f Sskip k' e m')〉
[20]493      ]
494    ]
[797]495  | _ ⇒ Wrong ??? (msg NonsenseState)
[20]496  ]
[252]497].
498
[797]499axiom MainMissing : String.
500
[1244]501definition make_global : clight_program → genv ≝
502λp. globalenv Genv ?? (fst ??) p.
[1231]503
504let rec make_initial_state (p:clight_program) : res state ≝
505  let ge ≝ make_global p in
[1139]506  do m0 ← init_mem Genv ?? (fst ??) p;
[797]507  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
508  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
[1231]509  OK ? (Callstate f (nil ?) Kstop m0).
[250]510
[708]511let rec is_final (s:state) : option int ≝
512match s with
513[ Returnstate res k m ⇒
514  match k with
515  [ Kstop ⇒
516    match res with
[961]517    [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?)
[708]518    | _ ⇒ None ?
519    ]
520  | _ ⇒ None ?
521  ]
522| _ ⇒ None ?
523].
524
[487]525definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
526#st elim st;
527[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
528| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
529| #v #k #m cases k;
530  [ cases v;
[961]531    [ 2: * #i [ 1,2: %2 % * #r #H inversion H #i' #m #e destruct
532              | %1 ; %{ i} //;
533              ]
[487]534    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
535    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
536    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
[500]537    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
[487]538    ]
539  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
540  | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
541  | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
542  | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
543  ]
544] qed.
[20]545
[487]546let rec exec_steps (n:nat) (ge:genv) (s:state) :
[366]547 IO io_out io_in (trace×state) ≝
[20]548match is_final_state s with
[252]549[ inl _ ⇒ ret ? 〈E0, s〉
[20]550| inr _ ⇒
551  match n with
[252]552  [ O ⇒ ret ? 〈E0, s〉
553  | S n' ⇒
[208]554      ! 〈t,s'〉 ← exec_step ge s;
[1147]555      ! 〈t',s''〉 ← exec_steps n' ge s';
[252]556      ret ? 〈t ⧺ t',s''〉
[20]557  ]
[252]558].
559
[487]560definition mem_of_state : state → mem ≝
[291]561λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
562
[1231]563definition clight_exec : trans_system io_out io_in ≝
564  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
[239]565
[731]566definition clight_fullexec : fullexec io_out io_in ≝
[1231]567  mk_fullexec ??? clight_exec make_global make_initial_state.
Note: See TracBrowser for help on using the repository browser.