Changeset 2473
 Timestamp:
 Nov 16, 2012, 6:59:24 PM (7 years ago)
 Location:
 src
 Files:

 1 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2470 r2473 11 11 12 12 13 (* move elsewhere *)14 definition is_internal_function_of_program :15 ∀A,B.program (λvars.fundef (A vars)) B → ident → Prop ≝16 λA,B,prog,i.∃ifd.In … (prog_funct ?? prog) 〈i, Internal ? ifd〉.17 18 lemma opt_elim : ∀A.∀m : option A.∀P : option A → Prop.19 (m = None ? → P (None ?)) →20 (∀x.m = Some ? x → P (Some ? x)) → P m.21 #A * [2: #x] #P #H1 #H222 [ @H2  @H1 ] % qed.23 24 axiom find_funct_ptr_symbol_inversion:25 ∀F,V,init. ∀p: program F V.26 ∀id: ident. ∀b: block. ∀f: F ?.27 find_symbol ? (globalenv ?? init p) id = Some ? b →28 find_funct_ptr ? (globalenv ?? init p) b = Some ? f →29 In … (prog_funct ?? p) 〈id, f〉.30 31 lemma is_internal_function_of_program_ok :32 ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.33 is_internal_function ?? (globalenv ?? init prog) i →34 is_internal_function_of_program ?? prog i.35 #A #B #init #prog #i whd in ⊢ (%→%); * #ifn36 @(opt_elim … (find_symbol … i)) [#_ #ABS normalize in ABS; destruct(ABS) ]37 #bl #EQbl >m_return_bind #EQfind %{ifn}38 @(find_funct_ptr_symbol_inversion … EQbl EQfind)39 qed.40 13 41 14 record prog_params : Type[1] ≝ … … 45 18 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 46 19 }. 20 21 lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l. 22 #A #B #f #P #l elim l l [*] 23 #hd #tl #IH * 24 [ #Phd %1{Phd} 25  #Ptl %2{(IH Ptl)} 26 ] 27 qed. 28 29 lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x. 30 #A #P #l elim l l [*] #hd #tl #IH * 31 [ #Phd %{hd} %{Phd} %1 % 32  #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1} 33 ] 34 qed. 35 36 lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l. 37 #A #P #l elim l l [ #x *] #hd #tl #IH #x * 38 [ #EQ >EQ #H %1{H} 39  #Intl #Px %2{(IH … Intl Px)} 40 ] 41 qed. 47 42 48 43 definition make_global : prog_params → evaluation_params … … 60 55 (* (prog_io pars) *). 61 56 [ @(is_internal_function_of_program_ok … (pi2 … i)) 62  (* TODO or TOBEFOUND *) 63 cases daemon 57  #s #H 58 lapply (map_Exists … H) H #H 59 elim (Exists_In … H) H ** #id #r #v * #id_in #EQ destruct(EQ) 60 elim (find_symbol_exists ??????? id_in) 61 [ #bl #EQ >EQ % #ABS destruct(ABS)] 64 62 ] 65 63 qed. … … 90 88 match ? return λx.description_of_function … main = x → ? with 91 89 [ Internal fn ⇒ λprf. 92 let main : Σi : ident.is_internal_function ??? ?≝ «main, ?» in90 let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in 93 91 ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ; 94 92 let pc' ≝ eval_internal_call_pc … ge main in … … 157 155 [ #fn normalize nodelta 158 156 lapply (refl … (description_of_function … (ev_genv p) fn)) 159 elim (description_of_function ?? ??) in ⊢ (???%→%); #fd157 elim (description_of_function ?? fn) in ⊢ (???%→%); #fd 160 158 #EQfd 161 159  #e … … 171 169 qed. 172 170 171 definition joint_after_ret : ∀p:evaluation_params. 172 (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝ 173 λp,s1,s2. 174 match fetch_statement ? p … (ev_genv p) (pc … s1) with 175 [ OK x ⇒ 176 match \snd x with 177 [ sequential s next ⇒ 178 pc … s2 = succ_pc p p (pc … s1) next 179  _ ⇒ False (* never happens *) 180 ] 181  _ ⇒ False (* never happens *) 182 ]. 183 173 184 definition joint_call_ident : ∀p:evaluation_params. 174 185 (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝ 186 (* this is a definition without a dummy ident : 175 187 λp,st. 176 188 match ? … … 198 210 lapply ABS ABS 199 211 >EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS) 200 qed. 212 qed. *) 213 (* with a dummy ident (which is never used as seen above in the commented script) 214 I think handling of the function is easier *) 215 λp,st. 216 let dummy : ident ≝ an_identifier ? one in 217 match fetch_statement ? p … (ev_genv p) (pc … st) with 218 [ OK x ⇒ 219 match \snd x with 220 [ sequential s next ⇒ 221 match s with 222 [ step_seq s ⇒ 223 match s with 224 [ CALL f' args dest ⇒ 225 match function_of_call … (ev_genv p) st f' with 226 [ OK f ⇒ f 227  _ ⇒ dummy 228 ] 229  _ ⇒ dummy 230 ] 231  _ ⇒ dummy 232 ] 233  _ ⇒ dummy 234 ] 235  _ ⇒ dummy 236 ]. 201 237 202 238 definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. … … 250 286  _ ⇒ None ? 251 287 ]) 252 (* as_after_return ≝ *) 253 (λs1,s2. 254 (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *) 255 ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧ 256 succ_pc p p (pc … s1) nxt = pc … s2) 288 (* as_after_return ≝ *) (joint_after_ret p) 257 289 (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?) 258 290 (* as_call_ident ≝ *) (joint_call_ident p). 
