source: src/Clight/Cexec.ma @ 3095

Last change on this file since 3095 was 2722, checked in by campbell, 7 years ago

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File size: 21.9 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
[487]12definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
[20]13  λv,ty. match v in val with
[961]14  [ Vint sz i ⇒ match ty with
15    [ Tint sz' _ ⇒ intsize_eq_elim ? sz sz' ? i
16                   (λi. OK ? (¬eq_bv ? i (zero ?))) (Error ? (msg TypeMismatch))
[797]17    | _ ⇒ Error ? (msg TypeMismatch)
[20]18    ]
[1545]19  | Vptr _ ⇒ match ty with
[2176]20    [ Tpointer _ ⇒ OK ? true
[797]21    | _ ⇒ Error ? (msg TypeMismatch)
[20]22    ]
[2176]23  | Vnull ⇒ match ty with
24    [ Tpointer _ ⇒ OK ? false
[797]25    | _ ⇒ Error ? (msg TypeMismatch)
[484]26    ]
[797]27  | _ ⇒ Error ? (msg ValueIsNotABoolean)
[250]28  ].
29
[487]30lemma 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.
31#v #ty #r #H elim H; #v #t #H' elim H';
[1516]32  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
[2176]33  | #ptr #ty %{ true} % //
[961]34  | * #sg %{ false} % //
[2176]35  | #t %{ false} % //;
[487]36  ]
37qed.
[20]38
39(* Prove a few minor results to make proof obligations easy. *)
40
[487]41lemma bind_OK: ∀A,B,P,e,f.
[797]42  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
43  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
[487]44#A #B #P #e #f elim e; /2/; qed.
[20]45
[487]46lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
[1603]47  (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
[797]48  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
[487]49#A #B #P #P' #e #f elim e;
50[ #v0 elim v0; #v #Hv #IH @IH
[797]51| #m #_ @I
[487]52] qed.
[20]53
[487]54lemma bind2_OK: ∀A,B,C,P,e,f.
[797]55  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
56  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
[487]57#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
[20]58
[797]59lemma opt_bind_OK: ∀A,B,P,m,e,f.
60  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
61  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
62#A #B #P #m #e #f elim e; normalize; /2/; qed.
[20]63
64
[961]65definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
66λm:mem. λsz. λi. λty:type. λty':type.
67match eq_bv ? i (zero ?) with
[124]68[ true ⇒
69  match ty with
[961]70  [ Tint sz' _ ⇒
71    if eq_intsize sz sz' then
72      match ty' with
[2176]73      [ Tpointer _ ⇒ OK ? Vnull
74      | Tarray _ _ ⇒ OK ? Vnull
75      | Tfunction _ _ ⇒ OK ? Vnull
[961]76      | _ ⇒ Error ? (msg BadCast)
77      ]
78    else Error ? (msg TypeMismatch)
[797]79  | _ ⇒ Error ? (msg BadCast)
[124]80  ]
[797]81| false ⇒ Error ? (msg BadCast)
[250]82].
[124]83
[2176]84definition ptr_like_type : type → bool ≝
85λt. match t with
86[ Tpointer _ ⇒ true
87| Tarray _ _ ⇒ true
88| Tfunction _ _ ⇒ true
89| _ ⇒ false
90].
91
[487]92definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
[189]93λm:mem. λv:val. λty:type. λty':type.
[20]94match v with
[961]95[ Vint sz i ⇒
[20]96  match ty with
97  [ Tint sz1 si1 ⇒
[961]98    intsize_eq_elim ? sz sz1 ? i
99    (λi.
100      match ty' with
[964]101      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
[2468]102(*      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))*)
[2176]103      | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
104      | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[961]105      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
106      | _ ⇒ Error ? (msg BadCast)
107      ])
108    (Error ? (msg BadCast))
[2176]109  | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
110  | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[961]111  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
[797]112  | _ ⇒ Error ? (msg TypeMismatch)
[20]113  ]
[2468]114(*| Vfloat f ⇒
[20]115  match ty with
116  [ Tfloat sz ⇒
117    match ty' with
[961]118    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
[250]119    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
[797]120    | _ ⇒ Error ? (msg BadCast)
[20]121    ]
[797]122  | _ ⇒ Error ? (msg TypeMismatch)
[2468]123  ]*)
[1545]124| Vptr ptr ⇒
[2176]125(*    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
[1545]126    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
[189]127    do s' ← match ty' with
[127]128         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
[797]129         | _ ⇒ Error ? (msg BadCast)];
[1545]130    match pointer_compat_dec (pblock ptr) s' with
131    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
[797]132    | inr _ ⇒ Error ? (msg BadCast)
[2176]133    ]*)
134    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? (Vptr ptr) else Error ? (msg BadCast)
135| Vnull ⇒
136(*
[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) ];
[2176]142    OK ? (Vnull s')*)
143    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? Vnull else Error ? (msg BadCast)
[797]144| _ ⇒ Error ? (msg BadCast)
[250]145].
146
[487]147definition load_value_of_type' ≝
[1599]148λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
[124]149
[1147]150(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
151   a structurally smaller value, we break out the surrounding Expr constructor
152   and use exec_lvalue'. *)
153
[487]154let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
[20]155match e with
156[ Expr e' ty ⇒
157  match e' with
[961]158  [ Econst_int sz i ⇒
159      match ty with
160      [ Tint sz' _ ⇒
161          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
162          else Error ? (msg BadlyTypedTerm)
163      | _ ⇒ Error ? (msg BadlyTypedTerm)
164      ]
[2468]165(*  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉 *)
[250]166  | Evar _ ⇒
[189]167      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]168      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]169      OK ? 〈v,tr〉
170  | Ederef _ ⇒
[189]171      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]172      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]173      OK ? 〈v,tr〉
174  | Efield _ _ ⇒
[189]175      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
[797]176      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
[250]177      OK ? 〈v,tr〉
178  | Eaddrof a ⇒
[498]179      do 〈lo,tr〉 ← exec_lvalue ge en m a;
180      match ty with
[2176]181      [ Tpointer  _ ⇒
[1599]182        let 〈loc,ofs〉 ≝ lo in
[2176]183(*          match pointer_compat_dec loc r with
[1545]184          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
[797]185          | inr _ ⇒ Error ? (msg TypeMismatch)
[2176]186          ]*)  OK ? 〈Vptr (mk_pointer loc ofs), tr〉
[797]187      | _ ⇒ Error ? (msg BadlyTypedTerm)
[498]188      ]
[961]189  | Esizeof ty' ⇒
190      match ty with
191      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
192      | _ ⇒ Error ? (msg BadlyTypedTerm)
193      ]
[250]194  | Eunop op a ⇒
[189]195      do 〈v1,tr〉 ← exec_expr ge en m a;
[797]196      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
[250]197      OK ? 〈v,tr〉
198  | Ebinop op a1 a2 ⇒
[189]199      do 〈v1,tr1〉 ← exec_expr ge en m a1;
200      do 〈v2,tr2〉 ← exec_expr ge en m a2;
[2588]201      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty);
[250]202      OK ? 〈v,tr1⧺tr2〉
203  | Econdition a1 a2 a3 ⇒
[189]204      do 〈v,tr1〉 ← exec_expr ge en m a1;
[250]205      do b ← exec_bool_of_val v (typeof a1);
[189]206      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
[175]207                 [ true ⇒ (exec_expr ge en m a2)
[189]208                 | false ⇒ (exec_expr ge en m a3) ];
[250]209      OK ? 〈v',tr1⧺tr2〉
[20]210(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
[250]211  | Eorbool a1 a2 ⇒
[189]212      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]213      do b1 ← exec_bool_of_val v1 (typeof a1);
[2588]214      match b1 return λ_.res (val×trace) with
215      [ true ⇒
216        match cast_bool_to_target ty (Some ? Vtrue) with
217        [ None ⇒
218          Error ? (msg BadlyTypedTerm)
219        | Some vtr ⇒
220          OK ? 〈vtr,tr1〉 ]
221      | false ⇒
[189]222        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]223        do b2 ← exec_bool_of_val v2 (typeof a2);
[2588]224        match cast_bool_to_target ty (Some ? (of_bool b2)) with
225        [ None ⇒
226          Error ? (msg BadlyTypedTerm)
227        | Some v2 ⇒
228          OK ? 〈v2,tr1⧺tr2〉 ] ]
[250]229  | Eandbool a1 a2 ⇒
[189]230      do 〈v1,tr1〉 ← exec_expr ge en m a1;
[250]231      do b1 ← exec_bool_of_val v1 (typeof a1);
[2588]232      match b1 return λ_.res (val×trace) with
233      [ true ⇒
[189]234        do 〈v2,tr2〉 ← exec_expr ge en m a2;
[250]235        do b2 ← exec_bool_of_val v2 (typeof a2);
[2588]236        match cast_bool_to_target ty (Some ? (of_bool b2)) with
237        [ None ⇒
238          Error ? (msg BadlyTypedTerm)
239        | Some v2 ⇒
240          OK ? 〈v2, tr1⧺tr2〉
241        ]
242      | false ⇒
243        match cast_bool_to_target ty (Some ? Vfalse) with
244        [ None ⇒
245          Error ? (msg BadlyTypedTerm)
246        | Some vfls ⇒
247          OK ? 〈vfls,tr1〉 ]
248      ]
[250]249  | Ecast ty' a ⇒
[189]250      do 〈v,tr〉 ← exec_expr ge en m a;
251      do v' ← exec_cast m v (typeof a) ty';
[250]252      OK ? 〈v',tr〉
253  | Ecost l a ⇒
[189]254      do 〈v,tr〉 ← exec_expr ge en m a;
[2560]255      OK ? 〈v,(Echarge l)⧺tr〉
[20]256  ]
257]
[583]258and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
[20]259  match e' with
260  [ Evar id ⇒
[1058]261      match (lookup ?? en id) with
[1986]262      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol … ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
[583]263      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
[20]264      ]
[250]265  | Ederef a ⇒
[189]266      do 〈v,tr〉 ← exec_expr ge en m a;
[20]267      match v with
[1545]268      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
[797]269      | _ ⇒ Error ? (msg TypeMismatch)
[250]270      ]
[20]271  | Efield a i ⇒
272      match (typeof a) with
[250]273      [ Tstruct id fList ⇒
[498]274          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
[189]275          do delta ← field_offset i fList;
[2588]276          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I16 delta)〉,tr〉
[250]277      | Tunion id fList ⇒
[498]278          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
279          OK ? 〈lofs,tr〉
[797]280      | _ ⇒ Error ? (msg BadlyTypedTerm)
[20]281      ]
[797]282  | _ ⇒ Error ? (msg BadLvalueTerm)
[20]283  ]
[583]284and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
[20]285match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
[250]286
[487]287lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
288#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
[250]289
[20]290(* TODO: Can we do this sensibly with a map combinator? *)
[487]291let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
[20]292match l with
[251]293[ nil ⇒ OK ? 〈nil val, E0〉
294| cons e1 es ⇒
[189]295  do 〈v,tr1〉 ← exec_expr ge e m e1;
296  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
[251]297  OK ? 〈cons val v vs, tr1⧺tr2〉
298].
[20]299
[487]300let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
[20]301match l with
[487]302[ nil ⇒ 〈en, m〉
[20]303| cons h vars ⇒
[1599]304  let 〈id,ty〉 ≝ h in
[2608]305  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) (* XData *) in
[1058]306      exec_alloc_variables (add ?? en id b1) m1 vars
[1599]307].
[20]308
309(* TODO: can we establish that length params = length vs in advance? *)
[487]310let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
[20]311  match params with
[797]312  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
[1599]313  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
[20]314      match vs with
[797]315      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
[487]316      | cons v1 vl ⇒
[1058]317          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
[797]318          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
[487]319          exec_bind_parameters e m1 params' vl
[20]320      ]
[1599]321  ].
[20]322
[638]323let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
[388]324match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
325[ Kstop ⇒ ?
326| Kcall _ _ _ _ ⇒ ?
327| _ ⇒ ?
328].
[487]329[ 1,8: %1 ; //
330| *: %2 ; /2/
331] qed.
[20]332
[891]333definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
334λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
[388]335[ Sskip ⇒ inl ?? (refl ??)
336| _ ⇒ inr ?? (nmk ? (λH.?))
[487]337]. destruct
338qed.
[388]339
[20]340
341(* execution *)
342
[487]343definition store_value_of_type' ≝
[124]344λty,m,l,v.
[1599]345let 〈loc,ofs〉 ≝ l in
346  store_value_of_type ty m loc ofs v.
[124]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 ⇒
[1647]353    ! 〈l,tr1〉 ← exec_lvalue ge e m a1 : IO ???;
354    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
[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 ⇒
[1647]358    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
359    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
[2722]360    ! 〈fd,id〉 ← opt_to_io … (msg BadFunctionValue) (find_funct_id … 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
[2722]372         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate id fd vargs (Kcall (None ?) f e k) m〉
[20]373         | Some lhs' ⇒
[1647]374           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
[2722]375           ret ? 〈tr1⧺tr2⧺tr3, Callstate id 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
[1988]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
[1988]388          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
[797]389          | _ ⇒ Wrong ??? (msg NonsenseState)
[20]390          ]
[2391]391      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
[252]392      | Kdowhile a s' k' ⇒
[1647]393          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[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〉
[2391]407      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
[252]408      | Kdowhile a s' k' ⇒
[1647]409          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[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〉
[2391]422      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
[252]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 ⇒
[1647]429      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[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〉
[2391]432  | Swhile a s' ⇒
[1647]433      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[250]434      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
[2391]435      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
436                      else State f Sskip k e m〉
[252]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 _ ⇒
[1647]441          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
[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
[1988]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 _ ⇒
[1647]456          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[1988]457          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
[388]458        ]
[20]459    ]
[252]460  | Sswitch a sl ⇒
[1647]461      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
[2428]462      match v with
463      [ Vint sz n ⇒
464        match typeof a with
465        [ Tint sz' _ ⇒
466          match sz_eq_dec sz sz' with
467          [ inl _ ⇒
468            ! sl' ← opt_to_io … (msg TypeMismatch) (select_switch sz n sl);
469            ret ? 〈tr, State f (seq_of_labeled_statement sl') (Kswitch k) e m〉
470          | _ ⇒ Wrong ??? (msg TypeMismatch)
471          ]
472        | _ ⇒ Wrong ??? (msg TypeMismatch)
473        ]
474      | _ ⇒ Wrong ??? (msg TypeMismatch)]
[252]475  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
[20]476  | Sgoto lbl ⇒
477      match find_label lbl (fn_body f) (call_cont k) with
[1599]478      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
[797]479      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
[20]480      ]
[252]481  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
[20]482  ]
[2677]483| Callstate _ f0 vargs k m ⇒
[20]484  match f0 with
[725]485  [ CL_Internal f ⇒
[1599]486    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
[1647]487      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
[20]488      ret ? 〈E0, State f (fn_body f) k e m2〉
[725]489  | CL_External f argtys retty ⇒
[1647]490      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
[366]491      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
492      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
[20]493  ]
494| Returnstate res k m ⇒
495  match k with
496  [ Kcall r f e k' ⇒
497    match r with
[389]498    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
[20]499    | Some r' ⇒
[1599]500      let 〈l,ty〉 ≝ r' in
[797]501          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
[252]502          ret ? 〈E0, (State f Sskip k' e m')〉
[20]503    ]
[1713]504  | Kstop ⇒
505    match res with
506    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
507    | _ ⇒ Wrong ??? (msg ReturnMismatch)
508    ]
[797]509  | _ ⇒ Wrong ??? (msg NonsenseState)
[20]510  ]
[1713]511| Finalstate r ⇒
512    Wrong ??? (msg NonsenseState)
[252]513].
514
[1244]515definition make_global : clight_program → genv ≝
[1986]516λp. globalenv … (fst ??) p.
[1231]517
518let rec make_initial_state (p:clight_program) : res state ≝
519  let ge ≝ make_global p in
[1986]520  do m0 ← init_mem … (fst ??) p;
521  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
522  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
[2722]523  OK ? (Callstate (prog_main ?? p) f (nil ?) Kstop m0).
[250]524
[708]525let rec is_final (s:state) : option int ≝
526match s with
[1713]527[ Finalstate r ⇒ Some ? r
[708]528| _ ⇒ None ?
529].
530
[487]531definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
532#st elim st;
533[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
[2677]534| #vf #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
[1713]535| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
536| #r %1 %{r} %
[487]537] qed.
[20]538
[487]539let rec exec_steps (n:nat) (ge:genv) (s:state) :
[366]540 IO io_out io_in (trace×state) ≝
[20]541match is_final_state s with
[252]542[ inl _ ⇒ ret ? 〈E0, s〉
[20]543| inr _ ⇒
544  match n with
[252]545  [ O ⇒ ret ? 〈E0, s〉
546  | S n' ⇒
[208]547      ! 〈t,s'〉 ← exec_step ge s;
[1147]548      ! 〈t',s''〉 ← exec_steps n' ge s';
[252]549      ret ? 〈t ⧺ t',s''〉
[20]550  ]
[252]551].
[1713]552(*
[487]553definition mem_of_state : state → mem ≝
[291]554λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
[1713]555*)
[1231]556definition clight_exec : trans_system io_out io_in ≝
557  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
[239]558
[731]559definition clight_fullexec : fullexec io_out io_in ≝
[1231]560  mk_fullexec ??? clight_exec make_global make_initial_state.
[2203]561
562
563(* A few lemmas about the semantics. *)
564
565lemma cl_step_not_final : ∀ge,s1,tr,s2.
566  exec_step ge s1 = OK … 〈tr,s2〉 →
567  is_final s1 = None ?.
568#ge * //
569#r #tr #s2 #E
570whd in E:(??%%);
571destruct
572qed.
573
574(* If you can step in Clight, then you aren't in a final state.  Hence we can
575   give nicer constructors for plus. *)
576lemma cl_plus_one : ∀ge,s1,tr,s2.
577  exec_step ge s1 = OK … 〈tr,s2〉 →
578  plus … clight_exec ge s1 tr s2.
579#ge #s1 #tr #s2 #EX @(plus_one … EX) /2/
580qed.
581
582lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3.
583    exec_step ge s1 = OK … 〈tr,s2〉 →
584    plus … clight_exec ge s2 tr' s3 →
585    plus … clight_exec ge s1 (tr⧺tr') s3.
586#ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX
587qed.
588
Note: See TracBrowser for help on using the repository browser.