Changeset 2473 for src/joint


Ignore:
Timestamp:
Nov 16, 2012, 6:59:24 PM (7 years ago)
Author:
tranquil
Message:

put some generic stuff we need in the back end in extraGlobalenvs (with some axioms that are
in the commented section of Globalenvs)
linearise now has a full spec

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2470 r2473  
    1111 
    1212
    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 #H2
    22 [ @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 ⊢ (%→%); * #ifn
    36 @(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.
    4013
    4114record prog_params : Type[1] ≝
     
    4518(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    4619 }.
     20
     21lemma 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]
     27qed.
     28
     29lemma 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]
     34qed.
     35
     36lemma 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]
     41qed.
    4742
    4843definition make_global : prog_params → evaluation_params
     
    6055 (* (prog_io pars) *).
    6156[ @(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)|]
    6462]
    6563qed.
     
    9088  match ? return λx.description_of_function … main = x → ? with
    9189  [ Internal fn ⇒ λprf.
    92     let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
     90    let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in
    9391    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
    9492    let pc' ≝ eval_internal_call_pc … ge main in
     
    157155        [ #fn normalize nodelta
    158156          lapply (refl … (description_of_function … (ev_genv p) fn))
    159           elim (description_of_function ????) in ⊢ (???%→%); #fd
     157          elim (description_of_function ?? fn) in ⊢ (???%→%); #fd
    160158          #EQfd
    161159        | #e
     
    171169qed.
    172170
     171definition 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.
     174match 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
    173184definition joint_call_ident : ∀p:evaluation_params.
    174185  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     186(* this is a definition without a dummy ident :
    175187λp,st.
    176188match ?
     
    198210lapply ABS -ABS
    199211>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
    200 qed.
     212qed. *)
     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.
     216let dummy : ident ≝ an_identifier ? one in
     217match 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].
    201237
    202238definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
     
    250286      | _ ⇒ None ?
    251287      ])
    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)
    257289   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    258290   (* as_call_ident ≝ *) (joint_call_ident p).
  • src/joint/linearise.ma

    r2440 r2473  
    11include "joint/TranslateUtils.ma".
     2include "common/extraGlobalenvs.ma".
    23include "utilities/hide.ma".
    34
     
    553554qed.
    554555
     556
     557definition 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
    555577definition linearise_code:
    556578 ∀p : unserialized_params.∀globals.
    557579  ∀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       (* ∧
    561585      ∃ sigma : identifier_map LabelTag ℕ.
    562586      lookup … sigma entry = Some ? 0 ∧
     
    570594                (λnext.Or (lookup … sigma next = Some ? (S n))
    571595                (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)*)
    573597
    574598 λp,globals,g,g_prf,entry_sig.
     
    583607      let crev ≝ \snd triple in
    584608      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 *)
    587612| #i >mem_set_empty *
    588613|3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS)
     
    594619| >commutative_plus change with (? ≤ |g|) %
    595620]
    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 ****
    600623#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
    603643  >stmt_at_filter_labels #EQ
    604644  %
     
    628668  ]
    629669]
    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 *)
     670qed.
     671
    651672definition linearise_int_fun :
    652673  ∀p : unserialized_params.
    653674  ∀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
    656680     (* ∃sigma : identifier_map LabelTag ℕ.
    657681        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    669693                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    670694                    (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〉.
     708normalize nodelta
     709cases (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 #_ % ]
    687715]
    688716qed.
     
    690718definition linearise : ∀p : unserialized_params.
    691719  program (joint_function (mk_graph_params p)) ℕ →
    692   program (joint_function (mk_lin_params p)) ℕ ≝
     720  program (joint_function (mk_lin_params p)) ℕ
     721   ≝
    693722  λ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
     726definition 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)
     739qed.
     740
     741lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma.
     742#p #prog
     743letin 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)
     749normalize nodelta
     750cases (linearise_int_fun ???) * #fn_out #sigma_loc
     751normalize nodelta #prf @prf
     752qed.
  • src/joint/semantics.ma

    r2470 r2473  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
     7include "common/extraGlobalenvs.ma".
    78
    89(* CSC: external functions never fail (??) and always return something of the
     
    1112   only the head is kept (or Undef if the list is empty) ??? *)
    1213
    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 bl
    23 return λx.(∃fd.x = ?) → ?
    24 with
    25 [ Some fd ⇒ λ_.fd
    26 | None ⇒ λprf.⊥
    27 ] (pi2 … i).
    28 cases prf #fd #ABS destruct
    29 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 #EQ
    39 #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
    40 %{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 bl
    52 return λx.(∃fn.x = ?) → ?
    53 with
    54 [ Some fd ⇒
    55   match fd return λx.(∃fn.Some ? x = ?) → ? with
    56   [ Internal fn ⇒ λ_.fn
    57   | External _ ⇒ λprf.⊥
    58   ]
    59 | None ⇒ λprf.⊥
    60 ] (pi2 … i).
    61 cases prf #fn #ABS destruct
    62 qed.
    63 
    6414(* Paolo: I'll put in this record the property about genv we need *)
    6515record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
    6616{ 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 globals ge i) → ℕ
     17; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
     18; stack_sizes : (Σi.is_internal_function ? ge i) → ℕ
    6919}.
     20
     21definition 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) ℕ.
     26let 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)».
    7032
    7133definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
     
    160122*)
    161123
    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 with
    169 [ 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 → ? with
    182    [ Some a ⇒ λprf.c1 a prf
    183    | None ⇒ λprf.c2 prf
    184    ] prf).
    185 #A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf
    186 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 #FFP
    192 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 destruct
    203 ] 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 bl
    209    return λx.find_funct_ptr … ge bl = x → ? with
    210    [ Some fd ⇒ λprf.return mk_Sig
    211         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 ?)) @prf
    217 | >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   with
    228   [ Internal fn ⇒ λprf.return «pi1 … f, ?»
    229   | External fn ⇒ λ_.None ?
    230   ] (refl …).
    231 @(description_of_internal_function … prf)
    232 qed.
    233 
    234124(* bevals hold a function pointer (BVptr) *)
    235 definition funct_of_bevals : ∀F,globals,ge.
    236   beval → beval → option (Σi.is_function F globals ge i) ≝
    237 λF,globals,ge,dpl,dph.
     125definition funct_of_bevals : ∀F,ge.
     126  beval → beval → option (Σi.is_function F ge i) ≝
     127λF,ge,dpl,dph.
    238128! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
    239129if 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? *)
    241131   funct_of_block … (pblock ptr)
    242132else 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; ? = ?) → ? with
    247   [ Some bl ⇒ λ_.bl
    248   | None ⇒ λprf.⊥
    249   ] (pi2 … i).
    250 cases prf #fd normalize #ABS destruct(ABS)
    251 qed.
    252133
    253134axiom ProgramCounterOutOfCode : String.
     
    531412      set_result … p' vs dest st.
    532413
    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 * #fd
    536 whd in ⊢ (?→??(?%)?);
    537 cases (find_symbol ???)
    538 [ #ABS normalize in ABS; destruct(ABS) ]
    539 #bl normalize nodelta >m_return_bind
    540 whd in ⊢ (??%?→?); cases (block_region bl)
    541 [ #ABS normalize in ABS; destruct(ABS) ]
    542 #_ %
    543 qed.
    544 
    545414definition eval_internal_call_pc ≝
    546415λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
    547416let fn ≝ if_of_function … ge i in
    548417let l' ≝ joint_if_entry ?? fn in
    549 mk_program_counter (block_of_funct_ident … ge (pi1 … i)) (offset_of_point ? p … l').
     418mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
    550419[ @block_of_funct_ident_is_code
    551420| cases i /2 by internal_function_is_function/
     
    625494  | _ ⇒ return st
    626495  ].
    627 [ @find_symbol_exists
     496[ @hide_prf
     497  @find_symbol_in_globals
    628498  lapply prf
    629499  elim globals [*]
Note: See TracChangeset for help on using the changeset viewer.