Changeset 2677 for src/RTLabs/RTLabs_abstract.ma

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:

• src/RTLabs/RTLabs_abstract.ma (modified) (9 diffs)

src/RTLabs/RTLabs_abstract.ma

@@ -35 +35 @@
   match state with
   [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
-  | Callstate fd _ _ fs _ ⇒
+  | Callstate _ fd _ _ fs _ ⇒
       match fn_stack with
       [ nil ⇒ False
@@ -58 +58 @@
   eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝
 λge,s,s',t,EX. mk_RTLabs_ext_state ge s' 
- (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)
+ (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)
  ?.
 cases s' in EX ⊢ %;
@@ -67 +67 @@
     | @M2 ]
   | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
-  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
+  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     whd cases stk in mtc ⊢ %; [ * ]
     #hd #tl #H @H
@@ -76 +76 @@
   | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
   ]
-| -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
+| -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
   whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
   [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
-  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
+  | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
     [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
@@ -111 +111 @@
     | _ ⇒ cl_other
     ]
-| Callstate _ _ _ _ _ ⇒ cl_call
+| Callstate _ _ _ _ _ _ ⇒ cl_call
 | Returnstate _ _ _ _ ⇒ cl_return
 | Finalstate _ ⇒ cl_other
@@ -179 +179 @@
 match s' return λs'. Ras_Fn_Match ? s' ? → ? with
 [ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
-| 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 ]
+| 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 ]
 | Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
 | Finalstate _ ⇒ λmtc. rapc_fin
@@ -206 +206 @@
   [ mk_Sig s p ⇒
     match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
-    [ Callstate fd args dst stk m ⇒
+    [ Callstate _ fd args dst stk m ⇒
       λ_. match s' with
       [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
@@ -233 +233 @@
     [ mk_RTLabs_ext_state s' stk mtc0 ⇒
       match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
-      [ Callstate fd _ _ _ _ ⇒
+      [ Callstate _ fd _ _ _ _ ⇒
         match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
         [ nil ⇒ λmtc. ⊥
@@ -304 +304 @@
   try (% #E' destruct)
   cases (NONE ?) assumption
-| #fd #args #dst #fs #m #stk #mtc %
+| #vf #fd #args #dst #fs #m #stk #mtc %
   [ #E normalize in E; destruct
   | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);