Changeset 2470 for src/joint/semantics.ma
 Timestamp:
 Nov 15, 2012, 7:06:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semantics.ma
r2462 r2470 117 117 record state_pc (semp : sem_state_params) : Type[0] ≝ 118 118 { st_no_pc :> state semp 119 ; pc : cpointer119 ; pc : program_counter 120 120 }. 121 121 … … 265 265 ∀globals. 266 266 ∀ge : genv pars globals. 267 cpointer →267 program_counter → 268 268 res (Σi.is_internal_function … ge i) ≝ 269 269 λpars,globals,ge,p. 270 270 opt_to_res … [MSG BadFunction; MSG BadPointer] 271 (int_funct_of_block … ge (p block p)).271 (int_funct_of_block … ge (pc_block p)). 272 272 273 273 record sem_unserialized_params … … 290 290 ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval 291 291 ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) 292 ; fetch_ra: state st_pars → res ( cpointer × (state st_pars))292 ; fetch_ra: state st_pars → res (program_counter × (state st_pars)) 293 293 294 294 ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars 295 295 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 296 ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)296 ; save_frame: program_counter → call_dest uns_pars → state st_pars → res (state st_pars) 297 297 (*CSC: setup_call returns a res only because we can call a function with the wrong number and 298 298 type of arguments. To be fixed using a dependent type *) … … 362 362 return 〈bv, set_istack … is st〉. 363 363 364 definition save_ra : ∀p. state p → cpointer → res (state p) ≝364 definition save_ra : ∀p. state p → program_counter → res (state p) ≝ 365 365 λp,st,l. 366 366 let 〈addrl,addrh〉 ≝ beval_pair_of_pc l in … … 368 368 push … st' addrh. 369 369 370 definition load_ra : ∀p.state p → res ( cpointer × (state p)) ≝370 definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝ 371 371 λp,st. 372 372 ! 〈addrh, st'〉 ← pop … st; … … 378 378 record more_sem_params (pp : params) : Type[1] ≝ 379 379 { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp) 380 ; offset_of_point : code_point pp → option offset (* can overflow *)381 ; point_of_offset : offset→ code_point pp380 ; offset_of_point : code_point pp → Pos 381 ; point_of_offset : Pos → code_point pp 382 382 ; point_of_offset_of_point : 383 ∀pt. opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))383 ∀pt.point_of_offset (offset_of_point pt) = pt 384 384 ; offset_of_point_of_offset : 385 ∀o.offset_of_point (point_of_offset o) = Some ?o385 ∀o.offset_of_point (point_of_offset o) = o 386 386 }. 387 387 … … 399 399 ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*) 400 400 401 axiom CodePointerOverflow : String. 402 403 definition pointer_of_point : ∀p.more_sem_params p → 404 cpointer→ code_point p → res cpointer ≝ 401 definition pc_of_point : ∀p.more_sem_params p → 402 program_counter → code_point p → program_counter ≝ 405 403 λp,msp,ptr,pt. 406 ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ; 407 return «mk_pointer (pblock ptr) o, ?». 408 elim ptr #ptr' #EQ <EQ % qed. 409 410 definition point_of_pointer : 411 ∀p.more_sem_params p → cpointer → code_point p ≝ 412 λp,msp,ptr.point_of_offset p msp (poff ptr). 404 mk_program_counter (pc_block ptr) (offset_of_point ? msp pt). 405 406 definition point_of_pc : 407 ∀p.more_sem_params p → program_counter → code_point p ≝ 408 λp,msp,ptr.point_of_offset p msp (pc_offset ptr). 413 409 414 410 lemma point_of_pointer_of_point : 415 ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt. 416 pointer_of_point p msp ptr1 pt = return ptr2 → 417 point_of_pointer p msp ptr2 = pt. 418 #p #msp #ptr1 #ptr2 #pt normalize 419 lapply (point_of_offset_of_point p msp pt) 420 cases (offset_of_point ???) normalize 421 [ * #ABS destruct(ABS) 422  #o #EQ1 #EQ2 destruct % 423 ] 424 qed. 411 ∀p,msp.∀ptr,pt. 412 point_of_pc ? msp (pc_of_point p msp ptr pt) = pt. 413 #p #msp #ptr #pt normalize // qed. 425 414 426 415 lemma pointer_of_point_block : 427 ∀p,msp,ptr1,ptr2,pt. 428 pointer_of_point p msp ptr1 pt = return ptr2 → 429 pblock ptr2 = pblock ptr1. 430 #p #msp #ptr1 #ptr2 #pt normalize 431 cases (offset_of_point ???) normalize 432 [ #ABS destruct(ABS) 433  #o #EQ destruct(EQ) % 434 ] 435 qed. 416 ∀p,msp,ptr,pt. 417 pc_block (pc_of_point p msp ptr pt) = pc_block ptr. 418 #p #msp #ptr #pt % qed. (* can probably do without *) 436 419 437 420 lemma pointer_of_point_uses_block : 438 ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt. 439 #p #msp ** #b1 #o1 #EQ1 440 ** #b2 #o2 #EQ2 441 #pt #EQ3 destruct normalize // 442 qed. 421 ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 → 422 pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt. 423 #p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed. 443 424 444 425 lemma pointer_of_point_of_pointer : 445 ∀p,msp.∀ptr1,ptr2 : cpointer. 446 pblock ptr1 = pblock ptr2 → 447 pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2. 448 #p #msp ** #b1 #o1 #EQ1 449 ** #b2 #o2 #EQ2 450 #EQ3 destruct 451 normalize >offset_of_point_of_offset normalize % 452 qed. 426 ∀p,msp.∀ptr1,ptr2. 427 pc_block ptr1 = pc_block ptr2 → 428 pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2. 429 #p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed. 453 430 454 431 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 455 ∀ge:genv p globals. cpointer →432 ∀ge:genv p globals. program_counter → 456 433 res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝ 457 434 λp,msp,globals,ge,ptr. 458 let bl ≝ pblock ptr in 459 ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer] 460 (int_funct_of_block … ge bl) ; 435 ! f ← fetch_function … ge ptr ; 461 436 let fn ≝ if_of_function … f in 462 let pt ≝ point_of_p ointer? msp ptr in437 let pt ≝ point_of_pc ? msp ptr in 463 438 ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); 464 439 return 〈f, stmt〉. 465 440 466 definition p ointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.467 genv p globals → cpointer → label → res cpointer ≝441 definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 442 genv p globals → program_counter → label → res program_counter ≝ 468 443 λp,msp,globals,ge,ptr,lbl. 469 444 ! f ← fetch_function … ge ptr ; … … 471 446 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 472 447 (point_of_label … (joint_if_code … fn) lbl) ; 473 pointer_of_point p msp ptr pt.448 return pc_of_point p msp ptr pt. 474 449 475 450 definition succ_pc : ∀p : params.∀ msp : more_sem_params p. 476 cpointer → succ p → res cpointer ≝451 program_counter → succ p → program_counter ≝ 477 452 λp,msp,ptr,nxt. 478 let curr ≝ point_of_p ointerp msp ptr in479 p ointer_of_point p msp ptr (point_of_succ p curr nxt).453 let curr ≝ point_of_pc p msp ptr in 454 pc_of_point p msp ptr (point_of_succ p curr nxt). 480 455 481 456 record sem_params : Type[1] ≝ … … 517 492 518 493 definition goto: ∀globals.∀p : sem_params. 519 genv p globals → label → state p → cpointer → res (state_pc p) ≝494 genv p globals → label → state p → program_counter → res (state_pc p) ≝ 520 495 λglobals,p,ge,l,st,b. 521 ! newpc ← p ointer_of_label ? p … ge b l ;496 ! newpc ← pc_of_label ? p … ge b l ; 522 497 return mk_state_pc ? st newpc. 523 498 … … 527 502 *) 528 503 529 definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p)≝504 definition next : ∀p : sem_params.succ p → state p → program_counter → state_pc p ≝ 530 505 λp,l,st,pc. 531 ! newpc ← succ_pc ? p … pc l ;532 returnmk_state_pc … st newpc.506 let newpc ≝ succ_pc ? p … pc l in 507 mk_state_pc … st newpc. 533 508 534 509 … … 572 547 let fn ≝ if_of_function … ge i in 573 548 let l' ≝ joint_if_entry ?? fn in 574 let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in 575 pointer_of_point ? p … pointer_in_fn l'. 549 mk_program_counter (block_of_funct_ident … ge (pi1 … i)) (offset_of_point ? p … l'). 576 550 [ @block_of_funct_ident_is_code 577 551  cases i /2 by internal_function_is_function/ … … 589 563 definition eval_seq_no_pc : 590 564 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) → 591 state p → cpointer → joint_seq p globals →565 state p → program_counter → joint_seq p globals → 592 566 IO io_out io_in (state p) ≝ 593 567 λp,globals,ge,curr_fn,st,next,seq. … … 662 636 definition eval_seq_pc : 663 637 ∀p:sem_params.∀globals.∀ge:genv p globals. 664 state p → cpointer → joint_seq p globals →665 res cpointer ≝638 state p → program_counter → joint_seq p globals → 639 res program_counter ≝ 666 640 λp,globals,ge,st,next,s. 667 641 match s with … … 669 643 ! fn ← function_of_call … ge st f; 670 644 match ? return λx.description_of_function … fn = x → ? with 671 [ Internal _ ⇒ λprf. eval_internal_call_pc … ge «fn, ?»645 [ Internal _ ⇒ λprf.return eval_internal_call_pc … ge «fn, ?» 672 646  External _ ⇒ λ_.return next 673 647 ] (refl …) … … 685 659 match s with 686 660 [ sequential s next ⇒ 687 ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ;661 let next_ptr ≝ succ_pc ? p (pc … st) next in 688 662 match s return λ_.IO ??? with 689 663 [ step_seq s ⇒ … … 696 670 ! pc' ← 697 671 if b then 698 p ointer_of_label ? p … ge (pc … st) l672 pc_of_label ? p … ge (pc … st) l 699 673 else 700 succ_pc ? p (pc … st) next ;674 return succ_pc ? p (pc … st) next ; 701 675 return mk_state_pc … st pc' 702 676 ] … … 704 678 match s with 705 679 [ GOTO l ⇒ 706 ! pc' ← p ointer_of_label ? p ? ge (pc … st) l ;680 ! pc' ← pc_of_label ? p ? ge (pc … st) l ; 707 681 return mk_state_pc … st pc' 708 682  RETURN ⇒ … … 714 688 match ? return λx.description_of_function … fn = x → ? with 715 689 [ Internal _ ⇒ λprf. 716 ! pc' ← eval_internal_call_pc … ge «fn, ?» ;690 let pc' ≝ eval_internal_call_pc … ge «fn, ?» in 717 691 return mk_state_pc … st pc' 718 692  External fd ⇒ λ_. … … 738 712 not static... *) 739 713 definition is_final: ∀globals:list ident. ∀p: sem_params. 740 genv p globals → cpointer → state_pc p → option int ≝714 genv p globals → program_counter → state_pc p → option int ≝ 741 715 λglobals,p,ge,exit,st.res_to_opt ? ( 742 716 do 〈f,s〉 ← fetch_statement ? p … ge (pc … st); … … 747 721 [ RETURN ⇒ 748 722 do 〈ra, st'〉 ← fetch_ra … st; 749 if eq_p ointer ra exit then723 if eq_program_counter ra exit then 750 724 do vals ← read_result … ge (joint_if_result … fn) st' ; 751 725 Word_of_list_beval vals … … 761 735 { globals: list ident 762 736 ; sparams:> sem_params 763 ; exit: cpointer737 ; exit: program_counter 764 738 ; genv2: genv globals sparams 765 739 }.
Note: See TracChangeset
for help on using the changeset viewer.