Changeset 2529 for src/joint/Traces.ma


Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2484 r2529  
    1515 { prog_spars : sem_params
    1616 ; prog : joint_program prog_spars
    17  ; stack_sizes : (Σi.is_internal_function_of_program … prog i) →
     17 ; stack_sizes : ident → option
    1818(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1919 }.
     
    7878  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    7979  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
    80   let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
     80  let spp : xpointer ≝
     81    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
     82     pi2 … spb» in
    8183(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8284  let main ≝ prog_main … p in
     
    8688  ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ;
    8789  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    88   ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
    89   match ? return λx.description_of_function … main = x → ? with
    90   [ Internal fn ⇒ λprf.
    91     let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in
    92     ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
    93     let pc' ≝ eval_internal_call_pc … ge main in
     90  ! bl ← block_of_call … ge st_pc0 (inl … main) ;
     91  ! 〈i, fn〉 ← fetch_function … ge bl ;
     92  match fn with
     93  [ Internal ifn ⇒
     94    ! st' ← eval_internal_call_no_pc … ge i ifn (call_args_for_main … pars) st_pc0 ;
     95    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    9496    return mk_state_pc … st' pc'
    95   | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    96   ] (refl …).
    97   [ @(description_of_internal_function … prf)
    98   | cases spb normalize //
    99   ]
    100 qed.
     97  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
     98  ].
    10199
    102100definition joint_classify_seq :
     
    105103  match stmt with
    106104  [ CALL f args dest ⇒
    107     match function_of_call ?? (ev_genv p) st f with
    108     [ OK fn ⇒
    109       match description_of_function … fn with
     105    match (! bl ← block_of_call … (ev_genv p) st f ;
     106            fetch_function … (ev_genv p) bl) with
     107    [ OK id_fn ⇒
     108      match \snd id_fn with
    110109      [ Internal _ ⇒ cl_call
    111110      | External _ ⇒ cl_other
     
    136135  ∀p : evaluation_params.state_pc p → status_class ≝
    137136  λp,st.
    138   match fetch_statement ? p … (ev_genv p) (pc … st) with
    139   [ OK f_s ⇒
    140     match \snd f_s with
     137  match fetch_statement … (ev_genv p) (pc … st) with
     138  [ OK i_f_s ⇒
     139    match \snd i_f_s with
    141140    [ sequential s _ ⇒ joint_classify_step p st s
    142141    | final s ⇒ joint_classify_final p s
     
    145144  ].
    146145
     146definition no_call : ∀p,g.joint_seq p g → Prop ≝
     147  λp,g,s.match s with
     148  [ CALL _ _ _ ⇒ False
     149  | _ ⇒ True
     150  ].
     151
     152definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
     153  λp,g,s.match s with
     154  [ COST_LABEL _ ⇒ False
     155  | _ ⇒ True
     156  ].
     157
     158lemma no_call_advance : ∀p : evaluation_params.
     159∀s,nxt.∀st : state_pc p.
     160no_call p (globals p) s →
     161eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
     162#p * // #f #args #dest #nxt #st *
     163qed.
     164
     165lemma no_call_other : ∀p : evaluation_params.∀st,s.
     166no_call p (globals p) s →
     167joint_classify_seq … st s = cl_other.
     168#p #st * // #f #args #dest *
     169qed.
     170
     171lemma cond_call_other :
     172  ∀p,globals.∀P : joint_step p globals → Prop.
     173  (∀a,lbltrue.P (COND … a lbltrue)) →
     174  (∀f,args,dest.P (CALL … f args dest)) →
     175  (∀s.no_call ?? s → P s) →
     176  ∀s.P s.
     177#p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
     178
    147179lemma joint_classify_call : ∀p : evaluation_params.∀st.
    148180  joint_classify p st = cl_call →
    149   ∃f,f',args,dest,next,fn,fd.
    150   fetch_statement ? p … (ev_genv p) (pc … st) =
    151     OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
    152   function_of_call … (ev_genv p) st f' = OK ? fn
    153   description_of_function … (ev_genv p) fn = Internal … fd.
     181  ∃i_f,f',args,dest,next,bl,i',fd'.
     182  fetch_statement … (ev_genv p) (pc … st) =
     183    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
     184  block_of_call … (ev_genv p) st f' = OK ? bl
     185  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
    154186#p #st
    155187whd in match joint_classify; normalize nodelta
    156 inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta
    157 [ * #f * [| * [ #lbl || #b #f #args ]]
    158   [ * [| #a #lbl #next ]
    159     [ *
    160       [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
    161       | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
    162       | #ext ] #next
    163       [ whd in match joint_classify_step; whd in match joint_classify_seq;
    164         normalize nodelta
    165         inversion (function_of_call ?????) normalize nodelta
    166         [ #fn
    167           inversion (description_of_function ?? fn) #fd
    168           #EQfd
    169         | #e
    170         ] #EQfn
    171       ]
     188inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta
     189[2: #e #_ #ABS destruct(ABS) ]
     190* #i_f * [2: * [ #lbl | | #fl #f #args ] #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     191@cond_call_other
     192[ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
     193|3: #s #no_call #nxt #_ whd in match joint_classify_step;
     194  normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS)
     195]
     196#f' #args #dest #nxt #fetch
     197whd in match joint_classify_step; whd in match joint_classify_seq;
     198normalize nodelta
     199inversion (block_of_call ?????)
     200[ #bl #block_of_c  >m_return_bind
     201  inversion (fetch_function ???)
     202  [ * #i' *
     203    [ #fd' #fetch' #_
     204      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
     205      % [ %{block_of_c} % ]
     206      whd in match fetch_internal_function; normalize nodelta
     207      >fetch' %
    172208    ]
    173209  ]
    174 | #e
    175 ] #EQfetch
    176 [|*: #ABS normalize in ABS; destruct(ABS) ]
    177 normalize nodelta #_
    178 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd}
    179 %{EQfd} %{EQfn} %
     210]
     211#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
    180212qed.
    181213
     
    183215  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
    184216λp,s1,s2.
    185 match fetch_statement ? p … (ev_genv p) (pc … s1) with
     217match fetch_statement … (ev_genv p) (pc … s1) with
    186218[ OK x ⇒
    187219  match \snd x with
    188220  [ sequential s next ⇒
    189     pc … s2 = succ_pc p p (pc … s1) next
     221    pc … s2 = succ_pc p (pc … s1) next
    190222  | _ ⇒ False (* never happens *)
    191223  ]
     
    225257   I think handling of the function is easier *)
    226258λp,st.
    227 let dummy : ident ≝ an_identifier ? one in
    228 match fetch_statement ? p … (ev_genv p) (pc … st) with
     259let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
     260match fetch_statement … (ev_genv p) (pc … st) with
    229261[ OK x ⇒
    230262  match \snd x with
     
    234266      match s with
    235267      [ CALL f' args dest ⇒
    236         match function_of_call … (ev_genv p) st f' with
    237         [ OK f ⇒ f
     268        match
     269          (! bl ← block_of_call … (ev_genv p) st f' ;
     270           fetch_internal_function … (ev_genv p) bl) with
     271        [ OK i_f ⇒ \fst i_f
    238272        | _ ⇒ dummy
    239273        ]
     
    279313  | _ ⇒ None ?
    280314  ].
     315
     316
     317lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
     318no_cost_label p (globals p) s →
     319cost_label_of_stmt … (sequential … s nxt) = None ?.
     320#p * // #lbl #next *
     321qed.
    281322
    282323definition joint_abstract_status :
     
    293334   (* as_label_of_pc ≝ *)
    294335    (λpc.
    295       match fetch_statement ? p … (ev_genv p) pc with
     336      match fetch_statement … (ev_genv p) pc with
    296337      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    297338      | _ ⇒ None ?
     
    300341   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    301342   (* as_call_ident ≝ *) (joint_call_ident p).
     343
Note: See TracChangeset for help on using the changeset viewer.