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/Cmconstrproof.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/Cmconstrproof.v')
-rw-r--r-- | backend/Cmconstrproof.v | 86 |
1 files changed, 48 insertions, 38 deletions
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) -> |