source: src/Clight/Cexec.ma @ 1058

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

Evict CompCert? Maps interface in favour of BitVectorTries?.

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