source: src/Clight/label.ma @ 2103

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

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

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