diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-19 18:17:31 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-19 18:17:31 +0200 |
| commit | be8d929aef8e86c2e22e32c525093c6bfe56a300 (patch) | |
| tree | 9026f38d9251477da228ba0d27706d448d7b7cfb /riscV/RTLpathSE_simplify.v | |
| parent | a6545d8fa35ab4ab3a12823eafacff99d7307314 (diff) | |
| download | compcert-kvx-be8d929aef8e86c2e22e32c525093c6bfe56a300.tar.gz compcert-kvx-be8d929aef8e86c2e22e32c525093c6bfe56a300.zip | |
Adding both RV expansion methods in kvx-work
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 7aca1772..ca049962 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -853,16 +853,6 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. -Remark cast32unsigned_from_cast32signed: - forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). -Proof. - intros. apply Int64.same_bits_eq; intros. - rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. - rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). - change Int.zwordsize with 32. - destruct (zlt i0 32). auto. apply Int.bits_above. auto. -Qed. - (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall |