Changeset 2946 for src/joint


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

Location:
src/joint
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2865 r2946  
    524524(p : params) (globals : list ident) (def : joint_internal_function p globals)
    525525: Prop ≝
    526 { entry_costed :
    527   ∃l,nxt.
    528         stmt_at … (joint_if_code … def) (joint_if_entry … def) =
    529           Some … (sequential … (COST_LABEL … l) nxt)
    530 ; entry_unused :
     526{ entry_unused :
    531527  let entry ≝ joint_if_entry … def in
    532528  let code ≝ joint_if_code … def in
     
    598594definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    599595
    600 definition joint_program ≝
    601  λp:params. program (joint_function p) nat.
     596record joint_program (p : params) : Type[0] ≝
     597{ joint_prog :> program (joint_function p) (list init_data)
     598; init_cost_label : costlabel
     599(* here we can have global invariants (like injectivity of cost labels) *)
     600}.
    602601
    603602(* The cost model for stack consumption *)
     
    613612   [ ] (prog_funct ?? pr).
    614613
     614include "common/Globalenvs.ma". (* for size_init_data_list, probably to be moved to AST.ma *)
    615615definition globals_stacksize : ∀p.joint_program p → nat ≝
    616616 λpars,p.
    617  Σ_{entry ∈ prog_vars … p}(\snd entry).
    618 
     617 Σ_{entry ∈ prog_vars … p}(size_init_data_list … (\snd entry)).
     618
  • src/joint/Traces.ma

    r2932 r2946  
    1 include "joint/joint_semantics.ma".
     1include "joint/semanticsUtils.ma".
    22include "common/StructuredTraces.ma".
    33
     
    3939
    4040lemma 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.
     41#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
     42
     43lemma 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)) →
     47P (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 ]
     51qed.
    4252
    4353definition make_global : prog_params → evaluation_params
     
    4656let p ≝ prog pars in
    4757let spars ≝ prog_spars pars in
    48 let genv ≝ globalenv_noinit ? p in
     58let genv ≝ joint_globalenv spars p in
    4959let get_pc_lbl ≝ λid,lbl.
    5060  ! bl ← block_of_funct_id … spars genv id ;
     
    5666 (* (prog_io pars) *).
    5767#s #H
    58 elim (find_symbol_exists … p s ?)
    59 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
     68elim (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) ]
    6075@Exists_append_r
    6176@(Exists_mp … H) //
     
    6681
    6782definition make_initial_state :
    68  ∀pars: prog_params.res (state_pc pars)
     83 ∀pars: prog_params.state_pc pars
    6984λpars.let p ≝ prog pars in
    7085  let sem_globals : evaluation_params ≝ pars in
    7186  let ge ≝ ev_genv sem_globals in
    72   let m0 ≝ alloc_mem … p in
     87  (* this is going to change shortly: globals will not reside in globalenv anymore *)
     88  let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
    7389  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
    7490  let globals_size ≝ globals_stacksize … p in
     
    8197(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8298  let main ≝ prog_main … p in
    83   let st0 ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m in
    84   (* use exit_pc as ra and call_dest_for_main as dest *)
    85   let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    86   ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
    87   let st0'' ≝ set_no_pc … st0_no_pc st0' in
    88   ! bl ← block_of_call … ge (inl … main) st0'';
    89   ! 〈i, fn〉 ← fetch_function … ge bl ;
    90   match fn with
    91   [ Internal ifn ⇒
    92     ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
    93     let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    94     return mk_state_pc … st' pc' exit_pc
    95   | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    96   ].
     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).
    97101cases m0 in H; #m1 #m2 #m3 #H
    98102whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
     
    197201    match s with
    198202    [ CALL f' args dest ⇒
    199         match
    200           (! bl ← block_of_call … (ev_genv p) f' st;
    201            fetch_internal_function … (ev_genv p) bl) with
    202         [ OK i_f ⇒ \fst i_f
    203         | _ ⇒ dummy
    204         ]
     203      match
     204        (! bl ← block_of_call … (ev_genv p) f' st;
     205         fetch_internal_function … (ev_genv p) bl) with
     206      [ OK i_f ⇒ \fst i_f
    205207      | _ ⇒ dummy
    206208      ]
     209    | _ ⇒ dummy
     210    ]
    207211  | _ ⇒ dummy
    208212  ]
     
    270274      ]).
    271275
     276(* the prime is to render obsolete old definition of exit_pc, remove when all is corrected *)
     277definition exit_pc' : program_counter ≝
     278mk_program_counter «mk_block (-1), refl …» (p1 one).
     279
     280definition joint_final: ∀p: sem_params.∀globals.
     281  genv p globals → state_pc p → option int ≝
     282 λp,globals,ge,st.
     283 if eq_program_counter (pc … st) exit_pc' then
     284   let ret ≝ call_dest_for_main ?? p in
     285   res_to_opt … (! vals ← read_result … ge ret st ;
     286               Word_of_list_beval vals)
     287 else None ?.
     288
    272289definition joint_abstract_status :
    273290 ∀p : prog_params.
     
    284301   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
    285302   (* as_after_return ≝ *) (joint_after_ret p)
    286    (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
     303   (* as_result ≝ *) (joint_final p  (globals ?) (ev_genv p))
    287304   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
    288305   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
  • src/joint/TranslateUtils.ma

    r2855 r2946  
    480480@hide_prf
    481481cases def in abs; -def #def #good_def
    482 cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
     482cases (entry_is_cost … good_def) #nxt' * #c #EQ >EQ #ABS destruct
    483483qed.
    484484
     
    600600  joint_program dst_g_pars ≝
    601601  λsrc,dst,init,p.
    602   transform_program ??? p
    603     (λvarnames.transf_fundef ?? (λdef_in.
    604       b_graph_translate … (init varnames def_in) def_in)).
     602  mk_joint_program ?
     603    (transform_program ??? p
     604      (λvarnames.transf_fundef ?? (λdef_in.
     605        b_graph_translate … (init varnames def_in) def_in)))
     606    (init_cost_label … p).
    605607
    606608definition added_registers :
  • src/joint/joint_fullexec.ma

    r2821 r2946  
    2020let p ≝ \fst p_stack in
    2121let stack_sizes ≝ \snd p_stack in
    22 let genv ≝ globalenv_noinit ? p in
    23 let get_pc_lbl ≝ λid,lbl.
    24   ! bl ← block_of_funct_id … pars genv id ;
    25   pc_of_label … genv bl lbl in
     22let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
    2623mk_joint_global pars
    27   (prog_var_names ?? p)
    28   (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl).
    29  (* (prog_io pars) *).
    30 #s #H
    31 elim (find_symbol_exists … p s ?)
    32 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
    33 @Exists_append_r
    34 @(Exists_mp … H) //
    35 qed.
     24  (globals … ev_pars)
     25  (ev_genv … ev_pars).
    3626
    3727definition joint_exec: sem_params → trans_system io_out io_in ≝
    3828  λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
    39    (λenv.is_final G (jglobals … env) env exit_pc)
     29   (λenv.joint_final G (jglobals … env) env)
    4030   (λenv.λst.! st' ← eval_state … env st ;
    4131    let charge ≝ match joint_label_of_pc env (pc … st) with
     
    4939    (make_joint_global G)
    5040    (λp_stacks.
    51       make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
     41      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
    5242
    5343definition joint_preclassified_system : sem_params →
  • src/joint/joint_semantics.ma

    r2920 r2946  
    6060 ; regs: regsT semp
    6161 ; m: bemem
     62 ; stack_usage : ℕ
    6263 }.
    6364
     
    6768  { st_no_pc :> state semp
    6869  ; pc : program_counter
    69   (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *)
     70  (* for correctness reasons: pc of last popped calling address (null_pc at the start) *)
    7071  ; last_pop : program_counter
    7172  }.
    7273
    73 (* special program counter that is guaranteed to not correspond to anything *)
    74 definition exit_pc : program_counter ≝
     74definition init_pc : program_counter ≝
    7575  mk_program_counter «mk_block (-1), refl …» one.
    7676
     
    7979
    8080definition set_m: ∀p. bemem → state p → state p ≝
    81  λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
     81 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st).
    8282
    8383definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    84  λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
     84 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st).
    8585
    8686definition set_sp: ∀p. ? → state p → state p ≝
    8787 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
    88  mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
     88 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st).
    8989
    9090definition set_carry: ∀p. bebit → state p → state p ≝
    91  λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     91 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st).
    9292
    9393definition set_istack: ∀p. internal_stack → state p → state p ≝
    94  λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
     94 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st).
    9595
    9696definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    100100 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
    101101
    102 definition set_last_pop: ∀p. ? → state p × program_counter → state_pc p ≝
    103  λp,s,st. mk_state_pc … (\fst … st) (\snd … st) s.
     102definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝
     103 λp,st,pc. mk_state_pc … st pc pc.
    104104
    105105definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    106  λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
     106 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st).
    107107
    108108(*
     
    268268
    269269(* parameters that are defined by serialization *)
    270 record sem_params : Type[1] ≝
     270record serialized_params : Type[1] ≝
    271271  { spp :> params
    272272  ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp)
     
    277277  ; offset_of_point_of_offset :
    278278    ∀o.offset_of_point (point_of_offset o) = o
     279  }.
     280
     281record sem_params : Type[1] ≝
     282  { spp' :> serialized_params
     283  ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p)
    279284  }.
    280285
     
    513518      set_result … p vs dest st.
    514519
     520definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
     521 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
     522  (n + stack_usage … st).
     523
     524definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
     525 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st) (m … st)
     526  (stack_usage … st - n).
     527
    515528definition eval_internal_call ≝
    516529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
    517530λst : state p.
    518531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    519 setup_call … stack_size (joint_if_params … globals fn) args st.
     532! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     533return increment_stack_usage … stack_size st'.
    520534
    521535definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
     
    555569λcurr_id.λcurr_ret : call_dest p.
    556570λst : state p.
    557 ! st' ← pop_frame … ge curr_id curr_ret st ;
    558 ! nxt ← next_of_call_pc … ge (\snd … st') ;
     571! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
     572! 〈st', call_pc〉 ← pop_frame … ge curr_id curr_ret st ;
     573! nxt ← next_of_call_pc … ge call_pc ;
     574let st'' ≝ set_last_pop … (decrement_stack_usage … stack_size st') call_pc in
    559575return
    560   next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
     576  next ? nxt st'' (* now address pushed on stack are calling ones! *).
    561577
    562578definition eval_tailcall ≝
     
    568584match fd with
    569585[ Internal ifd ⇒
    570   ! st' ← eval_internal_call p globals ge i ifd args st ;
     586  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
     587  let st' ≝ decrement_stack_usage … stack_size st in
     588  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    571589  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    572   return mk_state_pc … st' pc (last_pop … st)
     590  return mk_state_pc … st'' pc (last_pop … st)
    573591| External efd ⇒
    574592  ! st' ← eval_external_call … efd args curr_ret st ;
     
    621639  let st'' ≝ set_no_pc … st' st in
    622640  eval_statement_advance … ge id fn s st''.
    623 
    624 definition is_final: ∀p: sem_params.∀globals.
    625   genv p globals → program_counter → state_pc p → option int ≝
    626  λp,globals,ge,exit,st.res_to_opt ? (
    627   do 〈id,fn,s〉 ← fetch_statement  … ge (pc … st);
    628   match s with
    629   [ final s' ⇒
    630     match s' with
    631     [ RETURN ⇒
    632       let curr_ret ≝ joint_if_result … fn in
    633       do st' ← pop_frame … ge id curr_ret st;
    634       if eq_program_counter (\snd … st') exit then
    635       do vals ← read_result … ge curr_ret st ;
    636         Word_of_list_beval vals
    637       else
    638         Error ? [ ]
    639    | _ ⇒ Error ? [ ]
    640    ]
    641  | _ ⇒ Error ? [ ]
    642  ]).
  • src/joint/linearise.ma

    r2823 r2946  
    885885   ≝
    886886  λp,pr.transform_program ??? pr
    887     (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
     887    mk_joint_program
     888      (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in)))
     889      (init_cost_label … pr).
    888890
    889891(*
  • src/joint/semanticsUtils.ma

    r2843 r2946  
    77include "common/extraGlobalenvs.ma".
    88
     9definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
     10
     11definition reg_retrieve : register_env beval → register → res beval ≝
     12 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
     13
    914record hw_register_env : Type[0] ≝
    1015  { reg_env : BitVectorTrie beval 6
    1116  ; other_bit : bebit
    1217  }.
    13 
    14 definition empty_hw_register_env: hw_register_env ≝
    15   mk_hw_register_env (Stub …) BBundef.
    1618
    1719include alias "ASM/BitVectorTrie.ma".
     
    4244hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
    4345
     46definition init_hw_register_env: xpointer → hw_register_env ≝
     47 hwreg_store_sp (mk_hw_register_env (Stub …) BBundef).
     48
    4449(*** Store/retrieve on pseudo-registers ***)
    4550include alias "common/Identifiers.ma".
    4651
    47 record reg_sp : Type[0] ≝
    48 { reg_sp_env :> identifier_map RegisterTag beval
    49 ; stackp : xpointer
    50 }.
    51 
    52 definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
    53 
    54 definition reg_retrieve : register_env beval → register → res beval ≝
    55  λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
    56 
    57 definition reg_sp_store ≝ λreg,v,locals.
    58 let locals' ≝ reg_store reg v (reg_sp_env locals) in
    59 mk_reg_sp locals' (stackp locals).
    60 
    6152unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
    62 
    63 definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
    64 
    65 definition reg_sp_init ≝ mk_reg_sp (empty_map …).
    66 (*** Store/retrieve on hardware registers ***)
    67 
    68 definition init_hw_register_env: xpointer → hw_register_env ≝
    69  λsp.hwreg_store_sp empty_hw_register_env sp.
    7053
    7154(******************************** GRAPHS **************************************)
     
    7457{ sgp_pars : uns_params
    7558; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
     59; graph_pre_main_generator :
     60  ∀p : joint_program (mk_graph_params sgp_pars).
     61  joint_closed_internal_function (mk_graph_params sgp_pars) (prog_var_names … p)
    7662}.
    7763
     
    9177  λpars.
    9278  mk_sem_params
    93     (pars : graph_params)
    94     (sgp_sup pars ?)
    95     (word_of_identifier ?)
    96     (an_identifier ?)
    97     ? (refl …).
     79    (mk_serialized_params
     80      (pars : graph_params)
     81      (sgp_sup pars ?)
     82      (word_of_identifier ?)
     83      (an_identifier ?)
     84      ? (refl …))
     85    (graph_pre_main_generator pars).
    9886* #p % qed.
    9987
     
    113101{ slp_pars : uns_params
    114102; slp_sup : ∀F.sem_unserialized_params slp_pars F
     103; lin_pre_main_generator :
     104  ∀p : joint_program (mk_lin_params slp_pars).
     105  joint_closed_internal_function (mk_lin_params slp_pars) (prog_var_names … p)
    115106}.
    116107
     
    129120  λpars.
    130121  mk_sem_params
    131     (pars : lin_params)
    132     (slp_sup pars ?)
    133     succ_pos_of_nat
    134     (λp.pred (nat_of_pos p))
    135     ??.
    136 [ #n >nat_succ_pos %
    137 | @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
     122    (mk_serialized_params
     123      (pars : lin_params)
     124      (slp_sup pars ?)
     125      succ_pos_of_nat
     126      (λp.pred (nat_of_pos p))
     127      ??)
     128    (lin_pre_main_generator pars).
     129[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
     130| #n >nat_succ_pos %
    138131] qed.
    139132
     
    143136  on _pars : sem_lin_params to sem_params.
    144137
     138(* watch out, implementation dependent:
     139   an_identifier SymbolTag one must be unused (used for premain)
     140*)
     141definition pre_main_id : ident ≝ an_identifier … one.
     142
     143lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m.
     144  (p = q → P o) →
     145  (p ≠ q → P (lookup_opt A p m)) →
     146  P (lookup_opt A p (pm_set A q o m)).
     147#A #P #p #q
     148@(eqb_elim p q) #H #o #m #H1 #H2
     149[ >H >lookup_opt_pm_set_hit @H1 @H
     150| >lookup_opt_pm_set_miss [ @H2 ] @H
     151]
     152qed.
     153
     154lemma lookup_add_elim : ∀tag,A.∀P : option A → Prop.∀m,i,j,x.
     155  (i = j → P (Some ? x)) →
     156  (i ≠ j → P (lookup tag A m j)) →
     157  P (lookup tag A (add tag A m i x) j).
     158#tag #A #P * #m * #p * #q #x
     159#H1 #H2 whd in ⊢ (?%); normalize nodelta whd in match insert; normalize nodelta
     160@lookup_opt_pm_set_elim #H destruct
     161[ @H1 % | @H2 % #EQ destruct cases H #H @H % ]
     162qed.
     163
     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 *)
     166definition 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
     176whd 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
     183qed.
    145184
    146185lemma fetch_statement_eq : ∀p:sem_params.∀g.
     
    346385qed.
    347386
    348 
    349387lemma functions_transf:
    350388 ∀A,B,V,init.∀prog_in : program A V.
     
    403441
    404442lemma fetch_internal_function_transf :
    405  ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
     443 ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V.
    406444 ∀trans : ∀vars.A vars → B vars.
    407445 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
    408446 ∀bl.
    409  fetch_internal_function … (globalenv_noinit … prog_out) bl =
    410  ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ;
     447 fetch_internal_function … (globalenv … init prog_out) bl =
     448 ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ;
    411449 return 〈i, trans … f〉.
    412 #A #B #prog #trans #bl
     450#A #B #V #init #prog #trans #bl
    413451 whd in match fetch_internal_function; normalize nodelta
    414452>(fetch_function_transf … prog)
     
    452490  λf_regs : block → label → list register.
    453491   let prog_out ≝ b_graph_transform_program src dst data prog_in in
    454    let src_genv ≝ globalenv_noinit ? prog_in in
    455    let dst_genv ≝ globalenv_noinit ? prog_out in
     492   let src_genv ≝ joint_globalenv src prog_in in
     493   let dst_genv ≝ joint_globalenv dst prog_out in
    456494  ∀bl,def_in.
     495  block_id … bl ≠ -1 →
    457496  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
    458497  ∃init_data,def_out.
     
    468507 ∀prog_in : joint_program src.
    469508 let prog_out ≝ b_graph_transform_program … data prog_in in
    470  let src_genv ≝ globalenv_noinit ? prog_in in
    471  let dst_genv ≝ globalenv_noinit ? prog_out in
     509 let src_genv ≝ joint_globalenv src prog_in in
     510 let dst_genv ≝ joint_globalenv dst prog_out in
    472511 ∃init_regs : block → list register.
    473512 ∃f_lbls : block → label → list label.
    474513 ∃f_regs : block → label → list register.
    475514 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
     515cases daemon (* TOREDO
    476516#src #dst #data #prog_in
    477517whd in match b_graph_transform_program_props; normalize nodelta
     518whd in match joint_globalenv; normalize nodelta
    478519letin prog_out ≝ (b_graph_transform_program … data prog_in)
    479 letin src_genv ≝ (globalenv_noinit ? prog_in)
    480 letin dst_genv ≝ (globalenv_noinit ? prog_out)
     520letin src_genv ≝ (globalenv … (λx.x) prog_in)
     521letin dst_genv ≝ (globalenv … (λx.x) prog_out)
    481522cut (∀p.lookup_opt ? p (functions ? dst_genv) =
    482523     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
    483524      (lookup_opt ? p (functions ? src_genv)))
    484525[ @functions_transf ]
     526cut (symbols ? dst_genv = symbols ? src_genv)
     527[ @symbols_transf ]
    485528cases dst_genv #functs2 #nextf2 #symbols2 #H2
    486 cases src_genv #functs1 #nextf1 #symbols1 #H1
     529cases src_genv #functs1 #nextf1 #symbols1 #H1 #EQ destruct
    487530lapply H2 lapply H1 lapply functs2
    488531@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
     
    490533#functs2 #H1 #H2 #transf
    491534[ %{(λ_.[ ])} %{(λ_.λ_.[])} %{(λ_.λ_.[])}
    492   #bl #def_in #ABS @⊥ lapply ABS -ABS
     535  #bl #def_in #ABS1 #ABS2 @⊥ lapply ABS2 -ABS2 lapply ABS1 -ABS1
    493536  whd in match find_funct_ptr;
     537  whd in match find_symbol;
    494538  normalize nodelta
    495   whd in match (block_region bl);
    496   cases (block_id bl) normalize nodelta
    497   [2,3: #p [2: >functs1_empty ]]
    498   normalize #ABS destruct
     539  cases bl; * normalize nodelta
     540  [2,3: #p ]
     541  [1,3: #_ whd in ⊢ (???%→?); #EQ destruct ]
     542  >lookup_add_hit
     543  #H >lookup_opt_insert_miss
     544  [2: @(swap_neg … H) #EQ >EQ % ]
     545  whd in match drop_fn; normalize nodelta
     546  cases (lookup … symbols1 pre_main_id)
     547  normalize nodelta
     548  [ >functs1_empty | ** [2,3: #p' ] normalize nodelta
     549    [1,3: >functs1_empty
     550    | @lookup_opt_pm_set_elim #H destruct
     551      [2: >functs1_empty ]
     552    ]
     553  ] whd in ⊢ (???%→?); #EQ destruct
    499554]
    500555cases (IH (pm_set … p (None ?) functs2) ???)
    501 [2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) -G @(eqb_elim b p)
    502   [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ]
    503   #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H
    504 |3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) -G @(eqb_elim b p)
    505   [ #EQ destruct >lookup_opt_pm_set_hit #_ % ]
    506   #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H
    507 |4: #b @(eqb_elim b p)
    508   [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ]
    509   #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf
    510   >(lookup_opt_insert_miss ? f b p … NEQ) %
    511 ]
     556[|*: @hide_prf
     557  [ #b #G @(H1 b ?) @(swap_neg … G) -G
     558    whd in match insert; normalize nodelta
     559    @lookup_opt_pm_set_elim
     560    [ #EQ #ABS destruct ]
     561    #NEQ #H @H
     562  | #b #G @(H2 b ?) @(swap_neg … G) -G
     563    @lookup_opt_pm_set_elim
     564    [ #_ #_ % ]
     565    #_ #H @H
     566  | #b @lookup_opt_pm_set_elim
     567    [ #EQ destruct >p_not_in % ]
     568    #NEQ >transf
     569    >(lookup_opt_insert_miss ? f b p … NEQ) %
     570  ]
     571]
     572#init_regs * #f_lbls * #f_regs #props
    512573-IH cases f in H1 transf; -f #f #H1 #transf
    513 #init_regs * #f_lbls * #f_regs #props
    514574[ (* internal *)
    515575  letin upd ≝ (λA : Type[0].λf : block → A.
     
    532592whd in match (block_region (mk_block p'));
    533593cases p' -p' [2,3,5,6: #p' ] normalize nodelta
    534 [1,3,5,6: #ABS normalize in ABS; destruct]
    535 @(eqb_elim p' p) #pp' destruct
    536 [1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ)
    537   %{loc_data} %
    538   [2: % [ % ]
    539     [ >transf >lookup_opt_insert_hit %
    540     |*: >eq_block_b_b assumption
    541     ]
    542   |]
     594[1,3,5,6: #_ #ABS normalize in ABS; destruct]
     595whd in match find_symbol;
     596whd in match insert; normalize nodelta
     597#bl_prf
     598@lookup_opt_pm_set_elim #pp' destruct
     599[1,3: whd in ⊢ (??%%→?); #EQ destruct(EQ)
     600  [ %{loc_data} %
     601    [2: % [ % ]
     602      [ >lookup_opt_insert_hit %
     603      |*: >eq_block_b_b assumption
     604      ]
     605    |]
    543606|*: >(lookup_opt_insert_miss ???? functs1 … pp')
    544607  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
     
    546609  whd in match find_funct_ptr; normalize nodelta
    547610  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
    548 ]
     611] *)
    549612qed.
    550613
     
    559622 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    560623 let prog_out ≝ b_graph_transform_program … data prog_in in
    561  let src_genv ≝ globalenv_noinit ? prog_in in
    562  let dst_genv ≝ globalenv_noinit ? prog_out in
    563  ∀bl,id,def_in.
     624 let src_genv ≝ joint_globalenv src prog_in in
     625 let dst_genv ≝ joint_globalenv dst prog_out in
     626 ∀bl : Σbl.block_region … bl = Code.∀id,def_in.
     627 block_id … bl ≠ -1 →
    564628 fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
    565629 ∃init_data,def_out.
     
    570634#src #dst #data #prog_in
    571635#init_regs #f_lbls #f_regs #props
    572 #bl #id #def_in
     636#bl #id #def_in #NEQ
    573637#H @('bind_inversion H) * #id' * #def_in' -H
    574638normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
     
    576640#H @('bind_inversion H) -H #def_in' #H
    577641whd in ⊢ (??%%→?); #EQ destruct
    578 cases (props … H)
     642cases (props … NEQ H)
    579643#loc_data * #def_out ** #H1 #H2 #H3
    580644%{loc_data} %{def_out}
     
    582646whd in match fetch_internal_function;
    583647whd in match fetch_function; normalize nodelta
     648cases daemon (* TOREDO
    584649>symbol_for_block_transf >EQ1 >m_return_bind
    585 >H1 %
     650>H1 % *)
    586651qed.
    587652
     
    596661 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    597662 let prog_out ≝ b_graph_transform_program … data prog_in in
    598  let src_genv ≝ globalenv_noinit ? prog_in in
    599  let dst_genv ≝ globalenv_noinit ? prog_out in
     663 let src_genv ≝ joint_globalenv src prog_in in
     664 let dst_genv ≝ joint_globalenv dst prog_out in
    600665 ∀pc,id,def_in,s.
     666 block_id … (pc_block … pc) ≠ -1 →
    601667 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
    602668 ∃init_data,def_out.
     
    622688#src #dst #data #prog_in
    623689#init_regs #f_lbls #f_regs #props
    624 #pc #id #def_in #s
     690#pc #id #def_in #s #NEQ
    625691#H @('bind_inversion H) * #id' #def_in' -H
    626692#EQfif
     
    628694#H lapply (opt_eq_from_res ???? H) -H
    629695#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    630 cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     696cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
    631697#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    632698[ %{H1 H2}
     
    644710 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
    645711 let prog_out ≝ b_graph_transform_program … data prog_in in
    646  let src_genv ≝ globalenv_noinit ? prog_in in
    647  let dst_genv ≝ globalenv_noinit ? prog_out in
     712 let src_genv ≝ joint_globalenv src prog_in in
     713 let dst_genv ≝ joint_globalenv dst prog_out in
    648714 ∀pc,id,def_in,s.
     715 block_id … (pc_block … pc) ≠ -1 →
    649716 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
    650717 ∃init_data,def_out.
     
    679746#src #dst #data #prog_in
    680747#init_regs #f_lbls #f_regs #props
    681 #pc #id #def_in #s
     748#pc #id #def_in #s #NEQ
    682749#H @('bind_inversion H) * #id' #def_in' -H
    683750#EQfif
     
    685752#H lapply (opt_eq_from_res ???? H) -H
    686753#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
    687 cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     754cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
    688755#a * #b ** #H1 #H2 #H3 %{a} %{b} %
    689756[ %{H1 H2}
Note: See TracChangeset for help on using the changeset viewer.