1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 of *)
(* the License, or (at your option) any later version. *)
(* This file is also distributed under the terms of the *)
(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open Format
open Camlcoq
open Ctypes
open ExportBase
(* Raw attributes *)
let attribute p a =
if a = noattr then
fprintf p "noattr"
else
fprintf p "{| attr_volatile := %B; attr_alignas := %a |}"
a.attr_volatile
(print_option coqN) a.attr_alignas
(* Raw int size and signedness *)
let intsize p sz =
fprintf p "%s"
(match sz with
| I8 -> "I8"
| I16 -> "I16"
| I32 -> "I32"
| IBool -> "IBool")
let signedness p sg =
fprintf p "%s"
(match sg with
| Signed -> "Signed"
| Unsigned -> "Unsigned")
(* Types *)
let rec typ p t =
match attr_of_type t with
| { attr_volatile = false; attr_alignas = None} ->
rtyp p t
| { attr_volatile = true; attr_alignas = None} ->
fprintf p "(tvolatile %a)" rtyp t
| { attr_volatile = false; attr_alignas = Some n} ->
fprintf p "(talignas %a %a)" coqN n rtyp t
| { attr_volatile = true; attr_alignas = Some n} ->
fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t
and rtyp p = function
| Tvoid -> fprintf p "tvoid"
| Ctypes.Tint(sz, sg, _) ->
fprintf p "%s" (
match sz, sg with
| I8, Signed -> "tschar"
| I8, Unsigned -> "tuchar"
| I16, Signed -> "tshort"
| I16, Unsigned -> "tushort"
| I32, Signed -> "tint"
| I32, Unsigned -> "tuint"
| IBool, _ -> "tbool")
| Ctypes.Tlong(sg, _) ->
fprintf p "%s" (
match sg with
| Signed -> "tlong"
| Unsigned -> "tulong")
| Ctypes.Tfloat(sz, _) ->
fprintf p "%s" (
match sz with
| F32 -> "tfloat"
| F64 -> "tdouble")
| Tpointer(t, _) ->
fprintf p "(tptr %a)" typ t
| Tarray(t, sz, _) ->
fprintf p "(tarray %a %ld)" typ t (Z.to_int32 sz)
| Tfunction(targs, tres, cc) ->
fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]"
typlist targs typ tres callconv cc
| Tstruct(id, _) ->
fprintf p "(Tstruct %a noattr)" ident id
| Tunion(id, _) ->
fprintf p "(Tunion %a noattr)" ident id
and typlist p = function
| Tnil ->
fprintf p "Tnil"
| Tcons(t, tl) ->
fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl
(* Composite definitions *)
let print_member p = function
| Member_plain (id, ty) ->
fprintf p "@[<hov 2>Member_plain@ %a@ %a@]"
ident id typ ty
| Member_bitfield (id, sz, sg, a, width, pad) ->
fprintf p "@[<hov 2>Member_bitfield@ %a@ %a@ %a@ %a@ %a@ %B@]"
ident id
intsize sz
signedness sg
attribute a
coqZ width
pad
let print_composite_definition p (Composite(id, su, m, a)) =
fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]"
ident id
(match su with Struct -> "Struct" | Union -> "Union")
(print_list print_member) m
attribute a
|
