Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2645 r2722  
    425425qed.
    426426
     427
    427428lemma symbol_of_block_rev : ∀F,genv,b,id.
    428429  symbol_for_block F genv b = Some ? id →
     
    439440  | #_ *
    440441  ]
     442] qed.
     443
     444lemma symbol_of_block_rev' : ∀F,genv,b.
     445  symbol_for_block F genv b = None ? →
     446  find_funct_ptr F genv b = None ?.
     447#F #genv * * [ // | // ] #b #H
     448whd in ⊢ (??%?);
     449lapply (functions_inv ? genv b)
     450cases (lookup_opt F b ?) //
     451#f #H' cases (H' ?)
     452[ #id #E whd in H:(??%?);
     453  lapply (find_none ?? (symbols … genv) (λid,b'. eq_block (mk_block (neg b)) b') id (mk_block (neg b)))
     454  cases (find ????) in H ⊢ %;
     455  [ normalize #_ #H lapply (H (refl ??) E) >eqb_n_n *
     456  | * #id' #b' normalize #E destruct
     457  ]
     458| % #E destruct
    441459] qed.
    442460
     
    459477| * #id' #b' #_ normalize #_ #E destruct
    460478] qed.
     479
     480lemma symbol_of_function_block_ok : ∀F,ge,b,FFP,id.
     481  symbol_of_function_block F ge b FFP = id →
     482  symbol_for_block F ge b = Some ? id.
     483#F #ge #b #FFP #id whd in ⊢ (??%? → ?);
     484generalize in match (refl ? (symbol_for_block F ge b));
     485lapply (symbol_of_block_rev' F ge b)
     486cases (symbol_for_block F ge b) in ⊢ (% → ???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     487[ #H @⊥ >(H (refl ??)) in FFP; * /2/
     488| #id' #_ #E normalize in ⊢ (% → ?); #E' destruct @E
     489] qed.
     490
     491definition symbol_of_function_block' : ∀F,ge,b,f. find_funct_ptr F ge b = Some ? f → ident ≝
     492λF,ge,b,f,FFP. symbol_of_function_block F ge b ?.
     493>FFP % #E destruct
     494qed.
     495
     496definition find_funct_ptr_id : ∀F:Type[0]. genv_t F → block → option (F × ident) ≝
     497λF:Type[0].λge:genv_t F.λb:block.
     498match find_funct_ptr F ge b return λx:option F. ? = x → option (F × ident) with
     499[ None ⇒ λ_. None ?
     500| Some f ⇒ λFFP. Some ? 〈f,symbol_of_function_block' F ge b f FFP〉
     501] (refl ??).
     502
     503lemma find_funct_ptr_id_drop : ∀F,ge,b,f,id.
     504  find_funct_ptr_id F ge b = Some ? 〈f,id〉 →
     505  find_funct_ptr F ge b = Some ? f.
     506#F #ge #b #f #id whd in ⊢ (??%? → ?);
     507generalize in match (refl ??);
     508cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %);
     509[ #X #E normalize in E; destruct
     510| #f' #ID #E whd in E:(??%?); destruct %
     511] qed.
     512
     513coercion ffpi_drop :
     514  ∀F,ge,b,f,id.
     515  ∀FFP:find_funct_ptr_id F ge b = Some ? 〈f,id〉.
     516  find_funct_ptr F ge b = Some ? f ≝ find_funct_ptr_id_drop
     517  on _FFP:eq (option ?) ?? to eq (option ?) ??.
     518
     519lemma find_funct_ptr_id_inv : ∀F,ge,b,f,id.
     520  find_funct_ptr_id F ge b = Some ? 〈f,id〉 →
     521  find_funct_ptr F ge b = Some ? f ∧
     522  symbol_for_block F ge b = Some ? id.
     523#F #ge #b #f #id whd in ⊢ (??%? → ?);
     524generalize in match (refl ??);
     525cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %);
     526[ #X #E normalize in E; destruct
     527| #f' #FFP #E whd in E:(??%?); %
     528  [ destruct %
     529  | @(symbol_of_function_block_ok F ge b ? id)
     530    [ >FFP % #E' destruct
     531    | destruct %
     532    ]
     533  ]
     534] qed.
     535
     536lemma make_find_funct_ptr_id : ∀F,ge,b,f,id.
     537  find_funct_ptr F ge b = Some ? f →
     538  symbol_for_block F ge b = Some ? id →
     539  find_funct_ptr_id F ge b = Some ? 〈f,id〉.
     540#F #ge #b #f #id #FFP #SYM
     541whd in ⊢ (??%?); generalize in match (refl ??);
     542>FFP in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?);
     543#FFP' whd in ⊢ (??%?);
     544@eq_f @eq_f
     545whd in ⊢ (??%?);
     546generalize in match (refl ? (symbol_for_block F ge b));
     547>SYM in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?);
     548#SYM' whd in ⊢ (??%?); %
     549qed.
     550
     551definition symbol_of_function_val : ∀F,ge,v. find_funct F ge v ≠ None ? → ident ≝
     552λF,ge,v.
     553match v return λv. find_funct F ge v ≠ None ? → ident with
     554[ Vptr p ⇒ λH. symbol_of_function_block F ge (pblock p) ?
     555| _ ⇒ λH. ⊥
     556].
     557try (cases H #H' cases (H' (refl ??)))
     558lapply H
     559whd in match (find_funct ???);
     560@eq_offset_elim
     561[ #_ #H' @H'
     562| #X * #H' cases (H' (refl ??))
     563] qed.
     564
     565definition symbol_of_function_val' : ∀F,ge,v,f. find_funct F ge v = Some ? f → ident ≝
     566λF,ge,v,f,FF. symbol_of_function_val F ge v ?.
     567>FF % #E destruct
     568qed.
     569
     570definition find_funct_id : ∀F:Type[0]. genv_t F → val → option (F × ident) ≝
     571λF:Type[0].λge:genv_t F.λv:val.
     572match find_funct F ge v return λx:option F. ? = x → option (F × ident) with
     573[ None ⇒ λ_. None ?
     574| Some f ⇒ λFF. Some ? 〈f,symbol_of_function_val' F ge v f FF〉
     575] (refl ??).
     576
     577lemma find_funct_id_drop : ∀F,ge,v,f,id.
     578  find_funct_id F ge v = Some ? 〈f,id〉 →
     579  find_funct F ge v = Some ? f.
     580#F #ge #v #f #id whd in ⊢ (??%? → ?);
     581generalize in match (refl ??);
     582cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     583[ #X #E normalize in E; destruct
     584| #f' #ID #E whd in E:(??%?); destruct assumption
     585] qed.
     586
     587coercion ffi_drop :
     588  ∀F,ge,v,f,id.
     589  ∀FF:find_funct_id F ge v = Some ? 〈f,id〉.
     590  find_funct F ge v = Some ? f ≝ find_funct_id_drop
     591  on _FF:eq (option ?) ?? to eq (option ?) ??.
     592
     593lemma find_funct_id_ptr : ∀F,ge,v,f,id.
     594  find_funct_id F ge v = Some ? 〈f,id〉 →
     595  ∃b. v = Vptr (mk_pointer b zero_offset) ∧
     596  find_funct_ptr_id F ge b = Some ? 〈f,id〉.
     597#F #ge #v #f #id whd in ⊢ (??%? → ?);
     598generalize in match (refl ??);
     599cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %);
     600[ #X #E normalize in E; destruct
     601| #f' #FF #E whd in E:(??%?);
     602  cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} %{E1}
     603  whd in ⊢ (??%?);
     604  generalize in match (refl ??);
     605  >FFP in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?);
     606  #FFP' whd in ⊢ (??%?); <E
     607  @eq_f @eq_f >E1 in FF E ⊢ %; #FF #E %
     608] qed.
     609
     610lemma find_funct_ptr_id_conv : ∀F,ge,b,f,id.
     611  find_funct_ptr_id F ge b = Some ? 〈f,id〉 →
     612  find_funct_id F ge (Vptr (mk_pointer b zero_offset)) = Some ? 〈f,id〉.
     613#F #ge * * [2,3:#b] #f #id
     614whd in ⊢ (??%? → ??%?); #E destruct
     615@E
     616qed.
    461617
    462618(*
     
    9431099qed.
    9441100
     1101lemma symbols_match:
     1102    ∀M:matching.
     1103    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     1104    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     1105    match_program … M p p' →
     1106    symbols ? (globalenv … initW p') = symbols ? (globalenv … initV p).
     1107* #A #B #V #W #match_fun #match_var #initV #initW #initsize
     1108* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain
     1109whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     1110whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     1111change with (add_globals ?????) in match (foldl ?????);
     1112change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
     1113@sym_eq
     1114@(proj1 … (add_globals_match … Mvars))
     1115[ @(matching_fns_get_same_blocks … Mfns)
     1116  #f #g @match_funct_entry_id
     1117| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
     1118] qed.
     1119
    9451120lemma
    9461121  find_symbol_match:
     
    9511126    ∀s: ident.
    9521127    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
    953 * #A #B #V #W #match_fun #match_var #initV #initW #initsize
    954 * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
    955 whd in ⊢ (??%%);
    956 @sym_eq
    957 @(eq_f ??(λx. lookup SymbolTag block x s))
    958 whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
    959 whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
    960 change with (add_globals ?????) in match (foldl ?????);
    961 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
    962 @(proj1 … (add_globals_match … Mvars))
    963 [ @(matching_fns_get_same_blocks … Mfns)
    964   #f #g @match_funct_entry_id
    965 | * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
    966 ] qed.
     1128#M #initV #initW #initsize #p1 #p2 #MATCH #s
     1129whd in ⊢ (??%%); >(symbols_match M … initsize … MATCH) %
     1130qed.
    9671131 
    9681132lemma
     
    11181282  rg_find_symbol: ∀s.
    11191283    find_symbol … ge s = find_symbol … ge' s;
     1284  rg_symbol_for : ∀b.
     1285    symbol_for_block … ge b = symbol_for_block … ge' b;
    11201286  rg_find_funct: ∀v,f.
    11211287    find_funct … ge v = Some ? f →
     
    11261292}.
    11271293
     1294lemma rg_find_funct_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀v,f,id.
     1295  find_funct_id … ge v = Some ? 〈f,id〉 →
     1296  find_funct_id … ge' v = Some ? 〈t f,id〉.
     1297#A #B #t #ge #ge' #RG #v #f #id #FFI
     1298cases (find_funct_id_ptr ????? FFI)
     1299#b * #E1 #FFPI
     1300cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1301lapply (rg_find_funct_ptr … RG … FFP) #FFP'
     1302>(rg_symbol_for … RG b) in SYM; #SYM'
     1303lapply (make_find_funct_ptr_id … FFP' SYM')
     1304>E1 @find_funct_ptr_id_conv
     1305qed.
     1306
     1307lemma rg_find_funct_ptr_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀b,f,id.
     1308  find_funct_ptr_id … ge b = Some ? 〈f,id〉 →
     1309  find_funct_ptr_id … ge' b = Some ? 〈t f,id〉.
     1310#A #B #t #ge #ge' #RG #b #f #id #FFPI
     1311cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1312lapply (rg_find_funct_ptr … RG … FFP) #FFP'
     1313>(rg_symbol_for … RG b) in SYM; #SYM'
     1314@(make_find_funct_ptr_id … FFP' SYM')
     1315qed.
     1316
     1317
     1318
    11281319theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
    11291320  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
    11301321#A #B #V #iV #p #tf %
    11311322[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
     1323| #b whd in ⊢ (??%%); >(symbols_match … (transform_program_match … tf ?))
     1324  [ % | #v #w * #id #r #v1 #v2 #E destruct % | skip ]
    11321325| @(find_funct_transf A B V iV tf p)
    11331326| @(find_funct_ptr_transf A B V iV p tf)
     
    11371330  rgg_find_symbol: ∀s.
    11381331    find_symbol … ge s = find_symbol … ge' s;
     1332  rgg_symbol_for : ∀b.
     1333    symbol_for_block … ge b = symbol_for_block … ge' b;
    11391334  rgg_find_funct_ptr: ∀b,f.
    11401335    find_funct_ptr … ge b = Some ? f →
     
    11451340}.
    11461341
     1342lemma rgg_find_funct_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀v,f,id.
     1343  find_funct_id … ge v = Some ? 〈f,id〉 →
     1344  ∃g. find_funct_id … ge' v = Some ? 〈\fst (t g f),id〉.
     1345#tag #A #B #t #ge #ge' #RG #v #f #id #FFI
     1346cases (find_funct_id_ptr ????? FFI)
     1347#b * #E1 #FFPI
     1348cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1349cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g}
     1350>(rgg_symbol_for … RG b) in SYM; #SYM'
     1351lapply (make_find_funct_ptr_id … FFP' SYM')
     1352>E1 @find_funct_ptr_id_conv
     1353qed.
     1354
     1355lemma rgg_find_funct_ptr_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀b,f,id.
     1356  find_funct_ptr_id … ge b = Some ? 〈f,id〉 →
     1357  ∃g. find_funct_ptr_id … ge' b = Some ? 〈\fst (t g f),id〉.
     1358#tag #A #B #t #ge #ge' #RG #b #f #id #FFPI
     1359cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1360cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g}
     1361>(rgg_symbol_for … RG b) in SYM; #SYM'
     1362@(make_find_funct_ptr_id … FFP' SYM')
     1363qed.
     1364
    11471365include "utilities/extra_bool.ma".
    11481366
     
    11521370[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
    11531371  #v #w * //
     1372| #b whd in ⊢ (??%%); >(symbols_match … (transform_program_gen_match … tf p))
     1373  [ % | #v #w * #id #r #v1 #v2 #E destruct % | skip ]
    11541374| #b #f #FFP
    11551375  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
Note: See TracChangeset for help on using the changeset viewer.