aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmgenproof.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2017-11-12 19:23:49 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2019-03-26 16:08:10 +0100
commit8252140c54d9be6f8c62a068f96795eac1e6c078 (patch)
tree33a8ab2fd1a18c094f16888ab88acc6d940bf294 /arm/Asmgenproof.v
parent1df887f5a275e4c31096018ff1a8fdfc39bca591 (diff)
downloadcompcert-8252140c54d9be6f8c62a068f96795eac1e6c078.tar.gz
compcert-8252140c54d9be6f8c62a068f96795eac1e6c078.zip
Introduce and use the type fp_comparison for floating-point comparisons
With FP arithmetic, the negation of "x < y" is not "x >= y". For this reason, the back-end intermediate languages of CompCert used to have both "Ccompf c" and "Cnotcompf c" comparison operators, where "c" is of type Integers.comparison and "Cnotcompf c" denotes the negation of FP comparison c. There are some problems with this approach: - Beyond Cnotcompf we also need Cnotcompfs (for single precision FP) and, in case of ARM, special forms for not-comparison against 0.0. This duplication of comparison constructors inevitably causes some code and proof duplication. - Cnotcompf Ceq is really Ccompf Cne, and likewise Cnotcompf Cne is really Ccompf Ceq, hence the representation of FP comparisons is not canonical, adding to the code and proof duplication mentioned above. - Cnotcompf is introduced in CminorSel, but in Cminor we don't have it, making it impossible to express some transformations over comparisons at the machine-independent Cminor level. This commit develops an alternate approach, whereas FP comparisons have their own type, defined as Floats.fp_comparison, and which includes constructors for "not <", "not <=", "not >" and "not >=". Hence this type is closed under boolean negation, so to speak, and there is no longer a need for "Cnotcompf", given that "Ccompf" takes a fp_comparison and can therefore express all FP comparisons of interest.
Diffstat (limited to 'arm/Asmgenproof.v')
-rw-r--r--arm/Asmgenproof.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 2c001f45..e2a837f7 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -781,19 +781,19 @@ Opaque loadind.
left; eapply exec_straight_steps_goto; eauto.
intros. simpl in TR.
destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
- rewrite EC in B. destruct B as [Bpos Bneg].
+ rewrite EC in B.
econstructor; econstructor; econstructor; split. eexact A.
split. eapply agree_undef_regs; eauto with asmgen.
- simpl. rewrite Bpos. reflexivity.
+ simpl. rewrite B. reflexivity.
- (* Mcond false *)
exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
left; eapply exec_straight_steps; eauto. intros. simpl in TR.
destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
- rewrite EC in B. destruct B as [Bpos Bneg].
+ rewrite EC in B.
econstructor; split.
eapply exec_straight_trans. eexact A.
- apply exec_straight_one. simpl. rewrite Bpos. reflexivity. auto.
+ apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
split. eapply agree_undef_regs; eauto with asmgen.
intros; Simpl.
simpl. congruence.