Changeset 2457 for src/joint/Traces.ma
 Timestamp:
 Nov 13, 2012, 11:30:23 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2443 r2457 9 9 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) 10 10 }. 11 11 12 axiom is_internal_function_of_program : 13 ∀p:params.joint_program p → ident → Prop. 14 15 axiom 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 12 19 record prog_params : Type[1] ≝ 13 20 { prog_spars : sem_params 14 21 ; prog : joint_program prog_spars 22 ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ 15 23 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 16 24 }. … … 27 35 (prog_spars pars) 28 36 «ptr, refl …» 29 (mk_genv_gen ?? (globalenv_noinit ? p) ? )37 (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»)) 30 38 (* (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 ] 33 43 qed. 34 44 … … 36 46 ≝ make_global on _p : prog_params to evaluation_params. 37 47 38 39 axiom ExternalMain : String. 48 axiom BadMain : String. 40 49 41 50 definition make_initial_state : … … 56 65 ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ; 57 66 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 …). 65 76 [ % 77  @(description_of_internal_function … prf) 66 78  cases spb normalize // 67 79 ] 68 80 qed. 69 81 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 ] 82 definition 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 89 114 ]. 90 115 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 ]. 116 lemma 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 124 whd in match joint_classify; normalize nodelta 125 lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st))) 126 elim (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) ] 148 normalize nodelta #_ 149 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/ 150 qed. 151 152 definition joint_call_ident : ∀p:evaluation_params. 153 (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝ 154 λp,st. 155 match ? 156 return λ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 175 elim (joint_classify_call … (pi2 … st)) 176 #f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3 177 lapply ABS ABS 178 >EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS) 179 qed. 108 180 109 181 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?. … … 150 222 (* as_pc ≝ *) cpointerDeq 151 223 (* 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) 167 225 (* as_label_of_pc ≝ *) 168 226 (λpc. … … 177 235 succ_pc p p (pc … s1) nxt = return pc … s2) 178 236 (* 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.