source: src/Clight/clightPrintMatita.ml @ 978

Last change on this file since 978 was 965, checked in by campbell, 10 years ago

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