Changeset 1565 for src/RTLabs


Ignore:
Timestamp:
Nov 25, 2011, 5:30:20 PM (8 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1563 r1565  
    55discriminator status_class.
    66
    7 (* NB: we do not consider jumps in the traces of RTLabs programs. *)
     7(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
     8       will be added later (LTL → LIN). *)
    89
    910definition RTLabs_classify : state → status_class ≝
    1011λs. match s with
    11 [ State _ _ _ ⇒ cl_other
     12[ State f _ _ ⇒
     13    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
     14    [ St_cond _ _ _ ⇒ cl_jump
     15    | St_jumptable _ _ ⇒ cl_jump
     16    | _ ⇒ cl_other
     17    ]
    1218| Callstate _ _ _ _ _ ⇒ cl_call
    1319| Returnstate _ _ _ _ ⇒ cl_return
     
    4248      ]).
    4349[ normalize in H; destruct
    44 | normalize in H; destruct
     50| whd in H:(??%?);
     51  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
     52  normalize try #a try #b try #c try #d try #e try #g try #h destruct
    4553] qed.
    4654
     
    200208inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
    201209| nir_step : ∀n,s,tr,s',depth,EX,trace.
    202     RTLabs_classify s = cl_other
     210    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump
    203211    nth_is_return ge n depth s' trace →
    204212    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
     
    259267#ge #n #s #tr #s' #EX #trace #CLASS #H
    260268inversion H
    261 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
     269[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
    262270  -H2 destruct >H1 in CLASS; #E destruct
    263271| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
     
    268276] qed.
    269277
    270 (* Is the only well-labelledness fact I need here that the current state is
    271    labelled?  That doesn't seem like it should be enough?
    272    
    273    Is this because the insertion of labels after jumps in LTL → LIN takes care
    274    of the cost proof's needs?  Is the important thing that every branch is
    275    followed by a label?  The LTL → LIN stage then only adds labels at merges.
    276     *)
     278(* We require that labels appear after branch instructions and at the start of
     279   functions. *)
     280
     281definition is_cost_label : statement → Prop ≝
     282λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].
     283
     284let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
     285match l return λl.All A P l → Prop with
     286[ nil ⇒ λ_. True
     287| cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
     288] H.
     289
     290definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
     291λf,s. match s return λs. labels_present ? s → Prop with
     292[ St_cond _ l1 l2 ⇒ λH.
     293    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
     294    is_cost_label (lookup_present … (f_graph f) l2 ?)
     295| St_jumptable _ ls ⇒ λH.
     296    All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
     297| _ ⇒ λ_. True
     298]. whd in H;
     299[ @(proj1 … H)
     300| @(proj2 … H)
     301] qed.
     302
     303definition well_cost_labelled_fn : internal_function → Prop ≝
     304λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
     305          well_cost_labelled_statement f s (f_closed f …)) ∧
     306    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
     307[ 2: @H | skip | cases (f_entry f) // ] qed.
     308
     309(* We need to ensure that any code we come across is well-cost-labelled.  We may
     310   get function code from either the global environment or the state. *)
     311
     312definition well_cost_labelled_ge : genv → Prop ≝
     313λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f.
     314
     315definition well_cost_labelled_state : state → Prop ≝
     316λs. match s with
     317[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
     318| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
     319                          All ? (λf. well_cost_labelled_fn (func f)) fs
     320| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
     321].
     322
    277323let rec make_label_return n ge s
    278   (trace:flat_trace io_out io_in ge s)
    279   (TERMINATES:nth_is_return ge n O s trace)
     324  (trace: flat_trace io_out io_in ge s)
     325  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     326  (STATE_COSTLABELLED: well_cost_labelled_state s)
     327  (TERMINATES: nth_is_return ge n O s trace)
    280328  : Σs'.Σremainder:flat_trace io_out io_in ge s'.
    281329      trace_label_return (RTLabs_status ge) s s' ≝
Note: See TracChangeset for help on using the changeset viewer.