Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (8 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.

File:
1 edited

Legend:

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