diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-09 15:15:57 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-09 15:15:57 +0200 |
commit | 18312f0470cfb96e44ae1a26a24710cc1df3440d (patch) | |
tree | c1357af49873b291903741b59a2c39dc0ef47722 /riscV/RTLpathSE_simplify.v | |
parent | b7720bc5973e9890e7c320bb34b784e2e2b2da69 (diff) | |
download | compcert-kvx-18312f0470cfb96e44ae1a26a24710cc1df3440d.tar.gz compcert-kvx-18312f0470cfb96e44ae1a26a24710cc1df3440d.zip |
Removing expansions from Asmgen
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index d55d94ad..33e2db61 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -847,6 +847,16 @@ 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 |