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

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

changed representation of indexings to a nameless one implemented with arrays

File size: 6.6 KB
RevLine 
[486]1
2(** This module defines the labelling of a [Clight] program. *)
3
4open Clight
5open CostLabel
6
7
[1291]8(* Add a cost label in front of a statement with the current indexing. *)
[486]9
[1291]10let add_starting_cost_label indexing cost_universe stmt =
11  Clight.Scost (CostLabel.fresh indexing cost_universe, stmt)
[486]12
13(* Add a cost label at the end of a statement. *)
14
[1291]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)
[486]18
19
[818]20let int_type = Tint (I32, AST.Signed)
[486]21let const_int i = Expr (Econst_int i, int_type)
22
23
[796]24let typeof e = let Expr (_,t) = e in t
[486]25
26
[1291]27let add_cost_label_e indexing cost_universe e =
28  Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e)
[486]29
30
31(* Add cost labels to an expression. *)
32
[1291]33let rec add_cost_labels_e ind cost_universe = function 
34  | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty)
[486]35
[1291]36and add_cost_labels_expr ind cost_universe exp = match exp with
[486]37  | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp
[1291]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))
[486]41  | Ebinop (op,e1,e2) ->
42      Ebinop (op,
[1291]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)
[486]46  | Eandbool (e1,e2) ->
[1291]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
[486]51      let e2' = Expr (Econdition (e2', b1, b2), int_type) in
[1291]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
[486]54      Econdition (e1', e2', e3')
55  | Eorbool (e1,e2) ->
[1291]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
[486]61      let e3' = Expr (Econdition (e3', b1, b2), int_type) in
[1291]62      let e3' = add_cost_label_e ind cost_universe e3' in
[486]63      Econdition (e1', e2', e3')
[1291]64  | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id)
[486]65  | Econdition (e1,e2,e3) ->
[1291]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
[486]71      Econdition (e1', e2', e3')
72  | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
73
[1291]74let add_cost_labels_opt ind cost_universe =
75        Option.map (add_cost_labels_e ind cost_universe) 
[486]76
[1291]77let add_cost_labels_lst ind cost_universe l =
78  List.map (add_cost_labels_e ind cost_universe) l
[486]79
80
81(* Add cost labels to a statement. *)
82
[1291]83let rec add_cost_labels_st ind cost_universe = function
[486]84  | Sskip -> Sskip
85  | Sassign (e1,e2) ->
[1291]86      Sassign (add_cost_labels_e ind cost_universe e1,
87               add_cost_labels_e ind cost_universe e2)
[486]88  | Scall (e1,e2,lst) ->
[1291]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)
[486]92  | Ssequence (s1,s2) ->
[1291]93      Ssequence (add_cost_labels_st ind cost_universe s1,
94                 add_cost_labels_st ind cost_universe s2) 
[486]95  | Sifthenelse (e,s1,s2) ->
[1291]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')
[486]101  | Swhile (e,s) ->
[1291]102      let s' = add_cost_labels_st ind cost_universe s in
103      let s' = add_starting_cost_label ind cost_universe s' in
104      add_ending_cost_label ind cost_universe
105        (Swhile (add_cost_labels_e ind cost_universe e, s'))
[486]106  | Sdowhile (e,s) ->
[1291]107      let s1 = add_cost_labels_st ind cost_universe s in
108      let s2 = add_cost_labels_st ind cost_universe s in
109      let s2' = add_starting_cost_label ind cost_universe s2 in
110      add_ending_cost_label ind cost_universe
111        (Ssequence (s1, Swhile (add_cost_labels_e ind cost_universe e, s2')))
[486]112  | Sfor (s1,e,s2,s3) ->
[1291]113      let s1' = add_cost_labels_st ind cost_universe s1 in
114      let s2' = add_cost_labels_st ind cost_universe s2 in
115      let s3' = add_cost_labels_st ind cost_universe s3 in
116      let s3' = add_starting_cost_label ind cost_universe s3' in
117      add_ending_cost_label ind cost_universe
118        (Sfor (s1', add_cost_labels_e ind cost_universe e, s2', s3'))
119  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
[486]120  | Sswitch (e,ls) ->
[1291]121      Sswitch (add_cost_labels_e ind cost_universe e,
122               add_cost_labels_ls ind cost_universe ls)
[486]123  | Slabel (lbl,s) ->
[1291]124      let s' = add_cost_labels_st ind cost_universe s in
125      let s' = add_starting_cost_label ind cost_universe s' in
[486]126      Slabel (lbl,s')
127  | Scost (_,_) -> assert false
128  | _ as stmt -> stmt
129
[1291]130and add_cost_labels_ls ind cost_universe = function
[486]131  | LSdefault s ->
[1291]132      let s' = add_cost_labels_st ind cost_universe s in
133      let s' = add_starting_cost_label ind cost_universe s' in
[486]134      LSdefault s'
135  | LScase (i,s,ls) ->
[1291]136      let s' = add_cost_labels_st ind cost_universe s in
137      let s' = add_starting_cost_label ind cost_universe s' in
138      LScase (i, s', add_cost_labels_ls ind cost_universe ls)
[486]139
140
141(* Add cost labels to a function. *)
142
[1291]143let add_cost_labels_f ind cost_universe = function
[486]144  | (id,Internal fd) -> (id,Internal {
145      fn_return = fd.fn_return ;
146      fn_params = fd.fn_params ;
147      fn_vars = fd.fn_vars ;
[1291]148      fn_body = add_starting_cost_label ind cost_universe
149                             (add_cost_labels_st ind cost_universe fd.fn_body)
[486]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
157let add_cost_labels p =
158  let labs = ClightAnnotator.all_labels p in
[1291]159        let add = CostLabel.Atom.Set.add in
160        let empty = CostLabel.Atom.Set.empty in
161  let labs = StringTools.Set.fold add labs empty in
162  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
163  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
[1297]164        let ind = CostLabel.id_indexing 0 in
[486]165  {
[1291]166    prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct;
[486]167    prog_main = p.prog_main;
168    prog_vars = p.prog_vars
169  }
Note: See TracBrowser for help on using the repository browser.