source: extracted/label.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 26.1 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75(** val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list **)
76let rec labels_of_expr = function
77| Csyntax.Expr (e', x) ->
78  (match e' with
79   | Csyntax.Econst_int (x0, x1) -> List.Nil
80   | Csyntax.Evar x0 -> List.Nil
81   | Csyntax.Ederef e1 -> labels_of_expr e1
82   | Csyntax.Eaddrof e1 -> labels_of_expr e1
83   | Csyntax.Eunop (x0, e1) -> labels_of_expr e1
84   | Csyntax.Ebinop (x0, e1, e2) ->
85     List.append (labels_of_expr e1) (labels_of_expr e2)
86   | Csyntax.Ecast (x0, e1) -> labels_of_expr e1
87   | Csyntax.Econdition (e1, e2, e3) ->
88     List.append (labels_of_expr e1)
89       (List.append (labels_of_expr e2) (labels_of_expr e3))
90   | Csyntax.Eandbool (e1, e2) ->
91     List.append (labels_of_expr e1) (labels_of_expr e2)
92   | Csyntax.Eorbool (e1, e2) ->
93     List.append (labels_of_expr e1) (labels_of_expr e2)
94   | Csyntax.Esizeof x0 -> List.Nil
95   | Csyntax.Efield (e1, x0) -> labels_of_expr e1
96   | Csyntax.Ecost (cl, e1) -> List.Cons (cl, (labels_of_expr e1)))
97
98(** val labels_of_statement :
99    Csyntax.statement -> CostLabel.costlabel List.list **)
100let rec labels_of_statement = function
101| Csyntax.Sskip -> List.Nil
102| Csyntax.Sassign (e1, e2) ->
103  List.append (labels_of_expr e1) (labels_of_expr e2)
104| Csyntax.Scall (oe, e1, es) ->
105  List.append (Types.option_map_def labels_of_expr List.Nil oe)
106    (List.append (labels_of_expr e1)
107      (Util.foldl (fun ls e0 -> List.append (labels_of_expr e0) ls) List.Nil
108        es))
109| Csyntax.Ssequence (s1, s2) ->
110  List.append (labels_of_statement s1) (labels_of_statement s2)
111| Csyntax.Sifthenelse (e1, s1, s2) ->
112  List.append (labels_of_expr e1)
113    (List.append (labels_of_statement s1) (labels_of_statement s2))
114| Csyntax.Swhile (e1, s1) ->
115  List.append (labels_of_expr e1) (labels_of_statement s1)
116| Csyntax.Sdowhile (e1, s1) ->
117  List.append (labels_of_expr e1) (labels_of_statement s1)
118| Csyntax.Sfor (s1, e1, s2, s3) ->
119  List.append (labels_of_statement s1)
120    (List.append (labels_of_expr e1)
121      (List.append (labels_of_statement s2) (labels_of_statement s3)))
122| Csyntax.Sbreak -> List.Nil
123| Csyntax.Scontinue -> List.Nil
124| Csyntax.Sreturn oe -> Types.option_map_def labels_of_expr List.Nil oe
125| Csyntax.Sswitch (e1, ls) ->
126  List.append (labels_of_expr e1) (labels_of_labeled_statements ls)
127| Csyntax.Slabel (x, s1) -> labels_of_statement s1
128| Csyntax.Sgoto x -> List.Nil
129| Csyntax.Scost (cl, s1) -> List.Cons (cl, (labels_of_statement s1))
130(** val labels_of_labeled_statements :
131    Csyntax.labeled_statements -> CostLabel.costlabel List.list **)
132and labels_of_labeled_statements = function
133| Csyntax.LSdefault s1 -> labels_of_statement s1
134| Csyntax.LScase (x, x0, s1, ls1) ->
135  List.append (labels_of_statement s1) (labels_of_labeled_statements ls1)
136
137(** val labels_of_clight_fundef :
138    (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
139    List.list **)
140let labels_of_clight_fundef ifd =
141  match ifd.Types.snd with
142  | Csyntax.CL_Internal f -> labels_of_statement f.Csyntax.fn_body
143  | Csyntax.CL_External (x, x0, x1) -> List.Nil
144
145(** val labels_of_clight :
146    Csyntax.clight_program -> CostLabel.costlabel List.list **)
147let labels_of_clight p =
148  Util.foldl (fun ls f -> List.append (labels_of_clight_fundef f) ls)
149    List.Nil p.AST.prog_funct
150
151type in_clight_label = CostLabel.costlabel Types.sig0
152
153type clight_cost_map = in_clight_label -> Nat.nat
154
155(** val clight_label_free : Csyntax.clight_program -> Bool.bool **)
156let clight_label_free p =
157  match labels_of_clight p with
158  | List.Nil -> Bool.True
159  | List.Cons (x, x0) -> Bool.False
160
161(** val add_cost_before :
162    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
163    Identifiers.universe) Types.prod **)
164let add_cost_before s gen =
165  let { Types.fst = l; Types.snd = gen0 } =
166    Identifiers.fresh PreIdentifiers.CostTag gen
167  in
168  { Types.fst = (Csyntax.Scost (l, s)); Types.snd = gen0 }
169
170(** val add_cost_after :
171    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
172    Identifiers.universe) Types.prod **)
173let add_cost_after s gen =
174  let { Types.fst = l; Types.snd = gen0 } =
175    Identifiers.fresh PreIdentifiers.CostTag gen
176  in
177  { Types.fst = (Csyntax.Ssequence (s, (Csyntax.Scost (l, Csyntax.Sskip))));
178  Types.snd = gen0 }
179
180(** val add_cost_expr :
181    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
182    Identifiers.universe) Types.prod **)
183let add_cost_expr e0 gen =
184  let { Types.fst = l; Types.snd = gen0 } =
185    Identifiers.fresh PreIdentifiers.CostTag gen
186  in
187  { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e0)),
188  (Csyntax.typeof e0))); Types.snd = gen0 }
189
190(** val const_int : AST.intsize -> Nat.nat -> Csyntax.expr **)
191let const_int sz n =
192  Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr0 sz n))), (Csyntax.Tint
193    (sz, AST.Signed)))
194
195(** val label_expr :
196    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
197    Identifiers.universe) Types.prod **)
198let rec label_expr e0 costgen =
199  let Csyntax.Expr (ed, ty) = e0 in
200  let { Types.fst = ed0; Types.snd = costgen0 } =
201    label_expr_descr ed costgen ty
202  in
203  { Types.fst = (Csyntax.Expr (ed0, ty)); Types.snd = costgen0 }
204(** val label_expr_descr :
205    Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
206    (Csyntax.expr_descr, Identifiers.universe) Types.prod **)
207and label_expr_descr e0 costgen ty =
208  match e0 with
209  | Csyntax.Econst_int (x, x0) -> { Types.fst = e0; Types.snd = costgen }
210  | Csyntax.Evar x -> { Types.fst = e0; Types.snd = costgen }
211  | Csyntax.Ederef e' ->
212    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
213    { Types.fst = (Csyntax.Ederef e'0); Types.snd = costgen0 }
214  | Csyntax.Eaddrof e' ->
215    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
216    { Types.fst = (Csyntax.Eaddrof e'0); Types.snd = costgen0 }
217  | Csyntax.Eunop (op0, e') ->
218    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
219    { Types.fst = (Csyntax.Eunop (op0, e'0)); Types.snd = costgen0 }
220  | Csyntax.Ebinop (op0, e1, e2) ->
221    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
222    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
223    { Types.fst = (Csyntax.Ebinop (op0, e10, e20)); Types.snd = costgen1 }
224  | Csyntax.Ecast (ty0, e') ->
225    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
226    { Types.fst = (Csyntax.Ecast (ty0, e'0)); Types.snd = costgen0 }
227  | Csyntax.Econdition (e', e1, e2) ->
228    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
229    let { Types.fst = e10; Types.snd = costgen1 } = label_expr e1 costgen0 in
230    let { Types.fst = e11; Types.snd = costgen2 } =
231      add_cost_expr e10 costgen1
232    in
233    let { Types.fst = e20; Types.snd = costgen3 } = label_expr e2 costgen2 in
234    let { Types.fst = e21; Types.snd = costgen4 } =
235      add_cost_expr e20 costgen3
236    in
237    { Types.fst = (Csyntax.Econdition (e'0, e11, e21)); Types.snd =
238    costgen4 }
239  | Csyntax.Eandbool (e1, e2) ->
240    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
241    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
242    (match ty with
243     | Csyntax.Tvoid ->
244       let { Types.fst = et; Types.snd = costgen2 } =
245         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
246       in
247       let { Types.fst = ef; Types.snd = costgen3 } =
248         add_cost_expr (const_int AST.I32 Nat.O) costgen2
249       in
250       let { Types.fst = e21; Types.snd = costgen4 } =
251         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
252           ty)) costgen3
253       in
254       let { Types.fst = ef0; Types.snd = costgen5 } =
255         add_cost_expr (const_int AST.I32 Nat.O) costgen4
256       in
257       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
258       costgen5 }
259     | Csyntax.Tint (sz, sg) ->
260       let { Types.fst = et; Types.snd = costgen2 } =
261         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
262       in
263       let { Types.fst = ef; Types.snd = costgen3 } =
264         add_cost_expr (const_int sz Nat.O) costgen2
265       in
266       let { Types.fst = e21; Types.snd = costgen4 } =
267         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
268           ty)) costgen3
269       in
270       let { Types.fst = ef0; Types.snd = costgen5 } =
271         add_cost_expr (const_int sz Nat.O) costgen4
272       in
273       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
274       costgen5 }
275     | Csyntax.Tpointer x ->
276       let { Types.fst = et; Types.snd = costgen2 } =
277         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
278       in
279       let { Types.fst = ef; Types.snd = costgen3 } =
280         add_cost_expr (const_int AST.I32 Nat.O) costgen2
281       in
282       let { Types.fst = e21; Types.snd = costgen4 } =
283         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
284           ty)) costgen3
285       in
286       let { Types.fst = ef0; Types.snd = costgen5 } =
287         add_cost_expr (const_int AST.I32 Nat.O) costgen4
288       in
289       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
290       costgen5 }
291     | Csyntax.Tarray (x, x0) ->
292       let { Types.fst = et; Types.snd = costgen2 } =
293         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
294       in
295       let { Types.fst = ef; Types.snd = costgen3 } =
296         add_cost_expr (const_int AST.I32 Nat.O) costgen2
297       in
298       let { Types.fst = e21; Types.snd = costgen4 } =
299         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
300           ty)) costgen3
301       in
302       let { Types.fst = ef0; Types.snd = costgen5 } =
303         add_cost_expr (const_int AST.I32 Nat.O) costgen4
304       in
305       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
306       costgen5 }
307     | Csyntax.Tfunction (x, x0) ->
308       let { Types.fst = et; Types.snd = costgen2 } =
309         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
310       in
311       let { Types.fst = ef; Types.snd = costgen3 } =
312         add_cost_expr (const_int AST.I32 Nat.O) costgen2
313       in
314       let { Types.fst = e21; Types.snd = costgen4 } =
315         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
316           ty)) costgen3
317       in
318       let { Types.fst = ef0; Types.snd = costgen5 } =
319         add_cost_expr (const_int AST.I32 Nat.O) costgen4
320       in
321       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
322       costgen5 }
323     | Csyntax.Tstruct (x, x0) ->
324       let { Types.fst = et; Types.snd = costgen2 } =
325         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
326       in
327       let { Types.fst = ef; Types.snd = costgen3 } =
328         add_cost_expr (const_int AST.I32 Nat.O) costgen2
329       in
330       let { Types.fst = e21; Types.snd = costgen4 } =
331         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
332           ty)) costgen3
333       in
334       let { Types.fst = ef0; Types.snd = costgen5 } =
335         add_cost_expr (const_int AST.I32 Nat.O) costgen4
336       in
337       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
338       costgen5 }
339     | Csyntax.Tunion (x, x0) ->
340       let { Types.fst = et; Types.snd = costgen2 } =
341         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
342       in
343       let { Types.fst = ef; Types.snd = costgen3 } =
344         add_cost_expr (const_int AST.I32 Nat.O) costgen2
345       in
346       let { Types.fst = e21; Types.snd = costgen4 } =
347         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
348           ty)) costgen3
349       in
350       let { Types.fst = ef0; Types.snd = costgen5 } =
351         add_cost_expr (const_int AST.I32 Nat.O) costgen4
352       in
353       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
354       costgen5 }
355     | Csyntax.Tcomp_ptr x ->
356       let { Types.fst = et; Types.snd = costgen2 } =
357         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
358       in
359       let { Types.fst = ef; Types.snd = costgen3 } =
360         add_cost_expr (const_int AST.I32 Nat.O) costgen2
361       in
362       let { Types.fst = e21; Types.snd = costgen4 } =
363         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
364           ty)) costgen3
365       in
366       let { Types.fst = ef0; Types.snd = costgen5 } =
367         add_cost_expr (const_int AST.I32 Nat.O) costgen4
368       in
369       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
370       costgen5 })
371  | Csyntax.Eorbool (e1, e2) ->
372    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
373    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
374    (match ty with
375     | Csyntax.Tvoid ->
376       let { Types.fst = et; Types.snd = costgen2 } =
377         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
378       in
379       let { Types.fst = ef; Types.snd = costgen3 } =
380         add_cost_expr (const_int AST.I32 Nat.O) costgen2
381       in
382       let { Types.fst = e21; Types.snd = costgen4 } =
383         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
384           ty)) costgen3
385       in
386       let { Types.fst = et0; Types.snd = costgen5 } =
387         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
388       in
389       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
390       costgen5 }
391     | Csyntax.Tint (sz, sg) ->
392       let { Types.fst = et; Types.snd = costgen2 } =
393         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen1
394       in
395       let { Types.fst = ef; Types.snd = costgen3 } =
396         add_cost_expr (const_int sz Nat.O) costgen2
397       in
398       let { Types.fst = e21; Types.snd = costgen4 } =
399         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
400           ty)) costgen3
401       in
402       let { Types.fst = et0; Types.snd = costgen5 } =
403         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen4
404       in
405       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
406       costgen5 }
407     | Csyntax.Tpointer x ->
408       let { Types.fst = et; Types.snd = costgen2 } =
409         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
410       in
411       let { Types.fst = ef; Types.snd = costgen3 } =
412         add_cost_expr (const_int AST.I32 Nat.O) costgen2
413       in
414       let { Types.fst = e21; Types.snd = costgen4 } =
415         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
416           ty)) costgen3
417       in
418       let { Types.fst = et0; Types.snd = costgen5 } =
419         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
420       in
421       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
422       costgen5 }
423     | Csyntax.Tarray (x, x0) ->
424       let { Types.fst = et; Types.snd = costgen2 } =
425         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
426       in
427       let { Types.fst = ef; Types.snd = costgen3 } =
428         add_cost_expr (const_int AST.I32 Nat.O) costgen2
429       in
430       let { Types.fst = e21; Types.snd = costgen4 } =
431         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
432           ty)) costgen3
433       in
434       let { Types.fst = et0; Types.snd = costgen5 } =
435         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
436       in
437       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
438       costgen5 }
439     | Csyntax.Tfunction (x, x0) ->
440       let { Types.fst = et; Types.snd = costgen2 } =
441         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
442       in
443       let { Types.fst = ef; Types.snd = costgen3 } =
444         add_cost_expr (const_int AST.I32 Nat.O) costgen2
445       in
446       let { Types.fst = e21; Types.snd = costgen4 } =
447         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
448           ty)) costgen3
449       in
450       let { Types.fst = et0; Types.snd = costgen5 } =
451         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
452       in
453       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
454       costgen5 }
455     | Csyntax.Tstruct (x, x0) ->
456       let { Types.fst = et; Types.snd = costgen2 } =
457         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
458       in
459       let { Types.fst = ef; Types.snd = costgen3 } =
460         add_cost_expr (const_int AST.I32 Nat.O) costgen2
461       in
462       let { Types.fst = e21; Types.snd = costgen4 } =
463         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
464           ty)) costgen3
465       in
466       let { Types.fst = et0; Types.snd = costgen5 } =
467         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
468       in
469       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
470       costgen5 }
471     | Csyntax.Tunion (x, x0) ->
472       let { Types.fst = et; Types.snd = costgen2 } =
473         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
474       in
475       let { Types.fst = ef; Types.snd = costgen3 } =
476         add_cost_expr (const_int AST.I32 Nat.O) costgen2
477       in
478       let { Types.fst = e21; Types.snd = costgen4 } =
479         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
480           ty)) costgen3
481       in
482       let { Types.fst = et0; Types.snd = costgen5 } =
483         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
484       in
485       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
486       costgen5 }
487     | Csyntax.Tcomp_ptr x ->
488       let { Types.fst = et; Types.snd = costgen2 } =
489         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
490       in
491       let { Types.fst = ef; Types.snd = costgen3 } =
492         add_cost_expr (const_int AST.I32 Nat.O) costgen2
493       in
494       let { Types.fst = e21; Types.snd = costgen4 } =
495         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
496           ty)) costgen3
497       in
498       let { Types.fst = et0; Types.snd = costgen5 } =
499         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
500       in
501       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
502       costgen5 })
503  | Csyntax.Esizeof x -> { Types.fst = e0; Types.snd = costgen }
504  | Csyntax.Efield (e', id) ->
505    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
506    { Types.fst = (Csyntax.Efield (e'0, id)); Types.snd = costgen0 }
507  | Csyntax.Ecost (l, e') ->
508    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
509    { Types.fst = (Csyntax.Ecost (l, e'0)); Types.snd = costgen0 }
510
511(** val label_exprs :
512    Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr
513    List.list, Identifiers.universe) Types.prod **)
514let rec label_exprs l costgen =
515  match l with
516  | List.Nil -> { Types.fst = List.Nil; Types.snd = costgen }
517  | List.Cons (e0, es) ->
518    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
519    let { Types.fst = es0; Types.snd = costgen1 } = label_exprs es costgen0
520    in
521    { Types.fst = (List.Cons (e1, es0)); Types.snd = costgen1 }
522
523(** val label_opt_expr :
524    Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
525    Types.option, Identifiers.universe) Types.prod **)
526let label_opt_expr oe costgen =
527  match oe with
528  | Types.None -> { Types.fst = Types.None; Types.snd = costgen }
529  | Types.Some e0 ->
530    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
531    { Types.fst = (Types.Some e1); Types.snd = costgen0 }
532
533(** val label_statement :
534    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
535    Identifiers.universe) Types.prod **)
536let rec label_statement s costgen =
537  match s with
538  | Csyntax.Sskip -> { Types.fst = Csyntax.Sskip; Types.snd = costgen }
539  | Csyntax.Sassign (e1, e2) ->
540    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
541    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
542    { Types.fst = (Csyntax.Sassign (e10, e20)); Types.snd = costgen1 }
543  | Csyntax.Scall (e_ret, e_fn, e_args) ->
544    let { Types.fst = e_ret0; Types.snd = costgen0 } =
545      label_opt_expr e_ret costgen
546    in
547    let { Types.fst = e_fn0; Types.snd = costgen1 } =
548      label_expr e_fn costgen0
549    in
550    let { Types.fst = e_args0; Types.snd = costgen2 } =
551      label_exprs e_args costgen1
552    in
553    { Types.fst = (Csyntax.Scall (e_ret0, e_fn0, e_args0)); Types.snd =
554    costgen2 }
555  | Csyntax.Ssequence (s1, s2) ->
556    let { Types.fst = s10; Types.snd = costgen0 } =
557      label_statement s1 costgen
558    in
559    let { Types.fst = s20; Types.snd = costgen1 } =
560      label_statement s2 costgen0
561    in
562    { Types.fst = (Csyntax.Ssequence (s10, s20)); Types.snd = costgen1 }
563  | Csyntax.Sifthenelse (e0, s1, s2) ->
564    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
565    let { Types.fst = s10; Types.snd = costgen1 } =
566      label_statement s1 costgen0
567    in
568    let { Types.fst = s11; Types.snd = costgen2 } =
569      add_cost_before s10 costgen1
570    in
571    let { Types.fst = s20; Types.snd = costgen3 } =
572      label_statement s2 costgen2
573    in
574    let { Types.fst = s21; Types.snd = costgen4 } =
575      add_cost_before s20 costgen3
576    in
577    { Types.fst = (Csyntax.Sifthenelse (e1, s11, s21)); Types.snd =
578    costgen4 }
579  | Csyntax.Swhile (e0, s') ->
580    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
581    let { Types.fst = s'0; Types.snd = costgen1 } =
582      label_statement s' costgen0
583    in
584    let { Types.fst = s'1; Types.snd = costgen2 } =
585      add_cost_before s'0 costgen1
586    in
587    let { Types.fst = s0; Types.snd = costgen3 } =
588      add_cost_after (Csyntax.Swhile (e1, s'1)) costgen2
589    in
590    { Types.fst = s0; Types.snd = costgen3 }
591  | Csyntax.Sdowhile (e0, s') ->
592    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
593    let { Types.fst = s'0; Types.snd = costgen1 } =
594      label_statement s' costgen0
595    in
596    let { Types.fst = s'1; Types.snd = costgen2 } =
597      add_cost_before s'0 costgen1
598    in
599    let { Types.fst = s0; Types.snd = costgen3 } =
600      add_cost_after (Csyntax.Sdowhile (e1, s'1)) costgen2
601    in
602    { Types.fst = s0; Types.snd = costgen3 }
603  | Csyntax.Sfor (s1, e0, s2, s3) ->
604    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
605    let { Types.fst = s10; Types.snd = costgen1 } =
606      label_statement s1 costgen0
607    in
608    let { Types.fst = s20; Types.snd = costgen2 } =
609      label_statement s2 costgen1
610    in
611    let { Types.fst = s30; Types.snd = costgen3 } =
612      label_statement s3 costgen2
613    in
614    let { Types.fst = s31; Types.snd = costgen4 } =
615      add_cost_before s30 costgen3
616    in
617    let { Types.fst = s0; Types.snd = costgen5 } =
618      add_cost_after (Csyntax.Sfor (s10, e1, s20, s31)) costgen4
619    in
620    { Types.fst = s0; Types.snd = costgen5 }
621  | Csyntax.Sbreak -> { Types.fst = Csyntax.Sbreak; Types.snd = costgen }
622  | Csyntax.Scontinue ->
623    { Types.fst = Csyntax.Scontinue; Types.snd = costgen }
624  | Csyntax.Sreturn opt_e ->
625    let { Types.fst = opt_e0; Types.snd = costgen0 } =
626      label_opt_expr opt_e costgen
627    in
628    { Types.fst = (Csyntax.Sreturn opt_e0); Types.snd = costgen0 }
629  | Csyntax.Sswitch (e0, ls) ->
630    let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
631    let { Types.fst = ls0; Types.snd = costgen1 } =
632      label_lstatements ls costgen0
633    in
634    { Types.fst = (Csyntax.Sswitch (e1, ls0)); Types.snd = costgen1 }
635  | Csyntax.Slabel (l, s') ->
636    let { Types.fst = s'0; Types.snd = costgen0 } =
637      label_statement s' costgen
638    in
639    let { Types.fst = s'1; Types.snd = costgen1 } =
640      add_cost_before s'0 costgen0
641    in
642    { Types.fst = (Csyntax.Slabel (l, s'1)); Types.snd = costgen1 }
643  | Csyntax.Sgoto l -> { Types.fst = (Csyntax.Sgoto l); Types.snd = costgen }
644  | Csyntax.Scost (l, s') ->
645    let { Types.fst = s'0; Types.snd = costgen0 } =
646      label_statement s' costgen
647    in
648    { Types.fst = (Csyntax.Scost (l, s'0)); Types.snd = costgen0 }
649(** val label_lstatements :
650    Csyntax.labeled_statements -> Identifiers.universe ->
651    (Csyntax.labeled_statements, Identifiers.universe) Types.prod **)
652and label_lstatements ls costgen =
653  match ls with
654  | Csyntax.LSdefault s ->
655    let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
656    in
657    let { Types.fst = s1; Types.snd = costgen1 } =
658      add_cost_before s0 costgen0
659    in
660    { Types.fst = (Csyntax.LSdefault s1); Types.snd = costgen1 }
661  | Csyntax.LScase (sz, i, s, ls') ->
662    let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
663    in
664    let { Types.fst = s1; Types.snd = costgen1 } =
665      add_cost_before s0 costgen0
666    in
667    let { Types.fst = ls'0; Types.snd = costgen2 } =
668      label_lstatements ls' costgen1
669    in
670    { Types.fst = (Csyntax.LScase (sz, i, s1, ls'0)); Types.snd = costgen2 }
671
672(** val label_function :
673    Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
674    Identifiers.universe) Types.prod **)
675let label_function costgen f =
676  let { Types.fst = body; Types.snd = costgen0 } =
677    label_statement f.Csyntax.fn_body costgen
678  in
679  let { Types.fst = body0; Types.snd = costgen1 } =
680    add_cost_before body costgen0
681  in
682  { Types.fst = { Csyntax.fn_return = f.Csyntax.fn_return;
683  Csyntax.fn_params = f.Csyntax.fn_params; Csyntax.fn_vars =
684  f.Csyntax.fn_vars; Csyntax.fn_body = body0 }; Types.snd = costgen1 }
685
686(** val label_fundef :
687    Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
688    Identifiers.universe) Types.prod **)
689let label_fundef gen = function
690| Csyntax.CL_Internal f0 ->
691  let { Types.fst = f'; Types.snd = gen' } = label_function gen f0 in
692  { Types.fst = (Csyntax.CL_Internal f'); Types.snd = gen' }
693| Csyntax.CL_External (id, args, ty) ->
694  { Types.fst = (Csyntax.CL_External (id, args, ty)); Types.snd = gen }
695
696(** val clight_label :
697    Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
698    Types.prod **)
699let clight_label p =
700  let costgen = Identifiers.new_universe PreIdentifiers.CostTag in
701  let { Types.fst = init_cost; Types.snd = costgen0 } =
702    Identifiers.fresh PreIdentifiers.CostTag costgen
703  in
704  { Types.fst =
705  (AST.transform_program_gen PreIdentifiers.CostTag costgen0 p (fun x ->
706    label_fundef)).Types.fst; Types.snd = init_cost }
707
Note: See TracBrowser for help on using the repository browser.