1 open Extracted.RTLabs_syntax
3 open Extracted.FrontEndOps
5 open Extracted.Integers
8 let n_spaces n = String.make n ' '
11 let 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) ^ "]"
17 and print_size_list l =
18 MiscPottier.string_of_list ", " print_size l
20 let print_global_size = print_size
22 let print_data = function
24 | Data_reserve n -> Printf.sprintf "[%d]" n
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
32 let print_datas init =
33 let rec aux = function
35 | [data] -> print_data data
36 | data :: datas -> Printf.sprintf "%s, %s" (print_data data) (aux datas)
38 Printf.sprintf "{%s}" (aux init)
40 let print_datas_opt = function
42 | Some init -> " = " ^ (print_datas init)
44 let 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)
48 let print_globals eformat n =
49 List.iter (fun v -> Eformat.printf eformat "%s" (print_global n v))
52 let print_reg = Register.print
54 let print_oreg = function
56 | Some r -> print_reg r
58 let print_decl (r, t) =
59 (Primitive.print_type t) ^ " " ^ (Register.print r)
61 let rec print_args args =
62 Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
64 let print_result = function
66 | Some (r, t) -> (Primitive.print_type t) ^ " " ^ (Register.print r)
69 Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_decl r)
72 Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_decl r)
75 let print_cmp = function
83 let 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) ^ "]"
89 and print_size_list l =
90 MiscPottier.string_of_list ", " print_size l
92 let print_stacksize = print_size
94 let print_offset (size, depth) =
95 (print_size size) ^ ", " ^ (string_of_int depth)
97 let print_sizeof = print_size
99 let string_of_signedness = function
101 | AST.Unsigned -> "u"
103 let string_of_int_type (size, sign) =
104 Printf.sprintf "%d%s" size (string_of_signedness sign)
106 let 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"
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"
129 let 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)
140 let rec print_table = function
143 | lbl :: tbl -> lbl ^ ", " ^ (print_table tbl)
145 (* Duplicated, also in cerco.ml! *)
146 let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
148 let print_identifier pref n = pref ^ "_" ^ string_of_pos n
150 let print_fun_ident = print_identifier "fun"
151 let print_ident = print_identifier "id"
152 let print_label = print_identifier "l"
153 let print_reg = print_identifier "r"
154 let print_cost = print_identifier "k"
156 let print_nat n = string_of_int (Extracted.Glue.int_of_matitanat n)
158 let print_ubv bv = string_of_int (Extracted.Glue.int_of_bitvector 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)
164 let 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
170 let print_signedness = function
171 | Extracted.AST.Signed -> ""
172 | Extracted.AST.Unsigned -> "u"
174 let print_int_size = function
175 | Extracted.AST.I8 -> "8"
176 | Extracted.AST.I16 -> "16"
177 | Extracted.AST.I32 -> "32"
179 let 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)
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)
195 let print_comparison = function
203 let print_op2 = function
217 | Ocmp (_, _, _, cmp) -> print_comparison cmp
218 | Ocmpu (_, _, cmp) -> print_comparison cmp ^ "u"
223 | Ocmpp (_, cmp) -> print_comparison cmp ^ "p"
225 let rec get_list = function
226 | Extracted.List.Nil -> [ ]
227 | Extracted.List.Cons (hd, tl) -> hd :: get_list tl
229 let print_regs regs =
230 String.concat ", " (List.map print_reg (get_list regs))
232 let 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)
238 | St_const (_, destr, cst, lbl) ->
239 Printf.sprintf "%s = %s --> %s"
243 | St_op1 (_, _, op, dst, src, lbl) ->
244 Format.sprintf "%s = %s%s --> %s"
245 (print_reg dst) (print_op1 op) (print_reg src)
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)
261 | St_call_id (id, args, Extracted.Types.None, lbl) ->
262 Format.sprintf "%s(%s) --> %s"
263 (print_fun_ident id) (print_regs args)
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)
269 | St_call_ptr (addr, args, Extracted.Types.None, lbl) ->
270 Format.sprintf "*%s(%s) --> %s"
271 (print_reg addr) (print_regs args)
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"
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]
291 let get_bool = function
292 | Extracted.Bool.True -> true
293 | Extracted.Bool.False -> false
295 let rec graph_dfs_aux f acc visiting visited graph =
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
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
312 let graph_dfs f init entry =
313 graph_dfs_aux f init [entry]
314 (Extracted.Identifiers.empty_set Extracted.PreIdentifiers.LabelTag)
316 let 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
322 Format.sprintf "%s\n %s: %s" acc (print_label lbl) (print_statement s))
323 pre def.f_entry def.f_graph
325 let print_external_function id _ =
326 Format.sprintf "ext %s" (print_fun_ident id)
328 let 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
336 let print_program prog =
337 let functs = get_list (prog.Extracted.AST.prog_funct) in
338 String.concat "\n\n" (List.map print_function functs)