source: driver/rTLabsPrinter.ml

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

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

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"
151let print_ident = print_identifier "id"
152let print_label = print_identifier "l"
153let print_reg = print_identifier "r"
154let print_cost = print_identifier "k"
155
156let print_nat n = string_of_int (Extracted.Glue.int_of_matitanat n)
157
158let print_ubv bv = string_of_int (Extracted.Glue.int_of_bitvector bv)
159let print_sbv bv =
160  let z = Extracted.BitVectorZ.z_of_signed_bitvector Extracted.Nat.O bv in
161  string_of_int (Extracted.Glue.int_of_matitaZ z)
162
163
164let print_cst = function
165| Ointconst (_, Extracted.AST.Signed, bv) -> print_sbv bv
166| Ointconst (_, Extracted.AST.Unsigned, bv) -> print_ubv bv
167| Oaddrsymbol (id, off) -> "&" ^ print_ident id ^ " + " ^ print_nat off
168| Oaddrstack off -> "SP + " ^ print_nat off
169
170let print_signedness = function
171  | Extracted.AST.Signed -> ""
172  | Extracted.AST.Unsigned -> "u"
173
174let print_int_size = function
175  | Extracted.AST.I8 -> "8"
176  | Extracted.AST.I16 -> "16"
177  | Extracted.AST.I32 -> "32"
178
179let print_op1 = function
180| Ocastint (src_sy, src_sign, dst_sy, dst_sign) ->
181  Format.sprintf "(%sint%s->%sint%s)"
182    (print_signedness src_sign) (print_int_size src_sy)
183    (print_signedness dst_sign) (print_int_size dst_sy)
184| Onegint _ -> "-"
185| Onotbool _ -> "!"
186| Onotint _ -> "~"
187| Oid _ -> ""
188| Optrofint (sy, sign) ->
189  Format.sprintf "(%sint%s->ptr)"
190    (print_signedness sign) (print_int_size sy)
191| Ointofptr (sy, sign) ->
192  Format.sprintf "(ptr->%sint%s)"
193    (print_signedness sign) (print_int_size sy)
194
195let print_comparison = function
196| Ceq -> "=="
197| Cne -> "!="
198| Clt -> "<"
199| Cle -> "<="
200| Cgt -> ">"
201| Cge -> ">="
202
203let print_op2 = function
204| Oadd _ -> "+"
205| Osub _ -> "-"
206| Omul _ -> "*"
207| Odiv _ -> "/"
208| Odivu _ -> "/u"
209| Omod _ -> "%"
210| Omodu _ -> "%u"
211| Oand _ -> "&&"
212| Oor _ -> "||"
213| Oxor _ -> "^^"
214| Oshl _ -> "<<"
215| Oshr _ -> ">>"
216| Oshru _ -> ">>u"
217| Ocmp (_, _, _, cmp) -> print_comparison cmp
218| Ocmpu (_, _, cmp) ->  print_comparison cmp ^ "u"
219| Oaddpi _ -> "p+"
220| Oaddip _ -> "+p"
221| Osubpi _ -> "p-"
222| Osubpp _ -> "p-p"
223| Ocmpp (_, cmp) -> print_comparison cmp ^ "p"
224
225let rec get_list = function
226  | Extracted.List.Nil -> [ ]
227  | Extracted.List.Cons (hd, tl) -> hd :: get_list tl
228
229let print_regs regs =
230  String.concat ", " (List.map print_reg (get_list regs))
231
232let print_statement = function
233  | St_skip lbl -> "--> " ^ print_label lbl
234  | St_cost (cost_lbl, lbl) ->
235      Printf.sprintf "emit %s --> %s"
236        (print_cost cost_lbl)
237        (print_label lbl)
238  | St_const (_, destr, cst, lbl) ->
239      Printf.sprintf "%s = %s --> %s"
240        (print_reg destr)
241        (print_cst cst)
242        (print_label lbl)
243  | St_op1 (_, _, op, dst, src, lbl) ->
244    Format.sprintf "%s = %s%s --> %s"
245      (print_reg dst) (print_op1 op) (print_reg src)
246      (print_label lbl)
247  | St_op2 (_, _, _, op, dst, src1, src2, lbl) ->
248    Format.sprintf "%s = %s %s %s --> %s"
249      (print_reg dst) (print_reg src1) (print_op2 op)
250      (print_reg src2) (print_label lbl)
251  | St_load (_, addr, dst, lbl) ->
252    Format.sprintf "%s = *%s --> %s"
253      (print_reg dst) (print_reg addr) (print_label lbl)
254  | St_store (_, addr, src, lbl) ->
255    Format.sprintf "*%s = %s --> %s"
256      (print_reg addr) (print_reg src) (print_label lbl)
257  | St_call_id (id, args, Extracted.Types.Some dst, lbl) ->
258    Format.sprintf "%s = %s(%s) --> %s"
259      (print_reg dst) (print_fun_ident id) (print_regs args)
260      (print_label lbl)
261  | St_call_id (id, args, Extracted.Types.None, lbl) ->
262    Format.sprintf "%s(%s) --> %s"
263      (print_fun_ident id) (print_regs args)
264      (print_label lbl)
265  | St_call_ptr (addr, args, Extracted.Types.Some dst, lbl) ->
266    Format.sprintf "%s = *%s(%s) --> %s"
267      (print_reg dst) (print_reg addr) (print_regs args)
268      (print_label lbl)
269  | St_call_ptr (addr, args, Extracted.Types.None, lbl) ->
270    Format.sprintf "*%s(%s) --> %s"
271      (print_reg addr) (print_regs args)
272      (print_label lbl)
273  | St_cond (src, l_true, l_false) ->
274    Format.sprintf "if %s then --> %s else --> %s"
275      (print_reg src) (print_label l_true) (print_label l_false)
276  | St_return -> "return"
277
278let next = function
279  | St_skip lbl
280  | St_cost (_, lbl)
281  | St_const (_, _, _, lbl)
282  | St_op1 (_, _, _, _, _, lbl)
283  | St_op2 (_, _, _, _, _, _, _, lbl)
284  | St_load (_, _, _, lbl)
285  | St_store (_, _, _, lbl)
286  | St_call_id (_, _, _, lbl)
287  | St_call_ptr (_, _, _, lbl) -> [lbl]
288  | St_cond (_, l_true, l_false) -> [l_true ; l_false]
289  | St_return -> [ ]
290
291let get_bool = function
292  | Extracted.Bool.True -> true
293  | Extracted.Bool.False -> false
294
295let rec graph_dfs_aux f acc visiting visited graph =
296  match visiting with
297  | [ ] -> acc
298  | hd :: tl ->
299    let tag = Extracted.PreIdentifiers.LabelTag in
300    if get_bool (Extracted.Identifiers.member tag visited hd) then
301      graph_dfs_aux f acc tl visited graph
302    else
303      let visited = Extracted.Identifiers.add_set tag visited hd in
304      match Extracted.Identifiers.lookup tag graph hd with
305      | Extracted.Types.Some s ->
306        let acc = f hd s acc in
307        let visiting = next s @ tl in
308        graph_dfs_aux f acc visiting visited graph
309      | Extracted.Types.None ->
310        graph_dfs_aux f acc tl visited graph
311
312let graph_dfs f init entry =
313  graph_dfs_aux f init [entry]
314    (Extracted.Identifiers.empty_set Extracted.PreIdentifiers.LabelTag)
315
316let print_internal_function id def =
317  let regs = Extracted.List.map Extracted.Types.fst def.f_params in
318  let pre = Format.sprintf "def %s(%s):"
319    (print_fun_ident id) (print_regs regs) in
320  graph_dfs
321    (fun lbl s acc ->
322      Format.sprintf "%s\n  %s: %s" acc (print_label lbl) (print_statement s))
323    pre def.f_entry def.f_graph
324
325let print_external_function id _ =
326  Format.sprintf "ext %s" (print_fun_ident id)
327
328let print_function = function
329  | { Extracted.Types.fst = id ;
330      Extracted.Types.snd = Extracted.AST.Internal def } ->
331    print_internal_function id def
332  | { Extracted.Types.fst = id ;
333      Extracted.Types.snd = Extracted.AST.External def } ->
334    print_external_function id def
335
336let print_program prog =
337  let functs = get_list (prog.Extracted.AST.prog_funct) in
338  String.concat "\n\n" (List.map print_function functs)
Note: See TracBrowser for help on using the repository browser.