MPPA - Long comparisons

5 files changed, 158 insertions, 30 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index d769062f..d19f9340 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -187,6 +187,7 @@ Inductive instruction : Type :=
 
 (** Comparisons *)
   | Pcompw  (it: itest) (rd rs1 rs2: ireg)      (**r integer comparison *)
+  | Pcompd  (it: itest) (rd rs1 rs2: ireg)      (**r integer comparison *)
 
 (** 32-bit integer register-immediate instructions *)
   | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
@@ -602,6 +603,31 @@ Definition compare_int (t: itest) (v1 v2: val) (m: mem): val :=
   | ITnone => Vundef
   end.
 
+Definition compare_long (t: itest) (v1 v2: val) (m: mem): val :=
+  let res := match t with
+  | ITne  => Val.cmpl Cne v1 v2
+  | ITeq  => Val.cmpl Ceq v1 v2
+  | ITlt  => Val.cmpl Clt v1 v2
+  | ITge  => Val.cmpl Cge v1 v2
+  | ITle  => Val.cmpl Cle v1 v2
+  | ITgt  => Val.cmpl Cgt v1 v2
+  | ITneu => Val.cmplu (Mem.valid_pointer m) Cne v1 v2
+  | ITequ => Val.cmplu (Mem.valid_pointer m) Ceq v1 v2
+  | ITltu => Val.cmplu (Mem.valid_pointer m) Clt v1 v2
+  | ITgeu => Val.cmplu (Mem.valid_pointer m) Cge v1 v2
+  | ITleu => Val.cmplu (Mem.valid_pointer m) Cle v1 v2
+  | ITgtu => Val.cmplu (Mem.valid_pointer m) Cgt v1 v2
+  | ITall
+  | ITnall
+  | ITany
+  | ITnone => Some Vundef
+  end in 
+  match res with
+  | Some v => v
+  | None => Vundef
+  end
+  .
+
 (** Execution of a single instruction [i] in initial state [rs] and
     [m].  Return updated state.  For instructions that correspond to
     actual RISC-V instructions, the cases are straightforward
@@ -637,8 +663,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 
 (** Comparisons *)
   | Pcompw c d s1 s2 => 
-      (* Next (nextinstr (rs#d <- (Val.cmp Cne rs##s1 rs##s2))) m *)
       Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m
+  | Pcompd c d s1 s2 => 
+      Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m
 
 (** 32-bit integer register-immediate instructions *)
   | Paddiw d s i =>
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index f1ff363d..710bb32c 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -128,6 +128,10 @@ Definition transl_comp
     (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
   Pcompw (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
 
+Definition transl_compl
+    (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
+  Pcompd (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
+
 Definition transl_cbranch
     (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
   match cond, args with
@@ -143,19 +147,19 @@ Definition transl_cbranch
   | 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 =>
+  | Ccompluimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k))
+  | Ccompl c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64s c rd r1 r2 k)
+      OK (transl_compl c Signed r1 r2 lbl k)
   | Ccomplu c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64u c rd r1 r2 k)
+      OK (transl_compl c Unsigned r1 r2 lbl k)
   | Ccomplimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (transl_condimm_int64s c rd r1 n k)
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int64u c rd r1 n k)
-  | Ccompf c, f1 :: f2 :: nil =>
+      OK (loadimm64 RTMP n (transl_compl c Signed r1 RTMP lbl k))
+(*| Ccompf c, f1 :: f2 :: nil =>
       do r1 <- freg_of f1; do r2 <- freg_of f2;
       let (insn, normal) := transl_cond_float c rd r1 r2 in
       OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 1e616a01..3dce24cf 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -188,6 +188,14 @@ Proof.
   - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
 (* Ccompuimm *)
   - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
+(* Ccompl *)
+  - unfold transl_compl; TailNoLabel.
+(* Ccomplu *)
+  - unfold transl_compl; TailNoLabel.
+(* Ccomplimm *)
+  - unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
+(* Ccompluimm *)
+  - unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
 Qed.
 
 (*
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index e83ef307..fe037994 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -144,6 +144,22 @@ Proof.
   split. Simpl.
   intros; Simpl.
 Qed.
+
+Lemma loadimm64_correct:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
+  /\ rs'#rd = Vlong n
+  /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
+Proof.
+  unfold loadimm64; intros. generalize (make_immed64_sound n); intros E.
+  destruct (make_immed64 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. 
+  intros; Simpl.
+Qed.
+
 (*
 Lemma opimm32_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
@@ -194,28 +210,8 @@ Proof.
   split. Simpl. 
   intros; Simpl.
 Qed.
-
-Lemma loadimm64_correct:
-  forall rd n k rs m,
-  exists rs',
-     exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
-  /\ rs'#rd = Vlong n
-  /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r.
-Proof.
-  unfold loadimm64; intros. generalize (make_immed64_sound n); intros E.
-  destruct (make_immed64 n). 
-- subst imm. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. rewrite Int64.add_zero_l; Simpl. 
-  intros; Simpl.
-- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C).
-  rewrite E. exists rs'; eauto.
-- subst imm. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split. Simpl. 
-  intros; Simpl.
-Qed.
 *)
+
 Lemma opimm64_correct:
   forall (op: ireg -> ireg -> ireg -> instruction)
          (opi: ireg -> ireg -> int64 -> instruction)
@@ -390,6 +386,63 @@ Proof.
     rewrite H0. simpl; auto.
 Qed.
 
+Lemma transl_compl_correct:
+  forall cmp r1 r2 lbl k rs m b,
+  exists rs',
+     exec_straight ge fn (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
+       exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compl. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (nextinstr rs # GPR31 <- (compare_long (itest_for_cmp cmp Signed) rs ### r1 rs ### r2 m)) as rs'.
+    simpl. assert (Val.cmp_bool Cne rs' ## GPR31 (Vint (Int.repr 0)) = Some b).
+    { 
+      assert (rs' ## GPR31 = (compare_long (itest_for_cmp cmp Signed) rs ### r1 rs ### r2 m)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmpl_bool cmp rs###r1 rs###r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long;
+      unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_complu_correct:
+  forall cmp r1 r2 lbl k rs m b,
+  exists rs',
+     exec_straight ge fn (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
+       exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_compl. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (nextinstr rs # GPR31 <- (compare_long (itest_for_cmp cmp Unsigned) rs ### r1 rs ### r2 m)) as rs'.
+    simpl. assert (Val.cmp_bool Cne rs' ## GPR31 (Vint (Int.repr 0)) = Some b).
+    { 
+      assert (rs' ## GPR31 = (compare_long (itest_for_cmp cmp Unsigned) rs ### r1 rs ### r2 m)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold compare_long;
+      unfold Val.cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
 
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m',
@@ -442,6 +495,40 @@ Proof.
   + split; auto.
     * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen.
     * intros. rewrite B'; eauto with asmgen.
+(* Ccompl *)
+- exploit (transl_compl_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.
+(* Ccomplu *)
+- exploit (transl_complu_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.
+(* Ccomplimm *)
+- exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
+  exploit (transl_compl_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
+  exists rs'2, (Pcb BTwnez GPR31 lbl).
+  split.
+  + constructor. apply exec_straight_trans 
+       with (c2 := (transl_compl c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+    eexact A. eexact A'.
+  + split; auto.
+    * apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen.
+    * intros. rewrite B'; eauto with asmgen.
+(* Ccompluimm *)
+- exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
+  exploit (transl_complu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
+  exists rs'2, (Pcb BTwnez GPR31 lbl).
+  split.
+  + constructor. apply exec_straight_trans 
+       with (c2 := (transl_compl c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+    eexact A. eexact A'.
+  + split; auto.
+    * apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen.
+    * intros. rewrite B'; eauto with asmgen.
 Qed.
 
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 2c7b8cc8..2fafb127 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -210,6 +210,8 @@ module Target : TARGET =
 
       | Pcompw (it, rd, rs1, rs2) ->
          fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
+      | Pcompd (it, rd, rs1, rs2) ->
+         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
       | Pcb (bt, r, lbl) ->
          fprintf oc "	cb.%a	%a?%a\n;;\n" bcond bt ireg r print_label lbl