Library compcert.cfrontend.Csyntax
Abstract syntax for the Compcert C language
Require Import Coqlib.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Ctypes.
Require Import Cop.
Expressions
Inductive expr : Type :=
| Eval (v: val) (ty: type)
| Evar (x: ident) (ty: type)
| Efield (l: expr) (f: ident) (ty: type)
| Evalof (l: expr) (ty: type)
| Ederef (r: expr) (ty: type)
| Eaddrof (l: expr) (ty: type)
| Eunop (op: unary_operation) (r: expr) (ty: type)
| Ebinop (op: binary_operation) (r1 r2: expr) (ty: type)
| Ecast (r: expr) (ty: type)
| Eseqand (r1 r2: expr) (ty: type)
| Eseqor (r1 r2: expr) (ty: type)
| Econdition (r1 r2 r3: expr) (ty: type)
| Esizeof (ty´: type) (ty: type)
| Ealignof (ty´: type) (ty: type)
| Eassign (l: expr) (r: expr) (ty: type)
| Eassignop (op: binary_operation) (l: expr) (r: expr) (tyres ty: type)
| Epostincr (id: incr_or_decr) (l: expr) (ty: type)
| Ecomma (r1 r2: expr) (ty: type)
| Ecall (r1: expr) (rargs: exprlist) (ty: type)
| Ebuiltin (ef: external_function) (tyargs: typelist) (rargs: exprlist) (ty: type)
| Eloc (b: block) (ofs: int) (ty: type)
| Eparen (r: expr) (ty: type)
with exprlist : Type :=
| Enil
| Econs (r1: expr) (rl: exprlist).
Expressions are implicitly classified into l-values and r-values,
ranged over by l and r, respectively, in the grammar above.
L-values are those expressions that can occur to the left of an assignment.
They denote memory locations. (Indeed, the reduction semantics for
expression reduces them to Eloc b ofs expressions.) L-values are
variables (Evar), pointer dereferences (Ederef), field accesses (Efield).
R-values are all other expressions. They denote values, and the reduction
semantics reduces them to Eval v expressions.
A l-value can be used in a r-value context, but this use must be marked
explicitly with the Evalof operator, which is not materialized in the
concrete syntax of C but denotes a read from the location corresponding to
the l-value l argument of Evalof l.
The grammar above contains some forms that cannot appear in source terms
but appear during reduction. These forms are:
- Eval v where v is a pointer or Vundef. (Eval of an integer or float value can occur in a source term and represents a numeric literal.)
- Eloc b ofs, which appears during reduction of l-values.
- Eparen r, which appears during reduction of conditionals r1 ? r2 : r3.
Pre-increment ++l and pre-decrement --l are expressed as
l += 1 and l -= 1, respectively.
Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) :=
Eassignop (match id with Incr => Oadd | Decr => Osub end)
l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty.
Extract the type part of a type-annotated expression.
Definition typeof (a: expr) : type :=
match a with
| Eloc _ _ ty => ty
| Evar _ ty => ty
| Ederef _ ty => ty
| Efield _ _ ty => ty
| Eval _ ty => ty
| Evalof _ ty => ty
| Eaddrof _ ty => ty
| Eunop _ _ ty => ty
| Ebinop _ _ _ ty => ty
| Ecast _ ty => ty
| Econdition _ _ _ ty => ty
| Eseqand _ _ ty => ty
| Eseqor _ _ ty => ty
| Esizeof _ ty => ty
| Ealignof _ ty => ty
| Eassign _ _ ty => ty
| Eassignop _ _ _ _ ty => ty
| Epostincr _ _ ty => ty
| Ecomma _ _ ty => ty
| Ecall _ _ ty => ty
| Ebuiltin _ _ _ ty => ty
| Eparen _ ty => ty
end.
Statements
- empty statement Sskip
- evaluation of an expression for its side-effects Sdo r
- conditional if (...) { ... } else { ... }
- the three loops while(...) { ... } and do { ... } while (...) and for(..., ..., ...) { ... }
- the switch construct
- break, continue, return (with and without argument)
- goto and labeled statements.
Definition label := ident.
Inductive statement : Type :=
| Sskip : statement
| Sdo : expr -> statement
| Ssequence : statement -> statement -> statement
| Sifthenelse : expr -> statement -> statement -> statement
| Swhile : expr -> statement -> statement
| Sdowhile : expr -> statement -> statement
| Sfor: statement -> expr -> statement -> statement -> statement
| Sbreak : statement
| Scontinue : statement
| Sreturn : option expr -> statement
| Sswitch : expr -> labeled_statements -> statement
| Slabel : label -> statement -> statement
| Sgoto : label -> statement
with labeled_statements : Type :=
| LSnil: labeled_statements
| LScons: option int -> statement -> labeled_statements -> labeled_statements.
Functions
Record function : Type := mkfunction {
fn_return: type;
fn_callconv: calling_convention;
fn_params: list (ident * type);
fn_vars: list (ident * type);
fn_body: statement
}.
Definition var_names (vars: list(ident * type)) : list ident :=
List.map (@fst ident type) vars.
Functions can either be defined (Internal) or declared as
external functions (External).
Inductive fundef : Type :=
| Internal: function -> fundef
| External: external_function -> typelist -> type -> calling_convention -> fundef.
The type of a function definition.
Definition type_of_function (f: function) : type :=
Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f).
Definition type_of_fundef (f: fundef) : type :=
match f with
| Internal fd => type_of_function fd
| External id args res cc => Tfunction args res cc
end.