source: extracted/label.ml @ 2731

Last change on this file since 2731 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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