source: driver/extracted/label.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 26.0 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 Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77(** val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list **)
78let rec labels_of_expr = function
79| Csyntax.Expr (e', x) ->
80  (match e' with
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)))
99
100(** val labels_of_statement :
101    Csyntax.statement -> CostLabel.costlabel List.list **)
102let 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
110        es))
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 **)
134and 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)
138
139(** val labels_of_clight_fundef :
140    (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
141    List.list **)
142let 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
146
147(** val labels_of_clight :
148    Csyntax.clight_program -> CostLabel.costlabel List.list **)
149let 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
152
153type in_clight_label = CostLabel.costlabel Types.sig0
154
155type clight_cost_map = CostLabel.costlabel -> Nat.nat
156
157(** val clight_label_free : Csyntax.clight_program -> Bool.bool **)
158let clight_label_free p =
159  match labels_of_clight p with
160  | List.Nil -> Bool.True
161  | List.Cons (x, x0) -> Bool.False
162
163(** val add_cost_before :
164    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
165    Identifiers.universe) Types.prod **)
166let add_cost_before s gen =
167  let { Types.fst = l; Types.snd = gen0 } =
168    Identifiers.fresh PreIdentifiers.CostTag gen
169  in
170  { Types.fst = (Csyntax.Scost (l, s)); Types.snd = gen0 }
171
172(** val add_cost_after :
173    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
174    Identifiers.universe) Types.prod **)
175let add_cost_after s gen =
176  let { Types.fst = l; Types.snd = gen0 } =
177    Identifiers.fresh PreIdentifiers.CostTag gen
178  in
179  { Types.fst = (Csyntax.Ssequence (s, (Csyntax.Scost (l, Csyntax.Sskip))));
180  Types.snd = gen0 }
181
182(** val add_cost_expr :
183    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
184    Identifiers.universe) Types.prod **)
185let add_cost_expr e gen =
186  let { Types.fst = l; Types.snd = gen0 } =
187    Identifiers.fresh PreIdentifiers.CostTag gen
188  in
189  { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e)), (Csyntax.typeof e)));
190  Types.snd = gen0 }
191
192(** val const_int : AST.intsize -> Nat.nat -> Csyntax.expr **)
193let const_int sz n =
194  Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr sz n))), (Csyntax.Tint
195    (sz, AST.Signed)))
196
197(** val label_expr :
198    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
199    Identifiers.universe) Types.prod **)
200let 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
204  in
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 **)
209and label_expr_descr e costgen ty =
210  match e with
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
234    in
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
238    in
239    { Types.fst = (Csyntax.Econdition (e'0, e11, e21)); Types.snd =
240    costgen4 }
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
244    (match ty with
245     | Csyntax.Tvoid ->
246       let { Types.fst = et; Types.snd = costgen2 } =
247         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
248       in
249       let { Types.fst = ef; Types.snd = costgen3 } =
250         add_cost_expr (const_int AST.I32 Nat.O) costgen2
251       in
252       let { Types.fst = e21; Types.snd = costgen4 } =
253         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
254           ty)) costgen3
255       in
256       let { Types.fst = ef0; Types.snd = costgen5 } =
257         add_cost_expr (const_int AST.I32 Nat.O) costgen4
258       in
259       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
260       costgen5 }
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
264       in
265       let { Types.fst = ef; Types.snd = costgen3 } =
266         add_cost_expr (const_int sz Nat.O) costgen2
267       in
268       let { Types.fst = e21; Types.snd = costgen4 } =
269         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
270           ty)) costgen3
271       in
272       let { Types.fst = ef0; Types.snd = costgen5 } =
273         add_cost_expr (const_int sz Nat.O) costgen4
274       in
275       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
276       costgen5 }
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
280       in
281       let { Types.fst = ef; Types.snd = costgen3 } =
282         add_cost_expr (const_int AST.I32 Nat.O) costgen2
283       in
284       let { Types.fst = e21; Types.snd = costgen4 } =
285         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
286           ty)) costgen3
287       in
288       let { Types.fst = ef0; Types.snd = costgen5 } =
289         add_cost_expr (const_int AST.I32 Nat.O) costgen4
290       in
291       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
292       costgen5 }
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
296       in
297       let { Types.fst = ef; Types.snd = costgen3 } =
298         add_cost_expr (const_int AST.I32 Nat.O) costgen2
299       in
300       let { Types.fst = e21; Types.snd = costgen4 } =
301         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
302           ty)) costgen3
303       in
304       let { Types.fst = ef0; Types.snd = costgen5 } =
305         add_cost_expr (const_int AST.I32 Nat.O) costgen4
306       in
307       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
308       costgen5 }
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
312       in
313       let { Types.fst = ef; Types.snd = costgen3 } =
314         add_cost_expr (const_int AST.I32 Nat.O) costgen2
315       in
316       let { Types.fst = e21; Types.snd = costgen4 } =
317         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
318           ty)) costgen3
319       in
320       let { Types.fst = ef0; Types.snd = costgen5 } =
321         add_cost_expr (const_int AST.I32 Nat.O) costgen4
322       in
323       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
324       costgen5 }
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
328       in
329       let { Types.fst = ef; Types.snd = costgen3 } =
330         add_cost_expr (const_int AST.I32 Nat.O) costgen2
331       in
332       let { Types.fst = e21; Types.snd = costgen4 } =
333         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
334           ty)) costgen3
335       in
336       let { Types.fst = ef0; Types.snd = costgen5 } =
337         add_cost_expr (const_int AST.I32 Nat.O) costgen4
338       in
339       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
340       costgen5 }
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
344       in
345       let { Types.fst = ef; Types.snd = costgen3 } =
346         add_cost_expr (const_int AST.I32 Nat.O) costgen2
347       in
348       let { Types.fst = e21; Types.snd = costgen4 } =
349         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
350           ty)) costgen3
351       in
352       let { Types.fst = ef0; Types.snd = costgen5 } =
353         add_cost_expr (const_int AST.I32 Nat.O) costgen4
354       in
355       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
356       costgen5 }
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
360       in
361       let { Types.fst = ef; Types.snd = costgen3 } =
362         add_cost_expr (const_int AST.I32 Nat.O) costgen2
363       in
364       let { Types.fst = e21; Types.snd = costgen4 } =
365         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
366           ty)) costgen3
367       in
368       let { Types.fst = ef0; Types.snd = costgen5 } =
369         add_cost_expr (const_int AST.I32 Nat.O) costgen4
370       in
371       { Types.fst = (Csyntax.Econdition (e10, e21, ef0)); Types.snd =
372       costgen5 })
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
376    (match ty with
377     | Csyntax.Tvoid ->
378       let { Types.fst = et; Types.snd = costgen2 } =
379         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen1
380       in
381       let { Types.fst = ef; Types.snd = costgen3 } =
382         add_cost_expr (const_int AST.I32 Nat.O) costgen2
383       in
384       let { Types.fst = e21; Types.snd = costgen4 } =
385         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
386           ty)) costgen3
387       in
388       let { Types.fst = et0; Types.snd = costgen5 } =
389         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
390       in
391       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
392       costgen5 }
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
396       in
397       let { Types.fst = ef; Types.snd = costgen3 } =
398         add_cost_expr (const_int sz Nat.O) costgen2
399       in
400       let { Types.fst = e21; Types.snd = costgen4 } =
401         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
402           ty)) costgen3
403       in
404       let { Types.fst = et0; Types.snd = costgen5 } =
405         add_cost_expr (const_int sz (Nat.S Nat.O)) costgen4
406       in
407       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
408       costgen5 }
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
412       in
413       let { Types.fst = ef; Types.snd = costgen3 } =
414         add_cost_expr (const_int AST.I32 Nat.O) costgen2
415       in
416       let { Types.fst = e21; Types.snd = costgen4 } =
417         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
418           ty)) costgen3
419       in
420       let { Types.fst = et0; Types.snd = costgen5 } =
421         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
422       in
423       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
424       costgen5 }
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
428       in
429       let { Types.fst = ef; Types.snd = costgen3 } =
430         add_cost_expr (const_int AST.I32 Nat.O) costgen2
431       in
432       let { Types.fst = e21; Types.snd = costgen4 } =
433         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
434           ty)) costgen3
435       in
436       let { Types.fst = et0; Types.snd = costgen5 } =
437         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
438       in
439       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
440       costgen5 }
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
444       in
445       let { Types.fst = ef; Types.snd = costgen3 } =
446         add_cost_expr (const_int AST.I32 Nat.O) costgen2
447       in
448       let { Types.fst = e21; Types.snd = costgen4 } =
449         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
450           ty)) costgen3
451       in
452       let { Types.fst = et0; Types.snd = costgen5 } =
453         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
454       in
455       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
456       costgen5 }
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
460       in
461       let { Types.fst = ef; Types.snd = costgen3 } =
462         add_cost_expr (const_int AST.I32 Nat.O) costgen2
463       in
464       let { Types.fst = e21; Types.snd = costgen4 } =
465         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
466           ty)) costgen3
467       in
468       let { Types.fst = et0; Types.snd = costgen5 } =
469         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
470       in
471       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
472       costgen5 }
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
476       in
477       let { Types.fst = ef; Types.snd = costgen3 } =
478         add_cost_expr (const_int AST.I32 Nat.O) costgen2
479       in
480       let { Types.fst = e21; Types.snd = costgen4 } =
481         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
482           ty)) costgen3
483       in
484       let { Types.fst = et0; Types.snd = costgen5 } =
485         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
486       in
487       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
488       costgen5 }
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
492       in
493       let { Types.fst = ef; Types.snd = costgen3 } =
494         add_cost_expr (const_int AST.I32 Nat.O) costgen2
495       in
496       let { Types.fst = e21; Types.snd = costgen4 } =
497         add_cost_expr (Csyntax.Expr ((Csyntax.Econdition (e20, et, ef)),
498           ty)) costgen3
499       in
500       let { Types.fst = et0; Types.snd = costgen5 } =
501         add_cost_expr (const_int AST.I32 (Nat.S Nat.O)) costgen4
502       in
503       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
504       costgen5 })
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 }
512
513(** val label_exprs :
514    Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr
515    List.list, Identifiers.universe) Types.prod **)
516let rec label_exprs l costgen =
517  match l with
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
522    in
523    { Types.fst = (List.Cons (e0, es0)); Types.snd = costgen1 }
524
525(** val label_opt_expr :
526    Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
527    Types.option, Identifiers.universe) Types.prod **)
528let label_opt_expr oe costgen =
529  match oe with
530  | Types.None -> { Types.fst = Types.None; Types.snd = costgen }
531  | Types.Some e ->
532    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
533    { Types.fst = (Types.Some e0); Types.snd = costgen0 }
534
535(** val label_statement :
536    Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
537    Identifiers.universe) Types.prod **)
538let rec label_statement s costgen =
539  match s with
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
548    in
549    let { Types.fst = e_fn0; Types.snd = costgen1 } =
550      label_expr e_fn costgen0
551    in
552    let { Types.fst = e_args0; Types.snd = costgen2 } =
553      label_exprs e_args costgen1
554    in
555    { Types.fst = (Csyntax.Scall (e_ret0, e_fn0, e_args0)); Types.snd =
556    costgen2 }
557  | Csyntax.Ssequence (s1, s2) ->
558    let { Types.fst = s10; Types.snd = costgen0 } =
559      label_statement s1 costgen
560    in
561    let { Types.fst = s20; Types.snd = costgen1 } =
562      label_statement s2 costgen0
563    in
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
569    in
570    let { Types.fst = s11; Types.snd = costgen2 } =
571      add_cost_before s10 costgen1
572    in
573    let { Types.fst = s20; Types.snd = costgen3 } =
574      label_statement s2 costgen2
575    in
576    let { Types.fst = s21; Types.snd = costgen4 } =
577      add_cost_before s20 costgen3
578    in
579    { Types.fst = (Csyntax.Sifthenelse (e0, s11, s21)); Types.snd =
580    costgen4 }
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
585    in
586    let { Types.fst = s'1; Types.snd = costgen2 } =
587      add_cost_before s'0 costgen1
588    in
589    let { Types.fst = s0; Types.snd = costgen3 } =
590      add_cost_after (Csyntax.Swhile (e0, s'1)) costgen2
591    in
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
597    in
598    let { Types.fst = s'1; Types.snd = costgen2 } =
599      add_cost_before s'0 costgen1
600    in
601    let { Types.fst = s0; Types.snd = costgen3 } =
602      add_cost_after (Csyntax.Sdowhile (e0, s'1)) costgen2
603    in
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
609    in
610    let { Types.fst = s20; Types.snd = costgen2 } =
611      label_statement s2 costgen1
612    in
613    let { Types.fst = s30; Types.snd = costgen3 } =
614      label_statement s3 costgen2
615    in
616    let { Types.fst = s31; Types.snd = costgen4 } =
617      add_cost_before s30 costgen3
618    in
619    let { Types.fst = s0; Types.snd = costgen5 } =
620      add_cost_after (Csyntax.Sfor (s10, e0, s20, s31)) costgen4
621    in
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
629    in
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
635    in
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
640    in
641    let { Types.fst = s'1; Types.snd = costgen1 } =
642      add_cost_before s'0 costgen0
643    in
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
649    in
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 **)
654and label_lstatements ls costgen =
655  match ls with
656  | Csyntax.LSdefault s ->
657    let { Types.fst = s0; Types.snd = costgen0 } = label_statement s costgen
658    in
659    let { Types.fst = s1; Types.snd = costgen1 } =
660      add_cost_before s0 costgen0
661    in
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
665    in
666    let { Types.fst = s1; Types.snd = costgen1 } =
667      add_cost_before s0 costgen0
668    in
669    let { Types.fst = ls'0; Types.snd = costgen2 } =
670      label_lstatements ls' costgen1
671    in
672    { Types.fst = (Csyntax.LScase (sz, i, s1, ls'0)); Types.snd = costgen2 }
673
674(** val label_function :
675    Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
676    Identifiers.universe) Types.prod **)
677let label_function costgen f =
678  let { Types.fst = body; Types.snd = costgen0 } =
679    label_statement f.Csyntax.fn_body costgen
680  in
681  let { Types.fst = body0; Types.snd = costgen1 } =
682    add_cost_before body costgen0
683  in
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 }
687
688(** val label_fundef :
689    Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
690    Identifiers.universe) Types.prod **)
691let 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 }
697
698(** val clight_label :
699    Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
700    Types.prod **)
701let 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
705  in
706  { Types.fst =
707  (AST.transform_program_gen PreIdentifiers.CostTag costgen0 p (fun x ->
708    label_fundef)).Types.fst; Types.snd = init_cost }
709
Note: See TracBrowser for help on using the repository browser.