Changeset 250


Ignore:
Timestamp:
Nov 22, 2010, 2:40:22 PM (9 years ago)
Author:
campbell
Message:

Begin separating soundness from executable semantics.

Location:
C-semantics
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r245 r250  
    3838  on _c:sigma ? ? to ?.
    3939
    40 ndefinition bool_of_val_3 : ∀v:val. ∀ty:type. res (Σr:bool. bool_of_val v ty (of_bool r)) ≝
     40ndefinition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
     41  λA,P,a. match a with [ Error ⇒ True | OK v ⇒ P v ].
     42
     43ndefinition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
    4144  λv,ty. match v in val with
    4245  [ Vint i ⇒ match ty with
    43     [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    44     | Tpointer _ _ ⇒ Some ? (OK ? (¬eq i zero))
    45     | _ ⇒ Some ? (Error ?)
     46    [ Tint _ _ ⇒ OK ? (¬eq i zero)
     47    | Tpointer _ _ ⇒ OK ? (¬eq i zero)
     48    | _ ⇒ Error ?
    4649    ]
    4750  | Vfloat f ⇒ match ty with
    48     [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
    49     | _ ⇒ Some ? (Error ?)
     51    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
     52    | _ ⇒ Error ?
    5053    ]
    5154  | Vptr _ _ _ ⇒ match ty with
    52     [ Tint _ _ ⇒ Some ? (OK ? true)
    53     | Tpointer _ _ ⇒ Some ? (OK ? true)
    54     | _ ⇒ Some ? (Error ?)
     55    [ Tint _ _ ⇒ OK ? true
     56    | Tpointer _ _ ⇒ OK ? true
     57    | _ ⇒ Error ?
    5558    ]
    56   | _ ⇒ Some ? (Error ?)
    57   ]. nwhd; //;
    58 ##[ ##1,2: nlapply (eq_spec c0 zero); nelim (eq c0 zero);
     59  | _ ⇒ Error ?
     60  ].
     61
     62nlemma exec_bool_of_val_sound: ∀v,ty,r.
     63 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
     64#v ty r;
     65ncases v; ##[ ##2: #i ##| ##3: #f ##| ##4: #sp b of ##]
     66nwhd; ##[ ##4: #H; nwhd in H:(??%?); ndestruct ##]
     67ncases ty; ##[ ##2,11,20: #sz sg ##| ##3,12,21: #sz ##| ##4,13,22: #sp ty ##| ##5,14,23: #sp ty n ##| ##6,15,24: #args rty ##| ##7,8,16,17,25,26: #id fs ##| ##9,18,27: #id ##]
     68#H; nwhd in H:(??%?); ndestruct;
     69##[ ##1,4: nlapply (eq_spec i zero); nelim (eq i zero);
    5970  ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //;
    6071  ##| ##2,4: #ne; napply bool_of_val_true; /2/;
    6172  ##]
    62 ##| nelim (eq_dec c0 Fzero);
     73##| ##3: nelim (eq_dec f Fzero);
    6374  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
    6475  ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
    6576  ##]
    66 ##| ##4,5: napply bool_of_val_true; //
     77##| ##2,5: napply bool_of_val_true; //
    6778##] nqed.
    6879
    69 ndefinition err_eq ≝ λA,P. λx:res (sigma A P). λy:A.
    70   match x with [ Error ⇒ False | OK x' ⇒
    71     match x' with [ sig_intro x'' _ ⇒ x'' = y ]].
    72 (* TODO: can I write a coercion for the above? *)
    73 
    74 (* Same as before, except we have to use a slightly different "equality". *)
    75 
    76 nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ err_eq ?? (bool_of_val_3 v ty) b.
     80nlemma 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.
    7781#v ty r H; nelim H; #v t H'; nelim H';
    78   ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
     82  ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    7983  ##| #p b i i0 s; @ true; @; //
    80   ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
     84  ##| #i p t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    8185  ##| #p b i p0 t0; @ true; @; //
    82   ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    83   ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    84   ##| #p t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    85   ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
     86  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
     87  ##| #i s; @ false; @; //;
     88  ##| #p t; @ false; @; //;
     89  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    8690  ##]
    8791nqed.
     
    117121#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
    118122
    119 nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P').
    120   (∀v:A. err_eq A P' e v → P' v → P v) →
    121   match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ].
    122 #A P P' e; ncases e; //;
    123 #v0; nelim v0; #v Pv' IH; /2/;
    124 nqed.
    125 
    126123nlemma bool_val_distinct: Vtrue ≠ Vfalse.
    127124@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
     
    160157*)
    161158
    162 nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) on i : res (Σv':val. cast m (Vint i) ty ty' v') ≝
     159ndefinition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
     160λm:mem. λi:int. λty:type. λty':type.
    163161match eq i zero with
    164162[ true ⇒
     
    166164  [ Tint _ _ ⇒
    167165    match ty' with
    168     [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    169     | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    170     | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    171     | _ ⇒ Some ? (Error ?)
     166    [ Tpointer _ _ ⇒ OK ? (Vint i)
     167    | Tarray _ _ _ ⇒ OK ? (Vint i)
     168    | Tfunction _ _ ⇒ OK ? (Vint i)
     169    | _ ⇒ Error ?
    172170    ]
    173171  | Tpointer _ _ ⇒
    174172    match ty' with
    175     [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    176     | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    177     | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    178     | _ ⇒ Some ? (Error ?)
     173    [ Tpointer _ _ ⇒ OK ? (Vint i)
     174    | Tarray _ _ _ ⇒ OK ? (Vint i)
     175    | Tfunction _ _ ⇒ OK ? (Vint i)
     176    | _ ⇒ Error ?
    179177    ]
    180178  | Tarray _ _ _ ⇒
    181179    match ty' with
    182     [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    183     | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    184     | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    185     | _ ⇒ Some ? (Error ?)
     180    [ Tpointer _ _ ⇒ OK ? (Vint i)
     181    | Tarray _ _ _ ⇒ OK ? (Vint i)
     182    | Tfunction _ _ ⇒ OK ? (Vint i)
     183    | _ ⇒ Error ?
    186184    ]
    187185  | Tfunction _ _ ⇒
    188186    match ty' with
    189     [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
    190     | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
    191     | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
    192     | _ ⇒ Some ? (Error ?)
     187    [ Tpointer _ _ ⇒ OK ? (Vint i)
     188    | Tarray _ _ _ ⇒ OK ? (Vint i)
     189    | Tfunction _ _ ⇒ OK ? (Vint i)
     190    | _ ⇒ Error ?
    193191    ]
    194   | _ ⇒ Some ? (Error ?)
     192  | _ ⇒ Error ?
    195193  ]
    196 | false ⇒ Some ? (Error ?)
    197 ]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
    198    ##[ ##1,2,3: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //; nqed.
     194| false ⇒ Error ?
     195].
     196
     197nlemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'.
     198#m i ty ty' v';
     199nwhd in ⊢ (??%? → ?);
     200nlapply (eq_spec i zero); ncases (eq i zero);
     201##[ #e; nrewrite > e;
     202    ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #id ##]
     203    nwhd in ⊢ (??%? → ?); ##[ ##1,3,7,8,9: #H; ndestruct ##]
     204    ncases ty'; ##[ ##2,11,20,29: #sz' sg' ##| ##3,12,21,30: #sz' ##| ##4,13,22,31: #sp' ty' ##| ##5,14,23,32: #sp' ty' n' ##| ##6,15,24,33: #args' res' ##| ##7,8,16,17,25,26,34,35: #id' fs' ##| ##9,18,27,36: #id' ##]
     205    nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
     206    ##[ ##1,5,9: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //;
     207##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct
     208##]
     209nqed.
    199210
    200211ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
    201212#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    202213
    203 ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res (Σv':val. cast m v ty ty' v')
     214ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val
    204215λm:mem. λv:val. λty:type. λty':type.
    205216match v with
     
    208219  [ Tint sz1 si1 ⇒
    209220    match ty' with
    210     [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
    211     | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
    212     | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    213     | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    214     | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    215     | _ ⇒ Some ? (Error ?)
     221    [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i))
     222    | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
     223    | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     224    | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     225    | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     226    | _ ⇒ Error ?
    216227    ]
    217   | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    218   | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    219   | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    220   | _ ⇒ Some ? (Error ?)
     228  | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     229  | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     230  | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
     231  | _ ⇒ Error ?
    221232  ]
    222233| Vfloat f ⇒
     
    224235  [ Tfloat sz ⇒
    225236    match ty' with
    226     [ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))))
    227     | Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f)))
    228     | _ ⇒ Some ? (Error ?)
     237    [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
     238    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
     239    | _ ⇒ Error ?
    229240    ]
    230   | _ ⇒ Some ? (Error ?)
     241  | _ ⇒ Error ?
    231242  ]
    232243| Vptr p b ofs ⇒
    233   Some ? (
    234244    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    235245    do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];
     
    239249    if is_pointer_compat (block_space m b) s'
    240250    then OK ? (Vptr s' b ofs)
    241     else Error ?)
    242 | _ ⇒ Some ? (Error ?)
    243 ]. nwhd; //;
    244 ##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H;
    245 ##| napply bind_OK; #s es;
     251    else Error ?
     252| _ ⇒ Error ?
     253].
     254
     255ndefinition exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
     256#m v ty ty' v';
     257ncases v;
     258##[ #H; nwhd in H:(??%?); ndestruct;
     259##| #i; ncases ty;
     260  ##[ #H; nwhd in H:(??%?); ndestruct;
     261  ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct;
     262  ##| ##7,8: #a b; #H; nwhd in H:(??%?); ndestruct;
     263  ##| #sz1 si1; ncases ty';
     264    ##[ #H; nwhd in H:(??%?); ndestruct;
     265    ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct; //
     266    ##| ##2,7,8: #a b; #H; nwhd in H:(??%?); ndestruct; //
     267    ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
     268                 ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
     269                 ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
     270        nwhd in ⊢ (??%? → ?);
     271        nlapply (try_cast_null_sound m i (Tint sz1 si1) t v');
     272        ncases (try_cast_null m i (Tint sz1 si1) t);
     273        ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
     274        ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
     275        ##]
     276    ##]
     277  ##| ##*: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
     278           ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
     279           ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
     280        nwhd in ⊢ (??%? → ?);
     281        nlapply (try_cast_null_sound m i t ty' v');
     282        ncases (try_cast_null m i t ty');
     283        ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
     284        ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
     285        ##]
     286  ##]
     287##| #f; ncases ty;  ##[ ##3,9: #x; ##| ##2,4,6,7,8: #x y; ##| ##5: #x y z; ##]
     288                    ##[ ncases ty'; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     289                        nwhd in e:(??%?); ndestruct; //;
     290                    ##| ##*: #e; nwhd in e:(??%?); ndestruct
     291                    ##]
     292##| #sp b of; nwhd in ⊢ (??%? → ?); #e;
     293    nelim (bind_inversion ????? e); #s; *; #es e';
     294    nelim (bind_inversion ????? e'); #u; *; #eu e'';
     295    nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    246296    ncut (type_space ty s);
    247     ##[ ncases ty in es ⊢ %;
    248       ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] nwhd in e:(??%?); ndestruct; //;
     297    ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     298        nwhd in e:(??%?); ndestruct; //;
    249299    ##| #Hty;
    250         napply bind_OK; #u1 eeq;
    251         napply bind_OK; #s' es';
    252300        ncut (type_space ty' s');
    253301        ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    254302            nwhd in e:(??%?); ndestruct; //;
    255303        ##| #Hty';
    256             ncut (s = c0). nelim (ms_eq_dec c0 s) in eeq; //; nnormalize; #_; #e; ndestruct.
     304            ncut (s = sp). nelim (ms_eq_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.
    257305            #e; nrewrite < e;
    258             nwhd in match (is_pointer_compat ??) in ⊢ %;
    259             ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
    260             nwhd; /2/;
     306            nwhd in match (is_pointer_compat ??) in e''';
     307            ncases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat e''';
     308            nwhd in e''':(??%?); ndestruct (e'''); /2/
    261309        ##]
    262310    ##]
     
    271319   and use exec_lvalue'. *)
    272320
    273 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val×trace. eval_expr ge en m e (\fst r) (\snd r)) ≝
     321nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
    274322match e with
    275323[ Expr e' ty ⇒
    276324  match e' with
    277   [ Econst_int i ⇒ Some ? (OK ? 〈Vint i, E0〉)
    278   | Econst_float f ⇒ Some ? (OK ? 〈Vfloat f, E0〉)
    279   | Evar _ ⇒ Some ? (
     325  [ Econst_int i ⇒ OK ? 〈Vint i, E0〉
     326  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
     327  | Evar _ ⇒
    280328      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    281329      do v ← opt_to_res ? (load_value_of_type' ty m l);
    282       OK ? 〈v,tr〉)
    283   | Ederef _ ⇒ Some ? (
     330      OK ? 〈v,tr〉
     331  | Ederef _ ⇒
    284332      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    285333      do v ← opt_to_res ? (load_value_of_type' ty m l);
    286       OK ? 〈v,tr〉)
    287   | Efield _ _ ⇒ Some ? (
     334      OK ? 〈v,tr〉
     335  | Efield _ _ ⇒
    288336      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    289337      do v ← opt_to_res ? (load_value_of_type' ty m l);
    290       OK ? 〈v,tr〉)
    291   | Eaddrof a ⇒ Some ? (
     338      OK ? 〈v,tr〉
     339  | Eaddrof a ⇒
    292340      do 〈plo,tr〉 ← exec_lvalue ge en m a;
    293       OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉)
    294   | Esizeof ty' ⇒ Some ? (OK ? 〈Vint (repr (sizeof ty')), E0〉)
    295   | Eunop op a ⇒ Some ? (
     341      OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉
     342  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
     343  | Eunop op a ⇒
    296344      do 〈v1,tr〉 ← exec_expr ge en m a;
    297345      do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
    298       OK ? 〈v,tr〉)
    299   | Ebinop op a1 a2 ⇒ Some ? (
     346      OK ? 〈v,tr〉
     347  | Ebinop op a1 a2 ⇒
    300348      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    301349      do 〈v2,tr2〉 ← exec_expr ge en m a2;
    302350      do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
    303       OK ? 〈v,tr1⧺tr2〉)
    304   | Econdition a1 a2 a3 ⇒ Some ? (
     351      OK ? 〈v,tr1⧺tr2〉
     352  | Econdition a1 a2 a3 ⇒
    305353      do 〈v,tr1〉 ← exec_expr ge en m a1;
    306       do b ← bool_of_val_3 v (typeof a1);
     354      do b ← exec_bool_of_val v (typeof a1);
    307355      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
    308356                 [ true ⇒ (exec_expr ge en m a2)
    309357                 | false ⇒ (exec_expr ge en m a3) ];
    310       OK ? 〈v',tr1⧺tr2〉)
     358      OK ? 〈v',tr1⧺tr2〉
    311359(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
    312   | Eorbool a1 a2 ⇒ Some ? (
     360  | Eorbool a1 a2 ⇒
    313361      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    314       do b1 ← bool_of_val_3 v1 (typeof a1);
     362      do b1 ← exec_bool_of_val v1 (typeof a1);
    315363      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
    316364        do 〈v2,tr2〉 ← exec_expr ge en m a2;
    317         do b2 ← bool_of_val_3 v2 (typeof a2);
    318         OK ? 〈of_bool b2, tr1⧺tr2〉 ])
    319   | Eandbool a1 a2 ⇒ Some ? (
     365        do b2 ← exec_bool_of_val v2 (typeof a2);
     366        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
     367  | Eandbool a1 a2 ⇒
    320368      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    321       do b1 ← bool_of_val_3 v1 (typeof a1);
     369      do b1 ← exec_bool_of_val v1 (typeof a1);
    322370      match b1 return λ_.res (val×trace) with [ true ⇒
    323371        do 〈v2,tr2〉 ← exec_expr ge en m a2;
    324         do b2 ← bool_of_val_3 v2 (typeof a2);
     372        do b2 ← exec_bool_of_val v2 (typeof a2);
    325373        OK ? 〈of_bool b2, tr1⧺tr2〉
    326       | false ⇒ OK ? 〈Vfalse,tr1〉 ])
    327   | Ecast ty' a ⇒ Some ? (
     374      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
     375  | Ecast ty' a ⇒
    328376      do 〈v,tr〉 ← exec_expr ge en m a;
    329377      do v' ← exec_cast m v (typeof a) ty';
    330       OK ? 〈(* XXX *)sig_eject ?? v',tr〉)
    331   | Ecost l a ⇒ Some ? (
     378      OK ? 〈v',tr〉
     379  | Ecost l a ⇒
    332380      do 〈v,tr〉 ← exec_expr ge en m a;
    333       OK ? 〈v,tr⧺(Echarge l)〉)
     381      OK ? 〈v,tr⧺(Echarge l)〉
    334382  ]
    335383]
    336 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
     384and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (memory_space × block × int × trace) ≝
    337385  match e' with
    338386  [ Evar id ⇒
    339387      match (get … id en) with
    340       [ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
    341       | Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)
     388      [ None ⇒ do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉 (* global *)
     389      | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *)
    342390      ]
    343   | Ederef a ⇒ Some ? (
     391  | Ederef a ⇒
    344392      do 〈v,tr〉 ← exec_expr ge en m a;
    345393      match v with
    346394      [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
    347395      | _ ⇒ Error ?
    348       ])
     396      ]
    349397  | Efield a i ⇒
    350398      match (typeof a) with
    351       [ Tstruct id fList ⇒ Some ? (
     399      [ Tstruct id fList ⇒
    352400          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
    353401          do delta ← field_offset i fList;
    354           OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉)
    355       | Tunion id fList ⇒ Some ? (
     402          OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉
     403      | Tunion id fList ⇒
    356404          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
    357           OK ? 〈plofs,tr〉)
    358       | _ ⇒ Some ? (Error ?)
     405          OK ? 〈plofs,tr〉
     406      | _ ⇒ Error ?
    359407      ]
    360   | _ ⇒ Some ? (Error ?)
     408  | _ ⇒ Error ?
    361409  ]
    362 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
     410and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (memory_space × block × int × trace) ≝
    363411match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    364 nwhd;
    365 ##[ ##1,2: //
    366 ##| ##3,4:
    367     napply sig_bind2_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    368     napply opt_bind_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
    369 ##| napply sig_bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    370     nwhd; napply eval_Eaddrof; //;
    371 ##| napply sig_bind2_OK; #v1 tr Hv1;
     412
     413nlemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
     414#A P e v H1 H2; nrewrite > H2 in H1; nwhd in ⊢ (% → ?); //; nqed.
     415
     416nlemma exec_expr_sound_0: ∀ge:genv. ∀en:env. ∀m:mem.
     417(∀e,ty. P_res ? (λx.eval_lvalue ge en m (Expr e ty) (\fst (\fst (\fst x))) (\snd (\fst (\fst x))) (\snd (\fst x)) (\snd x)) (exec_lvalue' ge en m e ty)) →
     418∀e:expr. P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e).
     419#ge en m lvalue_sound e; ncases e; #e' ty; ncases e';
     420##[ ##1,2: #c; nwhd; //;
     421##| ##3,4: #z; nwhd in ⊢ (???%);
     422    napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
     423    napply opt_bind_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … ev);
     424    napply (P_res_to_P … (lvalue_sound ??) H);
     425##| #e''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
     426    nwhd; napply eval_Eaddrof; ncases e'' in H ⊢ %; #e0 ty0 H; napply (P_res_to_P … (lvalue_sound ??) H);
     427##| #op e1; napply bind2_OK; #v1 tr Hv1;
    372428    napply opt_bind_OK; #v ev;
    373     napply (eval_Eunop … Hv1 ev);
     429    napply (eval_Eunop … ev);
    374430##| napply sig_bind2_OK; #v1 tr1 Hv1;
    375431    napply sig_bind2_OK; #v2 tr2 Hv2;
     
    377433    napply (eval_Ebinop … Hv1 Hv2 ev);
    378434##| napply sig_bind2_OK; #v tr Hv;
    379     napply sig_bind_OK; #v' Hv';
    380     napply (eval_Ecast … Hv Hv');
     435    napply bind_OK; #v' ev';
     436    napply (eval_Ecast … Hv ?);
     437    /2/;
    381438##| napply sig_bind2_OK; #vb tr1 Hvb;
    382     napply sig_bind_OK; #b;
    383     ncases b; #Hb; napply sig_bind2_OK; #v tr Hv;
     439    napply bind_OK; #b;
     440    ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     441    napply sig_bind2_OK; #v tr Hv;
    384442    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    385443    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    386444    ##]
    387445##| napply sig_bind2_OK; #v1 tr1 Hv1;
    388     napply sig_bind_OK; #b1; ncases b1; #Hb1;
     446    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    389447    ##[ napply sig_bind2_OK; #v2 tr2 Hv2;
    390         napply sig_bind_OK; #b2 Hb2;
     448        napply bind_OK; #b2 eb2;
    391449        napply (eval_Eandbool_2 … Hv1 … Hv2);
    392         ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
     450        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    393451    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    394452    ##]
    395453##| napply sig_bind2_OK; #v1 tr1 Hv1;
    396     napply sig_bind_OK; #b1; ncases b1; #Hb1;
     454    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    397455    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    398456    ##| napply sig_bind2_OK; #v2 tr2 Hv2;
    399         napply sig_bind_OK; #b2 Hb2;
     457        napply bind_OK; #b2 eb2;
    400458        napply (eval_Eorbool_2 … Hv1 … Hv2);
    401         ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
     459        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    402460    ##]
    403461##| //
     
    420478##| //
    421479##] nqed.
     480and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
     481and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
    422482
    423483(* TODO: Can we do this sensibly with a map combinator? *)
     
    470530napply opt_bind_OK; #b eb;
    471531napply opt_bind_OK; #m1 em1;
    472 napply reinject; #m2 em2 Hm2;
     532napply sig_bind_OK; #m2 Hm2;
    473533napply (bind_parameters_cons … eb em1 Hm2);
    474534nqed.
     
    670730      | Kdowhile a s' k' ⇒ Some ? (
    671731          ! 〈v,tr〉 ← exec_expr ge e m a;
    672           ! b ← bool_of_val_3 v (typeof a);
     732          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    673733          match b with
    674734          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
     
    686746      | Kdowhile a s' k' ⇒ Some ? (
    687747          ! 〈v,tr〉 ← exec_expr ge e m a;
    688           ! b ← bool_of_val_3 v (typeof a);
     748          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    689749          match b with
    690750          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
     
    706766  | Sifthenelse a s1 s2 ⇒ Some ? (
    707767      ! 〈v,tr〉 ← exec_expr ge e m a;
    708       ! b ← bool_of_val_3 v (typeof a);
     768      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    709769      ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
    710770  | Swhile a s' ⇒ Some ? (
    711771      ! 〈v,tr〉 ← exec_expr ge e m a;
    712       ! b ← bool_of_val_3 v (typeof a);
     772      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    713773      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
    714774                      else State f Sskip k e m〉)
     
    718778      [ inl _ ⇒ Some ? (
    719779          ! 〈v,tr〉 ← exec_expr ge e m a2;
    720           ! b ← bool_of_val_3 v (typeof a2);
     780          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
    721781          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
    722782      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
     
    780840##| napply step_skip_or_continue_while; @; //;
    781841##| napply sig_bindIO2_OK; #v tr Hv;
    782     napply sig_bindIO_OK; #b; ncases b; #Hb;
    783     ##[ napply (step_skip_or_continue_dowhile_true … Hv);
    784       ##[ @; // ##| napply (bool_of … Hb); ##]
    785     ##| napply (step_skip_or_continue_dowhile_false … Hv);
    786       ##[ @; // ##| napply (bool_of … Hb); ##]
     842    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
     843    nlapply (refl ? bexpr);
     844    ncases bexpr in ⊢ (???% → %);
     845    ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     846        nwhd in ⊢ (?????%);
     847        ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     848          ##[ @; // ##| napply (bool_of … Hb); ##]
     849        ##| napply (step_skip_or_continue_dowhile_false … Hv);
     850          ##[ @; // ##| napply (bool_of … Hb); ##]
     851        ##]
     852    ##| #_; //;
    787853    ##]
    788854##| napply step_skip_or_continue_for2; @; //;
     
    804870    ##]
    805871##| napply sig_bindIO2_OK; #v tr Hv;
    806     napply sig_bindIO_OK; #b; ncases b; #Hb;
     872    nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
     873    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
     874    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    807875    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
    808876    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
    809877    ##]
    810878##| napply sig_bindIO2_OK; #v tr Hv;
    811     napply sig_bindIO_OK; #b; ncases b; #Hb;
     879    nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
     880    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
     881    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    812882    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
    813883    ##| napply (step_while_false … Hv); napply (bool_of … Hb);
     
    815885##| nrewrite > c11;
    816886    napply sig_bindIO2_OK; #v tr Hv;
    817     napply sig_bindIO_OK; #b; ncases b; #Hb;
     887    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
     888    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
     889    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    818890    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
    819891    ##| napply (step_for_false … Hv); napply (bool_of … Hb);
     
    823895##| napply step_skip_or_continue_while; @2; //;
    824896##| napply sig_bindIO2_OK; #v tr Hv;
    825     napply sig_bindIO_OK; #b; ncases b; #Hb;
     897    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
     898    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
     899    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    826900    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
    827901      ##[ @2; // ##| napply (bool_of … Hb); ##]
     
    849923nqed.
    850924
    851 nlet rec make_initial_state (p:program) : IO eventval io_out (Σs:state. initial_state p s)
     925nlet rec make_initial_state (p:program) : IO eventval io_out state
    852926  let ge ≝ globalenv Genv ?? p in
    853927  let m0 ≝ init_mem Genv ?? p in
    854   Some ? (
    855928    ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);
    856929    ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
    857930    ! f ← find_funct_ptr ? ? ge b;
    858     ret ? (Callstate f (nil ?) Kstop m0)).
    859 nwhd;
     931    ret ? (Callstate f (nil ?) Kstop m0).
     932
     933nlemma make_initial_state_sound : ∀p. P_io ??? (λs.initial_state p s) (make_initial_state p).
     934#p; ncases p; #fns main vars;
     935nwhd in ⊢ (?????%);
    860936napply opt_bindIO2_OK; #sp b esb;
    861937napply opt_bindIO_OK; #u ecode;
     
    9481024
    9491025ndefinition exec_inf : program → execution ≝
    950 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).
     1026λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
    9511027
    9521028nremark execution_cases: ∀e.
  • C-semantics/CexecIOcomplete.ma

    r239 r250  
    6161
    6262ntheorem the_initial_state:
    63   ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s.
     63  ∀p,s. initial_state p s → yieldsIObare ? (make_initial_state p) s.
    6464#p s; ncases p; #fns main globs H;
    65 napply remove_io_sig;
    6665ninversion H;
    6766#b f e1 e2 e3;
     67nwhd in ⊢ (??%?);
    6868nrewrite > e1;
    6969nwhd in ⊢ (??%?);
     
    8484
    8585nlemma cast_complete: ∀m,v,ty,ty',v'.
    86   cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'.
     86  cast m v ty ty' v' → yieldsbare ? (exec_cast m v ty ty') v'.
    8787#m v ty ty' v' H;
    8888nelim H;
     
    9191##| #m i sz sz' sg; napply refl;
    9292##| #m f sz sz'; napply refl;
    93 ##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig;
     93##| #m sp sp' ty ty' b ofs H1 H2 H3;
    9494    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
    9595    nwhd in ⊢ (??%?);
  • C-semantics/Csyntax.ma

    r175 r250  
    888888  and external functions. *)
    889889(* XXX: is this the best way to access these? *)
    890 alias id "ASTint" = "cic:/matita/c-semantics/AST/typ.con(0,1,0)".
    891 alias id "ASTfloat" = "cic:/matita/c-semantics/AST/typ.con(0,2,0)".
     890alias id "ASTint" = "cic:/matita/c-semantics-2/AST/typ.con(0,1,0)".
     891alias id "ASTfloat" = "cic:/matita/c-semantics-2/AST/typ.con(0,2,0)".
    892892
    893893ndefinition typ_of_type : type → typ ≝ λt.
  • C-semantics/Errors.ma

    r189 r250  
    1515
    1616include "datatypes/pairs.ma".
     17include "Plogic/equality.ma".
     18include "Plogic/connectives.ma".
    1719
    1820(* * Error reporting and the error monad. *)
     
    8385 (at level 200, X ident, Y ident, A at level 100, B at level 200)
    8486 : error_monad_scope.
     87*)
     88nremark bind_inversion:
     89  ∀A,B: Type. ∀f: res A. ∀g: A → res B. ∀y: B.
     90  bind ?? f g = OK ? y →
     91  ∃x. f = OK ? x ∧ g x = OK ? y.
     92#A B f g y; ncases f;
     93##[ #a e; @a; nwhd in e:(??%?); /2/;
     94##| #H; nwhd in H:(??%?); ndestruct (H);
     95##] nqed.
    8596
    86 Remark bind_inversion:
    87   forall (A B: Type) (f: res A) (g: A -> res B) (y: B),
    88   bind f g = OK y ->
    89   exists x, f = OK x /\ g x = OK y.
    90 Proof.
    91   intros until y. destruct f; simpl; intros.
    92   exists a; auto.
    93   discriminate.
    94 Qed.
     97nremark bind2_inversion:
     98  ∀A,B,C: Type. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
     99  bind2 ??? f g = OK ? z →
     100  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
     101#A B C f g z; ncases f;
     102##[ #ab; ncases ab; #a b e; @a; @b; nwhd in e:(??%?); /2/;
     103##| #H; nwhd in H:(??%?); ndestruct
     104##] nqed.
    95105
    96 Remark bind2_inversion:
    97   forall (A B C: Type) (f: res (A*B)) (g: A -> B -> res C) (z: C),
    98   bind2 f g = OK z ->
    99   exists x, exists y, f = OK (x, y) /\ g x y = OK z.
    100 Proof.
    101   intros until z. destruct f; simpl.
    102   destruct p; simpl; intros. exists a; exists b; auto.
    103   intros; discriminate.
    104 Qed.
    105 
     106(*
    106107Open Local Scope error_monad_scope.
    107108
  • C-semantics/root

    r3 r250  
    1 baseuri=cic:/matita/c-semantics
     1baseuri=cic:/matita/c-semantics-2
Note: See TracChangeset for help on using the changeset viewer.