Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Ctypes.
Require Import Cop.
Require Import CopSyntax.
Abstract syntax
Expressions
Clight expressions correspond to the "pure" subset of C expressions.
The main omissions are string literals and assignment operators
(=, +=, ++, etc). In Clight, assignment is a statement,
not an expression. Additionally, an expression can also refer to
temporary variables, which are a separate class of local variables
that do not reside in memory and whose address cannot be taken.
As in Compcert C, all expressions are annotated with their types,
as needed to resolve operator overloading and type-dependent behaviors.
Inductive expr :
Type :=
|
Econst_int:
int ->
type ->
expr (* integer literal *)
|
Econst_float:
float ->
type ->
expr (* double float literal *)
|
Econst_single:
float32 ->
type ->
expr (* single float literal *)
|
Econst_long:
int64 ->
type ->
expr (* long integer literal *)
|
Evar:
ident ->
type ->
expr (* variable *)
|
Etempvar:
ident ->
type ->
expr (* temporary variable *)
|
Ederef:
expr ->
type ->
expr (* pointer dereference (unary *) *)
|
Eaddrof:
expr ->
type ->
expr (* address-of operator (&) *)
|
Eunop:
unary_operation ->
expr ->
type ->
expr (* unary operation *)
|
Ebinop:
binary_operation ->
expr ->
expr ->
type ->
expr (* binary operation *)
|
Ecast:
expr ->
type ->
expr (* type cast ((ty) e) *)
|
Efield:
expr ->
ident ->
type ->
expr.
(* access to a member of a struct or union *)
sizeof and alignof are derived forms.
Definition Esizeof (
ty'
ty:
type) :
expr :=
Econst_int (
Int.repr(
sizeof ty'))
ty.
Definition Ealignof (
ty'
ty:
type) :
expr :=
Econst_int (
Int.repr(
alignof ty'))
ty.
Extract the type part of a type-annotated Clight expression.
Definition typeof (
e:
expr) :
type :=
match e with
|
Econst_int _ ty =>
ty
|
Econst_float _ ty =>
ty
|
Econst_single _ ty =>
ty
|
Econst_long _ ty =>
ty
|
Evar _ ty =>
ty
|
Etempvar _ ty =>
ty
|
Ederef _ ty =>
ty
|
Eaddrof _ ty =>
ty
|
Eunop _ _ ty =>
ty
|
Ebinop _ _ _ ty =>
ty
|
Ecast _ ty =>
ty
|
Efield _ _ ty =>
ty
end.
Statements
Clight statements are similar to those of Compcert C, with the addition
of assigment (of a rvalue to a lvalue), assignment to a temporary,
and function call (with assignment of the result to a temporary).
The three C loops are replaced by a single infinite loop Sloop s1
s2 that executes s1 then s2 repeatedly. A continue in s1
branches to s2.
Definition label :=
ident.
Inductive statement :
Type :=
|
Sskip :
statement (* do nothing *)
|
Sassign :
expr ->
expr ->
statement (* assignment lvalue = rvalue *)
|
Sset :
ident ->
expr ->
statement (* assignment tempvar = rvalue *)
|
Scall:
option ident ->
expr ->
list expr ->
statement (* function call *)
|
Sbuiltin:
option ident ->
external_function ->
typelist ->
list expr ->
statement (* builtin invocation *)
|
Ssequence :
statement ->
statement ->
statement (* sequence *)
|
Sifthenelse :
expr ->
statement ->
statement ->
statement (* conditional *)
|
Sloop:
statement ->
statement ->
statement (* infinite 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 *)
|
LSnil:
labeled_statements
|
LScons:
option Z ->
statement ->
labeled_statements ->
labeled_statements.
The C loops are derived forms.
Definition Swhile (
e:
expr) (
s:
statement) :=
Sloop (
Ssequence (
Sifthenelse e Sskip Sbreak)
s)
Sskip.
Definition Sdowhile (
s:
statement) (
e:
expr) :=
Sloop s (
Sifthenelse e Sskip Sbreak).
Definition Sfor (
s1:
statement) (
e2:
expr) (
s3:
statement) (
s4:
statement) :=
Ssequence s1 (
Sloop (
Ssequence (
Sifthenelse e2 Sskip Sbreak)
s3)
s4).