Ignore:
Timestamp:
Mar 16, 2013, 9:08:19 PM (7 years ago)
Author:
campbell
Message:

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2722 r2895  
    594594  find_funct_id F ge v = Some ? 〈f,id〉 →
    595595  ∃b. v = Vptr (mk_pointer b zero_offset) ∧
     596  find_symbol F ge id = Some ? b ∧
    596597  find_funct_ptr_id F ge b = Some ? 〈f,id〉.
    597598#F #ge #v #f #id whd in ⊢ (??%? → ?);
     
    600601[ #X #E normalize in E; destruct
    601602| #f' #FF #E whd in E:(??%?);
    602   cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} %{E1}
     603  cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} % [ %
     604  [ @E1
     605  | @symbol_of_block_rev
     606    @symbol_of_function_block_ok [ >FFP % #E2 destruct ]
     607    destruct %
     608  ] ]
    603609  whd in ⊢ (??%?);
    604610  generalize in match (refl ??);
     
    12971303#A #B #t #ge #ge' #RG #v #f #id #FFI
    12981304cases (find_funct_id_ptr ????? FFI)
    1299 #b * #E1 #FFPI
     1305#b * * #E1 #FS #FFPI
    13001306cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
    13011307lapply (rg_find_funct_ptr … RG … FFP) #FFP'
     
    13451351#tag #A #B #t #ge #ge' #RG #v #f #id #FFI
    13461352cases (find_funct_id_ptr ????? FFI)
    1347 #b * #E1 #FFPI
     1353#b * * #E1 #FS #FFPI
    13481354cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
    13491355cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g}
Note: See TracChangeset for help on using the changeset viewer.