diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 12:56:41 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 12:56:41 +0100 |
| commit | c8f019b509c20bea50330761c5aa0a95e17c6e65 (patch) | |
| tree | 1695b9bfe36f910349948ef0f3d59f6f760f3c5c | |
| parent | 9526f710a65f9009822240bf2b47e9bc6c07cf19 (diff) | |
| download | compcert-kvx-c8f019b509c20bea50330761c5aa0a95e17c6e65.tar.gz compcert-kvx-c8f019b509c20bea50330761c5aa0a95e17c6e65.zip | |
some more progress on rotate
| -rw-r--r-- | mppa_k1c/NeedOp.v | 1 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 5 |
2 files changed, 6 insertions, 0 deletions
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. |