diff options
Diffstat (limited to 'cfrontend/Cminorgen.v')
| -rw-r--r-- | cfrontend/Cminorgen.v | 228 |
1 files changed, 29 insertions, 199 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 419ffff..3b902c5 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -55,220 +55,50 @@ Local Open Scope error_monad_scope. Definition compilenv := PTree.t Z. -(** * Helper functions for code generation *) - -(** When the translation of an expression is stored in memory, - 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. *) - -Function uncast_int (m: int) (e: expr) {struct e} : expr := - match e with - | Eunop (Ocast8unsigned|Ocast8signed) e1 => - if Int.eq (Int.and (Int.repr 255) m) m then uncast_int m e1 else e - | Eunop (Ocast16unsigned|Ocast16signed) e1 => - if Int.eq (Int.and (Int.repr 65535) m) m then uncast_int m e1 else e - | Ebinop Oand e1 (Econst (Ointconst n)) => - if Int.eq (Int.and n m) m then uncast_int m e1 else e - | Ebinop Oshru e1 (Econst (Ointconst n)) => - if Int.eq (Int.shru (Int.shl m n) n) m - then Ebinop Oshru (uncast_int (Int.shl m n) e1) (Econst (Ointconst n)) - else e - | Ebinop Oshr e1 (Econst (Ointconst n)) => - if Int.eq (Int.shru (Int.shl m n) n) m - then Ebinop Oshr (uncast_int (Int.shl m n) e1) (Econst (Ointconst n)) - else e - | _ => e - end. - -Definition uncast_int8 (e: expr) : expr := uncast_int (Int.repr 255) e. - -Definition uncast_int16 (e: expr) : expr := uncast_int (Int.repr 65535) e. - -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. - -Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt := - Sstore chunk e1 (store_arg chunk e2). - -Definition make_stackaddr (ofs: Z): expr := - Econst (Oaddrstack (Int.repr ofs)). - -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 *) - | Int1 (**r [0] or [1] *) - | 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 - | Int1, Int1 => true - | Int7, (Int1 | Int7) => true - | Int8s, (Int1 | Int7 | Int8s) => true - | Int8u, (Int1 | Int7 | Int8u) => true - | Int15, (Int1 | Int7 | Int8u | Int15) => true - | Int16s, (Int1 | Int7 | Int8s | Int8u | Int15 | Int16s) => true - | Int16u, (Int1 | Int7 | Int8u | Int15 | Int16u) => true - | Float32, Float32 => true - | _, _ => false - end. - -Definition of_int (n: int) := - if Int.eq_dec n Int.zero || Int.eq_dec n Int.one then Int1 - else 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 - | Mint64 => Any - | Mfloat32 => Float32 - | Mfloat64 => Any - | Mfloat64al32 => Any - end. - -Definition unop (op: unary_operation) (a: approx) := - match op with - | Ocast8unsigned => Int8u - | Ocast8signed => Int8s - | Ocast16unsigned => Int16u - | Ocast16signed => Int16s - | Osingleoffloat => Float32 - | _ => 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 Int1 a1 || bge Int1 a2 then Int1 - else 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 Int1 a1 && bge Int1 a2 then Int1 - else 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 _ => Int1 - | Ocmpu _ => Int1 - | Ocmpf _ => Int1 - | _ => Any - end. - -End Approx. - -(** * Translation of expressions and statements. *) - (** Generation of a Cminor expression for taking the address of a Csharpminor variable. *) Definition var_addr (cenv: compilenv) (id: ident): expr := match PTree.get id cenv with - | Some ofs => make_stackaddr ofs - | None => make_globaladdr id + | Some ofs => Econst (Oaddrstack (Int.repr ofs)) + | None => Econst (Oaddrsymbol id Int.zero) end. +(** * Translation of expressions and statements. *) + (** Translation of constants. *) -Definition transl_constant (cst: Csharpminor.constant): (constant * approx) := +Definition transl_constant (cst: Csharpminor.constant): constant := match cst with | Csharpminor.Ointconst n => - (Ointconst n, Approx.of_int n) + Ointconst n | Csharpminor.Ofloatconst n => - (Ofloatconst n, Approx.of_float n) + Ofloatconst n | Csharpminor.Olongconst n => - (Olongconst n, Any) + Olongconst n end. -(** 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. *) +(** Translation of expressions. *) Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) - {struct e}: res (expr * approx) := + {struct e}: res expr := match e with | Csharpminor.Evar id => - OK (Evar id, Any) + OK (Evar id) | Csharpminor.Eaddrof id => - OK (var_addr cenv id, Any) + OK (var_addr cenv id) | Csharpminor.Econst cst => - let (tcst, a) := transl_constant cst in OK (Econst tcst, a) + OK (Econst (transl_constant cst)) | Csharpminor.Eunop op e1 => - 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) + do te1 <- transl_expr cenv e1; + OK (Eunop op te1) | Csharpminor.Ebinop op e1 e2 => - do (te1, a1) <- transl_expr cenv e1; - do (te2, a2) <- transl_expr cenv e2; - OK (Ebinop op te1 te2, Approx.binop op a1 a2) + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + OK (Ebinop op te1 te2) | Csharpminor.Eload chunk e => - do (te, a) <- transl_expr cenv e; - OK (Eload chunk te, Approx.of_chunk chunk) + do te <- transl_expr cenv e; + OK (Eload chunk te) end. Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) @@ -277,7 +107,7 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) | nil => OK nil | e1 :: e2 => - do (te1, a1) <- transl_expr cenv e1; + do te1 <- transl_expr cenv e1; do te2 <- transl_exprlist cenv e2; OK (te1 :: te2) end. @@ -331,14 +161,14 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) | Csharpminor.Sskip => OK Sskip | Csharpminor.Sset id e => - do (te, a) <- transl_expr cenv e; + do te <- transl_expr cenv e; OK (Sassign id te) | Csharpminor.Sstore chunk e1 e2 => - do (te1, a1) <- transl_expr cenv e1; - do (te2, a2) <- transl_expr cenv e2; - OK (make_store chunk te1 te2) + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + OK (Sstore chunk te1 te2) | Csharpminor.Scall optid sig e el => - do (te, a) <- transl_expr cenv e; + do te <- transl_expr cenv e; do tel <- transl_exprlist cenv el; OK (Scall optid sig te tel) | Csharpminor.Sbuiltin optid ef el => @@ -349,7 +179,7 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) do ts2 <- transl_stmt cenv xenv s2; OK (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => - do (te, a) <- transl_expr cenv e; + do te <- transl_expr cenv e; do ts1 <- transl_stmt cenv xenv s1; do ts2 <- transl_stmt cenv xenv s2; OK (Sifthenelse te ts1 ts2) @@ -364,12 +194,12 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) | Csharpminor.Sswitch e ls => let cases := switch_table ls O in let default := length cases in - do (te, a) <- transl_expr cenv e; + do te <- transl_expr cenv e; transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => - do (te, a) <- transl_expr cenv e; + do te <- transl_expr cenv e; OK (Sreturn (Some te)) | Csharpminor.Slabel lbl s => do ts <- transl_stmt cenv xenv s; OK (Slabel lbl ts) |