Changeset 1586


Ignore:
Timestamp:
Dec 5, 2011, 1:11:50 PM (8 years ago)
Author:
campbell
Message:

RTLabs structured traces: cost labels after jumps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1583 r1586  
    2020].
    2121
     22definition is_cost_label : statement → bool ≝
     23λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
     24
    2225definition RTLabs_cost : state → bool ≝
    2326λs. match s with
    2427[ State f fs m ⇒
    25     match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
    26     [ St_cost c l ⇒ true
    27     | _ ⇒ false
    28     ]
     28    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
    2929| _ ⇒ false
    3030].
     
    301301   between labels to catch loops for soundness (is this sufficient?). *)
    302302
    303 definition is_cost_label : statement → Prop ≝
    304 λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].
    305 
    306 let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
    307 match l return λl.All A P l → Prop with
    308 [ nil ⇒ λ_. True
    309 | cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
    310 ] H.
    311 
    312303definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
    313304λf,s. match s return λs. labels_present ? s → Prop with
    314305[ St_cond _ l1 l2 ⇒ λH.
    315     is_cost_label (lookup_present … (f_graph f) l1 ?)
    316     is_cost_label (lookup_present … (f_graph f) l2 ?)
     306    is_cost_label (lookup_present … (f_graph f) l1 ?) = true
     307    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
    317308| St_jumptable _ ls ⇒ λH.
    318     All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
     309    (* I did have a dependent version of All here, but it's a pain. *)
     310    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
    319311| _ ⇒ λ_. True
    320312]. whd in H;
     
    324316
    325317definition well_cost_labelled_fn : internal_function → Prop ≝
    326 λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
    327           well_cost_labelled_statement f s (f_closed f …)) ∧
    328     is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
    329 [ 2: @H | skip | cases (f_entry f) // ] qed.
     318λf. (∀l. ∀H:present … (f_graph f) l.
     319         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
     320    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
     321[ @lookup_lookup_present | cases (f_entry f) // ] qed.
    330322
    331323(* We need to ensure that any code we come across is well-cost-labelled.  We may
     
    356348| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
    357349] qed.
     350
     351lemma rtlabs_jump_inv : ∀s.
     352  RTLabs_classify s = cl_jump →
     353  ∃f,fs,m. s = State f fs m ∧
     354  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
     355  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
     356*
     357[ #f #fs #m #E
     358  %{f} %{fs} %{m} %
     359  [ @refl
     360  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
     361    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
     362    [ %1 %{A} %{B} %{C} @refl
     363    | %2 %{A} %{B} @refl
     364    ]
     365  ]
     366| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
     367| normalize #H8 #H9 #H10 #H11 #H12 destruct
     368] qed.
     369
     370lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
     371  eval_statement ge s = Value ??? 〈tr,s'〉 →
     372  well_cost_labelled_state s →
     373  RTLabs_classify s = cl_jump →
     374  RTLabs_cost s' = true.
     375#ge #s #tr #s' #EV #H #CL
     376cases (rtlabs_jump_inv s CL)
     377#fr * #fs * #m * #Es *
     378[ * #r * #l1 * #l2 #Estmt
     379  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
     380  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     381  >Estmt #LP whd in ⊢ (??%? → ?);
     382  (* replace with lemma on successors? *)
     383  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
     384  lapply (Hbody (next fr) (next_ok fr))
     385  generalize in ⊢ (???% → ?);
     386  >Estmt #LP'
     387  whd in ⊢ (% → ?);
     388  * #H1 #H2 [ @H1 | @H2 ]
     389| * #r * #ls #Estmt
     390  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
     391  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     392  >Estmt #LP whd in ⊢ (??%? → ?);
     393  (* replace with lemma on successors? *)
     394  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
     395  [ 2: (* later *)
     396  | *: #E destruct
     397  ]
     398  lapply (Hbody (next fr) (next_ok fr))
     399  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
     400  generalize in ⊢ (??(?%)? → ?);
     401  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     402  [ #E1 #E2 whd in E2:(??%?); destruct
     403  | #l' #E1 #E2 whd in E2:(??%?); destruct
     404    cases (All_nth ???? CP ? E1)
     405    #H1 #H2 @H2
     406  ]
     407] qed.
     408
    358409
    359410(* Don't need to know that labels break loops because we have termination. *)
     
    437488            ]
    438489        ] (refl ??)
    439     | cl_jump ⇒ λCL. ?
     490    | cl_jump ⇒ λCL.
     491        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 ???))
    440492    | cl_call ⇒ λCL. ?
    441493    | cl_return ⇒ λCL. ?
     
    456508|
    457509|
    458 |
     510| @(nth_is_return_notfn … TERMINATES) %2 @CL
     511| @(well_cost_labelled_state_step  … EV) //
     512| %{tr} @EV
     513| % whd in ⊢ (% → ?); >CL #E destruct
     514| @(well_cost_labelled_jump … EV) //
    459515|
    460516| @(nth_is_return_notfn … TERMINATES) %1 @CL
    461517| @(well_cost_labelled_state_step  … EV) //
    462518| %{tr} @EV
    463 |
     519| % whd in ⊢ (% → ?); >CL #E destruct
    464520| @CS
    465521| %{tr} @EV
Note: See TracChangeset for help on using the changeset viewer.