]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/clight/clight.mli
Package description and copyright added.
[pkg-cerco/acc.git] / src / clight / clight.mli
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
6 open AST
7
8 (** ** Types *)
9
10 type intsize = I8 | I16 | I32
11
12 type 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
49 type 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
66 type unary_operation =
67   | Onotbool    (**r boolean negation ([!] in C) *)
68   | Onotint     (**r integer complement ([~] in C) *)
69   | Oneg        (**r opposite (unary [-]) *)
70
71 type 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
99 type 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
130 type label = Label.t
131
132 type statement =
133   | Sskip                                       (**r do nothing *)
134   | Sassign of expr*expr                        (**r assignment [lvalue = rvalue] *)
135   | Scall of expr option*expr*expr list         (**r function call *)
136   | Ssequence of statement*statement            (**r sequence *)
137   | Sifthenelse of expr*statement*statement     (**r conditional *)
138   | Swhile of expr*statement                    (**r [while] loop *)
139   | Sdowhile of expr*statement                  (**r [do] loop *)
140   | Sfor of statement*expr*statement*statement  (**r [for] loop *)
141   | Sbreak                                      (**r [break] statement *)
142   | Scontinue                                   (**r [continue] statement *)
143   | Sreturn of expr option                      (**r [return] statement *)
144   | Sswitch of expr*labeled_statements          (**r [switch] statement *)
145   | Slabel of label*statement
146   | Sgoto of label
147   | Scost of CostLabel.t * statement
148
149 and labeled_statements =                        (**r cases of a [switch] *)
150   | LSdefault of statement
151   | LScase of int*statement*labeled_statements
152
153 (** ** Functions *)
154
155 (** A function definition is composed of its return type ([fn_return]),
156   the names and types of its parameters ([fn_params]), the names
157   and types of its local variables ([fn_vars]), and the body of the
158   function (a statement, [fn_body]). *)
159
160 type cfunction = {
161   fn_return : ctype ;
162   fn_params : (ident*ctype) list ;
163   fn_vars : (ident * ctype) list ;
164   fn_body : statement
165 }
166
167 (** Functions can either be defined ([Internal]) or declared as
168   external functions ([External]). *)
169
170 type fundef =
171   | Internal of cfunction
172   | External of ident*ctype list*ctype
173
174 (** ** Programs *)
175
176 (** A program is a collection of named functions, plus a collection
177   of named global variables, carrying their types and optional initialization 
178   data.  See module [AST] for more details. *)
179
180 type init_data =
181   | Init_int8 of int
182   | Init_int16 of int
183   | Init_int32 of int
184   | Init_float32 of float
185   | Init_float64 of float
186   | Init_space of int
187   | Init_addrof of ident*int  (**r address of symbol + offset *)
188
189 type program = {
190   prog_funct: (ident * fundef) list ;
191   prog_main: ident option;
192   prog_vars: ((ident * init_data list) * ctype) list
193 }