source: src/Clight/clightPrintMatita.ml @ 786

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

A version of the clight matita term printer for the current prototype.

File size: 15.2 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(** Pretty-printer for Csyntax *)
17
18open Format
19open AST
20open Clight
21
22(* If there's name hiding this might get us into trouble. *)
23let ident_map = Hashtbl.create 13;;
24let ident_next = ref 0;;
25let id_i n =
26  try Hashtbl.find ident_map n
27  with Not_found ->
28    let i = !ident_next in
29    Hashtbl.add ident_map n i;
30    ident_next := i+1;
31    i
32let id_s n = string_of_int (id_i n)
33
34let print_list f fmt l =
35  let rec aux fmt = function
36      | [] -> ()
37      | [x] -> f fmt x
38      | h::t -> f fmt h; fprintf fmt ";@ "; aux fmt t
39  in
40  fprintf fmt "@[[%a]@]" aux l
41
42let name_unop = function
43  | Onotbool -> "Onotbool"
44  | Onotint  -> "Onotint"
45  | Oneg     -> "Oneg"
46
47
48let name_binop = function
49  | Oadd -> "Oadd"
50  | Osub -> "Osub"
51  | Omul -> "Omul"
52  | Odiv -> "Odiv"
53  | Omod -> "Omod"
54  | Oand -> "Oand"
55  | Oor  -> "Oor"
56  | Oxor -> "Oxor"
57  | Oshl -> "Oshl"
58  | Oshr -> "Oshr"
59  | Oeq  -> "Oeq"
60  | One  -> "One"
61  | Olt  -> "Olt"
62  | Ogt  -> "Ogt"
63  | Ole  -> "Ole"
64  | Oge  -> "Oge"
65
66let name_inttype sz sg =
67  match sz, sg with
68  | I8, Signed    -> "I8 Signed   "
69  | I8, Unsigned  -> "I8 Unsigned "
70  | I16, Signed   -> "I16 Signed  "
71  | I16, Unsigned -> "I16 Unsigned"
72  | I32, Signed   -> "I32 Signed  "
73  | I32, Unsigned -> "I32 Unsigned"
74
75let name_floattype sz =
76  match sz with
77  | F32 -> "F32"
78  | F64 -> "F64"
79
80(* Collecting the names and fields of structs and unions *)
81
82module StructUnionSet = Set.Make(struct
83  type t = string * (ident*ctype) list
84  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
85end)
86
87let struct_unions = ref StructUnionSet.empty
88
89let register_struct_union id fld =
90  struct_unions := StructUnionSet.add (id, fld) !struct_unions
91
92(* Declarator (identifier + type) *)
93
94let name_optid id =
95  if id = "" then "" else " " ^ id
96
97let parenthesize_if_pointer id =
98  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
99
100let rec name_cdecl id ty =
101  match ty with
102  | Tvoid ->
103      "void" ^ name_optid id
104  | Tint(sz, sg) ->
105      name_inttype sz sg ^ name_optid id
106  | Tfloat sz ->
107      name_floattype sz ^ name_optid id
108  | Tpointer t -> (* XXX *)
109      name_cdecl ("*" ^ id) t
110  | Tarray( t, n) -> (* XXX *)
111      name_cdecl
112        (sprintf "%s[%d]" (parenthesize_if_pointer id) n)
113        t
114  | Tfunction(args, res) ->
115      let b = Buffer.create 20 in
116      if id = ""
117      then Buffer.add_string b "(*)"
118      else Buffer.add_string b (parenthesize_if_pointer id);
119      Buffer.add_char b '(';
120      begin match args with
121      | [] ->
122          Buffer.add_string b "void"
123      | _ ->
124          let rec add_args first = function
125          | [] -> ()
126          | t1::tl ->
127              if not first then Buffer.add_string b ", ";
128              Buffer.add_string b (name_cdecl "" t1);
129              add_args false tl in
130          add_args true args
131      end;
132      Buffer.add_char b ')';
133      name_cdecl (Buffer.contents b) res
134  | Tstruct(name, fld) ->
135      name ^ name_optid id
136  | Tunion(name, fld) ->
137      name ^ name_optid id
138  | Tcomp_ptr name ->
139      name ^ " *" ^ id
140
141(* Type *)
142
143let rec stype ty =
144  match ty with
145  | Tvoid -> "Tvoid"
146  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
147  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
148  | Tpointer t -> "(Tpointer Any " ^ stype t ^ ")"
149  | Tarray(t, n) -> "(Tarray Any " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
150  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
151  | Tstruct(name, fld) ->
152      fieldlist "(Tstruct (ident_of_nat " name fld
153  | Tunion(name, fld) ->
154      fieldlist "(Tunion (ident_of_nat " name fld
155  | Tcomp_ptr (name) ->
156      "(Tcomp_ptr Any (ident_of_nat " ^ id_s name ^ "))"
157 and typelist l =
158    let b = Buffer.create 20 in
159      let rec add_types = function
160        | [] -> Buffer.add_string b "Tnil"
161        | t1::tl ->
162            Buffer.add_string b "(Tcons ";
163            Buffer.add_string b (stype t1);
164            Buffer.add_char b ' ';
165            add_types tl;
166            Buffer.add_char b ')'
167      in add_types l;
168        Buffer.contents b
169 and fieldlist s name l =
170    let b = Buffer.create 20 in
171      Buffer.add_string b s;
172      Buffer.add_string b (id_s name);
173      Buffer.add_string b ") ";
174      let rec add_fields = function
175        | [] -> Buffer.add_string b "Fnil"
176        | (id, ty)::tl ->
177            Buffer.add_string b "(Fcons (ident_of_nat ";
178            Buffer.add_string b (id_s id);
179            Buffer.add_string b ") ";
180            Buffer.add_string b (stype ty);
181            Buffer.add_char b ' ';
182            add_fields tl;
183            Buffer.add_char b ')'
184      in add_fields l;
185        Buffer.add_char b ')';
186        Buffer.contents b
187
188let name_type ty = name_cdecl "" ty
189
190(* Expressions *)
191
192let rec print_expr p (Expr (eb, ty)) =
193  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
194and print_expr_descr p eb =
195  match eb with
196  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
197  | Econst_int n ->
198      fprintf p "(Econst_int (repr %d))" n
199  | Econst_float f ->
200      fprintf p "(Econst_float %F)" f
201  | Evar id ->
202      fprintf p "(Evar (ident_of_nat %d))" (id_i id)
203  | Eunop(op, e1) ->
204      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
205  | Ederef e ->
206      fprintf p "(Ederef@ %a)" print_expr e
207  | Eaddrof e ->
208      fprintf p "(Eaddrof@ %a)" print_expr e
209  | Ebinop(op, e1, e2) ->
210      fprintf p "(Ebinop@ %s@ %a@ %a)"
211                (name_binop op)
212                print_expr e1
213                print_expr e2
214  | Ecast(ty, e1) ->
215      fprintf p "(Ecast %s@ %a)"
216                (stype ty)
217                print_expr e1
218  | Econdition(e1, e2, e3) ->
219      fprintf p "(Econdition %a@ %a@ %a)"
220                print_expr e1
221                print_expr e2
222                print_expr e3
223  | Eandbool(e1, e2) ->
224      fprintf p "(Eandbool %a@ %a)"
225                print_expr e1
226                print_expr e2
227  | Eorbool(e1, e2) ->
228      fprintf p "(Eorbool %a@ %a)"
229                print_expr e1
230                print_expr e2
231  | Esizeof ty ->
232      fprintf p "(Esizeof %s)" (stype ty)
233  | Efield(e1, id) ->
234      fprintf p "(Efield %a (ident_of_nat %i))" print_expr e1 (id_i id)
235
236
237let rec print_stmt p s =
238  match s with
239  | Scost (_, s') -> print_stmt p s'
240  | Sskip ->
241      fprintf p "Sskip"
242  | Sassign(e1, e2) ->
243      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
244  | Scall(None, e1, el) ->
245      fprintf p "@[<hv 2>(Scall (None expr) %a @[<hov 0>%a@])@]"
246                print_expr e1
247                (print_list print_expr) el
248  | Scall(Some lhs, e1, el) ->
249      fprintf p "@[<hv 2>(Scall (Some expr %a)@ %a@ @[<hov 0>%a@])@]"
250                print_expr lhs
251                print_expr e1
252                (print_list print_expr) el
253  | Ssequence(s1, s2) ->
254      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
255  | Sifthenelse(e, s1, s2) ->
256      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
257              print_expr e
258              print_stmt s1
259              print_stmt s2
260  | Swhile(e, s) ->
261      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
262              print_expr e
263              print_stmt s
264  | Sdowhile(e, s) ->
265      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
266              print_expr e
267              print_stmt s
268  | Sfor(s_init, e, s_iter, s_body) ->
269      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
270              print_stmt s_init
271              print_expr e
272              print_stmt s_iter
273              print_stmt s_body
274  | Sbreak ->
275      fprintf p "Sbreak"
276  | Scontinue ->
277      fprintf p "Scontinue"
278  | Sswitch(e, cases) ->
279      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
280              print_expr e
281              print_cases cases
282  | Sreturn None ->
283      fprintf p "(Sreturn (None expr))"
284  | Sreturn (Some e) ->
285      fprintf p "(Sreturn (Some expr %a))" print_expr e
286  | Slabel(lbl, s1) ->
287      fprintf p "(Slabel (ident_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
288  | Sgoto lbl ->
289      fprintf p "(Sgoto (ident_of_nat %i))" (id_i lbl)
290
291and print_cases p cases =
292  match cases with
293  | LSdefault s ->
294      fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
295  | LScase(lbl, s, rem) ->
296      fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
297              lbl
298              print_stmt s
299              print_cases rem
300
301let name_function_parameters params =
302  let b = Buffer.create 20 in
303  Buffer.add_char b '[';
304    let rec add_params first = function
305      | [] -> ()
306      | (id, ty) :: rem ->
307          if not first then Buffer.add_string b "; ";
308          Buffer.add_string b "〈ident_of_nat ";
309          Buffer.add_string b (id_s id);
310          Buffer.add_string b ", ";
311          Buffer.add_string b (stype ty);
312          Buffer.add_string b "〉 ";
313          add_params false rem in
314      add_params true params;
315      Buffer.add_char b ']';
316      Buffer.contents b
317
318let print_function p f =
319  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
320    (name_function_parameters f.fn_params)
321    (name_function_parameters f.fn_vars);
322  print_stmt p f.fn_body;
323  fprintf p "@;<0 -2>@]@ @ "
324
325let print_fundef p (id, fd) =
326  fprintf p "@[<v 2>〈ident_of_nat %i (* %s *), " (id_i id) id;
327  match fd with
328  | External(id', args, res) ->
329      fprintf p "CL_External (ident_of_nat %i) %s %s〉@]" (id_i id) (typelist args) (stype res)
330  | Internal f ->
331      fprintf p "CL_Internal (@ %a@;<0 -2>)〉@]" print_function f
332
333let string_of_init id =
334  let b = Buffer.create (List.length id) in
335  let add_init = function
336  | Init_int8 c ->
337      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
338      then Buffer.add_char b (Char.chr c)
339      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
340  | _ ->
341      assert false
342  in List.iter add_init id; Buffer.contents b
343
344let chop_last_nul id =
345  match List.rev id with
346  | Init_int8 0 :: tl -> List.rev tl
347  | _ -> id
348
349let print_init p = function
350  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
351  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
352  (*| Init_null r -> fprintf p "(Init_null Any)@"*)
353  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
354  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
355  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
356  | Init_space n -> fprintf p "(Init_space %d)@ " n
357  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) (repr %d))" (id_i symb) ofs
358
359let re_string_literal = Str.regexp "__stringlit_[0-9]+"
360
361let print_globvar p (((id, init), ty)) =
362  fprintf p "@[<hov 2>〈〈〈ident_of_nat %i (* %s *),@ %a〉,@ Any〉,@ %s〉@]"
363    (id_i id)
364    id
365    (print_list print_init) init
366    (stype ty)
367
368(* Collect struct and union types *)
369
370let rec collect_type = function
371  | Tvoid -> ()
372  | Tint(sz, sg) -> ()
373  | Tfloat sz -> ()
374  | Tpointer t -> collect_type t
375  | Tarray(t, n) -> collect_type t
376  | Tfunction(args, res) -> List.iter collect_type args; collect_type res
377  | Tstruct(id, fld) -> register_struct_union id fld; List.iter collect_field fld
378  | Tunion(id, fld) -> register_struct_union id fld; List.iter collect_field fld
379  | Tcomp_ptr _ -> ()
380
381and collect_field f = collect_type (snd f)
382
383let rec collect_expr (Expr(ed, ty)) =
384  match ed with
385  | Ecost (_, e) -> collect_expr e
386  | Econst_int n -> ()
387  | Econst_float f -> ()
388  | Evar id -> ()
389  | Eunop(op, e1) -> collect_expr e1
390  | Ederef e -> collect_expr e
391  | Eaddrof e -> collect_expr e
392  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
393  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
394  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
395  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
396  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
397  | Esizeof ty -> collect_type ty
398  | Efield(e1, id) -> collect_expr e1
399
400let rec collect_expr_list = function
401  | [] -> ()
402  | hd :: tl -> collect_expr hd; collect_expr_list tl
403
404let rec collect_stmt = function
405  | Scost (_, s) -> collect_stmt s
406  | Sskip -> ()
407  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
408  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
409  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
410  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
411  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
412  | Swhile(e, s) -> collect_expr e; collect_stmt s
413  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
414  | Sfor(s_init, e, s_iter, s_body) ->
415      collect_stmt s_init; collect_expr e;
416      collect_stmt s_iter; collect_stmt s_body
417  | Sbreak -> ()
418  | Scontinue -> ()
419  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
420  | Sreturn None -> ()
421  | Sreturn (Some e) -> collect_expr e
422  | Slabel(lbl, s) -> collect_stmt s
423  | Sgoto lbl -> ()
424
425and collect_cases = function
426  | LSdefault s -> collect_stmt s
427  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
428
429let collect_function f =
430  collect_type f.fn_return;
431  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
432  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
433  collect_stmt f.fn_body
434
435let collect_fundef (id, fd) =
436  match fd with
437  | External(_, args, res) -> List.iter collect_type args; collect_type res
438  | Internal f -> collect_function f
439
440let collect_globvar ((id, init), ty) =
441  collect_type ty
442
443let collect_program p =
444  List.iter collect_globvar p.prog_vars;
445  List.iter collect_fundef p.prog_funct
446
447let declare_struct_or_union p (name, fld) =
448  fprintf p "%s;@ @ " name
449
450let print_struct_or_union p (name, fld) =
451  fprintf p "@[<v 2>%s {" name;
452  let rec print_field (id, ty) =
453    fprintf p "@ %s;" (name_cdecl id ty) in
454  List.iter print_field fld;
455  fprintf p "@;<0 -2>};@]@ "
456
457let print_program0 p prog =
458  struct_unions := StructUnionSet.empty;
459  collect_program prog;
460  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
461  fprintf p "@[<v 2>definition myprog := mk_program clight_fundef type@ ";
462(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
463  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
464  print_list print_fundef p prog.prog_funct;
465  fprintf p "@\n(ident_of_nat %i)@\n" (id_i "main");
466  print_list print_globvar p prog.prog_vars;
467  fprintf p "@;<0 -2>.@]@\n@\n";
468  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).@\n";
469  fprintf p "normalize  (* you can examine the result here *)@."
470
471let print_program prog =
472  let _ = Format.flush_str_formatter () in
473  print_program0 Format.str_formatter prog;
474  flush_str_formatter ()
475
476
Note: See TracBrowser for help on using the repository browser.