Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (7 years ago)
Author:
campbell
Message:

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_abstract.ma

    r2601 r2677  
    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 _ fd _ _ fs _ ⇒
    3838      match fn_stack with
    3939      [ nil ⇒ False
     
    5858  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝
    5959λge,s,s',t,EX. mk_RTLabs_ext_state ge s'
    60  (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
     60 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
    6161 ?.
    6262cases s' in EX ⊢ %;
     
    6767    | @M2 ]
    6868  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
    69   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     69  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    7070    whd cases stk in mtc ⊢ %; [ * ]
    7171    #hd #tl #H @H
     
    7676  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    7777  ]
    78 | -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
     78| -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
    7979  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    8080  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    81   | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     81  | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    8282    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
    8383    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     
    111111    | _ ⇒ cl_other
    112112    ]
    113 | Callstate _ _ _ _ _ ⇒ cl_call
     113| Callstate _ _ _ _ _ _ ⇒ cl_call
    114114| Returnstate _ _ _ _ ⇒ cl_return
    115115| Finalstate _ ⇒ cl_other
     
    179179match s' return λs'. Ras_Fn_Match ? s' ? → ? with
    180180[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
    181 | Callstate _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
     181| Callstate _ _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
    182182| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
    183183| Finalstate _ ⇒ λmtc. rapc_fin
     
    206206  [ mk_Sig s p ⇒
    207207    match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
    208     [ Callstate fd args dst stk m ⇒
     208    [ Callstate _ fd args dst stk m ⇒
    209209      λ_. match s' with
    210210      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
     
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234234      match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
    235       [ Callstate fd _ _ _ _ ⇒
     235      [ Callstate _ fd _ _ _ _ ⇒
    236236        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
    237237        [ nil ⇒ λmtc. ⊥
     
    304304  try (% #E' destruct)
    305305  cases (NONE ?) assumption
    306 | #fd #args #dst #fs #m #stk #mtc %
     306| #vf #fd #args #dst #fs #m #stk #mtc %
    307307  [ #E normalize in E; destruct
    308308  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
Note: See TracChangeset for help on using the changeset viewer.