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

Last change on this file since 459 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

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