 Timestamp:
 Nov 13, 2012, 11:30:23 AM (9 years ago)
 Location:
 src/joint
 Files:

 3 edited
 1 moved
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r2437 r2457 28 28 params : adds type of code and related properties *) 29 29 30 (* 30 31 inductive possible_flows : Type[0] ≝ 31 32  Labels : list label → possible_flows 32 33  Call : possible_flows. 34 *) 33 35 34 36 inductive argument (T : Type[0]) : Type[0] ≝ … … 82 84 (* other instructions not fitting in the general framework *) 83 85 ; ext_seq : Type[0] 84 (* ; ext_branch : Type[0] 85 ; ext_branch_labels : ext_branch → list label*) 86 ; ext_call : Type[0] 87 ; ext_tailcall : Type[0] 86 ; has_tailcalls : bool 88 87 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) 89 88 ; paramsT : Type[0] … … 143 142 step_seq on _s : joint_seq ?? to joint_step ??. 144 143 145 definition step_flows ≝ λp,globals.λs : joint_step p globals.146 match s with147 [ step_seq s ⇒148 match s with149 [ CALL _ _ _ ⇒ Call150  _ ⇒ Labels … [ ]151 ]152  COND _ l ⇒ Labels … [l]153 ].154 155 144 definition step_labels ≝ 156 145 λp, globals.λs : joint_step p globals. 157 match step_flows …s with158 [ Labels lbls ⇒ lbls159  Call ⇒ []160 146 match s with 147 [ step_seq s ⇒ [ ] 148  COND _ l ⇒ [l] 149 ]. 161 150 162 151 definition step_forall_labels : ∀p.∀globals. … … 173 162  GOTO: label → joint_fin_step p 174 163  RETURN: joint_fin_step p 175  tailcall : ext_tailcall p → joint_fin_step p. 176 177 definition fin_step_flows ≝ λp.λs : joint_fin_step p. 164  TAILCALL : 165 has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p)) → 166 call_args p → joint_fin_step p. 167 168 definition fin_step_labels ≝ λp.λs : joint_fin_step p. 178 169 match s with 179 [ GOTO l ⇒ Labels … [l] 180  tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *) 181  _ ⇒ Labels … [ ] 170 [ GOTO l ⇒ [l] 171  _ ⇒ [ ] 182 172 ]. 183 184 definition fin_step_labels ≝185 λp.λs : joint_fin_step p.186 match fin_step_flows … s with187 [ Labels lbls ⇒ lbls188  Call ⇒ [ ]189 ].190 173 191 174 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 192 175  sequential: joint_step p globals → succ p → joint_statement p globals 193 176  final: joint_fin_step p → joint_statement p globals. 194 195 coercion extension_fin_to_fin_step : ∀p : stmt_params.196 ∀s : ext_tailcall p.joint_fin_step p ≝197 tailcall on _s : ext_tailcall ? to joint_fin_step ?.198 177 199 178 coercion fin_step_to_stmt : ∀p : stmt_params.∀globals. 
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). 
src/joint/semantics.ma
r2443 r2457 11 11 only the head is kept (or Undef if the list is empty) ??? *) 12 12 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 13 64 (* Paolo: I'll put in this record the property about genv we need *) 14 65 record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝ 15 66 { ge :> genv_t (fundef (F globals)) 16 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 69 }. 18 70 … … 102 154 axiom BadProgramCounter : String. 103 155 104 definition function_of_block : 105 ∀pars : params. 106 ∀globals. 107 genv pars globals → 108 block → 109 res (joint_closed_internal_function pars globals) ≝ 110 λpars,globals,ge,b. 111 do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; 112 match def with 113 [ Internal def' ⇒ OK … def' 114  External _ ⇒ Error … [MSG BadProgramCounter]]. 115 116 (* this can replace graph_fetch function and lin_fetch_function *) 117 definition fetch_function: 118 ∀pars : params. 119 ∀globals. 120 genv pars globals → 121 cpointer → 122 res (joint_closed_internal_function pars globals) ≝ 123 λpars,globals,ge,p.function_of_block pars globals ge (pblock p). 124 156 (* 125 157 inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ 126 158  Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for gotolike flow alteration *) … … 133 165  FEnd1 : fin_step_flow p F (Labels [ ]) (* end flow *) 134 166  FEnd2 : fin_step_flow p F Call. (* end flow *) 167 *) 168 169 definition funct_of_ident : ∀F,globals,ge. 170 ident → option (Σi.is_function F globals ge i) 171 ≝ λF,globals,ge,i. 172 match ? 173 return λx.! bl ← find_symbol … ge i ; 174 find_funct_ptr … ge bl = x → ? 175 with 176 [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf» 177  None ⇒ λ_.None ? 178 ] (refl …). 179 180 lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A. 181 ∀Q : option A → Prop. 182 ∀c1 : ∀a.Q (Some ? a) → B. 183 ∀c2 : Q (None ?) → B. 184 ∀P : B → Prop. 185 (∀a,prf.P (c1 a prf)) → 186 (∀prf.P (c2 prf)) → 187 ∀prf : Q m. 188 P (match m return λx.Q x → ? with 189 [ Some a ⇒ λprf.c1 a prf 190  None ⇒ λprf.c2 prf 191 ] prf). 192 #A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf 193 normalize [@H1  @H2] 194 qed. 195 196 lemma symbol_of_function_block_ok : 197 ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf). 198 #F #ge #b #FFP 199 whd in ⊢ (???(??%)); 200 @match_opt_prf_elim [//] #H @⊥ 201 (* cut and paste from global env *) 202 whd in H:(??%?); 203 cases b in FFP H ⊢ %; * * b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP  *: * #H cases (H (refl ??)) ] 204 cases (functions_inv … ge b FFP) 205 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) 206 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) 207 cases (find ????) 208 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ *  * #H' cases (H' (refl ??)) ] 209  * #id' #b' #_ normalize #_ #E destruct 210 ] qed. 211 212 definition funct_of_block : ∀F,globals,ge. 213 block → option (Σi.is_function F globals ge i) ≝ 214 λF,globals,ge,bl. 215 match find_funct_ptr … ge bl 216 return λx.find_funct_ptr … ge bl = x → ? with 217 [ Some fd ⇒ λprf.return mk_Sig 218 ident (λi.is_function F globals ge i) 219 (symbol_of_function_block … ge bl ?) 220 (ex_intro … fd ?) 221  None ⇒ λ_.None ? 222 ] (refl …). 223 [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf 224  >prf % #ABS destruct(ABS) 225 ] 226 qed. 227 228 definition int_funct_of_block : ∀F,globals,ge. 229 block → option (Σi.is_internal_function F globals ge i) ≝ 230 λF,globals,ge,bl. 231 ! f ← funct_of_block … ge bl ; 232 match ? 233 return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) 234 with 235 [ Internal fn ⇒ λprf.return «pi1 … f, ?» 236  External fn ⇒ λ_.None ? 237 ] (refl …). 238 @(description_of_internal_function … prf) 239 qed. 240 241 definition funct_of_bevals : ∀F,globals,ge. 242 beval → beval → option (Σi.is_function F globals ge i) ≝ 243 λF,globals,ge,dpl,dph. 244 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; 245 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ 246 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then 247 funct_of_block … (pblock ptr) 248 else None ?. 249 250 definition block_of_funct_ident ≝ λF,globals,ge. 251 λi : Σi.is_function F globals ge i. 252 match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with 253 [ Some bl ⇒ λ_.bl 254  None ⇒ λprf.⊥ 255 ] (pi2 … i). 256 cases prf #fd normalize #ABS destruct(ABS) 257 qed. 258 259 axiom ProgramCounterOutOfCode : String. 260 axiom PointNotFound : String. 261 axiom LabelNotFound : String. 262 axiom MissingSymbol : String. 263 axiom FailedLoad : String. 264 axiom BadFunction : String. 265 axiom SuccessorNotProvided : String. 266 axiom BadPointer : String. 267 268 (* this can replace graph_fetch function and lin_fetch_function *) 269 definition fetch_function: 270 ∀pars : params. 271 ∀globals. 272 ∀ge : genv pars globals. 273 cpointer → 274 res (Σi.is_internal_function … ge i) ≝ 275 λpars,globals,ge,p. 276 opt_to_res … [MSG BadFunction; MSG BadPointer] 277 (int_funct_of_block … ge (pblock p)). 135 278 136 279 record sem_unserialized_params … … 138 281 (F : list ident → Type[0]) : Type[1] ≝ 139 282 { st_pars :> sem_state_params 283 140 284 ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) 141 285 ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval … … 161 305 ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → 162 306 state st_pars → res (state st_pars) 163 ; fetch_external_args: external_function → state st_pars → 307 ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → 164 308 res (list val) 165 309 ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) … … 170 314 ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) 171 315 (* change of pc must be left to *_flow execution *) 172 ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars → 173 F globals → state st_pars → IO io_out io_in (state st_pars) 174 ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars → 175 F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars)) 176 ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars → 177 state st_pars → IO io_out io_in ident 178 ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars) 179 (* do something more in some op2 calculations (e.g. mark a register for correction 180 with spilled_no in ERTL) *) 181 ; post_op2 : ∀globals.genv_gen F globals → 182 Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars → 183 state st_pars → state st_pars 316 ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars → 317 (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars) 318 ; pop_frame: ∀globals.∀ge : genv_gen F globals. 319 (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) 184 320 }. 185 321 … … 220 356 return set_regs ? r st. 221 357 222 axiom BadPointer : String.223 224 (* this is preamble to all calls (including tail ones). The optional argument in225 input tells the function whether it has to save the frame for internal226 calls.227 the first element of the triple is the entry point of the function if228 it is an internal one, or false in case of an external one.229 The actual update of the pc is left to later, as it depends on230 serialization and on whether the call is a tail one. *)231 definition eval_call_block:232 ∀p,F.∀p':sem_unserialized_params p F.∀globals.233 genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →234 IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝235 λp,F,p',globals,ge,st,b,args,dest.236 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);237 match fd with238 [ Internal fd ⇒239 return 〈Init ?? (block_id b) fd args dest, st〉240  External fn ⇒241 ! params ← fetch_external_args … p' fn st : IO ???;242 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;243 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));244 (* CSC: XXX bug here; I think I should split it into Bytelong245 components; instead I am making a singleton out of it. To be246 fixed once we fully implement external functions. *)247 let vs ≝ [mk_val ? evres] in248 ! st ← set_result … p' vs dest st : IO ???;249 return 〈Proceed ???, st〉250 ].251 252 358 axiom FailedStore: String. 253 359 … … 355 461 qed. 356 462 357 axiom ProgramCounterOutOfCode : String.358 axiom PointNotFound : String.359 axiom LabelNotFound : String.360 361 463 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 362 genv p globals →cpointer →363 res (( joint_closed_internal_function p globals) × (joint_statement p globals)) ≝464 ∀ge:genv p globals. cpointer → 465 res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝ 364 466 λp,msp,globals,ge,ptr. 467 let bl ≝ pblock ptr in 468 ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer] 469 (int_funct_of_block … ge bl) ; 470 let fn ≝ if_of_function … f in 365 471 let pt ≝ point_of_pointer ? msp ptr in 366 ! fn ← fetch_function … ge ptr ;367 472 ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); 368 return 〈f n, stmt〉.369 473 return 〈f, stmt〉. 474 370 475 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 371 476 genv p globals → cpointer → label → res cpointer ≝ 372 477 λp,msp,globals,ge,ptr,lbl. 373 ! fn ← fetch_function … ge ptr ; 478 ! f ← fetch_function … ge ptr ; 479 let fn ≝ if_of_function … ge f in 374 480 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 375 481 (point_of_label … (joint_if_code … fn) lbl) ; … … 435 541 return mk_state_pc … st newpc. 436 542 437 axiom MissingSymbol : String. 438 axiom FailedLoad : String. 439 axiom BadFunction : String. 440 axiom SuccessorNotProvided : String. 441 442 definition block_of_call ≝ λp:sem_params.λglobals. 543 544 definition function_of_call ≝ λp:sem_params.λglobals. 443 545 λge: genv p globals.λst : state p.λf. 444 546 match f with 445 547 [ inl id ⇒ 446 opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol… ge id)548 opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id) 447 549  inr addr ⇒ 448 550 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 449 551 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 450 ! ptr ← pointer_of_bevals [addr_l ; addr_h] ; 451 if eq_bv … (bv_zero …) (offv (poff … ptr)) then 452 return pblock ptr 453 else Error … [MSG BadFunction] 552 opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h) 454 553 ]. 455 554 555 (* Paolo: why external calls do not need args?? *) 556 definition eval_external_call ≝ 557 λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st. 558 ! params ← fetch_external_args … p' fn st args : IO ???; 559 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 560 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 561 (* CSC: XXX bug here; I think I should split it into Bytelong 562 components; instead I am making a singleton out of it. To be 563 fixed once we fully implement external functions. *) 564 let vs ≝ [mk_val ? evres] in 565 set_result … p' vs dest st. 566 567 lemma block_of_funct_ident_is_code : ∀F,globals,ge,i. 568 block_region (block_of_funct_ident F globals ge i) = Code. 569 #F #globals #ge * #i * #fd 570 whd in ⊢ (?→??(?%)?); 571 cases (find_symbol ???) 572 [ #ABS normalize in ABS; destruct(ABS) ] 573 #bl normalize nodelta >m_return_bind 574 whd in ⊢ (??%?→?); cases (block_region bl) 575 [ #ABS normalize in ABS; destruct(ABS) ] 576 #_ % 577 qed. 578 579 definition eval_internal_call_pc ≝ 580 λp : sem_params.λglobals : list ident.λge : genv p globals.λi. 581 let fn ≝ if_of_function … ge i in 582 let l' ≝ joint_if_entry ?? fn in 583 let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in 584 pointer_of_point ? p … pointer_in_fn l'. 585 [ @block_of_funct_ident_is_code 586  cases i /2 by internal_function_is_function/ 587 ] 588 qed. 589 590 definition eval_internal_call_no_pc ≝ 591 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st. 592 let fn ≝ if_of_function … ge i in 593 let stack_size ≝ stack_sizes … ge i in 594 ! st' ← setup_call … stack_size (joint_if_params … fn) args st ; 595 let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in 596 return set_regs p regs st. 597 456 598 definition eval_seq_no_pc : 457 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals→458 state p → ∀s:joint_seq p globals.599 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) → 600 state p → cpointer → joint_seq p globals → 459 601 IO io_out io_in (state p) ≝ 460 λp,globals,ge,curr_fn,st, seq.602 λp,globals,ge,curr_fn,st,next,seq. 461 603 match seq return λx.IO ??? with 462 604 [ extension_seq c ⇒ … … 489 631 ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ; 490 632 ! st' ← acca_store … dacc_a v' st; 491 return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')633 return set_carry … carry st' 492 634  CLEAR_CARRY ⇒ 493 635 return set_carry … (BBbit false) st … … 509 651 pair_reg_move … st dst_src 510 652  CALL f args dest ⇒ 511 ! b ← block_of_call … ge st f : IO ???; 512 ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ; 513 return st' 653 ! fn ← function_of_call … ge st f : IO ???; 654 match description_of_function … fn return λx.description_of_function … fn = x → ? with 655 [ Internal fd ⇒ λprf. 656 ! st' ← save_frame … next dest st ; 657 eval_internal_call_no_pc … ge «fn, ?» args st' (* only pc changes *) 658  External fd ⇒ λ_.eval_external_call … fd args dest st 659 ] (refl …) 514 660  _ ⇒ return st 515 661 ]. 516 662 [ @find_symbol_exists 517 663 lapply prf 518 664 elim globals [*] 519 665 #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ] 520 666 #G %2 @IH @G 521 qed. 522 523 definition eval_seq_pc : 524 ∀p:sem_params.∀globals. genv p globals → state p → 525 ∀s:joint_seq p globals. 526 IO io_out io_in (step_flow p ? (step_flows … s)) ≝ 527 λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with 667  @(description_of_internal_function … prf) 668 ] 669 qed. 670 671 definition eval_seq_pc : 672 ∀p:sem_params.∀globals.∀ge:genv p globals. 673 state p → cpointer → joint_seq p globals → 674 res cpointer ≝ 675 λp,globals,ge,st,next,s. 676 match s with 528 677 [ CALL f args dest ⇒ 529 ! b ← block_of_call … ge st f : IO ???; 530 ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ; 531 return flow 532  _ ⇒ return Proceed ??? 678 ! fn ← function_of_call … ge st f; 679 match ? return λx.description_of_function … fn = x → ? with 680 [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?» 681  External _ ⇒ λ_.return next 682 ] (refl …) 683  _ ⇒ return next 533 684 ]. 534 535 definition eval_step : 536 ∀p:sem_params.∀globals. genv p globals → 537 joint_closed_internal_function p globals → state p → 538 ∀s:joint_step p globals. 539 IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝ 540 λp,globals,ge,curr_fn,st,s. 541 match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with 542 [ step_seq s ⇒ 543 ! flow ← eval_seq_pc ?? ge st s ; 544 ! st' ← eval_seq_no_pc ?? ge curr_fn st s ; 545 return 〈flow,st'〉 546  COND src ltrue ⇒ 547 ! v ← acca_retrieve … st src; 548 ! b ← bool_of_beval v; 549 if b then 550 return 〈Redirect ??? ltrue, st〉 551 else 552 return 〈Proceed ???, st〉 685 @(description_of_internal_function … prf) 686 qed. 687 688 definition eval_statement : 689 ∀p:sem_params.∀globals.∀ge:genv p globals. 690 (Σi.is_internal_function … ge i) → state_pc p → 691 ∀s:joint_statement p globals. 692 IO io_out io_in (state_pc p) ≝ 693 λp,g,ge,curr_fn,st,s. 694 match s with 695 [ sequential s next ⇒ 696 ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ; 697 match s return λ_.IO ??? with 698 [ step_seq s ⇒ 699 ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ; 700 ! pc' ← eval_seq_pc … ge st next_ptr s ; 701 return mk_state_pc … st' pc' 702  COND a l ⇒ 703 ! v ← acca_retrieve … st a ; 704 ! b ← bool_of_beval … v ; 705 ! pc' ← 706 if b then 707 pointer_of_label ? p … ge (pc … st) l 708 else 709 succ_pc ? p (pc … st) next ; 710 return mk_state_pc … st pc' 711 ] 712  final s ⇒ 713 match s with 714 [ GOTO l ⇒ 715 ! pc' ← pointer_of_label ? p ? ge (pc … st) l ; 716 return mk_state_pc … st pc' 717  RETURN ⇒ 718 ! st' ← pop_frame … curr_fn st ; 719 ! 〈pc', st''〉 ← fetch_ra … p st' ; 720 return mk_state_pc … st'' pc' 721  TAILCALL _ f args ⇒ 722 ! fn ← function_of_call … ge st f : IO ???; 723 match ? return λx.description_of_function … fn = x → ? with 724 [ Internal _ ⇒ λprf. 725 ! pc' ← eval_internal_call_pc … ge «fn, ?» ; 726 return mk_state_pc … st pc' 727  External fd ⇒ λ_. 728 let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in 729 ! st' ← eval_external_call ??? fd args curr_dest st ; 730 ! st'' ← pop_frame … curr_fn st ; 731 ! 〈pc', st'''〉 ← fetch_ra … p st'' ; 732 return mk_state_pc … st''' pc' 733 ] (refl …) 734 ] 553 735 ]. 554 %1 % qed. 555 556 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals → 557 (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p. 558 IO io_out io_in (state p) ≝ 559 λp,globals,ge,curr_fn,st,s. 560 match s return λx.IO ??? with 561 [ tailcall c ⇒ 562 !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ; 563 return st' 564  _ ⇒ return st 565 ]. 566 567 definition eval_fin_step_pc : 568 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p → 569 ∀s:joint_fin_step p. 570 IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝ 571 λp,g,ge,curr_fn,st,s. 572 match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with 573 [ tailcall c ⇒ 574 !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ; 575 return flow 576  GOTO l ⇒ return FRedirect … l 577  RETURN ⇒ return FEnd1 ?? 578 ]. %1 % qed. 579 580 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals → 581 state p → Z → joint_closed_internal_function p globals → call_args p → 582 res (state_pc p) ≝ 583 λp,globals,ge,st,id,fn,args. 584 ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) 585 args st ; 586 let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in 587 let l' ≝ joint_if_entry … fn in 588 let st' ≝ set_regs p regs st in 589 let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in 590 ! pc ← pointer_of_point ? p … pointer_in_fn l' ; 591 return mk_state_pc ? st' pc. % qed. 592 593 (* The pointer provided is the one to the *next* instruction. *) 594 definition eval_step_flow : 595 ∀p:sem_params.∀globals.∀flows.genv p globals → 596 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝ 597 λp,globals,flows,ge,st,nxt,cmd. 598 match cmd with 599 [ Redirect _ l ⇒ 600 goto … ge l st nxt 601  Init id fn args dest ⇒ 602 ! st' ← save_frame … nxt dest st ; 603 do_call ?? ge st' id fn args 604  Proceed _ ⇒ 605 return mk_state_pc ? st nxt 606 ]. 607 608 definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals → 609 state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝ 610 λp,globals,lbls,ge,st,curr,cmd. 611 match cmd with 612 [ FRedirect _ l ⇒ goto … ge l st curr 613  FTailInit id fn args ⇒ 614 do_call … ge st id fn args 615  _ ⇒ 616 ! 〈ra, st'〉 ← fetch_ra … st ; 617 ! fn ← fetch_function … ge curr ; 618 ! st'' ← pop_frame … ge fn st'; 619 return mk_state_pc ? st'' ra 620 ]. 621 622 definition eval_statement : 623 ∀globals.∀p:sem_params.genv p globals → 624 state_pc p → joint_closed_internal_function p globals → joint_statement p globals → 625 IO io_out io_in (state_pc p) ≝ 626 λglobals,p,ge,st,curr_fn,stmt. 627 match stmt with 628 [ sequential s nxt ⇒ 629 ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ; 630 ! nxtptr ← succ_pc ? p (pc … st) nxt ; 631 eval_step_flow … ge st' nxtptr flow 632  final s ⇒ 633 ! st' ← eval_fin_step_no_pc … ge curr_fn st s ; 634 ! flow ← eval_fin_step_pc … ge curr_fn st s ; 635 eval_fin_step_flow … ge st' (pc … st) flow 636 ]. 736 @(description_of_internal_function … prf) 737 qed. 637 738 638 739 definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals → … … 640 741 λglobals,p,ge,st. 641 742 ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???; 642 eval_statement … ge st fns.743 eval_statement … ge fn st s. 643 744 644 745 (* Paolo: what if in an intermediate language main finishes with an external … … 648 749 genv p globals → cpointer → state_pc p → option int ≝ 649 750 λglobals,p,ge,exit,st.res_to_opt ? ( 650 do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st); 751 do 〈f,s〉 ← fetch_statement ? p … ge (pc … st); 752 let fn ≝ if_of_function … f in 651 753 match s with 652 754 [ final s' ⇒
Note: See TracChangeset
for help on using the changeset viewer.