Changeset 2952 for src


Ignore:
Timestamp:
Mar 26, 2013, 2:01:15 PM (7 years ago)
Author:
tranquil
Message:
  • corrected all back-end premains to not pass any arguments to the main
  • premain fetching is made by fetch_function in joint_semantics.ma
  • reorganised some definition between Traces.ma and joint_fullexec.ma
Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed

  • src/ERTL/ERTL.ma

    r2946 r2952  
    140140  res in
    141141let res ≝ add_graph … l2
    142   (sequential … (CALL ERTL ? (inl … (prog_main … p)) 4 it) l3)
     142  (sequential … (CALL ERTL ? (inl … (prog_main … p)) 0 it) l3)
    143143  res in
    144144let res ≝ add_graph … l3

  • src/ERTLptr/ERTLptr.ma

    r2946 r2952  
    6868  res in
    6969let res ≝ add_graph … l2
    70   (sequential … (CALL ERTLptr ? (inl … (prog_main … p)) 4 it) l3)
     70  (sequential … (CALL ERTLptr ? (inl … (prog_main … p)) 0 it) l3)
    7171  res in
    7272let res ≝ add_graph … l3

  • src/LIN/LIN.ma

    r2946 r2952  
    3434let code ≝
    3535  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
    36    〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 4 it) it〉 ;
     36   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
    3737   〈Some ? l3, GOTO ? l3〉 ] in
    3838mk_joint_internal_function LIN (prog_var_names … p)

  • src/LTL/LTL.ma

    r2946 r2952  
    4949  res in
    5050let res ≝ add_graph … l2
    51   (sequential … (CALL LTL ? (inl … (prog_main … p)) 4 it) l3)
     51  (sequential … (CALL LTL ? (inl … (prog_main … p)) 0 it) l3)
    5252  res in
    5353let res ≝ add_graph … l3

  • src/RTL/RTL.ma

    r2946 r2952  
    113113  res in
    114114let res ≝ add_graph … l2
    115   (sequential … (CALL RTL ? (inl … (prog_main … p)) (map … (Reg ?) rs) rs) l3)
     115  (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] l3)
    116116  res in
    117117let res ≝ add_graph … l3

  • src/joint/Traces.ma

    r2946 r2952  
    22include "common/StructuredTraces.ma".
    33
    4 record evaluation_params : Type[1] ≝
    5  { globals: list ident
    6  ; sparams:> sem_params
    7  ; ev_genv: genv sparams globals
    8 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    9  }.
     4record evaluation_params (p : sem_params) : Type[0] ≝
     5{ globals : list ident
     6; ev_genv :> genv p globals
     7}.
    108
    119record prog_params : Type[1] ≝
    12  { prog_spars : sem_params
     10 { prog_spars :> sem_params
    1311 ; prog : joint_program prog_spars
    1412 ; stack_sizes : ident → option ℕ
    … …  
    1614 }.
    1715
    18 lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
    19 #A #B #f #P #l elim l -l [*]
    20 #hd #tl #IH *
    21 [ #Phd %1{Phd}
    22 | #Ptl %2{(IH Ptl)}
    23 ]
    24 qed.
    25 
    26 lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
    27 #A #P #l elim l -l [*] #hd #tl #IH *
    28 [ #Phd %{hd} %{Phd} %1 %
    29 | #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
    30 ]
    31 qed.
    32 
    33 lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
    34 #A #P #l elim l -l [ #x *] #hd #tl #IH #x *
    35 [ #EQ >EQ #H %1{H}
    36 | #Intl #Px %2{(IH … Intl Px)}
    37 ]
    38 qed.
    39 
    40 lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
    41 #A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
    42 
    43 lemma lookup_remove_elim : ∀tag,A.∀P : option A → Prop.
    44 ∀m,i,j.
    45 (i = j → P (None ?)) →
    46 (i ≠ j → P (lookup tag A m i)) →
    47 P (lookup tag A (remove tag A m j) i).
    48 #tag #A #P #m #i #j #H1 #H2
    49 @(eq_identifier_elim … i j) #H destruct
    50 [ >lookup_remove_hit @H1 % | >lookup_remove_miss try @H2 assumption ]
    51 qed.
    52 
    53 definition make_global : prog_params → evaluation_params
    54 ≝
    55 λpars.
    56 let p ≝ prog pars in
    57 let spars ≝ prog_spars pars in
    58 let genv ≝ joint_globalenv spars p in
    59 let get_pc_lbl ≝ λid,lbl.
    60   ! bl ← block_of_funct_id … spars genv id ;
    61   pc_of_label … genv bl lbl in
    62 mk_evaluation_params
    63   (prog_var_names … p)
    64   spars
    65   (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl)
    66  (* (prog_io pars) *).
    67 #s #H
    68 elim (find_symbol_exists … (λx.x) … p s ?)
    69 [ #bl #EQ %
    70   whd in match genv; whd in match find_symbol; whd in match drop_fn; normalize nodelta
    71   @lookup_add_elim #H
    72   [2: @lookup_remove_elim [ #EQ >EQ in H; * #ABS cases (ABS ?) % ]
    73     #_ change with (find_symbol ? (globalenv … (λx.x) p) s = ? → ?) >EQ ]
    74   #ABS destruct(ABS) ]
    75 @Exists_append_r
    76 @(Exists_mp … H) //
    77 qed.
    78 
    79 coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
    80 ≝ make_global on _p : prog_params to evaluation_params.
     16definition joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝
     17λp.mk_evaluation_params ?
     18  (prog_var_names … (prog p))
     19  (joint_globalenv p (prog p) (stack_sizes p)).
     20
     21coercion joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝
     22joint_make_global on p : prog_params to evaluation_params ?.
    8123
    8224definition make_initial_state :
    8325 ∀pars: prog_params.state_pc pars ≝
    8426λpars.let p ≝ prog pars in
    85   let sem_globals : evaluation_params ≝ pars in
    86   let ge ≝ ev_genv sem_globals in
     27  let ge ≝ ev_genv pars in
    8728  (* this is going to change shortly: globals will not reside in globalenv anymore *)
    8829  let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
    … …  
    9738(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    9839  let main ≝ prog_main … p in
    99   let st ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m globals_size in
    100   mk_state_pc ? (set_sp … spp st) init_pc (null_pc one).
     40  let st ≝ mk_state pars
     41    (* frames ≝ *)(Some ? (empty_framesT …))
     42    (* internal_stack ≝ *) empty_is
     43    (* carry ≝ *)(BBbit false)
     44    (* regs ≝ *)(empty_regsT … spp)
     45    (* mem ≝ *)m
     46    (* stack_usage ≝ *)globals_size in
     47  mk_state_pc ?
     48    (* state_no_pc ≝ *)(set_sp … spp st)
     49    (* pc ≝ *)init_pc
     50    (* last_pop ≝ *)(null_pc one).
     51@hide_prf
    10152cases m0 in H; #m1 #m2 #m3 #H
    10253whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
    … …  
    10556
    10657definition joint_classify_step :
    107   ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝
    108   λp,stmt.
     58  ∀p,globals.joint_step p globals → status_class ≝
     59  λp,g,stmt.
    10960  match stmt with
    11061  [ CALL f args dest ⇒ cl_call
    … …  
    11465
    11566definition joint_classify_final :
    116   ∀p : evaluation_params.joint_fin_step p → status_class ≝
     67  ∀p.joint_fin_step p → status_class ≝
    11768  λp,stmt.
    11869  match stmt with
    … …  
    12374
    12475definition joint_classify :
    125   ∀p : evaluation_params.state_pc p → status_class ≝
    126   λp,st.
    127   match fetch_statement … (ev_genv p) (pc … st) with
     76  ∀p.∀pars : evaluation_params p.state_pc p → status_class ≝
     77  λp,pars,st.
     78  match fetch_statement … (ev_genv … pars) (pc … st) with
    12879  [ OK i_fn_s ⇒
    12980    match \snd i_fn_s with
    130     [ sequential s _ ⇒ joint_classify_step p s
    131     | final s ⇒ joint_classify_final p s
     81    [ sequential s _ ⇒ joint_classify_step … s
     82    | final s ⇒ joint_classify_final … s
    13283    | FCOND _ _ _ _ ⇒ cl_jump
    13384    ]
    … …  
    13586  ].
    13687
    137 lemma joint_classify_call : ∀p : evaluation_params.∀st.
    138   joint_classify p st = cl_call →
     88lemma joint_classify_call : ∀p,pars,st.
     89  joint_classify p pars st = cl_call →
    13990  ∃i_f,f',args,dest,next.
    140   fetch_statement … (ev_genv p) (pc … st) =
     91  fetch_statement … (ev_genv … pars) (pc … st) =
    14192    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
    142 #p #st
     93#p #pars #st
    14394whd in match joint_classify; normalize nodelta
    144 inversion (fetch_statement … (ev_genv p) (pc … st))
     95inversion (fetch_statement ????)
    14596[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
    14697* #i_f *
    … …  
    153104qed.
    154105
    155 definition joint_after_ret : ∀p:evaluation_params.
    156   (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
    157 λp,s1,s2.
    158 match fetch_statement … (ev_genv p) (pc … s1) with
     106definition joint_after_ret : ∀p : sem_params.∀pars.
     107  (Σs : state_pc p.joint_classify p pars s = cl_call) → state_pc p → Prop ≝
     108λp,pars,s1,s2.
     109match fetch_statement … (ev_genv … pars) (pc … s1) with
    159110[ OK x ⇒
    160111  match \snd x with
    … …  
    167118].
    168119
    169 definition joint_call_ident : ∀p:evaluation_params.
     120definition joint_call_ident : ∀p : sem_params.∀pars.
    170121  state_pc p → ident ≝
    171122(* this is a definition without a dummy ident :
    … …  
    193144(* with a dummy ident (which is never used as seen above in the commented script)
    194145   I think handling of the function is easier *)
    195 λp,st.
     146λp,pars,st.
    196147let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
    197 match fetch_statement … (ev_genv p) (pc … st) with
     148match fetch_statement … (ev_genv … pars) (pc … st) with
    198149[ OK x ⇒
    199150  match \snd x with
    … …  
    202153    [ CALL f' args dest ⇒
    203154      match
    204         (! bl ← block_of_call … (ev_genv p) f' st;
    205          fetch_internal_function … (ev_genv p) bl) with
     155        (! bl ← block_of_call … (ev_genv … pars) f' st;
     156         fetch_internal_function … (ev_genv … pars) bl) with
    206157      [ OK i_f ⇒ \fst i_f
    207158      | _ ⇒ dummy
    … …  
    214165].
    215166
    216 definition joint_tailcall_ident : ∀p:evaluation_params.
     167definition joint_tailcall_ident : ∀p:sem_params.∀pars.
    217168  state_pc p → ident ≝
    218 λp,st.
     169λp,pars,st.
    219170let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
    220 match fetch_statement … (ev_genv p) (pc … st) with
     171match fetch_statement … (ev_genv … pars) (pc … st) with
    221172[ OK x ⇒
    222173  match \snd x with
    … …  
    225176    [ TAILCALL _ f' args ⇒
    226177      match
    227         (! bl ← block_of_call … (ev_genv p) f' st;
    228          fetch_internal_function … (ev_genv p) bl) with
     178        (! bl ← block_of_call … (ev_genv … pars) f' st;
     179         fetch_internal_function … (ev_genv … pars) bl) with
    229180      [ OK i_f ⇒ \fst i_f
    230181      | _ ⇒ dummy
    … …  
    256207
    257208definition cost_label_of_stmt :
    258   ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
    259   λp,s.match s with
     209  ∀p : sem_params.∀pars.joint_statement p (globals p pars) → option costlabel ≝
     210  λp,pars,s.match s with
    260211  [ sequential s _ ⇒
    261212    match s with
    … …  
    267218
    268219definition joint_label_of_pc ≝
    269   λp : evaluation_params.
     220  λp,pars.
    270221    (λpc.
    271       match fetch_statement … (ev_genv p) pc with
     222      match fetch_statement … (ev_genv p pars) pc with
    272223      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    273224      | _ ⇒ None ?
    … …  
    278229mk_program_counter «mk_block (-1), refl …» (p1 one).
    279230
    280 definition joint_final: ∀p: sem_params.∀globals.
    281   genv p globals → state_pc p → option int ≝
    282  λp,globals,ge,st.
     231definition joint_final: ∀p: sem_params.∀pars.
     232  state_pc p → option int ≝
     233 λp,pars,st.
     234 let ge ≝ ev_genv p pars in
    283235 if eq_program_counter (pc … st) exit_pc' then
    284236   let ret ≝ call_dest_for_main ?? p in
    … …  
    294246   (* as_status ≝ *) (state_pc p)
    295247   (* as_execute ≝ *)
    296     (λs1,s2.eval_state … (ev_genv p) s1 = return s2)
     248    (λs1,s2.eval_state … (ev_genv … p) s1 = return s2)
    297249   (* (* as_init ≝ *) (make_initial_state p) *)
    298250   (* as_pc ≝ *) pcDeq
    299251   (* as_pc_of ≝ *) (pc …)
    300    (* as_classify ≝ *) (joint_classify p)
    301    (* as_label_of_pc ≝ *) (joint_label_of_pc p)
    302    (* as_after_return ≝ *) (joint_after_ret p)
    303    (* as_result ≝ *) (joint_final p  (globals ?) (ev_genv p))
    304    (* as_call_ident ≝ *) (λst.joint_call_ident p st)
    305    (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
     252   (* as_classify ≝ *) (joint_classify … p)
     253   (* as_label_of_pc ≝ *) (joint_label_of_pc … p)
     254   (* as_after_return ≝ *) (joint_after_ret … p)
     255   (* as_result ≝ *) (joint_final … p)
     256   (* as_call_ident ≝ *) (λst.joint_call_ident … p st)
     257   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident … p st).
    306258
    307259(* alternative definition with integrated prog_params constructor *)

  • src/joint/joint_fullexec.ma

    r2946 r2952  
    22include "common/Measurable.ma".
    33
    4 (* fullexec and co. *)
    5 record joint_global (p : sem_params) : Type[0] ≝
    6 { jglobals : list ident
    7 ; jgenv :> genv p jglobals
    8 }.
    9 
    10 definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝
    11 λp,gl.mk_evaluation_params (jglobals … gl) p gl.
    12 
    13 coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝
    14 eval_params_of_global on _gl : joint_global ? to evaluation_params.
    15 
    16 definition make_joint_global : ∀p : sem_params.
    17   (joint_program p × (ident → option ℕ)) →
    18   joint_global p ≝
    19 λpars, p_stack.
    20 let p ≝ \fst p_stack in
    21 let stack_sizes ≝ \snd p_stack in
    22 let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
    23 mk_joint_global pars
    24   (globals … ev_pars)
    25   (ev_genv … ev_pars).
    26 
    274definition joint_exec: sem_params → trans_system io_out io_in ≝
    28   λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
    29    (λenv.joint_final G (jglobals … env) env)
     5  λG.mk_trans_system ?? (evaluation_params G)  (λ_. state_pc G)
     6   (λenv.joint_final … env)
    307   (λenv.λst.! st' ← eval_state … env st ;
    31     let charge ≝ match joint_label_of_pc env (pc … st) with
     8    let charge ≝ match joint_label_of_pc … env (pc … st) with
    329      [ Some c ⇒ Echarge c | None ⇒ E0 ] in
    3310     return 〈charge, st'〉).
    … …  
    3714  λG.mk_fullexec ?? (joint_program G × (ident → option ℕ))
    3815    (joint_exec G)
    39     (make_joint_global G)
     16    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
    4017    (λp_stacks.
    4118      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
    … …  
    4421  preclassified_system ≝
    4522  λG.mk_preclassified_system (joint_fullexec G)
    46     (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env) (pc … st)))
    47     (λenv.joint_classify (eval_params_of_global … env))
    48     (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s).
     23    (λenv.λst.¬is_none … (joint_label_of_pc  … env (pc … st)))
     24    (λenv.joint_classify … env)
     25    (λenv.λs.λ_.joint_call_ident … env s).

  • src/joint/joint_semantics.ma

    r2946 r2952  
    1717; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
    1818; stack_sizes : ident → option ℕ
    19 ; get_pc_from_label : ident (* current function *) → label → res program_counter
     19; premain : F globals
    2020}.
    2121
    … …  
    119119*)
    120120
     121definition pre_main_id : ident ≝ an_identifier … one.
     122
    121123(* this can replace graph_fetch function and lin_fetch_function *)
    122124definition fetch_function:
    123  ∀F.
    124  ∀ge : genv_t F.
     125 ∀F,globals.
     126 ∀ge : genv_gen F globals.
    125127  (Σb.block_region b = Code) →
    126   res (ident×F) ≝
    127  λF,ge,bl.
    128  opt_to_res … [MSG BadFunction]
    129   (! id ← symbol_for_block … ge bl ;
    130    ! fd ← find_funct_ptr … ge bl ;
    131    return 〈id, fd〉).
     128  res (ident×(fundef (F globals))) ≝
     129 λF,g,ge,bl.
     130 if eqZb (block_id bl) (-1) then
     131   return 〈pre_main_id, Internal ? (premain … ge)〉
     132 else
     133   opt_to_res … [MSG BadFunction]
     134    (! id ← symbol_for_block … ge bl ;
     135     ! fd ← find_funct_ptr … ge bl ;
     136     return 〈id, fd〉).
    132137
    133138definition fetch_internal_function :
    134  ∀F.
    135  ∀ge : genv_t (fundef F).
     139 ∀F,globals.
     140 ∀ge : genv_gen F globals.
    136141  (Σb.block_region b = Code) →
    137   res (ident×F) ≝
    138  λF,ge,bl.
     142  res (ident×(F globals)) ≝
     143 λF,g,ge,bl.
    139144 ! 〈id, fd〉 ← fetch_function … ge bl ;
    140145 match fd with
    … …  
    143148 ].
    144149 
    145 lemma fetch_internal_function_no_minus_one :
     150(* lemma fetch_internal_function_minus_one :
    146151  ∀F,V,i,p,bl.
    147152  block_id (pi1 … bl) = -1 →
    … …  
    154159  cases (symbol_for_block ???) normalize //
    155160qed.
     161*)
    156162
    157163inductive call_kind : Type[0] ≝
    … …  
    317323
    318324definition fetch_statement: ∀p : sem_params.∀globals.
    319   ∀ge : genv_t (joint_function p globals). program_counter →
     325  ∀ge : genv p globals. program_counter →
    320326  res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
    321327  λp,globals,ge,ptr.
    … …  
    326332
    327333definition pc_of_label : ∀p : sem_params.∀globals.
    328   genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝
     334  genv p globals → (Σb.block_region b = Code) → label → res program_counter ≝
    329335  λp,globals,ge,bl,lbl.
    330336  ! 〈i, fn〉 ← fetch_internal_function … ge bl ;
    … …  
    378384
    379385definition goto: ∀p : sem_params.∀globals.
    380   genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝
     386  genv p globals → label → state_pc p → res (state_pc p) ≝
    381387 λp,globals,ge,l,st.
    382388  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
    … …  
    393399 set_pc … newpc st.
    394400
    395 definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
     401definition next_of_call_pc : ∀p : sem_params.∀globals.
     402  genv p globals →
    396403  program_counter → res (succ p) ≝
    397404λp,globals,ge,pc.
    … …  
    488495    ! bl ← find_symbol … ge id;
    489496    code_block_of_block bl).
    490  
     497
     498definition get_pc_from_label :
     499  ∀p : sem_params.∀globals.
     500  genv p globals →
     501  ident (* current function *) → label → res program_counter ≝
     502  λp,g,ge,id,lbl.
     503  ! bl ← block_of_funct_id … p ge id ;
     504  pc_of_label … ge bl lbl.
     505   
    491506definition block_of_call ≝ λp : sem_params.
    492507  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.

  • src/joint/semanticsUtils.ma

    r2946 r2952  
    136136  on _pars : sem_lin_params to sem_params.
    137137
    138 (* watch out, implementation dependent:
    139    an_identifier SymbolTag one must be unused (used for premain)
    140 *)
    141 definition pre_main_id : ident ≝ an_identifier … one.
    142 
     138(* TODO move elsewhere *)
    143139lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m.
    144140  (p = q → P o) →
    … …  
    162158qed.
    163159
    164 (* we just manually overwrite genv_t tables with the pre_main.
    165    the RTLabs → RTL pass will need to ensure no pre_main_id is actually present *)
    166 definition joint_globalenv :
    167   ∀pars : sem_params.joint_program pars → genv_t ? ≝
    168   λpars,prog.
    169   let genv ≝ drop_fn … pre_main_id (globalenv … (λx.x) prog) in
    170   mk_genv_t ?
    171     (insert … one (Internal … (pre_main_generator … pars prog)) (functions … genv))
    172     (nextfunction … genv)
    173     (add … (symbols … genv) pre_main_id (mk_block (-1)))
    174     ?.
    175 @hide_prf
    176 whd in match insert; normalize nodelta #b
    177 @lookup_opt_pm_set_elim #H destruct
    178 [ #_ %{pre_main_id} @lookup_add_hit ]
    179 #G cases (functions_inv … G) #id #EQ %{id}
    180 @lookup_add_elim #EQid destruct [2: assumption ]
    181 @⊥ whd in match drop_fn in EQ; normalize nodelta in EQ;
    182 >lookup_remove_hit in EQ; #ABS destruct
    183 qed.
    184 
    185160lemma fetch_statement_eq : ∀p:sem_params.∀g.
    186   ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
     161  ∀ge : genv p g.∀ptr : program_counter.
    187162  ∀i,fn,s.
    188163  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
    … …  
    196171
    197172lemma fetch_statement_inv : ∀p:sem_params.∀g.
    198   ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
     173  ∀ge : genv p g.∀ptr : program_counter.
    199174  ∀i,fn,s.
    200175  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
    … …  
    204179#p #g #ge #ptr #i #fn #s #H
    205180elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
    206 elim (bind_inversion ????? H) #s' * #H
     181elim (bind_inversion ????? H) #s' * -H #H
    207182lapply (opt_eq_from_res ???? H) -H #EQ2
    208183whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
    … …  
    421396include alias "common/Pointers.ma".
    422397
    423 lemma fetch_function_transf :
    424  ∀A,B,V,init.∀prog_in : program A V.
    425  ∀trans : ∀vars.A vars → B vars.
    426  let prog_out ≝ transform_program … prog_in trans in
     398(* TODO move *)
     399lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
     400#A #P #Q #l #H elim l -l [2: #hd #tl #IH] * #G whd /3 by or_introl, or_intror/ qed.
     401
     402definition joint_globalenv :
     403  ∀p : sem_params.∀pr:joint_program p.
     404    (ident → option ℕ) → genv p (prog_var_names … pr) ≝
     405λp,prog,stacksizes.
     406let genv ≝ globalenv … (λx.x) prog in
     407mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog).
     408#s #H
     409elim (find_symbol_exists ?? (λx.x) … prog s ?)
     410[ #bl #EQ >EQ % #ABS destruct ]
     411@Exists_append_r
     412@(Exists_mp … H) //
     413qed.
     414
     415lemma opt_to_res_bind : ∀X,Y,m,f,e.opt_to_res Y e (! x ← m ; f x) =
     416  ! x ← opt_to_res X e m ; opt_to_res Y e (f x).
     417#X #Y * [2: #x] #f #e % qed.
     418
     419lemma fetch_function_transf:
     420 ∀src,dst : sem_params.∀prog_in : joint_program src.
     421 ∀stacksizes.
     422 ∀trans : ∀vars.joint_function src vars → joint_function dst vars.
     423 let prog_out ≝
     424  mk_joint_program dst
     425    (transform_program … prog_in trans) (init_cost_label … prog_in) in
    427426 ∀bl.
    428  fetch_function … (globalenv … init prog_out) bl =
    429  ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ;
    430  return 〈i, trans … f〉.
    431 #A #B #V #init #prog_in #trans #bl
    432 whd in match fetch_function; normalize nodelta
    433 >(symbol_for_block_transf A B V init prog_in trans)
    434 cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind
     427 fetch_function … (joint_globalenv … prog_out stacksizes) bl =
     428 if eqZb (block_id bl) (-1) then
     429   return 〈pre_main_id, Internal ? (pre_main_generator … dst prog_out)〉
     430 else
     431   ! 〈id, f〉 ← fetch_function … (joint_globalenv … prog_in stacksizes) bl ;
     432   return 〈id, trans … f〉.
     433#src #dst #p #sizes #tf whd
     434lapply (transform_program_match … tf p)
     435#MATCH
     436whd in match fetch_function;
     437whd in match joint_globalenv; normalize nodelta
     438#bl @eqZb_elim #Hbl normalize nodelta [ % ]
     439>symbol_for_block_transf
     440>opt_to_res_bind >opt_to_res_bind in ⊢ (???%); >m_bind_bind
     441@m_bind_ext_eq #id
    435442whd in match find_funct_ptr; normalize nodelta
    436 whd in match (block_region (pi1 ?? bl));
    437 cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try %
    438 >(functions_transf A B V init prog_in trans p)
    439 cases (lookup_opt ???) //
     443cases bl -bl ** [2,3: #p] normalize nodelta #_ try %
     444lapply (functions_match … (globalenv_match … MATCH) p) try @(λx.x)
     445[#v #w * //]
     446lapply (sym_eq ????)
     447whd in match prog_var_names; normalize nodelta
     448#E >(K ?? E) -E normalize nodelta
     449cases (lookup_opt ???) [2: #x ] normalize nodelta
     450cases (lookup_opt ???) [2,4: #y ] normalize nodelta
     451* %
    440452qed.
    441453
    442454lemma fetch_internal_function_transf :
    443  ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V.
    444  ∀trans : ∀vars.A vars → B vars.
    445  let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
     455 ∀src,dst : sem_params.∀prog_in : joint_program src.
     456 ∀stacksizes.
     457 ∀trans : ∀vars.joint_closed_internal_function src vars → joint_closed_internal_function dst vars.
     458 let prog_out ≝
     459  mk_joint_program dst
     460    (transform_program … prog_in (λvars.transf_fundef … (trans vars))) (init_cost_label … prog_in) in
    446461 ∀bl.
    447  fetch_internal_function … (globalenv … init prog_out) bl =
    448  ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ;
    449  return 〈i, trans … f〉.
    450 #A #B #V #init #prog #trans #bl
    451  whd in match fetch_internal_function; normalize nodelta
    452 >(fetch_function_transf … prog)
    453 cases (fetch_function ???)
    454 [ * #id * #f % | #e % ]
     462 fetch_internal_function … (joint_globalenv … prog_out stacksizes) bl =
     463 if eqZb (block_id bl) (-1) then
     464   return 〈pre_main_id, pre_main_generator … dst prog_out〉
     465 else
     466   ! 〈i, f〉 ← fetch_internal_function … (joint_globalenv … prog_in stacksizes) bl ;
     467   return 〈i, trans … f〉.
     468#src #dst #p #sizes #tf whd
     469#bl whd in match fetch_internal_function; normalize nodelta
     470>(fetch_function_transf … p)
     471@eqZb_elim #Hbl [%] normalize nodelta >m_bind_bind >m_bind_bind
     472@m_bind_ext_eq * #id * #f %
    455473qed.
    456474
    … …  
    485503definition b_graph_transform_program_props ≝
    486504  λsrc,dst : sem_graph_params.
     505  λstacksizes.
    487506  λdata,prog_in.
    488507  λinit_regs : block → list register.
    … …  
    490509  λf_regs : block → label → list register.
    491510   let prog_out ≝ b_graph_transform_program src dst data prog_in in
    492    let src_genv ≝ joint_globalenv src prog_in in
    493    let dst_genv ≝ joint_globalenv dst prog_out in
     511   let src_genv ≝ joint_globalenv src prog_in stacksizes in
     512   let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    494513  ∀bl,def_in.
    495514  block_id … bl ≠ -1 →
    … …  
    503522lemma make_b_graph_transform_program_props :
    504523 ∀src,dst:sem_graph_params.
     524 ∀stacksizes.
    505525 ∀data : ∀globals.joint_closed_internal_function src globals →
    506526  bound_b_graph_translate_data src dst globals.
    507527 ∀prog_in : joint_program src.
    508528 let prog_out ≝ b_graph_transform_program … data prog_in in
    509  let src_genv ≝ joint_globalenv src prog_in in
    510  let dst_genv ≝ joint_globalenv dst prog_out in
     529 let src_genv ≝ joint_globalenv src prog_in stacksizes in
     530 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    511531 ∃init_regs : block → list register.
    512532 ∃f_lbls : block → label → list label.
    513533 ∃f_regs : block → label → list register.
    514  b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
     534 b_graph_transform_program_props src dst stacksizes data prog_in init_regs f_lbls f_regs.
    515535cases daemon (* TOREDO
    516536#src #dst #data #prog_in
    … …  
    612632qed.
    613633
     634lemma if_elim' : ∀A : Type[0].∀P : A → Prop.∀b : bool.∀c1,c2 : A.
     635  (b → P c1) → (¬(bool_to_Prop b) → P c2) → P (if b then c1 else c2).
     636#A #P * /3 by Prop_notb/ qed.
     637
    614638lemma b_graph_transform_program_fetch_internal_function :
    615639 ∀src,dst:sem_graph_params.
     640 ∀stacksizes.
    616641 ∀data : ∀globals.joint_closed_internal_function src globals →
    617642  bound_b_graph_translate_data src dst globals.
    … …  
    620645 ∀f_lbls : block → label → list label.
    621646 ∀f_regs : block → label → list register.
    622  b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
     647 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs →
    623648 let prog_out ≝ b_graph_transform_program … data prog_in in
    624  let src_genv ≝ joint_globalenv src prog_in in
    625  let dst_genv ≝ joint_globalenv dst prog_out in
     649 let src_genv ≝ joint_globalenv src prog_in stacksizes in
     650 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    626651 ∀bl : Σbl.block_region … bl = Code.∀id,def_in.
    627652 block_id … bl ≠ -1 →
    … …  
    632657 b_graph_translate_props src dst ? init_data
    633658    def_in def_out (f_lbls bl) (f_regs bl).
    634 #src #dst #data #prog_in
     659#src #dst #stacksizes #data #prog_in
    635660#init_regs #f_lbls #f_regs #props
    636661#bl #id #def_in #NEQ
    637662#H @('bind_inversion H) * #id' * #def_in' -H
    638 normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
    639 @('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1
    640 #H @('bind_inversion H) -H #def_in' #H
    641 whd in ⊢ (??%%→?); #EQ destruct
     663normalize nodelta [2: #_ whd in ⊢ (??%%→?); #ABS destruct ]
     664whd in match fetch_function; normalize nodelta
     665>(eqZb_false … NEQ) normalize nodelta
     666#H @('bind_inversion (opt_eq_from_res … H)) -H #id'' #EQ1
     667#H @('bind_inversion H) -H #def_in'' #H
     668whd in ⊢ (??%%→??%%→?); #EQ2 #EQ3 destruct
    642669cases (props … NEQ H)
    643670#loc_data * #def_out ** #H1 #H2 #H3
    … …  
    646673whd in match fetch_internal_function;
    647674whd in match fetch_function; normalize nodelta
    648 cases daemon (* TOREDO
     675>(eqZb_false … NEQ) normalize nodelta
    649676>symbol_for_block_transf >EQ1 >m_return_bind
    650 >H1 % *)
     677>H1 %
    651678qed.
    652679
    653680lemma b_graph_transform_program_fetch_statement :
    654  ∀src,dst:sem_graph_params.
     681 ∀src,dst:sem_graph_params.∀stacksizes.
    655682 ∀data : ∀globals.joint_closed_internal_function src globals →
    656683  bound_b_graph_translate_data src dst globals.
    … …  
    659686 ∀f_lbls : block → label → list label.
    660687 ∀f_regs : block → label → list register.
    661  b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
     688 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs →
    662689 let prog_out ≝ b_graph_transform_program … data prog_in in
    663  let src_genv ≝ joint_globalenv src prog_in in
    664  let dst_genv ≝ joint_globalenv dst prog_out in
     690 let src_genv ≝ joint_globalenv src prog_in stacksizes in
     691 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    665692 ∀pc,id,def_in,s.
    666693 block_id … (pc_block … pc) ≠ -1 →
    … …  
    686713  | FCOND abs _ _ _ ⇒ Ⓧabs
    687714  ].
    688 #src #dst #data #prog_in
     715#src #dst #stacksizes #data #prog_in
    689716#init_regs #f_lbls #f_regs #props
    690717#pc #id #def_in #s #NEQ
    … …  
    701728
    702729lemma b_graph_transform_program_fetch_statement_plus :
    703  ∀src,dst:sem_graph_params.
     730 ∀src,dst:sem_graph_params.∀stacksizes.
    704731 ∀data : ∀globals.joint_closed_internal_function src globals →
    705732  bound_b_graph_translate_data src dst globals.
    … …  
    708735 ∀f_lbls : block → label → list label.
    709736 ∀f_regs : block → label → list register.
    710  b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
     737 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs →
    711738 let prog_out ≝ b_graph_transform_program … data prog_in in
    712  let src_genv ≝ joint_globalenv src prog_in in
    713  let dst_genv ≝ joint_globalenv dst prog_out in
     739 let src_genv ≝ joint_globalenv src prog_in stacksizes in
     740 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
    714741 ∀pc,id,def_in,s.
    715742 block_id … (pc_block … pc) ≠ -1 →
    … …  
    744771  | FCOND abs _ _ _ ⇒ Ⓧabs
    745772  ].
    746 #src #dst #data #prog_in
     773#src #dst #stacksizes #data #prog_in
    747774#init_regs #f_lbls #f_regs #props
    748775#pc #id #def_in #s #NEQ
Note: See TracChangeset for help on using the changeset viewer.