(** This module defines the abstract syntax tree of [Clight].
This is a (quasi-)direct translation of the Coq definition that
can be found in the CompCert development. *)
open AST
(** ** Types *)
type memory_space = Any | Data | IData | PData | XData | Code
(** Clight types are similar to those of C. They include numeric types,
pointers, arrays, function types, and composite types (struct and
union). Numeric types (integers and floats) fully specify the
bit size of the type. An integer type is a pair of a signed/unsigned
flag and a bit size: 8, 16 or 32 bits. *)
type signedness = Signed | Unsigned
type intsize = I8 | I16 | I32
(** Float types come in two sizes: 32 bits (single precision)
and 64-bit (double precision). *)
type floatsize = F32 | F64
(** The syntax of type expressions. Some points to note:
- Array types [Tarray n] carry the size [n] of the array.
Arrays with unknown sizes are represented by pointer types.
- Function types [Tfunction targs tres] specify the number and types
of the function arguments (list [targs]), and the type of the
function result ([tres]). Variadic functions and old-style unprototyped
functions are not supported.
- In C, struct and union types are named and compared by name.
This enables the definition of recursive struct types such as
{[
struct s1 { int n; struct * s1 next; };
]}
Note that recursion within types must go through a pointer type.
For instance, the following is not allowed in C.
{[
struct s2 { int n; struct s2 next; };
]}
In Clight, struct and union types [Tstruct id fields] and
[Tunion id fields] are compared by structure: the [fields]
argument gives the names and types of the members. The AST_common.identifier
[id] is a local name which can be used in conjuction with the
[Tcomp_ptr] constructor to express recursive types. [Tcomp_ptr id]
stands for a pointer type to the nearest enclosing [Tstruct]
or [Tunion] type named [id]. For instance. the structure [s1]
defined above in C is expressed by
{[
Tstruct "s1" (Fcons "n" (Tint I32 Signed)
(Fcons "next" (Tcomp_ptr "s1")
Fnil))
]}
Note that the incorrect structure [s2] above cannot be expressed at
all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
structure or union, but not to the structure or union directly.
*)
type ctype =
| Tvoid (**r the [void] type *)
| Tint of intsize*signedness (**r integer types *)
| Tfloat of floatsize (**r floating-point types *)
| Tpointer of memory_space * ctype (**r pointer types ([*ty]) *)
| Tarray of memory_space * ctype*int (**r array types ([ty[len]]) *)
| Tfunction of ctype list*ctype (**r function types *)
| Tstruct of ident*(ident*ctype) list
(**r struct types *)
| Tunion of ident*(ident*ctype) list
(**r union types *)
| Tcomp_ptr of ident (**r pointer to named struct or union *)
(** ** Expressions *)
(** Arithmetic and logical operators. *)
type unary_operation =
| Onotbool (**r boolean negation ([!] in C) *)
| Onotint (**r integer complement ([~] in C) *)
| Oneg (**r opposite (unary [-]) *)
type binary_operation =
| Oadd (**r addition (binary [+]) *)
| Osub (**r subtraction (binary [-]) *)
| Omul (**r multiplication (binary [*]) *)
| Odiv (**r division ([/]) *)
| Omod (**r remainder ([%]) *)
| Oand (**r bitwise and ([&]) *)
| Oor (**r bitwise or ([|]) *)
| Oxor (**r bitwise xor ([^]) *)
| Oshl (**r left shift ([<<]) *)
| Oshr (**r right shift ([>>]) *)
| Oeq (**r comparison ([==]) *)
| One (**r comparison ([!=]) *)
| Olt (**r comparison ([<]) *)
| Ogt (**r comparison ([>]) *)
| Ole (**r comparison ([<=]) *)
| Oge (**r comparison ([>=]) *)
(** Clight expressions are a large subset of those of C.
The main omissions are string literals and assignment operators
([=], [+=], [++], etc). In Clight, assignment is a statement,
not an expression.
All expressions are annotated with their types. An expression
(type [expr]) is therefore a pair of a type and an expression
description (type [expr_descr]).
*)
type expr =
| Expr of expr_descr*ctype
and expr_descr =
| Econst_int of int (**r integer literal *)
| Econst_float of float (**r float literal *)
| Evar of ident (**r variable *)
| Ederef of expr (**r pointer dereference (unary [*]) *)
| Eaddrof of expr (**r address-of operator ([&]) *)
| Eunop of unary_operation*expr (**r unary operation *)
| Ebinop of binary_operation*expr*expr (**r binary operation *)
| Ecast of ctype*expr (**r type cast ([(ty) e]) *)
| Econdition of expr*expr*expr (**r conditional ([e1 ? e2 : e3]) *)
| Eandbool of expr*expr (**r sequential and ([&&]) *)
| Eorbool of expr*expr (**r sequential or ([||]) *)
| Esizeof of ctype (**r size of a type *)
| Efield of expr*ident (**r access to a member of a struct or union *)
(** The following constructors are used by the annotation process only. *)
| Ecost of CostLabel.t*expr (**r cost label. *)
| Ecall of ident * expr * expr
(** ** Statements *)
(** Clight statements include all C statements.
Only structured forms of [switch] are supported; moreover,
the [default] case must occur last. Blocks and block-scoped declarations
are not supported. *)
type label = Label.t
type statement =
| Sskip (**r do nothing *)
| Sassign of expr*expr (**r assignment [lvalue = rvalue] *)
| Scall of expr option*expr*expr list (**r function call *)
| Ssequence of statement*statement (**r sequence *)
| Sifthenelse of expr*statement*statement (**r conditional *)
| Swhile of expr*statement (**r [while] loop *)
| Sdowhile of expr*statement (**r [do] loop *)
| Sfor of statement*expr*statement*statement (**r [for] loop *)
| Sbreak (**r [break] statement *)
| Scontinue (**r [continue] statement *)
| Sreturn of expr option (**r [return] statement *)
| Sswitch of expr*labeled_statements (**r [switch] statement *)
| Slabel of label*statement
| Sgoto of label
| Scost of CostLabel.t * statement
and labeled_statements = (**r cases of a [switch] *)
| LSdefault of statement
| LScase of int*statement*labeled_statements
(** ** Functions *)
(** A function definition is composed of its return type ([fn_return]),
the names and types of its parameters ([fn_params]), the names
and types of its local variables ([fn_vars]), and the body of the
function (a statement, [fn_body]). *)
type cfunction = {
fn_return : ctype ;
fn_params : (ident*ctype) list ;
fn_vars : (ident * ctype) list ;
fn_body : statement
}
(** Functions can either be defined ([Internal]) or declared as
external functions ([External]). *)
type fundef =
| Internal of cfunction
| External of ident*ctype list*ctype
(** ** Programs *)
(** A program is a collection of named functions, plus a collection
of named global variables, carrying their types and optional initialization
data. See module [AST] for more details. *)
type init_data =
| Init_int8 of int
| Init_int16 of int
| Init_int32 of int
| Init_float32 of float
| Init_float64 of float
| Init_space of int
| Init_addrof of ident*int (**r address of symbol + offset *)
type program = {
prog_funct: (ident * fundef) list ;
prog_main: ident option;
prog_vars: (((ident * init_data list) * memory_space) * ctype) list
}