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 }