source: src/Cminor/cminorMatitaPrinter.ml @ 816

Last change on this file since 816 was 816, checked in by campbell, 9 years ago

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File size: 10.1 KB
Line 
1open AST
2
3let next_id = ref 0
4let fresh () = let i = !next_id in next_id := i+1; i
5
6let print_type = function
7  | Sig_int -> "ASTint"
8  | Sig_float -> "ASTfloat"
9  | Sig_ptr -> "ASTptr Any"
10
11let print_ret_type = function
12  | Type_ret t -> print_type t
13  | Type_void -> "void"
14
15
16let print_data = function
17  | Data_reserve n -> Printf.sprintf "Init_space %d" n
18  | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i
19  | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i
20  | Data_int32 i -> Printf.sprintf "Init_int32 (repr %d)" i
21  | Data_float32 f -> Printf.sprintf "Init_float32 %f" f
22  | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
23
24let print_var n (id, init) =
25  Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
26    id
27    (MiscPottier.string_of_list ";" print_data init)
28
29let print_vars n = MiscPottier.string_of_list ";\n" (print_var n) 
30
31let print_cmp = function
32  | AST.Cmp_eq -> "Ceq"
33  | AST.Cmp_ne -> "Cne"
34  | AST.Cmp_gt -> "Cgt"
35  | AST.Cmp_ge -> "Cge"
36  | AST.Cmp_lt -> "Clt"
37  | AST.Cmp_le -> "Cle"
38
39let print_constant = function
40  | AST.Cst_int i -> Printf.sprintf "Ointconst (repr %d)" i
41  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
42  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
43  | AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off
44
45let print_op1 = function
46  | AST.Op_cast8unsigned -> "Ocast8unsigned"
47  | AST.Op_cast8signed -> "Ocast8signed"
48  | AST.Op_cast16unsigned -> "Ocast16unsigned"
49  | AST.Op_cast16signed -> "Ocast16signed"
50  | AST.Op_negint -> "Onegint"
51  | AST.Op_notbool -> "Onotbool"
52  | AST.Op_notint -> "Onotint"
53  | AST.Op_negf -> "Onegf"
54  | AST.Op_absf -> "Oabsf"
55  | AST.Op_singleoffloat -> "Osingleoffloat"
56  | AST.Op_intoffloat -> "Ointoffloat"
57  | AST.Op_intuoffloat -> "Ointuoffloat"
58  | AST.Op_floatofint -> "Ofloatofint"
59  | AST.Op_floatofintu -> "Ofloatofintu"
60  | AST.Op_id -> "Oid"
61  | AST.Op_ptrofint -> "Optrofint"
62  | AST.Op_intofptr -> "Ointofptr"
63
64let print_op2 = function
65  | AST.Op_add -> "Oadd"
66  | AST.Op_sub -> "Osub"
67  | AST.Op_mul -> "Omul"
68  | AST.Op_div -> "Odiv"
69  | AST.Op_divu -> "Odivu"
70  | AST.Op_mod -> "Omod"
71  | AST.Op_modu -> "Omodu"
72  | AST.Op_and -> "Oand"
73  | AST.Op_or -> "Oor"
74  | AST.Op_xor -> "Oxor"
75  | AST.Op_shl -> "Oshl"
76  | AST.Op_shr -> "Oshr"
77  | AST.Op_shru -> "Oshru"
78  | AST.Op_addf -> "Oaddf"
79  | AST.Op_subf -> "Osubf"
80  | AST.Op_mulf -> "Omulf"
81  | AST.Op_divf -> "Odivf"
82  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
83  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
84  | AST.Op_cmpf cmp -> "(Ocmpf " ^ (print_cmp cmp) ^ ")"
85  | AST.Op_addp -> "Oaddp"
86  | AST.Op_subp -> "Osubpi" (* FIXME: there should be separate subpi and subpp ops*)
87  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
88
89let rec define_expr_labels = function
90  | Cminor.Op1 (_, e) -> define_expr_labels e
91  | Cminor.Op2 (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
92  | Cminor.Mem (_, e) -> define_expr_labels e
93  | Cminor.Cond (e1, e2, e3) ->
94      define_expr_labels e1 ^ define_expr_labels e2 ^ define_expr_labels e3 
95  | Cminor.Exp_cost (lab, e) ->
96      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
97        lab (fresh ()) (define_expr_labels e)
98  | _ -> ""
99
100let print_quantity = function
101  | Memory.QInt 1 -> "Mint8unsigned"
102  | Memory.QInt 2 -> "Mint16unsigned"
103  | Memory.QInt 4 -> "Mint32"
104  | Memory.QPtr -> "Mpointer Any"
105
106let rec print_expression p_id = function
107  | Cminor.Id id -> "Id " ^ (p_id id)
108  | Cminor.Cst cst -> Printf.sprintf "Cst (%s)" (print_constant cst)
109  | Cminor.Op1 (op1, e) ->
110      Printf.sprintf "Op1 %s (%s)" (print_op1 op1) (print_expression p_id e)
111  | Cminor.Op2 (op2, e1, e2) ->
112      Printf.sprintf "Op2 %s (%s) (%s)"
113        (print_op2 op2)
114        (print_expression p_id e1)
115        (print_expression p_id e2)
116  | Cminor.Mem (q, e) ->
117      Printf.sprintf "Mem %s (%s)" (print_quantity q) (print_expression p_id e)
118  | Cminor.Cond (e1, e2, e3) ->
119      Printf.sprintf "Cond (%s) (%s) (%s)"
120        (print_expression p_id e1)
121        (print_expression p_id e2)
122        (print_expression p_id e3)
123  | Cminor.Exp_cost (lab, e) ->
124      Printf.sprintf "Ecost C%s (%s)" lab (print_expression p_id e)
125
126
127let rec print_args p_id = 
128  MiscPottier.string_of_list "; " (print_expression p_id)
129
130
131let n_spaces n = String.make n ' '
132
133
134let print_sig s =
135  Printf.sprintf "mk_signature [%s] (%s)"
136    (MiscPottier.string_of_list "; " print_type s.AST.args)
137    (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
138                        | AST.Type_void  -> "None ?")
139
140let print_locals p_id vars =
141  (MiscPottier.string_of_list "; " p_id vars)
142
143
144let print_table n =
145  let f (case, exit) =
146    Printf.sprintf "(pair ?? (repr %d) %d)" case exit
147  in
148  MiscPottier.string_of_list (";\n" ^ n_spaces n) f
149
150let rec define_labels = function
151  | Cminor.St_assign (_, e) -> define_expr_labels e
152  | Cminor.St_store (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
153  | Cminor.St_call (_, _, args, _) -> String.concat "" (List.map define_expr_labels args)
154  | Cminor.St_tailcall (_, args, _) -> String.concat "" (List.map define_expr_labels args)
155  | Cminor.St_seq (s1, s2) -> define_labels s1 ^ define_labels s2
156  | Cminor.St_ifthenelse (e, s1, s2) -> define_expr_labels e ^ define_labels s1 ^ define_labels s2
157  | Cminor.St_loop s -> define_labels s
158  | Cminor.St_block s -> define_labels s
159  | Cminor.St_switch (e, _, _) -> define_expr_labels e
160  | Cminor.St_return (Some e) -> define_expr_labels e
161  | Cminor.St_label (l, s) ->
162      Printf.sprintf "definition L%s := ident_of_nat %d.\n%s"
163        l (fresh ()) (define_labels s)
164  | Cminor.St_cost (l, s) ->
165      Printf.sprintf "definition C%s := costlabel_of_nat %d.\n%s"
166        l (fresh ()) (define_labels s)
167  | _ -> ""
168
169let rec print_body p_id n = function
170  | Cminor.St_skip -> Printf.sprintf "%sSt_skip" (n_spaces n)
171  | Cminor.St_assign (id, e) ->
172      Printf.sprintf "%sSt_assign %s (%s)\n" (n_spaces n) (p_id id) (print_expression p_id e)
173  | Cminor.St_store (q, e1, e2) ->
174      Printf.sprintf "%sSt_store %s (%s) (%s)\n"
175        (n_spaces n)
176        (print_quantity q)
177        (print_expression p_id e1)
178        (print_expression p_id e2)
179  | Cminor.St_call (None, f, args, sg) ->
180      Printf.sprintf "%sSt_call (None ?) (%s) [%s]\n"
181        (n_spaces n)
182        (print_expression p_id f)
183        (print_args p_id args)
184  | Cminor.St_call (Some id, f, args, sg) ->
185      Printf.sprintf "%sSt_call (Some ? %s) (%s) [%s]\n"
186        (n_spaces n)
187        (p_id id)
188        (print_expression p_id f)
189        (print_args p_id args)
190  | Cminor.St_tailcall (f, args, sg) ->
191      Printf.sprintf "%sSt_tailcall (%s) [%s]\n"
192        (n_spaces n)
193        (print_expression p_id f)
194        (print_args p_id args)
195  | Cminor.St_seq (s1, s2) ->
196      Printf.sprintf "%sSt_seq (\n%s%s) (\n%s%s)\n"
197        (n_spaces n)
198        (print_body p_id (n+2) s1)
199        (n_spaces n)
200        (print_body p_id n s2)
201        (n_spaces n)
202  | Cminor.St_ifthenelse (e, s1, s2) ->
203      Printf.sprintf "%sSt_ifthenelse (%s) (\n%s%s) (\n%s%s)\n"
204        (n_spaces n)
205        (print_expression p_id e)
206        (print_body p_id (n+2) s1)
207        (n_spaces n)
208        (print_body p_id (n+2) s2)
209        (n_spaces n)
210  | Cminor.St_loop s ->
211      Printf.sprintf "%sSt_loop (\n%s%s)\n"
212        (n_spaces n)
213        (print_body p_id (n+2) s)
214        (n_spaces n)
215  | Cminor.St_block s ->
216      Printf.sprintf "%sSt_block (\n%s%s)\n"
217        (n_spaces n)
218        (print_body p_id (n+2) s)
219        (n_spaces n)
220  | Cminor.St_exit i ->
221      Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
222  | Cminor.St_switch (e, tbl, dflt) ->
223      Printf.sprintf "%sSt_switch (%s) [\n%s%s] %d\n"
224        (n_spaces n)
225        (print_expression p_id e)
226        (n_spaces (n+2))
227        (print_table ( n+2) tbl)
228        dflt
229  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
230  | Cminor.St_return (Some e) ->
231      Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_expression p_id e)
232  | Cminor.St_label (lbl, s) ->
233      Printf.sprintf "%sSt_label L%s (\n%s%s)\n" 
234        (n_spaces n)
235        lbl
236        (print_body p_id n s)
237        (n_spaces n)
238  | Cminor.St_goto lbl ->
239      Printf.sprintf "%sSt_goto L%s\n" (n_spaces n) lbl
240  | Cminor.St_cost (lbl, s) ->
241      Printf.sprintf "%sSt_cost C%s (\n%s%s)\n"
242        (n_spaces n) lbl (print_body p_id n s)
243        (n_spaces n)
244
245let print_ids fname vs =
246  List.fold_left (fun s v ->
247                  Printf.sprintf "%sdefinition id_%s_%s := ident_of_nat %d.\n"
248                                 s fname v (fresh ()))
249       "" vs
250
251let print_internal f_name f_def =
252  let fid = fresh () in
253  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
254  Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  [%s]\n  %d (\n%s\n)).\n\n"
255    f_name
256    fid
257    (print_ids f_name (f_def.Cminor.f_vars @ f_def.Cminor.f_params))
258    (define_labels f_def.Cminor.f_body)
259    f_name
260    (print_sig f_def.Cminor.f_sig)
261    (print_locals p_id f_def.Cminor.f_params)
262    (print_locals p_id f_def.Cminor.f_vars)
263    (print_locals p_id f_def.Cminor.f_ptrs)
264    f_def.Cminor.f_stacksize
265    (print_body p_id 2 f_def.Cminor.f_body)
266
267
268let print_external f def =
269  Printf.sprintf "definition id_%s := ident_of_nat %d.\ndefinition f_%s := External internal_function (mk_external_function id_%s (%s)).\n"
270    f
271    (fresh ())
272    f
273    f
274    (print_sig def.AST.ef_sig)
275
276
277let print_funct (f_name, f_def) = match f_def with
278  | Cminor.F_int f_def -> print_internal f_name f_def
279  | Cminor.F_ext f_def -> print_external f_name f_def
280
281let print_functs = List.fold_left (fun s f -> s ^ (print_funct f)) ""
282
283
284let print_fun' n functs =
285  MiscPottier.string_of_list ";\n" (fun (f,def) ->
286    Printf.sprintf "%s(pair ?? id_%s f_%s)"
287      (n_spaces n) 
288      f
289      f)
290      functs
291
292let print_main n main =
293  Printf.sprintf "%s%s"
294    (n_spaces n)
295    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
296
297let define_var_id (id,_) =
298  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
299
300let define_var_ids =
301  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
302
303let print_program p =
304  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n"
305    (define_var_ids p.Cminor.vars)
306    (print_functs p.Cminor.functs)
307    (print_fun' 2 p.Cminor.functs)
308    (print_main 2 p.Cminor.main)
309    (print_vars 2 p.Cminor.vars)
310
Note: See TracBrowser for help on using the repository browser.