From ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 19 Nov 2009 13:32:09 +0000 Subject: Revised lib/Integers.v to make it parametric w.r.t. word size. Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr (Z_of_nat wordsize)". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Op.v | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'powerpc/Op.v') diff --git a/powerpc/Op.v b/powerpc/Op.v index 27e12c2..c6e196f 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -224,15 +224,15 @@ Definition eval_operation | Onor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.or n1 n2))) | Onxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.xor n1 n2))) | Oshl, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None | Oshr, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None | Oshrimm n, Vint n1 :: nil => - if Int.ltu n (Int.repr 32) then Some (Vint (Int.shr n1 n)) else None + if Int.ltu n Int.iwordsize then Some (Vint (Int.shr n1 n)) else None | Oshrximm n, Vint n1 :: nil => - if Int.ltu n (Int.repr 32) then Some (Vint (Int.shrx n1 n)) else None + if Int.ltu n Int.iwordsize then Some (Vint (Int.shrx n1 n)) else None | Oshru, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None | Orolm amount mask, Vint n1 :: nil => Some (Vint (Int.rolm n1 amount mask)) | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) @@ -522,15 +522,15 @@ Proof. injection H0; intro; subst v; exact I. destruct (Int.eq i0 Int.zero). discriminate. injection H0; intro; subst v; exact I. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i (Int.repr 32)). + destruct (Int.ltu i Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i (Int.repr 32)). + destruct (Int.ltu i Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. destruct v0; exact I. destruct (eval_condition c vl). @@ -694,11 +694,11 @@ Proof. unfold eq_block in H. destruct (zeq b b0); congruence. destruct (Int.eq i0 Int.zero); congruence. destruct (Int.eq i0 Int.zero); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. - destruct (Int.ltu i (Int.repr 32)); congruence. - destruct (Int.ltu i (Int.repr 32)); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. + destruct (Int.ltu i Int.iwordsize); congruence. + destruct (Int.ltu i Int.iwordsize); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. caseEq (eval_condition c vl); intros; rewrite H0 in H. replace v with (Val.of_bool b). eapply eval_condition_weaken; eauto. @@ -797,11 +797,11 @@ Proof. destruct (eq_block b b0); inv H0. TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. caseEq (eval_condition c vl1); intros. rewrite H1 in H0. rewrite (eval_condition_lessdef c H H1). -- cgit v1.2.3