source: Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clight.mli @ 489

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

Pointer fixes for the temporary version of the compiler that can output matita
terms.

File size: 7.3 KB
Line 
1(** This module defines the abstract syntax tree of [Clight].
2
3    This is a (quasi-)direct translation of the Coq definition that
4    can be found in the CompCert development. *)
5
6open AST
7
8(** ** Types *)
9
10type memory_space = Any | Data | IData | PData | XData | Code
11
12(** Clight types are similar to those of C.  They include numeric types,
13  pointers, arrays, function types, and composite types (struct and
14  union).  Numeric types (integers and floats) fully specify the
15  bit size of the type.  An integer type is a pair of a signed/unsigned
16  flag and a bit size: 8, 16 or 32 bits. *)
17
18type signedness = Signed | Unsigned
19
20type intsize = I8 | I16 | I32
21
22(** Float types come in two sizes: 32 bits (single precision)
23  and 64-bit (double precision). *)
24
25type floatsize = F32 | F64
26
27(** The syntax of type expressions.  Some points to note:
28  - Array types [Tarray n] carry the size [n] of the array.
29  Arrays with unknown sizes are represented by pointer types.
30  - Function types [Tfunction targs tres] specify the number and types
31  of the function arguments (list [targs]), and the type of the
32  function result ([tres]).  Variadic functions and old-style unprototyped
33  functions are not supported.
34  - In C, struct and union types are named and compared by name.
35  This enables the definition of recursive struct types such as
36  {[
37  struct s1 { int n; struct * s1 next; };
38  ]}
39  Note that recursion within types must go through a pointer type.
40  For instance, the following is not allowed in C.
41  {[
42  struct s2 { int n; struct s2 next; };
43  ]}
44  In Clight, struct and union types [Tstruct id fields] and
45  [Tunion id fields] are compared by structure: the [fields]
46  argument gives the names and types of the members.  The AST_common.identifier
47  [id] is a local name which can be used in conjuction with the
48  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr id]
49  stands for a pointer type to the nearest enclosing [Tstruct]
50  or [Tunion] type named [id].  For instance. the structure [s1]
51  defined above in C is expressed by
52  {[
53  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
54  (Fcons "next" (Tcomp_ptr "s1")
55  Fnil))
56  ]}
57  Note that the incorrect structure [s2] above cannot be expressed at
58  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
59  structure or union, but not to the structure or union directly.
60  *)
61
62type ctype =
63  | Tvoid                                       (**r the [void] type *)
64  | Tint of intsize*signedness                  (**r integer types *)
65  | Tfloat of floatsize                         (**r floating-point types *)
66  | Tpointer of memory_space * ctype            (**r pointer types ([*ty]) *)
67  | Tarray of memory_space * ctype*int          (**r array types ([ty[len]]) *)
68  | Tfunction of ctype list*ctype               (**r function types *)
69  | Tstruct of ident*(ident*ctype) list
70  (**r struct types *)
71  | Tunion of ident*(ident*ctype) list
72  (**r union types *)
73  | Tcomp_ptr of memory_space * ident           (**r pointer to named struct or union *)
74
75(** ** Expressions *)
76
77(** Arithmetic and logical operators. *)
78
79type unary_operation =
80  | Onotbool    (**r boolean negation ([!] in C) *)
81  | Onotint     (**r integer complement ([~] in C) *)
82  | Oneg        (**r opposite (unary [-]) *)
83
84type binary_operation =
85  | Oadd        (**r addition (binary [+]) *)
86  | Osub        (**r subtraction (binary [-]) *)
87  | Omul        (**r multiplication (binary [*]) *)
88  | Odiv        (**r division ([/]) *)
89  | Omod        (**r remainder ([%]) *)
90  | Oand        (**r bitwise and ([&]) *)
91  | Oor         (**r bitwise or ([|]) *)
92  | Oxor        (**r bitwise xor ([^]) *)
93  | Oshl        (**r left shift ([<<]) *)
94  | Oshr        (**r right shift ([>>]) *)
95  | Oeq         (**r comparison ([==]) *)
96  | One         (**r comparison ([!=]) *)
97  | Olt         (**r comparison ([<]) *)
98  | Ogt         (**r comparison ([>]) *)
99  | Ole         (**r comparison ([<=]) *)
100  | Oge         (**r comparison ([>=]) *)
101
102(** Clight expressions are a large subset of those of C.
103  The main omissions are string literals and assignment operators
104  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
105  not an expression. 
106
107  All expressions are annotated with their types.  An expression
108  (type [expr]) is therefore a pair of a type and an expression
109  description (type [expr_descr]).
110  *)
111
112type expr =
113  | Expr of expr_descr*ctype
114
115                         and expr_descr =
116  | Econst_int of int                           (**r integer literal *)
117  | Econst_float of float                       (**r float literal *)
118  | Evar of ident                       (**r variable *)
119  | Ederef of expr                              (**r pointer dereference (unary [*]) *)
120  | Eaddrof of expr                             (**r address-of operator ([&]) *)
121  | Eunop of unary_operation*expr               (**r unary operation *)
122  | Ebinop of binary_operation*expr*expr        (**r binary operation *)
123  | Ecast of ctype*expr                         (**r type cast ([(ty) e]) *)
124  | Econdition of expr*expr*expr                (**r conditional ([e1 ? e2 : e3]) *)
125  | Eandbool of expr*expr                       (**r sequential and ([&&]) *)
126  | Eorbool of expr*expr                        (**r sequential or ([||]) *)
127  | Esizeof of ctype                            (**r size of a type *)
128  | Efield of expr*ident                (**r access to a member of a struct or union *)
129
130  (** The following constructors are used by the annotation process only. *)
131
132  | Ecost of CostLabel.t*expr                   (**r cost label. *)
133  | Ecall of ident * expr * expr
134
135
136(** ** Statements *)
137
138(** Clight statements include all C statements.
139  Only structured forms of [switch] are supported; moreover,
140  the [default] case must occur last.  Blocks and block-scoped declarations
141  are not supported. *)
142
143type label = Label.t
144
145type statement =
146  | Sskip                                       (**r do nothing *)
147  | Sassign of expr*expr                        (**r assignment [lvalue = rvalue] *)
148  | Scall of expr option*expr*expr list         (**r function call *)
149  | Ssequence of statement*statement            (**r sequence *)
150  | Sifthenelse of expr*statement*statement     (**r conditional *)
151  | Swhile of expr*statement            (**r [while] loop *)
152  | Sdowhile of expr*statement          (**r [do] loop *)
153  | Sfor of statement*expr*statement*statement  (**r [for] loop *)
154  | Sbreak                                      (**r [break] statement *)
155  | Scontinue                                   (**r [continue] statement *)
156  | Sreturn of expr option                      (**r [return] statement *)
157  | Sswitch of expr*labeled_statements          (**r [switch] statement *)
158  | Slabel of label*statement
159  | Sgoto of label
160  | Scost of CostLabel.t * statement
161
162               and labeled_statements =            (**r cases of a [switch] *)
163  | LSdefault of statement
164  | LScase of int*statement*labeled_statements
165
166(** ** Functions *)
167
168(** A function definition is composed of its return type ([fn_return]),
169  the names and types of its parameters ([fn_params]), the names
170  and types of its local variables ([fn_vars]), and the body of the
171  function (a statement, [fn_body]). *)
172
173type cfunction = {
174  fn_return : ctype ;
175  fn_params : (ident*ctype) list ;
176  fn_vars : (ident * ctype) list ;
177  fn_body : statement
178}
179
180(** Functions can either be defined ([Internal]) or declared as
181  external functions ([External]). *)
182
183type fundef =
184  | Internal of cfunction
185  | External of ident*ctype list*ctype
186
187(** ** Programs *)
188
189(** A program is a collection of named functions, plus a collection
190  of named global variables, carrying their types and optional initialization
191  data.  See module [AST] for more details. *)
192
193type init_data =
194  | Init_int8 of int
195  | Init_int16 of int
196  | Init_null of memory_space
197  | Init_int32 of int
198  | Init_float32 of float
199  | Init_float64 of float
200  | Init_space of int
201  | Init_addrof of memory_space*ident*int  (**r address of symbol + offset *)
202
203type program = {
204  prog_funct: (ident * fundef) list ;
205  prog_main: ident option;
206  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
207}
Note: See TracBrowser for help on using the repository browser.