diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 21:59:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 21:59:22 +0200 |
| commit | 4518486a771055e633aa050141d9721353d542d7 (patch) | |
| tree | 0916e82f7229068dd492c9552c248d9d94137920 /mppa_k1c | |
| parent | 104681e5db184659a36762e0776cef133d70455b (diff) | |
| download | compcert-kvx-4518486a771055e633aa050141d9721353d542d7.tar.gz compcert-kvx-4518486a771055e633aa050141d9721353d542d7.zip | |
ternary ops in AES and TEA
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 2 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 9 |
4 files changed, 9 insertions, 8 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6315192c..a7e3c8ef 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -741,7 +741,7 @@ Definition transl_op do r0 <- ireg_of a0; do r1 <- ireg_of a1; do rS <- ireg_of aS; - OK (Pcmove BTdnez r0 rS r1 ::i k) + OK (Pcmove BTwnez r0 rS r1 ::i k) | _, _ => Error(msg "Asmgenblock.transl_op") diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index d90b73e2..99ab1b91 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1661,8 +1661,8 @@ Opaque Int.eq. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. simpl. - rewrite int64_eq_comm. - destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 7fefe594..f8f5bf3b 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -286,6 +286,7 @@ Nondetfunction orl (e1: expr) (e2: expr) := | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) + | _, _ => Eop Oorl (e1:::e2:::Enil) end. (* @@ -300,7 +301,6 @@ Nondetfunction orl (e1: expr) (e2: expr) := && Int64.eq zero1 Int64.zero then Eop Oselectl (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) - | _, _ => Eop Oorl (e1:::e2:::Enil) *) Nondetfunction xorlimm (n1: int64) (e2: expr) := diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index de2fd422..da108ada 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -53,8 +53,8 @@ Definition select (v0 v1 vselect : aval) : aval := Definition selectl (v0 v1 vselect : aval) : aval := match vselect with - | L iselect => - if Int64.eq Int64.zero iselect + | I iselect => + if Int.eq Int.zero iselect then binop_long (fun x0 x1 => x0) v0 v1 else binop_long (fun x0 x1 => x1) v0 v1 | _ => Vtop @@ -274,8 +274,9 @@ Proof. (* selectl *) - inv H2; simpl; try constructor. + destruct (Int.eq _ _); apply binop_long_sound; trivial. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. End SOUNDNESS. |