Changeset 175


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

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

Location:
C-semantics
Files:
4 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;
  • C-semantics/Csem.ma

    r155 r175  
    568568  [e] is the current environment and [m] is the current memory state. *)
    569569
    570 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → Prop ≝
     570ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
    571571  | eval_Econst_int:   ∀i,ty.
    572       eval_expr ge e m (Expr (Econst_int i) ty) (Vint i)
     572      eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0
    573573  | eval_Econst_float:   ∀f,ty.
    574       eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
    575   | eval_Elvalue: ∀a,ty,psp,loc,ofs,v.
    576       eval_lvalue ge e m (Expr a ty) psp loc ofs ->
    577       load_value_of_type ty m psp loc ofs = Some ? v ->
    578       eval_expr ge e m (Expr a ty) v
    579   | eval_Eaddrof: ∀a,ty,psp,loc,ofs.
    580       eval_lvalue ge e m a psp loc ofs ->
    581       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs)
     574      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
     575  | eval_Elvalue: ∀a,ty,psp,loc,ofs,v,tr.
     576      eval_lvalue ge e m (Expr a ty) psp loc ofs tr →
     577      load_value_of_type ty m psp loc ofs = Some ? v
     578      eval_expr ge e m (Expr a ty) v tr
     579  | eval_Eaddrof: ∀a,ty,psp,loc,ofs,tr.
     580      eval_lvalue ge e m a psp loc ofs tr →
     581      eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) tr
    582582  | eval_Esizeof: ∀ty',ty.
    583       eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
    584   | eval_Eunop:  ∀op,a,ty,v1,v.
    585       eval_expr ge e m a v1 ->
    586       sem_unary_operation op v1 (typeof a) = Some ? v ->
    587       eval_expr ge e m (Expr (Eunop op a) ty) v
    588   | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v.
    589       eval_expr ge e m a1 v1 ->
    590       eval_expr ge e m a2 v2 ->
    591       sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v ->
    592       eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v
    593   | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2.
    594       eval_expr ge e m a1 v1 ->
    595       is_true v1 (typeof a1) ->
    596       eval_expr ge e m a2 v2 ->
    597       eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2
    598   | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3.
    599       eval_expr ge e m a1 v1 ->
    600       is_false v1 (typeof a1) ->
    601       eval_expr ge e m a3 v3 ->
    602       eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3
    603   | eval_Eorbool_1: ∀a1,a2,ty,v1.
    604       eval_expr ge e m a1 v1 ->
    605       is_true v1 (typeof a1) ->
    606       eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue
    607   | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v.
    608       eval_expr ge e m a1 v1 ->
    609       is_false v1 (typeof a1) ->
    610       eval_expr ge e m a2 v2 ->
    611       bool_of_val v2 (typeof a2) v ->
    612       eval_expr ge e m (Expr (Eorbool a1 a2) ty) v
    613   | eval_Eandbool_1: ∀a1,a2,ty,v1.
    614       eval_expr ge e m a1 v1 ->
    615       is_false v1 (typeof a1) ->
    616       eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse
    617   | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v.
    618       eval_expr ge e m a1 v1 ->
    619       is_true v1 (typeof a1) ->
    620       eval_expr ge e m a2 v2 ->
    621       bool_of_val v2 (typeof a2) v ->
    622       eval_expr ge e m (Expr (Eandbool a1 a2) ty) v
    623   | eval_Ecast:   ∀a,ty,ty',v1,v.
    624       eval_expr ge e m a v1 ->
    625       cast m v1 (typeof a) ty v ->
    626       eval_expr ge e m (Expr (Ecast ty a) ty') v
     583      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     584  | eval_Eunop:  ∀op,a,ty,v1,v,tr.
     585      eval_expr ge e m a v1 tr →
     586      sem_unary_operation op v1 (typeof a) = Some ? v →
     587      eval_expr ge e m (Expr (Eunop op a) ty) v tr
     588  | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2.
     589      eval_expr ge e m a1 v1 tr1 →
     590      eval_expr ge e m a2 v2 tr2 →
     591      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v →
     592      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2)
     593  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2.
     594      eval_expr ge e m a1 v1 tr1 →
     595      is_true v1 (typeof a1) →
     596      eval_expr ge e m a2 v2 tr2 →
     597      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2)
     598  | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2.
     599      eval_expr ge e m a1 v1 tr1 →
     600      is_false v1 (typeof a1) →
     601      eval_expr ge e m a3 v3 tr2 →
     602      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2)
     603  | eval_Eorbool_1: ∀a1,a2,ty,v1,tr.
     604      eval_expr ge e m a1 v1 tr →
     605      is_true v1 (typeof a1) →
     606      eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr
     607  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     608      eval_expr ge e m a1 v1 tr1 →
     609      is_false v1 (typeof a1) →
     610      eval_expr ge e m a2 v2 tr2 →
     611      bool_of_val v2 (typeof a2) v →
     612      eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2)
     613  | eval_Eandbool_1: ∀a1,a2,ty,v1,tr.
     614      eval_expr ge e m a1 v1 tr →
     615      is_false v1 (typeof a1) →
     616      eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr
     617  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     618      eval_expr ge e m a1 v1 tr1 →
     619      is_true v1 (typeof a1) →
     620      eval_expr ge e m a2 v2 tr2 →
     621      bool_of_val v2 (typeof a2) v →
     622      eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2)
     623  | eval_Ecast:   ∀a,ty,ty',v1,v,tr.
     624      eval_expr ge e m a v1 tr →
     625      cast m v1 (typeof a) ty v →
     626      eval_expr ge e m (Expr (Ecast ty a) ty') v tr
     627  | eval_Ecost: ∀a,ty,v,l,tr.
     628      eval_expr ge e m a v tr →
     629      eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l)
    627630
    628631(* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
     
    630633  that contains the value of the expression [a]. *)
    631634
    632 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block -> int -> Prop ≝
     635with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝
    633636  | eval_Evar_local:   ∀id,l,ty.
    634637      (* XXX notation? e!id*) get ??? id e = Some ? l →
    635       eval_lvalue ge e m (Expr (Evar id) ty) Any l zero
     638      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    636639  | eval_Evar_global: ∀id,sp,l,ty.
    637       (* XXX e!id *) get ??? id e = None ? ->
    638       find_symbol ?? ge id = Some ? 〈sp,l〉 ->
    639       eval_lvalue ge e m (Expr (Evar id) ty) sp l zero
    640   | eval_Ederef: ∀a,ty,psp,l,ofs.
    641       eval_expr ge e m a (Vptr psp l ofs) ->
    642       eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs
    643  | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta.
    644       eval_lvalue ge e m a psp l ofs ->
    645       typeof a = Tstruct id fList ->
    646       field_offset i fList = OK ? delta ->
    647       eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta))
    648  | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList.
    649       eval_lvalue ge e m a psp l ofs ->
    650       typeof a = Tunion id fList ->
    651       eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs.
     640      (* XXX e!id *) get ??? id e = None ?
     641      find_symbol ?? ge id = Some ? 〈sp,l〉
     642      eval_lvalue ge e m (Expr (Evar id) ty) sp l zero E0
     643  | eval_Ederef: ∀a,ty,psp,l,ofs,tr.
     644      eval_expr ge e m a (Vptr psp l ofs) tr →
     645      eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs tr
     646 | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta,tr.
     647      eval_lvalue ge e m a psp l ofs tr →
     648      typeof a = Tstruct id fList
     649      field_offset i fList = OK ? delta
     650      eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) tr
     651 | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList,tr.
     652      eval_lvalue ge e m a psp l ofs tr →
     653      typeof a = Tunion id fList
     654      eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr.
    652655
    653656(*
     
    659662  expressions [al] to their values [vl]. *)
    660663
    661 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr -> list val -> Prop :=
     664ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝
    662665  | eval_Enil:
    663       eval_exprlist ge e m (nil ?) (nil ?)
    664   | eval_Econs:   ∀a,bl,v,vl.
    665       eval_expr ge e m a v ->
    666       eval_exprlist ge e m bl vl ->
    667       eval_exprlist ge e m (a :: bl) (v :: vl).
     666      eval_exprlist ge e m (nil ?) (nil ?) E0
     667  | eval_Econs:   ∀a,bl,v,vl,tr1,tr2.
     668      eval_expr ge e m a v tr1 →
     669      eval_exprlist ge e m bl vl tr2 →
     670      eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2).
    668671
    669672(*End EXPR.*)
     
    783786(* * Transition relation *)
    784787
    785 ninductive step (ge:genv) : state -> trace -> state -> Prop :=
    786 
    787   | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m'.
    788       eval_lvalue ge e m a1 psp loc ofs ->
    789       eval_expr ge e m a2 v2 ->
    790       store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' ->
     788(* XXX: note that cost labels in exprs expose a particular eval order. *)
     789
     790ninductive step (ge:genv) : state → trace → state → Prop ≝
     791
     792  | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
     793      eval_lvalue ge e m a1 psp loc ofs tr1 →
     794      eval_expr ge e m a2 v2 tr2 →
     795      store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' →
    791796      step ge (State f (Sassign a1 a2) k e m)
    792            E0 (State f Sskip k e m')
    793 
    794   | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd.
    795       eval_expr ge e m a vf ->
    796       eval_exprlist ge e m al vargs ->
    797       find_funct ?? ge vf = Some ? fd ->
    798       type_of_fundef fd = typeof a ->
     797           (tr1⧺tr2) (State f Sskip k e m')
     798
     799  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2.
     800      eval_expr ge e m a vf tr1 →
     801      eval_exprlist ge e m al vargs tr2 →
     802      find_funct ?? ge vf = Some ? fd
     803      type_of_fundef fd = typeof a
    799804      step ge (State f (Scall (None ?) a al) k e m)
    800            E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
    801 
    802   | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd.
    803       eval_lvalue ge e m lhs psp loc ofs ->
    804       eval_expr ge e m a vf ->
    805       eval_exprlist ge e m al vargs ->
    806       find_funct ?? ge vf = Some ? fd ->
    807       type_of_fundef fd = typeof a ->
     805           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
     806
     807  | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     808      eval_lvalue ge e m lhs psp loc ofs tr1 →
     809      eval_expr ge e m a vf tr2 →
     810      eval_exprlist ge e m al vargs tr3 →
     811      find_funct ?? ge vf = Some ? fd
     812      type_of_fundef fd = typeof a
    808813      step ge (State f (Scall (Some ? lhs) a al) k e m)
    809            E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
     814           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
    810815
    811816  | step_seq:  ∀f,s1,s2,k,e,m.
     
    822827           E0 (State f Sbreak k e m)
    823828
    824   | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1.
    825       eval_expr ge e m a v1 ->
    826       is_true v1 (typeof a) ->
     829  | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1,tr.
     830      eval_expr ge e m a v1 tr →
     831      is_true v1 (typeof a)
    827832      step ge (State f (Sifthenelse a s1 s2) k e m)
    828            E0 (State f s1 k e m)
    829   | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1.
    830       eval_expr ge e m a v1 ->
    831       is_false v1 (typeof a) ->
     833           tr (State f s1 k e m)
     834  | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr.
     835      eval_expr ge e m a v1 tr →
     836      is_false v1 (typeof a)
    832837      step ge (State f (Sifthenelse a s1 s2) k e m)
    833            E0 (State f s2 k e m)
    834 
    835   | step_while_false: ∀f,a,s,k,e,m,v.
    836       eval_expr ge e m a v ->
    837       is_false v (typeof a) ->
     838           tr (State f s2 k e m)
     839
     840  | step_while_false: ∀f,a,s,k,e,m,v,tr.
     841      eval_expr ge e m a v tr →
     842      is_false v (typeof a)
    838843      step ge (State f (Swhile a s) k e m)
    839            E0 (State f Sskip k e m)
    840   | step_while_true: ∀f,a,s,k,e,m,v.
    841       eval_expr ge e m a v ->
    842       is_true v (typeof a) ->
     844           tr (State f Sskip k e m)
     845  | step_while_true: ∀f,a,s,k,e,m,v,tr.
     846      eval_expr ge e m a v tr →
     847      is_true v (typeof a)
    843848      step ge (State f (Swhile a s) k e m)
    844            E0 (State f s (Kwhile a s k) e m)
     849           tr (State f s (Kwhile a s k) e m)
    845850  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
    846       x = Sskip ∨ x = Scontinue ->
     851      x = Sskip ∨ x = Scontinue
    847852      step ge (State f x (Kwhile a s k) e m)
    848853           E0 (State f (Swhile a s) k e m)
     
    854859      step ge (State f (Sdowhile a s) k e m)
    855860        E0 (State f s (Kdowhile a s k) e m)
    856   | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v.
    857       x = Sskip ∨ x = Scontinue ->
    858       eval_expr ge e m a v ->
    859       is_false v (typeof a) ->
     861  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
     862      x = Sskip ∨ x = Scontinue
     863      eval_expr ge e m a v tr →
     864      is_false v (typeof a)
    860865      step ge (State f x (Kdowhile a s k) e m)
    861            E0 (State f Sskip k e m)
    862   | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v.
    863       x = Sskip ∨ x = Scontinue ->
    864       eval_expr ge e m a v ->
    865       is_true v (typeof a) ->
     866           tr (State f Sskip k e m)
     867  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
     868      x = Sskip ∨ x = Scontinue
     869      eval_expr ge e m a v tr →
     870      is_true v (typeof a)
    866871      step ge (State f x (Kdowhile a s k) e m)
    867            E0 (State f (Sdowhile a s) k e m)
     872           tr (State f (Sdowhile a s) k e m)
    868873  | step_break_dowhile: ∀f,a,s,k,e,m.
    869874      step ge (State f Sbreak (Kdowhile a s k) e m)
     
    871876
    872877  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
    873       a1 ≠ Sskip ->
     878      a1 ≠ Sskip
    874879      step ge (State f (Sfor a1 a2 a3 s) k e m)
    875880           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
    876   | step_for_false: ∀f,a2,a3,s,k,e,m,v.
    877       eval_expr ge e m a2 v ->
    878       is_false v (typeof a2) ->
     881  | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
     882      eval_expr ge e m a2 v tr →
     883      is_false v (typeof a2)
    879884      step ge (State f (Sfor Sskip a2 a3 s) k e m)
    880            E0 (State f Sskip k e m)
    881   | step_for_true: ∀f,a2,a3,s,k,e,m,v.
    882       eval_expr ge e m a2 v ->
    883       is_true v (typeof a2) ->
     885           tr (State f Sskip k e m)
     886  | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
     887      eval_expr ge e m a2 v tr →
     888      is_true v (typeof a2)
    884889      step ge (State f (Sfor Sskip a2 a3 s) k e m)
    885            E0 (State f s (Kfor2 a2 a3 s k) e m)
     890           tr (State f s (Kfor2 a2 a3 s k) e m)
    886891  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
    887       x = Sskip ∨ x = Scontinue ->
     892      x = Sskip ∨ x = Scontinue
    888893      step ge (State f x (Kfor2 a2 a3 s k) e m)
    889894           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
     
    896901
    897902  | step_return_0: ∀f,k,e,m.
    898       fn_return f = Tvoid ->
     903      fn_return f = Tvoid
    899904      step ge (State f (Sreturn (None ?)) k e m)
    900905           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
    901   | step_return_1: ∀f,a,k,e,m,v.
    902       fn_return f ≠ Tvoid ->
    903       eval_expr ge e m a v ->
     906  | step_return_1: ∀f,a,k,e,m,v,tr.
     907      fn_return f ≠ Tvoid
     908      eval_expr ge e m a v tr →
    904909      step ge (State f (Sreturn (Some ? a)) k e m)
    905            E0 (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
     910           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
    906911  | step_skip_call: ∀f,k,e,m.
    907       is_call_cont k ->
    908       fn_return f = Tvoid ->
     912      is_call_cont k
     913      fn_return f = Tvoid
    909914      step ge (State f Sskip k e m)
    910915           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    911916
    912   | step_switch: ∀f,a,sl,k,e,m,n.
    913       eval_expr ge e m a (Vint n) ->
     917  | step_switch: ∀f,a,sl,k,e,m,n,tr.
     918      eval_expr ge e m a (Vint n) tr →
    914919      step ge (State f (Sswitch a sl) k e m)
    915            E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
     920           tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
    916921  | step_skip_break_switch: ∀f,x,k,e,m.
    917       x = Sskip ∨ x = Sbreak ->
     922      x = Sskip ∨ x = Sbreak
    918923      step ge (State f x (Kswitch k) e m)
    919924           E0 (State f Sskip k e m)
     
    927932
    928933  | step_goto: ∀f,lbl,k,e,m,s',k'.
    929       find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 ->
     934      find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉
    930935      step ge (State f (Sgoto lbl) k e m)
    931936           E0 (State f s' k' e m)
    932937
    933938  | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
    934       alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 ->
    935       bind_parameters e m1 (fn_params f) vargs m2 ->
     939      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1
     940      bind_parameters e m1 (fn_params f) vargs m2
    936941      step ge (Callstate (Internal f) vargs k m)
    937942           E0 (State f (fn_body f) k e m2)
    938943
    939944  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
    940       event_match (external_function id targs tres) vargs t vres ->
     945      event_match (external_function id targs tres) vargs t vres
    941946      step ge (Callstate (External id targs tres) vargs k m)
    942947            t (Returnstate vres k m)
     
    947952
    948953  | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
    949       store_value_of_type ty m psp loc ofs v = Some ? m' ->
     954      store_value_of_type ty m psp loc ofs v = Some ? m'
    950955      step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
    951            E0 (State f Sskip k e m').
     956           E0 (State f Sskip k e m')
     957           
     958  | step_cost: ∀f,lbl,s,k,e,m.
     959      step ge (State f (Scost lbl s) k e m)
     960           (Echarge lbl) (State f s k e m).
    952961(*
    953962(** * Alternate big-step semantics *)
  • C-semantics/Csyntax.ma

    r156 r175  
    2020include "Coqlib.ma".
    2121include "Errors.ma".
     22include "CostLabel.ma".
    2223
    2324(* * * Abstract syntax *)
     
    189190  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
    190191  | Esizeof: type → expr_descr         (**r size of a type *)
    191   | Efield: expr → ident → expr_descr. (**r access to a member of a struct or union *)
     192  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
     193  | Ecost: costlabel → expr → expr_descr.
    192194
    193195(* * Extract the type part of a type-annotated Clight expression. *)
     
    220222  | Slabel : label → statement → statement
    221223  | Sgoto : label → statement
     224  | Scost : costlabel → statement → statement
    222225
    223226with labeled_statements : Type ≝            (**r cases of a [switch] *)
     
    241244  (Sla:∀l,s. P s → P (Slabel l s))
    242245  (Sgo:∀l. P (Sgoto l))
     246  (Scs:∀l,s. P s → P (Scost l s))
    243247  (LSd:∀s. P s → Q (LSdefault s))
    244248  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     
    249253| Scall eo e args ⇒ Sca eo e args
    250254| Ssequence s1 s2 ⇒ Ssq s1 s2
    251     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
    252     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     255    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     256    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    253257| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    254     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
    255     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     258    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     259    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    256260| Swhile e s ⇒ Swh e s
    257     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    258262| Sdowhile e s ⇒ Sdo e s
    259     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     263    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    260264| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
    261     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
    262     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
    263     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s3)
     265    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     266    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     267    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
    264268| Sbreak ⇒ Sbr
    265269| Scontinue ⇒ Sco
    266270| Sreturn eo ⇒ Sre eo
    267271| Sswitch e ls ⇒ Ssw e ls
    268     (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc ls)
     272    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
    269273| Slabel l s ⇒ Sla l s
    270     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     274    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    271275| Sgoto l ⇒ Sgo l
     276| Scost l s ⇒ Scs l s
     277    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    272278]
    273279and labeled_statements_ind2
     
    287293  (Sla:∀l,s. P s → P (Slabel l s))
    288294  (Sgo:∀l. P (Sgoto l))
     295  (Scs:∀l,s. P s → P (Scost l s))
    289296  (LSd:∀s. P s → Q (LSdefault s))
    290297  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     
    292299match ls with
    293300[ LSdefault s ⇒ LSd s
    294     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     301    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    295302| LScase i s t ⇒ LSc i s t
    296     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
    297     (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc t)
     303    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     304    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
    298305].
    299306
    300 ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo.
    301   statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo
     307ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
     308  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
    302309  (λ_,_. I) (λ_,_,_,_,_.I).
    303310
  • C-semantics/Events.ma

    r3 r175  
    2424include "datatypes/list.ma".
    2525include "extralib.ma".
     26include "CostLabel.ma".
    2627
    2728(* * The observable behaviour of programs is stated in terms of
     
    4041  | EVfloat: float -> eventval.
    4142
    42 nrecord event : Type := {
    43   ev_name: ident;
    44   ev_args: list eventval;
    45   ev_res: eventval
    46 }.
     43ninductive event : Type ≝
     44  | EVcost: costlabel → event
     45  | EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event.
    4746
    4847(* * The dynamic semantics for programs collect traces of events.
     
    5352ndefinition E0 : trace := nil ?.
    5453
     54ndefinition Echarge : costlabel → trace ≝
     55λlabel. EVcost label :: (nil ?).
     56
    5557ndefinition Eextcall : ident → list eventval → eventval → trace ≝
    5658             λname: ident. λargs: list eventval. λres: eventval.
    57   mk_event name args res :: (nil ?).
     59  EVextcall name args res :: (nil ?).
    5860
    5961ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
Note: See TracChangeset for help on using the changeset viewer.