MPPA - Added non immediate comparison

3 files changed, 21 insertions, 5 deletions

diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index bd65bab9..f1ff363d 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -134,13 +134,13 @@ Definition transl_cbranch
   | Ccompuimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k))
-(*| Ccomp c, a1 :: a2 :: nil =>
+  | Ccomp c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32s c rd r1 r2 k)
+      OK (transl_comp c Signed r1 r2 lbl k)
   | Ccompu c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32u c rd r1 r2 k)
-*)| Ccompimm c n, a1 :: nil =>
+      OK (transl_comp c Unsigned r1 r2 lbl k)
+  | Ccompimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k))
 (*| Ccompl c, a1 :: a2 :: nil =>
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index cc5383a0..1e616a01 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -179,7 +179,11 @@ Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
-  intros. unfold transl_cbranch in H. (* unfold transl_cond_op in H. *) destruct cond; TailNoLabel.
+  intros. unfold transl_cbranch in H. destruct cond; TailNoLabel.
+(* Ccomp *)
+  - unfold transl_comp; TailNoLabel.
+(* Ccompu *)
+  - unfold transl_comp; TailNoLabel.
 (* Ccompimm *)
   - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
 (* Ccompuimm *)
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 1d5a26c9..e83ef307 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -408,6 +408,18 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
+(* Ccomp *)
+- exploit (transl_comp_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez GPR31 lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
+(* Ccompu *)
+- exploit (transl_compu_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
+  exists rs', (Pcb BTwnez GPR31 lbl).
+  split.
+  + constructor. eexact A.
+  + split; auto. apply C; auto.
 (* Ccompimm *)
 - exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
   exploit (transl_comp_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').