Changeset 2677 for src/correctness.ma


Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (7 years ago)
Author:
campbell
Message:

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2623 r2677  
    4747definition stack_cost_T ≝ ident → nat.
    4848
    49 axiom Clight_stack_cost :
     49(* Again, in principle we can use the fact that the state must be a call and
     50   also show some relevant invariants about call states, but we go with the
     51   easier option of returning zero elsewhere. *)
     52definition Clight_stack_cost :
    5053  stack_cost_T →
     54  cl_genv →
    5155  ∀s:Clight_state.
    52   match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] →
    53   nat.
     56  match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
     57  nat ≝
     58λcost,ge,s,H.
     59match s with
     60[ Callstate v _ _ _ _ ⇒
     61  match v with [ Vptr p ⇒ match symbol_for_block … ge (pblock p) with [ Some id ⇒ cost id | _ ⇒ 0 ] | _ ⇒ 0 ]
     62| _ ⇒ 0
     63].
    5464
    5565definition Clight_pcs : preclassified_system ≝
     
    5868  (λ_.Clight_labelled)
    5969  (λ_.Clight_classify)
    60   (λf,g. Clight_stack_cost f).
     70  Clight_stack_cost.
    6171
    6272(* From measurable on Clight, we will end up with an RTLabs flat trace where
Note: See TracChangeset for help on using the changeset viewer.