Changeset 1583 for src/RTLabs/Traces.ma

Timestamp:

Dec 2, 2011, 1:02:08 PM (8 years ago)

Author:

campbell

Message:

More on RTLabs structured traces.
Fixed mistake in structure trace definition that made it unhabitable.

File:

• src/RTLabs/Traces.ma (modified) (10 diffs)

src/RTLabs/Traces.ma

@@ -20 +20 @@
 ].
 
-inductive RTLabs_stmt_cost : statement → Prop ≝
-| stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l).
-
-inductive RTLabs_cost : state → Prop ≝
-| cost_instr : ∀f,fs,m.
-    RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) →
-    RTLabs_cost (State f fs m).
+definition RTLabs_cost : state → bool ≝
+λs. match s with
+[ State f fs m ⇒
+    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
+    [ St_cost c l ⇒ true
+    | _ ⇒ false
+    ]
+| _ ⇒ false
+].
 
 definition RTLabs_status : genv → abstract_status ≝
@@ -34 +36 @@
     (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
     (λs,c. RTLabs_classify s = c)
-    RTLabs_cost
+    (λs. RTLabs_cost s = true)
     (λs,s'. match s with
       [ dp s p ⇒
@@ -219 +221 @@
     nth_is_return ge n depth s' trace →
     nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
-| nir_base : ∀s,trace.
+    (* Note that we require the ability to make a step after the return (this
+       corresponds to somewhere that will be guaranteed to be a label at the
+       end of the compilation chain). *)
+| nir_base : ∀s,tr,s',EX,trace.
     RTLabs_classify s = cl_return →
-    nth_is_return ge O O s trace
+    nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
 .
 
@@ -273 +278 @@
 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
   -H2 destruct
-| #s1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
+| #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
+] qed.
+
+lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace.
+  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
+  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
+  nth_is_return ge (pred n) O s' trace.
+#ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM
+[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
+| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct
+| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
+| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct
+| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct //
+| #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct
+| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
+| #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
 ] qed.
 
@@ -313 +333 @@
 
 definition well_cost_labelled_ge : genv → Prop ≝
-λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f.
+λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
 
 definition well_cost_labelled_state : state → Prop ≝
@@ -322 +342 @@
 | Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
 ].
+
+lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
+  eval_statement ge s = Value ??? 〈tr,s'〉 →
+  well_cost_labelled_ge ge →
+  well_cost_labelled_state s →
+  well_cost_labelled_state s'.
+#ge #s #tr' #s' #EV cases (eval_perserves … EV)
+[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
+| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
+| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
+| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
+| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
+| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
+] qed.
 
 (* Don't need to know that labels break loops because we have termination. *)
@@ -349 +383 @@
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
-  (STATEMENT_COSTLABEL: RTLabs_cost s)              (* current statement is a cost label *)
+  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
   (TERMINATES: nth_is_return ge n O s trace)
   : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
@@ -371 +405 @@
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
-  (STATEMENT_COSTLABEL: RTLabs_cost s)              (* current statement is a cost label *)
+  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
   (TERMINATES: nth_is_return ge n O s trace)
   : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
@@ -387 +421 @@
   (TERMINATES: nth_is_return ge n O s trace)
   : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
-match trace return λs,trace. nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with
-[ ft_stop st FINAL ⇒ λTERMINATES. ?
-| ft_step start tr next EV trace' ⇒ λTERMINATES. ?
-| ft_wrong start m EV ⇒ λTERMINATES. ⊥
-] TERMINATES.
+match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with
+[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
+| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
+    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
+    [ cl_other ⇒ λCL.
+        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
+        [ true ⇒ λCS.
+            mk_make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???))
+        | false ⇒ λCS.
+            let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
+            match new_trace … r with
+            [ dp ends trc ⇒
+                replace_new_trace ??? r
+                  (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??))
+            ]
+        ] (refl ??)
+    | cl_jump ⇒ λCL. ?
+    | cl_call ⇒ λCL. ?
+    | cl_return ⇒ λCL. ?
+    ] (refl ? (RTLabs_classify start))
+| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
+] STATE_COSTLABELLED TERMINATES.
 
 [ //
@@ -405 +456 @@
 |
 |
+|
+|
+| @(nth_is_return_notfn … TERMINATES) %1 @CL
+| @(well_cost_labelled_state_step  … EV) //
+| %{tr} @EV
+|
+| @CS
+| %{tr} @EV
+| @CL
+| % whd in ⊢ (% → ?); >CS #E destruct
+| @(well_cost_labelled_state_step … EV) //
+| @(nth_is_return_notfn … TERMINATES) %1 @CL
 | inversion TERMINATES
   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
   | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
   | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
-  | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 -TERMINATES destruct
+  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
+  ]
+|
+
+
   
-(* Now we're in trouble - if we're at the end of the function we don't have the
-   required guarantee that we can make another step.  In particular, there isn't
-   one at the end of the program. *)
+(* FIXME: there's trouble at the end of the program because we can't make a step
+   away from the final return. *)