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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.