Library Csyntax
Abstract syntax for the Clight language
Require Import Coqlib.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import AST.
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.
Inductive signedness : Type :=
| Signed: signedness
| Unsigned: signedness.
Inductive intsize : Type :=
| I8: intsize
| I16: intsize
| I32: intsize.
Float types come in two sizes: 32 bits (single precision)
and 64-bit (double precision).
Inductive floatsize : Type :=
| F32: floatsize
| F64: floatsize.
The syntax of type expressions. Some points to note:
Note that recursion within types must go through a pointer type. For instance, the following is not allowed in C.
In Clight, struct and union types
Note that the incorrect structure
- Array types
Tarray n
carry the sizen
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 (listtargs
), 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 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 "id") 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.
Inductive type : Type :=
| Tvoid: type
the void
type
| Tint: intsize -> signedness -> type
integer types
| Tfloat: floatsize -> type
floating-point types
| Tpointer: type -> type
pointer types (*ty
)
| Tarray: type -> Z -> type
array types (ty[len]
)
| Tfunction: typelist -> type -> type
function types
| Tstruct: ident -> fieldlist -> type
struct types
| Tunion: ident -> fieldlist -> type
union types
| Tcomp_ptr: ident -> type
pointer to named struct or union
with typelist : Type :=
| Tnil: typelist
| Tcons: type -> typelist -> typelist
with fieldlist : Type :=
| Fnil: fieldlist
| Fcons: ident -> type -> fieldlist -> fieldlist.
Arithmetic and logical operators.
Inductive unary_operation : Type :=
| Onotbool : unary_operation
boolean negation (!
in C)
| Onotint : unary_operation
integer complement (~
in C)
| Oneg : unary_operation.
opposite (unary -
)
Inductive binary_operation : Type :=
| Oadd : binary_operation
addition (binary +
)
| Osub : binary_operation
subtraction (binary -
)
| Omul : binary_operation
multiplication (binary *
)
| Odiv : binary_operation
division (/
)
| Omod : binary_operation
remainder (%
)
| Oand : binary_operation
bitwise and (&
)
| Oor : binary_operation
bitwise or (|
)
| Oxor : binary_operation
bitwise xor (^
)
| Oshl : binary_operation
left shift (<<
)
| Oshr : binary_operation
right shift (>>
)
| Oeq: binary_operation
comparison (==
)
| One: binary_operation
comparison (!=
)
| Olt: binary_operation
comparison (<
)
| Ogt: binary_operation
comparison (>
)
| Ole: binary_operation
comparison (<=
)
| Oge: binary_operation.
comparison (>=
)
Clight expressions are a large subset of those of C.
The main omissions are string literals and assignment operators
(
All expressions are annotated with their types. An expression (type
=
, +=
, ++
, 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
).
Inductive expr : Type :=
| Expr: expr_descr -> type -> expr
with expr_descr : Type :=
| Econst_int: int -> expr_descr
integer literal
| Econst_float: float -> expr_descr
float literal
| Evar: ident -> expr_descr
variable
| Ederef: expr -> expr_descr
pointer dereference (unary *
)
| Eaddrof: expr -> expr_descr
address-of operator (&
)
| Eunop: unary_operation -> expr -> expr_descr
unary operation
| Ebinop: binary_operation -> expr -> expr -> expr_descr
binary operation
| Ecast: type -> expr -> expr_descr
type cast ((ty) e
)
| Econdition: expr -> expr -> expr -> expr_descr
conditional (e1 ? e2 : e3
)
| Eandbool: expr -> expr -> expr_descr
sequential and (&&
)
| Eorbool: expr -> expr -> expr_descr
sequential or (||
)
| Esizeof: type -> expr_descr
size of a type
| Efield: expr -> ident -> expr_descr.
access to a member of a struct or union
Extract the type part of a type-annotated Clight expression.
Definition typeof (e: expr) : type :=
match e with Expr de te => te end.
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.
Definition label := ident.
Inductive statement : Type :=
| Sskip : statement
do nothing
| Sassign : expr -> expr -> statement
assignment lvalue = rvalue
| Scall: option expr -> expr -> list expr -> statement
function call
| Ssequence : statement -> statement -> statement
sequence
| Sifthenelse : expr -> statement -> statement -> statement
conditional
| Swhile : expr -> statement -> statement
while
loop
| Sdowhile : expr -> statement -> statement
do
loop
| Sfor: statement -> expr -> statement -> statement -> statement
for
loop
| Sbreak : statement
break
statement
| Scontinue : statement
continue
statement
| Sreturn : option expr -> statement
return
statement
| Sswitch : expr -> labeled_statements -> statement
switch
statement
| Slabel : label -> statement -> statement
| Sgoto : label -> statement
with labeled_statements : Type :=
cases of a switch
| LSdefault: statement -> labeled_statements
| LScase: int -> statement -> labeled_statements -> labeled_statements.
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
).
Record function : Type := mkfunction {
fn_return: type;
fn_params: list (ident * type);
fn_vars: list (ident * type);
fn_body: statement
}.
Functions can either be defined (
Internal
) or declared as
external functions (External
).
Inductive fundef : Type :=
| Internal: function -> fundef
| External: ident -> typelist -> type -> fundef.
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.
Definition program : Type := AST.program fundef type.
The type of a function definition.
Fixpoint type_of_params (params: list (ident * type)) : typelist :=
match params with
| nil => Tnil
| (id, ty) :: rem => Tcons ty (type_of_params rem)
end.
Definition type_of_function (f: function) : type :=
Tfunction (type_of_params (fn_params f)) (fn_return f).
Definition type_of_fundef (f: fundef) : type :=
match f with
| Internal fd => type_of_function fd
| External id args res => Tfunction args res
end.
Natural alignment of a type, in bytes.
Fixpoint alignof (t: type) : Z :=
match t with
| Tvoid => 1
| Tint I8 _ => 1
| Tint I16 _ => 2
| Tint I32 _ => 4
| Tfloat F32 => 4
| Tfloat F64 => 8
| Tpointer _ => 4
| Tarray t' n => alignof t'
| Tfunction _ _ => 1
| Tstruct _ fld => alignof_fields fld
| Tunion _ fld => alignof_fields fld
| Tcomp_ptr _ => 4
end
with alignof_fields (f: fieldlist) : Z :=
match f with
| Fnil => 1
| Fcons id t f' => Zmax (alignof t) (alignof_fields f')
end.
Scheme type_ind2 := Induction for type Sort Prop
with fieldlist_ind2 := Induction for fieldlist Sort Prop.
Lemma alignof_fields_pos:
forall f, alignof_fields f > 0.
Lemma alignof_pos:
forall t, alignof t > 0.
Size of a type, in bytes.
Fixpoint sizeof (t: type) : Z :=
match t with
| Tvoid => 1
| Tint I8 _ => 1
| Tint I16 _ => 2
| Tint I32 _ => 4
| Tfloat F32 => 4
| Tfloat F64 => 8
| Tpointer _ => 4
| Tarray t' n => sizeof t' * Zmax 1 n
| Tfunction _ _ => 1
| Tstruct _ fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
| Tunion _ fld => align (Zmax 1 (sizeof_union fld)) (alignof t)
| Tcomp_ptr _ => 4
end
with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
match fld with
| Fnil => pos
| Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t)
end
with sizeof_union (fld: fieldlist) : Z :=
match fld with
| Fnil => 0
| Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld')
end.
Lemma sizeof_pos:
forall t, sizeof t > 0.
Lemma sizeof_struct_incr:
forall fld pos, pos <= sizeof_struct fld pos.
Byte offset for a field in a struct or union.
Field are laid out consecutively, and padding is inserted
to align each field to the natural alignment for its type.
Open Local Scope string_scope.
Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
{struct fld} : res Z :=
match fld with
| Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
| Fcons id' t fld' =>
if ident_eq id id'
then OK (align pos (alignof t))
else field_offset_rec id fld' (align pos (alignof t) + sizeof t)
end.
Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
field_offset_rec id fld 0.
Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type :=
match fld with
| Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
| Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld'
end.
Some sanity checks about field offsets. First, field offsets are
within the range of acceptable offsets.
Remark field_offset_rec_in_range:
forall id ofs ty fld pos,
field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
Lemma field_offset_in_range:
forall id fld ofs ty,
field_offset id fld = OK ofs -> field_type id fld = OK ty ->
0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
Second, two distinct fields do not overlap
Lemma field_offset_no_overlap:
forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
id1 <> id2 ->
ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
Third, if a struct is a prefix of another, the offsets of fields
in common is the same.
Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
match fld1 with
| Fnil => fld2
| Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2)
end.
Lemma field_offset_prefix:
forall id ofs fld2 fld1,
field_offset id fld1 = OK ofs ->
field_offset id (fieldlist_app fld1 fld2) = OK ofs.
The
We currently do not support 64-bit integers and 128-bit floats, so these have an access mode of
access_mode
function describes how a variable of the given
type must be accessed:
-
By_value ch
: access by value, i.e. by loading from the address of the variable using the memory chunkch
; -
By_reference
: access by reference, i.e. by just returning the address of the variable; -
By_nothing
: no access is possible, e.g. for thevoid
type.
We currently do not support 64-bit integers and 128-bit floats, so these have an access mode of
By_nothing
.
Inductive mode: Type :=
| By_value: memory_chunk -> mode
| By_reference: mode
| By_nothing: mode.
Definition access_mode (ty: type) : mode :=
match ty with
| Tint I8 Signed => By_value Mint8signed
| Tint I8 Unsigned => By_value Mint8unsigned
| Tint I16 Signed => By_value Mint16signed
| Tint I16 Unsigned => By_value Mint16unsigned
| Tint I32 _ => By_value Mint32
| Tfloat F32 => By_value Mfloat32
| Tfloat F64 => By_value Mfloat64
| Tvoid => By_nothing
| Tpointer _ => By_value Mint32
| Tarray _ _ => By_reference
| Tfunction _ _ => By_reference
| Tstruct _ fList => By_nothing
| Tunion _ fList => By_nothing
| Tcomp_ptr _ => By_value Mint32
end.
Classification of arithmetic operations and comparisons.
The following
classify_
functions take as arguments the types
of the arguments of an operation. They return enough information
to resolve overloading for this operator applications, such as
``both arguments are floats'', or ``the first is a pointer
and the second is an integer''. These functions are used to resolve
overloading both in the dynamic semantics (module Csem
) and in the
compiler (module Cshmgen
).
Inductive classify_add_cases : Type :=
| add_case_ii: classify_add_cases
int , int
| add_case_ff: classify_add_cases
float , float
| add_case_pi: type -> classify_add_cases
ptr or array, int
| add_case_ip: type -> classify_add_cases
int, ptr or array
| add_default: classify_add_cases.
other
Definition classify_add (ty1: type) (ty2: type) :=
match ty1, ty2 with
| Tint _ _, Tint _ _ => add_case_ii
| Tfloat _, Tfloat _ => add_case_ff
| Tpointer ty, Tint _ _ => add_case_pi ty
| Tarray ty _, Tint _ _ => add_case_pi ty
| Tint _ _, Tpointer ty => add_case_ip ty
| Tint _ _, Tarray ty _ => add_case_ip ty
| _, _ => add_default
end.
Inductive classify_sub_cases : Type :=
| sub_case_ii: classify_sub_cases
int , int
| sub_case_ff: classify_sub_cases
float , float
| sub_case_pi: type -> classify_sub_cases
ptr or array , int
| sub_case_pp: type -> classify_sub_cases
ptr or array , ptr or array
| sub_default: classify_sub_cases .
other
Definition classify_sub (ty1: type) (ty2: type) :=
match ty1, ty2 with
| Tint _ _ , Tint _ _ => sub_case_ii
| Tfloat _ , Tfloat _ => sub_case_ff
| Tpointer ty , Tint _ _ => sub_case_pi ty
| Tarray ty _ , Tint _ _ => sub_case_pi ty
| Tpointer ty , Tpointer _ => sub_case_pp ty
| Tpointer ty , Tarray _ _=> sub_case_pp ty
| Tarray ty _ , Tpointer _ => sub_case_pp ty
| Tarray ty _ , Tarray _ _ => sub_case_pp ty
| _ ,_ => sub_default
end.
Inductive classify_mul_cases : Type:=
| mul_case_ii: classify_mul_cases
int , int
| mul_case_ff: classify_mul_cases
float , float
| mul_default: classify_mul_cases .
other
Definition classify_mul (ty1: type) (ty2: type) :=
match ty1,ty2 with
| Tint _ _, Tint _ _ => mul_case_ii
| Tfloat _ , Tfloat _ => mul_case_ff
| _,_ => mul_default
end.
Inductive classify_div_cases : Type:=
| div_case_I32unsi: classify_div_cases
unsigned int32 , int
| div_case_ii: classify_div_cases
int , int
| div_case_ff: classify_div_cases
float , float
| div_default: classify_div_cases.
other
Definition classify_div (ty1: type) (ty2: type) :=
match ty1,ty2 with
| Tint I32 Unsigned, Tint _ _ => div_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => div_case_I32unsi
| Tint _ _ , Tint _ _ => div_case_ii
| Tfloat _ , Tfloat _ => div_case_ff
| _ ,_ => div_default
end.
Inductive classify_mod_cases : Type:=
| mod_case_I32unsi: classify_mod_cases
unsigned I32 , int
| mod_case_ii: classify_mod_cases
int , int
| mod_default: classify_mod_cases .
other
Definition classify_mod (ty1: type) (ty2: type) :=
match ty1,ty2 with
| Tint I32 Unsigned , Tint _ _ => mod_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => mod_case_I32unsi
| Tint _ _ , Tint _ _ => mod_case_ii
| _ , _ => mod_default
end .
Inductive classify_shr_cases :Type:=
| shr_case_I32unsi: classify_shr_cases
unsigned I32 , int
| shr_case_ii :classify_shr_cases
int , int
| shr_default : classify_shr_cases .
other
Definition classify_shr (ty1: type) (ty2: type) :=
match ty1,ty2 with
| Tint I32 Unsigned , Tint _ _ => shr_case_I32unsi
| Tint _ _ , Tint _ _ => shr_case_ii
| _ , _ => shr_default
end.
Inductive classify_cmp_cases : Type:=
| cmp_case_I32unsi: classify_cmp_cases
unsigned I32 , int
| cmp_case_ipip: classify_cmp_cases
int|ptr|array , int|ptr|array
| cmp_case_ff: classify_cmp_cases
float , float
| cmp_default: classify_cmp_cases .
other
Definition classify_cmp (ty1: type) (ty2: type) :=
match ty1,ty2 with
| Tint I32 Unsigned , Tint _ _ => cmp_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => cmp_case_I32unsi
| Tint _ _ , Tint _ _ => cmp_case_ipip
| Tfloat _ , Tfloat _ => cmp_case_ff
| Tpointer _ , Tint _ _ => cmp_case_ipip
| Tarray _ _ , Tint _ _ => cmp_case_ipip
| Tpointer _ , Tpointer _ => cmp_case_ipip
| Tpointer _ , Tarray _ _ => cmp_case_ipip
| Tarray _ _ ,Tpointer _ => cmp_case_ipip
| Tarray _ _ ,Tarray _ _ => cmp_case_ipip
| _ , _ => cmp_default
end.
Inductive classify_fun_cases : Type:=
| fun_case_f: typelist -> type -> classify_fun_cases
(pointer to) function
| fun_default: classify_fun_cases .
other
Definition classify_fun (ty: type) :=
match ty with
| Tfunction args res => fun_case_f args res
| Tpointer (Tfunction args res) => fun_case_f args res
| _ => fun_default
end.
Translating Clight types to Cminor types, function signatures,
and external functions.
Definition typ_of_type (t: type) : AST.typ :=
match t with
| Tfloat _ => AST.Tfloat
| _ => AST.Tint
end.
Definition opttyp_of_type (t: type) : option AST.typ :=
match t with
| Tvoid => None
| Tfloat _ => Some AST.Tfloat
| _ => Some AST.Tint
end.
Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
match tl with
| Tnil => nil
| Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl
end.
Definition signature_of_type (args: typelist) (res: type) : signature :=
mksignature (typlist_of_typelist args) (opttyp_of_type res).
Definition external_function
(id: ident) (targs: typelist) (tres: type) : AST.external_function :=
mkextfun id (signature_of_type targs tres).