From 8539759095f95f2fbb680efc7633d868099114c8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Dec 2012 16:55:38 +0000 Subject: Merge of the clightgen branch: - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 116 ++++++++-------------------------------------------- 1 file changed, 17 insertions(+), 99 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index a4592977..9d518cba 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -34,36 +34,6 @@ Require Import Csharpminor. Open Local Scope string_scope. Open Local Scope error_monad_scope. -(** * Operations on C types *) - -Definition chunk_of_type (ty: type): res memory_chunk := - match access_mode ty with - | By_value chunk => OK chunk - | _ => Error (msg "Cshmgen.chunk_of_type") - end. - -(** [var_kind_of_type ty] returns the Csharpminor ``variable kind'' - (scalar or array) that corresponds to the given Clight type [ty]. *) - -Definition var_kind_of_type (ty: type): res var_kind := - match ty with - | Tint I8 Signed _ => OK(Vscalar Mint8signed) - | Tint I8 Unsigned _ => OK(Vscalar Mint8unsigned) - | Tint I16 Signed _ => OK(Vscalar Mint16signed) - | Tint I16 Unsigned _ => OK(Vscalar Mint16unsigned) - | Tint I32 _ _ => OK(Vscalar Mint32) - | Tint IBool _ _ => OK(Vscalar Mint8unsigned) - | Tfloat F32 _ => OK(Vscalar Mfloat32) - | Tfloat F64 _ => OK(Vscalar Mfloat64) - | Tvoid => Error (msg "Cshmgen.var_kind_of_type(void)") - | Tpointer _ _ => OK(Vscalar Mint32) - | Tarray _ _ _ => OK(Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) - | Tfunction _ _ => Error (msg "Cshmgen.var_kind_of_type(function)") - | Tstruct _ fList _ => OK(Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) - | Tunion _ fList _ => OK(Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) - | Tcomp_ptr _ _ => OK(Vscalar Mint32) -end. - (** * Csharpminor constructors *) (** The following functions build Csharpminor expressions that compute @@ -284,42 +254,6 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) := | _ => Error (msg "Cshmgen.make_store") end. -(** * Reading and writing variables *) - -(** Determine if a C expression is a variable *) - -Definition is_variable (e: Clight.expr) : option ident := - match e with - | Clight.Evar id _ => Some id - | _ => None - end. - -(** [var_get id ty] returns Csharpminor code that evaluates to the - value of C variable [id] with type [ty]. Note that - C variables of array or function type evaluate to the address - of the corresponding Clight memory block, while variables of other types - evaluate to the contents of the corresponding C memory block. -*) - -Definition var_get (id: ident) (ty: type) := - match access_mode ty with - | By_value chunk => OK (Evar id) - | By_reference => OK (Eaddrof id) - | By_copy => OK (Eaddrof id) - | _ => Error (MSG "Cshmgen.var_get " :: CTX id :: nil) - end. - -(** Likewise, [var_set id ty rhs] stores the value of the Csharpminor - expression [rhs] into the Clight variable [id] of type [ty]. -*) - -Definition var_set (id: ident) (ty: type) (rhs: expr) := - match access_mode ty with - | By_value chunk => OK (Sassign id rhs) - | By_copy => OK (make_memcpy (Eaddrof id) rhs ty) - | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil) - end. - (** ** Translation of operators *) Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr := @@ -364,12 +298,12 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := | Clight.Econst_float n _ => OK(make_floatconst n) | Clight.Evar id ty => - var_get id ty + make_load (Eaddrof id) ty | Clight.Etempvar id ty => - OK(Etempvar id) - | Clight.Ederef b _ => + OK(Evar id) + | Clight.Ederef b ty => do tb <- transl_expr b; - make_load tb (typeof a) + make_load tb ty | Clight.Eaddrof b _ => transl_lvalue b | Clight.Eunop op b _ => @@ -472,15 +406,9 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) | Clight.Sskip => OK Sskip | Clight.Sassign b c => - match is_variable b with - | Some id => - do tc <- transl_expr c; - var_set id (typeof b) (make_cast (typeof c) (typeof b) tc) - | None => - do tb <- transl_lvalue b; - do tc <- transl_expr c; - make_store tb (typeof b) (make_cast (typeof c) (typeof b) tc) - end + do tb <- transl_lvalue b; + do tc <- transl_expr c; + make_store tb (typeof b) (make_cast (typeof c) (typeof b) tc) | Clight.Sset x b => do tb <- transl_expr b; OK(Sset x tb) @@ -543,29 +471,19 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat) (*** Translation of functions *) -Definition prefix_var_name (id: ident) : errmsg := - MSG "In local variable " :: CTX id :: MSG ": " :: nil. - -Fixpoint transl_vars (l: list (ident * type)) : res (list (ident * var_kind)) := - match l with - | nil => OK nil - | (id, ty) :: l' => - match var_kind_of_type ty with - | Error msg => Error (MSG "In local variable " :: CTX id :: MSG ": " :: msg) - | OK vk => - do tl' <- transl_vars l'; OK ((id, vk) :: tl') - end - end. +Definition transl_var (v: ident * type) := (fst v, sizeof (snd v)). + +Definition signature_of_function (f: Clight.function) := + mksignature (map typ_of_type (map snd (Clight.fn_params f))) + (opttyp_of_type (Clight.fn_return f)). Definition transl_function (f: Clight.function) : res function := - do tparams <- transl_vars (Clight.fn_params f); - do tvars <- transl_vars (Clight.fn_vars f); do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f); OK (mkfunction - (opttyp_of_type (Clight.fn_return f)) - tparams - tvars - (List.map (@fst ident type) f.(Clight.fn_temps)) + (signature_of_function f) + (map fst (Clight.fn_params f)) + (map transl_var (Clight.fn_vars f)) + (map fst (Clight.fn_temps f)) tbody). Definition list_typ_eq: @@ -587,7 +505,7 @@ Definition transl_fundef (f: Clight.fundef) : res fundef := (** ** Translation of programs *) -Definition transl_globvar (ty: type) := var_kind_of_type ty. +Definition transl_globvar (ty: type) := OK tt. Definition transl_program (p: Clight.program) : res program := transform_partial_program2 transl_fundef transl_globvar p. -- cgit