source: src/Clight/label.ma @ 2103

Last change on this file since 2103 was 2103, checked in by campbell, 8 years ago

Make transform_*program take a more general transformation to make
properties easier to state.

File size: 7.5 KB
RevLine 
[781]1include "Clight/Csyntax.ma".
2
[1056]3definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
[781]4λs,gen.
[1056]5  let 〈l,gen〉 ≝ fresh … gen in
6  〈Scost l s, gen〉.
[781]7
[1056]8definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝
[781]9λs,gen.
[1056]10  let 〈l,gen〉 ≝ fresh … gen in
11  〈Ssequence s (Scost l Sskip), gen〉.
[781]12
[1056]13definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝
[781]14λe,gen.
[1056]15  let 〈l,gen〉 ≝ fresh … gen in
16  〈Expr (Ecost l e) (typeof e), gen〉.
[781]17
[1888]18definition const_int : nat → expr ≝
19λn. Expr (Econst_int ? (repr I32 n)) (Tint I32 Signed).
20
[781]21let rec label_expr (e:expr) (costgen:universe CostTag)
[1056]22        on e : expr × (universe CostTag) ≝
[781]23match e with
[1888]24[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen ty in
[1056]25               〈Expr ed ty, costgen〉
[781]26]
[1888]27and label_expr_descr (e:expr_descr) (costgen:universe CostTag) (ty:type)
[1056]28    on e : expr_descr × (universe CostTag) ≝
[781]29match e with
30[ Ederef e' ⇒
[1056]31    let 〈e',costgen〉 ≝ label_expr e' costgen in
32    〈Ederef e', costgen〉
[781]33| Eaddrof e' ⇒
[1056]34    let 〈e',costgen〉 ≝ label_expr e' costgen in
35    〈Eaddrof e', costgen〉
[781]36| Eunop op e' ⇒
[1056]37    let 〈e',costgen〉 ≝ label_expr e' costgen in
38    〈Eunop op e', costgen〉
[781]39| Ebinop op e1 e2 ⇒
[1056]40    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
41    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
42    〈Ebinop op e1 e2, costgen〉
[781]43| Ecast ty e' ⇒
[1056]44    let 〈e',costgen〉 ≝ label_expr e' costgen in
45    〈Ecast ty e', costgen〉
[781]46| Econdition e' e1 e2 ⇒
[1056]47    let 〈e',costgen〉 ≝ label_expr e' costgen in
48    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
49    let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in
50    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
51    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
52    〈Econdition e' e1 e2, costgen〉
[781]53(* andbool and orbool are changed to conditionals to capture their
[1888]54   short-circuiting cost difference; note that we have to return 0 or 1 *)
[781]55| Eandbool e1 e2 ⇒
[1056]56    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
57    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
[1888]58    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
59    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
[1056]60    〈Econdition e1 e2 ef, costgen〉
[781]61| Eorbool e1 e2 ⇒
[1056]62    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
[1888]63    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
[1056]64    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
[1888]65    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
[1056]66    〈Econdition e1 et e2, costgen〉
[781]67
68| Efield e' id ⇒
[1056]69    let 〈e',costgen〉 ≝ label_expr e' costgen in
70    〈Efield e' id, costgen〉
[781]71(* The prototype asserts on preexisting cost labels, but I'd quite like to
72   keep them. *)
73| Ecost l e' ⇒
[1056]74    let 〈e',costgen〉 ≝ label_expr e' costgen in
75    〈Ecost l e', costgen〉
[781]76
77(* The remaining expressions don't have subexpressions. *)
[1056]78| _ ⇒ 〈e,costgen〉
[781]79].
80
81let rec label_exprs (l:list expr) (costgen:universe CostTag)
[1056]82        on l : list expr × (universe CostTag) ≝
[781]83match l with
[1056]84[ nil ⇒ 〈nil ?,costgen〉
[781]85| cons e es ⇒
[1056]86    let 〈e,costgen〉 ≝ label_expr e costgen in
87    let 〈es,costgen〉 ≝ label_exprs es costgen in
88    〈e::es,costgen〉
[781]89].
90
91definition label_opt_expr ≝
92λoe,costgen. match oe with
[1056]93[ None ⇒ 〈None ?, costgen〉
94| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
[781]95].
96
97
98let rec label_statement (s:statement) (costgen:universe CostTag)
[1056]99        on s : statement × (universe CostTag) ≝
[781]100match s with
[1056]101[ Sskip ⇒ 〈Sskip,costgen〉
[781]102| Sassign e1 e2 ⇒
[1056]103    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
104    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
105    〈Sassign e1 e2, costgen〉
[781]106| Scall e_ret e_fn e_args ⇒
[1056]107    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
108    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
109    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
110    〈Scall e_ret e_fn e_args, costgen〉
[781]111| Ssequence s1 s2 ⇒
[1056]112    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
113    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
114    〈Ssequence s1 s2, costgen〉
[781]115| Sifthenelse e s1 s2 ⇒
[1056]116    let 〈e,costgen〉 ≝ label_expr e costgen in
117    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
118    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
119    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
120    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
121    〈Sifthenelse e s1 s2, costgen〉
[781]122| Swhile e s' ⇒
[1056]123    let 〈e,costgen〉 ≝ label_expr e costgen in
124    let 〈s',costgen〉 ≝ label_statement s' costgen in
125    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
126    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
127    〈s,costgen〉
[781]128| Sdowhile e s' ⇒
[1056]129    let 〈e,costgen〉 ≝ label_expr e costgen in
130    let 〈s',costgen〉 ≝ label_statement s' costgen in
131    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
132    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
133    〈s,costgen〉
[781]134| Sfor s1 e s2 s3 ⇒
[1056]135    let 〈e,costgen〉 ≝ label_expr e costgen in
136    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
137    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
138    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
139    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
140    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
141    〈s,costgen〉
142| Sbreak ⇒ 〈Sbreak,costgen〉
143| Scontinue ⇒ 〈Scontinue,costgen〉
[781]144| Sreturn opt_e ⇒
[1056]145    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
146    〈Sreturn opt_e,costgen〉
[781]147| Sswitch e ls ⇒
[1056]148    let 〈e,costgen〉 ≝ label_expr e costgen in
149    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
150    〈Sswitch e ls, costgen〉
[781]151| Slabel l s' ⇒
[1056]152    let 〈s',costgen〉 ≝ label_statement s' costgen in
153    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
154    〈Slabel l s', costgen〉
155| Sgoto l ⇒ 〈Sgoto l, costgen〉
[781]156
157(* The prototype asserts on preexisting cost labels, but I'd quite like to
158   keep them. *)
159| Scost l s' ⇒
[1056]160    let 〈s',costgen〉 ≝ label_statement s' costgen in
161    〈Scost l s', costgen〉
[781]162]
163and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
[1056]164        on ls : labeled_statements × (universe CostTag) ≝
[781]165match ls with
166[ LSdefault s ⇒
[1056]167    let 〈s,costgen〉 ≝ label_statement s costgen in
168    let 〈s,costgen〉 ≝ add_cost_before s costgen in
169    〈LSdefault s, costgen〉
[961]170| LScase sz i s ls' ⇒
[1056]171    let 〈s,costgen〉 ≝ label_statement s costgen in
172    let 〈s,costgen〉 ≝ add_cost_before s costgen in
173    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
174    〈LScase sz i s ls', costgen〉
[781]175].
176
[1515]177definition label_function : function → function ≝
[781]178λf.
179  let costgen ≝ new_universe CostTag in
[1056]180  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
181  let 〈body,costgen〉 ≝ add_cost_before body costgen in
[1515]182    mk_function (fn_return f) (fn_params f) (fn_vars f) body.
[781]183
[1515]184definition label_fundef : clight_fundef → clight_fundef ≝
[781]185λf. match f with
[1515]186[ CL_Internal f ⇒ CL_Internal (label_function f)
187| CL_External id args ty ⇒ CL_External id args ty
[781]188].
189
[1515]190definition clight_label : clight_program → clight_program ≝
[2103]191 λp. transform_program … p (λ_.label_fundef).
Note: See TracBrowser for help on using the repository browser.