source: Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml @ 1319

Last change on this file since 1319 was 1319, checked in by tranquil, 8 years ago

indexing branch is compiling again:

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