From c8f019b509c20bea50330761c5aa0a95e17c6e65 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 16 Mar 2019 12:56:41 +0100 Subject: some more progress on rotate --- mppa_k1c/NeedOp.v | 1 + mppa_k1c/Op.v | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 28d60fa5..5f8648d3 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -155,6 +155,7 @@ Proof. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. +- apply ror_sound; auto. Qed. Lemma operation_is_redundant_sound: diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index e91c6ae1..3a006fb2 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -256,6 +256,7 @@ Definition eval_operation | Oshlimm n, v1 :: nil => Some (Val.shl v1 (Vint n)) | Oshr, v1 :: v2 :: nil => Some (Val.shr v1 v2) | Oshrimm n, v1 :: nil => Some (Val.shr v1 (Vint n)) + | Ororimm n, v1 :: nil => Some (Val.ror v1 (Vint n)) | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2) | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n)) | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) @@ -568,6 +569,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... (* shrx *) - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0... + (* shrimm *) + - destruct v0; simpl... (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -1031,6 +1034,8 @@ Proof. (* shrx *) - inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists. + (* rorimm *) + - inv H4; simpl; auto. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. -- cgit