Changeset 2473 for src/joint/Traces.ma


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

File:
1 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).
Note: See TracChangeset for help on using the changeset viewer.