Changeset 2328


Ignore:
Timestamp:
Sep 10, 2012, 6:18:56 PM (7 years ago)
Author:
campbell
Message:

Cut down the notion of a Clight labelled state to those where we pick out
the cost label, rather than allowing it to appear in the middle of some
complex computation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/abstract.ma

    r2326 r2328  
    11include "Clight/Csem.ma".
    22
    3 (* Definitions about Clight syntax and semantics for use in overall results. *)
    4 
    5 let rec any_expr (P:expr → bool) (e:expr) on e : bool ≝
    6 P e ∨
    7 match e with [ Expr e _ ⇒
    8 match e with
    9 [ Ederef e' ⇒ any_expr P e'
    10 | Eunop _ e' ⇒ any_expr P e'
    11 | Ebinop _ e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
    12 | Ecast _ e' ⇒ any_expr P e'
    13 | Econdition e1 e2 e3 ⇒ any_expr P e1 ∨ any_expr P e2 ∨ any_expr P e3
    14 | Eandbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
    15 | Eorbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
    16 | Efield e' _ ⇒ any_expr P e'
    17 | Ecost _ e' ⇒ any_expr P e'
    18 | _ ⇒ false
    19 ] ].
    20 
    21 definition any_expr_statement : (expr → bool) → statement → bool ≝
    22 λP,s.
    23 match s with
    24 [ Sassign e1 e2 ⇒ P e1 ∨ P e2
    25 | Scall oe e es ⇒ (option_map_def … P false oe) ∨ P e ∨ all ? P es
    26 | Sifthenelse e _ _ ⇒ P e
    27 | Swhile e _ ⇒ P e
    28 | Sdowhile e _ ⇒ P e
    29 | Sfor _ e _ _ ⇒ P e
    30 | Sreturn oe ⇒ option_map_def … P false oe
    31 | _ ⇒ false
    32 ].
    33 
    34 let rec any_statement (P:statement → bool) (s:statement) on s : bool ≝
    35 P s ∨
    36 match s with
    37 [ Ssequence s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2
    38 | Sifthenelse _ s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2
    39 | Swhile _ s1 ⇒ any_statement P s1
    40 | Sdowhile _ s1 ⇒ any_statement P s1
    41 | Sfor s1 _ s2 s3 ⇒ any_statement P s1 ∨ any_statement P s2 ∨ any_statement P s3
    42 | Sswitch _ ls ⇒ any_labeled_statement P ls
    43 | Slabel _ s1 ⇒ any_statement P s1
    44 | Scost _ s1 ⇒ any_statement P s1
    45 | _ ⇒ false
    46 ] and any_labeled_statement (P:statement → bool) (ls:labeled_statements) on ls : bool ≝
    47 match ls with
    48 [ LSdefault s ⇒ any_statement P s
    49 | LScase _ _ s ls' ⇒ any_statement P s ∨ any_labeled_statement P ls'
    50 ].
    51 
    52 (* Labelled states in Clight are a little tricky because there are cost labels
    53    in the expressions in addition to the cost statement.  Note that a labelled
    54    state may produce several cost labels due to expressions, and that we should
    55    only check the root of the statement because sub-statements will not be
    56    executed until later.
     3(* I previously had a complicated definition that said a labelled Clight state
     4   was one with a syntactic form that would emit a cost label in the trace when
     5   the next step is evaluated.  This is the wrong notion.
    576   
    58    Also, a labelled state will only be guaranteed to generate a cost label in
    59    the trace if the program is properly cost labelled - if it isn't then an
    60    Econd might be used to with a cost label in only one branch.
    61     *)
    62 
    63 definition expr_labelled : expr → bool ≝
    64 any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true | _ ⇒ false ] ]).
    65 
    66 definition statement_cont_labelled : statement → cont → bool ≝
    67 λs,k.
    68 match s with
    69 [ Sskip ⇒
    70   match k with
    71   [ Kdowhile e _ _ ⇒ expr_labelled e
    72   | _ ⇒ false
    73   ]
    74 | Sassign e1 e2 ⇒ expr_labelled e1 ∨ expr_labelled e2
    75 | Scall oe e es ⇒ (option_map_def … expr_labelled false oe) ∨ expr_labelled e ∨ all ? expr_labelled es
    76 | Ssequence _ _ ⇒ false
    77 | Sifthenelse e _ _ ⇒ expr_labelled e
    78 | Swhile e _ ⇒ expr_labelled e
    79 | Sdowhile e _ ⇒ false
    80 | Sfor s e _ _ ⇒ match s with [ Sskip ⇒ expr_labelled e | _ ⇒ false ]
    81 | Sbreak ⇒ false
    82 | Scontinue ⇒
    83   match k with
    84   [ Kdowhile e _ _ ⇒ expr_labelled e
    85   | _ ⇒ false
    86   ]
    87 | Sreturn oe ⇒ option_map_def … expr_labelled false oe
    88 | Sswitch e _ ⇒ expr_labelled e (* should not occur due to early switch removal *)
    89 | Slabel _ _ ⇒ false
    90 | Sgoto _ ⇒ false
    91 | Scost _ _ ⇒ true
    92 ].
     7   We want a labelled Clight state to indicate that we can measure the time of
     8   some correspondingly labelled machine code from there.  Only explicit
     9   statement level cost labels are useful for this.  Cost labels that appear
     10   in the middle of expressions are only useful for allowing the amount of time
     11   measured to differ.
     12   
     13   (Otherwise you see something silly like "x=(y-1) ? c1: 1 : c2: z;" as a
     14   labelled state, even though the labels c1 and c2 will appear in the *middle*
     15   of the corresponding machine code, and so you measure the wrong thing and
     16   can't prove it.)
     17 *)
    9318
    9419definition Clight_labelled : state → bool ≝
    9520λs. match s with
    96 [ State f s k e m ⇒ statement_cont_labelled s k
     21[ State f s k e m ⇒ match s with [ Scost _ _ ⇒ true | _ ⇒ false ]
    9722| _ ⇒ false
    9823].
Note: See TracChangeset for help on using the changeset viewer.