blob: c2b38a9261a900bf4c0e4be05dd7dfc37b4e8904 (
plain)
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
(* *********************************************************************)
(* *)
(* 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 General Public License as published by *)
(* the Free Software Foundation, either version 2 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. *)
(* *)
(* *********************************************************************)
(** All imports and definitions used by .v Clight files generated by clightgen *)
From Coq Require Import Ascii String List ZArith.
From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
Definition tvoid := Tvoid.
Definition tschar := Tint I8 Signed noattr.
Definition tuchar := Tint I8 Unsigned noattr.
Definition tshort := Tint I16 Signed noattr.
Definition tushort := Tint I16 Unsigned noattr.
Definition tint := Tint I32 Signed noattr.
Definition tuint := Tint I32 Unsigned noattr.
Definition tbool := Tint IBool Unsigned noattr.
Definition tlong := Tlong Signed noattr.
Definition tulong := Tlong Unsigned noattr.
Definition tfloat := Tfloat F32 noattr.
Definition tdouble := Tfloat F64 noattr.
Definition tptr (t: type) := Tpointer t noattr.
Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}.
Definition tattr (a: attr) (ty: type) :=
match ty with
| Tvoid => Tvoid
| Tint sz si _ => Tint sz si a
| Tlong si _ => Tlong si a
| Tfloat sz _ => Tfloat sz a
| Tpointer elt _ => Tpointer elt a
| Tarray elt sz _ => Tarray elt sz a
| Tfunction args res cc => Tfunction args res cc
| Tstruct id _ => Tstruct id a
| Tunion id _ => Tunion id a
end.
Definition tvolatile (ty: type) := tattr volatile_attr ty.
Definition talignas (n: N) (ty: type) :=
tattr {| attr_volatile := false; attr_alignas := Some n |} ty.
Definition tvolatile_alignas (n: N) (ty: type) :=
tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
Definition wf_composites (types: list composite_definition) : Prop :=
match build_composite_env types with OK _ => True | Error _ => False end.
Definition build_composite_env' (types: list composite_definition)
(WF: wf_composites types)
: { ce | build_composite_env types = OK ce }.
Proof.
revert WF. unfold wf_composites. case (build_composite_env types); intros.
- exists c; reflexivity.
- contradiction.
Defined.
Definition mkprogram (types: list composite_definition)
(defs: list (ident * globdef fundef type))
(public: list ident)
(main: ident)
(WF: wf_composites types) : Clight.program :=
let (ce, EQ) := build_composite_env' types WF in
{| prog_defs := defs;
prog_public := public;
prog_main := main;
prog_types := types;
prog_comp_env := ce;
prog_comp_env_eq := EQ |}.
(** The following encoding of character strings as positive numbers
must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
Definition append_bit_pos (b: bool) (p: positive) : positive :=
if b then xI p else xO p.
Definition append_char_pos_default (c: ascii) (p: positive) : positive :=
let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in
xI (xI (xI (xI (xI (xI
(append_bit_pos b0 (append_bit_pos b1
(append_bit_pos b2 (append_bit_pos b3
(append_bit_pos b4 (append_bit_pos b5
(append_bit_pos b6 (append_bit_pos b7 p))))))))))))).
Definition append_char_pos (c: ascii) (p: positive) : positive :=
match c with
| "0"%char => xO (xO (xO (xO (xO (xO p)))))
| "1"%char => xI (xO (xO (xO (xO (xO p)))))
| "2"%char => xO (xI (xO (xO (xO (xO p)))))
| "3"%char => xI (xI (xO (xO (xO (xO p)))))
| "4"%char => xO (xO (xI (xO (xO (xO p)))))
| "5"%char => xI (xO (xI (xO (xO (xO p)))))
| "6"%char => xO (xI (xI (xO (xO (xO p)))))
| "7"%char => xI (xI (xI (xO (xO (xO p)))))
| "8"%char => xO (xO (xO (xI (xO (xO p)))))
| "9"%char => xI (xO (xO (xI (xO (xO p)))))
| "a"%char => xO (xI (xO (xI (xO (xO p)))))
| "b"%char => xI (xI (xO (xI (xO (xO p)))))
| "c"%char => xO (xO (xI (xI (xO (xO p)))))
| "d"%char => xI (xO (xI (xI (xO (xO p)))))
| "e"%char => xO (xI (xI (xI (xO (xO p)))))
| "f"%char => xI (xI (xI (xI (xO (xO p)))))
| "g"%char => xO (xO (xO (xO (xI (xO p)))))
| "h"%char => xI (xO (xO (xO (xI (xO p)))))
| "i"%char => xO (xI (xO (xO (xI (xO p)))))
| "j"%char => xI (xI (xO (xO (xI (xO p)))))
| "k"%char => xO (xO (xI (xO (xI (xO p)))))
| "l"%char => xI (xO (xI (xO (xI (xO p)))))
| "m"%char => xO (xI (xI (xO (xI (xO p)))))
| "n"%char => xI (xI (xI (xO (xI (xO p)))))
| "o"%char => xO (xO (xO (xI (xI (xO p)))))
| "p"%char => xI (xO (xO (xI (xI (xO p)))))
| "q"%char => xO (xI (xO (xI (xI (xO p)))))
| "r"%char => xI (xI (xO (xI (xI (xO p)))))
| "s"%char => xO (xO (xI (xI (xI (xO p)))))
| "t"%char => xI (xO (xI (xI (xI (xO p)))))
| "u"%char => xO (xI (xI (xI (xI (xO p)))))
| "v"%char => xI (xI (xI (xI (xI (xO p)))))
| "w"%char => xO (xO (xO (xO (xO (xI p)))))
| "x"%char => xI (xO (xO (xO (xO (xI p)))))
| "y"%char => xO (xI (xO (xO (xO (xI p)))))
| "z"%char => xI (xI (xO (xO (xO (xI p)))))
| "A"%char => xO (xO (xI (xO (xO (xI p)))))
| "B"%char => xI (xO (xI (xO (xO (xI p)))))
| "C"%char => xO (xI (xI (xO (xO (xI p)))))
| "D"%char => xI (xI (xI (xO (xO (xI p)))))
| "E"%char => xO (xO (xO (xI (xO (xI p)))))
| "F"%char => xI (xO (xO (xI (xO (xI p)))))
| "G"%char => xO (xI (xO (xI (xO (xI p)))))
| "H"%char => xI (xI (xO (xI (xO (xI p)))))
| "I"%char => xO (xO (xI (xI (xO (xI p)))))
| "J"%char => xI (xO (xI (xI (xO (xI p)))))
| "K"%char => xO (xI (xI (xI (xO (xI p)))))
| "L"%char => xI (xI (xI (xI (xO (xI p)))))
| "M"%char => xO (xO (xO (xO (xI (xI p)))))
| "N"%char => xI (xO (xO (xO (xI (xI p)))))
| "O"%char => xO (xI (xO (xO (xI (xI p)))))
| "P"%char => xI (xI (xO (xO (xI (xI p)))))
| "Q"%char => xO (xO (xI (xO (xI (xI p)))))
| "R"%char => xI (xO (xI (xO (xI (xI p)))))
| "S"%char => xO (xI (xI (xO (xI (xI p)))))
| "T"%char => xI (xI (xI (xO (xI (xI p)))))
| "U"%char => xO (xO (xO (xI (xI (xI p)))))
| "V"%char => xI (xO (xO (xI (xI (xI p)))))
| "W"%char => xO (xI (xO (xI (xI (xI p)))))
| "X"%char => xI (xI (xO (xI (xI (xI p)))))
| "Y"%char => xO (xO (xI (xI (xI (xI p)))))
| "Z"%char => xI (xO (xI (xI (xI (xI p)))))
| "_"%char => xO (xI (xI (xI (xI (xI p)))))
| _ => append_char_pos_default c p
end.
Fixpoint ident_of_string (s: string) : ident :=
match s with
| EmptyString => xH
| String c s => append_char_pos c (ident_of_string s)
end.
(** A convenient notation [$ "ident"] to force evaluation of
[ident_of_string "ident"] *)
Ltac ident_of_string s :=
let x := constr:(ident_of_string s) in
let y := eval compute in x in
exact y.
Notation "$ s" := (ltac:(ident_of_string s))
(at level 1, only parsing) : string_scope.
|
