Changeset 124 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r25 r124  
    55include "IOMonad.ma".
    66
    7 (* Some experimental definitions for an executable semantics. *)
    8 
    9 ndefinition bool_of_val_1 : val → type → res val ≝
    10   λv,ty. match v with
    11   [ Vint i ⇒ match ty with
    12     [ Tint _ _ ⇒ OK ? (of_bool (¬eq i zero))
    13     | Tpointer _ ⇒ OK ? (of_bool (¬eq i zero))
    14     | _ ⇒ Error ?
    15     ]
    16   | Vfloat f ⇒ match ty with
    17     [ Tfloat _ ⇒ OK ? (of_bool (¬Fcmp Ceq f Fzero))
    18     | _ ⇒ Error ?
    19     ]
    20   | Vptr _ _ ⇒ match ty with
    21     [ Tint _ _ ⇒ OK ? Vtrue
    22     | Tpointer _ ⇒ OK ? Vtrue
    23     | _ ⇒ Error ?
    24     ]
    25   | _ ⇒ Error ?
    26   ].
    27 
    28 (* There's a lot more repetition than I'd like here, in large part because
    29    there's no way to introduce different numbers of hypotheses when doing the
    30    case distinctions. *)
    31 
    32 nlemma bool_of_val_1_ok : ∀v,ty,r. bool_of_val_1 v ty = OK ? r ↔ bool_of_val v ty r.
    33 #v ty r; @;
    34 ##[
    35   nelim v; ##[ #H; nnormalize in H; ndestruct; ##| ##2,3: #x; ##| ##4: #x y; ##]
    36   ncases ty;
    37   ##[ ##1,10,19: #H; nnormalize in H; ndestruct;
    38   ##| #i s; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
    39     ##[ nrewrite > H; nrewrite > (eq_true …); #H';
    40         ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    41         #H''; nrewrite > H''; /2/;
    42     ##| nrewrite > (eq_false …); //; #H';
    43         ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    44         #H''; nrewrite > H''; /3/;
    45     ##]
    46   ##|##3,9,13,18,21,27: #x H; nnormalize in H; ndestruct;
    47   ##| #t; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
    48     ##[ nrewrite > H; nrewrite > (eq_true …); #H';
    49         ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    50         #H''; nrewrite > H''; /2/;
    51     ##| nrewrite > (eq_false …); //; #H';
    52         ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    53         #H''; nrewrite > H''; /3/;
    54     ##]
    55   ##| ##5,6,7,8,11,14,15,16,17,23,24,25,26: #a b H; nnormalize in H; ndestruct;
    56   ##| #f; nwhd in ⊢ (??%? → ?); nelim (eq_dec x Fzero); #H;
    57     ##[ nrewrite > H; nrewrite > (Feq_zero_true …); #H';
    58         ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    59         #H''; nrewrite > H''; /2/;
    60     ##| nrewrite > (Feq_zero_false …); //; #H';
    61         ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    62         #H''; nrewrite > H''; /3/;
    63     ##]
    64   ##| #i s H; nwhd in H:(??%?);
    65       ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
    66       #H'; nrewrite > H'; /2/;
    67   ##| #t H; nwhd in H:(??%?);
    68       ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
    69       #H'; nrewrite > H'; /2/;
    70   ##]
    71 ##| #H; nelim H; #v t H'; nelim H';
    72   ##[ #i is s ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    73   ##| ##2,4: //
    74   ##| #i t ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    75   ##| #f s ne; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    76   ##| #i s; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
    77   ##| #t; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
    78   ##| #s; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    79   ##]
    80 ##] nqed.
    81 
    827include "Plogic/russell_support.ma".
    83 
    84 (* Nicer - we still have to deal with all of the cases, but only need to
    85    introduce the result value, so there's a single case for getting rid of
    86    all the Error goals. *)
    87 
    88 ndefinition bool_of_val_2 : ∀v:val. ∀ty:type. { r : res bool | ∀r'. r = OK ? r' → bool_of_val v ty (of_bool r') } ≝
    89   λv,ty. match v in val with
    90   [ Vint i ⇒ match ty with
    91     [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    92     | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
    93     | _ ⇒ Some ? (Error ?)
    94     ]
    95   | Vfloat f ⇒ match ty with
    96     [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
    97     | _ ⇒ Some ? (Error ?)
    98     ]
    99   | Vptr _ _ ⇒ match ty with
    100     [ Tint _ _ ⇒ Some ? (OK ? true)
    101     | Tpointer _ ⇒ Some ? (OK ? true)
    102     | _ ⇒ Some ? (Error ?)
    103     ]
    104   | _ ⇒ Some ? (Error ?)
    105   ]. nwhd;
    106 ##[ ##3,5: #r; nlapply (eq_spec c0 zero); nelim (eq c0 zero);
    107   ##[ ##1,3: #e H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2,4: ndestruct; // ##] nrewrite > e; /3/;
    108   ##| ##2,4: #ne H; nrewrite > (?:of_bool r=Vtrue);  ##[ ##2,4: ndestruct; // ##] /3/;
    109   ##]
    110 ##| ##13: #r; nelim (eq_dec c0 Fzero);
    111   ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); #H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2: ndestruct; // ##] /2/;
    112   ##| #ne; nrewrite > (Feq_zero_false …); //; #H;
    113       nrewrite > (?:of_bool r=Vtrue);  ##[ ##2: ndestruct; // ##] /3/;
    114   ##]
    115 ##| ##21,23: #r H; nrewrite > (?:of_bool r = Vtrue); ##[ ##2,4: ndestruct; // ##] /2/
    116 ##| ##*: #a b; ndestruct;
    117 ##] nqed.
    118 
    119 (* Same as before, except we have to write eject in because the type for the
    120    equality is left implied, so the coercion isn't used. *)
    121 
    122 nlemma bool_of_val_2_complete : ∀v,ty,r.
    123   bool_of_val v ty r →
    124   ∃b. r = of_bool b ∧ eject ?? (bool_of_val_2 v ty) = OK ? b.
    125 #v ty r H; nelim H; #v t H'; nelim H';
    126   ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    127   ##| #b i i0 s; @ true; @; //
    128   ##| #i t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    129   ##| #b i t0; @ true; @; //
    130   ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    131   ##| #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
    132   ##| #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
    133   ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    134   ##]
    135 nqed.
    136 
    137 
    138 (* Nicer again (after the extra definitions).  Just use sigma type rather than
    139    the subset, but take into account the error monad.  The error cases all
    140    become trivial and we don't have to muck around to get the result. *)
    1418
    1429ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
     
    17542  [ Vint i ⇒ match ty with
    17643    [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    177     | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
     44    | Tpointer _ _ ⇒ Some ? (OK ? (¬eq i zero))
    17845    | _ ⇒ Some ? (Error ?)
    17946    ]
     
    18249    | _ ⇒ Some ? (Error ?)
    18350    ]
    184   | Vptr _ _ ⇒ match ty with
     51  | Vptr _ _ _ ⇒ match ty with
    18552    [ Tint _ _ ⇒ Some ? (OK ? true)
    186     | Tpointer _ ⇒ Some ? (OK ? true)
     53    | Tpointer _ _ ⇒ Some ? (OK ? true)
    18754    | _ ⇒ Some ? (Error ?)
    18855    ]
     
    21077#v ty r H; nelim H; #v t H'; nelim H';
    21178  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    212   ##| #b i i0 s; @ true; @; //
    213   ##| #i t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    214   ##| #b i t0; @ true; @; //
     79  ##| #p b i i0 s; @ true; @; //
     80  ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
     81  ##| #p b i p0 t0; @ true; @; //
    21582  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    21683  ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    217   ##| #t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
     84  ##| #p t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    21885  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
    21986  ##]
     
    23299
    233100nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
    234   (∀v:A. err_eq A P e v → ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
     101  (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
    235102  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
    236 #A B P P' e f; nelim e; //;
    237 #v0; nelim v0; #v Hv IH; napply IH; //; nqed.
     103#A B P P' e f; nelim e;
     104##[ #v0; nelim v0; #v Hv IH; napply IH;
     105##| #_; napply I;
     106##] nqed.
    238107
    239108nlemma bind2_OK: ∀A,B,C,P,e,f.
     
    286155##] nqed.
    287156
    288 nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝
    289 match ty with
    290 [ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something) | _ ⇒ Some ? (Error ?) ]
    291 | Tpointer _ ⇒ Some ? (OK ? something)
    292 | Tarray _ _ ⇒ Some ? (OK ? something)
    293 | Tfunction _ _ ⇒ Some ? (OK ? something)
    294 | _ ⇒ Some ? (Error ?)
    295 ]. nwhd; //; nqed.
    296157(*
    297158nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
     
    299160*)
    300161
    301 nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝
     162nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) : res (Σv':val. cast m (Vint i) ty ty' v') ≝
     163match eq i zero with
     164[ true ⇒
     165  match ty with
     166  [ Tpointer _ _ ⇒
     167    match ty' with
     168    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     169    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     170    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     171    | _ ⇒ Some ? (Error ?)
     172    ]
     173  | Tarray _ _ _ ⇒
     174    match ty' with
     175    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     176    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     177    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     178    | _ ⇒ Some ? (Error ?)
     179    ]
     180  | Tfunction _ _ ⇒
     181    match ty' with
     182    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     183    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     184    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     185    | _ ⇒ Some ? (Error ?)
     186    ]
     187  | _ ⇒ Some ? (Error ?)
     188  ]
     189| false ⇒ Some ? (Error ?)
     190]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
     191   napply cast_pp_z; //; nqed.
     192
     193nlet rec exec_cast (m:mem) (v:val) (ty:type) (ty':type) : res (Σv':val. cast m v ty ty' v') ≝
    302194match v with
    303195[ Vint i ⇒
     
    307199    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
    308200    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
    309     (* no change in data repr *)
    310     | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
    311     ]
    312   | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
     201    | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     202    | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     203    | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     204    | _ ⇒ Some ? (Error ?)
     205    ]
     206  | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     207  | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     208  | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     209  | _ ⇒ Some ? (Error ?)
    313210  ]
    314211| Vfloat f ⇒
     
    322219  | _ ⇒ Some ? (Error ?)
    323220  ]
    324 | Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs))
     221| Vptr p b ofs ⇒
     222  Some ? (
     223    p ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
     224    s' ← match ty' with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
     225    if is_class_compat (blockclass m b) (ptr_spc_cls s')
     226    then OK ? (Vptr (ptr_spc_cls s') b ofs)
     227    else Error ?)
     228  (* XXX: maybe should allow some Tint? *)
    325229| _ ⇒ Some ? (Error ?)
    326 ]. ndestruct; /2/;
    327 ##[ ##1,2,3: ncases c2; //; napply cast_nn_i; //
    328 ##| ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //;
    329 ##| napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H';
    330     napply cast_nn_p; //
     230]. nwhd; //;
     231##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H;
     232##| napply bind_OK; #u1 tyok;
     233    napply bind_OK; #s' es';
     234    ncut (type_pointable ty);
     235    ##[ ncases ty in tyok ⊢ %; //;
     236      ##[ #e; ##| ##3,6: #a e; ##| ##2,4,5: #a b e; ##] nwhd in e:(??%?); ndestruct;
     237    ##| ncut (type_space ty' s');
     238      ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     239          nwhd in e:(??%?); ndestruct; //;
     240      ##| #Hty' Hty;
     241          nwhd in match (is_class_compat ??) in ⊢ %;
     242          ncases (class_compat_dec (blockclass m c1) (ptr_spc_cls s')); #Hcompat;
     243          nwhd; /2/;
     244      ##]
     245    ##]
    331246##] nqed.
     247
     248ndefinition load_value_of_type' ≝
     249λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒
     250  load_value_of_type ty m pcl loc ofs ] ].
    332251
    333252(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    342261  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
    343262  | Evar _ ⇒ Some ? (
    344       〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    345       opt_to_res ? (load_value_of_type ty m loc ofs))
     263      l ← exec_lvalue' ge en m e' ty;:
     264      opt_to_res ? (load_value_of_type' ty m l))
    346265  | Ederef _ ⇒ Some ? (
    347       〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    348       opt_to_res ? (load_value_of_type ty m loc ofs))
     266      l ← exec_lvalue' ge en m e' ty;:
     267      opt_to_res ? (load_value_of_type' ty m l))
    349268  | Efield _ _ ⇒ Some ? (
    350       〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    351       opt_to_res ? (load_value_of_type ty m loc ofs))
     269      l ← exec_lvalue' ge en m e' ty;:
     270      opt_to_res ? (load_value_of_type' ty m l))
    352271  | Eaddrof a ⇒ Some ? (
    353       〈loc, ofs〉 ← exec_lvalue ge en m a;:
    354       OK ? (Vptr loc ofs))
     272      〈pl, ofs〉 ← exec_lvalue ge en m a;:
     273      OK ? (match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ]))
    355274  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
    356275  | Eunop op a ⇒ Some ? (
     
    383302  | Ecast ty' a ⇒ Some ? (
    384303      v ← exec_expr ge en m a;:
    385       exec_cast v (typeof a) ty')
     304      exec_cast m v (typeof a) ty')
    386305  ]
    387306]
    388 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝
     307and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:ptr_class × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
    389308  match e' with
    390309  [ Evar id ⇒
    391310      match (get … id en) with
    392       [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
    393       | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
     311      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈Universal (* XXX *),l〉,zero〉) (* global *)
     312      | Some bl ⇒ match bl with [ mk_pair bcl loc ⇒ Some ? (OK ? 〈〈blk_ptr_cls bcl,loc〉,zero〉) ] (* local *)
    394313      ]
    395314  | Ederef a ⇒ Some ? (
    396315      v ← exec_expr ge en m a;:
    397316      match v with
    398       [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
     317      [ Vptr pcl l ofs ⇒ OK ? 〈〈pcl,l〉,ofs〉
    399318      | _ ⇒ Error ?
    400319      ])
     
    402321      match (typeof a) with
    403322      [ Tstruct id fList ⇒ Some ? (
    404           〈l,ofs〉 ← exec_lvalue ge en m a;:
     323          〈pl,ofs〉 ← exec_lvalue ge en m a;:
    405324          delta ← field_offset i fList;:
    406           OK ? 〈l,add ofs (repr delta)〉)
     325          OK ? 〈pl,add ofs (repr delta)〉)
    407326      | Tunion id fList ⇒ Some ? (
    408           〈l,ofs〉 ← exec_lvalue ge en m a;:
    409           OK ? 〈l,ofs〉)
     327          〈pl,ofs〉 ← exec_lvalue ge en m a;:
     328          OK ? 〈pl,ofs〉)
    410329      | _ ⇒ Some ? (Error ?)
    411330      ]
    412331  | _ ⇒ Some ? (Error ?)
    413332  ]
    414 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:block × int. eval_lvalue ge en m e (\fst r) (\snd r)) ≝
     333and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:ptr_class × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
    415334match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    416 nwhd; //;
    417 ##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
    418     napply opt_OK;  #v ev; /2/;
    419 ##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
    420     napply opt_OK;  #v ev; /2/;
    421 ##| napply sig_bind2_OK; #loc ofs H;
     335nwhd;
     336##[ //
     337##| //
     338##| ##3,4:
     339    napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #pcl loc ofs H;
     340    napply opt_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
     341##| napply sig_bind2_OK; #x; ncases x; #pcl loc ofs H;
    422342    nwhd; napply eval_Eaddrof; //;
    423 ##| napply sig_bind_OK; #v1 ev1 Hv1;
     343##| napply sig_bind_OK; #v1 Hv1;
    424344    napply opt_OK; #v ev;
    425345    napply (eval_Eunop … Hv1 ev);
    426 ##| napply sig_bind_OK; #v1 ev1 Hv1;
    427     napply sig_bind_OK; #v2 ev2 Hv2;
     346##| napply sig_bind_OK; #v1 Hv1;
     347    napply sig_bind_OK; #v2 Hv2;
    428348    napply opt_OK; #v ev;
    429349    napply (eval_Ebinop … Hv1 Hv2 ev);
    430 ##| napply sig_bind_OK; #v ev Hv;
    431     napply sig_bind_OK; #v' ev' Hv';
     350##| napply sig_bind_OK; #v Hv;
     351    napply sig_bind_OK; #v' Hv';
    432352    napply (eval_Ecast … Hv Hv');
    433 ##| napply sig_bind_OK; #vb evb Hvb;
     353##| napply sig_bind_OK; #vb Hvb;
    434354    napply sig_bind_OK; #b;
    435     ncases b; #eb Hb; napply reinject; #v ev Hv;
     355    ncases b; #Hb; napply reinject; #v ev Hv;
    436356    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    437357    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    438358    ##]
    439 ##| napply sig_bind_OK; #v1 ev1 Hv1;
    440     napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
    441     ##[ napply sig_bind_OK; #v2 ev2 Hv2;
    442         napply sig_bind_OK; #b2 eb2 Hb2;
     359##| napply sig_bind_OK; #v1 Hv1;
     360    napply sig_bind_OK; #b1; ncases b1; #Hb1;
     361    ##[ napply sig_bind_OK; #v2 Hv2;
     362        napply sig_bind_OK; #b2 Hb2;
    443363        napply (eval_Eandbool_2 … Hv1 … Hv2);
    444364        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    445365    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    446366    ##]
    447 ##| napply sig_bind_OK; #v1 ev1 Hv1;
    448     napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
     367##| napply sig_bind_OK; #v1 Hv1;
     368    napply sig_bind_OK; #b1; ncases b1; #Hb1;
    449369    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    450     ##| napply sig_bind_OK; #v2 ev2 Hv2;
    451         napply sig_bind_OK; #b2 eb2 Hb2;
     370    ##| napply sig_bind_OK; #v2 Hv2;
     371        napply sig_bind_OK; #b2 Hb2;
    452372        napply (eval_Eorbool_2 … Hv1 … Hv2);
    453373        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    454374    ##]
    455 ##| napply sig_bind2_OK; nrewrite > c5; #l ofs H;
    456     napply opt_OK; #v ev; /2/;
     375##| //
     376##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #pcl l ofs H;
     377    napply opt_OK; #v ev; napply (eval_Elvalue … H ev);
     378##| //
     379##| //
    457380##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
    458 ##| napply eval_Evar_local; /2/
    459 ##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
     381##| napply eval_Evar_local; nrewrite < c6; /2/
     382##| napply sig_bind_OK; #v; ncases v; //; #pcl l ofs Hv; nwhd;
    460383    napply eval_Ederef; //
    461 ##| napply sig_bind2_OK; #l ofs H;
     384##| ##19,20,21,22,23,24,25,26,27,28,29,30,31,32: //
     385##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
    462386    napply bind_OK; #delta Hdelta;
    463387    napply (eval_Efield_struct … H c5 Hdelta);
    464 ##| napply sig_bind2_OK; #l ofs H;
     388##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
    465389    napply (eval_Efield_union … H c5);
     390##| //
    466391##] nqed.
    467392
     
    475400  OK ? (cons val v vs))
    476401]. nwhd; //;
    477 napply sig_bind_OK; #v ev Hv;
    478 napply sig_bind_OK; #vs evs Hvs;
     402napply sig_bind_OK; #v Hv;
     403napply sig_bind_OK; #vs Hvs;
    479404nnormalize; /2/;
    480405nqed.
     
    489414| cons h vars ⇒
    490415  match h with [ mk_pair id ty ⇒
    491     match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
    492       match exec_alloc_variables (set … id b1 en) m1 vars with
     416    match alloc m 0 (sizeof ty) UnspecifiedB with [ mk_pair m1 b1 ⇒
     417      match exec_alloc_variables (set … id 〈UnspecifiedB,b1〉 en) m1 vars with
    493418      [ sig_intro r p ⇒ r ]
    494419]]]. nwhd; //;
    495 nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1);
     420nelim (exec_alloc_variables (set ident ? ? c3 〈UnspecifiedB,c7〉 en) c6 c1);
    496421#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
    497422napply (alloc_variables_cons … IH); /2/;
     
    506431      [ nil ⇒ Some ? (Error ?)
    507432      | cons v1 vl ⇒ Some ? (
    508           b ← opt_to_res ? (get … id e);:
    509           m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
     433          〈bcl,b〉 ← opt_to_res ? (get … id e);:
     434          m1 ← opt_to_res ? (store_value_of_type ty m (blk_ptr_cls bcl) b zero v1);:
    510435          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
    511436      ]
    512437  ] ].
    513438nwhd; //;
    514 napply opt_bind_OK; #b eb;
     439napply opt_bind_OK; #x; ncases x; #bcl b eb;
    515440napply opt_bind_OK; #m1 em1;
    516441napply reinject; #m2 em2 Hm2;
     
    549474ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    550475#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     476ndefinition ms_eq_dec : ∀s1,s2:mem_space. (s1 = s2) + (s1 ≠ s2).
     477#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    551478
    552479nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
     
    555482| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    556483| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    557 | Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    558 | Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
    559     match assert_type_eq t t' with [ OK _ ⇒
    560       match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     484| Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒
     485    match ms_eq_dec s s' with [ inl _ ⇒
     486      match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     487| Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒
     488    match ms_eq_dec s s' with [ inl _ ⇒
     489      match assert_type_eq t t' with [ OK _ ⇒
     490        match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    561491| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
    562492    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     
    652582  ]
    653583]. nwhd; //;
    654 napply sig_bind_OK; #ev eev Hev;
    655 napply sig_bind_OK; #evt eevt Hevt;
     584napply sig_bind_OK; #ev Hev;
     585napply sig_bind_OK; #evt Hevt;
    656586nnormalize; /2/;
    657587nqed.
    658588
    659589(* execution *)
     590
     591ndefinition store_value_of_type' ≝
     592λty,m,l,v.
     593match l with [ mk_pair pl ofs ⇒
     594  match pl with [ mk_pair pcl loc ⇒
     595    store_value_of_type ty m pcl loc ofs v ] ].
    660596
    661597nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
     
    664600  match s with
    665601  [ Sassign a1 a2 ⇒ Some ? (
    666     ! 〈loc, ofs〉 ← exec_lvalue ge e m a1;:
     602    ! l ← exec_lvalue ge e m a1;:
    667603    ! v2 ← exec_expr ge e m a2;:
    668     ! m' ← store_value_of_type (typeof a1) m loc ofs v2;:
     604    ! m' ← store_value_of_type' (typeof a1) m l v2;:
    669605    ret ? 〈E0, State f Sskip k e m'〉)
    670606  | Scall lhs a al ⇒ Some ? (
     
    802738      ]
    803739    | Some r' ⇒
    804       match r' with [ mk_pair locofs ty ⇒
    805         match locofs with [ mk_pair loc ofs ⇒ Some ? (
    806           ! m' ← store_value_of_type ty m loc ofs res;:
     740      match r' with [ mk_pair l ty ⇒
     741        Some ? (
     742          ! m' ← store_value_of_type' ty m l res;:
    807743          ret ? 〈E0, (State f Sskip k' e m')〉)
    808         ]
    809744      ]
    810745    ]
     
    824759##| napply step_skip_break_switch; @; //;
    825760##| nrewrite > c11; napply step_skip_call; //; napply c12;
    826 ##| napply sig_bindIO2_OK; #loc ofs Hlval;
     761##| napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlval;
    827762    napply sig_bindIO_OK; #v2 Hv2;
    828763    napply opt_bindIO_OK; #m' em';
     
    835770    ##[ napply (step_call_none … Hvf Hvargs efd ety);
    836771    ##| #lhs';
    837         napply sig_bindIO_OK; #locofs; ncases locofs; #loc ofs Hlocofs;
     772        napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlocofs;
    838773        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    839774    ##]
     
    879814    napply sig_bindIO_OK; #res Hres;
    880815    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] 
    881 ##| napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; //;
     816##| ncases c11; #x; ncases x; #pcl b ofs;
     817    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
    882818##]
    883819nqed.
     
    905841    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    906842    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    907     ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     843    ##| #pcl b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    908844    ##]
    909845  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
Note: See TracChangeset for help on using the changeset viewer.