Ignore:
Timestamp:
Nov 16, 2012, 6:59:24 PM (7 years ago)
Author:
tranquil
Message:

put some generic stuff we need in the back end in extraGlobalenvs (with some axioms that are
in the commented section of Globalenvs)
linearise now has a full spec

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2470 r2473  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
     7include "common/extraGlobalenvs.ma".
    78
    89(* CSC: external functions never fail (??) and always return something of the
     
    1112   only the head is kept (or Undef if the list is empty) ??? *)
    1213
    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 
    6414(* Paolo: I'll put in this record the property about genv we need *)
    6515record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
    6616{ 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 globals ge i) → ℕ
     17; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
     18; stack_sizes : (Σi.is_internal_function ? ge i) → ℕ
    6919}.
     20
     21definition 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) ℕ.
     26let 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)».
    7032
    7133definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
     
    160122*)
    161123
    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 with
    169 [ 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 → ? with
    182    [ Some a ⇒ λprf.c1 a prf
    183    | None ⇒ λprf.c2 prf
    184    ] prf).
    185 #A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf
    186 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 #FFP
    192 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 destruct
    203 ] 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 bl
    209    return λx.find_funct_ptr … ge bl = x → ? with
    210    [ Some fd ⇒ λprf.return mk_Sig
    211         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 ?)) @prf
    217 | >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   with
    228   [ Internal fn ⇒ λprf.return «pi1 … f, ?»
    229   | External fn ⇒ λ_.None ?
    230   ] (refl …).
    231 @(description_of_internal_function … prf)
    232 qed.
    233 
    234124(* bevals hold a function pointer (BVptr) *)
    235 definition funct_of_bevals : ∀F,globals,ge.
    236   beval → beval → option (Σi.is_function F globals ge i) ≝
    237 λF,globals,ge,dpl,dph.
     125definition funct_of_bevals : ∀F,ge.
     126  beval → beval → option (Σi.is_function F ge i) ≝
     127λF,ge,dpl,dph.
    238128! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
    239129if 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? *)
    241131   funct_of_block … (pblock ptr)
    242132else 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; ? = ?) → ? with
    247   [ Some bl ⇒ λ_.bl
    248   | None ⇒ λprf.⊥
    249   ] (pi2 … i).
    250 cases prf #fd normalize #ABS destruct(ABS)
    251 qed.
    252133
    253134axiom ProgramCounterOutOfCode : String.
     
    531412      set_result … p' vs dest st.
    532413
    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 * #fd
    536 whd in ⊢ (?→??(?%)?);
    537 cases (find_symbol ???)
    538 [ #ABS normalize in ABS; destruct(ABS) ]
    539 #bl normalize nodelta >m_return_bind
    540 whd in ⊢ (??%?→?); cases (block_region bl)
    541 [ #ABS normalize in ABS; destruct(ABS) ]
    542 #_ %
    543 qed.
    544 
    545414definition eval_internal_call_pc ≝
    546415λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
    547416let fn ≝ if_of_function … ge i in
    548417let l' ≝ joint_if_entry ?? fn in
    549 mk_program_counter (block_of_funct_ident … ge (pi1 … i)) (offset_of_point ? p … l').
     418mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l').
    550419[ @block_of_funct_ident_is_code
    551420| cases i /2 by internal_function_is_function/
     
    625494  | _ ⇒ return st
    626495  ].
    627 [ @find_symbol_exists
     496[ @hide_prf
     497  @find_symbol_in_globals
    628498  lapply prf
    629499  elim globals [*]
Note: See TracChangeset for help on using the changeset viewer.