From 76f49ca6af4ffbc77c0ba7965d409c3de04011bd Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 6 Apr 2014 18:32:27 +0000 Subject: Support Onot operator / notl instruction. More constant propagation during selection. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2451 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asm.v | 3 +++ ia32/Asmgen.v | 3 +++ ia32/ConstpropOp.vp | 4 +-- ia32/ConstpropOpproof.v | 2 ++ ia32/Machregs.v | 1 + ia32/NeedOp.v | 2 ++ ia32/Op.v | 5 ++++ ia32/PrintAsm.ml | 2 ++ ia32/SelectOp.vp | 66 ++++++++++++++++++++++++++++++++++++++----------- ia32/SelectOpproof.v | 37 +++++++++++++++++++-------- ia32/ValueAOp.v | 1 + 11 files changed, 100 insertions(+), 26 deletions(-) (limited to 'ia32') diff --git a/ia32/Asm.v b/ia32/Asm.v index 08a1ef4..f03ea75 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -156,6 +156,7 @@ Inductive instruction: Type := | Pxor_r (rd: ireg) (**r [xor] with self = set to zero *) | Pxor_rr (rd: ireg) (r1: ireg) | Pxor_ri (rd: ireg) (n: int) + | Pnot (rd: ireg) | Psal_rcl (rd: ireg) | Psal_ri (rd: ireg) (n: int) | Pshr_rcl (rd: ireg) @@ -573,6 +574,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd rs#r1))) m | Pxor_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd (Vint n)))) m + | Pnot rd => + Next (nextinstr_nf (rs#rd <- (Val.notint rs#rd))) m | Psal_rcl rd => Next (nextinstr_nf (rs#rd <- (Val.shl rs#rd rs#ECX))) m | Psal_ri rd n => diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index fa4112d..f92d72c 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -357,6 +357,9 @@ Definition transl_op | Oxorimm n, a1 :: nil => assertion (mreg_eq a1 res); do r <- ireg_of res; OK (Pxor_ri r n :: k) + | Onot, a1 :: nil => + assertion (mreg_eq a1 res); + do r <- ireg_of res; OK (Pnot r :: k) | Oshl, a1 :: a2 :: nil => assertion (mreg_eq a1 res); assertion (mreg_eq a2 CX); diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index aaf08a1..172f7a4 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -132,8 +132,8 @@ Definition make_orimm (n: int) (r: reg) := else (Oorimm n, r :: nil). Definition make_xorimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) + if Int.eq n Int.zero then (Omove, r :: nil) + else if Int.eq n Int.mone then (Onot, r :: nil) else (Oxorimm n, r :: nil). Definition make_divimm n (r1 r2: reg) := diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index 148a08d..6a83c1a 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -309,6 +309,8 @@ Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto. + predSpec Int.eq Int.eq_spec n Int.mone; intros. + subst n. exists (Val.notint e#r); split; auto. econstructor; split; eauto. auto. Qed. diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 85b561e..da80a6e 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -211,6 +211,7 @@ Definition two_address_op (op: operation) : bool := | Oorimm _ => true | Oxor => true | Oxorimm _ => true + | Onot => true | Oshl => true | Oshlimm _ => true | Oshr => true diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v index 1237473..2c8698f 100644 --- a/ia32/NeedOp.v +++ b/ia32/NeedOp.v @@ -53,6 +53,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oorimm n => op1 (orimm nv n) | Oxor => op2 (bitwise nv) | Oxorimm n => op1 (bitwise nv) + | Onot => op1 (bitwise nv) | Oshl => op2 (default nv) | Oshlimm n => op1 (shlimm nv n) | Oshr => op2 (default nv) @@ -158,6 +159,7 @@ Proof. - apply orimm_sound; auto. - apply xor_sound; auto. - apply xor_sound; auto with na. +- apply notint_sound; auto. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. diff --git a/ia32/Op.v b/ia32/Op.v index 26e6688..5420607 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -90,6 +90,7 @@ Inductive operation : Type := | Oorimm: int -> operation (**r [rd = r1 | n] *) | Oxor: operation (**r [rd = r1 ^ r2] *) | Oxorimm: int -> operation (**r [rd = r1 ^ n] *) + | Onot: operation (**r [rd = ~r1] *) | Oshl: operation (**r [rd = r1 << r2] *) | Oshlimm: int -> operation (**r [rd = r1 << n] *) | Oshr: operation (**r [rd = r1 >> r2] (signed) *) @@ -230,6 +231,7 @@ Definition eval_operation | Oorimm n, v1::nil => Some (Val.or v1 (Vint n)) | Oxor, v1::v2::nil => Some(Val.xor v1 v2) | Oxorimm n, v1::nil => Some (Val.xor v1 (Vint n)) + | Onot, v1::nil => Some(Val.notint v1) | Oshl, v1::v2::nil => Some (Val.shl v1 v2) | Oshlimm n, v1::nil => Some (Val.shl v1 (Vint n)) | Oshr, v1::v2::nil => Some (Val.shr v1 v2) @@ -321,6 +323,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oorimm _ => (Tint :: nil, Tint) | Oxor => (Tint :: Tint :: nil, Tint) | Oxorimm _ => (Tint :: nil, Tint) + | Onot => (Tint :: nil, Tint) | Oshl => (Tint :: Tint :: nil, Tint) | Oshlimm _ => (Tint :: nil, Tint) | Oshr => (Tint :: Tint :: nil, Tint) @@ -407,6 +410,7 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... + destruct v0... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... @@ -835,6 +839,7 @@ Proof. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. + inv H4; simpl; auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index d67fb9e..9a2648a 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -644,6 +644,8 @@ let print_instruction oc = function fprintf oc " xorl %a, %a\n" ireg r1 ireg rd | Pxor_ri(rd, n) -> fprintf oc " xorl $%a, %a\n" coqint n ireg rd + | Pnot(rd) -> + fprintf oc " notl %a\n" ireg rd | Psal_rcl(rd) -> fprintf oc " sall %%cl, %a\n" ireg rd | Psal_ri(rd, n) -> diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index e80c3f3..5f47df2 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -68,7 +68,12 @@ Definition addrstack (ofs: int) := (** ** Integer logical negation *) -Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil). +Nondetfunction notint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil + | Eop (Oxorimm n) (e1 ::: Enil) => Eop (Oxorimm (Int.not n)) (e1 ::: Enil) + | _ => Eop Onot (e ::: Enil) + end. (** ** Integer addition and pointer addition *) @@ -110,6 +115,14 @@ Nondetfunction add (e1: expr) (e2: expr) := Eop (Olea (Aindexed2 Int.zero)) (e1:::e2:::Enil) end. +(** ** Opposite *) + +Nondetfunction negint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil + | _ => Eop Oneg (e ::: Enil) + end. + (** ** Integer and pointer subtraction *) Nondetfunction sub (e1: expr) (e2: expr) := @@ -125,8 +138,6 @@ Nondetfunction sub (e1: expr) (e2: expr) := Eop Osub (e1:::e2:::Enil) end. -Definition negint (e: expr) := Eop Oneg (e ::: Enil). - (** ** Immediate shifts *) Definition shift_is_scale (n: int) : bool := @@ -275,6 +286,8 @@ Nondetfunction xorimm (n1: int) (e2: expr) := Eop (Ointconst (Int.xor n1 n2)) Enil | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil) + | Eop Onot (t2:::Enil) => + Eop (Oxorimm (Int.not n1)) (t2:::Enil) | _ => Eop (Oxorimm n1) (e2:::Enil) end. @@ -399,29 +412,50 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) := Nondetfunction cast8unsigned (e: expr) := match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (Int.zero_ext 8 n)) Enil | Eop (Oandimm n) (t:::Enil) => - Eop (Oandimm (Int.and (Int.repr 255) n)) (t:::Enil) + andimm (Int.and (Int.repr 255) n) t | _ => Eop Ocast8unsigned (e:::Enil) end. -Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil). +Nondetfunction cast8signed (e: expr) := + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (Int.sign_ext 8 n)) Enil + | _ => + Eop Ocast8signed (e ::: Enil) + end. Nondetfunction cast16unsigned (e: expr) := match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (Int.zero_ext 16 n)) Enil | Eop (Oandimm n) (t:::Enil) => - Eop (Oandimm (Int.and (Int.repr 65535) n)) (t:::Enil) + andimm (Int.and (Int.repr 65535) n) t | _ => Eop Ocast16unsigned (e:::Enil) end. -Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil). +Nondetfunction cast16signed (e: expr) := + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (Int.sign_ext 16 n)) Enil + | _ => + Eop Ocast16signed (e ::: Enil) + end. (** Floating-point conversions *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). -Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). + +Nondetfunction floatofint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil + | _ => Eop Ofloatofint (e ::: Enil) + end. Definition intuoffloat (e: expr) := Elet e @@ -430,12 +464,16 @@ Definition intuoffloat (e: expr) := (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. -Definition floatofintu (e: expr) := - let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in - Elet e - (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) - (floatofint (Eletvar O)) - (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)). +Nondetfunction floatofintu (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil + | _ => + let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in + Elet e + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) + (floatofint (Eletvar O)) + (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)) + end. (** ** Addressing modes *) diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 02d3bee..30e8c5b 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -136,7 +136,10 @@ Qed. Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. - unfold notint; red; intros. TrivialExists. + unfold notint; red; intros until x. case (notint_match a); intros. + InvEval. TrivialExists. + InvEval. subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists. + TrivialExists. Qed. Lemma shift_symbol_address: @@ -198,7 +201,9 @@ Qed. Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v). Proof. - red; intros. unfold negint. TrivialExists. + red; intros until x. unfold negint. case (negint_match a); intros; InvEval. + TrivialExists. + TrivialExists. Qed. Theorem eval_shlimm: @@ -443,7 +448,9 @@ Proof. destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto. destruct (xorimm_match a); intros; InvEval. TrivialExists. simpl. rewrite Int.xor_commut; auto. - subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. + subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. + subst. rewrite Val.not_xor. rewrite Val.xor_assoc. + rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists. TrivialExists. Qed. @@ -679,27 +686,33 @@ Qed. Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. - red; intros. unfold cast8signed. TrivialExists. + red; intros until x. unfold cast8signed. case (cast8signed_match a); intros; InvEval. + TrivialExists. + TrivialExists. Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval. - subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. - rewrite Int.and_commut. TrivialExists. compute; auto. + TrivialExists. + subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. + rewrite Int.and_commut. apply eval_andimm; auto. compute; auto. TrivialExists. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). Proof. - red; intros. unfold cast16signed. TrivialExists. + red; intros until x. unfold cast16signed. case (cast16signed_match a); intros; InvEval. + TrivialExists. + TrivialExists. Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval. + TrivialExists. subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. - rewrite Int.and_commut. TrivialExists. compute; auto. + rewrite Int.and_commut. apply eval_andimm; auto. compute; auto. TrivialExists. Qed. @@ -723,7 +736,9 @@ Theorem eval_floatofint: Val.floatofint x = Some y -> exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v. Proof. - intros; unfold floatofint. TrivialExists. + intros until y; unfold floatofint. case (floatofint_match a); intros; InvEval. + TrivialExists. + TrivialExists. Qed. Theorem eval_intuoffloat: @@ -770,7 +785,9 @@ Theorem eval_floatofintu: Val.floatofintu x = Some y -> exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v. Proof. - intros. destruct x; simpl in H0; try discriminate. inv H0. + intros until y; unfold floatofintu. case (floatofintu_match a); intros. + InvEval. TrivialExists. + destruct x; simpl in H0; try discriminate. inv H0. exists (Vfloat (Float.floatofintu i)); split; auto. econstructor. eauto. set (fm := Float.floatofintu Float.ox8000_0000). diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 1802e11..f3e2194 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -76,6 +76,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oorimm n, v1::nil => or v1 (I n) | Oxor, v1::v2::nil => xor v1 v2 | Oxorimm n, v1::nil => xor v1 (I n) + | Onot, v1::nil => notint v1 | Oshl, v1::v2::nil => shl v1 v2 | Oshlimm n, v1::nil => shl v1 (I n) | Oshr, v1::v2::nil => shr v1 v2 -- cgit v1.2.3