diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-06-05 09:03:10 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-06-05 09:03:10 +0000 |
commit | 02d3c953c79af64a542ff659822fe003c0c532f3 (patch) | |
tree | df69cc24530341e9f37773ee8afdd0297853aac6 /backend/Cmconstr.v | |
parent | a7010ea01d63c73892ba14fd1d5170f4c2b28f98 (diff) | |
download | compcert-02d3c953c79af64a542ff659822fe003c0c532f3.tar.gz compcert-02d3c953c79af64a542ff659822fe003c0c532f3.zip |
Optimisation des casts (idempotence, etc)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@33 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Cmconstr.v')
-rw-r--r-- | backend/Cmconstr.v | 86 |
1 files changed, 73 insertions, 13 deletions
diff --git a/backend/Cmconstr.v b/backend/Cmconstr.v index da642f8f..e6168d1a 100644 --- a/backend/Cmconstr.v +++ b/backend/Cmconstr.v @@ -187,19 +187,6 @@ Fixpoint notbool (e: expr) {struct e} : expr := notbool_base e end. -(** ** Truncations and sign extensions *) - -Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil). - -Definition cast8unsigned (e: expr) := - Eop (Orolm Int.zero (Int.repr 255)) (e ::: Enil). -Definition cast16signed (e: expr) := - Eop Ocast16signed (e ::: Enil). -Definition cast16unsigned (e: expr) := - Eop (Orolm Int.zero (Int.repr 65535)) (e ::: Enil). -Definition singleoffloat (e: expr) := - Eop Osingleoffloat (e ::: Enil). - (** ** Integer addition and pointer addition *) (* @@ -806,6 +793,79 @@ Definition subf (e1: expr) (e2: expr) := Definition mulf (e1 e2: expr) := Eop Omulf (e1:::e2:::Enil). Definition divf (e1 e2: expr) := Eop Odivf (e1:::e2:::Enil). +(** ** Truncations and sign extensions *) + +Definition cast8unsigned (e: expr) := + rolm e Int.zero (Int.repr 255). +Definition cast16unsigned (e: expr) := + rolm e Int.zero (Int.repr 65535). + +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 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 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 and conditional expressions *) Definition cmp (c: comparison) (e1 e2: expr) := |