Changeset 2457 for src/joint/Traces.ma


Ignore:
Timestamp:
Nov 13, 2012, 11:30:23 AM (8 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

    r2443 r2457  
    99(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    11  
     11
     12axiom is_internal_function_of_program :
     13  ∀p:params.joint_program p → ident → Prop.
     14
     15axiom is_internal_function_of_program_ok :
     16  ∀p.∀prog:joint_program p.∀i.is_internal_function ?? (globalenv_noinit ? prog) i →
     17  is_internal_function_of_program p prog i.
     18
    1219record prog_params : Type[1] ≝
    1320 { prog_spars : sem_params
    1421 ; prog : joint_program prog_spars
     22 ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ
    1523(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1624 }.
     
    2735  (prog_spars pars)
    2836  «ptr, refl …»
    29   (mk_genv_gen ?? (globalenv_noinit ? p) ?)
     37  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
    3038 (* (prog_io pars) *).
    31 (* TODO or TOBEFOUND *)
    32 cases daemon
     39[ @is_internal_function_of_program_ok @(pi2 … i)
     40| (* TODO or TOBEFOUND *)
     41  cases daemon
     42]
    3343qed.
    3444
     
    3646≝ make_global on _p : prog_params to evaluation_params.
    3747
    38 
    39 axiom ExternalMain : String.
     48axiom BadMain : String.
    4049
    4150definition make_initial_state :
     
    5665  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
    5766  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    58   ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
    59   ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
    60   match main_fd with
    61   [ Internal fn ⇒
    62     do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
    63   | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    64   ].
     67  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
     68  match ? return λx.description_of_function … main = x → ? with
     69  [ Internal fn ⇒ λprf.
     70    let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
     71    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
     72    ! pc' ← eval_internal_call_pc … ge main ;
     73    return mk_state_pc … st' pc'
     74  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
     75  ] (refl …).
    6576  [ %
     77  | @(description_of_internal_function … prf)
    6678  | cases spb normalize //
    6779  ]
    6880qed.
    6981
    70 definition step_flow_classifier :
    71   ∀p : evaluation_params.∀F,flows.
    72   step_flow p F flows → status_class ≝
    73   λp,F,flows,flow.match flow with
    74   [ Redirect _ _ ⇒ cl_jump
    75   | Init bl _ _ _ ⇒
    76     match symbol_for_block … (ev_genv p) (mk_block Code bl) with
    77     [ Some f ⇒ cl_call
    78     | None ⇒ cl_other (* we don't care, as call will fail anyway *)
    79     ]
    80   | Proceed flows ⇒
    81     match flows with
    82     [ Labels lbls ⇒
    83       match lbls with
    84       [ nil ⇒ cl_other
    85       | _ ⇒ cl_jump
    86       ]
    87     | _ ⇒ cl_other
    88     ]
     82definition joint_classify :
     83  ∀p : evaluation_params.state_pc p → status_class ≝
     84  λp,st.
     85  match fetch_statement ? p … (ev_genv p) (pc … st) with
     86  [ OK f_s ⇒
     87    let 〈f, s〉 ≝ f_s in
     88    match s with
     89    [ sequential s _ ⇒
     90      match s with
     91      [ step_seq s ⇒
     92        match s with
     93        [ CALL f' args dest ⇒
     94          match function_of_call ?? (ev_genv p) st f' with
     95          [ OK fn ⇒
     96            match description_of_function … fn with
     97            [ Internal _ ⇒ cl_call
     98            | External _ ⇒ cl_other
     99            ]
     100          | Error _ ⇒ cl_other
     101          ]
     102        | _ ⇒ cl_other
     103        ]
     104      | COND _ _ ⇒ cl_jump
     105      ]
     106    | final s ⇒
     107      match s with
     108      [ GOTO _ ⇒ cl_other
     109      | RETURN ⇒ cl_return
     110      | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
     111      ]
     112    ]
     113  | Error _ ⇒ cl_other
    89114  ].
    90115
    91 definition fin_step_flow_classifier :
    92   ∀p : evaluation_params.∀F,flows.
    93   fin_step_flow p F flows → status_class ≝
    94   λp,F,flows,flow.match flow with
    95   [ FRedirect lbls _ ⇒
    96     match lbls with
    97     [ nil ⇒ (* not really possible, we don't care *) cl_other
    98     | cons _ tl ⇒
    99       match tl with
    100       [ nil ⇒ (* only one label *) cl_other
    101       | _ ⇒ (* fork *) cl_jump
    102       ]
    103     ]
    104   | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
    105     cl_other
    106   | _ ⇒ cl_return
    107   ].
     116lemma joint_classify_call : ∀p : evaluation_params.∀st.
     117  joint_classify p st = cl_call →
     118  ∃f,f',args,dest,next,fn,fd.
     119  fetch_statement ? p … (ev_genv p) (pc … st) =
     120    OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
     121  function_of_call … (ev_genv p) st f' = OK ? fn ∧
     122  description_of_function … (ev_genv p) fn = Internal … fd.
     123#p #st
     124whd in match joint_classify; normalize nodelta
     125lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
     126elim (fetch_statement ?????) in ⊢ (???%→%);
     127[ * #f * [| * [ #lbl || #b #f #args ]]
     128  [ * [| #a #lbl #next ]
     129    [ *
     130      [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
     131      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
     132      | #ext ] #next
     133      [ normalize nodelta
     134        lapply (refl … (function_of_call … (ev_genv p) st f'))
     135        elim (function_of_call ?????) in ⊢ (???%→%);
     136        [ #fn normalize nodelta
     137          lapply (refl … (description_of_function … (ev_genv p) fn))
     138          elim (description_of_function ????) in ⊢ (???%→%); #fd
     139          #EQfd
     140        | #e
     141        ] #EQfn
     142      ]
     143    ]
     144  ]
     145| #e
     146] #EQfetch
     147[|*: #ABS normalize in ABS; destruct(ABS) ]
     148normalize nodelta #_
     149%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
     150qed.
     151
     152definition joint_call_ident : ∀p:evaluation_params.
     153  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     154λp,st.
     155match ?
     156return λx.
     157  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
     158  match s with
     159  [ sequential s next ⇒
     160    match s with
     161    [ step_seq s ⇒
     162      match s with
     163      [ CALL f' args dest ⇒
     164        function_of_call … (ev_genv p) st f'
     165      | _ ⇒ Error … [ ]
     166      ]
     167    | _ ⇒ Error … [ ]
     168    ]
     169  | _ ⇒ Error … [ ]
     170  ] = x → ? with
     171[ OK v ⇒ λ_.v
     172| Error e ⇒ λABS.⊥
     173] (refl …).
     174@hide_prf
     175elim (joint_classify_call … (pi2 … st))
     176#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
     177lapply ABS -ABS
     178>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
     179qed.
    108180
    109181definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
     
    150222   (* as_pc ≝ *) cpointerDeq
    151223   (* as_pc_of ≝ *) (pc …)
    152    (* as_classify ≝ *)
    153     (λs.
    154       match (
    155         ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
    156         match stmt with
    157         [ sequential stp nxt ⇒
    158           ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
    159           return step_flow_classifier … flow
    160         | final stp ⇒
    161           ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
    162           return fin_step_flow_classifier … flow
    163         ]) with
    164       [ Value c ⇒ c
    165       | _ ⇒ cl_other
    166       ])
     224   (* as_classify ≝ *) (joint_classify p)
    167225   (* as_label_of_pc ≝ *)
    168226    (λpc.
     
    177235      succ_pc p p (pc … s1) nxt = return pc … s2)
    178236   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    179    (* as_call_ident_≝ *)
    180    (λst.?). cases daemon (* TODO *) qed.
     237   (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracChangeset for help on using the changeset viewer.