From 12421d717405aa7964e437fc1167a23699b61ecc Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Dec 2008 12:47:56 +0000 Subject: Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext. lib/Integers.v: added more properties for ARM port. lib/Coqlib.v: added more properties for division and powers of 2. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@928 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Mem.v | 20 +++++++-------- common/Values.v | 80 ++++++++++++++++++++++++++++----------------------------- 2 files changed, 50 insertions(+), 50 deletions(-) (limited to 'common') diff --git a/common/Mem.v b/common/Mem.v index 35d93ed7..3db2ceba 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1932,12 +1932,12 @@ Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop := | val_content_inject_8: forall chunk n1 n2, chunk = Mint8unsigned \/ chunk = Mint8signed -> - Int.cast8unsigned n1 = Int.cast8unsigned n2 -> + Int.zero_ext 8 n1 = Int.zero_ext 8 n2 -> val_content_inject f chunk (Vint n1) (Vint n2) | val_content_inject_16: forall chunk n1 n2, chunk = Mint16unsigned \/ chunk = Mint16signed -> - Int.cast16unsigned n1 = Int.cast16unsigned n2 -> + Int.zero_ext 16 n1 = Int.zero_ext 16 n2 -> val_content_inject f chunk (Vint n1) (Vint n2) | val_content_inject_32: forall f1 f2, @@ -1957,20 +1957,20 @@ Proof. elim H1; intro; subst chunk; destruct chunk'; simpl in H0; try discriminate; simpl. - replace (Int.cast8signed n1) with (Int.cast8signed n2). - constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto. + replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2). + constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. rewrite H2. constructor. - replace (Int.cast8signed n1) with (Int.cast8signed n2). - constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto. + replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2). + constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. rewrite H2. constructor. elim H1; intro; subst chunk; destruct chunk'; simpl in H0; try discriminate; simpl. - replace (Int.cast16signed n1) with (Int.cast16signed n2). - constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto. + replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2). + constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. rewrite H2. constructor. - replace (Int.cast16signed n1) with (Int.cast16signed n2). - constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto. + replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2). + constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto. rewrite H2. constructor. destruct chunk'; simpl in H0; try discriminate; simpl. diff --git a/common/Values.v b/common/Values.v index 19772446..27d4f50c 100644 --- a/common/Values.v +++ b/common/Values.v @@ -150,27 +150,15 @@ Definition notbool (v: val) : val := | _ => Vundef end. -Definition cast8signed (v: val) : val := +Definition zero_ext (nbits: Z) (v: val) : val := match v with - | Vint n => Vint(Int.cast8signed n) + | Vint n => Vint(Int.zero_ext nbits n) | _ => Vundef end. -Definition cast8unsigned (v: val) : val := +Definition sign_ext (nbits: Z) (v: val) : val := match v with - | Vint n => Vint(Int.cast8unsigned n) - | _ => Vundef - end. - -Definition cast16signed (v: val) : val := - match v with - | Vint n => Vint(Int.cast16signed n) - | _ => Vundef - end. - -Definition cast16unsigned (v: val) : val := - match v with - | Vint n => Vint(Int.cast16unsigned n) + | Vint n => Vint(Int.sign_ext nbits n) | _ => Vundef end. @@ -300,6 +288,15 @@ Definition rolm (v: val) (amount mask: int): val := | _ => Vundef end. +Definition ror (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) + then Vint(Int.ror n1 n2) + else Vundef + | _, _ => Vundef + end. + Definition addf (v1 v2: val): val := match v1, v2 with | Vfloat f1, Vfloat f2 => Vfloat(Float.add f1 f2) @@ -377,10 +374,10 @@ Definition cmpf (c: comparison) (v1 v2: val): val := Definition load_result (chunk: memory_chunk) (v: val) := match chunk, v with - | Mint8signed, Vint n => Vint (Int.cast8signed n) - | Mint8unsigned, Vint n => Vint (Int.cast8unsigned n) - | Mint16signed, Vint n => Vint (Int.cast16signed n) - | Mint16unsigned, Vint n => Vint (Int.cast16unsigned n) + | Mint8signed, Vint n => Vint (Int.sign_ext 8 n) + | Mint8unsigned, Vint n => Vint (Int.zero_ext 8 n) + | Mint16signed, Vint n => Vint (Int.sign_ext 16 n) + | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n) | Mint32, Vint n => Vint n | Mint32, Vptr b ofs => Vptr b ofs | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f) @@ -391,15 +388,17 @@ Definition load_result (chunk: memory_chunk) (v: val) := (** Theorems on arithmetic operations. *) Theorem cast8unsigned_and: - forall x, cast8unsigned x = and x (Vint(Int.repr 255)). + forall x, zero_ext 8 x = and x (Vint(Int.repr 255)). Proof. - destruct x; simpl; auto. decEq. apply Int.cast8unsigned_and. + destruct x; simpl; auto. decEq. + change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto. Qed. Theorem cast16unsigned_and: - forall x, cast16unsigned x = and x (Vint(Int.repr 65535)). + forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)). Proof. - destruct x; simpl; auto. decEq. apply Int.cast16unsigned_and. + destruct x; simpl; auto. decEq. + change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto. Qed. Theorem istrue_not_isfalse: @@ -532,6 +531,12 @@ Proof. destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto. Qed. +Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y). +Proof. + intros. unfold sub, add. + destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto. +Qed. + Theorem sub_add_l: forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i). Proof. @@ -823,6 +828,13 @@ Proof. apply notbool_idem2. Qed. +Theorem negate_cmpf_ne: + forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2. +Proof. + destruct v1; destruct v2; simpl; auto. + rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto. +Qed. + Lemma or_of_bool: forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2). Proof. @@ -940,26 +952,14 @@ Proof. intros. inv H. auto. destruct chunk; simpl; auto. Qed. -Lemma cast8signed_lessdef: - forall v1 v2, lessdef v1 v2 -> lessdef (cast8signed v1) (cast8signed v2). -Proof. - intros; inv H; simpl; auto. -Qed. - -Lemma cast8unsigned_lessdef: - forall v1 v2, lessdef v1 v2 -> lessdef (cast8unsigned v1) (cast8unsigned v2). -Proof. - intros; inv H; simpl; auto. -Qed. - -Lemma cast16signed_lessdef: - forall v1 v2, lessdef v1 v2 -> lessdef (cast16signed v1) (cast16signed v2). +Lemma zero_ext_lessdef: + forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2). Proof. intros; inv H; simpl; auto. Qed. -Lemma cast16unsigned_lessdef: - forall v1 v2, lessdef v1 v2 -> lessdef (cast16unsigned v1) (cast16unsigned v2). +Lemma sign_ext_lessdef: + forall n v1 v2, lessdef v1 v2 -> lessdef (sign_ext n v1) (sign_ext n v2). Proof. intros; inv H; simpl; auto. Qed. -- cgit