Select cmplu

2 files changed, 32 insertions, 1 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index ce47cf52..d8706239 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -378,6 +378,17 @@ Definition btest_for_cmpuwz (c: comparison) :=
   | Cgt => Error (msg "btest_for_compuwz: Cgt")
   end.
 
+(* CoMPare Unsigned Words to Zero *)
+Definition btest_for_cmpudz (c: comparison) :=
+  match c with
+  | Cne => OK BTdnez
+  | Ceq => OK BTdeqz
+  | Clt => Error (msg "btest_for_compudz: Clt")
+  | Cge => Error (msg "btest_for_compudz: Cge")
+  | Cle => Error (msg "btest_for_compudz: Cle")
+  | Cgt => Error (msg "btest_for_compudz: Cgt")
+  end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -753,7 +764,9 @@ Definition transl_op
            OK (Pcmoveu bt r0 rS r1 ::i k)
        | Ccompl0 cmp =>
          OK (Pcmove (btest_for_cmpsdz cmp) r0 rS r1 ::i k)
-       | _ => Error (msg "Asmblockgen Oselect")
+       | Ccomplu0 cmp =>
+         do bt <- btest_for_cmpudz cmp;
+           OK (Pcmoveu bt r0 rS r1 ::i k)
        end)
     
   | Oselectl, a0 :: a1 :: aS :: nil
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 75f2005c..1cb75c4c 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1680,6 +1680,24 @@ Opaque Int.eq.
         destruct b; simpl; rewrite Pregmap.gss; constructor.
     * intros.
       rewrite Pregmap.gso; congruence.
+      
+  (* Cmplu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
 - (* Oselectl *)
   econstructor; split.
   + eapply exec_straight_one.