From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 456 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 456 insertions(+) create mode 100644 cfrontend/Csyntax.v (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v new file mode 100644 index 00000000..d3bd8d6f --- /dev/null +++ b/cfrontend/Csyntax.v @@ -0,0 +1,456 @@ +(** * Abstract syntax for the Clight language *) + +Require Import Coqlib. +Require Import Integers. +Require Import Floats. +Require Import AST. + +(** ** Abstract syntax *) + +(** Types *) + +Inductive signedness : Set := + | Signed: signedness + | Unsigned: signedness. + +Inductive intsize : Set := + | I8: intsize + | I16: intsize + | I32: intsize. + +Inductive floatsize : Set := + | F32: floatsize + | F64: floatsize. + +Inductive type : Set := + | Tvoid: type + | Tint: intsize -> signedness -> type + | Tfloat: floatsize -> type + | Tpointer: type -> type + | Tarray: type -> Z -> type + | Tfunction: typelist -> type -> type + | Tstruct: fieldlist -> type + | Tunion: fieldlist -> type + +with typelist : Set := + | Tnil: typelist + | Tcons: type -> typelist -> typelist + +with fieldlist : Set := + | Fnil: fieldlist + | Fcons: ident -> type -> fieldlist -> fieldlist. + +(** Arithmetic and logical operators *) + +Inductive unary_operation : Set := + | Onotbool : unary_operation + | Onotint : unary_operation + | Oneg : unary_operation. + +Inductive binary_operation : Set := + | Oadd : binary_operation + | Osub : binary_operation + | Omul : binary_operation + | Odiv : binary_operation + | Omod : binary_operation + | Oand : binary_operation + | Oor : binary_operation + | Oxor : binary_operation + | Oshl : binary_operation + | Oshr : binary_operation + | Oeq: binary_operation + | One: binary_operation + | Olt: binary_operation + | Ogt: binary_operation + | Ole: binary_operation + | Oge: binary_operation. + +(** Expressions *) + +Inductive expr : Set := + | Expr: expr_descr -> type -> expr + +with expr_descr : Set := + | Econst_int: int -> expr_descr + | Econst_float: float -> expr_descr + | Evar: ident -> expr_descr + | Ederef: expr -> expr_descr + | Eaddrof: expr -> expr_descr + | Eunop: unary_operation -> expr -> expr_descr + | Ebinop: binary_operation -> expr -> expr -> expr_descr + | Ecast: type -> expr -> expr_descr + | Eindex: expr -> expr -> expr_descr + | Ecall: expr -> exprlist -> expr_descr + | Eandbool: expr -> expr -> expr_descr + | Eorbool: expr -> expr -> expr_descr + | Esizeof: type -> expr_descr + | Efield: expr -> ident -> expr_descr + +with exprlist : Set := + | Enil: exprlist + | Econs: expr -> exprlist -> exprlist. + +(** Extract the type part of a type-annotated Clight expression. *) + +Definition typeof (e: expr) : type := + match e with Expr de te => te end. + +(** Statements *) + +Inductive statement : Set := + | Sskip : statement + | Sexpr : expr -> statement + | Sassign : expr -> 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 + +with labeled_statements : Set := + | LSdefault: statement -> labeled_statements + | LScase: int -> statement -> labeled_statements -> labeled_statements. + +(** Function definition *) + +Record function : Set := mkfunction { + fn_return: type; + fn_params: list (ident * type); + fn_vars: list (ident * type); + fn_body: statement +}. + +Inductive fundef : Set := + | Internal: function -> fundef + | External: ident -> typelist -> type -> fundef. + +(** Program *) + +Record program : Set := mkprogram { + prog_funct: list (ident * fundef); + prog_defs: list (ident * type * list init_data); + prog_main: ident +}. + +(** ** Operations over types *) + +(** 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 *) + +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 + 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. +Proof. + induction f; simpl. + omega. + generalize (Zmax2 (alignof t) (alignof_fields f)). omega. +Qed. + +Lemma alignof_pos: + forall t, alignof t > 0. +Proof. + induction t; simpl; auto; try omega. + destruct i; omega. + destruct f; omega. + apply alignof_fields_pos. + apply alignof_fields_pos. +Qed. + +(** 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) + 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. +Proof. + intro t0. + apply (type_ind2 (fun t => sizeof t > 0) + (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0)); + intros; simpl; auto; try omega. + destruct i; omega. + destruct f; omega. + apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. + destruct H. + generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). + generalize (Zmax1 1 (sizeof_struct f 0)). omega. + generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). + generalize (Zmax1 1 (sizeof_union f)). omega. + split. omega. auto. + destruct H0. split; intros. + generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. + apply H1. + generalize (align_le pos (alignof t) (alignof_pos t)). omega. +Qed. + +(** Byte offset for a field in a struct. *) + +Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) + {struct fld} : option Z := + match fld with + | Fnil => None + | Fcons id' t fld' => + if ident_eq id id' + then Some (align pos (alignof t)) + else field_offset_rec id fld' (align pos (alignof t) + sizeof t) + end. + +Definition field_offset (id: ident) (fld: fieldlist) : option Z := + field_offset_rec id fld 0. + +(* Describe how a variable of the given type must be accessed: + - by value, i.e. by loading from the address of the variable + with the given chunk + - by reference, i.e. by just returning the address of the variable + - not at all, e.g. the [void] type. *) + +Inductive mode: Set := + | 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 +end. + +(** Conversion of a Clight program into an AST program *) + +Definition extract_global_var (id_ty_init: ident * type * list init_data) := + match id_ty_init with (id, ty, init) => (id, init) end. + +Definition program_of_program (p: program) : AST.program fundef := + AST.mkprogram + p.(prog_funct) + p.(prog_main) + (List.map extract_global_var p.(prog_defs)). + +(** Classification of arithmetic operations and comparisons *) + +Inductive classify_add_cases : Set := + | add_case_ii: classify_add_cases (* int , int *) + | add_case_ff: classify_add_cases (* float , float *) + | add_case_pi: type -> classify_add_cases (* ptr | array, int *) + | 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 + | _, _ => add_default + end. + +Inductive classify_sub_cases : Set := + | sub_case_ii: classify_sub_cases (* int , int *) + | sub_case_ff: classify_sub_cases (* float , float *) + | sub_case_pi: type -> classify_sub_cases (* ptr | array , int *) + | sub_case_pp: type -> classify_sub_cases (* ptr | array , ptr | 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 : Set:= + | 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 : Set:= + | div_case_I32unsi: classify_div_cases (* uns 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 : Set:= + | mod_case_I32unsi: classify_mod_cases (* uns 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 :Set:= + | shr_case_I32unsi: classify_shr_cases (* uns 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 : Set:= + | cmp_case_I32unsi: classify_cmp_cases (* uns I32 , int *) + | cmp_case_ii: classify_cmp_cases (* int , int*) + | cmp_case_ff: classify_cmp_cases (* float , float *) + | cmp_case_pi: classify_cmp_cases (* ptr | array , int *) + | cmp_case_pp:classify_cmp_cases (* ptr | array , ptr | array *) + | 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_ii + | Tfloat _ , Tfloat _ => cmp_case_ff + | Tpointer _ , Tint _ _ => cmp_case_pi + | Tarray _ _ , Tint _ _ => cmp_case_pi + | Tpointer _ , Tpointer _ => cmp_case_pp + | Tpointer _ , Tarray _ _ => cmp_case_pp + | Tarray _ _ ,Tpointer _ => cmp_case_pp + | Tarray _ _ ,Tarray _ _ => cmp_case_pp + | _ , _ => cmp_default + end. + +Inductive classify_fun_cases : Set:= + | fun_case_f: typelist -> type -> classify_fun_cases (* type fun | ptr fun*) + | 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. + +(** Mapping between Clight types and Cminor types 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). -- cgit