Changeset 175 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Oct 13, 2010, 12:19:22 PM (10 years ago)
Author:
campbell
Message:

Add cost labels, with the semantics that the label is added to the
event trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r174 r175  
    263263   and use exec_lvalue'. *)
    264264
    265 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝
     265nlet 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)) ≝
    266266match e with
    267267[ Expr e' ty ⇒
    268268  match e' with
    269   [ Econst_int i ⇒ Some ? (OK ? (Vint i))
    270   | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
     269  [ Econst_int i ⇒ Some ? (OK ? 〈Vint i, E0〉)
     270  | Econst_float f ⇒ Some ? (OK ? 〈Vfloat f, E0〉)
    271271  | Evar _ ⇒ Some ? (
    272       l ← exec_lvalue' ge en m e' ty;:
    273       opt_to_res ? (load_value_of_type' ty m l))
     272      〈l,tr〉 ← exec_lvalue' ge en m e' ty;:
     273      v ← opt_to_res ? (load_value_of_type' ty m l);:
     274      OK ? 〈v,tr〉)
    274275  | Ederef _ ⇒ Some ? (
    275       l ← exec_lvalue' ge en m e' ty;:
    276       opt_to_res ? (load_value_of_type' ty m l))
     276      〈l,tr〉 ← exec_lvalue' ge en m e' ty;:
     277      v ← opt_to_res ? (load_value_of_type' ty m l);:
     278      OK ? 〈v,tr〉)
    277279  | Efield _ _ ⇒ Some ? (
    278       l ← exec_lvalue' ge en m e' ty;:
    279       opt_to_res ? (load_value_of_type' ty m l))
     280      〈l,tr〉 ← exec_lvalue' ge en m e' ty;:
     281      v ← opt_to_res ? (load_value_of_type' ty m l);:
     282      OK ? 〈v,tr〉)
    280283  | Eaddrof a ⇒ Some ? (
    281       〈pl, ofs〉 ← exec_lvalue ge en m a;:
    282       OK ? (match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ]))
    283   | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
     284      〈plo,tr〉 ← exec_lvalue ge en m a;:
     285      OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉)
     286  | Esizeof ty' ⇒ Some ? (OK ? 〈Vint (repr (sizeof ty')), E0〉)
    284287  | Eunop op a ⇒ Some ? (
    285       v1 ← exec_expr ge en m a;:
    286       opt_to_res ? (sem_unary_operation op v1 (typeof a)))
     288      〈v1,tr〉 ← exec_expr ge en m a;:
     289      v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));:
     290      OK ? 〈v,tr〉)
    287291  | Ebinop op a1 a2 ⇒ Some ? (
    288       v1 ← exec_expr ge en m a1;:
    289       v2 ← exec_expr ge en m a2;:
    290       opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
     292      〈v1,tr1〉 ← exec_expr ge en m a1;:
     293      〈v2,tr2〉 ← exec_expr ge en m a2;:
     294      v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);:
     295      OK ? 〈v,tr1⧺tr2〉)
    291296  | Econdition a1 a2 a3 ⇒ Some ? (
    292       v ← exec_expr ge en m a1;:
     297      〈v,tr1〉 ← exec_expr ge en m a1;:
    293298      b ← bool_of_val_3 v (typeof a1);:
    294       match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
     299      〈v',tr2〉 ← match b return λ_.res (val×trace) with
     300                 [ true ⇒ (exec_expr ge en m a2)
     301                 | false ⇒ (exec_expr ge en m a3) ];:
     302      OK ? 〈v',tr1⧺tr2〉)
    295303(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
    296304  | Eorbool a1 a2 ⇒ Some ? (
    297       v1 ← exec_expr ge en m a1;:
     305      〈v1,tr1〉 ← exec_expr ge en m a1;:
    298306      b1 ← bool_of_val_3 v1 (typeof a1);:
    299       match b1 return λ_.res val with [ true ⇒ OK ? Vtrue | false ⇒
    300         v2 ← exec_expr ge en m a2;:
     307      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
     308        〈v2,tr2〉 ← exec_expr ge en m a2;:
    301309        b2 ← bool_of_val_3 v2 (typeof a2);:
    302         OK ? (of_bool b2) ])
     310        OK ? 〈of_bool b2, tr1⧺tr2〉 ])
    303311  | Eandbool a1 a2 ⇒ Some ? (
    304       v1 ← exec_expr ge en m a1;:
     312      〈v1,tr1〉 ← exec_expr ge en m a1;:
    305313      b1 ← bool_of_val_3 v1 (typeof a1);:
    306       match b1 return λ_.res val with [ true ⇒
    307         v2 ← exec_expr ge en m a2;:
     314      match b1 return λ_.res (val×trace) with [ true ⇒
     315        〈v2,tr2〉 ← exec_expr ge en m a2;:
    308316        b2 ← bool_of_val_3 v2 (typeof a2);:
    309         OK ? (of_bool b2)
    310       | false ⇒ OK ? Vfalse ])
     317        OK ? 〈of_bool b2, tr1⧺tr2〉
     318      | false ⇒ OK ? 〈Vfalse,tr1〉 ])
    311319  | Ecast ty' a ⇒ Some ? (
    312       v ← exec_expr ge en m a;:
    313       exec_cast m v (typeof a) ty')
     320      〈v,tr〉 ← exec_expr ge en m a;:
     321      v' ← exec_cast m v (typeof a) ty';:
     322      OK ? 〈(* XXX *)sig_eject ?? v',tr〉)
     323  | Ecost l a ⇒ Some ? (
     324      〈v,tr〉 ← exec_expr ge en m a;:
     325      OK ? 〈v,tr⧺(Echarge l)〉)
    314326  ]
    315327]
    316 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
     328and 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)) ≝
    317329  match e' with
    318330  [ Evar id ⇒
    319331      match (get … id en) with
    320       [ None ⇒ Some ? (〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈sp,l〉,zero〉) (* global *)
    321       | Some loc ⇒ Some ? (OK ? 〈〈Any,loc〉,zero〉) (* local *)
     332      [ None ⇒ Some ? (〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
     333      | Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)
    322334      ]
    323335  | Ederef a ⇒ Some ? (
    324       v ← exec_expr ge en m a;:
     336      〈v,tr〉 ← exec_expr ge en m a;:
    325337      match v with
    326       [ Vptr sp l ofs ⇒ OK ? 〈〈sp,l〉,ofs
     338      [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr
    327339      | _ ⇒ Error ?
    328340      ])
     
    330342      match (typeof a) with
    331343      [ Tstruct id fList ⇒ Some ? (
    332           〈pl,ofs〉 ← exec_lvalue ge en m a;:
     344          〈plofs,tr〉 ← exec_lvalue ge en m a;:
    333345          delta ← field_offset i fList;:
    334           OK ? 〈pl,add ofs (repr delta)〉)
     346          OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉)
    335347      | Tunion id fList ⇒ Some ? (
    336           〈pl,ofs〉 ← exec_lvalue ge en m a;:
    337           OK ? 〈pl,ofs〉)
     348          〈plofs,tr〉 ← exec_lvalue ge en m a;:
     349          OK ? 〈plofs,tr〉)
    338350      | _ ⇒ Some ? (Error ?)
    339351      ]
    340352  | _ ⇒ Some ? (Error ?)
    341353  ]
    342 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
     354and 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)) ≝
    343355match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    344356nwhd;
    345357##[ ##1,2: //
    346358##| ##3,4:
    347     napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs H;
    348     napply opt_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
    349 ##| napply sig_bind2_OK; #x; ncases x; #sp loc ofs H;
     359    napply sig_bind2_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
     360    napply opt_bind_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
     361##| napply sig_bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    350362    nwhd; napply eval_Eaddrof; //;
    351 ##| napply sig_bind_OK; #v1 Hv1;
    352     napply opt_OK; #v ev;
     363##| napply sig_bind2_OK; #v1 tr Hv1;
     364    napply opt_bind_OK; #v ev;
    353365    napply (eval_Eunop … Hv1 ev);
    354 ##| napply sig_bind_OK; #v1 Hv1;
    355     napply sig_bind_OK; #v2 Hv2;
    356     napply opt_OK; #v ev;
     366##| napply sig_bind2_OK; #v1 tr1 Hv1;
     367    napply sig_bind2_OK; #v2 tr2 Hv2;
     368    napply opt_bind_OK; #v ev;
    357369    napply (eval_Ebinop … Hv1 Hv2 ev);
    358 ##| napply sig_bind_OK; #v Hv;
     370##| napply sig_bind2_OK; #v tr Hv;
    359371    napply sig_bind_OK; #v' Hv';
    360372    napply (eval_Ecast … Hv Hv');
    361 ##| napply sig_bind_OK; #vb Hvb;
     373##| napply sig_bind2_OK; #vb tr1 Hvb;
    362374    napply sig_bind_OK; #b;
    363     ncases b; #Hb; napply reinject; #v ev Hv;
     375    ncases b; #Hb; napply sig_bind2_OK; #v tr Hv;
    364376    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    365377    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    366378    ##]
    367 ##| napply sig_bind_OK; #v1 Hv1;
     379##| napply sig_bind2_OK; #v1 tr1 Hv1;
    368380    napply sig_bind_OK; #b1; ncases b1; #Hb1;
    369     ##[ napply sig_bind_OK; #v2 Hv2;
     381    ##[ napply sig_bind2_OK; #v2 tr2 Hv2;
    370382        napply sig_bind_OK; #b2 Hb2;
    371383        napply (eval_Eandbool_2 … Hv1 … Hv2);
     
    373385    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    374386    ##]
    375 ##| napply sig_bind_OK; #v1 Hv1;
     387##| napply sig_bind2_OK; #v1 tr1 Hv1;
    376388    napply sig_bind_OK; #b1; ncases b1; #Hb1;
    377389    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    378     ##| napply sig_bind_OK; #v2 Hv2;
     390    ##| napply sig_bind2_OK; #v2 tr2 Hv2;
    379391        napply sig_bind_OK; #b2 Hb2;
    380392        napply (eval_Eorbool_2 … Hv1 … Hv2);
     
    382394    ##]
    383395##| //
    384 ##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs H;
    385     napply opt_OK; #v ev; napply (eval_Elvalue … H ev);
     396##| napply sig_bind2_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs tr H;
     397    napply opt_bind_OK; #v ev; napply (eval_Elvalue … H ev);
     398##| napply sig_bind2_OK; #v tr1 H; napply (eval_Ecost … H);
    386399##| //
    387400##| //
    388401##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
    389402##| napply (eval_Evar_local … c3);
    390 ##| napply sig_bind_OK; #v; ncases v; //; #sp l ofs Hv; nwhd;
     403##| napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
    391404    napply eval_Ederef; //
    392 ##| ##19,20,21,22,23,24,25,26,27,28,29,30,31,32: //
     405##| ##20,21,22,23,24,25,26,27,28,29,30,31,32,33: //
    393406##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    394407    napply bind_OK; #delta Hdelta;
     
    397410    napply (eval_Efield_union … H c5);
    398411##| //
     412##| //
    399413##] nqed.
    400414
    401415(* TODO: Can we do this sensibly with a map combinator? *)
    402 nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvl:list val. eval_exprlist ge e m l vl) ≝
     416nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) ≝
    403417match l with
    404 [ nil ⇒ Some ? (OK ? (nil val))
     418[ nil ⇒ Some ? (OK ? 〈nil val, E0〉)
    405419| cons e1 es ⇒ Some ? (
    406   v ← exec_expr ge e m e1;:
    407   vs ← exec_exprlist ge e m es;:
    408   OK ? (cons val v vs))
     420  〈v,tr1〉 ← exec_expr ge e m e1;:
     421  〈vs,tr2〉 ← exec_exprlist ge e m es;:
     422  OK ? 〈cons val v vs, tr1⧺tr2〉)
    409423]. nwhd; //;
    410 napply sig_bind_OK; #v Hv;
    411 napply sig_bind_OK; #vs Hvs;
    412 nnormalize; /2/;
     424napply sig_bind2_OK; #v tr1 Hv;
     425napply sig_bind2_OK; #vs tr2 Hvs;
     426nwhd; napply eval_Econs; //;
    413427nqed.
    414428
     
    607621  match s with
    608622  [ Sassign a1 a2 ⇒ Some ? (
    609     ! l ← exec_lvalue ge e m a1;:
    610     ! v2 ← exec_expr ge e m a2;:
     623    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;:
     624    ! 〈v2,tr2〉 ← exec_expr ge e m a2;:
    611625    ! m' ← store_value_of_type' (typeof a1) m l v2;:
    612     ret ? 〈E0, State f Sskip k e m'〉)
     626    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
    613627  | Scall lhs a al ⇒ Some ? (
    614     ! vf ← exec_expr ge e m a;:
    615     ! vargs ← exec_exprlist ge e m al;:
     628    ! 〈vf,tr2〉 ← exec_expr ge e m a;:
     629    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;:
    616630    ! fd ← find_funct ? ? ge vf;:
    617631    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));:
     
    626640*)
    627641    match lhs with
    628          [ None ⇒ ret ? 〈E0, Callstate fd vargs (Kcall (None ?) f e k) m〉
     642         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
    629643         | Some lhs' ⇒
    630            ! locofs ← exec_lvalue ge e m lhs';:
    631            ret ? 〈E0, Callstate fd vargs (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) m〉
     644           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';:
     645           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    632646         ])
    633647  | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
     
    647661      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
    648662      | Kdowhile a s' k' ⇒ Some ? (
    649           ! v ← exec_expr ge e m a;:
     663          ! 〈v,tr〉 ← exec_expr ge e m a;:
    650664          ! b ← bool_of_val_3 v (typeof a);:
    651665          match b with
    652           [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
    653           | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
     666          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
     667          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
    654668          ])
    655669      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
     
    663677      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
    664678      | Kdowhile a s' k' ⇒ Some ? (
    665           ! v ← exec_expr ge e m a;:
     679          ! 〈v,tr〉 ← exec_expr ge e m a;:
    666680          ! b ← bool_of_val_3 v (typeof a);:
    667681          match b with
    668           [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
    669           | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
     682          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
     683          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
    670684          ])
    671685      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
     
    683697      ]
    684698  | Sifthenelse a s1 s2 ⇒ Some ? (
    685       ! v ← exec_expr ge e m a;:
     699      ! 〈v,tr〉 ← exec_expr ge e m a;:
    686700      ! b ← bool_of_val_3 v (typeof a);:
    687       ret ? 〈E0, State f (if b then s1 else s2) k e m〉)
     701      ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
    688702  | Swhile a s' ⇒ Some ? (
    689       ! v ← exec_expr ge e m a;:
     703      ! 〈v,tr〉 ← exec_expr ge e m a;:
    690704      ! b ← bool_of_val_3 v (typeof a);:
    691       ret ? 〈E0, if b then State f s' (Kwhile a s' k) e m
    692                      else State f Sskip k e m〉)
     705      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
     706                      else State f Sskip k e m〉)
    693707  | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
    694708  | Sfor a1 a2 a3 s' ⇒
    695709      match is_Sskip a1 with
    696710      [ inl _ ⇒ Some ? (
    697           ! v ← exec_expr ge e m a2;:
     711          ! 〈v,tr〉 ← exec_expr ge e m a2;:
    698712          ! b ← bool_of_val_3 v (typeof a2);:
    699           ret ? 〈E0, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
     713          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
    700714      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
    701715      ]
     
    708722    | Some a ⇒ Some ? (
    709723        ! u ← is_not_void (fn_return f);:
    710         ! v ← exec_expr ge e m a;:
    711         ret ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
     724        ! 〈v,tr〉 ← exec_expr ge e m a;:
     725        ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
    712726    ]
    713727  | Sswitch a sl ⇒ Some ? (
    714       ! v ← exec_expr ge e m a;:
    715       match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
     728      ! 〈v,tr〉 ← exec_expr ge e m a;:
     729      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
    716730                   | _ ⇒ Wrong ??? ])
    717731  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
     
    721735      | None ⇒ Some ? (Wrong ???)
    722736      ]
     737  | Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉)
    723738  ]
    724739| Callstate f0 vargs k m ⇒
     
    756771##[ nrewrite > c7; napply step_skip_call; //; napply c8;
    757772##| napply step_skip_or_continue_while; @; //;
    758 ##| napply sig_bindIO_OK; #v Hv;
     773##| napply sig_bindIO2_OK; #v tr Hv;
    759774    napply sig_bindIO_OK; #b; ncases b; #Hb;
    760775    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     
    766781##| napply step_skip_break_switch; @; //;
    767782##| nrewrite > c11; napply step_skip_call; //; napply c12;
    768 ##| napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlval;
    769     napply sig_bindIO_OK; #v2 Hv2;
     783##| napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
     784    napply sig_bindIO2_OK; #v2 tr2 Hv2;
    770785    napply opt_bindIO_OK; #m' em';
    771786    nwhd; napply (step_assign … Hlval Hv2 em');
    772 ##| napply sig_bindIO_OK; #vf Hvf;
    773     napply sig_bindIO_OK; #vargs Hvargs;
     787##| napply sig_bindIO2_OK; #vf tr1 Hvf;
     788    napply sig_bindIO2_OK; #vargs tr2 Hvargs;
    774789    napply opt_bindIO_OK; #fd efd;
    775790    napply bindIO_OK; #ety;
     
    777792    ##[ napply (step_call_none … Hvf Hvargs efd ety);
    778793    ##| #lhs';
    779         napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlocofs;
     794        napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
    780795        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    781796    ##]
    782 ##| napply sig_bindIO_OK; #v Hv;
     797##| napply sig_bindIO2_OK; #v tr Hv;
    783798    napply sig_bindIO_OK; #b; ncases b; #Hb;
    784799    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
    785800    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
    786801    ##]
    787 ##| napply sig_bindIO_OK; #v Hv;
     802##| napply sig_bindIO2_OK; #v tr Hv;
    788803    napply sig_bindIO_OK; #b; ncases b; #Hb;
    789804    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
     
    791806    ##]
    792807##| nrewrite > c11;
    793     napply sig_bindIO_OK; #v Hv;
     808    napply sig_bindIO2_OK; #v tr Hv;
    794809    napply sig_bindIO_OK; #b; ncases b; #Hb;
    795810    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
     
    799814##| napply step_skip_break_switch; @2; //;
    800815##| napply step_skip_or_continue_while; @2; //;
    801 ##| napply sig_bindIO_OK; #v Hv;
     816##| napply sig_bindIO2_OK; #v tr Hv;
    802817    napply sig_bindIO_OK; #b; ncases b; #Hb;
    803818    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     
    809824##| napply step_return_0; napply c9;
    810825##| napply sig_bindIO_OK; #u Hnotvoid;
    811     napply sig_bindIO_OK; #v Hv;
     826    napply sig_bindIO2_OK; #v tr Hv;
    812827    nwhd; napply (step_return_1 … Hnotvoid Hv);
    813 ##| napply sig_bindIO_OK; #v; ncases v; //; #n Hv;
     828##| napply sig_bindIO2_OK; #v; ncases v; //; #n tr Hv;
    814829    napply step_switch; //;
    815830##| napply step_goto; nrewrite < c12; napply c9;
Note: See TracChangeset for help on using the changeset viewer.