From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 266 ++++++++------------------------------------------ 1 file changed, 38 insertions(+), 228 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index e60de3de..22c3a5a8 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -48,6 +48,9 @@ Open Local Scope error_monad_scope. of Cminor. *) +Definition for_var (id: ident) : ident := xO id. +Definition for_temp (id: ident) : ident := xI id. + (** Compile-time information attached to each Csharpminor variable: global variables, local variables, function parameters. [Var_local] denotes a scalar local variable whose address is not @@ -66,128 +69,7 @@ Inductive var_info: Type := Definition compilenv := PMap.t var_info. -(** Infer the type or memory chunk of the result of an expression. *) - -Definition chunktype_const (c: Csharpminor.constant) := - match c with - | Csharpminor.Ointconst n => - if Int.ltu n (Int.repr 256) then Mint8unsigned - else if Int.ltu n (Int.repr 65536) then Mint16unsigned - else Mint32 - | Csharpminor.Ofloatconst n => Mfloat64 - end. - -Definition chunktype_unop (op: unary_operation) := - match op with - | Ocast8unsigned => Mint8unsigned - | Ocast8signed => Mint8signed - | Ocast16unsigned => Mint16unsigned - | Ocast16signed => Mint16signed - | Onegint => Mint32 - | Onotbool => Mint8unsigned - | Onotint => Mint32 - | Onegf => Mfloat64 - | Oabsf => Mfloat64 - | Osingleoffloat => Mfloat32 - | Ointoffloat => Mint32 - | Ointuoffloat => Mint32 - | Ofloatofint => Mfloat64 - | Ofloatofintu => Mfloat64 - end. - -Definition chunktype_logical_op (chunk1 chunk2: memory_chunk) := - match chunk1, chunk2 with - | Mint8unsigned, Mint8unsigned => Mint8unsigned - | Mint8unsigned, Mint16unsigned => Mint16unsigned - | Mint16unsigned, Mint8unsigned => Mint16unsigned - | Mint16unsigned, Mint16unsigned => Mint16unsigned - | _, _ => Mint32 - end. - -Definition chunktype_binop (op: binary_operation) (chunk1 chunk2: memory_chunk) := - match op with - | Oadd => Mint32 - | Osub => Mint32 - | Omul => Mint32 - | Odiv => Mint32 - | Odivu => Mint32 - | Omod => Mint32 - | Omodu => Mint32 - | Oand => chunktype_logical_op chunk1 chunk2 - | Oor => chunktype_logical_op chunk1 chunk2 - | Oxor => chunktype_logical_op chunk1 chunk2 - | Oshl => Mint32 - | Oshr => Mint32 - | Oshru => Mint32 - | Oaddf => Mfloat64 - | Osubf => Mfloat64 - | Omulf => Mfloat64 - | Odivf => Mfloat64 - | Ocmp c => Mint8unsigned - | Ocmpu c => Mint8unsigned - | Ocmpf c => Mint8unsigned - end. - -Definition chunktype_compat (src dst: memory_chunk) : bool := - match src, dst with - | Mint8unsigned, (Mint8unsigned|Mint16unsigned|Mint16signed|Mint32) => true - | Mint8signed, (Mint8signed|Mint16signed|Mint32) => true - | Mint16unsigned, (Mint16unsigned|Mint32) => true - | Mint16signed, (Mint16signed|Mint32) => true - | Mint32, Mint32 => true - | Mfloat32, (Mfloat32|Mfloat64) => true - | Mfloat64, Mfloat64 => true - | _, _ => false - end. - -Definition chunk_for_type (ty: typ) : memory_chunk := - match ty with Tint => Mint32 | Tfloat => Mfloat64 end. - -Definition chunktype_merge (c1 c2: memory_chunk) : res memory_chunk := - if chunktype_compat c1 c2 then - OK c2 - else if chunktype_compat c2 c1 then - OK c1 - else if typ_eq (type_of_chunk c1) (type_of_chunk c2) then - OK (chunk_for_type (type_of_chunk c1)) - else - Error(msg "Cminorgen: chunktype_merge"). - -Fixpoint chunktype_expr (cenv: compilenv) (e: Csharpminor.expr) - {struct e}: res memory_chunk := - match e with - | Csharpminor.Evar id => - match cenv!!id with - | Var_local chunk => OK chunk - | Var_stack_scalar chunk ofs => OK chunk - | Var_global_scalar chunk => OK chunk - | _ => Error(msg "Cminorgen.chunktype_expr") - end - | Csharpminor.Eaddrof id => - OK Mint32 - | Csharpminor.Econst cst => - OK (chunktype_const cst) - | Csharpminor.Eunop op e1 => - OK (chunktype_unop op) - | Csharpminor.Ebinop op e1 e2 => - do chunk1 <- chunktype_expr cenv e1; - do chunk2 <- chunktype_expr cenv e2; - OK (chunktype_binop op chunk1 chunk2) - | Csharpminor.Eload chunk e => - OK chunk - | Csharpminor.Econdition e1 e2 e3 => - do chunk2 <- chunktype_expr cenv e2; - do chunk3 <- chunktype_expr cenv e3; - chunktype_merge chunk2 chunk3 - end. - -Definition type_expr (cenv: compilenv) (e: Csharpminor.expr): res typ := - do c <- chunktype_expr cenv e; OK(type_of_chunk c). - -Definition type_exprlist (cenv: compilenv) (el: list Csharpminor.expr): - res (list typ) := - mmap (type_expr cenv) el. - +(***** (** [make_cast chunk e] returns a Cminor expression that normalizes the value of Cminor expression [e] as prescribed by the memory chunk [chunk]. For instance, 8-bit sign extension is performed if @@ -203,6 +85,7 @@ Definition make_cast (chunk: memory_chunk) (e: expr): expr := | Mfloat32 => Eunop Osingleoffloat e | Mfloat64 => e end. +**********) (** When the translation of an expression is stored in memory, a cast at the toplevel of the expression can be redundant @@ -233,24 +116,12 @@ Definition make_stackaddr (ofs: Z): expr := Definition make_globaladdr (id: ident): expr := Econst (Oaddrsymbol id Int.zero). -(** Auxiliary to remove useless conversions. *) - -Definition unop_is_cast (op: unary_operation) : option memory_chunk := - match op with - | Ocast8unsigned => Some Mint8unsigned - | Ocast8signed => Some Mint8signed - | Ocast16unsigned => Some Mint16unsigned - | Ocast16signed => Some Mint16signed - | Osingleoffloat => Some Mfloat32 - | _ => None - end. - (** Generation of a Cminor expression for reading a Csharpminor variable. *) Definition var_get (cenv: compilenv) (id: ident): res expr := match PMap.get id cenv with | Var_local chunk => - OK(Evar id) + OK(Evar (for_var id)) | Var_stack_scalar chunk ofs => OK(Eload chunk (make_stackaddr ofs)) | Var_global_scalar chunk => @@ -271,45 +142,33 @@ Definition var_addr (cenv: compilenv) (id: ident): res expr := end. (** Generation of a Cminor statement performing an assignment to - a variable. [rhs_chunk] is the inferred chunk type for the - right-hand side. If the variable was allocated to a Cminor variable, - a cast may need to be inserted to normalize the value of the r.h.s., - as per Csharpminor's semantics. *) + a variable. The value being assigned is normalized according to + its chunk type, as guaranteed by C#minor semantics. *) Definition var_set (cenv: compilenv) - (id: ident) (rhs: expr) (rhs_chunk: memory_chunk): res stmt := + (id: ident) (rhs: expr): res stmt := match PMap.get id cenv with | Var_local chunk => - if chunktype_compat rhs_chunk chunk then - OK(Sassign id rhs) - else if typ_eq (type_of_chunk chunk) (type_of_chunk rhs_chunk) then - OK(Sassign id (make_cast chunk rhs)) - else - Error(msg "Cminorgen.var_set.1") + OK(Sassign (for_var id) rhs) | Var_stack_scalar chunk ofs => OK(make_store chunk (make_stackaddr ofs) rhs) | Var_global_scalar chunk => OK(make_store chunk (make_globaladdr id) rhs) | _ => - Error(msg "Cminorgen.var_set.2") + Error(msg "Cminorgen.var_set") end. -(** A variant of [var_set] used for initializing function parameters - and storing the return values of function calls. The value to - be stored already resides in the Cminor variable called [id]. - Moreover, its chunk type is not known, only its int-or-float type. *) +(** A variant of [var_set] used for initializing function parameters. + The value to be stored already resides in the Cminor variable called [id]. *) -Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ): res stmt := +Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ) (k: stmt): res stmt := match PMap.get id cenv with | Var_local chunk => - if typ_eq (type_of_chunk chunk) ty then - OK(Sassign id (make_cast chunk (Evar id))) - else - Error(msg "Cminorgen.var_set_self.1") + OK k | Var_stack_scalar chunk ofs => - OK(make_store chunk (make_stackaddr ofs) (Evar id)) + OK (Sseq (make_store chunk (make_stackaddr ofs) (Evar (for_var id))) k) | Var_global_scalar chunk => - OK(make_store chunk (make_globaladdr id) (Evar id)) + OK (Sseq (make_store chunk (make_globaladdr id) (Evar (for_var id))) k) | _ => Error(msg "Cminorgen.var_set_self.2") end. @@ -329,19 +188,13 @@ Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) {struct e}: res expr := match e with | Csharpminor.Evar id => var_get cenv id + | Csharpminor.Etempvar id => OK (Evar (for_temp id)) | Csharpminor.Eaddrof id => var_addr cenv id | Csharpminor.Econst cst => OK (Econst (transl_constant cst)) | Csharpminor.Eunop op e1 => do te1 <- transl_expr cenv e1; - match unop_is_cast op with - | None => OK (Eunop op te1) - | Some chunk => - do chunk1 <- chunktype_expr cenv e1; - if chunktype_compat chunk1 chunk - then OK te1 - else OK (Eunop op te1) - end + OK (Eunop op te1) | Csharpminor.Ebinop op e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; @@ -425,28 +278,19 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) | Csharpminor.Sskip => OK Sskip | Csharpminor.Sassign id e => - do chunk <- chunktype_expr cenv e; do te <- transl_expr cenv e; - var_set cenv id te chunk + var_set cenv id te + | Csharpminor.Sset id e => + do te <- transl_expr cenv e; + OK (Sassign (for_temp id) te) | Csharpminor.Sstore chunk e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; OK (make_store chunk te1 te2) - | Csharpminor.Scall None sig e el => - do te <- transl_expr cenv e; - do tel <- transl_exprlist cenv el; - do tyl <- type_exprlist cenv el; - if list_eq_dec typ_eq tyl sig.(sig_args) - then OK (Scall None sig te tel) - else Error(msg "Cminorgen.transl_stmt(call0)") - | Csharpminor.Scall (Some id) sig e el => + | Csharpminor.Scall optid sig e el => do te <- transl_expr cenv e; do tel <- transl_exprlist cenv el; - do tyl <- type_exprlist cenv el; - do s <- var_set_self cenv id (proj_sig_res sig); - if list_eq_dec typ_eq tyl sig.(sig_args) - then OK (Sseq (Scall (Some id) sig te tel) s) - else Error(msg "Cminorgen.transl_stmt(call1)") + OK (Scall (option_map for_temp optid) sig te tel) | Csharpminor.Sseq s1 s2 => do ts1 <- transl_stmt ret cenv xenv s1; do ts2 <- transl_stmt ret cenv xenv s2; @@ -473,10 +317,7 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) OK (Sreturn None) | Csharpminor.Sreturn (Some e) => do te <- transl_expr cenv e; - do ty <- type_expr cenv e; - if typ_eq ty (typ_of_opttyp ret) - then OK (Sreturn (Some te)) - else Error(msg "Cminorgen.transl_stmt(return)") + OK (Sreturn (Some te)) | Csharpminor.Slabel lbl s => do ts <- transl_stmt ret cenv xenv s; OK (Slabel lbl ts) | Csharpminor.Sgoto lbl => @@ -503,6 +344,7 @@ Module Identset := FSetAVL.Make(OrderedPositive). Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t := match e with | Csharpminor.Evar id => Identset.empty + | Csharpminor.Etempvar id => Identset.empty | Csharpminor.Eaddrof id => Identset.add id Identset.empty | Csharpminor.Econst cst => Identset.empty | Csharpminor.Eunop op e1 => addr_taken_expr e1 @@ -525,6 +367,7 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := match s with | Csharpminor.Sskip => Identset.empty | Csharpminor.Sassign id e => addr_taken_expr e + | Csharpminor.Sset id e => addr_taken_expr e | Csharpminor.Sstore chunk e1 e2 => Identset.union (addr_taken_expr e1) (addr_taken_expr e2) | Csharpminor.Scall optid sig e el => @@ -601,8 +444,11 @@ Definition build_compilenv Definition assign_global_variable (ce: compilenv) (info: ident * globvar var_kind) : compilenv := match info with - | (id, mkglobvar (Vscalar chunk) _ _ _ ) => PMap.set id (Var_global_scalar chunk) ce - | (id, mkglobvar (Varray _) _ _ _) => PMap.set id Var_global_array ce + | (id, mkglobvar vk _ _ _) => + PMap.set id (match vk with Vscalar chunk => Var_global_scalar chunk + | Varray _ => Var_global_array + end) + ce end. Definition build_global_compilenv (p: Csharpminor.program) : compilenv := @@ -619,45 +465,10 @@ Fixpoint store_parameters match params with | nil => OK Sskip | (id, chunk) :: rem => - do s1 <- var_set_self cenv id (type_of_chunk chunk); - do s2 <- store_parameters cenv rem; - OK (Sseq s1 s2) + do s <- store_parameters cenv rem; + var_set_self cenv id (type_of_chunk chunk) s end. -(** The local variables of the generated Cminor function - must include all local variables of the C#minor function - (to help the proof in [Cminorgenproof] go through). - We must also add the destinations [x] of calls [x = f(args)], - because some of these [x] can be global variables and therefore - not part of the C#minor local variables. *) - -Fixpoint call_dest (s: stmt) : Identset.t := - match s with - | Sskip => Identset.empty - | Sassign x e => Identset.empty - | Sstore chunk e1 e2 => Identset.empty - | Scall None sg e el => Identset.empty - | Scall (Some x) sg e el => Identset.singleton x - | Stailcall sg e el => Identset.empty - | Sseq s1 s2 => Identset.union (call_dest s1) (call_dest s2) - | Sifthenelse e s1 s2 => Identset.union (call_dest s1) (call_dest s2) - | Sloop s1 => call_dest s1 - | Sblock s1 => call_dest s1 - | Sexit n => Identset.empty - | Sswitch e cases dfl => Identset.empty - | Sreturn opte => Identset.empty - | Slabel lbl s1 => call_dest s1 - | Sgoto lbl => Identset.empty - end. - -Definition identset_removelist (l: list ident) (s: Identset.t) : Identset.t := - List.fold_right Identset.remove s l. - -Definition make_vars (params: list ident) (vars: list ident) - (body: Cminor.stmt) : list ident := - vars ++ - Identset.elements (identset_removelist (params ++ vars) (call_dest body)). - (** Translation of a Csharpminor function. We must check that the required Cminor stack block is no bigger than [Int.max_signed], otherwise address computations within the stack block could @@ -669,10 +480,9 @@ Definition transl_funbody do sparams <- store_parameters cenv f.(Csharpminor.fn_params); OK (mkfunction (Csharpminor.fn_sig f) - (Csharpminor.fn_params_names f) - (make_vars (Csharpminor.fn_params_names f) - (Csharpminor.fn_vars_names f) - (Sseq sparams tbody)) + (List.map for_var (Csharpminor.fn_params_names f)) + (List.map for_var (Csharpminor.fn_vars_names f) ++ + List.map for_temp (Csharpminor.fn_temps f)) stacksize (Sseq sparams tbody)). -- cgit