Changeset 3154 for src/joint/joint_semantics.ma
 Timestamp:
 Apr 17, 2013, 2:53:45 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/joint_semantics.ma
r3037 r3154 516 516 ! bl ← match f with 517 517 [ inl id ⇒ 518 opt_to_res … [MSG BadFunction; CTX … id] 519 (find_symbol … ge id) 518 !bl ← opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id) ; 519 if eqZb (block_id bl) (1) then 520 Error … [MSG BadFunction; CTX … id] 521 else return bl 520 522  inr addr ⇒ 521 523 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 522 524 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 523 525 ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ; 524 if eq_bv … (bv_zero …) (offv (poff ptr)) then 526 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ 527 (notb (eqZb (block_id (pblock ptr)) (1))) then 525 528 return pblock ptr 526 529 else … … 529 532 opt_to_res … [MSG BadFunction; MSG BadPointer] 530 533 (code_block_of_block bl). 534 535 lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region. 536 ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → 537 (∀ prf : r = Code.P (g prf)) → 538 P ((match r return λx.(r = x → ?) with 539 [XData ⇒ f  Code ⇒ g])(refl ? r)). 540 #A #P * #f #g #H1 #H2 normalize nodelta [ @H1  @H2] 541 qed. 542 543 lemma block_of_call_no_minus_one : ∀p,globals,ge,f,st,bl. 544 block_of_call p globals ge f st = return bl → 545 block_id bl ≠ 1. 546 #p #globals #ge #f #st #bl whd in match block_of_call; normalize nodelta 547 #H cases(bind_inversion ????? H) #bl1 cases f f normalize nodelta 548 [ #id * #H cases(bind_inversion ????? H) H #bl2 * #_ @eqZb_elim #EQbl2 549 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 550 #H lapply(opt_eq_from_res ???? H) H whd in match code_block_of_block; 551 normalize nodelta @match_reg_elim [ #_ #EQ destruct] #prf #EQ destruct(EQ) 552 assumption 553  * #dpl #dph * #H cases(bind_inversion ????? H) H #bv1 * #_ #H 554 cases(bind_inversion ????? H) H #bv2 * #_ #H cases(bind_inversion ????? H) H 555 #ptr * #_ @eq_bv_elim #_ normalize nodelta [2: whd in ⊢ (??%% → ?); #EQ destruct] 556 @eqZb_elim #EQptr normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct 557 #H lapply(opt_eq_from_res ???? H) H whd in match code_block_of_block; 558 normalize nodelta @match_reg_elim [#_ #EQ destruct] #prf #EQ destruct 559 assumption 560 ] 561 qed. 562 531 563 532 564 definition eval_external_call ≝
Note: See TracChangeset
for help on using the changeset viewer.