source: Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml @ 740

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 7.2 KB
Line 
1
2(** This module performs a transformation of a [Clight] program with potentially
3    32 and 16 bits integers to an equivalent [Clight] program that only uses 8
4    bits integers.
5
6    The main changes are: defining two types that represent 32 and 16 bits
7    integers with a structure of 8 bits integers, making the substitution,
8    replacing primitive integer operations on 32 and 16 bits integers with new
9    functions emulating them on the new types, and finally defining a global
10    variable for each 32 and 16 bits integer constant, which is then replaced by
11    its associated variable. *)
12
13
14let rec seq = function
15  | [] -> Clight.Sskip
16  | [stmt] -> stmt
17  | stmt :: l -> Clight.Ssequence (stmt, seq l)
18
19
20let call tmp f_id args_and_type res_type =
21  let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in
22  let (args, args_type) = List.split args_and_type in
23  let f_var = Clight.Evar f_id in
24  let f_type = Clight.Tfunction (args_type, res_type) in
25  let f = Clight.Expr (f_var, f_type) in
26  (tmpe, Clight.Scall (Some tmpe, f, args))
27
28let replace_primitives_expression fresh unop_assoc binop_assoc =
29
30  let rec aux e =
31    let Clight.Expr (ed, t) = e in
32    let expr ed = Clight.Expr (ed, t) in
33    match ed with
34
35      | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
36      | Clight.Esizeof _ ->
37        (e, Clight.Sskip, [])
38
39      | Clight.Ederef e ->
40        let (e', stmt, tmps) = aux e in
41        (expr (Clight.Ederef e'), stmt, tmps)
42
43      | Clight.Eaddrof e ->
44        let (e', stmt, tmps) = aux e in
45        (expr (Clight.Eaddrof e'), stmt, tmps)
46
47      | Clight.Eunop (unop, Clight.Expr (ed', t'))
48          when List.mem_assoc (unop, t') unop_assoc ->
49        let (e', stmt, tmps) = aux (Clight.Expr (ed', t')) in
50        let tmp = fresh () in
51        let (tmpe, call) =
52          call tmp (List.assoc (unop, t') unop_assoc) [(e', t')] t in
53        let stmt = seq [stmt ; call] in
54        (tmpe, stmt, tmps @ [(tmp, t)])
55
56      | Clight.Ebinop (binop, Clight.Expr (ed1, t1), Clight.Expr (ed2, t2))
57          when List.mem_assoc (binop, t1, t2) binop_assoc ->
58        let (e1, stmt1, tmps1) = aux (Clight.Expr (ed1, t1)) in
59        let (e2, stmt2, tmps2) = aux (Clight.Expr (ed2, t2)) in
60        let tmp = fresh () in
61        let (tmpe, call) =
62          call tmp (List.assoc (binop, t1, t2) binop_assoc)
63            [(e1, t1) ; (e2, t2)] t in
64        let stmt = seq [stmt1 ; stmt2 ; call] in
65        (tmpe, stmt, tmps1 @ tmps2 @ [(tmp, t)])
66
67      | _ -> (e, Clight.Sskip, []) (* TODO *)
68
69  in
70  aux
71
72
73let replace_primitives_expression_list fresh unop_assoc binop_assoc =
74  let f (l, stmt, tmps) e =
75    let (e', stmt', tmps') =
76      replace_primitives_expression fresh unop_assoc binop_assoc e in
77    (l @ [e], seq [stmt ; stmt'], tmps @ tmps') in
78  List.fold_left f ([], Clight.Sskip, [])
79
80
81let replace_primitives_statement fresh unop_assoc binop_assoc =
82  let aux_exp =
83    replace_primitives_expression fresh unop_assoc binop_assoc in
84  let aux_exp_list =
85    replace_primitives_expression_list fresh unop_assoc binop_assoc in
86
87  let rec aux = function
88
89    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sgoto _
90    | Clight.Sreturn None
91      as stmt -> (stmt, [])
92
93    | Clight.Slabel (lbl, stmt) ->
94      let (stmt', tmps) = aux stmt in
95      (Clight.Slabel (lbl, stmt'), tmps)
96
97    | Clight.Scost (lbl, stmt) ->
98      let (stmt', tmps) = aux stmt in
99      (Clight.Scost (lbl, stmt'), tmps)
100
101    | Clight.Sassign (e1, e2) ->
102      let (e1', stmt1, tmps1) = aux_exp e1 in
103      let (e2', stmt2, tmps2) = aux_exp e2 in
104      let stmt = seq [stmt1 ; stmt2 ; Clight.Sassign (e1', e2')] in
105      (stmt, tmps1 @ tmps2)
106
107    | Clight.Scall (None, f, args) ->
108      let (f', stmt1, tmps1) = aux_exp f in
109      let (args', stmt2, tmps2) = aux_exp_list args in
110      let stmt = seq [stmt1 ; stmt2 ; Clight.Scall (None, f', args')] in
111      (stmt, tmps1 @ tmps2)
112
113    | Clight.Scall (Some e, f, args) ->
114      let (e', stmt1, tmps1) = aux_exp e in
115      let (f', stmt2, tmps2) = aux_exp f in
116      let (args', stmt3, tmps3) = aux_exp_list args in
117      let stmt = seq [stmt1 ; stmt2 ; stmt3 ;
118                           Clight.Scall (Some e', f', args')] in
119      (stmt, tmps1 @ tmps2 @ tmps3)
120
121    | Clight.Sifthenelse (e, stmt1, stmt2) ->
122      let (e', stmte, tmpse) = aux_exp e in
123      let (stmt1', tmps1) = aux stmt1 in
124      let (stmt2', tmps2) = aux stmt2 in
125      let stmt = seq [stmte ; Clight.Sifthenelse (e', stmt1', stmt2')] in
126      (stmt, tmpse @ tmps1 @ tmps2)
127
128    | Clight.Swhile (e, stmt) ->
129      let (e', stmte, tmpse) = aux_exp e in
130      let (stmt', tmps) = aux stmt in
131      let stmt = seq [stmte ; Clight.Swhile (e', seq [stmt' ; stmte])] in
132      (stmt, tmpse @ tmps)
133
134    | Clight.Sdowhile (e, stmt) ->
135      let (e', stmte, tmpse) = aux_exp e in
136      let (stmt', tmps) = aux stmt in
137      let stmt = seq [Clight.Sdowhile (e', seq [stmt' ; stmte])] in
138      (stmt, tmpse @ tmps)
139
140    | Clight.Sfor (stmt1, e, stmt2, stmt3) ->
141      let (e', stmte, tmpse) = aux_exp e in
142      let (stmt1', tmps1) = aux stmt1 in
143      let (stmt2', tmps2) = aux stmt2 in
144      let (stmt3', tmps3) = aux stmt3 in
145      let stmt = seq [stmt1' ; stmte ;
146                      Clight.Swhile (e', seq [stmt2' ; stmt3' ; stmte])] in
147      (stmt, tmpse @ tmps1 @ tmps2 @ tmps3)
148
149    | Clight.Sswitch (e, lbl_stmts) ->
150      let (e', stmte, tmpse) = aux_exp e in
151      let (lbl_stmts', tmps) = aux_lbl_stmts lbl_stmts in
152      let stmt = seq [stmte ; Clight.Sswitch (e', lbl_stmts')] in
153      (stmt, tmpse @ tmps)
154
155    | Clight.Sreturn (Some e) ->
156      let (e', stmte, tmpse) = aux_exp e in
157      let stmt = seq [stmte ; Clight.Sreturn (Some e')] in
158      (stmt, tmpse)
159
160    | Clight.Ssequence (stmt1, stmt2) ->
161      let (stmt1', tmps1) = aux stmt1 in
162      let (stmt2', tmps2) = aux stmt2 in
163      let stmt = seq [stmt1' ; stmt2'] in
164      (stmt, tmps1 @ tmps2)
165
166  and aux_lbl_stmts = function
167
168    | Clight.LSdefault stmt ->
169      let (stmt', tmps) = aux stmt in
170      (Clight.LSdefault stmt', tmps)
171
172    | Clight.LScase (i, stmt, lbl_stmts) ->
173      let (stmt', tmps1) = aux stmt in
174      let (lbl_stmts', tmps2) = aux_lbl_stmts lbl_stmts in
175      (Clight.LScase (i, stmt', lbl_stmts'), tmps1 @ tmps2)
176
177  in
178
179  aux
180
181
182let replace_primitives_internal fresh unop_assoc binop_assoc def =
183  let (new_body, tmps) =
184    replace_primitives_statement fresh unop_assoc binop_assoc
185      def.Clight.fn_body in
186  { def with Clight.fn_vars = def.Clight.fn_vars @ tmps ;
187             Clight.fn_body = new_body }
188
189let replace_primitives_funct fresh unop_assoc binop_assoc (id, fundef) =
190  let fundef' = match fundef with
191    | Clight.Internal def ->
192      Clight.Internal
193        (replace_primitives_internal fresh unop_assoc binop_assoc def)
194    | _ -> fundef in
195  (id, fundef')
196
197let replace_primitives fresh unop_assoc binop_assoc p =
198  let prog_funct =
199    List.map (replace_primitives_funct fresh unop_assoc binop_assoc)
200      p.Clight.prog_funct in
201  { p with Clight.prog_funct = prog_funct }
202
203
204let translate p =
205  (* TODO: restore below *)
206(*
207  let (p, unop_assoc, binop_assoc) = Runtime.add p in
208  let p = ClightCasts.simplify p in
209  let labs = ClightAnnotator.all_labels p in
210  let tmp_prefix = StringTools.Gen.fresh_prefix labs "_tmp" in
211  let tmp_universe = StringTools.Gen.new_universe tmp_prefix in
212  let fresh () = StringTools.Gen.fresh tmp_universe in
213  let p = replace_primitives fresh unop_assoc binop_assoc p in
214  (* TODO: do the translation *)
215  p
216*)
217  ClightCasts.simplify p
Note: See TracBrowser for help on using the repository browser.