From 02d3c953c79af64a542ff659822fe003c0c532f3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 5 Jun 2006 09:03:10 +0000 Subject: Optimisation des casts (idempotence, etc) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@33 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cmconstr.v | 86 +++++++++++++++++++++++++++++++++++++++++-------- backend/Cmconstrproof.v | 86 +++++++++++++++++++++++++++---------------------- 2 files changed, 121 insertions(+), 51 deletions(-) (limited to 'backend') 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) := diff --git a/backend/Cmconstrproof.v b/backend/Cmconstrproof.v index b7469be8..f27fa73c 100644 --- a/backend/Cmconstrproof.v +++ b/backend/Cmconstrproof.v @@ -329,44 +329,6 @@ Proof. destruct v1; eauto. Qed. -Theorem eval_cast8signed: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast8signed a) e2 m2 (Vint (Int.cast8signed x)). -Proof. TrivialOp cast8signed. Qed. - -Theorem eval_cast8unsigned: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast8unsigned a) e2 m2 (Vint (Int.cast8unsigned x)). -Proof. - TrivialOp cast8unsigned. simpl. - rewrite Int.rolm_zero. rewrite Int.cast8unsigned_and. auto. -Qed. - -Theorem eval_cast16signed: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast16signed a) e2 m2 (Vint (Int.cast16signed x)). -Proof. TrivialOp cast16signed. Qed. - -Theorem eval_cast16unsigned: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> - eval_expr ge sp le e1 m1 (cast16unsigned a) e2 m2 (Vint (Int.cast16unsigned x)). -Proof. - TrivialOp cast16unsigned. simpl. - rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto. -Qed. - -Theorem eval_singleoffloat: - forall sp le e1 m1 a e2 m2 x, - eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> - eval_expr ge sp le e1 m1 (singleoffloat a) e2 m2 (Vfloat (Float.singleoffloat x)). -Proof. - TrivialOp singleoffloat. -Qed. - Theorem eval_addimm: forall sp le e1 m1 n a e2 m2 x, eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> @@ -929,6 +891,54 @@ Theorem eval_divf: eval_expr ge sp le e1 m1 (divf a b) e3 m3 (Vfloat (Float.div x y)). Proof. TrivialOp divf. Qed. +Theorem eval_cast8signed: + forall sp le e1 m1 a e2 m2 x, + eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (cast8signed a) e2 m2 (Vint (Int.cast8signed x)). +Proof. + intros until x; unfold cast8signed; case (cast8signed_match a); intros. + InvEval H. FuncInv. EvalOp. subst x. rewrite Int.cast8_signed_idem. reflexivity. + EvalOp. +Qed. + +Theorem eval_cast8unsigned: + forall sp le e1 m1 a e2 m2 x, + eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (cast8unsigned a) e2 m2 (Vint (Int.cast8unsigned x)). +Proof. + intros. unfold cast8unsigned. rewrite Int.cast8unsigned_and. + rewrite <- Int.rolm_zero. eapply eval_rolm; eauto. +Qed. + +Theorem eval_cast16signed: + forall sp le e1 m1 a e2 m2 x, + eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (cast16signed a) e2 m2 (Vint (Int.cast16signed x)). +Proof. + intros until x; unfold cast16signed; case (cast16signed_match a); intros. + InvEval H. FuncInv. EvalOp. subst x. rewrite Int.cast16_signed_idem. reflexivity. + EvalOp. +Qed. + +Theorem eval_cast16unsigned: + forall sp le e1 m1 a e2 m2 x, + eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> + eval_expr ge sp le e1 m1 (cast16unsigned a) e2 m2 (Vint (Int.cast16unsigned x)). +Proof. + intros. unfold cast16unsigned. rewrite Int.cast16unsigned_and. + rewrite <- Int.rolm_zero. eapply eval_rolm; eauto. +Qed. + +Theorem eval_singleoffloat: + forall sp le e1 m1 a e2 m2 x, + eval_expr ge sp le e1 m1 a e2 m2 (Vfloat x) -> + eval_expr ge sp le e1 m1 (singleoffloat a) e2 m2 (Vfloat (Float.singleoffloat x)). +Proof. + intros until x; unfold singleoffloat; case (singleoffloat_match a); intros. + InvEval H. FuncInv. EvalOp. subst x. rewrite Float.singleoffloat_idem. reflexivity. + EvalOp. +Qed. + Theorem eval_cmp: forall sp le c e1 m1 a e2 m2 x b e3 m3 y, eval_expr ge sp le e1 m1 a e2 m2 (Vint x) -> -- cgit