Meilleure compilation de la negation booleenne

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 15 insertions, 7 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 27aa453..34a1080 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -50,6 +50,7 @@ Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr :=
       | Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1)
       | Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1)
       | Csharpminor.Onotint => Some(Cmconstr.notint e1)
+      | Csharpminor.Onotbool => Some(Cmconstr.notbool e1)
       | Csharpminor.Onegf => Some(Cmconstr.negfloat e1)
       | Csharpminor.Oabsf => Some(Cmconstr.absfloat e1)
       | Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1)
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index f700f82..93eb99d 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -888,6 +888,13 @@ Proof.
   change (Vint (Int.cast8signed i)) with (Val.cast8signed (Vint i)). eauto with evalexpr.
   change (Vint (Int.cast16unsigned i)) with (Val.cast16unsigned (Vint i)). eauto with evalexpr.
   change (Vint (Int.cast16signed i)) with (Val.cast16signed (Vint i)). eauto with evalexpr.
+  replace (Int.eq i Int.zero) with (negb (negb (Int.eq i Int.zero))).
+  eapply eval_notbool. eauto. 
+  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro; simpl.
+  rewrite H1; constructor. constructor; auto. 
+  apply negb_elim.
+  unfold Vfalse; TrivialOp. change (Vint Int.zero) with (Val.of_bool (negb true)). 
+  eapply eval_notbool. eauto. constructor. 
   change (Vfloat (Float.singleoffloat f0)) with (Val.singleoffloat (Vfloat f0)). eauto with evalexpr.
   (* Binary operations *)
   inversion H1; clear H1; subst. inversion H11; clear H11; subst.
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 016fab4..f1d22d7 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -37,6 +37,7 @@ Inductive operation : Set :=
   | Ocast8signed: operation             (**r 8-bit sign extension  *)
   | Ocast16unsigned: operation          (**r 16-bit zero extension  *)
   | Ocast16signed: operation            (**r 16-bit sign extension *)
+  | Onotbool: operation                 (**r boolean negation  *)
   | Onotint: operation                  (**r bitwise complement  *)
   | Oadd: operation                     (**r integer addition *)
   | Osub: operation                     (**r integer subtraction *)
@@ -214,6 +215,8 @@ Definition eval_operation (op: operation) (vl: list val) (m: mem): option val :=
   | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1))
   | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1))
   | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1))
+  | Onotbool, Vint n1 :: nil => Some (Val.of_bool (Int.eq n1 Int.zero))
+  | Onotbool, Vptr b1 n1 :: nil => Some (Vfalse)
   | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1))
   | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
   | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index aaec07d..664c6fc 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -96,7 +96,10 @@ Definition make_neg (e: expr) (ty: type) :=
   end.
 
 Definition make_notbool (e: expr) (ty: type) :=
-  make_binop (Ocmp Ceq) (make_boolean e ty) (make_intconst Int.zero).
+  match ty with
+  | Tfloat _ => make_binop (Ocmpf Ceq) e (make_floatconst Float.zero)
+  | _ => make_unop Onotbool e
+  end.
 
 Definition make_notint (e: expr) (ty: type) :=
   make_unop Onotint e.
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 1a5eaa0..0458bd5 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -171,12 +171,6 @@ Proof.
   intros until m2; intro SEM. unfold make_notbool. 
   functional inversion SEM; intros; inversion H4; simpl;
   eauto with cshm.
-  eapply make_binop_correct. 
-  eapply make_binop_correct. eauto. eauto with cshm. 
-  simpl; reflexivity. reflexivity. eauto with cshm. 
-  simpl. rewrite Float.cmp_ne_eq. 
-  destruct (Float.cmp Ceq f Float.zero); reflexivity.
-  traceEq.
 Qed.
 
 Lemma make_notint_correct: