From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 305 +++++++++++++++++++++++++++++++++++++------------- 1 file changed, 225 insertions(+), 80 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index c293efbe..3a8b8575 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -20,12 +20,13 @@ Require Import Maps. Require Import Ordered. Require Import AST. Require Import Integers. +Require Import Floats. Require Import Memdata. Require Import Csharpminor. Require Import Cminor. -Open Local Scope string_scope. -Open Local Scope error_monad_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. (** The main task in translating Csharpminor to Cminor is to explicitly stack-allocate local variables whose address is taken: these local @@ -37,17 +38,17 @@ Open Local Scope error_monad_scope. taken in the Csharpminor code can be mapped to Cminor local variable, since the latter do not reside in memory. - Another task performed during the translation to Cminor is the - insertion of truncation, zero- and sign-extension operations when - assigning to a Csharpminor local variable of ``small'' type - (e.g. [Mfloat32] or [Mint8signed]). This is necessary to preserve - the ``normalize at assignment-time'' semantics of Clight and Csharpminor. + Another task performed during the translation to Cminor is to eliminate + redundant casts to small numerical types (8- and 16-bit integers, + single-precision floats). Finally, the Clight-like [switch] construct of Csharpminor is transformed into the simpler, lower-level [switch] construct of Cminor. *) +(** * Handling of variables *) + Definition for_var (id: ident) : ident := xO id. Definition for_temp (id: ident) : ident := xI id. @@ -69,41 +70,46 @@ Inductive var_info: Type := Definition compilenv := PMap.t var_info. -(***** -(** [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 - [chunk] is [Mint8signed]. *) - -Definition make_cast (chunk: memory_chunk) (e: expr): expr := - match chunk with - | Mint8signed => Eunop Ocast8signed e - | Mint8unsigned => Eunop Ocast8unsigned e - | Mint16signed => Eunop Ocast16signed e - | Mint16unsigned => Eunop Ocast16unsigned e - | Mint32 => e - | Mfloat32 => Eunop Osingleoffloat e - | Mfloat64 => e - end. -**********) +(** * Helper functions for code generation *) (** When the translation of an expression is stored in memory, - a cast at the toplevel of the expression can be redundant + one or several casts at the toplevel of the expression can be redundant with that implicitly performed by the memory store. [store_arg] detects this case and strips away the redundant cast. *) -Definition store_arg (chunk: memory_chunk) (e: expr) : expr := +Function uncast_int8 (e: expr) : expr := + match e with + | Eunop (Ocast8unsigned|Ocast8signed|Ocast16unsigned|Ocast16signed) e1 => + uncast_int8 e1 + | Ebinop Oand e1 (Econst (Ointconst n)) => + if Int.eq (Int.and n (Int.repr 255)) (Int.repr 255) + then uncast_int8 e1 + else e + | _ => e + end. + +Function uncast_int16 (e: expr) : expr := match e with - | Eunop Ocast8signed e1 => - match chunk with Mint8signed => e1 | _ => e end - | Eunop Ocast8unsigned e1 => - match chunk with Mint8unsigned => e1 | _ => e end - | Eunop Ocast16signed e1 => - match chunk with Mint16signed => e1 | _ => e end - | Eunop Ocast16unsigned e1 => - match chunk with Mint16unsigned => e1 | _ => e end - | Eunop Osingleoffloat e1 => - match chunk with Mfloat32 => e1 | _ => e end + | Eunop (Ocast16unsigned|Ocast16signed) e1 => + uncast_int16 e1 + | Ebinop Oand e1 (Econst (Ointconst n)) => + if Int.eq (Int.and n (Int.repr 65535)) (Int.repr 65535) + then uncast_int16 e1 + else e + | _ => e + end. + +Function uncast_float32 (e: expr) : expr := + match e with + | Eunop Osingleoffloat e1 => uncast_float32 e1 + | _ => e + end. + +Function store_arg (chunk: memory_chunk) (e: expr) : expr := + match chunk with + | Mint8signed | Mint8unsigned => uncast_int8 e + | Mint16signed | Mint16unsigned => uncast_int16 e + | Mfloat32 => uncast_float32 e | _ => e end. @@ -116,16 +122,148 @@ Definition make_stackaddr (ofs: Z): expr := Definition make_globaladdr (id: ident): expr := Econst (Oaddrsymbol id Int.zero). +Definition make_unop (op: unary_operation) (e: expr): expr := + match op with + | Ocast8unsigned => Eunop Ocast8unsigned (uncast_int8 e) + | Ocast8signed => Eunop Ocast8signed (uncast_int8 e) + | Ocast16unsigned => Eunop Ocast16unsigned (uncast_int16 e) + | Ocast16signed => Eunop Ocast16signed (uncast_int16 e) + | Osingleoffloat => Eunop Osingleoffloat (uncast_float32 e) + | _ => Eunop op e + end. + +(** * Optimization of casts *) + +(** To remove redundant casts, we perform a modest static analysis + on the values of expressions, classifying them into the following + ranges. *) + +Inductive approx : Type := + | Any (**r any value *) + | Int7 (**r [[0,127]] *) + | Int8s (**r [[-128,127]] *) + | Int8u (**r [[0,255]] *) + | Int15 (**r [[0,32767]] *) + | Int16s (**r [[-32768,32767]] *) + | Int16u (**r [[0,65535]] *) + | Float32. (**r single-precision float *) + +Module Approx. + +Definition bge (x y: approx) : bool := + match x, y with + | Any, _ => true + | Int7, Int7 => true + | Int8s, (Int7 | Int8s) => true + | Int8u, (Int7 | Int8u) => true + | Int15, (Int7 | Int8u | Int15) => true + | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => true + | Int16u, (Int7 | Int8u | Int15 | Int16u) => true + | Float32, Float32 => true + | _, _ => false + end. + +Definition lub (x y: approx) : approx := + match x, y with + | Int7, Int7 => Int7 + | Int7, Int8u => Int8u + | Int7, Int8s => Int8s + | Int7, Int15 => Int15 + | Int7, Int16u => Int16u + | Int7, Int16s => Int16s + | Int8u, (Int7|Int8u) => Int8u + | Int8u, Int15 => Int15 + | Int8u, Int16u => Int16u + | Int8u, Int16s => Int16s + | Int8s, (Int7|Int8s) => Int8s + | Int8s, (Int15|Int16s) => Int16s + | Int15, (Int7|Int8u|Int15) => Int15 + | Int15, Int16u => Int16u + | Int15, (Int8s|Int16s) => Int16s + | Int16u, (Int7|Int8u|Int15|Int16u) => Int16u + | Int16s, (Int7|Int8u|Int8s|Int15|Int16s) => Int16s + | Float32, Float32 => Float32 + | _, _ => Any + end. + +Definition of_int (n: int) := + if Int.eq_dec n (Int.zero_ext 7 n) then Int7 + else if Int.eq_dec n (Int.zero_ext 8 n) then Int8u + else if Int.eq_dec n (Int.sign_ext 8 n) then Int8s + else if Int.eq_dec n (Int.zero_ext 15 n) then Int15 + else if Int.eq_dec n (Int.zero_ext 16 n) then Int16u + else if Int.eq_dec n (Int.sign_ext 16 n) then Int16s + else Any. + +Definition of_float (n: float) := + if Float.eq_dec n (Float.singleoffloat n) then Float32 else Any. + +Definition of_chunk (chunk: memory_chunk) := + match chunk with + | Mint8signed => Int8s + | Mint8unsigned => Int8u + | Mint16signed => Int16s + | Mint16unsigned => Int16u + | Mint32 => Any + | Mfloat32 => Float32 + | Mfloat64 => Any + end. + +Definition unop (op: unary_operation) (a: approx) := + match op with + | Ocast8unsigned => Int8u + | Ocast8signed => Int8s + | Ocast16unsigned => Int16u + | Ocast16signed => Int16s + | Osingleoffloat => Float32 + | Onotbool => Int7 + | _ => Any + end. + +Definition unop_is_redundant (op: unary_operation) (a: approx) := + match op with + | Ocast8unsigned => bge Int8u a + | Ocast8signed => bge Int8s a + | Ocast16unsigned => bge Int16u a + | Ocast16signed => bge Int16s a + | Osingleoffloat => bge Float32 a + | _ => false + end. + +Definition bitwise_and (a1 a2: approx) := + if bge Int8u a1 || bge Int8u a2 then Int8u + else if bge Int16u a1 || bge Int16u a2 then Int16u + else Any. + +Definition bitwise_or (a1 a2: approx) := + if bge Int8u a1 && bge Int8u a2 then Int8u + else if bge Int16u a1 && bge Int16u a2 then Int16u + else Any. + +Definition binop (op: binary_operation) (a1 a2: approx) := + match op with + | Oand => bitwise_and a1 a2 + | Oor | Oxor => bitwise_or a1 a2 + | Ocmp _ => Int7 + | Ocmpu _ => Int7 + | Ocmpf _ => Int7 + | _ => Any + end. + +End Approx. + +(** * Translation of expressions and statements. *) + (** Generation of a Cminor expression for reading a Csharpminor variable. *) -Definition var_get (cenv: compilenv) (id: ident): res expr := +Definition var_get (cenv: compilenv) (id: ident): res (expr * approx) := match PMap.get id cenv with | Var_local chunk => - OK(Evar (for_var id)) + OK(Evar (for_var id), Approx.of_chunk chunk) | Var_stack_scalar chunk ofs => - OK(Eload chunk (make_stackaddr ofs)) + OK(Eload chunk (make_stackaddr ofs), Approx.of_chunk chunk) | Var_global_scalar chunk => - OK(Eload chunk (make_globaladdr id)) + OK(Eload chunk (make_globaladdr id), Approx.of_chunk chunk) | _ => Error(msg "Cminorgen.var_get") end. @@ -133,12 +271,12 @@ Definition var_get (cenv: compilenv) (id: ident): res expr := (** Generation of a Cminor expression for taking the address of a Csharpminor variable. *) -Definition var_addr (cenv: compilenv) (id: ident): res expr := +Definition var_addr (cenv: compilenv) (id: ident): res (expr * approx) := match PMap.get id cenv with | Var_local chunk => Error(msg "Cminorgen.var_addr") - | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs) - | Var_stack_array ofs => OK (make_stackaddr ofs) - | _ => OK (make_globaladdr id) + | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs, Any) + | Var_stack_array ofs => OK (make_stackaddr ofs, Any) + | _ => OK (make_globaladdr id, Any) end. (** Generation of a Cminor statement performing an assignment to @@ -175,38 +313,46 @@ Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ) (k: stmt): res s (** Translation of constants. *) -Definition transl_constant (cst: Csharpminor.constant): constant := +Definition transl_constant (cst: Csharpminor.constant): (constant * approx) := match cst with - | Csharpminor.Ointconst n => Ointconst n - | Csharpminor.Ofloatconst n => Ofloatconst n + | Csharpminor.Ointconst n => + (Ointconst n, Approx.of_int n) + | Csharpminor.Ofloatconst n => + (Ofloatconst n, Approx.of_float n) end. -(** Translation of expressions. All the hard work is done by the - [make_*] and [var_*] functions defined above. *) +(** Translation of expressions. Return both a Cminor expression and + a compile-time approximation of the value of the original + C#minor expression, which is used to remove redundant casts. *) Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) - {struct e}: res expr := + {struct e}: res (expr * approx) := 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.Evar id => + var_get cenv id + | Csharpminor.Etempvar id => + OK (Evar (for_temp id), Any) + | Csharpminor.Eaddrof id => + var_addr cenv id | Csharpminor.Econst cst => - OK (Econst (transl_constant cst)) + let (tcst, a) := transl_constant cst in OK (Econst tcst, a) | Csharpminor.Eunop op e1 => - do te1 <- transl_expr cenv e1; - OK (Eunop op te1) + do (te1, a1) <- transl_expr cenv e1; + if Approx.unop_is_redundant op a1 + then OK (te1, a1) + else OK (make_unop op te1, Approx.unop op a1) | Csharpminor.Ebinop op e1 e2 => - do te1 <- transl_expr cenv e1; - do te2 <- transl_expr cenv e2; - OK (Ebinop op te1 te2) + do (te1, a1) <- transl_expr cenv e1; + do (te2, a2) <- transl_expr cenv e2; + OK (Ebinop op te1 te2, Approx.binop op a1 a2) | Csharpminor.Eload chunk e => - do te <- transl_expr cenv e; - OK (Eload chunk te) + do (te, a) <- transl_expr cenv e; + OK (Eload chunk te, Approx.of_chunk chunk) | Csharpminor.Econdition e1 e2 e3 => - do te1 <- transl_expr cenv e1; - do te2 <- transl_expr cenv e2; - do te3 <- transl_expr cenv e3; - OK (Econdition te1 te2 te3) + do (te1, a1) <- transl_expr cenv e1; + do (te2, a2) <- transl_expr cenv e2; + do (te3, a3) <- transl_expr cenv e3; + OK (Econdition te1 te2 te3, Approx.lub a2 a3) end. Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) @@ -215,7 +361,7 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) | nil => OK nil | e1 :: e2 => - do te1 <- transl_expr cenv e1; + do (te1, a1) <- transl_expr cenv e1; do te2 <- transl_exprlist cenv e2; OK (te1 :: te2) end. @@ -261,12 +407,7 @@ Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env := end. (** Translation of statements. The nonobvious part is - the translation of [switch] statements, outlined above. - Also note the additional type checks on arguments to calls and returns. - These checks should always succeed for C#minor code generated from - well-typed Clight code, but are necessary for the correctness proof - to go through. -*) + the translation of [switch] statements, outlined above. *) Definition typ_of_opttyp (ot: option typ) := match ot with None => Tint | Some t => t end. @@ -278,17 +419,17 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) | Csharpminor.Sskip => OK Sskip | Csharpminor.Sassign id e => - do te <- transl_expr cenv e; + do (te, a) <- transl_expr cenv e; var_set cenv id te | Csharpminor.Sset id e => - do te <- transl_expr cenv e; + do (te, a) <- 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; + do (te1, a1) <- transl_expr cenv e1; + do (te2, a2) <- transl_expr cenv e2; OK (make_store chunk te1 te2) | Csharpminor.Scall optid sig e el => - do te <- transl_expr cenv e; + do (te, a) <- transl_expr cenv e; do tel <- transl_exprlist cenv el; OK (Scall (option_map for_temp optid) sig te tel) | Csharpminor.Sseq s1 s2 => @@ -296,7 +437,7 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) do ts2 <- transl_stmt ret cenv xenv s2; OK (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => - do te <- transl_expr cenv e; + do (te, a) <- transl_expr cenv e; do ts1 <- transl_stmt ret cenv xenv s1; do ts2 <- transl_stmt ret cenv xenv s2; OK (Sifthenelse te ts1 ts2) @@ -311,12 +452,12 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) | Csharpminor.Sswitch e ls => let cases := switch_table ls O in let default := length cases in - do te <- transl_expr cenv e; + do (te, a) <- transl_expr cenv e; transl_lblstmt ret cenv (switch_env ls xenv) ls (Sswitch te cases default) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => - do te <- transl_expr cenv e; + do (te, a) <- transl_expr cenv e; OK (Sreturn (Some te)) | Csharpminor.Slabel lbl s => do ts <- transl_stmt ret cenv xenv s; OK (Slabel lbl ts) @@ -336,6 +477,8 @@ with transl_lblstmt (ret: option typ) (cenv: compilenv) transl_lblstmt ret cenv (List.tail xenv) ls' (Sseq (Sblock body) ts) end. +(** * Stack layout *) + (** Computation of the set of variables whose address is taken in a piece of Csharpminor code. *) @@ -455,6 +598,8 @@ Definition build_global_compilenv (p: Csharpminor.program) : compilenv := List.fold_left assign_global_variable p.(prog_vars) (PMap.init Var_global_array). +(** * Translation of functions *) + (** Function parameters whose address is taken must be stored in their stack slots at function entry. (Cminor passes these parameters in local variables.) *) -- cgit