source: Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightLabelling.ml @ 460

Last change on this file since 460 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

File size: 6.1 KB
Line 
1
2(** This module defines the labelling of a [Clight] program. *)
3
4open Clight
5open CostLabel
6
7
8(* Add a cost label in front of a statement. *)
9
10let 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
15let add_ending_cost_label cost_universe stmt =
16  Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
17
18
19let int_type = Tint (I32, Signed)
20let const_int i = Expr (Econst_int i, int_type)
21
22
23let add_cost_label_e cost_universe e =
24  Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), int_type)
25
26
27let typeof e = let Expr (_,t) = e in t
28
29
30(* Add cost labels to an expression. *)
31
32let rec add_cost_labels_e cost_universe = function 
33  | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
34
35and 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
73let add_cost_labels_opt cost_universe = function
74  | None -> None
75  | Some e -> Some (add_cost_labels_e cost_universe e)
76
77let 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
83let 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 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)
119  | Sswitch (e,ls) ->
120      Sswitch (add_cost_labels_e cost_universe e,
121               add_cost_labels_ls cost_universe ls)
122  | Slabel (lbl,s) ->
123      let s' = add_cost_labels_st cost_universe s in
124      let s' = add_starting_cost_label cost_universe s' in
125      Slabel (lbl,s')
126  | Scost (_,_) -> assert false
127  | _ as stmt -> stmt
128
129and add_cost_labels_ls cost_universe = function
130  | LSdefault s ->
131      let s' = add_cost_labels_st cost_universe s in
132      let s' = add_starting_cost_label cost_universe s' in
133      LSdefault s'
134  | LScase (i,s,ls) ->
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)
138
139
140(* Add cost labels to a function. *)
141
142let 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)
149    })
150  | (id,External (a,b,c)) -> (id,External (a,b,c))
151
152
153(** [add_cost_labels prog] inserts some labels to enable
154    cost annotation. *)
155
156let 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
161  {
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
165  }
Note: See TracBrowser for help on using the repository browser.