Changeset 2473 for src/joint/semantics.ma
 Timestamp:
 Nov 16, 2012, 6:59:24 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semantics.ma
r2470 r2473 5 5 include "joint/Joint.ma". 6 6 include "ASM/I8051bis.ma". 7 include "common/extraGlobalenvs.ma". 7 8 8 9 (* CSC: external functions never fail (??) and always return something of the … … 11 12 only the head is kept (or Undef if the list is empty) ??? *) 12 13 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 bl23 return λx.(∃fd.x = ?) → ?24 with25 [ Some fd ⇒ λ_.fd26  None ⇒ λprf.⊥27 ] (pi2 … i).28 cases prf #fd #ABS destruct29 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 #EQ39 #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ40 %{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 bl52 return λx.(∃fn.x = ?) → ?53 with54 [ Some fd ⇒55 match fd return λx.(∃fn.Some ? x = ?) → ? with56 [ Internal fn ⇒ λ_.fn57  External _ ⇒ λprf.⊥58 ]59  None ⇒ λprf.⊥60 ] (pi2 … i).61 cases prf #fn #ABS destruct62 qed.63 64 14 (* Paolo: I'll put in this record the property about genv we need *) 65 15 record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝ 66 16 { ge :> genv_t (fundef (F globals)) 67 ; find_symbol_ exists : ∀id.In ? globals id → find_symbol … ge id≠ None ?68 ; stack_sizes : (Σi.is_internal_function F globalsge i) → ℕ17 ; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ? 18 ; stack_sizes : (Σi.is_internal_function ? ge i) → ℕ 69 19 }. 20 21 definition stack_sizes_lift : 22 ∀pars_in, pars_out : params. 23 ∀trans : ∀globals.joint_closed_internal_function pars_in globals → 24 joint_closed_internal_function pars_out globals. 25 ∀prog_in : program (joint_function pars_in) ℕ. 26 let prog_out ≝ 27 transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in 28 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) → 29 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝ 30 λpars_in,pars_out,prog_in,trans,stack_sizes. 31 λi.stack_sizes «i, if_propagate … (pi2 … i)». 70 32 71 33 definition genv ≝ λp.genv_gen (joint_closed_internal_function p). … … 160 122 *) 161 123 162 definition funct_of_ident : ∀F,globals,ge.163 ident → option (Σi.is_function F globals ge i)164 ≝ λF,globals,ge,i.165 match ?166 return λx.! bl ← find_symbol … ge i ;167 find_funct_ptr … ge bl = x → ?168 with169 [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»170  None ⇒ λ_.None ?171 ] (refl …).172 173 lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A.174 ∀Q : option A → Prop.175 ∀c1 : ∀a.Q (Some ? a) → B.176 ∀c2 : Q (None ?) → B.177 ∀P : B → Prop.178 (∀a,prf.P (c1 a prf)) →179 (∀prf.P (c2 prf)) →180 ∀prf : Q m.181 P (match m return λx.Q x → ? with182 [ Some a ⇒ λprf.c1 a prf183  None ⇒ λprf.c2 prf184 ] prf).185 #A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf186 normalize [@H1  @H2]187 qed.188 189 lemma symbol_of_function_block_ok :190 ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).191 #F #ge #b #FFP192 whd in ⊢ (???(??%));193 @match_opt_prf_elim [//] #H @⊥194 (* cut and paste from global env *)195 whd in H:(??%?);196 cases b in FFP H ⊢ %; * * b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP  *: * #H cases (H (refl ??)) ]197 cases (functions_inv … ge b FFP)198 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))199 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))200 cases (find ????)201 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ *  * #H' cases (H' (refl ??)) ]202  * #id' #b' #_ normalize #_ #E destruct203 ] qed.204 205 definition funct_of_block : ∀F,globals,ge.206 block → option (Σi.is_function F globals ge i) ≝207 λF,globals,ge,bl.208 match find_funct_ptr … ge bl209 return λx.find_funct_ptr … ge bl = x → ? with210 [ Some fd ⇒ λprf.return mk_Sig211 ident (λi.is_function F globals ge i)212 (symbol_of_function_block … ge bl ?)213 (ex_intro … fd ?)214  None ⇒ λ_.None ?215 ] (refl …).216 [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf217  >prf % #ABS destruct(ABS)218 ]219 qed.220 221 definition int_funct_of_block : ∀F,globals,ge.222 block → option (Σi.is_internal_function F globals ge i) ≝223 λF,globals,ge,bl.224 ! f ← funct_of_block … ge bl ;225 match ?226 return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)227 with228 [ Internal fn ⇒ λprf.return «pi1 … f, ?»229  External fn ⇒ λ_.None ?230 ] (refl …).231 @(description_of_internal_function … prf)232 qed.233 234 124 (* bevals hold a function pointer (BVptr) *) 235 definition funct_of_bevals : ∀F,g lobals,ge.236 beval → beval → option (Σi.is_function F g lobals ge i) ≝237 λF,g lobals,ge,dpl,dph.125 definition funct_of_bevals : ∀F,ge. 126 beval → beval → option (Σi.is_function F ge i) ≝ 127 λF,ge,dpl,dph. 238 128 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; 239 129 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *) 240 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then 130 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then (* ← already checked in funct_of_block? *) 241 131 funct_of_block … (pblock ptr) 242 132 else None ?. 243 244 definition block_of_funct_ident ≝ λF,globals,ge.245 λi : Σi.is_function F globals ge i.246 match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with247 [ Some bl ⇒ λ_.bl248  None ⇒ λprf.⊥249 ] (pi2 … i).250 cases prf #fd normalize #ABS destruct(ABS)251 qed.252 133 253 134 axiom ProgramCounterOutOfCode : String. … … 531 412 set_result … p' vs dest st. 532 413 533 lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.534 block_region (block_of_funct_ident F globals ge i) = Code.535 #F #globals #ge * #i * #fd536 whd in ⊢ (?→??(?%)?);537 cases (find_symbol ???)538 [ #ABS normalize in ABS; destruct(ABS) ]539 #bl normalize nodelta >m_return_bind540 whd in ⊢ (??%?→?); cases (block_region bl)541 [ #ABS normalize in ABS; destruct(ABS) ]542 #_ %543 qed.544 545 414 definition eval_internal_call_pc ≝ 546 415 λp : sem_params.λglobals : list ident.λge : genv p globals.λi. 547 416 let fn ≝ if_of_function … ge i in 548 417 let l' ≝ joint_if_entry ?? fn in 549 mk_program_counter (block_of_funct _ident… ge (pi1 … i)) (offset_of_point ? p … l').418 mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l'). 550 419 [ @block_of_funct_ident_is_code 551 420  cases i /2 by internal_function_is_function/ … … 625 494  _ ⇒ return st 626 495 ]. 627 [ @find_symbol_exists 496 [ @hide_prf 497 @find_symbol_in_globals 628 498 lapply prf 629 499 elim globals [*]
Note: See TracChangeset
for help on using the changeset viewer.