From 4032ed3192424a23dbb0a4f3bd2a539b22625168 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 3 Apr 2019 21:00:46 +0200
Subject: problem in ValueAOp

---
 mppa_k1c/Op.v              | 6 +++---
 mppa_k1c/SelectLong.vp     | 8 +++++---
 mppa_k1c/SelectLongproof.v | 3 ++-
 mppa_k1c/ValueAOp.v        | 4 ++--
 4 files changed, 12 insertions(+), 9 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 10e4a350..74788387 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -272,12 +272,12 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : val :=
 
 Definition selectl (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
-  | Vlong iselect =>
+  | Vint iselect =>
     match v0 with
     | Vlong i0 =>
       match v1 with
       | Vlong i1 =>
-        Vlong (if Int64.cmp Ceq Int64.zero iselect
+        Vlong (if Int.cmp Ceq Int.zero iselect
                then i0
                else i1)
       | _ => Vundef
@@ -607,7 +607,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocmp c => (type_of_condition c, Tint)
                 
   | Oselect  => (Tint :: Tint :: Tint :: nil, Tint)
-  | Oselectl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
+  | Oselectl => (Tlong :: Tlong :: Tint :: nil, Tlong)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 60b8f094..7fefe594 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -285,7 +285,10 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
   | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
   | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
   | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) 
-  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil) 
+  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil)
+  end.
+     
+  (*
   |  (Eop Oandl ((Eop Ocast32signed
          ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0))
         (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)),
@@ -298,8 +301,7 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
      then Eop Oselectl (v0:::v1:::y0:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
   | _, _ => Eop Oorl (e1:::e2:::Enil)
-  end.
-     
+  *)
 
 Nondetfunction xorlimm (n1: int64) (e2: expr) :=
   if Int64.eq n1 Int64.zero then e2 else
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 11804d2e..e18de2ee 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -452,6 +452,7 @@ Proof.
 - InvEval. apply eval_orlimm; auto.
 - (*orn*) InvEval. TrivialExists; simpl; congruence.
 - (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence.
+                   (*
   - (* selectl *)
     destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
     predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
@@ -525,7 +526,7 @@ Proof.
       rewrite Int64.and_mone.
       rewrite Int64.and_zero.
       rewrite Int64.or_zero.
-      reflexivity.
+      reflexivity. *)
 - TrivialExists.
 Qed.
 
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 9c851573..de2fd422 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -273,8 +273,8 @@ Proof.
       destruct a1; destruct a0; eauto; constructor.
   (* selectl *)
   - inv H2; simpl; try constructor.
-    + destruct (Int64.eq _ _); apply binop_long_sound; trivial.
-    + destruct (Int64.eq _ _);
+    + destruct (Int.eq _ _); apply binop_long_sound; trivial.
+    + destruct (Int.eq _ _);
       destruct a1; destruct a0; eauto; constructor.
 Qed.
 
-- 
cgit