diff options
Diffstat (limited to 'arm/Selection.v')
| -rw-r--r-- | arm/Selection.v | 1394 |
1 files changed, 1394 insertions, 0 deletions
diff --git a/arm/Selection.v b/arm/Selection.v new file mode 100644 index 0000000..d5eb6b8 --- /dev/null +++ b/arm/Selection.v @@ -0,0 +1,1394 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection *) + +(** The instruction selection pass recognizes opportunities for using + combined arithmetic and logical operations and addressing modes + offered by the target processor. For instance, the expression [x + 1] + can take advantage of the "immediate add" instruction of the processor, + and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned + into a "rotate and mask" instruction. + + Instruction selection proceeds by bottom-up rewriting over expressions. + The source language is Cminor and the target language is CminorSel. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Cminor. +Require Import Op. +Require Import CminorSel. + +Infix ":::" := Econs (at level 60, right associativity) : selection_scope. + +Open Local Scope selection_scope. + +(** * Lifting of let-bound variables *) + +(** Some of the instruction functions generate [Elet] constructs to + share the evaluation of a subexpression. Owing to the use of de + Bruijn indices for let-bound variables, we need to shift de Bruijn + indices when an expression [b] is put in a [Elet a b] context. *) + +Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := + match a with + | Evar id => Evar id + | Eop op bl => Eop op (lift_exprlist p bl) + | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) + | Econdition b c d => + Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d) + | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) + | Eletvar n => + if le_gt_dec p n then Eletvar (S n) else Eletvar n + end + +with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := + match a with + | CEtrue => CEtrue + | CEfalse => CEfalse + | CEcond cond bl => CEcond cond (lift_exprlist p bl) + | CEcondition b c d => + CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d) + end + +with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := + match a with + | Enil => Enil + | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) + end. + +Definition lift (a: expr): expr := lift_expr O a. + +(** * Smart constructors for operators *) + +(** This section defines functions for building CminorSel expressions + and statements, especially expressions consisting of operator + applications. These functions examine their arguments to choose + cheaper forms of operators whenever possible. + + For instance, [add e1 e2] will return a CminorSel expression semantically + equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a + [Oaddimm] operator if one of the arguments is an integer constant, + or suppress the addition altogether if one of the arguments is the + null integer. In passing, we perform operator reassociation + ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount + of constant propagation. +*) + +(** ** Integer logical negation *) + +(** The natural way to write smart constructors is by pattern-matching + on their arguments, recognizing cases where cheaper operators + or combined operators are applicable. For instance, integer logical + negation has three special cases (not-and, not-or and not-xor), + along with a default case that uses not-or over its arguments and itself. + This is written naively as follows: +<< +Definition notint (e: expr) := + match e with + | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) + | Eop Onot (t1:::Enil) => t1 + | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) + | _ => Eop Onot (e:::Enil) + end. +>> + However, Coq expands complex pattern-matchings like the above into + elementary matchings over all constructors of an inductive type, + resulting in much duplication of the final catch-all case. + Such duplications generate huge executable code and duplicate + cases in the correctness proofs. + + To limit this duplication, we use the following trick due to + Yves Bertot. We first define a dependent inductive type that + characterizes the expressions that match each of the 4 cases of interest. +*) + +Inductive notint_cases: forall (e: expr), Set := + | notint_case1: + forall s t1, + notint_cases (Eop (Oshift s) (t1:::Enil)) + | notint_case2: + forall t1, + notint_cases (Eop Onot (t1:::Enil)) + | notint_case3: + forall s t1, + notint_cases (Eop (Onotshift s) (t1:::Enil)) + | notint_default: + forall (e: expr), + notint_cases e. + +(** We then define a classification function that takes an expression + and return the case in which it falls. Note that the catch-all case + [notint_default] does not state that it is mutually exclusive with + the first three, more specific cases. The classification function + nonetheless chooses the specific cases in preference to the catch-all + case. *) + +Definition notint_match (e: expr) := + match e as z1 return notint_cases z1 with + | Eop (Oshift s) (t1:::Enil) => + notint_case1 s t1 + | Eop Onot (t1:::Enil) => + notint_case2 t1 + | Eop (Onotshift s) (t1:::Enil) => + notint_case3 s t1 + | e => + notint_default e + end. + +(** Finally, the [notint] function we need is defined by a 4-case match + over the result of the classification function. Thus, no duplication + of the right-hand sides of this match occur, and the proof has only + 4 cases to consider (it proceeds by case over [notint_match e]). + Since the default case is not obviously exclusive with the three + specific cases, it is important that its right-hand side is + semantically correct for all possible values of [e], which is the + case here and for all other smart constructors. *) + +Definition notint (e: expr) := + match notint_match e with + | notint_case1 s t1 => + Eop (Onotshift s) (t1:::Enil) + | notint_case2 t1 => + t1 + | notint_case3 s t1 => + Eop (Oshift s) (t1:::Enil) + | notint_default e => + Eop Onot (e:::Enil) + end. + +(** This programming pattern will be applied systematically for the + other smart constructors in this file. *) + +(** ** Boolean negation *) + +Definition notbool_base (e: expr) := + Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil). + +Fixpoint notbool (e: expr) {struct e} : expr := + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil + | Eop (Ocmp cond) args => + Eop (Ocmp (negate_condition cond)) args + | Econdition e1 e2 e3 => + Econdition e1 (notbool e2) (notbool e3) + | _ => + notbool_base e + end. + +(** ** Integer addition and pointer addition *) + +(** Addition of an integer constant. *) + +(* +Definition addimm (n: int) (e: expr) := + if Int.eq n Int.zero then e else + match e with + | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil + | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | _ => Eop (Oaddimm n) (e ::: Enil) + end. +*) + +Inductive addimm_cases: forall (e: expr), Set := + | addimm_case1: + forall m, + addimm_cases (Eop (Ointconst m) Enil) + | addimm_case2: + forall s m, + addimm_cases (Eop (Oaddrsymbol s m) Enil) + | addimm_case3: + forall m, + addimm_cases (Eop (Oaddrstack m) Enil) + | addimm_case4: + forall m t, + addimm_cases (Eop (Oaddimm m) (t ::: Enil)) + | addimm_default: + forall (e: expr), + addimm_cases e. + +Definition addimm_match (e: expr) := + match e as z1 return addimm_cases z1 with + | Eop (Ointconst m) Enil => + addimm_case1 m + | Eop (Oaddrsymbol s m) Enil => + addimm_case2 s m + | Eop (Oaddrstack m) Enil => + addimm_case3 m + | Eop (Oaddimm m) (t ::: Enil) => + addimm_case4 m t + | e => + addimm_default e + end. + +Definition addimm (n: int) (e: expr) := + if Int.eq n Int.zero then e else + match addimm_match e with + | addimm_case1 m => + Eop (Ointconst(Int.add n m)) Enil + | addimm_case2 s m => + Eop (Oaddrsymbol s (Int.add n m)) Enil + | addimm_case3 m => + Eop (Oaddrstack (Int.add n m)) Enil + | addimm_case4 m t => + Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | addimm_default e => + Eop (Oaddimm n) (e ::: Enil) + end. + +(** Addition of two integer or pointer expressions. *) + +(* +Definition add (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) + | Eop(Oaddimm n1) (t1:::Enil)), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) + | t1, Eop (Ointconst n2) Enil => addimm n2 t1 + | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) + | _, _ => Eop Oadd (e1:::e2:::Enil) + end. +*) + +Inductive add_cases: forall (e1: expr) (e2: expr), Set := + | add_case1: + forall n1 t2, + add_cases (Eop (Ointconst n1) Enil) (t2) + | add_case2: + forall n1 t1 n2 t2, + add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) + | add_case3: + forall n1 t1 t2, + add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) + | add_case4: + forall t1 n2, + add_cases (t1) (Eop (Ointconst n2) Enil) + | add_case5: + forall t1 n2 t2, + add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) + | add_case6: + forall s t1 t2, + add_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | add_case7: + forall t1 s t2, + add_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | add_default: + forall (e1: expr) (e2: expr), + add_cases e1 e2. + +Definition add_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return add_cases z1 z2 with + | Eop (Ointconst n1) Enil, t2 => + add_case1 n1 t2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => + add_case2 n1 t1 n2 t2 + | Eop(Oaddimm n1) (t1:::Enil), t2 => + add_case3 n1 t1 t2 + | t1, Eop (Ointconst n2) Enil => + add_case4 t1 n2 + | t1, Eop (Oaddimm n2) (t2:::Enil) => + add_case5 t1 n2 t2 + | Eop (Oshift s) (t1:::Enil), t2 => + add_case6 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + add_case7 t1 s t2 + | e1, e2 => + add_default e1 e2 + end. + +Definition add (e1: expr) (e2: expr) := + match add_match e1 e2 with + | add_case1 n1 t2 => + addimm n1 t2 + | add_case2 n1 t1 n2 t2 => + addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) + | add_case3 n1 t1 t2 => + addimm n1 (Eop Oadd (t1:::t2:::Enil)) + | add_case4 t1 n2 => + addimm n2 t1 + | add_case5 t1 n2 t2 => + addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | add_case6 s t1 t2 => + Eop (Oaddshift s) (t2:::t1:::Enil) + | add_case7 t1 s t2 => + Eop (Oaddshift s) (t1:::t2:::Enil) + | add_default e1 e2 => + Eop Oadd (e1:::e2:::Enil) + end. + +(** ** Integer and pointer subtraction *) + +(* +Definition sub (e1: expr) (e2: expr) := + match e1, e2 with + | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (intsub n1 n2) (Eop Osub (t1:::t2:::Enil)) + | Eop (Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Osub (t1:::t2:::Rnil)) + | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.neg n2) (Eop Osub (t1::::t2:::Enil)) + | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) + | _, _ => Eop Osub (e1:::e2:::Enil) + end. +*) + +Inductive sub_cases: forall (e1: expr) (e2: expr), Set := + | sub_case1: + forall t1 n2, + sub_cases (t1) (Eop (Ointconst n2) Enil) + | sub_case2: + forall n1 t1 n2 t2, + sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) + | sub_case3: + forall n1 t1 t2, + sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) + | sub_case4: + forall t1 n2 t2, + sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) + | sub_case5: + forall n1 t2, + sub_cases (Eop (Ointconst n1) Enil) (t2) + | sub_case6: + forall s t1 t2, + sub_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | sub_case7: + forall t1 s t2, + sub_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | sub_default: + forall (e1: expr) (e2: expr), + sub_cases e1 e2. + +Definition sub_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return sub_cases z1 z2 with + | t1, Eop (Ointconst n2) Enil => + sub_case1 t1 n2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => + sub_case2 n1 t1 n2 t2 + | Eop (Oaddimm n1) (t1:::Enil), t2 => + sub_case3 n1 t1 t2 + | t1, Eop (Oaddimm n2) (t2:::Enil) => + sub_case4 t1 n2 t2 + | Eop (Ointconst n1) Enil, t2 => + sub_case5 n1 t2 + | Eop (Oshift s) (t1:::Enil), t2 => + sub_case6 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + sub_case7 t1 s t2 + | e1, e2 => + sub_default e1 e2 + end. + +Definition sub (e1: expr) (e2: expr) := + match sub_match e1 e2 with + | sub_case1 t1 n2 => + addimm (Int.neg n2) t1 + | sub_case2 n1 t1 n2 t2 => + addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) + | sub_case3 n1 t1 t2 => + addimm n1 (Eop Osub (t1:::t2:::Enil)) + | sub_case4 t1 n2 t2 => + addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) + | sub_case5 n1 t2 => + Eop (Orsubimm n1) (t2:::Enil) + | sub_case6 s t1 t2 => + Eop (Orsubshift s) (t2:::t1:::Enil) + | sub_case7 t1 s t2 => + Eop (Osubshift s) (t1:::t2:::Enil) + | sub_default e1 e2 => + Eop Osub (e1:::e2:::Enil) + end. + +(** ** Immediate shifts *) + +(* +Definition shlimm (e1: expr) := + if Int.eq n Int.zero then e1 else + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) + | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil) + | _ => Eop (Oshift (Olsl n)) (e1:::Enil) + end. +*) + +Inductive shlimm_cases: forall (e1: expr), Set := + | shlimm_case1: + forall n1, + shlimm_cases (Eop (Ointconst n1) Enil) + | shlimm_case2: + forall n1 t1, + shlimm_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) + | shlimm_default: + forall (e1: expr), + shlimm_cases e1. + +Definition shlimm_match (e1: expr) := + match e1 as z1 return shlimm_cases z1 with + | Eop (Ointconst n1) Enil => + shlimm_case1 n1 + | Eop (Oshift (Slsl n1)) (t1:::Enil) => + shlimm_case2 n1 t1 + | e1 => + shlimm_default e1 + end. + +Definition shlimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + match is_shift_amount n with + | None => Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) + | Some n' => + match shlimm_match e1 with + | shlimm_case1 n1 => + Eop (Ointconst(Int.shl n1 n)) Enil + | shlimm_case2 n1 t1 => + match is_shift_amount (Int.add n (s_amount n1)) with + | None => + Eop (Oshift (Slsl n')) (e1:::Enil) + | Some n'' => + Eop (Oshift (Slsl n'')) (t1:::Enil) + end + | shlimm_default e1 => + Eop (Oshift (Slsl n')) (e1:::Enil) + end + end. + +(* +Definition shruimm (e1: expr) := + if Int.eq n Int.zero then e1 else + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) + | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil) + | _ => Eop (Oshift (Olsr n)) (e1:::Enil) + end. +*) + +Inductive shruimm_cases: forall (e1: expr), Set := + | shruimm_case1: + forall n1, + shruimm_cases (Eop (Ointconst n1) Enil) + | shruimm_case2: + forall n1 t1, + shruimm_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) + | shruimm_default: + forall (e1: expr), + shruimm_cases e1. + +Definition shruimm_match (e1: expr) := + match e1 as z1 return shruimm_cases z1 with + | Eop (Ointconst n1) Enil => + shruimm_case1 n1 + | Eop (Oshift (Slsr n1)) (t1:::Enil) => + shruimm_case2 n1 t1 + | e1 => + shruimm_default e1 + end. + +Definition shruimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + match is_shift_amount n with + | None => Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) + | Some n' => + match shruimm_match e1 with + | shruimm_case1 n1 => + Eop (Ointconst(Int.shru n1 n)) Enil + | shruimm_case2 n1 t1 => + match is_shift_amount (Int.add n (s_amount n1)) with + | None => + Eop (Oshift (Slsr n')) (e1:::Enil) + | Some n'' => + Eop (Oshift (Slsr n'')) (t1:::Enil) + end + | shruimm_default e1 => + Eop (Oshift (Slsr n')) (e1:::Enil) + end + end. + +(* +Definition shrimm (e1: expr) := + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) + | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil) + | _ => Eop (Oshift (Oasr n)) (e1:::Enil) + end. +*) + +Inductive shrimm_cases: forall (e1: expr), Set := + | shrimm_case1: + forall n1, + shrimm_cases (Eop (Ointconst n1) Enil) + | shrimm_case2: + forall n1 t1, + shrimm_cases (Eop (Oshift (Sasr n1)) (t1:::Enil)) + | shrimm_default: + forall (e1: expr), + shrimm_cases e1. + +Definition shrimm_match (e1: expr) := + match e1 as z1 return shrimm_cases z1 with + | Eop (Ointconst n1) Enil => + shrimm_case1 n1 + | Eop (Oshift (Sasr n1)) (t1:::Enil) => + shrimm_case2 n1 t1 + | e1 => + shrimm_default e1 + end. + +Definition shrimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + match is_shift_amount n with + | None => Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) + | Some n' => + match shrimm_match e1 with + | shrimm_case1 n1 => + Eop (Ointconst(Int.shr n1 n)) Enil + | shrimm_case2 n1 t1 => + match is_shift_amount (Int.add n (s_amount n1)) with + | None => + Eop (Oshift (Sasr n')) (e1:::Enil) + | Some n'' => + Eop (Oshift (Sasr n'')) (t1:::Enil) + end + | shrimm_default e1 => + Eop (Oshift (Sasr n')) (e1:::Enil) + end + end. + +(** ** Integer multiply *) + +Definition mulimm_base (n1: int) (e2: expr) := + match Int.one_bits n1 with + | i :: nil => + shlimm e2 i + | i :: j :: nil => + Elet e2 + (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) + | _ => + Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) + end. + +(* +Definition mulimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then + Eop (Ointconst Int.zero) Enil + else if Int.eq n1 Int.one then + e2 + else match e2 with + | Eop (Ointconst n2) Enil => Eop (Ointconst(intmul n1 n2)) Enil + | Eop (Oaddimm n2) (t2:::Enil) => addimm (intmul n1 n2) (mulimm_base n1 t2) + | _ => mulimm_base n1 e2 + end. +*) + +Inductive mulimm_cases: forall (e2: expr), Set := + | mulimm_case1: + forall (n2: int), + mulimm_cases (Eop (Ointconst n2) Enil) + | mulimm_case2: + forall (n2: int) (t2: expr), + mulimm_cases (Eop (Oaddimm n2) (t2:::Enil)) + | mulimm_default: + forall (e2: expr), + mulimm_cases e2. + +Definition mulimm_match (e2: expr) := + match e2 as z1 return mulimm_cases z1 with + | Eop (Ointconst n2) Enil => + mulimm_case1 n2 + | Eop (Oaddimm n2) (t2:::Enil) => + mulimm_case2 n2 t2 + | e2 => + mulimm_default e2 + end. + +Definition mulimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then + Eop (Ointconst Int.zero) Enil + else if Int.eq n1 Int.one then + e2 + else match mulimm_match e2 with + | mulimm_case1 n2 => + Eop (Ointconst(Int.mul n1 n2)) Enil + | mulimm_case2 n2 t2 => + addimm (Int.mul n1 n2) (mulimm_base n1 t2) + | mulimm_default e2 => + mulimm_base n1 e2 + end. + +(* +Definition mul (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 + | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 + | _, _ => Eop Omul (e1:::e2:::Enil) + end. +*) + +Inductive mul_cases: forall (e1: expr) (e2: expr), Set := + | mul_case1: + forall (n1: int) (t2: expr), + mul_cases (Eop (Ointconst n1) Enil) (t2) + | mul_case2: + forall (t1: expr) (n2: int), + mul_cases (t1) (Eop (Ointconst n2) Enil) + | mul_default: + forall (e1: expr) (e2: expr), + mul_cases e1 e2. + +Definition mul_match_aux (e1: expr) (e2: expr) := + match e2 as z2 return mul_cases e1 z2 with + | Eop (Ointconst n2) Enil => + mul_case2 e1 n2 + | e2 => + mul_default e1 e2 + end. + +Definition mul_match (e1: expr) (e2: expr) := + match e1 as z1 return mul_cases z1 e2 with + | Eop (Ointconst n1) Enil => + mul_case1 n1 e2 + | e1 => + mul_match_aux e1 e2 + end. + +Definition mul (e1: expr) (e2: expr) := + match mul_match e1 e2 with + | mul_case1 n1 t2 => + mulimm n1 t2 + | mul_case2 t1 n2 => + mulimm n2 t1 + | mul_default e1 e2 => + Eop Omul (e1:::e2:::Enil) + end. + +(** ** Integer division and modulus *) + +Definition mod_aux (divop: operation) (e1 e2: expr) := + Elet e1 + (Elet (lift e2) + (Eop Osub (Eletvar 1 ::: + Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: + Eletvar 0 ::: + Enil) ::: + Enil))). + +Inductive divu_cases: forall (e2: expr), Set := + | divu_case1: + forall (n2: int), + divu_cases (Eop (Ointconst n2) Enil) + | divu_default: + forall (e2: expr), + divu_cases e2. + +Definition divu_match (e2: expr) := + match e2 as z1 return divu_cases z1 with + | Eop (Ointconst n2) Enil => + divu_case1 n2 + | e2 => + divu_default e2 + end. + +Definition divu (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => + match Int.is_power2 n2 with + | Some l2 => shruimm e1 l2 + | None => Eop Odivu (e1:::e2:::Enil) + end + | divu_default e2 => + Eop Odivu (e1:::e2:::Enil) + end. + +Definition modu (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => + match Int.is_power2 n2 with + | Some l2 => Eop (Oandimm (Int.sub n2 Int.one)) (e1:::Enil) + | None => mod_aux Odivu e1 e2 + end + | divu_default e2 => + mod_aux Odivu e1 e2 + end. + +Definition divs (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => + match Int.is_power2 n2 with + | Some l2 => if Int.ltu l2 (Int.repr 31) + then Eop (Oshrximm l2) (e1:::Enil) + else Eop Odiv (e1:::e2:::Enil) + | None => Eop Odiv (e1:::e2:::Enil) + end + | divu_default e2 => + Eop Odiv (e1:::e2:::Enil) + end. + +Definition mods := mod_aux Odiv. (* could be improved *) + + +(** ** Bitwise and, or, xor *) + +(* +Definition and (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil) + | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil) + | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil) + | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil) + | _, _ => Eop Oand (e1:::e2:::Enil) + end. +*) + +Inductive and_cases: forall (e1: expr) (e2: expr), Set := + | and_case1: + forall s t1 t2, + and_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | and_case2: + forall t1 s t2, + and_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | and_case3: + forall s t1 t2, + and_cases (Eop (Onotshift s) (t1:::Enil)) (t2) + | and_case4: + forall t1 s t2, + and_cases (t1) (Eop (Onotshift s) (t2:::Enil)) + | and_case5: + forall t1 t2, + and_cases (Eop Onot (t1:::Enil)) (t2) + | and_case6: + forall t1 t2, + and_cases (t1) (Eop Onot (t2:::Enil)) + | and_default: + forall (e1: expr) (e2: expr), + and_cases e1 e2. + +Definition and_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return and_cases z1 z2 with + | Eop (Oshift s) (t1:::Enil), t2 => + and_case1 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + and_case2 t1 s t2 + | Eop (Onotshift s) (t1:::Enil), t2 => + and_case3 s t1 t2 + | t1, Eop (Onotshift s) (t2:::Enil) => + and_case4 t1 s t2 + | Eop Onot (t1:::Enil), t2 => + and_case5 t1 t2 + | t1, Eop Onot (t2:::Enil) => + and_case6 t1 t2 + | e1, e2 => + and_default e1 e2 + end. + +Definition and (e1: expr) (e2: expr) := + match and_match e1 e2 with + | and_case1 s t1 t2 => + Eop (Oandshift s) (t2:::t1:::Enil) + | and_case2 t1 s t2 => + Eop (Oandshift s) (t1:::t2:::Enil) + | and_case3 s t1 t2 => + Eop (Obicshift s) (t2:::t1:::Enil) + | and_case4 t1 s t2 => + Eop (Obicshift s) (t1:::t2:::Enil) + | and_case5 t1 t2 => + Eop Obic (t2:::t1:::Enil) + | and_case6 t1 t2 => + Eop Obic (t1:::t2:::Enil) + | and_default e1 e2 => + Eop Oand (e1:::e2:::Enil) + end. + +Definition same_expr_pure (e1 e2: expr) := + match e1, e2 with + | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false + | _, _ => false + end. + +(* +Definition or (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Oshift (Olsl n1) (t1:::Enil), Eop (Oshift (Olsr n2) (t2:::Enil)) => ... + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oor (e1:::e2:::Enil) + end. +*) + +(* TODO: symmetric of first case *) + +Inductive or_cases: forall (e1: expr) (e2: expr), Set := + | or_case1: + forall n1 t1 n2 t2, + or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil)) + | or_case2: + forall s t1 t2, + or_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | or_case3: + forall t1 s t2, + or_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | or_default: + forall (e1: expr) (e2: expr), + or_cases e1 e2. + +Definition or_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return or_cases z1 z2 with + | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => + or_case1 n1 t1 n2 t2 + | Eop (Oshift s) (t1:::Enil), t2 => + or_case2 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + or_case3 t1 s t2 + | e1, e2 => + or_default e1 e2 + end. + +Definition or (e1: expr) (e2: expr) := + match or_match e1 e2 with + | or_case1 n1 t1 n2 t2 => + if Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n2)) (t1:::Enil) + else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) + | or_case2 s t1 t2 => + Eop (Oorshift s) (t2:::t1:::Enil) + | or_case3 t1 s t2 => + Eop (Oorshift s) (t1:::t2:::Enil) + | or_default e1 e2 => + Eop Oor (e1:::e2:::Enil) + end. + +(* +Definition xor (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oxor (e1:::e2:::Enil) + end. +*) + +Inductive xor_cases: forall (e1: expr) (e2: expr), Set := + | xor_case1: + forall s t1 t2, + xor_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | xor_case2: + forall t1 s t2, + xor_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | xor_default: + forall (e1: expr) (e2: expr), + xor_cases e1 e2. + +Definition xor_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return xor_cases z1 z2 with + | Eop (Oshift s) (t1:::Enil), t2 => + xor_case1 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + xor_case2 t1 s t2 + | e1, e2 => + xor_default e1 e2 + end. + +Definition xor (e1: expr) (e2: expr) := + match xor_match e1 e2 with + | xor_case1 s t1 t2 => + Eop (Oxorshift s) (t2:::t1:::Enil) + | xor_case2 t1 s t2 => + Eop (Oxorshift s) (t1:::t2:::Enil) + | xor_default e1 e2 => + Eop Oxor (e1:::e2:::Enil) + end. + +(** ** General shifts *) + +Inductive shift_cases: forall (e1: expr), Set := + | shift_case1: + forall (n2: int), + shift_cases (Eop (Ointconst n2) Enil) + | shift_default: + forall (e1: expr), + shift_cases e1. + +Definition shift_match (e1: expr) := + match e1 as z1 return shift_cases z1 with + | Eop (Ointconst n2) Enil => + shift_case1 n2 + | e1 => + shift_default e1 + end. + +Definition shl (e1: expr) (e2: expr) := + match shift_match e2 with + | shift_case1 n2 => + shlimm e1 n2 + | shift_default e2 => + Eop Oshl (e1:::e2:::Enil) + end. + +Definition shru (e1: expr) (e2: expr) := + match shift_match e2 with + | shift_case1 n2 => + shruimm e1 n2 + | shift_default e2 => + Eop Oshru (e1:::e2:::Enil) + end. + +Definition shr (e1: expr) (e2: expr) := + match shift_match e2 with + | shift_case1 n2 => + shrimm e1 n2 + | shift_default e2 => + Eop Oshr (e1:::e2:::Enil) + end. + +(** ** Truncations and sign extensions *) + +Inductive cast8signed_cases: forall (e1: expr), Set := + | cast8signed_case1: + forall (e2: expr), + cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) + | cast8signed_default: + forall (e1: expr), + cast8signed_cases e1. + +Definition cast8signed_match (e1: expr) := + match e1 as z1 return cast8signed_cases z1 with + | Eop Ocast8signed (e2 ::: Enil) => + cast8signed_case1 e2 + | e1 => + cast8signed_default e1 + end. + +Definition cast8signed (e: expr) := + match cast8signed_match e with + | cast8signed_case1 e1 => e + | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) + end. + +Inductive cast8unsigned_cases: forall (e1: expr), Set := + | cast8unsigned_case1: + forall (e2: expr), + cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) + | cast8unsigned_default: + forall (e1: expr), + cast8unsigned_cases e1. + +Definition cast8unsigned_match (e1: expr) := + match e1 as z1 return cast8unsigned_cases z1 with + | Eop Ocast8unsigned (e2 ::: Enil) => + cast8unsigned_case1 e2 + | e1 => + cast8unsigned_default e1 + end. + +Definition cast8unsigned (e: expr) := + match cast8unsigned_match e with + | cast8unsigned_case1 e1 => e + | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) + end. + +Inductive cast16signed_cases: forall (e1: expr), Set := + | cast16signed_case1: + forall (e2: expr), + cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) + | cast16signed_default: + forall (e1: expr), + cast16signed_cases e1. + +Definition cast16signed_match (e1: expr) := + match e1 as z1 return cast16signed_cases z1 with + | Eop Ocast16signed (e2 ::: Enil) => + cast16signed_case1 e2 + | e1 => + cast16signed_default e1 + end. + +Definition cast16signed (e: expr) := + match cast16signed_match e with + | cast16signed_case1 e1 => e + | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) + end. + +Inductive cast16unsigned_cases: forall (e1: expr), Set := + | cast16unsigned_case1: + forall (e2: expr), + cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) + | cast16unsigned_default: + forall (e1: expr), + cast16unsigned_cases e1. + +Definition cast16unsigned_match (e1: expr) := + match e1 as z1 return cast16unsigned_cases z1 with + | Eop Ocast16unsigned (e2 ::: Enil) => + cast16unsigned_case1 e2 + | e1 => + cast16unsigned_default e1 + end. + +Definition cast16unsigned (e: expr) := + match cast16unsigned_match e with + | cast16unsigned_case1 e1 => e + | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) + end. + +Inductive singleoffloat_cases: forall (e1: expr), Set := + | singleoffloat_case1: + forall (e2: expr), + singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) + | singleoffloat_default: + forall (e1: expr), + singleoffloat_cases e1. + +Definition singleoffloat_match (e1: expr) := + match e1 as z1 return singleoffloat_cases z1 with + | Eop Osingleoffloat (e2 ::: Enil) => + singleoffloat_case1 e2 + | e1 => + singleoffloat_default e1 + end. + +Definition singleoffloat (e: expr) := + match singleoffloat_match e with + | singleoffloat_case1 e1 => e + | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) + end. + +(** ** Comparisons *) + +(* +Definition comp (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) + | t1, Eop (Ointconst n2) Enil => Eop (Ocmp (Ccompimm c n1)) (t1:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) + | _, _ => Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) + end. +*) + +Inductive comp_cases: forall (e1: expr) (e2: expr), Set := + | comp_case1: + forall n1 t2, + comp_cases (Eop (Ointconst n1) Enil) (t2) + | comp_case2: + forall t1 n2, + comp_cases (t1) (Eop (Ointconst n2) Enil) + | comp_case3: + forall s t1 t2, + comp_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | comp_case4: + forall t1 s t2, + comp_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | comp_default: + forall (e1: expr) (e2: expr), + comp_cases e1 e2. + +Definition comp_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return comp_cases z1 z2 with + | Eop (Ointconst n1) Enil, t2 => + comp_case1 n1 t2 + | t1, Eop (Ointconst n2) Enil => + comp_case2 t1 n2 + | Eop (Oshift s) (t1:::Enil), t2 => + comp_case3 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + comp_case4 t1 s t2 + | e1, e2 => + comp_default e1 e2 + end. + +Definition comp (c: comparison) (e1: expr) (e2: expr) := + match comp_match e1 e2 with + | comp_case1 n1 t2 => + Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) + | comp_case2 t1 n2 => + Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) + | comp_case3 s t1 t2 => + Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) + | comp_case4 t1 s t2 => + Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) + | comp_default e1 e2 => + Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) + end. + +Definition compu (c: comparison) (e1: expr) (e2: expr) := + match comp_match e1 e2 with + | comp_case1 n1 t2 => + Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) + | comp_case2 t1 n2 => + Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) + | comp_case3 s t1 t2 => + Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) + | comp_case4 t1 s t2 => + Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) + | comp_default e1 e2 => + Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) + end. + +Definition compf (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). + +(** ** Conditional expressions *) + +Fixpoint negate_condexpr (e: condexpr): condexpr := + match e with + | CEtrue => CEfalse + | CEfalse => CEtrue + | CEcond c el => CEcond (negate_condition c) el + | CEcondition e1 e2 e3 => + CEcondition e1 (negate_condexpr e2) (negate_condexpr e3) + end. + + +Definition is_compare_neq_zero (c: condition) : bool := + match c with + | Ccompimm Cne n => Int.eq n Int.zero + | Ccompuimm Cne n => Int.eq n Int.zero + | _ => false + end. + +Definition is_compare_eq_zero (c: condition) : bool := + match c with + | Ccompimm Ceq n => Int.eq n Int.zero + | Ccompuimm Ceq n => Int.eq n Int.zero + | _ => false + end. + +Fixpoint condexpr_of_expr (e: expr) : condexpr := + match e with + | Eop (Ointconst n) Enil => + if Int.eq n Int.zero then CEfalse else CEtrue + | Eop (Ocmp c) (e1 ::: Enil) => + if is_compare_neq_zero c then + condexpr_of_expr e1 + else if is_compare_eq_zero c then + negate_condexpr (condexpr_of_expr e1) + else + CEcond c (e1 ::: Enil) + | Eop (Ocmp c) el => + CEcond c el + | Econdition ce e1 e2 => + CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2) + | _ => + CEcond (Ccompimm Cne Int.zero) (e:::Enil) + end. + +(** ** Recognition of addressing modes for load and store operations *) + +(* +Definition addressing (e: expr) := + match e with + | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) + | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) + | Eop (Oaddshift s) (e1:::e2:::Enil) => (Aindexed2shift s, e1:::e2:::Enil) + | Eop Oadd (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) + | _ => (Aindexed Int.zero, e:::Enil) + end. +*) + +Inductive addressing_cases: forall (e: expr), Set := + | addressing_case2: + forall n, + addressing_cases (Eop (Oaddrstack n) Enil) + | addressing_case3: + forall n e1, + addressing_cases (Eop (Oaddimm n) (e1:::Enil)) + | addressing_case4: + forall s e1 e2, + addressing_cases (Eop (Oaddshift s) (e1:::e2:::Enil)) + | addressing_case5: + forall e1 e2, + addressing_cases (Eop Oadd (e1:::e2:::Enil)) + | addressing_default: + forall (e: expr), + addressing_cases e. + +Definition addressing_match (e: expr) := + match e as z1 return addressing_cases z1 with + | Eop (Oaddrstack n) Enil => + addressing_case2 n + | Eop (Oaddimm n) (e1:::Enil) => + addressing_case3 n e1 + | Eop (Oaddshift s) (e1:::e2:::Enil) => + addressing_case4 s e1 e2 + | Eop Oadd (e1:::e2:::Enil) => + addressing_case5 e1 e2 + | e => + addressing_default e + end. + +(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes + for floating-point accesses, since these are not supported + by the hardware and emulated inefficiently in [ARMgen]. *) + +Definition is_float_addressing (chunk: memory_chunk): bool := + match chunk with + | Mfloat32 => true + | Mfloat64 => true + | _ => false + end. + +Definition addressing (chunk: memory_chunk) (e: expr) := + match addressing_match e with + | addressing_case2 n => + (Ainstack n, Enil) + | addressing_case3 n e1 => + (Aindexed n, e1:::Enil) + | addressing_case4 s e1 e2 => + if is_float_addressing chunk + then (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) + else (Aindexed2shift s, e1:::e2:::Enil) + | addressing_case5 e1 e2 => + if is_float_addressing chunk + then (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) + else (Aindexed2, e1:::e2:::Enil) + | addressing_default e => + (Aindexed Int.zero, e:::Enil) + end. + +Definition load (chunk: memory_chunk) (e1: expr) := + match addressing chunk e1 with + | (mode, args) => Eload chunk mode args + end. + +Definition store (chunk: memory_chunk) (e1 e2: expr) := + match addressing chunk e1 with + | (mode, args) => Sstore chunk mode args e2 + end. + +(** * Translation from Cminor to CminorSel *) + +(** Instruction selection for operator applications *) + +Definition sel_constant (cst: Cminor.constant) : expr := + match cst with + | Cminor.Ointconst n => Eop (Ointconst n) Enil + | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil + | Cminor.Oaddrsymbol id ofs => Eop (Oaddrsymbol id ofs) Enil + | Cminor.Oaddrstack ofs => Eop (Oaddrstack ofs) Enil + end. + +Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := + match op with + | Cminor.Ocast8unsigned => cast8unsigned arg + | Cminor.Ocast8signed => cast8signed arg + | Cminor.Ocast16unsigned => cast16unsigned arg + | Cminor.Ocast16signed => cast16signed arg + | Cminor.Onegint => Eop (Orsubimm Int.zero) (arg ::: Enil) + | Cminor.Onotbool => notbool arg + | Cminor.Onotint => notint arg + | Cminor.Onegf => Eop Onegf (arg ::: Enil) + | Cminor.Oabsf => Eop Oabsf (arg ::: Enil) + | Cminor.Osingleoffloat => singleoffloat arg + | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil) + | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil) + | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil) + | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil) + end. + +Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := + match op with + | Cminor.Oadd => add arg1 arg2 + | Cminor.Osub => sub arg1 arg2 + | Cminor.Omul => mul arg1 arg2 + | Cminor.Odiv => divs arg1 arg2 + | Cminor.Odivu => divu arg1 arg2 + | Cminor.Omod => mods arg1 arg2 + | Cminor.Omodu => modu arg1 arg2 + | Cminor.Oand => and arg1 arg2 + | Cminor.Oor => or arg1 arg2 + | Cminor.Oxor => xor arg1 arg2 + | Cminor.Oshl => shl arg1 arg2 + | Cminor.Oshr => shr arg1 arg2 + | Cminor.Oshru => shru arg1 arg2 + | Cminor.Oaddf => Eop Oaddf (arg1 ::: arg2 ::: Enil) + | Cminor.Osubf => Eop Osubf (arg1 ::: arg2 ::: Enil) + | Cminor.Omulf => Eop Omulf (arg1 ::: arg2 ::: Enil) + | Cminor.Odivf => Eop Odivf (arg1 ::: arg2 ::: Enil) + | Cminor.Ocmp c => comp c arg1 arg2 + | Cminor.Ocmpu c => compu c arg1 arg2 + | Cminor.Ocmpf c => compf c arg1 arg2 + end. + +(** Conversion from Cminor expression to Cminorsel expressions *) + +Fixpoint sel_expr (a: Cminor.expr) : expr := + match a with + | Cminor.Evar id => Evar id + | Cminor.Econst cst => sel_constant cst + | Cminor.Eunop op arg => sel_unop op (sel_expr arg) + | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2) + | Cminor.Eload chunk addr => load chunk (sel_expr addr) + | Cminor.Econdition cond ifso ifnot => + Econdition (condexpr_of_expr (sel_expr cond)) + (sel_expr ifso) (sel_expr ifnot) + end. + +Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := + match al with + | nil => Enil + | a :: bl => Econs (sel_expr a) (sel_exprlist bl) + end. + +(** Conversion from Cminor statements to Cminorsel statements. *) + +Fixpoint sel_stmt (s: Cminor.stmt) : stmt := + match s with + | Cminor.Sskip => Sskip + | Cminor.Sassign id e => Sassign id (sel_expr e) + | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) + | Cminor.Scall optid sg fn args => + Scall optid sg (sel_expr fn) (sel_exprlist args) + | Cminor.Stailcall sg fn args => + Stailcall sg (sel_expr fn) (sel_exprlist args) + | Cminor.Salloc id b => Salloc id (sel_expr b) + | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) + | Cminor.Sifthenelse e ifso ifnot => + Sifthenelse (condexpr_of_expr (sel_expr e)) + (sel_stmt ifso) (sel_stmt ifnot) + | Cminor.Sloop body => Sloop (sel_stmt body) + | Cminor.Sblock body => Sblock (sel_stmt body) + | Cminor.Sexit n => Sexit n + | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl + | Cminor.Sreturn None => Sreturn None + | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) + | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body) + | Cminor.Sgoto lbl => Sgoto lbl + end. + +(** Conversion of functions and programs. *) + +Definition sel_function (f: Cminor.function) : function := + mkfunction + f.(Cminor.fn_sig) + f.(Cminor.fn_params) + f.(Cminor.fn_vars) + f.(Cminor.fn_stackspace) + (sel_stmt f.(Cminor.fn_body)). + +Definition sel_fundef (f: Cminor.fundef) : fundef := + transf_fundef sel_function f. + +Definition sel_program (p: Cminor.program) : program := + transform_program sel_fundef p. + + + |