source: src/Clight/label.ma @ 781

Last change on this file since 781 was 781, checked in by campbell, 9 years ago

Implement labelling pass for Clight.

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