source: driver/rTLabsPrinter.ml @ 3000

Last change on this file since 3000 was 3000, checked in by tranquil, 6 years ago

added RTLabs printer

File size: 9.9 KB
Line 
1open Extracted.RTLabs_syntax
2
3open Extracted.FrontEndOps
4
5open Extracted.Integers
6
7(*
8let n_spaces n = String.make n ' '
9
10
11let rec print_size = function
12  | AST.SQ q -> Memory.string_of_quantity q
13  | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
14  | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
15  | AST.SArray (i, se) ->
16    (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
17and print_size_list l =
18  MiscPottier.string_of_list ", " print_size l
19
20let print_global_size = print_size
21
22let print_data = function
23(*
24  | Data_reserve n -> Printf.sprintf "[%d]" n
25*)
26  | AST.Data_int8 i -> Printf.sprintf "(int8) %d" i
27  | AST.Data_int16 i -> Printf.sprintf "(int16) %d" i
28  | AST.Data_int32 i -> Printf.sprintf "%d" i
29  | AST.Data_float32 f -> Printf.sprintf "%f" f
30  | AST.Data_float64 f -> Printf.sprintf "(float64) %f" f
31
32let print_datas init =
33  let rec aux = function
34    | [] -> ""
35    | [data] -> print_data data
36    | data :: datas -> Printf.sprintf "%s, %s" (print_data data) (aux datas)
37  in
38  Printf.sprintf "{%s}" (aux init)
39
40let print_datas_opt = function
41  | None -> ""
42  | Some init -> " = " ^ (print_datas init)
43
44let print_global n (id, size, init_opt) =
45  Printf.sprintf "%s\"%s\" : %s%s;\n"
46    (n_spaces n) id (print_global_size size) (print_datas_opt init_opt)
47
48let print_globals eformat n =
49  List.iter (fun v -> Eformat.printf eformat "%s" (print_global n v))
50
51
52let print_reg = Register.print
53
54let print_oreg = function
55  | None -> "_"
56  | Some r -> print_reg r
57
58let print_decl (r, t) =
59  (Primitive.print_type t) ^ " " ^ (Register.print r)
60
61let rec print_args args =
62  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
63
64let print_result = function
65  | None -> "_"
66  | Some (r, t) -> (Primitive.print_type t) ^ " " ^ (Register.print r)
67
68let print_params r =
69  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_decl r)
70
71let print_locals r =
72  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_decl r)
73
74
75let print_cmp = function
76  | AST.Cmp_eq -> "eq"
77  | AST.Cmp_ne -> "ne"
78  | AST.Cmp_gt -> "gt"
79  | AST.Cmp_ge -> "ge"
80  | AST.Cmp_lt -> "lt"
81  | AST.Cmp_le -> "le"
82
83let rec print_size = function
84  | AST.SQ q -> Memory.string_of_quantity q
85  | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
86  | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
87  | AST.SArray (i, se) ->
88    (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
89and print_size_list l =
90  MiscPottier.string_of_list ", " print_size l
91
92let print_stacksize = print_size
93
94let print_offset (size, depth) =
95  (print_size size) ^ ", " ^ (string_of_int depth)
96
97let print_sizeof = print_size
98
99let string_of_signedness = function
100  | AST.Signed -> "s"
101  | AST.Unsigned -> "u"
102
103let string_of_int_type (size, sign) =
104  Printf.sprintf "%d%s" size (string_of_signedness sign)
105
106let print_op2 = function
107  | AST.Op_add -> "add"
108  | AST.Op_sub -> "sub"
109  | AST.Op_mul -> "mul"
110  | AST.Op_div -> "div"
111  | AST.Op_divu -> "/u"
112  | AST.Op_mod -> "mod"
113  | AST.Op_modu -> "modu"
114  | AST.Op_and -> "and"
115  | AST.Op_or -> "or"
116  | AST.Op_xor -> "xor"
117  | AST.Op_shl -> "shl"
118  | AST.Op_shr -> "shr"
119  | AST.Op_shru -> "shru"
120  | AST.Op_cmp cmp -> print_cmp cmp
121  | AST.Op_addp -> "addp"
122  | AST.Op_subp -> "subp"
123  | AST.Op_subpp -> "subpp"
124  | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
125  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
126
127
128(*
129let print_addressing = function
130  | RTLabs.Aindexed off -> Printf.sprintf "{ %s }" (print_offset off)
131  | RTLabs.Aindexed2 -> "add"
132  | RTLabs.Aglobal (id, off) ->
133    Printf.sprintf "{ %s }(\"%s\")" (print_offset off) id
134  | RTLabs.Abased (id, off) ->
135    Printf.sprintf "add, { %s }(\"%s\")" (print_offset off) id
136  | RTLabs.Ainstack off -> Printf.sprintf "{ %s }(STACK)" (print_offset off)
137*)
138
139
140let rec print_table = function
141  | [] -> ""
142  | [lbl] -> lbl
143  | lbl :: tbl -> lbl ^ ", " ^ (print_table tbl)
144*)
145(* Duplicated, also in cerco.ml! *)
146let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
147
148let print_identifier pref n = pref ^ "_" ^ string_of_pos n
149
150let print_fun_ident = print_identifier "fun"
151
152let print_ident = print_identifier "id"
153
154let print_label = print_identifier "l"
155
156let print_reg = print_identifier "r"
157
158let print_nat n = string_of_int (Extracted.Glue.int_of_matitanat n)
159
160let print_ubv bv = string_of_int (Extracted.Glue.int_of_bitvector bv)
161let print_sbv bv =
162  let z = Extracted.BitVectorZ.z_of_signed_bitvector Extracted.Nat.O bv in
163  string_of_int (Extracted.Glue.int_of_matitaZ z)
164
165
166let print_cst = function
167| Ointconst (_, Extracted.AST.Signed, bv) -> print_sbv bv
168| Ointconst (_, Extracted.AST.Unsigned, bv) -> print_ubv bv
169| Oaddrsymbol (id, off) -> "&" ^ print_ident id ^ " + " ^ print_nat off
170| Oaddrstack off -> "SP + " ^ print_nat off
171
172let print_signedness = function
173  | Extracted.AST.Signed -> ""
174  | Extracted.AST.Unsigned -> "u"
175
176let print_int_size = function
177  | Extracted.AST.I8 -> "8"
178  | Extracted.AST.I16 -> "16"
179  | Extracted.AST.I32 -> "32"
180
181let print_op1 = function
182| Ocastint (src_sy, src_sign, dst_sy, dst_sign) ->
183  Format.sprintf "(%sint%s->%sint%s)"
184    (print_signedness src_sign) (print_int_size src_sy)
185    (print_signedness dst_sign) (print_int_size dst_sy)
186| Onegint _ -> "-"
187| Onotbool _ -> "!"
188| Onotint _ -> "~"
189| Oid _ -> ""
190| Optrofint (sy, sign) ->
191  Format.sprintf "(%sint%s->ptr)"
192    (print_signedness sign) (print_int_size sy)
193| Ointofptr (sy, sign) ->
194  Format.sprintf "(ptr->%sint%s)"
195    (print_signedness sign) (print_int_size sy)
196
197let print_comparison = function
198| Ceq -> "=="
199| Cne -> "!="
200| Clt -> "<"
201| Cle -> "<="
202| Cgt -> ">"
203| Cge -> ">="
204
205let print_op2 = function
206| Oadd _ -> "+"
207| Osub _ -> "-"
208| Omul _ -> "*"
209| Odiv _ -> "/"
210| Odivu _ -> "/u"
211| Omod _ -> "%"
212| Omodu _ -> "%u"
213| Oand _ -> "&&"
214| Oor _ -> "||"
215| Oxor _ -> "^^"
216| Oshl _ -> "<<"
217| Oshr _ -> ">>"
218| Oshru _ -> ">>u"
219| Ocmp (_, _, _, cmp) -> print_comparison cmp
220| Ocmpu (_, _, cmp) ->  print_comparison cmp ^ "u"
221| Oaddpi _ -> "p+"
222| Oaddip _ -> "+p"
223| Osubpi _ -> "p-"
224| Osubpp _ -> "p-p"
225| Ocmpp (_, cmp) -> print_comparison cmp ^ "p"
226
227let rec get_list = function
228  | Extracted.List.Nil -> [ ]
229  | Extracted.List.Cons (hd, tl) -> hd :: get_list tl
230
231let print_regs regs =
232  String.concat ", " (List.map print_reg (get_list regs))
233
234let print_statement = function
235  | St_skip lbl -> "--> " ^ print_label lbl
236  | St_cost (cost_lbl, lbl) ->
237      Printf.sprintf "emit %s --> %s"
238        (print_label cost_lbl)
239        (print_label lbl)
240  | St_const (_, destr, cst, lbl) ->
241      Printf.sprintf "%s = %s --> %s"
242        (print_reg destr)
243        (print_cst cst)
244        (print_label lbl)
245  | St_op1 (_, _, op, dst, src, lbl) ->
246    Format.sprintf "%s = %s%s --> %s"
247      (print_reg dst) (print_op1 op) (print_reg src)
248      (print_label lbl)
249  | St_op2 (_, _, _, op, dst, src1, src2, lbl) ->
250    Format.sprintf "%s = %s %s %s --> %s"
251      (print_reg dst) (print_reg src1) (print_op2 op)
252      (print_reg src2) (print_label lbl)
253  | St_load (_, addr, dst, lbl) ->
254    Format.sprintf "%s = *%s --> %s"
255      (print_reg dst) (print_reg addr) (print_label lbl)
256  | St_store (_, addr, src, lbl) ->
257    Format.sprintf "*%s = %s --> %s"
258      (print_reg addr) (print_reg src) (print_label lbl)
259  | St_call_id (id, args, Extracted.Types.Some dst, lbl) ->
260    Format.sprintf "%s = %s(%s) --> %s"
261      (print_reg dst) (print_fun_ident id) (print_regs args)
262      (print_label lbl)
263  | St_call_id (id, args, Extracted.Types.None, lbl) ->
264    Format.sprintf "%s(%s) --> %s"
265      (print_fun_ident id) (print_regs args)
266      (print_label lbl)
267  | St_call_ptr (addr, args, Extracted.Types.Some dst, lbl) ->
268    Format.sprintf "%s = *%s(%s) --> %s"
269      (print_reg dst) (print_reg addr) (print_regs args)
270      (print_label lbl)
271  | St_call_ptr (addr, args, Extracted.Types.None, lbl) ->
272    Format.sprintf "*%s(%s) --> %s"
273      (print_reg addr) (print_regs args)
274      (print_label lbl)
275  | St_cond (src, l_true, l_false) ->
276    Format.sprintf "if %s then --> %s else --> %s"
277      (print_reg src) (print_label l_true) (print_label l_false)
278  | St_return -> "return"
279
280let next = function
281  | St_skip lbl
282  | St_cost (_, lbl)
283  | St_const (_, _, _, lbl)
284  | St_op1 (_, _, _, _, _, lbl)
285  | St_op2 (_, _, _, _, _, _, _, lbl)
286  | St_load (_, _, _, lbl)
287  | St_store (_, _, _, lbl)
288  | St_call_id (_, _, _, lbl)
289  | St_call_ptr (_, _, _, lbl) -> [lbl]
290  | St_cond (_, l_true, l_false) -> [l_true ; l_false]
291  | St_return -> [ ]
292
293let get_bool = function
294  | Extracted.Bool.True -> true
295  | Extracted.Bool.False -> false
296
297let rec graph_dfs_aux f acc visiting visited graph =
298  match visiting with
299  | [ ] -> acc
300  | hd :: tl ->
301    let tag = Extracted.PreIdentifiers.LabelTag in
302    if get_bool (Extracted.Identifiers.member tag visited hd) then
303      graph_dfs_aux f acc tl visited graph
304    else
305      let visited = Extracted.Identifiers.add_set tag visited hd in
306      match Extracted.Identifiers.lookup tag graph hd with
307      | Extracted.Types.Some s ->
308        let acc = f hd s acc in
309        let visiting = next s @ tl in
310        graph_dfs_aux f acc visiting visited graph
311      | Extracted.Types.None ->
312        graph_dfs_aux f acc tl visited graph
313
314let graph_dfs f init entry =
315  graph_dfs_aux f init [entry]
316    (Extracted.Identifiers.empty_set Extracted.PreIdentifiers.LabelTag)
317
318let print_internal_function id def =
319  let regs = Extracted.List.map Extracted.Types.fst def.f_params in
320  let pre = Format.sprintf "def %s(%s):"
321    (print_fun_ident id) (print_regs regs) in
322  graph_dfs
323    (fun lbl s acc ->
324      Format.sprintf "%s\n  %s: %s" acc (print_label lbl) (print_statement s))
325    pre def.f_entry def.f_graph
326
327let print_external_function id _ =
328  Format.sprintf "ext %s" (print_fun_ident id)
329
330let print_function = function
331  | { Extracted.Types.fst = id ;
332      Extracted.Types.snd = Extracted.AST.Internal def } ->
333    print_internal_function id def
334  | { Extracted.Types.fst = id ;
335      Extracted.Types.snd = Extracted.AST.External def } ->
336    print_external_function id def
337
338let print_program prog =
339  let functs = get_list (prog.Extracted.AST.prog_funct) in
340  String.concat "\n\n" (List.map print_function functs)
Note: See TracBrowser for help on using the repository browser.