source: Deliverables/D2.2/8051/src/clight/clight.mli

Last change on this file was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

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