Changeset 2683 for src


Ignore:
Timestamp:
Feb 20, 2013, 6:41:46 PM (7 years ago)
Author:
tranquil
Message:

proof of properties of b_graph_program_transform (with an open axiom)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2681 r2683  
    44include "ASM/BitVectorTrie.ma".
    55include "joint/TranslateUtils.ma".
     6include "common/ExtraMonads.ma".
     7include "common/extraGlobalenvs.ma".
    68
    79record hw_register_env : Type[0] ≝
     
    164166qed.
    165167
    166 axiom b_graph_transform_program_props :
     168lemma symbols_match :
     169    ∀M:matching.∀initV,initW.
     170     (∀v,w. match_var_entry M v w →
     171      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     172    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     173    ∀MATCH:match_program … M p p'.
     174    symbols … (globalenv … initW p') = symbols … (globalenv … initV p).
     175* #A #B #V #W #match_fn #match_var #initV #initW #H
     176#p #p' * #Mvars #Mfn #Mmain
     177whd in match globalenv in ⊢ (???%); normalize nodelta
     178whd in match (globalenv_allocmem ????);
     179change with (add_globals ?????) in match (foldl ?????);
     180>(proj1 … (add_globals_match … initW … Mvars))
     181[ % |*:]
     182[ * #idr #v * #idr' #w #MVE %
     183  [ inversion MVE
     184    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
     185  | @(H … MVE)
     186  ]
     187| @(matching_fns_get_same_blocks … Mfn)
     188  #f #g @match_funct_entry_id
     189]
     190qed.
     191
     192lemma symbols_transf:
     193 ∀A,B,V,init.∀prog_in : program A V.
     194 ∀trans : ∀vars.A vars → B vars.
     195 let prog_out ≝ transform_program … prog_in trans in
     196 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
     197#A #B #V #iV #p #tf whd
     198@(symbols_match … (transform_program_match … tf ?))
     199#v0 #w0 * //
     200qed.
     201
     202definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝
     203λA,B,P,mA,mB.
     204∀p.
     205match lookup_opt … p mA with
     206[ Some a ⇒
     207  match lookup_opt … p mB with
     208  [ Some b ⇒ P a b
     209  | _ ⇒ False
     210  ]
     211| _ ⇒ match lookup_opt … p mB with
     212  [ Some _ ⇒ False
     213  | _ ⇒ True
     214  ]
     215].
     216
     217definition match_funct_map :
     218  ∀M : matching.
     219  ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝
     220  λM,vars.pm_P … (match_fundef M ?).
     221
     222axiom functions_match:
     223    ∀M:matching.∀initV,initW.
     224    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     225    ∀MATCH:match_program … M p p'.
     226    match_funct_map M ?
     227      (functions ? (globalenv ?? initV p))
     228      (functions ? (globalenv ?? initW p') ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
     229@sym_eq @(matching_vars … (mp_vars … MATCH)) qed.
     230
     231lemma functions_transf:
     232 ∀A,B,V,init.∀prog_in : program A V.
     233 ∀trans : ∀vars.A vars → B vars.
     234 let prog_out ≝ transform_program … prog_in trans in
     235 ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) =
     236 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
     237#A #B #V #iV #p #tf #n
     238lapply(functions_match … (transform_program_match … tf p) n) try @iV
     239cases (lookup_opt … n ?) [2: #f] normalize nodelta
     240generalize in ⊢ (match (???match % with [ _ ⇒ ?]) with [ _ ⇒ ? | _ ⇒ ? ] → ?);
     241#e >(K ?? e) normalize nodelta
     242cases (lookup_opt ???) [2,4: #f'] normalize nodelta
     243[2,3,4: * % ]
     244#EQ destruct %
     245qed.
     246
     247lemma symbol_for_block_transf :
     248 ∀A,B,V,init.∀prog_in : program A V.
     249 ∀trans : ∀vars.A vars → B vars.
     250 let prog_out ≝ transform_program … prog_in trans in
     251 ∀bl.
     252 symbol_for_block … (globalenv … init prog_out) bl =
     253 symbol_for_block … (globalenv … init prog_in) bl.
     254#A #B #V #iV #p #tf whd
     255#bl
     256whd in match symbol_for_block; normalize nodelta
     257>(symbols_match … (transform_program_match … tf ?))
     258[ % |*:]
     259#v #w * //
     260qed.
     261
     262include alias "common/Pointers.ma".
     263
     264lemma fetch_function_transf :
     265 ∀A,B,V,init.∀prog_in : program A V.
     266 ∀trans : ∀vars.A vars → B vars.
     267 let prog_out ≝ transform_program … prog_in trans in
     268 ∀bl.
     269 fetch_function … (globalenv … init prog_out) bl =
     270 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ;
     271 return 〈i, trans … f〉.
     272#A #B #V #init #prog_in #trans #bl
     273whd in match fetch_function; normalize nodelta
     274>(symbol_for_block_transf A B V init prog_in trans)
     275cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind
     276whd in match find_funct_ptr; normalize nodelta
     277whd in match (block_region (pi1 ?? bl));
     278cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try %
     279>(functions_transf A B V init prog_in trans p)
     280cases (lookup_opt ???) //
     281qed.
     282
     283lemma fetch_internal_function_transf :
     284 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
     285 ∀trans : ∀vars.A vars → B vars.
     286 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
     287 ∀bl.
     288 fetch_internal_function … (globalenv_noinit … prog_out) bl =
     289 ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ;
     290 return 〈i, trans … f〉.
     291#A #B #prog #trans #bl
     292 whd in match fetch_internal_function; normalize nodelta
     293>(fetch_function_transf … prog)
     294cases (fetch_function ???)
     295[ * #id * #f % | #e % ]
     296qed.
     297
     298include alias "utilities/binary/positive.ma".
     299
     300lemma pm_map_cases : ∀A.∀P : positive_map A → Prop.∀m : positive_map A.
     301((∀p.lookup_opt … p m = None ?) → P m) →
     302(∀p,v.lookup_opt … p m = Some ? v → P m) →
     303P m.
     304#A #P #m lapply P -P elim m -m
     305[ #P #H1 #_ @H1 #p % ]
     306* [2: #x ] #l #r #IHl #IHr #P #H1 #H2 [ @(H2 one x) % ]
     307@IHl [2: #p #v #EQ @(H2 (p0 p) v EQ) ]
     308#l_empty
     309@IHr [2: #p #v #EQ @(H2 (p1 p) v EQ) ]
     310#r_empty
     311@H1 * normalize //
     312qed.
     313
     314lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
     315(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
     316(∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) →
     317∀m.P m.
     318#A #P #H1 #H2 #m lapply H2 lapply H1 lapply P -P elim m -m
     319[ #P #H1 #_ @H1 #p % ]
     320#o #l #r #IHl #IHr #P #H1 #H2
     321@IHl #l'
     322[ #empty_l' @IHr #r'
     323  [ #empty_r' cases o [ @H1 * try #p normalize // ]
     324    #v change with (P (insert ? one v (pm_node ? (None ?) ??)))
     325    @H2 [ @H1 * try #p normalize // | % ]
     326  ]
     327]
     328#p #v #H #G
     329[ change with (P (insert ? (p1 p) v (pm_node ? ???)))
     330| change with (P (insert ? (p0 p) v (pm_node ? ???)))
     331] @H2 assumption
     332qed.
     333
     334include alias "basics/logic.ma".
     335include alias "common/PositiveMap.ma".
     336
     337lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A.
     338#A #B #impl * #Bf % #At @Bf @impl @At qed-.
     339
     340lemma b_graph_transform_program_find_funct_ptr :
    167341 ∀src,dst:sem_graph_params.
    168342 ∀data : ∀globals.joint_closed_internal_function src globals →
     
    172346 let src_genv ≝ globalenv_noinit ? prog_in in
    173347 let dst_genv ≝ globalenv_noinit ? prog_out in
    174  ∃init_regs : ident → list register.
    175  ∃f_lbls : ident → label → option (list label).
    176  ∃f_regs : ident → label → option (list register).
     348 ∃init_regs : block → list register.
     349 ∃f_lbls : block → label → option (list label).
     350 ∃f_regs : block → label → option (list register).
     351 ∀bl,def_in.
     352 find_funct_ptr … src_genv bl = return (Internal ? def_in) →
     353 ∃init_data,def_out.
     354 find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
     355 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     356 b_graph_translate_props src dst ? init_data (init_regs bl)
     357    def_in def_out (f_lbls bl) (f_regs bl).
     358#src #dst #data #prog_in
     359whd
     360letin prog_out ≝ (b_graph_transform_program … data prog_in)
     361letin src_genv ≝ (globalenv_noinit ? prog_in)
     362letin dst_genv ≝ (globalenv_noinit ? prog_out)
     363cut (∀p.lookup_opt ? p (functions ? dst_genv) =
     364     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
     365      (lookup_opt ? p (functions ? src_genv)))
     366[ @functions_transf ]
     367cases dst_genv #functs2 #nextf2 #symbols2 #H2
     368cases src_genv #functs1 #nextf1 #symbols1 #H1
     369lapply H2 lapply H1 lapply functs2
     370@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
     371[ #functs1_empty | #p #f #IH #p_not_in ]
     372#functs2 #H1 #H2 #transf
     373[ %{(λ_.[ ])} %{(λ_.λ_.None ?)} %{(λ_.λ_.None ?)}
     374  #bl #def_in #ABS @⊥ lapply ABS -ABS
     375  whd in match find_funct_ptr;
     376  normalize nodelta
     377  whd in match (block_region bl);
     378  cases (block_id bl) normalize nodelta
     379  [2,3: #p [2: >functs1_empty ]]
     380  normalize #ABS destruct
     381]
     382cases (IH (pm_set … p (None ?) functs2) ???)
     383[2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) -G @(eqb_elim b p)
     384  [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ]
     385  #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H
     386|3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) -G @(eqb_elim b p)
     387  [ #EQ destruct >lookup_opt_pm_set_hit #_ % ]
     388  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H
     389|4: #b @(eqb_elim b p)
     390  [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ]
     391  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf
     392  >(lookup_opt_insert_miss ? f b p … NEQ) %
     393]
     394-IH cases f in H1 transf; -f #f #H1 #transf
     395#init_regs * #f_lbls * #f_regs #props
     396[ (* internal *)
     397  letin upd ≝ (λA : Type[0].λf : block → A.
     398    λid.λv,id'.
     399    if eq_block id id' then v else f id')
     400  cases (pi2 ?? (b_graph_translate … (data … f) f))
     401  #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs *
     402  #inst_loc_data #loc_props
     403  letin bl ≝ (mk_block (neg p))
     404  %{(upd … init_regs bl loc_init_regs)}
     405  %{(upd … f_lbls bl loc_f_lbls)}
     406  %{(upd … f_regs bl loc_f_regs)}
     407| (* external, nothing changes *)
     408  %{init_regs}
     409  %{f_lbls}
     410  %{f_regs}
     411]
     412* #p' #def_in
     413whd in match find_funct_ptr; normalize nodelta
     414whd in match (block_region (mk_block p'));
     415cases p' -p' [2,3,5,6: #p' ] normalize nodelta
     416[1,3,5,6: #ABS normalize in ABS; destruct]
     417@(eqb_elim p' p) #pp' destruct
     418[1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ)
     419  %{loc_data} %
     420  [2: % [ % ]
     421    [ >transf >lookup_opt_insert_hit %
     422    |*: >eq_block_b_b assumption
     423    ]
     424  |]
     425|*: >(lookup_opt_insert_miss ???? functs1 … pp')
     426  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
     427  #EQ lapply (props (mk_block (neg p')) def_in EQ)
     428  whd in match find_funct_ptr; normalize nodelta
     429  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
     430]
     431qed.
     432
     433lemma b_graph_transform_program_fetch_internal_function :
     434 ∀src,dst:sem_graph_params.
     435 ∀data : ∀globals.joint_closed_internal_function src globals →
     436  bind_new register (b_graph_translate_data src dst globals).
     437 ∀prog_in : joint_program src.
     438 let prog_out ≝ b_graph_transform_program … data prog_in in
     439 let src_genv ≝ globalenv_noinit ? prog_in in
     440 let dst_genv ≝ globalenv_noinit ? prog_out in
     441 let code_block ≝ (Σbl.block_region bl = Code) in
     442 ∃init_regs : code_block → list register.
     443 ∃f_lbls : code_block → label → option (list label).
     444 ∃f_regs : code_block → label → option (list register).
    177445 ∀bl,id,def_in.
    178  fetch_internal_function ? src_genv bl = return 〈id, def_in〉 →
     446 fetch_internal_function src_genv bl = return 〈id, def_in〉 →
    179447 ∃init_data,def_out.
    180  fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧
    181  bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧
    182  b_graph_translate_props src dst ? init_data (init_regs id)
    183     def_in def_out (f_lbls id) (f_regs id).
     448 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     449 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     450 b_graph_translate_props src dst ? init_data (init_regs bl)
     451    def_in def_out (f_lbls bl) (f_regs bl).
     452#src #dst #data #prog_in
     453cases (b_graph_transform_program_find_funct_ptr src dst data prog_in)
     454#init_regs * #f_lbls * #f_regs #props
     455%{(λb.init_regs b)}
     456%{(λb.f_lbls b)}
     457%{(λb.f_regs b)}
     458#bl #id #def_in
     459#H @('bind_inversion H) * #id' * #def_in' -H
     460normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
     461@('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1
     462#H @('bind_inversion H) -H #def_in' #H
     463whd in ⊢ (??%%→?); #EQ destruct
     464cases (props … H)
     465#loc_data * #def_out ** #H1 #H2 #H3
     466%{loc_data} %{def_out}
     467%{H3} %{H2}
     468whd in match fetch_internal_function;
     469whd in match fetch_function; normalize nodelta
     470>symbol_for_block_transf >EQ1 >m_return_bind
     471>H1 %
     472qed.
     473
     474lemma b_graph_transform_program_fetch_statement :
     475 ∀src,dst:sem_graph_params.
     476 ∀data : ∀globals.joint_closed_internal_function src globals →
     477  bind_new register (b_graph_translate_data src dst globals).
     478 ∀prog_in : joint_program src.
     479 let prog_out ≝ b_graph_transform_program … data prog_in in
     480 let src_genv ≝ globalenv_noinit ? prog_in in
     481 let dst_genv ≝ globalenv_noinit ? prog_out in
     482 let code_block ≝ (Σbl.block_region bl = Code) in
     483 ∃init_regs : code_block → list register.
     484 ∃f_lbls : code_block → label → option (list label).
     485 ∃f_regs : code_block → label → option (list register).
     486 ∀pc,id,def_in,s.
     487 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     488 ∃init_data,def_out.
     489 let bl ≝ pc_block pc in
     490 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     491 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     492 b_graph_translate_props src dst ? init_data (init_regs bl)
     493    def_in def_out (f_lbls bl) (f_regs bl) ∧
     494 let l ≝ point_of_pc dst pc in
     495 ∃lbls,regs.
     496 f_lbls bl l = Some ? lbls ∧
     497 f_regs bl l = Some ? regs ∧
     498  match s with
     499  [ sequential s' nxt ⇒
     500    let block ≝
     501      if eq_identifier … (joint_if_entry … def_in) l then
     502        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
     503      else
     504        f_step … init_data l s' in
     505    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
     506  | final s' ⇒
     507    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
     508  | FCOND abs _ _ _ ⇒ Ⓧabs
     509  ].
     510#src #dst #data #prog_in
     511cases (b_graph_transform_program_fetch_internal_function src dst data prog_in)
     512#init_regs * #f_lbls * #f_regs #props
     513%{init_regs}
     514%{f_lbls}
     515%{f_regs}
     516#pc #id #def_in #s
     517#H @('bind_inversion H) * #id' #def_in' -H
     518#EQfif
     519#H @('bind_inversion H) -H #s
     520#H lapply (opt_eq_from_res ???? H) -H
     521#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
     522cases (props … EQfif)
     523#a * #b #H %{a} %{b} %{H}
     524cases H -H #_ #props'
     525@(multi_fetch_ok … props' … EQstmt_at)
     526qed.
Note: See TracChangeset for help on using the changeset viewer.