aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v2
-rw-r--r--mppa_k1c/Asmblock.v17
-rw-r--r--mppa_k1c/Asmblockdeps.v1
-rw-r--r--mppa_k1c/Asmblockgen.v14
-rw-r--r--mppa_k1c/Asmblockgenproof1.v26
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml3
-rw-r--r--mppa_k1c/TargetPrinter.ml2
-rw-r--r--test/monniaux/ternary_builtin/ternary_builtin.c2
8 files changed, 61 insertions, 6 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 2dc62e11..b323a67c 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -215,6 +215,7 @@ Inductive instruction : Type :=
| Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
| Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *)
| Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *)
+ | Pcmoveu (bt: btest) (rcond rd rs : ireg) (** conditional move, unsigned semantics *)
.
(** Correspondance between Asmblock and Asm *)
@@ -363,6 +364,7 @@ Definition basic_to_instruction (b: basic) :=
| PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
| PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
| PArithARRR (Asmblock.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
+ | PArithARRR (Asmblock.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
(** ARRI32 *)
| PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 1711886d..339b44c6 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -418,6 +418,7 @@ 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 :=
@@ -1229,6 +1230,22 @@ Definition arith_eval_arrr n v1 v2 v3 :=
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 :=
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index d8ca465e..96547342 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1446,6 +1446,7 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
| Pmaddw => "Pmaddw"
| Pmaddl => "Pmaddl"
| Pcmove _ => "Pcmove"
+ | Pcmoveu _ => "Pcmoveu"
end.
Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index d770eebc..ce47cf52 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -367,6 +367,17 @@ Definition transl_cond_op
Error(msg "Asmblockgen.transl_cond_op")
end.
+(* CoMPare Unsigned Words to Zero *)
+Definition btest_for_cmpuwz (c: comparison) :=
+ match c with
+ | Cne => OK BTwnez
+ | Ceq => OK BTweqz
+ | Clt => Error (msg "btest_for_compuwz: Clt")
+ | Cge => Error (msg "btest_for_compuwz: Cge")
+ | Cle => Error (msg "btest_for_compuwz: Cle")
+ | Cgt => Error (msg "btest_for_compuwz: Cgt")
+ end.
+
(** Translation of the arithmetic operation [r <- op(args)].
The corresponding instructions are prepended to [k]. *)
@@ -737,6 +748,9 @@ Definition transl_op
(match cond with
| Ccomp0 cmp =>
OK (Pcmove (btest_for_cmpswz cmp) r0 rS r1 ::i k)
+ | Ccompu0 cmp =>
+ do bt <- btest_for_cmpuwz cmp;
+ 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")
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 7da86de4..75f2005c 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1638,10 +1638,12 @@ Opaque Int.eq.
exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen.
- (* Oselect *)
- destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *;
+ destruct cond in *; simpl in *; try congruence;
+ try monadInv EQ3;
+ try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
econstructor; split;
- try ( eapply exec_straight_one;
- simpl; reflexivity ).
+ try ( eapply exec_straight_one; simpl; reflexivity ).
+ (* Cmp *)
+ split.
* unfold eval_select.
destruct (rs x) eqn:eqX; try constructor.
@@ -1651,6 +1653,24 @@ Opaque Int.eq.
destruct b; simpl; rewrite Pregmap.gss; constructor.
* intros.
rewrite Pregmap.gso; congruence.
+ (* Cmpu *)
+ + 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 (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
+ destruct (Val.cmpu_bool _ _); simpl; try constructor.
+ destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+ rewrite Pregmap.gss; constructor.
+ ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
+ destruct (Val.cmpu_bool _ _); simpl; try constructor.
+ destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+ rewrite Pregmap.gss; constructor.
+ * intros.
+ rewrite Pregmap.gso; congruence.
+
+ (* Cmpl *)
+ split.
* unfold eval_select.
destruct (rs x) eqn:eqX; try constructor.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 6f37412b..b01b7e54 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -129,6 +129,7 @@ let arith_arrr_str = function
| Pmaddw -> "Pmaddw"
| Pmaddl -> "Pmaddl"
| Pcmove _ -> "Pcmove"
+ | Pcmoveu _ -> "Pcmoveu"
let arith_ri32_str = "Pmake"
@@ -488,7 +489,7 @@ let ab_inst_to_real = function
| "Pfixedudrzz" -> Fixedudz
| "Pfixeddrzz_i32" -> Fixeddz
| "Pfixedudrzz_i32" -> Fixedudz
- | "Pcmove" -> Cmoved
+ | "Pcmove" | "Pcmoveu" -> Cmoved
| "Plb" -> Lbs
| "Plbu" -> Lbz
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 4f19e1d8..6f292460 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -529,7 +529,7 @@ module Target (*: TARGET*) =
| Pmaddil (rd, rs, imm) ->
fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs coqint64 imm
- | Pcmove (bt, rd, rcond, rs) ->
+ | Pcmove (bt, rd, rcond, rs) | Pcmoveu (bt, rd, rcond, rs) ->
fprintf oc " cmoved.%a %a? %a = %a\n"
bcond bt ireg rcond ireg rd ireg rs
diff --git a/test/monniaux/ternary_builtin/ternary_builtin.c b/test/monniaux/ternary_builtin/ternary_builtin.c
index 6ea456ab..7f2043ec 100644
--- a/test/monniaux/ternary_builtin/ternary_builtin.c
+++ b/test/monniaux/ternary_builtin/ternary_builtin.c
@@ -4,7 +4,7 @@
int main(int argc, char **argv) {
int i=0;
if (argc >= 2) i=atoi(argv[1]);
- printf("%ld\n", __builtin_ternary_int(i, 42, 69));
+ printf("%ld\n", __builtin_ternary_uint(i, 42, 69));
printf("%f\n", __builtin_ternary_double(i, 42.0, 69.0));
return 0;
}
generated by cgit (git 2.34.1) at 2024-07-02 00:18:46 +0000