source: src/Clight/Cexec.ma @ 2324

Last change on this file since 2324 was 2203, checked in by campbell, 8 years ago

A general result about simulations of executions.

File size: 21.7 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    ]
[1545]25  | Vptr _ ⇒ match ty with
[2176]26    [ Tpointer _ ⇒ OK ? true
[797]27    | _ ⇒ Error ? (msg TypeMismatch)
[20]28    ]
[2176]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';
[1516]38  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
[2176]39  | #ptr #ty %{ true} % //
[487]40  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
[961]41  | * #sg %{ false} % //
[2176]42  | #t %{ false} % //;
[487]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.
[1603]55  (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
[797]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
[2176]83      [ Tpointer _ ⇒ OK ? Vnull
84      | Tarray _ _ ⇒ OK ? Vnull
85      | Tfunction _ _ ⇒ OK ? Vnull
[961]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
[2176]94definition ptr_like_type : type → bool ≝
95λt. match t with
96[ Tpointer _ ⇒ true
97| Tarray _ _ ⇒ true
98| Tfunction _ _ ⇒ true
99| _ ⇒ false
100].
101
[487]102definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
[189]103λm:mem. λv:val. λty:type. λty':type.
[20]104match v with
[961]105[ Vint sz i ⇒
[20]106  match ty with
107  [ Tint sz1 si1 ⇒
[961]108    intsize_eq_elim ? sz sz1 ? i
109    (λi.
110      match ty' with
[964]111      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
[961]112      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
[2176]113      | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
114      | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[961]115      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
116      | _ ⇒ Error ? (msg BadCast)
117      ])
118    (Error ? (msg BadCast))
[2176]119  | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
120  | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[961]121  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[797]122  | _ ⇒ Error ? (msg TypeMismatch)
[20]123  ]
124| Vfloat f ⇒
125  match ty with
126  [ Tfloat sz ⇒
127    match ty' with
[961]128    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
[250]129    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
[797]130    | _ ⇒ Error ? (msg BadCast)
[20]131    ]
[797]132  | _ ⇒ Error ? (msg TypeMismatch)
[20]133  ]
[1545]134| Vptr ptr ⇒
[2176]135(*    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
[1545]136    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
[189]137    do s' ← match ty' with
[127]138         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
[797]139         | _ ⇒ Error ? (msg BadCast)];
[1545]140    match pointer_compat_dec (pblock ptr) s' with
141    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
[797]142    | inr _ ⇒ Error ? (msg BadCast)
[2176]143    ]*)
144    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? (Vptr ptr) else Error ? (msg BadCast)
145| Vnull ⇒
146(*
[797]147    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
148    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
[484]149    do s' ← match ty' with
150         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
[797]151         | _ ⇒ Error ? (msg BadCast) ];
[2176]152    OK ? (Vnull s')*)
153    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? Vnull else Error ? (msg BadCast)
[797]154| _ ⇒ Error ? (msg BadCast)
[250]155].
156
[487]157definition load_value_of_type' ≝
[1599]158λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
[124]159
[797]160axiom BadlyTypedTerm : String.
161axiom UnknownIdentifier : String.
162axiom BadLvalueTerm : String.
163axiom FailedLoad : String.
164axiom FailedOp : String.
165
[1147]166(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
167   a structurally smaller value, we break out the surrounding Expr constructor
168   and use exec_lvalue'. *)
169
[487]170let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
[20]171match e with
172[ Expr e' ty ⇒
173  match e' with
[961]174  [ Econst_int sz i ⇒
175      match ty with
176      [ Tint sz' _ ⇒
177          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
178          else Error ? (msg BadlyTypedTerm)
179      | _ ⇒ Error ? (msg BadlyTypedTerm)
180      ]
[250]181  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
182  | Evar _ ⇒
[189]183      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]184      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]185      OK ? 〈v,tr〉
186  | Ederef _ ⇒
[189]187      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]188      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]189      OK ? 〈v,tr〉
190  | Efield _ _ ⇒
[189]191      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]192      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]193      OK ? 〈v,tr〉
194  | Eaddrof a ⇒
[498]195      do 〈lo,tr〉 ← exec_lvalue ge en m a;
196      match ty with
[2176]197      [ Tpointer  _ ⇒
[1599]198        let 〈loc,ofs〉 ≝ lo in
[2176]199(*          match pointer_compat_dec loc r with
[1545]200          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
[797]201          | inr _ ⇒ Error ? (msg TypeMismatch)
[2176]202          ]*)  OK ? 〈Vptr (mk_pointer loc ofs), tr〉
[797]203      | _ ⇒ Error ? (msg BadlyTypedTerm)
[498]204      ]
[961]205  | Esizeof ty' ⇒
206      match ty with
207      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
208      | _ ⇒ Error ? (msg BadlyTypedTerm)
209      ]
[250]210  | Eunop op a ⇒
[189]211      do 〈v1,tr〉 ← exec_expr ge en m a;
[797]212      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
[250]213      OK ? 〈v,tr〉
214  | Ebinop op a1 a2 ⇒
[189]215      do 〈v1,tr1〉 ← exec_expr ge en m a1;
216      do 〈v2,tr2〉 ← exec_expr ge en m a2;
[797]217      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
[250]218      OK ? 〈v,tr1⧺tr2〉
219  | Econdition a1 a2 a3 ⇒
[189]220      do 〈v,tr1〉 ← exec_expr ge en m a1;
[250]221      do b ← exec_bool_of_val v (typeof a1);
[189]222      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
[175]223                 [ true ⇒ (exec_expr ge en m a2)
[189]224                 | false ⇒ (exec_expr ge en m a3) ];
[250]225      OK ? 〈v',tr1⧺tr2〉
[20]226(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
[250]227  | Eorbool a1 a2 ⇒
[189]228      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]229      do b1 ← exec_bool_of_val v1 (typeof a1);
[175]230      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
[189]231        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]232        do b2 ← exec_bool_of_val v2 (typeof a2);
233        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
234  | Eandbool a1 a2 ⇒
[189]235      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]236      do b1 ← exec_bool_of_val v1 (typeof a1);
[175]237      match b1 return λ_.res (val×trace) with [ true ⇒
[189]238        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]239        do b2 ← exec_bool_of_val v2 (typeof a2);
[175]240        OK ? 〈of_bool b2, tr1⧺tr2〉
[250]241      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
242  | Ecast ty' a ⇒
[189]243      do 〈v,tr〉 ← exec_expr ge en m a;
244      do v' ← exec_cast m v (typeof a) ty';
[250]245      OK ? 〈v',tr〉
246  | Ecost l a ⇒
[189]247      do 〈v,tr〉 ← exec_expr ge en m a;
[250]248      OK ? 〈v,tr⧺(Echarge l)〉
[20]249  ]
250]
[583]251and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
[20]252  match e' with
253  [ Evar id ⇒
[1058]254      match (lookup ?? en id) with
[1986]255      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol … ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
[583]256      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
[20]257      ]
[250]258  | Ederef a ⇒
[189]259      do 〈v,tr〉 ← exec_expr ge en m a;
[20]260      match v with
[1545]261      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
[797]262      | _ ⇒ Error ? (msg TypeMismatch)
[250]263      ]
[20]264  | Efield a i ⇒
265      match (typeof a) with
[250]266      [ Tstruct id fList ⇒
[498]267          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
[189]268          do delta ← field_offset i fList;
[961]269          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
[250]270      | Tunion id fList ⇒
[498]271          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
272          OK ? 〈lofs,tr〉
[797]273      | _ ⇒ Error ? (msg BadlyTypedTerm)
[20]274      ]
[797]275  | _ ⇒ Error ? (msg BadLvalueTerm)
[20]276  ]
[583]277and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
[20]278match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
[250]279
[487]280lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
281#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
[250]282
[20]283(* TODO: Can we do this sensibly with a map combinator? *)
[487]284let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
[20]285match l with
[251]286[ nil ⇒ OK ? 〈nil val, E0〉
287| cons e1 es ⇒
[189]288  do 〈v,tr1〉 ← exec_expr ge e m e1;
289  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
[251]290  OK ? 〈cons val v vs, tr1⧺tr2〉
291].
[20]292
[487]293let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
[20]294match l with
[487]295[ nil ⇒ 〈en, m〉
[20]296| cons h vars ⇒
[1599]297  let 〈id,ty〉 ≝ h in
[2176]298  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) XData in
[1058]299      exec_alloc_variables (add ?? en id b1) m1 vars
[1599]300].
[20]301
[797]302axiom WrongNumberOfParameters : String.
303axiom FailedStore : String.
304
[20]305(* TODO: can we establish that length params = length vs in advance? *)
[487]306let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
[20]307  match params with
[797]308  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
[1599]309  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
[20]310      match vs with
[797]311      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
[487]312      | cons v1 vl ⇒
[1058]313          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
[797]314          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
[487]315          exec_bind_parameters e m1 params' vl
[20]316      ]
[1599]317  ].
[20]318
[638]319let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
[388]320match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
321[ Kstop ⇒ ?
322| Kcall _ _ _ _ ⇒ ?
323| _ ⇒ ?
324].
[487]325[ 1,8: %1 ; //
326| *: %2 ; /2/
327] qed.
[20]328
[891]329definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
330λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
[388]331[ Sskip ⇒ inl ?? (refl ??)
332| _ ⇒ inr ?? (nmk ? (λH.?))
[487]333]. destruct
334qed.
[388]335
[20]336
337(* execution *)
338
[487]339definition store_value_of_type' ≝
[124]340λty,m,l,v.
[1599]341let 〈loc,ofs〉 ≝ l in
342  store_value_of_type ty m loc ofs v.
[124]343
[797]344axiom NonsenseState : String.
345axiom ReturnMismatch : String.
346axiom UnknownLabel : String.
347axiom BadFunctionValue : String.
348
[487]349let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
[20]350match st with
351[ State f s k e m ⇒
352  match s with
[252]353  [ Sassign a1 a2 ⇒
[1647]354    ! 〈l,tr1〉 ← exec_lvalue ge e m a1 : IO ???;
355    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
[797]356    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
[252]357    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
358  | Scall lhs a al ⇒
[1647]359    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
360    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
[1986]361    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct … ge vf);
[457]362    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
[388]363(* requires associativity of IOMonad, so rearrange it below
[20]364    ! k' ← match lhs with
365         [ None ⇒ ret ? (Kcall (None ?) f e k)
366         | Some lhs' ⇒
[208]367           ! locofs ← exec_lvalue ge e m lhs';
[498]368           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
[208]369         ];
[20]370    ret ? 〈E0, Callstate fd vargs k' m〉)
371*)
372    match lhs with
[175]373         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
[20]374         | Some lhs' ⇒
[1647]375           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
[175]376           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
[252]377         ]
378  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
[20]379  | Sskip ⇒
380      match k with
[252]381      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
[20]382      | Kstop ⇒
383          match fn_return f with
[1988]384          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
[797]385          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]386          ]
387      | Kcall _ _ _ _ ⇒
388          match fn_return f with
[1988]389          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
[797]390          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]391          ]
[252]392      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
393      | Kdowhile a s' k' ⇒
[1647]394          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]395          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[20]396          match b with
[175]397          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
398          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
[252]399          ]
400      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
401      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
402      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[797]403      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]404      ]
405  | Scontinue ⇒
406      match k with
[252]407      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
408      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
409      | Kdowhile a s' k' ⇒
[1647]410          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]411          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[20]412          match b with
[175]413          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
414          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
[252]415          ]
416      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
417      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
[797]418      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]419      ]
420  | Sbreak ⇒
421      match k with
[252]422      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
423      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
424      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
425      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
426      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[797]427      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]428      ]
[252]429  | Sifthenelse a s1 s2 ⇒
[1647]430      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]431      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[252]432      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
433  | Swhile a s' ⇒
[1647]434      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]435      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[175]436      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
[252]437                      else State f Sskip k e m〉
438  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
[20]439  | Sfor a1 a2 a3 s' ⇒
440      match is_Sskip a1 with
[252]441      [ inl _ ⇒
[1647]442          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
[250]443          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
[252]444          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
445      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
[20]446      ]
447  | Sreturn a_opt ⇒
448    match a_opt with
449    [ None ⇒ match fn_return f with
[1988]450      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
[797]451      | _ ⇒ Wrong ??? (msg ReturnMismatch)
[20]452      ]
[252]453    | Some a ⇒
[388]454        match type_eq_dec (fn_return f) Tvoid with
[797]455        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
[388]456        | inr _ ⇒
[1647]457          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[1988]458          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
[388]459        ]
[20]460    ]
[252]461  | Sswitch a sl ⇒
[1647]462      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[961]463      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
[797]464                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
[252]465  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
[20]466  | Sgoto lbl ⇒
467      match find_label lbl (fn_body f) (call_cont k) with
[1599]468      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
[797]469      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
[20]470      ]
[252]471  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
[20]472  ]
473| Callstate f0 vargs k m ⇒
474  match f0 with
[725]475  [ CL_Internal f ⇒
[1599]476    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
[1647]477      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
[20]478      ret ? 〈E0, State f (fn_body f) k e m2〉
[725]479  | CL_External f argtys retty ⇒
[1647]480      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
[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' ⇒
[1599]490      let 〈l,ty〉 ≝ r' in
[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    ]
[1713]494  | Kstop ⇒
495    match res with
496    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
497    | _ ⇒ Wrong ??? (msg ReturnMismatch)
498    ]
[797]499  | _ ⇒ Wrong ??? (msg NonsenseState)
[20]500  ]
[1713]501| Finalstate r ⇒
502    Wrong ??? (msg NonsenseState)
[252]503].
504
[797]505axiom MainMissing : String.
506
[1244]507definition make_global : clight_program → genv ≝
[1986]508λp. globalenv … (fst ??) p.
[1231]509
510let rec make_initial_state (p:clight_program) : res state ≝
511  let ge ≝ make_global p in
[1986]512  do m0 ← init_mem … (fst ??) p;
513  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
514  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
[1231]515  OK ? (Callstate f (nil ?) Kstop m0).
[250]516
[708]517let rec is_final (s:state) : option int ≝
518match s with
[1713]519[ Finalstate r ⇒ Some ? r
[708]520| _ ⇒ None ?
521].
522
[487]523definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
524#st elim st;
525[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
526| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
[1713]527| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
528| #r %1 %{r} %
[487]529] qed.
[20]530
[487]531let rec exec_steps (n:nat) (ge:genv) (s:state) :
[366]532 IO io_out io_in (trace×state) ≝
[20]533match is_final_state s with
[252]534[ inl _ ⇒ ret ? 〈E0, s〉
[20]535| inr _ ⇒
536  match n with
[252]537  [ O ⇒ ret ? 〈E0, s〉
538  | S n' ⇒
[208]539      ! 〈t,s'〉 ← exec_step ge s;
[1147]540      ! 〈t',s''〉 ← exec_steps n' ge s';
[252]541      ret ? 〈t ⧺ t',s''〉
[20]542  ]
[252]543].
[1713]544(*
[487]545definition mem_of_state : state → mem ≝
[291]546λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
[1713]547*)
[1231]548definition clight_exec : trans_system io_out io_in ≝
549  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
[239]550
[731]551definition clight_fullexec : fullexec io_out io_in ≝
[1231]552  mk_fullexec ??? clight_exec make_global make_initial_state.
[2203]553
554
555(* A few lemmas about the semantics. *)
556
557lemma cl_step_not_final : ∀ge,s1,tr,s2.
558  exec_step ge s1 = OK … 〈tr,s2〉 →
559  is_final s1 = None ?.
560#ge * //
561#r #tr #s2 #E
562whd in E:(??%%);
563destruct
564qed.
565
566(* If you can step in Clight, then you aren't in a final state.  Hence we can
567   give nicer constructors for plus. *)
568lemma cl_plus_one : ∀ge,s1,tr,s2.
569  exec_step ge s1 = OK … 〈tr,s2〉 →
570  plus … clight_exec ge s1 tr s2.
571#ge #s1 #tr #s2 #EX @(plus_one … EX) /2/
572qed.
573
574lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3.
575    exec_step ge s1 = OK … 〈tr,s2〉 →
576    plus … clight_exec ge s2 tr' s3 →
577    plus … clight_exec ge s1 (tr⧺tr') s3.
578#ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX
579qed.
580
Note: See TracBrowser for help on using the repository browser.