63 open Hints_declaration
77 (** val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list **)
78 let rec labels_of_expr = function
79 | Csyntax.Expr (e', x) ->
81 | Csyntax.Econst_int (x0, x1) -> List.Nil
82 | Csyntax.Evar x0 -> List.Nil
83 | Csyntax.Ederef e1 -> labels_of_expr e1
84 | Csyntax.Eaddrof e1 -> labels_of_expr e1
85 | Csyntax.Eunop (x0, e1) -> labels_of_expr e1
86 | Csyntax.Ebinop (x0, e1, e2) ->
87 List.append (labels_of_expr e1) (labels_of_expr e2)
88 | Csyntax.Ecast (x0, e1) -> labels_of_expr e1
89 | Csyntax.Econdition (e1, e2, e3) ->
90 List.append (labels_of_expr e1)
91 (List.append (labels_of_expr e2) (labels_of_expr e3))
92 | Csyntax.Eandbool (e1, e2) ->
93 List.append (labels_of_expr e1) (labels_of_expr e2)
94 | Csyntax.Eorbool (e1, e2) ->
95 List.append (labels_of_expr e1) (labels_of_expr e2)
96 | Csyntax.Esizeof x0 -> List.Nil
97 | Csyntax.Efield (e1, x0) -> labels_of_expr e1
98 | Csyntax.Ecost (cl, e1) -> List.Cons (cl, (labels_of_expr e1)))
100 (** val labels_of_statement :
101 Csyntax.statement -> CostLabel.costlabel List.list **)
102 let rec labels_of_statement = function
103 | Csyntax.Sskip -> List.Nil
104 | Csyntax.Sassign (e1, e2) ->
105 List.append (labels_of_expr e1) (labels_of_expr e2)
106 | Csyntax.Scall (oe, e1, es) ->
107 List.append (Types.option_map_def labels_of_expr List.Nil oe)
108 (List.append (labels_of_expr e1)
109 (Util.foldl (fun ls e -> List.append (labels_of_expr e) ls) List.Nil
111 | Csyntax.Ssequence (s1, s2) ->
112 List.append (labels_of_statement s1) (labels_of_statement s2)
113 | Csyntax.Sifthenelse (e1, s1, s2) ->
114 List.append (labels_of_expr e1)
115 (List.append (labels_of_statement s1) (labels_of_statement s2))
116 | Csyntax.Swhile (e1, s1) ->
117 List.append (labels_of_expr e1) (labels_of_statement s1)
118 | Csyntax.Sdowhile (e1, s1) ->
119 List.append (labels_of_expr e1) (labels_of_statement s1)
120 | Csyntax.Sfor (s1, e1, s2, s3) ->
121 List.append (labels_of_statement s1)
122 (List.append (labels_of_expr e1)
123 (List.append (labels_of_statement s2) (labels_of_statement s3)))
124 | Csyntax.Sbreak -> List.Nil
125 | Csyntax.Scontinue -> List.Nil
126 | Csyntax.Sreturn oe -> Types.option_map_def labels_of_expr List.Nil oe
127 | Csyntax.Sswitch (e1, ls) ->
128 List.append (labels_of_expr e1) (labels_of_labeled_statements ls)
129 | Csyntax.Slabel (x, s1) -> labels_of_statement s1
130 | Csyntax.Sgoto x -> List.Nil
131 | Csyntax.Scost (cl, s1) -> List.Cons (cl, (labels_of_statement s1))
132 (** val labels_of_labeled_statements :
133 Csyntax.labeled_statements -> CostLabel.costlabel List.list **)
134 and labels_of_labeled_statements = function
135 | Csyntax.LSdefault s1 -> labels_of_statement s1
136 | Csyntax.LScase (x, x0, s1, ls1) ->
137 List.append (labels_of_statement s1) (labels_of_labeled_statements ls1)
139 (** val labels_of_clight_fundef :
140 (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
142 let labels_of_clight_fundef ifd =
143 match ifd.Types.snd with
144 | Csyntax.CL_Internal f -> labels_of_statement f.Csyntax.fn_body
145 | Csyntax.CL_External (x, x0, x1) -> List.Nil
147 (** val labels_of_clight :
148 Csyntax.clight_program -> CostLabel.costlabel List.list **)
149 let labels_of_clight p =
150 Util.foldl (fun ls f -> List.append (labels_of_clight_fundef f) ls)
151 List.Nil p.AST.prog_funct
153 type in_clight_label = CostLabel.costlabel Types.sig0
155 type clight_cost_map = CostLabel.costlabel -> Nat.nat
157 (** val clight_label_free : Csyntax.clight_program -> Bool.bool **)
158 let clight_label_free p =
159 match labels_of_clight p with
160 | List.Nil -> Bool.True
161 | List.Cons (x, x0) -> Bool.False
163 (** val add_cost_before :
164 Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
165 Identifiers.universe) Types.prod **)
166 let add_cost_before s gen =
167 let { Types.fst = l; Types.snd = gen0 } =
168 Identifiers.fresh PreIdentifiers.CostTag gen
170 { Types.fst = (Csyntax.Scost (l, s)); Types.snd = gen0 }
172 (** val add_cost_after :
173 Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
174 Identifiers.universe) Types.prod **)
175 let add_cost_after s gen =
176 let { Types.fst = l; Types.snd = gen0 } =
177 Identifiers.fresh PreIdentifiers.CostTag gen
179 { Types.fst = (Csyntax.Ssequence (s, (Csyntax.Scost (l, Csyntax.Sskip))));
182 (** val add_cost_expr :
183 Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
184 Identifiers.universe) Types.prod **)
185 let add_cost_expr e gen =
186 let { Types.fst = l; Types.snd = gen0 } =
187 Identifiers.fresh PreIdentifiers.CostTag gen
189 { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e)), (Csyntax.typeof e)));
192 (** val const_int : AST.intsize -> Nat.nat -> Csyntax.expr **)
194 Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr sz n))), (Csyntax.Tint
198 Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
199 Identifiers.universe) Types.prod **)
200 let rec label_expr e costgen =
201 let Csyntax.Expr (ed, ty) = e in
202 let { Types.fst = ed0; Types.snd = costgen0 } =
203 label_expr_descr ed costgen ty
205 { Types.fst = (Csyntax.Expr (ed0, ty)); Types.snd = costgen0 }
206 (** val label_expr_descr :
207 Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
208 (Csyntax.expr_descr, Identifiers.universe) Types.prod **)
209 and label_expr_descr e costgen ty =
211 | Csyntax.Econst_int (x, x0) -> { Types.fst = e; Types.snd = costgen }
212 | Csyntax.Evar x -> { Types.fst = e; Types.snd = costgen }
213 | Csyntax.Ederef e' ->
214 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
215 { Types.fst = (Csyntax.Ederef e'0); Types.snd = costgen0 }
216 | Csyntax.Eaddrof e' ->
217 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
218 { Types.fst = (Csyntax.Eaddrof e'0); Types.snd = costgen0 }
219 | Csyntax.Eunop (op, e') ->
220 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
221 { Types.fst = (Csyntax.Eunop (op, e'0)); Types.snd = costgen0 }
222 | Csyntax.Ebinop (op, e1, e2) ->
223 let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
224 let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
225 { Types.fst = (Csyntax.Ebinop (op, e10, e20)); Types.snd = costgen1 }
226 | Csyntax.Ecast (ty0, e') ->
227 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
228 { Types.fst = (Csyntax.Ecast (ty0, e'0)); Types.snd = costgen0 }
229 | Csyntax.Econdition (e', e1, e2) ->
230 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
231 let { Types.fst = e10; Types.snd = costgen1 } = label_expr e1 costgen0 in
232 let { Types.fst = e11; Types.snd = costgen2 } =
233 add_cost_expr e10 costgen1
235 let { Types.fst = e20; Types.snd = costgen3 } = label_expr e2 costgen2 in
236 let { Types.fst = e21; Types.snd = costgen4 } =
237 add_cost_expr e20 costgen3
239 { Types.fst = (Csyntax.Econdition (e'0, e11, e21)); Types.snd =
241 | Csyntax.Eandbool (e1, e2) ->
242 let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
243 let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
246 let { Types.fst = et; Types.snd = costgen2 } =
247 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
249 let { Types.fst = ef; Types.snd = costgen3 } =
250 add_cost_expr (const_int AST.I32 Nat.O) costgen2
252 let { Types.fst = e21; Types.snd = costgen4 } =
253 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
256 let { Types.fst = ef0; Types.snd = costgen5 } =
257 add_cost_expr (const_int AST.I32 Nat.O) costgen4
259 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
261 | Csyntax.Tint (sz, sg) ->
262 let { Types.fst = et; Types.snd = costgen2 } =
263 add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
265 let { Types.fst = ef; Types.snd = costgen3 } =
266 add_cost_expr (const_int sz Nat.O) costgen2
268 let { Types.fst = e21; Types.snd = costgen4 } =
269 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
272 let { Types.fst = ef0; Types.snd = costgen5 } =
273 add_cost_expr (const_int sz Nat.O) costgen4
275 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
277 | Csyntax.Tpointer x ->
278 let { Types.fst = et; Types.snd = costgen2 } =
279 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
281 let { Types.fst = ef; Types.snd = costgen3 } =
282 add_cost_expr (const_int AST.I32 Nat.O) costgen2
284 let { Types.fst = e21; Types.snd = costgen4 } =
285 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
288 let { Types.fst = ef0; Types.snd = costgen5 } =
289 add_cost_expr (const_int AST.I32 Nat.O) costgen4
291 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
293 | Csyntax.Tarray (x, x0) ->
294 let { Types.fst = et; Types.snd = costgen2 } =
295 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
297 let { Types.fst = ef; Types.snd = costgen3 } =
298 add_cost_expr (const_int AST.I32 Nat.O) costgen2
300 let { Types.fst = e21; Types.snd = costgen4 } =
301 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
304 let { Types.fst = ef0; Types.snd = costgen5 } =
305 add_cost_expr (const_int AST.I32 Nat.O) costgen4
307 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
309 | Csyntax.Tfunction (x, x0) ->
310 let { Types.fst = et; Types.snd = costgen2 } =
311 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
313 let { Types.fst = ef; Types.snd = costgen3 } =
314 add_cost_expr (const_int AST.I32 Nat.O) costgen2
316 let { Types.fst = e21; Types.snd = costgen4 } =
317 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
320 let { Types.fst = ef0; Types.snd = costgen5 } =
321 add_cost_expr (const_int AST.I32 Nat.O) costgen4
323 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
325 | Csyntax.Tstruct (x, x0) ->
326 let { Types.fst = et; Types.snd = costgen2 } =
327 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
329 let { Types.fst = ef; Types.snd = costgen3 } =
330 add_cost_expr (const_int AST.I32 Nat.O) costgen2
332 let { Types.fst = e21; Types.snd = costgen4 } =
333 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
336 let { Types.fst = ef0; Types.snd = costgen5 } =
337 add_cost_expr (const_int AST.I32 Nat.O) costgen4
339 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
341 | Csyntax.Tunion (x, x0) ->
342 let { Types.fst = et; Types.snd = costgen2 } =
343 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
345 let { Types.fst = ef; Types.snd = costgen3 } =
346 add_cost_expr (const_int AST.I32 Nat.O) costgen2
348 let { Types.fst = e21; Types.snd = costgen4 } =
349 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
352 let { Types.fst = ef0; Types.snd = costgen5 } =
353 add_cost_expr (const_int AST.I32 Nat.O) costgen4
355 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
357 | Csyntax.Tcomp_ptr x ->
358 let { Types.fst = et; Types.snd = costgen2 } =
359 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
361 let { Types.fst = ef; Types.snd = costgen3 } =
362 add_cost_expr (const_int AST.I32 Nat.O) costgen2
364 let { Types.fst = e21; Types.snd = costgen4 } =
365 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
368 let { Types.fst = ef0; Types.snd = costgen5 } =
369 add_cost_expr (const_int AST.I32 Nat.O) costgen4
371 { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
373 | Csyntax.Eorbool (e1, e2) ->
374 let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
375 let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
378 let { Types.fst = et; Types.snd = costgen2 } =
379 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
381 let { Types.fst = ef; Types.snd = costgen3 } =
382 add_cost_expr (const_int AST.I32 Nat.O) costgen2
384 let { Types.fst = e21; Types.snd = costgen4 } =
385 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
388 let { Types.fst = et0; Types.snd = costgen5 } =
389 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
391 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
393 | Csyntax.Tint (sz, sg) ->
394 let { Types.fst = et; Types.snd = costgen2 } =
395 add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
397 let { Types.fst = ef; Types.snd = costgen3 } =
398 add_cost_expr (const_int sz Nat.O) costgen2
400 let { Types.fst = e21; Types.snd = costgen4 } =
401 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
404 let { Types.fst = et0; Types.snd = costgen5 } =
405 add_cost_expr (const_int sz (Nat.S Nat.O)) costgen4
407 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
409 | Csyntax.Tpointer x ->
410 let { Types.fst = et; Types.snd = costgen2 } =
411 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
413 let { Types.fst = ef; Types.snd = costgen3 } =
414 add_cost_expr (const_int AST.I32 Nat.O) costgen2
416 let { Types.fst = e21; Types.snd = costgen4 } =
417 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
420 let { Types.fst = et0; Types.snd = costgen5 } =
421 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
423 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
425 | Csyntax.Tarray (x, x0) ->
426 let { Types.fst = et; Types.snd = costgen2 } =
427 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
429 let { Types.fst = ef; Types.snd = costgen3 } =
430 add_cost_expr (const_int AST.I32 Nat.O) costgen2
432 let { Types.fst = e21; Types.snd = costgen4 } =
433 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
436 let { Types.fst = et0; Types.snd = costgen5 } =
437 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
439 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
441 | Csyntax.Tfunction (x, x0) ->
442 let { Types.fst = et; Types.snd = costgen2 } =
443 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
445 let { Types.fst = ef; Types.snd = costgen3 } =
446 add_cost_expr (const_int AST.I32 Nat.O) costgen2
448 let { Types.fst = e21; Types.snd = costgen4 } =
449 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
452 let { Types.fst = et0; Types.snd = costgen5 } =
453 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
455 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
457 | Csyntax.Tstruct (x, x0) ->
458 let { Types.fst = et; Types.snd = costgen2 } =
459 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
461 let { Types.fst = ef; Types.snd = costgen3 } =
462 add_cost_expr (const_int AST.I32 Nat.O) costgen2
464 let { Types.fst = e21; Types.snd = costgen4 } =
465 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
468 let { Types.fst = et0; Types.snd = costgen5 } =
469 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
471 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
473 | Csyntax.Tunion (x, x0) ->
474 let { Types.fst = et; Types.snd = costgen2 } =
475 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
477 let { Types.fst = ef; Types.snd = costgen3 } =
478 add_cost_expr (const_int AST.I32 Nat.O) costgen2
480 let { Types.fst = e21; Types.snd = costgen4 } =
481 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
484 let { Types.fst = et0; Types.snd = costgen5 } =
485 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
487 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
489 | Csyntax.Tcomp_ptr x ->
490 let { Types.fst = et; Types.snd = costgen2 } =
491 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
493 let { Types.fst = ef; Types.snd = costgen3 } =
494 add_cost_expr (const_int AST.I32 Nat.O) costgen2
496 let { Types.fst = e21; Types.snd = costgen4 } =
497 add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
500 let { Types.fst = et0; Types.snd = costgen5 } =
501 add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
503 { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
505 | Csyntax.Esizeof x -> { Types.fst = e; Types.snd = costgen }
506 | Csyntax.Efield (e', id) ->
507 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
508 { Types.fst = (Csyntax.Efield (e'0, id)); Types.snd = costgen0 }
509 | Csyntax.Ecost (l, e') ->
510 let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
511 { Types.fst = (Csyntax.Ecost (l, e'0)); Types.snd = costgen0 }
513 (** val label_exprs :
514 Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr
515 List.list, Identifiers.universe) Types.prod **)
516 let rec label_exprs l costgen =
518 | List.Nil -> { Types.fst = List.Nil; Types.snd = costgen }
519 | List.Cons (e, es) ->
520 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
521 let { Types.fst = es0; Types.snd = costgen1 } = label_exprs es costgen0
523 { Types.fst = (List.Cons (e0, es0)); Types.snd = costgen1 }
525 (** val label_opt_expr :
526 Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
527 Types.option, Identifiers.universe) Types.prod **)
528 let label_opt_expr oe costgen =
530 | Types.None -> { Types.fst = Types.None; Types.snd = costgen }
532 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
533 { Types.fst = (Types.Some e0); Types.snd = costgen0 }
535 (** val label_statement :
536 Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
537 Identifiers.universe) Types.prod **)
538 let rec label_statement s costgen =
540 | Csyntax.Sskip -> { Types.fst = Csyntax.Sskip; Types.snd = costgen }
541 | Csyntax.Sassign (e1, e2) ->
542 let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
543 let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
544 { Types.fst = (Csyntax.Sassign (e10, e20)); Types.snd = costgen1 }
545 | Csyntax.Scall (e_ret, e_fn, e_args) ->
546 let { Types.fst = e_ret0; Types.snd = costgen0 } =
547 label_opt_expr e_ret costgen
549 let { Types.fst = e_fn0; Types.snd = costgen1 } =
550 label_expr e_fn costgen0
552 let { Types.fst = e_args0; Types.snd = costgen2 } =
553 label_exprs e_args costgen1
555 { Types.fst = (Csyntax.Scall (e_ret0, e_fn0, e_args0)); Types.snd =
557 | Csyntax.Ssequence (s1, s2) ->
558 let { Types.fst = s10; Types.snd = costgen0 } =
559 label_statement s1 costgen
561 let { Types.fst = s20; Types.snd = costgen1 } =
562 label_statement s2 costgen0
564 { Types.fst = (Csyntax.Ssequence (s10, s20)); Types.snd = costgen1 }
565 | Csyntax.Sifthenelse (e, s1, s2) ->
566 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
567 let { Types.fst = s10; Types.snd = costgen1 } =
568 label_statement s1 costgen0
570 let { Types.fst = s11; Types.snd = costgen2 } =
571 add_cost_before s10 costgen1
573 let { Types.fst = s20; Types.snd = costgen3 } =
574 label_statement s2 costgen2
576 let { Types.fst = s21; Types.snd = costgen4 } =
577 add_cost_before s20 costgen3
579 { Types.fst = (Csyntax.Sifthenelse (e0, s11, s21)); Types.snd =
581 | Csyntax.Swhile (e, s') ->
582 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
583 let { Types.fst = s'0; Types.snd = costgen1 } =
584 label_statement s' costgen0
586 let { Types.fst = s'1; Types.snd = costgen2 } =
587 add_cost_before s'0 costgen1
589 let { Types.fst = s0; Types.snd = costgen3 } =
590 add_cost_after (Csyntax.Swhile (e0, s'1)) costgen2
592 { Types.fst = s0; Types.snd = costgen3 }
593 | Csyntax.Sdowhile (e, s') ->
594 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
595 let { Types.fst = s'0; Types.snd = costgen1 } =
596 label_statement s' costgen0
598 let { Types.fst = s'1; Types.snd = costgen2 } =
599 add_cost_before s'0 costgen1
601 let { Types.fst = s0; Types.snd = costgen3 } =
602 add_cost_after (Csyntax.Sdowhile (e0, s'1)) costgen2
604 { Types.fst = s0; Types.snd = costgen3 }
605 | Csyntax.Sfor (s1, e, s2, s3) ->
606 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
607 let { Types.fst = s10; Types.snd = costgen1 } =
608 label_statement s1 costgen0
610 let { Types.fst = s20; Types.snd = costgen2 } =
611 label_statement s2 costgen1
613 let { Types.fst = s30; Types.snd = costgen3 } =
614 label_statement s3 costgen2
616 let { Types.fst = s31; Types.snd = costgen4 } =
617 add_cost_before s30 costgen3
619 let { Types.fst = s0; Types.snd = costgen5 } =
620 add_cost_after (Csyntax.Sfor (s10, e0, s20, s31)) costgen4
622 { Types.fst = s0; Types.snd = costgen5 }
623 | Csyntax.Sbreak -> { Types.fst = Csyntax.Sbreak; Types.snd = costgen }
624 | Csyntax.Scontinue ->
625 { Types.fst = Csyntax.Scontinue; Types.snd = costgen }
626 | Csyntax.Sreturn opt_e ->
627 let { Types.fst = opt_e0; Types.snd = costgen0 } =
628 label_opt_expr opt_e costgen
630 { Types.fst = (Csyntax.Sreturn opt_e0); Types.snd = costgen0 }
631 | Csyntax.Sswitch (e, ls) ->
632 let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
633 let { Types.fst = ls0; Types.snd = costgen1 } =
634 label_lstatements ls costgen0
636 { Types.fst = (Csyntax.Sswitch (e0, ls0)); Types.snd = costgen1 }
637 | Csyntax.Slabel (l, s') ->
638 let { Types.fst = s'0; Types.snd = costgen0 } =
639 label_statement s' costgen
641 let { Types.fst = s'1; Types.snd = costgen1 } =
642 add_cost_before s'0 costgen0
644 { Types.fst = (Csyntax.Slabel (l, s'1)); Types.snd = costgen1 }
645 | Csyntax.Sgoto l -> { Types.fst = (Csyntax.Sgoto l); Types.snd = costgen }
646 | Csyntax.Scost (l, s') ->
647 let { Types.fst = s'0; Types.snd = costgen0 } =
648 label_statement s' costgen
650 { Types.fst = (Csyntax.Scost (l, s'0)); Types.snd = costgen0 }
651 (** val label_lstatements :
652 Csyntax.labeled_statements -> Identifiers.universe ->
653 (Csyntax.labeled_statements, Identifiers.universe) Types.prod **)
654 and label_lstatements ls costgen =
656 | Csyntax.LSdefault s ->
657 let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
659 let { Types.fst = s1; Types.snd = costgen1 } =
660 add_cost_before s0 costgen0
662 { Types.fst = (Csyntax.LSdefault s1); Types.snd = costgen1 }
663 | Csyntax.LScase (sz, i, s, ls') ->
664 let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
666 let { Types.fst = s1; Types.snd = costgen1 } =
667 add_cost_before s0 costgen0
669 let { Types.fst = ls'0; Types.snd = costgen2 } =
670 label_lstatements ls' costgen1
672 { Types.fst = (Csyntax.LScase (sz, i, s1, ls'0)); Types.snd = costgen2 }
674 (** val label_function :
675 Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
676 Identifiers.universe) Types.prod **)
677 let label_function costgen f =
678 let { Types.fst = body; Types.snd = costgen0 } =
679 label_statement f.Csyntax.fn_body costgen
681 let { Types.fst = body0; Types.snd = costgen1 } =
682 add_cost_before body costgen0
684 { Types.fst = { Csyntax.fn_return = f.Csyntax.fn_return;
685 Csyntax.fn_params = f.Csyntax.fn_params; Csyntax.fn_vars =
686 f.Csyntax.fn_vars; Csyntax.fn_body = body0 }; Types.snd = costgen1 }
688 (** val label_fundef :
689 Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
690 Identifiers.universe) Types.prod **)
691 let label_fundef gen = function
692 | Csyntax.CL_Internal f0 ->
693 let { Types.fst = f'; Types.snd = gen' } = label_function gen f0 in
694 { Types.fst = (Csyntax.CL_Internal f'); Types.snd = gen' }
695 | Csyntax.CL_External (id, args, ty) ->
696 { Types.fst = (Csyntax.CL_External (id, args, ty)); Types.snd = gen }
698 (** val clight_label :
699 Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
701 let rec clight_label p =
702 let costgen = Identifiers.new_universe PreIdentifiers.CostTag in
703 let { Types.fst = init_cost; Types.snd = costgen0 } =
704 Identifiers.fresh PreIdentifiers.CostTag costgen
707 (AST.transform_program_gen PreIdentifiers.CostTag costgen0 p (fun x ->
708 label_fundef)).Types.fst; Types.snd = init_cost }