source: src/Clight/Cexec.ma @ 1976

Last change on this file since 1976 was 1874, checked in by campbell, 8 years ago

First cut at using back-end memory model throughout.
Note the correction to BEValues.

File size: 21.1 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
[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';
[1516]38  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
[1545]39  | #ptr #r #ty %{ 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.
[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
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  ]
[1545]126| Vptr ptr ⇒
[797]127    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
[1545]128    do u ← match eq_region_dec (ptype ptr) 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)];
[1545]132    match pointer_compat_dec (pblock ptr) s' with
133    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
[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' ≝
[1599]147λty,m,l. let 〈loc,ofs〉 ≝ l in 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 _ ⇒
[1599]187        let 〈loc,ofs〉 ≝ lo in
[500]188          match pointer_compat_dec loc r with
[1545]189          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
[797]190          | inr _ ⇒ Error ? (msg TypeMismatch)
[500]191          ]
[797]192      | _ ⇒ Error ? (msg BadlyTypedTerm)
[498]193      ]
[961]194  | Esizeof ty' ⇒
195      match ty with
196      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
197      | _ ⇒ Error ? (msg BadlyTypedTerm)
198      ]
[250]199  | Eunop op a ⇒
[189]200      do 〈v1,tr〉 ← exec_expr ge en m a;
[797]201      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
[250]202      OK ? 〈v,tr〉
203  | Ebinop op a1 a2 ⇒
[189]204      do 〈v1,tr1〉 ← exec_expr ge en m a1;
205      do 〈v2,tr2〉 ← exec_expr ge en m a2;
[797]206      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
[250]207      OK ? 〈v,tr1⧺tr2〉
208  | Econdition a1 a2 a3 ⇒
[189]209      do 〈v,tr1〉 ← exec_expr ge en m a1;
[250]210      do b ← exec_bool_of_val v (typeof a1);
[189]211      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
[175]212                 [ true ⇒ (exec_expr ge en m a2)
[189]213                 | false ⇒ (exec_expr ge en m a3) ];
[250]214      OK ? 〈v',tr1⧺tr2〉
[20]215(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
[250]216  | Eorbool a1 a2 ⇒
[189]217      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]218      do b1 ← exec_bool_of_val v1 (typeof a1);
[175]219      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
[189]220        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]221        do b2 ← exec_bool_of_val v2 (typeof a2);
222        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
223  | Eandbool a1 a2 ⇒
[189]224      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]225      do b1 ← exec_bool_of_val v1 (typeof a1);
[175]226      match b1 return λ_.res (val×trace) with [ true ⇒
[189]227        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]228        do b2 ← exec_bool_of_val v2 (typeof a2);
[175]229        OK ? 〈of_bool b2, tr1⧺tr2〉
[250]230      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
231  | Ecast ty' a ⇒
[189]232      do 〈v,tr〉 ← exec_expr ge en m a;
233      do v' ← exec_cast m v (typeof a) ty';
[250]234      OK ? 〈v',tr〉
235  | Ecost l a ⇒
[189]236      do 〈v,tr〉 ← exec_expr ge en m a;
[250]237      OK ? 〈v,tr⧺(Echarge l)〉
[20]238  ]
239]
[583]240and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
[20]241  match e' with
242  [ Evar id ⇒
[1058]243      match (lookup ?? en id) with
[797]244      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
[583]245      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
[20]246      ]
[250]247  | Ederef a ⇒
[189]248      do 〈v,tr〉 ← exec_expr ge en m a;
[20]249      match v with
[1545]250      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
[797]251      | _ ⇒ Error ? (msg TypeMismatch)
[250]252      ]
[20]253  | Efield a i ⇒
254      match (typeof a) with
[250]255      [ Tstruct id fList ⇒
[498]256          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
[189]257          do delta ← field_offset i fList;
[961]258          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
[250]259      | Tunion id fList ⇒
[498]260          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
261          OK ? 〈lofs,tr〉
[797]262      | _ ⇒ Error ? (msg BadlyTypedTerm)
[20]263      ]
[797]264  | _ ⇒ Error ? (msg BadLvalueTerm)
[20]265  ]
[583]266and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
[20]267match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
[250]268
[487]269lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
270#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
[250]271
[251]272(* We define a special induction principle tailored to the recursive definition
273   above. *)
274
[487]275definition is_not_lvalue: expr_descr → Prop ≝
[251]276λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
277
[487]278definition Plvalue ≝ λP:(expr → Prop).λe,ty.
[251]279match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
280
[20]281(* TODO: Can we do this sensibly with a map combinator? *)
[487]282let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
[20]283match l with
[251]284[ nil ⇒ OK ? 〈nil val, E0〉
285| cons e1 es ⇒
[189]286  do 〈v,tr1〉 ← exec_expr ge e m e1;
287  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
[251]288  OK ? 〈cons val v vs, tr1⧺tr2〉
289].
[20]290
[487]291let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
[20]292match l with
[487]293[ nil ⇒ 〈en, m〉
[20]294| cons h vars ⇒
[1599]295  let 〈id,ty〉 ≝ h in
[1874]296  let 〈m1,b1〉 ≝ alloc becontentT m 0 (sizeof ty) Any in
[1058]297      exec_alloc_variables (add ?? en id b1) m1 vars
[1599]298].
[20]299
[797]300axiom WrongNumberOfParameters : String.
301axiom FailedStore : String.
302
[20]303(* TODO: can we establish that length params = length vs in advance? *)
[487]304let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
[20]305  match params with
[797]306  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
[1599]307  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
[20]308      match vs with
[797]309      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
[487]310      | cons v1 vl ⇒
[1058]311          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
[797]312          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
[487]313          exec_bind_parameters e m1 params' vl
[20]314      ]
[1599]315  ].
[20]316
[638]317let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
[388]318match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
319[ Kstop ⇒ ?
320| Kcall _ _ _ _ ⇒ ?
321| _ ⇒ ?
322].
[487]323[ 1,8: %1 ; //
324| *: %2 ; /2/
325] qed.
[20]326
[891]327definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
328λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
[388]329[ Sskip ⇒ inl ?? (refl ??)
330| _ ⇒ inr ?? (nmk ? (λH.?))
[487]331]. destruct
332qed.
[388]333
[20]334
335(* execution *)
336
[487]337definition store_value_of_type' ≝
[124]338λty,m,l,v.
[1599]339let 〈loc,ofs〉 ≝ l in
340  store_value_of_type ty m loc ofs v.
[124]341
[797]342axiom NonsenseState : String.
343axiom ReturnMismatch : String.
344axiom UnknownLabel : String.
345axiom BadFunctionValue : String.
346
[487]347let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
[20]348match st with
349[ State f s k e m ⇒
350  match s with
[252]351  [ Sassign a1 a2 ⇒
[1647]352    ! 〈l,tr1〉 ← exec_lvalue ge e m a1 : IO ???;
353    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
[797]354    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
[252]355    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
356  | Scall lhs a al ⇒
[1647]357    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
358    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
[797]359    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
[457]360    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
[388]361(* requires associativity of IOMonad, so rearrange it below
[20]362    ! k' ← match lhs with
363         [ None ⇒ ret ? (Kcall (None ?) f e k)
364         | Some lhs' ⇒
[208]365           ! locofs ← exec_lvalue ge e m lhs';
[498]366           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
[208]367         ];
[20]368    ret ? 〈E0, Callstate fd vargs k' m〉)
369*)
370    match lhs with
[175]371         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
[20]372         | Some lhs' ⇒
[1647]373           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
[175]374           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
[252]375         ]
376  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
[20]377  | Sskip ⇒
378      match k with
[252]379      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
[20]380      | Kstop ⇒
381          match fn_return f with
[1874]382          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
[797]383          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]384          ]
385      | Kcall _ _ _ _ ⇒
386          match fn_return f with
[1874]387          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
[797]388          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]389          ]
[252]390      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
391      | Kdowhile a s' k' ⇒
[1647]392          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]393          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[20]394          match b with
[175]395          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
396          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
[252]397          ]
398      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
399      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
400      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[797]401      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]402      ]
403  | Scontinue ⇒
404      match k with
[252]405      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
406      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
407      | Kdowhile a s' k' ⇒
[1647]408          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]409          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[20]410          match b with
[175]411          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
412          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
[252]413          ]
414      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
415      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
[797]416      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]417      ]
418  | Sbreak ⇒
419      match k with
[252]420      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
421      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
422      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
423      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
424      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[797]425      | _ ⇒ Wrong ??? (msg NonsenseState)
[20]426      ]
[252]427  | Sifthenelse a s1 s2 ⇒
[1647]428      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]429      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[252]430      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
431  | Swhile a s' ⇒
[1647]432      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]433      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[175]434      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
[252]435                      else State f Sskip k e m〉
436  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
[20]437  | Sfor a1 a2 a3 s' ⇒
438      match is_Sskip a1 with
[252]439      [ inl _ ⇒
[1647]440          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
[250]441          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
[252]442          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
443      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
[20]444      ]
445  | Sreturn a_opt ⇒
446    match a_opt with
447    [ None ⇒ match fn_return f with
[1874]448      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e))〉
[797]449      | _ ⇒ Wrong ??? (msg ReturnMismatch)
[20]450      ]
[252]451    | Some a ⇒
[388]452        match type_eq_dec (fn_return f) Tvoid with
[797]453        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
[388]454        | inr _ ⇒
[1647]455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[1874]456          ret ? 〈tr, Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e))〉
[388]457        ]
[20]458    ]
[252]459  | Sswitch a sl ⇒
[1647]460      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[961]461      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
[797]462                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
[252]463  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
[20]464  | Sgoto lbl ⇒
465      match find_label lbl (fn_body f) (call_cont k) with
[1599]466      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
[797]467      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
[20]468      ]
[252]469  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
[20]470  ]
471| Callstate f0 vargs k m ⇒
472  match f0 with
[725]473  [ CL_Internal f ⇒
[1599]474    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
[1647]475      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
[20]476      ret ? 〈E0, State f (fn_body f) k e m2〉
[725]477  | CL_External f argtys retty ⇒
[1647]478      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
[366]479      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
480      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
[20]481  ]
482| Returnstate res k m ⇒
483  match k with
484  [ Kcall r f e k' ⇒
485    match r with
[389]486    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
[20]487    | Some r' ⇒
[1599]488      let 〈l,ty〉 ≝ r' in
[797]489          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
[252]490          ret ? 〈E0, (State f Sskip k' e m')〉
[20]491    ]
[1713]492  | Kstop ⇒
493    match res with
494    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
495    | _ ⇒ Wrong ??? (msg ReturnMismatch)
496    ]
[797]497  | _ ⇒ Wrong ??? (msg NonsenseState)
[20]498  ]
[1713]499| Finalstate r ⇒
500    Wrong ??? (msg NonsenseState)
[252]501].
502
[797]503axiom MainMissing : String.
504
[1244]505definition make_global : clight_program → genv ≝
506λp. globalenv Genv ?? (fst ??) p.
[1231]507
508let rec make_initial_state (p:clight_program) : res state ≝
509  let ge ≝ make_global p in
[1139]510  do m0 ← init_mem Genv ?? (fst ??) p;
[797]511  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
512  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
[1231]513  OK ? (Callstate f (nil ?) Kstop m0).
[250]514
[708]515let rec is_final (s:state) : option int ≝
516match s with
[1713]517[ Finalstate r ⇒ Some ? r
[708]518| _ ⇒ None ?
519].
520
[487]521definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
522#st elim st;
523[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
524| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
[1713]525| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
526| #r %1 %{r} %
[487]527] qed.
[20]528
[487]529let rec exec_steps (n:nat) (ge:genv) (s:state) :
[366]530 IO io_out io_in (trace×state) ≝
[20]531match is_final_state s with
[252]532[ inl _ ⇒ ret ? 〈E0, s〉
[20]533| inr _ ⇒
534  match n with
[252]535  [ O ⇒ ret ? 〈E0, s〉
536  | S n' ⇒
[208]537      ! 〈t,s'〉 ← exec_step ge s;
[1147]538      ! 〈t',s''〉 ← exec_steps n' ge s';
[252]539      ret ? 〈t ⧺ t',s''〉
[20]540  ]
[252]541].
[1713]542(*
[487]543definition mem_of_state : state → mem ≝
[291]544λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
[1713]545*)
[1231]546definition clight_exec : trans_system io_out io_in ≝
547  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
[239]548
[731]549definition clight_fullexec : fullexec io_out io_in ≝
[1231]550  mk_fullexec ??? clight_exec make_global make_initial_state.
Note: See TracBrowser for help on using the repository browser.