2 (** This module defines the labelling of a [Clight] program. *)
8 (* Add a cost label in front of a statement. *)
10 let add_starting_cost_label cost_universe stmt =
11 Clight.Scost (CostLabel.Gen.fresh cost_universe, stmt)
13 (* Add a cost label at the end of a statement. *)
15 let add_ending_cost_label cost_universe stmt =
16 Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
19 let int_type = Tint (I32, AST.Signed)
20 let const_int i = Expr (Econst_int i, int_type)
23 let typeof e = let Expr (_,t) = e in t
26 let add_cost_label_e cost_universe e =
27 Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e)
30 (* Add cost labels to an expression. *)
32 let rec add_cost_labels_e cost_universe = function
33 | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
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) ->
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)
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')
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 *)
73 let add_cost_labels_opt cost_universe = function
75 | Some e -> Some (add_cost_labels_e cost_universe e)
77 let add_cost_labels_lst cost_universe l =
78 List.map (add_cost_labels_e cost_universe) l
81 (* Add cost labels to a statement. *)
83 let rec add_cost_labels_st cost_universe = function
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')
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'))
107 let s = add_cost_labels_st cost_universe s in
108 let s' = add_starting_cost_label cost_universe s in
109 add_ending_cost_label cost_universe
110 (Sdowhile (add_cost_labels_e cost_universe e, s'))
111 | Sfor (s1,e,s2,s3) ->
112 let s1' = add_cost_labels_st cost_universe s1 in
113 let s2' = add_cost_labels_st cost_universe s2 in
114 let s3' = add_cost_labels_st cost_universe s3 in
115 let s3' = add_starting_cost_label cost_universe s3' in
116 add_ending_cost_label cost_universe
117 (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3'))
118 | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e)
120 Sswitch (add_cost_labels_e cost_universe e,
121 add_cost_labels_ls cost_universe ls)
123 let s' = add_cost_labels_st cost_universe s in
124 let s' = add_starting_cost_label cost_universe s' in
126 | Scost (_,_) -> assert false
129 and add_cost_labels_ls cost_universe = function
131 let s' = add_cost_labels_st cost_universe s in
132 let s' = add_starting_cost_label cost_universe s' in
135 let s' = add_cost_labels_st cost_universe s in
136 let s' = add_starting_cost_label cost_universe s' in
137 LScase (i, s', add_cost_labels_ls cost_universe ls)
140 (* Add cost labels to a function. *)
142 let add_cost_labels_f cost_universe = function
143 | (id,Internal fd) -> (id,Internal {
144 fn_return = fd.fn_return ;
145 fn_params = fd.fn_params ;
146 fn_vars = fd.fn_vars ;
147 fn_body = add_starting_cost_label cost_universe
148 (add_cost_labels_st cost_universe fd.fn_body)
150 | (id,External (a,b,c)) -> (id,External (a,b,c))
153 (** [add_cost_labels prog] inserts some labels to enable
156 let add_cost_labels p =
157 let labs = ClightAnnotator.all_labels p in
158 let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in
159 let cost_prefix = CostLabel.Gen.fresh_prefix labs "__cost" in
160 let cost_universe = CostLabel.Gen.new_universe cost_prefix in
162 prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct;
163 prog_main = p.prog_main;
164 prog_vars = p.prog_vars