1 | |
---|
2 | (** This module defines the labelling of a [Clight] program. *) |
---|
3 | |
---|
4 | open Clight |
---|
5 | open CostLabel |
---|
6 | |
---|
7 | |
---|
8 | (* Add a cost label in front of a statement. *) |
---|
9 | |
---|
10 | let add_starting_cost_label cost_universe stmt = |
---|
11 | Clight.Scost (CostLabel.Gen.fresh cost_universe, stmt) |
---|
12 | |
---|
13 | (* Add a cost label at the end of a statement. *) |
---|
14 | |
---|
15 | let add_ending_cost_label cost_universe stmt = |
---|
16 | Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip) |
---|
17 | |
---|
18 | |
---|
19 | let int_type = Tint (I32, AST.Signed) |
---|
20 | let const_int i = Expr (Econst_int i, int_type) |
---|
21 | |
---|
22 | |
---|
23 | let typeof e = let Expr (_,t) = e in t |
---|
24 | |
---|
25 | |
---|
26 | let add_cost_label_e cost_universe e = |
---|
27 | Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e) |
---|
28 | |
---|
29 | |
---|
30 | (* Add cost labels to an expression. *) |
---|
31 | |
---|
32 | let rec add_cost_labels_e cost_universe = function |
---|
33 | | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty) |
---|
34 | |
---|
35 | and add_cost_labels_expr cost_universe exp = match exp with |
---|
36 | | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp |
---|
37 | | Ederef e -> Ederef (add_cost_labels_e cost_universe e) |
---|
38 | | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e) |
---|
39 | | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e)) |
---|
40 | | Ebinop (op,e1,e2) -> |
---|
41 | Ebinop (op, |
---|
42 | add_cost_labels_e cost_universe e1, |
---|
43 | add_cost_labels_e cost_universe e2) |
---|
44 | | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e) |
---|
45 | | Eandbool (e1,e2) -> |
---|
46 | let e1' = add_cost_labels_e cost_universe e1 in |
---|
47 | let e2' = add_cost_labels_e cost_universe e2 in |
---|
48 | let b1 = add_cost_label_e cost_universe (const_int 1) in |
---|
49 | let b2 = add_cost_label_e cost_universe (const_int 0) in |
---|
50 | let e2' = Expr (Econdition (e2', b1, b2), int_type) in |
---|
51 | let e2' = add_cost_label_e cost_universe e2' in |
---|
52 | let e3' = add_cost_label_e cost_universe (const_int 0) in |
---|
53 | Econdition (e1', e2', e3') |
---|
54 | | Eorbool (e1,e2) -> |
---|
55 | let e1' = add_cost_labels_e cost_universe e1 in |
---|
56 | let e2' = add_cost_label_e cost_universe (const_int 1) in |
---|
57 | let e3' = add_cost_labels_e cost_universe e2 in |
---|
58 | let b1 = add_cost_label_e cost_universe (const_int 1) in |
---|
59 | let b2 = add_cost_label_e cost_universe (const_int 0) in |
---|
60 | let e3' = Expr (Econdition (e3', b1, b2), int_type) in |
---|
61 | let e3' = add_cost_label_e cost_universe e3' in |
---|
62 | Econdition (e1', e2', e3') |
---|
63 | | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id) |
---|
64 | | Econdition (e1,e2,e3) -> |
---|
65 | let e1' = add_cost_labels_e cost_universe e1 in |
---|
66 | let e2' = add_cost_labels_e cost_universe e2 in |
---|
67 | let e2' = add_cost_label_e cost_universe e2' in |
---|
68 | let e3' = add_cost_labels_e cost_universe e3 in |
---|
69 | let e3' = add_cost_label_e cost_universe e3' in |
---|
70 | Econdition (e1', e2', e3') |
---|
71 | | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *) |
---|
72 | |
---|
73 | let add_cost_labels_opt cost_universe = function |
---|
74 | | None -> None |
---|
75 | | Some e -> Some (add_cost_labels_e cost_universe e) |
---|
76 | |
---|
77 | let add_cost_labels_lst cost_universe l = |
---|
78 | List.map (add_cost_labels_e cost_universe) l |
---|
79 | |
---|
80 | |
---|
81 | (* Add cost labels to a statement. *) |
---|
82 | |
---|
83 | let rec add_cost_labels_st cost_universe = function |
---|
84 | | Sskip -> Sskip |
---|
85 | | Sassign (e1,e2) -> |
---|
86 | Sassign (add_cost_labels_e cost_universe e1, |
---|
87 | add_cost_labels_e cost_universe e2) |
---|
88 | | Scall (e1,e2,lst) -> |
---|
89 | Scall (add_cost_labels_opt cost_universe e1, |
---|
90 | add_cost_labels_e cost_universe e2, |
---|
91 | add_cost_labels_lst cost_universe lst) |
---|
92 | | Ssequence (s1,s2) -> |
---|
93 | Ssequence (add_cost_labels_st cost_universe s1, |
---|
94 | add_cost_labels_st cost_universe s2) |
---|
95 | | Sifthenelse (e,s1,s2) -> |
---|
96 | let s1' = add_cost_labels_st cost_universe s1 in |
---|
97 | let s1' = add_starting_cost_label cost_universe s1' in |
---|
98 | let s2' = add_cost_labels_st cost_universe s2 in |
---|
99 | let s2' = add_starting_cost_label cost_universe s2' in |
---|
100 | Sifthenelse (add_cost_labels_e cost_universe e, s1', s2') |
---|
101 | | Swhile (e,s) -> |
---|
102 | let s' = add_cost_labels_st cost_universe s in |
---|
103 | let s' = add_starting_cost_label cost_universe s' in |
---|
104 | add_ending_cost_label cost_universe |
---|
105 | (Swhile (add_cost_labels_e cost_universe e, s')) |
---|
106 | | Sdowhile (e,s) -> |
---|
107 | let s1 = add_cost_labels_st cost_universe s in |
---|
108 | let s2 = add_cost_labels_st cost_universe s in |
---|
109 | let s2' = add_starting_cost_label cost_universe s2 in |
---|
110 | add_ending_cost_label cost_universe |
---|
111 | (Ssequence (s1, Swhile (add_cost_labels_e cost_universe e, s2'))) |
---|
112 | | Sfor (s1,e,s2,s3) -> |
---|
113 | let s1' = add_cost_labels_st cost_universe s1 in |
---|
114 | let s2' = add_cost_labels_st cost_universe s2 in |
---|
115 | let s3' = add_cost_labels_st cost_universe s3 in |
---|
116 | let s3' = add_starting_cost_label cost_universe s3' in |
---|
117 | add_ending_cost_label cost_universe |
---|
118 | (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3')) |
---|
119 | | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e) |
---|
120 | | Sswitch (e,ls) -> |
---|
121 | Sswitch (add_cost_labels_e cost_universe e, |
---|
122 | add_cost_labels_ls cost_universe ls) |
---|
123 | | Slabel (lbl,s) -> |
---|
124 | let s' = add_cost_labels_st cost_universe s in |
---|
125 | let s' = add_starting_cost_label cost_universe s' in |
---|
126 | Slabel (lbl,s') |
---|
127 | | Scost (_,_) -> assert false |
---|
128 | | _ as stmt -> stmt |
---|
129 | |
---|
130 | and add_cost_labels_ls cost_universe = function |
---|
131 | | LSdefault s -> |
---|
132 | let s' = add_cost_labels_st cost_universe s in |
---|
133 | let s' = add_starting_cost_label cost_universe s' in |
---|
134 | LSdefault s' |
---|
135 | | LScase (i,s,ls) -> |
---|
136 | let s' = add_cost_labels_st cost_universe s in |
---|
137 | let s' = add_starting_cost_label cost_universe s' in |
---|
138 | LScase (i, s', add_cost_labels_ls cost_universe ls) |
---|
139 | |
---|
140 | |
---|
141 | (* Add cost labels to a function. *) |
---|
142 | |
---|
143 | let add_cost_labels_f cost_universe = function |
---|
144 | | (id,Internal fd) -> (id,Internal { |
---|
145 | fn_return = fd.fn_return ; |
---|
146 | fn_params = fd.fn_params ; |
---|
147 | fn_vars = fd.fn_vars ; |
---|
148 | fn_body = add_starting_cost_label cost_universe |
---|
149 | (add_cost_labels_st cost_universe fd.fn_body) |
---|
150 | }) |
---|
151 | | (id,External (a,b,c)) -> (id,External (a,b,c)) |
---|
152 | |
---|
153 | |
---|
154 | (** [add_cost_labels prog] inserts some labels to enable |
---|
155 | cost annotation. *) |
---|
156 | |
---|
157 | let add_cost_labels p = |
---|
158 | let labs = ClightAnnotator.all_labels p in |
---|
159 | let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in |
---|
160 | let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in |
---|
161 | let cost_universe = CostLabel.Gen.new_universe cost_prefix in |
---|
162 | { |
---|
163 | prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct; |
---|
164 | prog_main = p.prog_main; |
---|
165 | prog_vars = p.prog_vars |
---|
166 | } |
---|