Changeset 175 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Oct 13, 2010, 12:19:22 PM (10 years ago)
Author:
campbell
Message:

Add cost labels, with the semantics that the label is added to the
event trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r156 r175  
    2020include "Coqlib.ma".
    2121include "Errors.ma".
     22include "CostLabel.ma".
    2223
    2324(* * * Abstract syntax *)
     
    189190  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
    190191  | Esizeof: type → expr_descr         (**r size of a type *)
    191   | Efield: expr → ident → expr_descr. (**r access to a member of a struct or union *)
     192  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
     193  | Ecost: costlabel → expr → expr_descr.
    192194
    193195(* * Extract the type part of a type-annotated Clight expression. *)
     
    220222  | Slabel : label → statement → statement
    221223  | Sgoto : label → statement
     224  | Scost : costlabel → statement → statement
    222225
    223226with labeled_statements : Type ≝            (**r cases of a [switch] *)
     
    241244  (Sla:∀l,s. P s → P (Slabel l s))
    242245  (Sgo:∀l. P (Sgoto l))
     246  (Scs:∀l,s. P s → P (Scost l s))
    243247  (LSd:∀s. P s → Q (LSdefault s))
    244248  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     
    249253| Scall eo e args ⇒ Sca eo e args
    250254| Ssequence s1 s2 ⇒ Ssq s1 s2
    251     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
    252     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     255    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     256    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    253257| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    254     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
    255     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     258    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     259    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    256260| Swhile e s ⇒ Swh e s
    257     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    258262| Sdowhile e s ⇒ Sdo e s
    259     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     263    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    260264| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
    261     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
    262     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
    263     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s3)
     265    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
     266    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
     267    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
    264268| Sbreak ⇒ Sbr
    265269| Scontinue ⇒ Sco
    266270| Sreturn eo ⇒ Sre eo
    267271| Sswitch e ls ⇒ Ssw e ls
    268     (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc ls)
     272    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
    269273| Slabel l s ⇒ Sla l s
    270     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     274    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    271275| Sgoto l ⇒ Sgo l
     276| Scost l s ⇒ Scs l s
     277    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    272278]
    273279and labeled_statements_ind2
     
    287293  (Sla:∀l,s. P s → P (Slabel l s))
    288294  (Sgo:∀l. P (Sgoto l))
     295  (Scs:∀l,s. P s → P (Scost l s))
    289296  (LSd:∀s. P s → Q (LSdefault s))
    290297  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     
    292299match ls with
    293300[ LSdefault s ⇒ LSd s
    294     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     301    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    295302| LScase i s t ⇒ LSc i s t
    296     (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
    297     (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc t)
     303    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
     304    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
    298305].
    299306
    300 ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo.
    301   statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo
     307ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
     308  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
    302309  (λ_,_. I) (λ_,_,_,_,_.I).
    303310
Note: See TracChangeset for help on using the changeset viewer.