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

11 files changed, 100 insertions, 26 deletions

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