src/joint/linearise.ma
r2440 r2473 1 1 include "joint/TranslateUtils.ma". 2 include "common/extraGlobalenvs.ma". 2 3 include "utilities/hide.ma". 3 4 … … 553 554 qed. 554 555 556 557 definition good_local_sigma : 558 ∀p:unserialized_params. 559 ∀globals. 560 ∀g:codeT (mk_graph_params p) globals. 561 (Σl.bool_to_Prop (code_has_label … g l)) → 562 codeT (mk_lin_params p) globals → 563 (label → option ℕ) → Prop ≝ 564 λp,globals,g,entry,c,sigma. 565 sigma entry = Some ? 0 ∧ 566 ∀l,n.sigma l = Some ? n → 567 ∃s. lookup … g l = Some ? s ∧ 568 opt_Exists ? 569 (λls.let 〈lopt, ts〉 ≝ ls in 570 opt_All ? (eq ? l) lopt ∧ 571 ts = graph_to_lin_statement … s ∧ 572 opt_All ? 573 (λnext.Or (sigma next = Some ? (S n)) 574 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 575 (stmt_implicit_label … s)) (nth_opt … n c). 576 555 577 definition linearise_code: 556 578 ∀p : unserialized_params.∀globals. 557 579 ∀g : codeT (mk_graph_params p) globals.code_closed … g → 558 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). 559 (Σc : codeT (mk_lin_params p) globals. 560 code_closed … c ∧ 580 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)) 581 .Σ〈c, sigma〉. 582 good_local_sigma … g entry c sigma ∧ 583 code_closed … c 584 (* ∧ 561 585 ∃ sigma : identifier_map LabelTag ℕ. 562 586 lookup … sigma entry = Some ? 0 ∧ … … 570 594 (λnext.Or (lookup … sigma next = Some ? (S n)) 571 595 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 572 (stmt_implicit_label … s)) (nth_opt … n c) )596 (stmt_implicit_label … s)) (nth_opt … n c)*) 573 597 ≝ 574 598 λp,globals,g,g_prf,entry_sig. … … 583 607 let crev ≝ \snd triple in 584 608 let lbld_code ≝ rev ? crev in 585 mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ]. 586 [ (* done later *) 609 〈filter_labels … (λl.l∈required) lbld_code, lookup … sigma〉 ]. 610 [ cases (graph_visit ????????????????????) 611 (* done later *) 587 612  #i >mem_set_empty * 588 613 3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS) … … 594 619  >commutative_plus change with (? ≤ g) % 595 620 ] 596 lapply (refl … triple) 597 generalize in match triple in ⊢ (???%→%); ** 598 #visited #required #generated #EQtriple 599 >EQtriple in H ⊢ %; normalize nodelta **** 621 ** 622 #visited #required #generated normalize nodelta **** 600 623 #entry_O #req_vis #last_fin #labels_in_req #sigma_prop 601 % >EQtriple 602 [ #i #s 624 % 625 [ % [assumption] 626 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 627 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 628 % [2: % [ assumption ] ] 629 >nth_opt_filter_labels in ⊢ (???%); 630 >nth_opt_is_stmt >m_return_bind whd >m_return_bind 631 % [ % ] 632 [ elim (lbl ∈ required) % 633  % 634  lapply succ_is_in 635 lapply (refl … (stmt_implicit_label … stmt)) 636 cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] 637 #next #EQ_next * 638 [ #H %1{H} ] 639 #H %2 640 >nth_opt_filter_labels >H % 641 ] 642  #i #s 603 643 >stmt_at_filter_labels #EQ 604 644 % … … 628 668 ] 629 669 ] 630 %{visited} % [assumption] 631 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 632 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 633 % [2: % [ assumption ] ] 634 >nth_opt_filter_labels in ⊢ (???%); 635 >nth_opt_is_stmt >m_return_bind whd >m_return_bind 636 % [ % ] 637 [ elim (lbl ∈ required) % 638  % 639  lapply succ_is_in 640 lapply (refl … (stmt_implicit_label … stmt)) 641 cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] 642 #next #EQ_next * 643 [ #H %1{H} ] 644 #H %2 645 >nth_opt_filter_labels >H % 646 ] 647 qed. 648 649 (* Paolo: for now I'm leaving the closed graph stuff out, waiting for it to 650 be done on all passes *) 670 qed. 671 651 672 definition linearise_int_fun : 652 673 ∀p : unserialized_params. 653 674 ∀globals. 654 joint_closed_internal_function (mk_graph_params p) globals → 655 joint_closed_internal_function (mk_lin_params p) globals 675 ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals 676 .Σ〈fn_out : joint_closed_internal_function (mk_lin_params p) globals, 677 sigma : ?〉. 678 good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in) 679 (joint_if_code … fn_out) sigma 656 680 (* ∃sigma : identifier_map LabelTag ℕ. 657 681 let g ≝ joint_if_code ?? (pi1 … fin) in … … 669 693 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 670 694 (stmt_implicit_label … s)) (nth_opt … n c)*) ≝ 671 λp,globals,f_sig.let f_in ≝ pi1 … f_sig in 672 «mk_joint_internal_function (mk_lin_params p) globals 673 (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in) 674 (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in) 675 (joint_if_stacksize ?? f_in) 676 (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in)) 677 0 0 (* exit is dummy! *), ?». [2,4:// ] 678 elim (linearise_code ?????) #c * #code_closed 679 [3: #_ assumption ] 680 @hide_prf 681 * #sigma * #O_in #sigma_prop 682 >lin_code_has_point 683 elim (sigma_prop … O_in) #s * #_ 684 cases c 685 [1,3: * 686 *: #hd #tl #_ % 695 λp,globals,f_sig. 696 let code_sigma ≝ linearise_code … 697 (joint_if_code … f_sig) 698 (pi2 … f_sig) 699 (joint_if_entry … f_sig) in 700 let code ≝ \fst code_sigma in 701 let sigma ≝ \snd code_sigma in 702 let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in 703 〈«mk_joint_internal_function (mk_lin_params p) globals 704 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 705 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig) 706 (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?», 707 sigma〉. 708 normalize nodelta 709 cases (linearise_code ?????) * #code #sigma normalize nodelta * #H1 #H2 710 [ @H2 711  @H1 712  cases H1 #H3 #H4 elim (H4 … H3) 713 #s * #_ >lin_code_has_point cases code 714 [ *  #hd #tl #_ % ] 687 715 ] 688 716 qed. … … 690 718 definition linearise : ∀p : unserialized_params. 691 719 program (joint_function (mk_graph_params p)) ℕ → 692 program (joint_function (mk_lin_params p)) ℕ ≝ 720 program (joint_function (mk_lin_params p)) ℕ 721 ≝ 693 722 λp,pr.transform_program ??? pr 694 (λglobals.transf_fundef ?? (linearise_int_fun p globals)). 723 (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))). 724 725 726 definition good_sigma : 727 ∀p:unserialized_params. 728 ∀prog_in : joint_program (mk_graph_params p). 729 ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝ 730 λp,prog_in,sigma. 731 let prog_out ≝ linearise … prog_in in 732 ∀i. 733 let fn_in ≝ prog_if_of_function ?? prog_in i in 734 let fn_out ≝ prog_if_of_function ?? prog_out «i, hide_prf ??» in 735 let sigma_local ≝ sigma i in 736 good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in) 737 (joint_if_code ?? fn_out) sigma_local. 738 @if_propagate @(pi2 … i) 739 qed. 740 741 lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma. 742 #p #prog 743 letin sigma ≝ 744 (λi. 745 let fn_in ≝ prog_if_of_function ?? prog i in 746 \snd (linearise_int_fun … fn_in)) 747 %{sigma} 748 * #i #i_prf >(prog_if_of_function_transform … i_prf) 749 normalize nodelta 750 cases (linearise_int_fun ???) * #fn_out #sigma_loc 751 normalize nodelta #prf @prf 752 qed. 
src/joint/semantics.ma
r2470 r2473 5 5 include "joint/Joint.ma". 6 6 include "ASM/I8051bis.ma". 7 include "common/extraGlobalenvs.ma". 7 8 8 9 (* CSC: external functions never fail (??) and always return something of the … … 11 12 only the head is kept (or Undef if the list is empty) ??? *) 12 13 13 definition is_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).14 λi : ident.∃fd.15 ! bl ← find_symbol … ge i ;16 find_funct_ptr … ge bl = Some ? fd.17 18 definition description_of_function : ∀F,globals,ge.(Σi.is_function F globals ge i) →19 fundef (F globals) ≝20 λF,globals,ge,i.21 match ! bl ← find_symbol … ge i ;22 find_funct_ptr … ge bl23 return λx.(∃fd.x = ?) → ?24 with25 [ Some fd ⇒ λ_.fd26  None ⇒ λprf.⊥27 ] (pi2 … i).28 cases prf #fd #ABS destruct29 qed.30 31 definition is_internal_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).32 λi : ident.∃fd.33 ! bl ← find_symbol … ge i ;34 find_funct_ptr … ge bl = Some ? (Internal ? fd).35 36 lemma description_of_internal_function : ∀F,globals,ge,i,fn.37 description_of_function F globals ge i = Internal ? fn → is_internal_function … ge i.38 #F #globals #ge * #i * #fd #EQ39 #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ40 %{EQ}41 qed.42 43 lemma internal_function_is_function : ∀F,globals,ge,i.44 is_internal_function F globals ge i → is_function … ge i.45 #F #globals #ge #i * #fn #prf %{prf} qed.46 47 definition if_of_function : ∀F,globals,ge.(Σi.is_internal_function F globals ge i) →48 F globals ≝49 λF,globals,ge,i.50 match ! bl ← find_symbol … ge i ;51 find_funct_ptr … ge bl52 return λx.(∃fn.x = ?) → ?53 with54 [ Some fd ⇒55 match fd return λx.(∃fn.Some ? x = ?) → ? with56 [ Internal fn ⇒ λ_.fn57  External _ ⇒ λprf.⊥58 ]59  None ⇒ λprf.⊥60 ] (pi2 … i).61 cases prf #fn #ABS destruct62 qed.63 64 14 (* Paolo: I'll put in this record the property about genv we need *) 65 15 record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝ 66 16 { ge :> genv_t (fundef (F globals)) 67 ; find_symbol_ exists : ∀id.In ? globals id → find_symbol … ge id≠ None ?68 ; stack_sizes : (Σi.is_internal_function F globalsge i) → ℕ17 ; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ? 18 ; stack_sizes : (Σi.is_internal_function ? ge i) → ℕ 69 19 }. 20 21 definition stack_sizes_lift : 22 ∀pars_in, pars_out : params. 23 ∀trans : ∀globals.joint_closed_internal_function pars_in globals → 24 joint_closed_internal_function pars_out globals. 25 ∀prog_in : program (joint_function pars_in) ℕ. 26 let prog_out ≝ 27 transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in 28 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) → 29 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝ 30 λpars_in,pars_out,prog_in,trans,stack_sizes. 31 λi.stack_sizes «i, if_propagate … (pi2 … i)». 70 32 71 33 definition genv ≝ λp.genv_gen (joint_closed_internal_function p). … … 160 122 *) 161 123 162 definition funct_of_ident : ∀F,globals,ge.163 ident → option (Σi.is_function F globals ge i)164 ≝ λF,globals,ge,i.165 match ?166 return λx.! bl ← find_symbol … ge i ;167 find_funct_ptr … ge bl = x → ?168 with169 [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»170  None ⇒ λ_.None ?171 ] (refl …).172 173 lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A.174 ∀Q : option A → Prop.175 ∀c1 : ∀a.Q (Some ? a) → B.176 ∀c2 : Q (None ?) → B.177 ∀P : B → Prop.178 (∀a,prf.P (c1 a prf)) →179 (∀prf.P (c2 prf)) →180 ∀prf : Q m.181 P (match m return λx.Q x → ? with182 [ Some a ⇒ λprf.c1 a prf183  None ⇒ λprf.c2 prf184 ] prf).185 #A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf186 normalize [@H1  @H2]187 qed.188 189 lemma symbol_of_function_block_ok :190 ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).191 #F #ge #b #FFP192 whd in ⊢ (???(??%));193 @match_opt_prf_elim [//] #H @⊥194 (* cut and paste from global env *)195 whd in H:(??%?);196 cases b in FFP H ⊢ %; * * b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP  *: * #H cases (H (refl ??)) ]197 cases (functions_inv … ge b FFP)198 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))199 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))200 cases (find ????)201 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ *  * #H' cases (H' (refl ??)) ]202  * #id' #b' #_ normalize #_ #E destruct203 ] qed.204 205 definition funct_of_block : ∀F,globals,ge.206 block → option (Σi.is_function F globals ge i) ≝207 λF,globals,ge,bl.208 match find_funct_ptr … ge bl209 return λx.find_funct_ptr … ge bl = x → ? with210 [ Some fd ⇒ λprf.return mk_Sig211 ident (λi.is_function F globals ge i)212 (symbol_of_function_block … ge bl ?)213 (ex_intro … fd ?)214  None ⇒ λ_.None ?215 ] (refl …).216 [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf217  >prf % #ABS destruct(ABS)218 ]219 qed.220 221 definition int_funct_of_block : ∀F,globals,ge.222 block → option (Σi.is_internal_function F globals ge i) ≝223 λF,globals,ge,bl.224 ! f ← funct_of_block … ge bl ;225 match ?226 return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)227 with228 [ Internal fn ⇒ λprf.return «pi1 … f, ?»229  External fn ⇒ λ_.None ?230 ] (refl …).231 @(description_of_internal_function … prf)232 qed.233 234 124 (* bevals hold a function pointer (BVptr) *) 235 definition funct_of_bevals : ∀F,g lobals,ge.236 beval → beval → option (Σi.is_function F g lobals ge i) ≝237 λF,g lobals,ge,dpl,dph.125 definition funct_of_bevals : ∀F,ge. 126 beval → beval → option (Σi.is_function F ge i) ≝ 127 λF,ge,dpl,dph. 238 128 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; 239 129 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *) 240 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then 130 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then (* ← already checked in funct_of_block? *) 241 131 funct_of_block … (pblock ptr) 242 132 else None ?. 243 244 definition block_of_funct_ident ≝ λF,globals,ge.245 λi : Σi.is_function F globals ge i.246 match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with247 [ Some bl ⇒ λ_.bl248  None ⇒ λprf.⊥249 ] (pi2 … i).250 cases prf #fd normalize #ABS destruct(ABS)251 qed.252 133 253 134 axiom ProgramCounterOutOfCode : String. … … 531 412 set_result … p' vs dest st. 532 413 533 lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.534 block_region (block_of_funct_ident F globals ge i) = Code.535 #F #globals #ge * #i * #fd536 whd in ⊢ (?→??(?%)?);537 cases (find_symbol ???)538 [ #ABS normalize in ABS; destruct(ABS) ]539 #bl normalize nodelta >m_return_bind540 whd in ⊢ (??%?→?); cases (block_region bl)541 [ #ABS normalize in ABS; destruct(ABS) ]542 #_ %543 qed.544 545 414 definition eval_internal_call_pc ≝ 546 415 λp : sem_params.λglobals : list ident.λge : genv p globals.λi. 547 416 let fn ≝ if_of_function … ge i in 548 417 let l' ≝ joint_if_entry ?? fn in 549 mk_program_counter (block_of_funct _ident… ge (pi1 … i)) (offset_of_point ? p … l').418 mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l'). 550 419 [ @block_of_funct_ident_is_code 551 420  cases i /2 by internal_function_is_function/ … … 625 494  _ ⇒ return st 626 495 ]. 627 [ @find_symbol_exists 496 [ @hide_prf 497 @find_symbol_in_globals 628 498 lapply prf 629 499 elim globals [*]
Note: See TracChangeset
for help on using the changeset viewer.