Changeset 175
 Timestamp:
 Oct 13, 2010, 12:19:22 PM (11 years ago)
 Location:
 Csemantics
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIO.ma
r174 r175 263 263 and use exec_lvalue'. *) 264 264 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) ≝265 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val×trace. eval_expr ge en m e (\fst r) (\snd r)) ≝ 266 266 match e with 267 267 [ Expr e' ty ⇒ 268 268 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〉) 271 271  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〉) 274 275  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〉) 277 279  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〉) 280 283  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〉) 284 287  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〉) 287 291  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〉) 291 296  Econdition a1 a2 a3 ⇒ Some ? ( 292 v← exec_expr ge en m a1;:297 〈v,tr1〉 ← exec_expr ge en m a1;: 293 298 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〉) 295 303 (* if b then exec_expr ge en m a2 else exec_expr ge en m a3)*) 296 304  Eorbool a1 a2 ⇒ Some ? ( 297 v1← exec_expr ge en m a1;:305 〈v1,tr1〉 ← exec_expr ge en m a1;: 298 306 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;: 301 309 b2 ← bool_of_val_3 v2 (typeof a2);: 302 OK ? (of_bool b2)])310 OK ? 〈of_bool b2, tr1⧺tr2〉 ]) 303 311  Eandbool a1 a2 ⇒ Some ? ( 304 v1← exec_expr ge en m a1;:312 〈v1,tr1〉 ← exec_expr ge en m a1;: 305 313 b1 ← bool_of_val_3 v1 (typeof a1);: 306 match b1 return λ_.res valwith [ 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;: 308 316 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〉 ]) 311 319  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)〉) 314 326 ] 315 327 ] 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)) ≝328 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝ 317 329 match e' with 318 330 [ Evar id ⇒ 319 331 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 *) 322 334 ] 323 335  Ederef a ⇒ Some ? ( 324 v← exec_expr ge en m a;:336 〈v,tr〉 ← exec_expr ge en m a;: 325 337 match v with 326 [ Vptr sp l ofs ⇒ OK ? 〈〈 sp,l〉,ofs〉338 [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉 327 339  _ ⇒ Error ? 328 340 ]) … … 330 342 match (typeof a) with 331 343 [ Tstruct id fList ⇒ Some ? ( 332 〈pl ,ofs〉 ← exec_lvalue ge en m a;:344 〈plofs,tr〉 ← exec_lvalue ge en m a;: 333 345 delta ← field_offset i fList;: 334 OK ? 〈 pl,add ofs (repr delta)〉)346 OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉) 335 347  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〉) 338 350  _ ⇒ Some ? (Error ?) 339 351 ] 340 352  _ ⇒ Some ? (Error ?) 341 353 ] 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)) ≝354 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝ 343 355 match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. 344 356 nwhd; 345 357 ##[ ##1,2: // 346 358 ## ##3,4: 347 napply sig_bind _OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofsH;348 napply opt_ OK; #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);349 ## napply sig_bind2_OK; #x; ncases x; # sp loc ofsH;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; 350 362 nwhd; napply eval_Eaddrof; //; 351 ## napply sig_bind _OK; #v1Hv1;352 napply opt_ OK; #v ev;363 ## napply sig_bind2_OK; #v1 tr Hv1; 364 napply opt_bind_OK; #v ev; 353 365 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; 357 369 napply (eval_Ebinop … Hv1 Hv2 ev); 358 ## napply sig_bind _OK; #vHv;370 ## napply sig_bind2_OK; #v tr Hv; 359 371 napply sig_bind_OK; #v' Hv'; 360 372 napply (eval_Ecast … Hv Hv'); 361 ## napply sig_bind _OK; #vbHvb;373 ## napply sig_bind2_OK; #vb tr1 Hvb; 362 374 napply sig_bind_OK; #b; 363 ncases b; #Hb; napply reinject; #v evHv;375 ncases b; #Hb; napply sig_bind2_OK; #v tr Hv; 364 376 ##[ napply (eval_Econdition_true … Hvb ? Hv); napply (bool_of ??? Hb); 365 377 ## napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb); 366 378 ##] 367 ## napply sig_bind _OK; #v1 Hv1;379 ## napply sig_bind2_OK; #v1 tr1 Hv1; 368 380 napply sig_bind_OK; #b1; ncases b1; #Hb1; 369 ##[ napply sig_bind _OK; #v2 Hv2;381 ##[ napply sig_bind2_OK; #v2 tr2 Hv2; 370 382 napply sig_bind_OK; #b2 Hb2; 371 383 napply (eval_Eandbool_2 … Hv1 … Hv2); … … 373 385 ## napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1); 374 386 ##] 375 ## napply sig_bind _OK; #v1 Hv1;387 ## napply sig_bind2_OK; #v1 tr1 Hv1; 376 388 napply sig_bind_OK; #b1; ncases b1; #Hb1; 377 389 ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1); 378 ## napply sig_bind _OK; #v2 Hv2;390 ## napply sig_bind2_OK; #v2 tr2 Hv2; 379 391 napply sig_bind_OK; #b2 Hb2; 380 392 napply (eval_Eorbool_2 … Hv1 … Hv2); … … 382 394 ##] 383 395 ## // 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); 386 399 ## // 387 400 ## // 388 401 ## napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/; 389 402 ## napply (eval_Evar_local … c3); 390 ## napply sig_bind _OK; #v; ncases v; //; #sp l ofsHv; nwhd;403 ## napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd; 391 404 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: // 393 406 ## napply sig_bind2_OK; #x; ncases x; #sp l ofs H; 394 407 napply bind_OK; #delta Hdelta; … … 397 410 napply (eval_Efield_union … H c5); 398 411 ## // 412 ## // 399 413 ##] nqed. 400 414 401 415 (* 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) ≝416 nlet 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)) ≝ 403 417 match l with 404 [ nil ⇒ Some ? (OK ? (nil val))418 [ nil ⇒ Some ? (OK ? 〈nil val, E0〉) 405 419  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〉) 409 423 ]. nwhd; //; 410 napply sig_bind _OK; #vHv;411 napply sig_bind _OK; #vsHvs;412 n normalize; /2/;424 napply sig_bind2_OK; #v tr1 Hv; 425 napply sig_bind2_OK; #vs tr2 Hvs; 426 nwhd; napply eval_Econs; //; 413 427 nqed. 414 428 … … 607 621 match s with 608 622 [ 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;: 611 625 ! 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'〉) 613 627  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;: 616 630 ! fd ← find_funct ? ? ge vf;: 617 631 ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));: … … 626 640 *) 627 641 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〉 629 643  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〉 632 646 ]) 633 647  Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉) … … 647 661  Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) 648 662  Kdowhile a s' k' ⇒ Some ? ( 649 ! v← exec_expr ge e m a;:663 ! 〈v,tr〉 ← exec_expr ge e m a;: 650 664 ! b ← bool_of_val_3 v (typeof a);: 651 665 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〉 654 668 ]) 655 669  Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉) … … 663 677  Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉) 664 678  Kdowhile a s' k' ⇒ Some ? ( 665 ! v← exec_expr ge e m a;:679 ! 〈v,tr〉 ← exec_expr ge e m a;: 666 680 ! b ← bool_of_val_3 v (typeof a);: 667 681 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〉 670 684 ]) 671 685  Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉) … … 683 697 ] 684 698  Sifthenelse a s1 s2 ⇒ Some ? ( 685 ! v← exec_expr ge e m a;:699 ! 〈v,tr〉 ← exec_expr ge e m a;: 686 700 ! 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〉) 688 702  Swhile a s' ⇒ Some ? ( 689 ! v← exec_expr ge e m a;:703 ! 〈v,tr〉 ← exec_expr ge e m a;: 690 704 ! b ← bool_of_val_3 v (typeof a);: 691 ret ? 〈 E0, if b then State f s' (Kwhile a s' k) e m692 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〉) 693 707  Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉) 694 708  Sfor a1 a2 a3 s' ⇒ 695 709 match is_Sskip a1 with 696 710 [ inl _ ⇒ Some ? ( 697 ! v← exec_expr ge e m a2;:711 ! 〈v,tr〉 ← exec_expr ge e m a2;: 698 712 ! 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〉) 700 714  inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉) 701 715 ] … … 708 722  Some a ⇒ Some ? ( 709 723 ! 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))〉) 712 726 ] 713 727  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〉 716 730  _ ⇒ Wrong ??? ]) 717 731  Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉) … … 721 735  None ⇒ Some ? (Wrong ???) 722 736 ] 737  Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉) 723 738 ] 724 739  Callstate f0 vargs k m ⇒ … … 756 771 ##[ nrewrite > c7; napply step_skip_call; //; napply c8; 757 772 ## napply step_skip_or_continue_while; @; //; 758 ## napply sig_bindIO _OK; #vHv;773 ## napply sig_bindIO2_OK; #v tr Hv; 759 774 napply sig_bindIO_OK; #b; ncases b; #Hb; 760 775 ##[ napply (step_skip_or_continue_dowhile_true … Hv); … … 766 781 ## napply step_skip_break_switch; @; //; 767 782 ## nrewrite > c11; napply step_skip_call; //; napply c12; 768 ## napply sig_bindIO _OK; #x; ncases x; #y; ncases y; #pcl loc ofsHlval;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; 770 785 napply opt_bindIO_OK; #m' em'; 771 786 nwhd; napply (step_assign … Hlval Hv2 em'); 772 ## napply sig_bindIO _OK; #vfHvf;773 napply sig_bindIO _OK; #vargsHvargs;787 ## napply sig_bindIO2_OK; #vf tr1 Hvf; 788 napply sig_bindIO2_OK; #vargs tr2 Hvargs; 774 789 napply opt_bindIO_OK; #fd efd; 775 790 napply bindIO_OK; #ety; … … 777 792 ##[ napply (step_call_none … Hvf Hvargs efd ety); 778 793 ## #lhs'; 779 napply sig_bindIO _OK; #x; ncases x; #y; ncases y; #pcl loc ofsHlocofs;794 napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs; 780 795 nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety); 781 796 ##] 782 ## napply sig_bindIO _OK; #vHv;797 ## napply sig_bindIO2_OK; #v tr Hv; 783 798 napply sig_bindIO_OK; #b; ncases b; #Hb; 784 799 ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb); 785 800 ## napply (step_ifthenelse_false … Hv); napply (bool_of … Hb) 786 801 ##] 787 ## napply sig_bindIO _OK; #vHv;802 ## napply sig_bindIO2_OK; #v tr Hv; 788 803 napply sig_bindIO_OK; #b; ncases b; #Hb; 789 804 ##[ napply (step_while_true … Hv); napply (bool_of … Hb); … … 791 806 ##] 792 807 ## nrewrite > c11; 793 napply sig_bindIO _OK; #vHv;808 napply sig_bindIO2_OK; #v tr Hv; 794 809 napply sig_bindIO_OK; #b; ncases b; #Hb; 795 810 ##[ napply (step_for_true … Hv); napply (bool_of … Hb); … … 799 814 ## napply step_skip_break_switch; @2; //; 800 815 ## napply step_skip_or_continue_while; @2; //; 801 ## napply sig_bindIO _OK; #vHv;816 ## napply sig_bindIO2_OK; #v tr Hv; 802 817 napply sig_bindIO_OK; #b; ncases b; #Hb; 803 818 ##[ napply (step_skip_or_continue_dowhile_true … Hv); … … 809 824 ## napply step_return_0; napply c9; 810 825 ## napply sig_bindIO_OK; #u Hnotvoid; 811 napply sig_bindIO _OK; #vHv;826 napply sig_bindIO2_OK; #v tr Hv; 812 827 nwhd; napply (step_return_1 … Hnotvoid Hv); 813 ## napply sig_bindIO _OK; #v; ncases v; //; #nHv;828 ## napply sig_bindIO2_OK; #v; ncases v; //; #n tr Hv; 814 829 napply step_switch; //; 815 830 ## napply step_goto; nrewrite < c12; napply c9; 
Csemantics/Csem.ma
r155 r175 568 568 [e] is the current environment and [m] is the current memory state. *) 569 569 570 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → Prop ≝570 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ 571 571  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 573 573  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 582 582  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) 627 630 628 631 (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] … … 630 633 that contains the value of the expression [a]. *) 631 634 632 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block > int >Prop ≝635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝ 633 636  eval_Evar_local: ∀id,l,ty. 634 637 (* 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 636 639  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. 652 655 653 656 (* … … 659 662 expressions [al] to their values [vl]. *) 660 663 661 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr > list val > Prop :=664 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ 662 665  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). 668 671 669 672 (*End EXPR.*) … … 783 786 (* * Transition relation *) 784 787 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 790 ninductive 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' → 791 796 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 → 799 804 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 → 808 813 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) 810 815 811 816  step_seq: ∀f,s1,s2,k,e,m. … … 822 827 E0 (State f Sbreak k e m) 823 828 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) → 827 832 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) → 832 837 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) → 838 843 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) → 843 848 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) 845 850  step_skip_or_continue_while: ∀f,x,a,s,k,e,m. 846 x = Sskip ∨ x = Scontinue >851 x = Sskip ∨ x = Scontinue → 847 852 step ge (State f x (Kwhile a s k) e m) 848 853 E0 (State f (Swhile a s) k e m) … … 854 859 step ge (State f (Sdowhile a s) k e m) 855 860 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) → 860 865 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) → 866 871 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) 868 873  step_break_dowhile: ∀f,a,s,k,e,m. 869 874 step ge (State f Sbreak (Kdowhile a s k) e m) … … 871 876 872 877  step_for_start: ∀f,a1,a2,a3,s,k,e,m. 873 a1 ≠ Sskip >878 a1 ≠ Sskip → 874 879 step ge (State f (Sfor a1 a2 a3 s) k e m) 875 880 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) → 879 884 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) → 884 889 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) 886 891  step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m. 887 x = Sskip ∨ x = Scontinue >892 x = Sskip ∨ x = Scontinue → 888 893 step ge (State f x (Kfor2 a2 a3 s k) e m) 889 894 E0 (State f a3 (Kfor3 a2 a3 s k) e m) … … 896 901 897 902  step_return_0: ∀f,k,e,m. 898 fn_return f = Tvoid >903 fn_return f = Tvoid → 899 904 step ge (State f (Sreturn (None ?)) k e m) 900 905 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 → 904 909 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))) 906 911  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 → 909 914 step ge (State f Sskip k e m) 910 915 E0 (Returnstate Vundef k (free_list m (blocks_of_env e))) 911 916 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 → 914 919 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) 916 921  step_skip_break_switch: ∀f,x,k,e,m. 917 x = Sskip ∨ x = Sbreak >922 x = Sskip ∨ x = Sbreak → 918 923 step ge (State f x (Kswitch k) e m) 919 924 E0 (State f Sskip k e m) … … 927 932 928 933  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'〉 → 930 935 step ge (State f (Sgoto lbl) k e m) 931 936 E0 (State f s' k' e m) 932 937 933 938  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 → 936 941 step ge (Callstate (Internal f) vargs k m) 937 942 E0 (State f (fn_body f) k e m2) 938 943 939 944  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 → 941 946 step ge (Callstate (External id targs tres) vargs k m) 942 947 t (Returnstate vres k m) … … 947 952 948 953  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' → 950 955 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). 952 961 (* 953 962 (** * Alternate bigstep semantics *) 
Csemantics/Csyntax.ma
r156 r175 20 20 include "Coqlib.ma". 21 21 include "Errors.ma". 22 include "CostLabel.ma". 22 23 23 24 (* * * Abstract syntax *) … … 189 190  Eorbool: expr → expr → expr_descr (**r sequential or ([]) *) 190 191  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. 192 194 193 195 (* * Extract the type part of a typeannotated Clight expression. *) … … 220 222  Slabel : label → statement → statement 221 223  Sgoto : label → statement 224  Scost : costlabel → statement → statement 222 225 223 226 with labeled_statements : Type ≝ (**r cases of a [switch] *) … … 241 244 (Sla:∀l,s. P s → P (Slabel l s)) 242 245 (Sgo:∀l. P (Sgoto l)) 246 (Scs:∀l,s. P s → P (Scost l s)) 243 247 (LSd:∀s. P s → Q (LSdefault s)) 244 248 (LSc:∀i,s,t. P s → Q t → Q (LScase i s t)) … … 249 253  Scall eo e args ⇒ Sca eo e args 250 254  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) 253 257  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) 256 260  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) 258 262  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) 260 264  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) 264 268  Sbreak ⇒ Sbr 265 269  Scontinue ⇒ Sco 266 270  Sreturn eo ⇒ Sre eo 267 271  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) 269 273  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) 271 275  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) 272 278 ] 273 279 and labeled_statements_ind2 … … 287 293 (Sla:∀l,s. P s → P (Slabel l s)) 288 294 (Sgo:∀l. P (Sgoto l)) 295 (Scs:∀l,s. P s → P (Scost l s)) 289 296 (LSd:∀s. P s → Q (LSdefault s)) 290 297 (LSc:∀i,s,t. P s → Q t → Q (LScase i s t)) … … 292 299 match ls with 293 300 [ 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) 295 302  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) 298 305 ]. 299 306 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 307 ndefinition 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 302 309 (λ_,_. I) (λ_,_,_,_,_.I). 303 310 
Csemantics/Events.ma
r3 r175 24 24 include "datatypes/list.ma". 25 25 include "extralib.ma". 26 include "CostLabel.ma". 26 27 27 28 (* * The observable behaviour of programs is stated in terms of … … 40 41  EVfloat: float > eventval. 41 42 42 nrecord event : Type := { 43 ev_name: ident; 44 ev_args: list eventval; 45 ev_res: eventval 46 }. 43 ninductive event : Type ≝ 44  EVcost: costlabel → event 45  EVextcall: ∀ev_name: ident. ∀ev_args: list eventval. ∀ev_res: eventval. event. 47 46 48 47 (* * The dynamic semantics for programs collect traces of events. … … 53 52 ndefinition E0 : trace := nil ?. 54 53 54 ndefinition Echarge : costlabel → trace ≝ 55 λlabel. EVcost label :: (nil ?). 56 55 57 ndefinition Eextcall : ident → list eventval → eventval → trace ≝ 56 58 λname: ident. λargs: list eventval. λres: eventval. 57 mk_eventname args res :: (nil ?).59 EVextcall name args res :: (nil ?). 58 60 59 61 ndefinition Eapp : trace → trace → trace ≝ λt1,t2. t1 @ t2.
Note: See TracChangeset
for help on using the changeset viewer.