Changeset 1565 for src/RTLabs

Timestamp:

Nov 25, 2011, 5:30:20 PM (9 years ago)

Author:

campbell

Message:

Note that RTLabs ought to classify branches as "jumps" (in the
structural traces sense), and define a notion of well-cost-labelling.

File:

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

src/RTLabs/Traces.ma

@@ -5 +5 @@
 discriminator status_class.
 
-(* NB: we do not consider jumps in the traces of RTLabs programs. *)
+(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
+       will be added later (LTL → LIN). *)
 
 definition RTLabs_classify : state → status_class ≝
 λs. match s with
-[ State _ _ _ ⇒ cl_other
+[ State f _ _ ⇒
+    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
+    [ St_cond _ _ _ ⇒ cl_jump
+    | St_jumptable _ _ ⇒ cl_jump
+    | _ ⇒ cl_other
+    ]
 | Callstate _ _ _ _ _ ⇒ cl_call
 | Returnstate _ _ _ _ ⇒ cl_return
@@ -42 +48 @@
       ]).
 [ normalize in H; destruct
-| normalize in H; destruct
+| whd in H:(??%?);
+  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
+  normalize try #a try #b try #c try #d try #e try #g try #h destruct
 ] qed.
 
@@ -200 +208 @@
 inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
 | nir_step : ∀n,s,tr,s',depth,EX,trace.
-    RTLabs_classify s = cl_other →
+    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
     nth_is_return ge n depth s' trace →
     nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
@@ -259 +267 @@
 #ge #n #s #tr #s' #EX #trace #CLASS #H 
 inversion H
-[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
+[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
   -H2 destruct >H1 in CLASS; #E destruct
 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
@@ -268 +276 @@
 ] qed.
 
-(* Is the only well-labelledness fact I need here that the current state is
-   labelled?  That doesn't seem like it should be enough?
-   
-   Is this because the insertion of labels after jumps in LTL → LIN takes care
-   of the cost proof's needs?  Is the important thing that every branch is 
-   followed by a label?  The LTL → LIN stage then only adds labels at merges.
-    *)
+(* We require that labels appear after branch instructions and at the start of
+   functions. *)
+
+definition is_cost_label : statement → Prop ≝
+λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].
+
+let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
+match l return λl.All A P l → Prop with
+[ nil ⇒ λ_. True
+| cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
+] H. 
+
+definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
+λf,s. match s return λs. labels_present ? s → Prop with
+[ St_cond _ l1 l2 ⇒ λH.
+    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
+    is_cost_label (lookup_present … (f_graph f) l2 ?)
+| St_jumptable _ ls ⇒ λH.
+    All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
+| _ ⇒ λ_. True
+]. whd in H;
+[ @(proj1 … H)
+| @(proj2 … H)
+] qed.
+
+definition well_cost_labelled_fn : internal_function → Prop ≝
+λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
+          well_cost_labelled_statement f s (f_closed f …)) ∧
+    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
+[ 2: @H | skip | cases (f_entry f) // ] qed.
+
+(* We need to ensure that any code we come across is well-cost-labelled.  We may
+   get function code from either the global environment or the state. *)
+
+definition well_cost_labelled_ge : genv → Prop ≝
+λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f.
+
+definition well_cost_labelled_state : state → Prop ≝
+λs. match s with
+[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
+| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
+                          All ? (λf. well_cost_labelled_fn (func f)) fs
+| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
+].
+
 let rec make_label_return n ge s
-  (trace:flat_trace io_out io_in ge s)
-  (TERMINATES:nth_is_return ge n O s trace)
+  (trace: flat_trace io_out io_in ge s)
+  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
+  (STATE_COSTLABELLED: well_cost_labelled_state s)
+  (TERMINATES: nth_is_return ge n O s trace)
   : Σs'.Σremainder:flat_trace io_out io_in ge s'.
       trace_label_return (RTLabs_status ge) s s' ≝