source: src/Clight/label.ma @ 978

Last change on this file since 978 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 7.4 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 I32 (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 I32 (repr ? 1)) (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 sz 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 sz 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.