source: Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml @ 461

Last change on this file since 461 was 461, checked in by campbell, 8 years ago

Handle null pointer constants properly for generic pointers (introducing a 24-bit quantity for them).

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 (s,t) -> (* XXX *)
109      name_cdecl ("*" ^ id) t
110  | Tarray(s, 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 sspace = function
144| Any -> "Any"
145| Data -> "Data"
146| IData -> "IData"
147| PData -> "PData"
148| XData -> "XData"
149| Code -> "Code"
150
151let rec stype ty =
152  match ty with
153  | Tvoid -> "Tvoid"
154  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
155  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
156  | Tpointer (sp, t) -> "(Tpointer " ^ sspace sp ^ " " ^ stype t ^ ")"
157  | Tarray(sp, t, n) -> "(Tarray " ^ sspace sp ^ " " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
158  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
159  | Tstruct(name, fld) ->
160      fieldlist "(Tstruct (succ_pos_of_nat " name fld
161  | Tunion(name, fld) ->
162      fieldlist "(Tunion (succ_pos_of_nat " name fld
163  | Tcomp_ptr name ->
164      "(Tcomp_ptr (succ_pos_of_nat " ^ id_s name ^ "))"
165 and typelist l =
166    let b = Buffer.create 20 in
167      let rec add_types = function
168        | [] -> Buffer.add_string b "Tnil"
169        | t1::tl ->
170            Buffer.add_string b "(Tcons ";
171            Buffer.add_string b (stype t1);
172            Buffer.add_char b ' ';
173            add_types tl;
174            Buffer.add_char b ')'
175      in add_types l;
176        Buffer.contents b
177 and fieldlist s name l =
178    let b = Buffer.create 20 in
179      Buffer.add_string b s;
180      Buffer.add_string b (id_s name);
181      Buffer.add_string b ") ";
182      let rec add_fields = function
183        | [] -> Buffer.add_string b "Fnil"
184        | (id, ty)::tl ->
185            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
186            Buffer.add_string b (id_s id);
187            Buffer.add_string b ") ";
188            Buffer.add_string b (stype ty);
189            Buffer.add_char b ' ';
190            add_fields tl;
191            Buffer.add_char b ')'
192      in add_fields l;
193        Buffer.add_char b ')';
194        Buffer.contents b
195
196let name_type ty = name_cdecl "" ty
197
198(* Expressions *)
199
200let rec print_expr p (Expr (eb, ty)) =
201  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
202and print_expr_descr p eb =
203  match eb with
204  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
205  | Econst_int n ->
206      fprintf p "(Econst_int (repr %d))" n
207  | Econst_float f ->
208      fprintf p "(Econst_float %F)" f
209  | Evar id ->
210      fprintf p "(Evar (succ_pos_of_nat %d))" (id_i id)
211  | Eunop(op, e1) ->
212      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
213  | Ederef e ->
214      fprintf p "(Ederef@ %a)" print_expr e
215  | Eaddrof e ->
216      fprintf p "(Eaddrof@ %a)" print_expr e
217  | Ebinop(op, e1, e2) ->
218      fprintf p "(Ebinop@ %s@ %a@ %a)"
219                (name_binop op)
220                print_expr e1
221                print_expr e2
222  | Ecast(ty, e1) ->
223      fprintf p "(Ecast %s@ %a)"
224                (stype ty)
225                print_expr e1
226  | Econdition(e1, e2, e3) ->
227      fprintf p "(Econdition %a@ %a@ %a)"
228                print_expr e1
229                print_expr e2
230                print_expr e3
231  | Eandbool(e1, e2) ->
232      fprintf p "(Eandbool %a@ %a)"
233                print_expr e1
234                print_expr e2
235  | Eorbool(e1, e2) ->
236      fprintf p "(Eorbool %a@ %a)"
237                print_expr e1
238                print_expr e2
239  | Esizeof ty ->
240      fprintf p "(Esizeof %s)" (stype ty)
241  | Efield(e1, id) ->
242      fprintf p "(Efield %a (succ_pos_of_nat %i))" print_expr e1 (id_i id)
243
244let rec print_expr_list p (first, el) =
245  match el with
246  | [] -> ()
247  | e1 :: et ->
248      if not first then fprintf p ",@ ";
249      print_expr p e1;
250      print_expr_list p (false, et)
251
252let rec print_stmt p s =
253  match s with
254  | Scost (_, s') -> print_stmt p s'
255  | Sskip ->
256      fprintf p "Sskip"
257  | Sassign(e1, e2) ->
258      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
259  | Scall(None, e1, el) ->
260      fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
261                print_expr e1
262                (print_list print_expr) el
263  | Scall(Some lhs, e1, el) ->
264      fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
265                print_expr lhs
266                print_expr e1
267                (print_list print_expr) el
268  | Ssequence(s1, s2) ->
269      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
270  | Sifthenelse(e, s1, s2) ->
271      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
272              print_expr e
273              print_stmt s1
274              print_stmt s2
275  | Swhile(e, s) ->
276      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
277              print_expr e
278              print_stmt s
279  | Sdowhile(e, s) ->
280      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
281              print_expr e
282              print_stmt s
283  | Sfor(s_init, e, s_iter, s_body) ->
284      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
285              print_stmt s_init
286              print_expr e
287              print_stmt s_iter
288              print_stmt s_body
289  | Sbreak ->
290      fprintf p "Sbreak"
291  | Scontinue ->
292      fprintf p "Scontinue"
293  | Sswitch(e, cases) ->
294      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
295              print_expr e
296              print_cases cases
297  | Sreturn None ->
298      fprintf p "(Sreturn (None ?))"
299  | Sreturn (Some e) ->
300      fprintf p "(Sreturn (Some ? %a))" print_expr e
301  | Slabel(lbl, s1) ->
302      fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
303  | Sgoto lbl ->
304      fprintf p "(Sgoto (succ_pos_of_nat %i))" (id_i lbl)
305
306and print_cases p cases =
307  match cases with
308  | LSdefault s ->
309      fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
310  | LScase(lbl, s, rem) ->
311      fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
312              lbl
313              print_stmt s
314              print_cases rem
315
316let name_function_parameters params =
317  let b = Buffer.create 20 in
318  Buffer.add_char b '[';
319    let rec add_params first = function
320      | [] -> ()
321      | (id, ty) :: rem ->
322          if not first then Buffer.add_string b "; ";
323          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
324          Buffer.add_string b (id_s id);
325          Buffer.add_string b ") ";
326          Buffer.add_string b (stype ty);
327          add_params false rem in
328      add_params true params;
329      Buffer.add_char b ']';
330      Buffer.contents b
331
332let print_function p f =
333  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
334    (name_function_parameters f.fn_params)
335    (name_function_parameters f.fn_vars);
336  print_stmt p f.fn_body;
337  fprintf p "@;<0 -2>@]@ @ "
338
339let print_fundef p (id, fd) =
340  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
341  match fd with
342  | External(id', args, res) ->
343      fprintf p "(External (succ_pos_of_nat %i) %s %s)@]" (id_i id) (typelist args) (stype res)
344  | Internal f ->
345      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
346
347let string_of_init id =
348  let b = Buffer.create (List.length id) in
349  let add_init = function
350  | Init_int8 c ->
351      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
352      then Buffer.add_char b (Char.chr c)
353      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
354  | _ ->
355      assert false
356  in List.iter add_init id; Buffer.contents b
357
358let chop_last_nul id =
359  match List.rev id with
360  | Init_int8 0 :: tl -> List.rev tl
361  | _ -> id
362
363let print_init p = function
364  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
365  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
366  | Init_int24 n -> fprintf p "(Init_int24 (repr %d))@ " n
367  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
368  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
369  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
370  | Init_space n -> fprintf p "(Init_space %d)@ " n
371  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %d (repr %d))" (id_i symb) ofs
372
373let re_string_literal = Str.regexp "__stringlit_[0-9]+"
374
375let print_globvar p ((((id, init), sp), ty)) =
376  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat %i (* %s *))@ %a)@ %s)@ %s)@]"
377    (id_i id)
378    id
379    (print_list print_init) init
380    (sspace sp)
381    (stype ty)
382
383(* Collect struct and union types *)
384
385let rec collect_type = function
386  | Tvoid -> ()
387  | Tint(sz, sg) -> ()
388  | Tfloat sz -> ()
389  | Tpointer (_,t) -> collect_type t
390  | Tarray(_, t, n) -> collect_type t
391  | Tfunction(args, res) -> List.iter collect_type args; collect_type res
392  | Tstruct(id, fld) -> register_struct_union id fld; List.iter collect_field fld
393  | Tunion(id, fld) -> register_struct_union id fld; List.iter collect_field fld
394  | Tcomp_ptr _ -> ()
395
396and collect_field f = collect_type (snd f)
397
398let rec collect_expr (Expr(ed, ty)) =
399  match ed with
400  | Ecost (_, e) -> collect_expr e
401  | Econst_int n -> ()
402  | Econst_float f -> ()
403  | Evar id -> ()
404  | Eunop(op, e1) -> collect_expr e1
405  | Ederef e -> collect_expr e
406  | Eaddrof e -> collect_expr e
407  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
408  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
409  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
410  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
411  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
412  | Esizeof ty -> collect_type ty
413  | Efield(e1, id) -> collect_expr e1
414
415let rec collect_expr_list = function
416  | [] -> ()
417  | hd :: tl -> collect_expr hd; collect_expr_list tl
418
419let rec collect_stmt = function
420  | Scost (_, s) -> collect_stmt s
421  | Sskip -> ()
422  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
423  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
424  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
425  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
426  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
427  | Swhile(e, s) -> collect_expr e; collect_stmt s
428  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
429  | Sfor(s_init, e, s_iter, s_body) ->
430      collect_stmt s_init; collect_expr e;
431      collect_stmt s_iter; collect_stmt s_body
432  | Sbreak -> ()
433  | Scontinue -> ()
434  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
435  | Sreturn None -> ()
436  | Sreturn (Some e) -> collect_expr e
437  | Slabel(lbl, s) -> collect_stmt s
438  | Sgoto lbl -> ()
439
440and collect_cases = function
441  | LSdefault s -> collect_stmt s
442  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
443
444let collect_function f =
445  collect_type f.fn_return;
446  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
447  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
448  collect_stmt f.fn_body
449
450let collect_fundef (id, fd) =
451  match fd with
452  | External(_, args, res) -> List.iter collect_type args; collect_type res
453  | Internal f -> collect_function f
454
455let collect_globvar ((id, init), ty) =
456  collect_type ty
457
458let collect_program p =
459  List.iter collect_globvar p.prog_vars;
460  List.iter collect_fundef p.prog_funct
461
462let declare_struct_or_union p (name, fld) =
463  fprintf p "%s;@ @ " name
464
465let print_struct_or_union p (name, fld) =
466  fprintf p "@[<v 2>%s {" name;
467  let rec print_field (id, ty) =
468    fprintf p "@ %s;" (name_cdecl id ty) in
469  List.iter print_field fld;
470  fprintf p "@;<0 -2>};@]@ "
471
472let print_program p prog =
473  struct_unions := StructUnionSet.empty;
474  collect_program prog;
475  fprintf p "include \"Csyntax.ma\".@\n@\n";
476  fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
477(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
478  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
479  print_list print_fundef p prog.prog_funct;
480  fprintf p "@\n(succ_pos_of_nat %i)@\n" (id_i "main");
481  print_list print_globvar p prog.prog_vars;
482  fprintf p "@;<0 -2>.@]@."
483
484
Note: See TracBrowser for help on using the repository browser.