From 483d0e37880dbe44af3dafdcac9b1110a37139c4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 06:15:28 +0200 Subject: Select cmplu --- mppa_k1c/Asmblockgen.v | 15 ++++++++++++++- mppa_k1c/Asmblockgenproof1.v | 18 ++++++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) 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. -- cgit