Changeset 1563 for src/RTLabs

Timestamp:

Nov 25, 2011, 1:49:27 PM (8 years ago)

Author:

campbell

Message:

A little progress on constructing RTLabs structured traces.

File:

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

src/RTLabs/Traces.ma

@@ -7 +7 @@
 (* NB: we do not consider jumps in the traces of RTLabs programs. *)
 
-inductive RTLabs_classify : state → status_class → Prop ≝
-| rtla_other : ∀f,fs,m.    RTLabs_classify (State f fs m)        cl_other
-| rtla_call  : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call
-| rtla_ret   : ∀a,b,c,d.   RTLabs_classify (Returnstate a b c d) cl_return
-.
+definition RTLabs_classify : state → status_class ≝
+λs. match s with
+[ State _ _ _ ⇒ cl_other
+| Callstate _ _ _ _ _ ⇒ cl_call
+| Returnstate _ _ _ _ ⇒ cl_return
+].
 
 inductive RTLabs_stmt_cost : statement → Prop ≝
@@ -26 +27 @@
     state
     (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
-    RTLabs_classify
+    (λs,c. RTLabs_classify s = c)
     RTLabs_cost
     (λs,s'. match s with
       [ dp s p ⇒
-        match s return λs. RTLabs_classify s cl_call → ? with
+        match s return λs. RTLabs_classify s = cl_call → ? with
         [ Callstate fd args dst stk m ⇒
           λ_. match s' with
@@ -40 +41 @@
         ] p
       ]).
-inversion H try #a try #b try #c try #d try #e try #f destruct
-qed.
+[ normalize in H; destruct
+| normalize in H; destruct
+] qed.
 
 (* Before attempting to construct a structured trace, let's show that we can
@@ -164 +166 @@
 ] qed.
 
+(* Need a way to choose whether a called function terminates.  Then,
+     if the initial function terminates we generate a purely inductive structured trace,
+     otherwise we start generating the coinductive one, and on every function call
+       use the choice method again to decide whether to step over or keep going.
+
+Not quite what we need - have to decide on seeing each label whether we will see
+another or hit a non-terminating call?
+
+Also - need the notion of well-labelled in order to break loops.
+
+
+
+outline:
+
+ does function terminate?
+ - yes, get (bound on the number of steps until return), generate finite
+        structure using bound as termination witness
+ - no,  get (¬ bound on steps to return), start building infinite trace out of
+        finite steps.  At calls, check for termination, generate appr. form.
+
+generating the finite parts:
+
+We start with the status after the call has been executed; well-labelling tells
+us that this is a labelled state.  Now we want to generate a trace_label_return
+and also return the remainder of the flat trace.
+
+*)
+
+(* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
+   [s] we reach the return state for the current function.  [depth] performs
+   the call/return counting necessary for handling deeper function calls.
+   It should be zero at the top level. *)
+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 →
+    nth_is_return ge n depth s' trace →
+    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
+| nir_call : ∀n,s,tr,s',depth,EX,trace.
+    RTLabs_classify s = cl_call →
+    nth_is_return ge n (S depth) s' trace →
+    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
+| nir_ret : ∀n,s,tr,s',depth,EX,trace.
+    RTLabs_classify s = cl_return →
+    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.
+    RTLabs_classify s = cl_return →
+    nth_is_return ge O O s trace
+.
+
+discriminator nat.
+
+(* Find time until a nested call completes. *)
+lemma nth_is_return_down : ∀ge,n,depth,s,trace.
+  nth_is_return ge n (S depth) s trace →
+  ∃m. nth_is_return ge m depth s trace.
+#ge #n elim n
+(* It's impossible to run out of time... *)
+[ #depth #s #trace #H inversion H
+  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
+  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
+  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
+  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
+  ]
+| #n' #IH #depth #s #trace #H inversion H
+  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
+    cases (IH depth s1' trace1 ?)
+    [ #m' #H' %{(S m')} %1 //
+    | //
+    ]
+  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
+    cases (IH (S depth) s1' trace1 ?)
+    [ #m' #H' %{(S m')} %2 //
+    | //
+    ]
+  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
+    cases (depth1) in H2 ⊢ %;
+    [ #H2 %{O} %4 //
+    | #depth' #H2 cases (IH depth' s1' trace1 ?)
+      [ #m' #H' %{(S m')} %3 //
+      | //
+      ]
+    ]
+  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
+  ]
+] qed.
+
+lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
+  RTLabs_classify s = cl_call →
+  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
+  ∃m. nth_is_return ge m O s' trace.
+#ge #n #s #tr #s' #EX #trace #CLASS #H 
+inversion H
+[ #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
+  @nth_is_return_down //
+| #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
+] 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.
+    *)
+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)
+  : Σs'.Σremainder:flat_trace io_out io_in ge s'.
+      trace_label_return (RTLabs_status ge) s s' ≝
+?.