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/RTLabs/RTLabs_abstract.ma

    r2757 r2895  
    3535  match state with
    3636  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
    37   | Callstate _ fd _ _ fs _ ⇒
     37  | Callstate fid fd _ _ fs _ ⇒
    3838      match fn_stack with
    3939      [ nil ⇒ False
    40       | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
    41         All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
     40      | cons h t ⇒
     41          find_symbol … ge fid = Some ? h ∧
     42          find_funct_ptr ? ge h = Some ? fd ∧
     43          All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
    4244      ]
    4345  | Returnstate _ _ fs _ ⇒
     
    6971  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    7072    whd cases stk in mtc ⊢ %; [ * ]
    71     #hd #tl #H @H
     73    #hd #tl * * /3/
    7274  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    7375  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
     
    7678  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    7779  ]
    78 | -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
     80| -s' #fid #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
    7981  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    8082  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     
    232234    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
    233235    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
    235       [ Callstate _ fd _ _ _ _ ⇒
    236         match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
    237         [ nil ⇒ λmtc. ⊥
    238         | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?
    239         ]
    240       | State f _ _ ⇒ λ_. λH.⊥
    241       | _ ⇒ λ_. λH.⊥
    242       ] mtc0
     236      match s' return λs'. RTLabs_classify s' = cl_call → ident with
     237      [ Callstate fid _ _ _ _ _ ⇒ λ_. fid
     238      | State f _ _ ⇒ λH.⊥
     239      | _ ⇒ λH.⊥
     240      ]
    243241    ] p
    244242  ].
     
    246244  cases (next_instruction f) in H;
    247245  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    248 | 4,5: normalize in H; destruct (H)
    249 | cases mtc
    250 | cases mtc #FFP #_ >FFP % #E destruct (E)
     246| *: normalize in H; destruct (H)
    251247] qed.
    252248
Note: See TracChangeset for help on using the changeset viewer.