Merge remote-tracking branch 'origin/mppa-work' into mppa-refactor

Conflicts:
	mppa_k1c/Asm.v
	mppa_k1c/Asmblock.v

1 files changed, 35 insertions, 1 deletions

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 6c18ac32..8620326f 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -426,6 +426,8 @@ Inductive arith_name_rri64 : Type :=
 Inductive arith_name_arrr : Type :=
   | Pmaddw                                           (**r multiply add word *)
   | Pmaddl                                           (**r multiply add long *)
+  | Pcmove (bt: btest)                               (**r conditional move *)
+  | Pcmoveu (bt: btest)                              (**r conditional move, test on unsigned semantics *)
 .
 
 Inductive arith_name_arri32 : Type :=
@@ -990,6 +992,38 @@ Definition arith_eval_arrr n v1 v2 v3 :=
   match n with
   | Pmaddw => Val.add v1 (Val.mul v2 v3)
   | Pmaddl => Val.addl v1 (Val.mull v2 v3)
+  | Pcmove bt =>
+    match cmp_for_btest bt with
+    | (Some c, Int)  =>
+      match Val.cmp_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val.cmpl_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
+  | Pcmoveu bt =>
+    match cmpu_for_btest bt with
+    | (Some c, Int)  =>
+      match Val_cmpu_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val_cmplu_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
   end.
 
 Definition arith_eval_arri32 n v1 v2 v3 :=
@@ -1528,4 +1562,4 @@ Ltac Det_WIO X :=
   inv H; rewrite H0 in *; eelim NOTNULL; eauto.
 - (* final states *)
   intros s r1 r2 H H0; inv H; inv H0. congruence.
-Qed.
\ No newline at end of file
+Qed.