From b9eef9995d212255ee1fa94877ca891aee6adfc3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 13 Nov 2007 14:49:02 +0000
Subject: [PATCH] In Clight, revised handling of comparisons between pointers
and 0
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
cfrontend/Csem.v | 35 +++++++++++++++--------------------
cfrontend/Cshmgen.v | 4 +---
cfrontend/Cshmgenproof2.v | 21 +++++++++++++++------
cfrontend/Csyntax.v | 18 ++++++++----------
4 files changed, 39 insertions(+), 39 deletions(-)
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 8d8f88a30..761761631 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -266,35 +266,30 @@ Function sem_cmp (c:comparison)
match classify_cmp t1 t2 with
| cmp_case_I32unsi =>
match v1,v2 with
- | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmpu c n1 n2))
+ | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
| _, _ => None
end
- | cmp_case_ii =>
- match v1,v2 with
- | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmp c n1 n2))
- | _, _ => None
- end
- | cmp_case_ff =>
- match v1,v2 with
- | Vfloat f1, Vfloat f2 =>Some (Val.of_bool (Float.cmp c f1 f2))
- | _, _ => None
- end
- | cmp_case_pi =>
- match v1,v2 with
- | Vptr b ofs, Vint n2 =>
- if Int.eq n2 Int.zero then sem_cmp_mismatch c else None
- | _, _ => None
- end
- | cmp_case_pp =>
+ | cmp_case_ipip =>
match v1,v2 with
+ | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
| Vptr b1 ofs1, Vptr b2 ofs2 =>
- if valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b2 (Int.signed ofs2) then
+ if valid_pointer m b1 (Int.signed ofs1)
+ && valid_pointer m b2 (Int.signed ofs2) then
if zeq b1 b2
then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
else None
else None
+ | Vptr b ofs, Vint n =>
+ if Int.eq n Int.zero then sem_cmp_mismatch c else None
+ | Vint n, Vptr b ofs =>
+ if Int.eq n Int.zero then sem_cmp_mismatch c else None
| _, _ => None
- end
+ end
+ | cmp_case_ff =>
+ match v1,v2 with
+ | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2))
+ | _, _ => None
+ end
| cmp_default => None
end.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 6ec3757b3..4090c55a1 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -174,10 +174,8 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
match classify_cmp ty1 ty2 with
| cmp_case_I32unsi => OK (Ebinop (Ocmpu c) e1 e2)
- | cmp_case_ii => OK (Ebinop (Ocmp c) e1 e2)
+ | cmp_case_ipip => OK (Ebinop (Ocmp c) e1 e2)
| cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
- | cmp_case_pi => OK (Ebinop (Ocmp c) e1 e2)
- | cmp_case_pp => OK (Ebinop (Ocmp c) e1 e2)
| cmp_default => Error (msg "Cshmgen.make_shr")
end.
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index aa4e391a9..6b7b5e3c7 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -285,15 +285,24 @@ Lemma make_cmp_correct:
eval_expr tprog e m c v.
Proof.
intros until m. intro SEM. unfold make_cmp.
- functional inversion SEM; rewrite H0; intros.
- inversion H8. eauto with cshm.
+ functional inversion SEM; rewrite H0; intros.
+ (* I32unsi *)
inversion H8. eauto with cshm.
+ (* ipip int int *)
inversion H8. eauto with cshm.
- inversion H9. eapply eval_Ebinop; eauto with cshm.
- simpl. functional inversion H; subst; unfold eval_compare_null;
- rewrite H8; auto.
+ (* ipip ptr ptr *)
inversion H10. eapply eval_Ebinop; eauto with cshm.
- simpl. rewrite H3. unfold eq_block; rewrite H9. auto.
+ simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
+ (* ipip ptr int *)
+ inversion H9. eapply eval_Ebinop; eauto with cshm.
+ simpl. unfold eval_compare_null. rewrite H8.
+ functional inversion H; subst; auto.
+ (* ipip int ptr *)
+ inversion H9. eapply eval_Ebinop; eauto with cshm.
+ simpl. unfold eval_compare_null. rewrite H8.
+ functional inversion H; subst; auto.
+ (* ff *)
+ inversion H8. eauto with cshm.
Qed.
Lemma transl_unop_correct:
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 31d1d873e..00fdaa55f 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -466,24 +466,22 @@ Definition classify_shr (ty1: type) (ty2: type) :=
Inductive classify_cmp_cases : Set:=
| cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
- | cmp_case_ii: classify_cmp_cases (**r int , int*)
+ | cmp_case_ipip: classify_cmp_cases (**r int|ptr|array , int|ptr|array*)
| cmp_case_ff: classify_cmp_cases (**r float , float *)
- | cmp_case_pi: classify_cmp_cases (**r ptr or array , int *)
- | cmp_case_pp:classify_cmp_cases (**r ptr or array , ptr or array *)
| cmp_default: classify_cmp_cases . (**r other *)
Definition classify_cmp (ty1: type) (ty2: type) :=
match ty1,ty2 with
| Tint I32 Unsigned , Tint _ _ => cmp_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => cmp_case_I32unsi
- | Tint _ _ , Tint _ _ => cmp_case_ii
+ | Tint _ _ , Tint _ _ => cmp_case_ipip
| Tfloat _ , Tfloat _ => cmp_case_ff
- | Tpointer _ , Tint _ _ => cmp_case_pi
- | Tarray _ _ , Tint _ _ => cmp_case_pi
- | Tpointer _ , Tpointer _ => cmp_case_pp
- | Tpointer _ , Tarray _ _ => cmp_case_pp
- | Tarray _ _ ,Tpointer _ => cmp_case_pp
- | Tarray _ _ ,Tarray _ _ => cmp_case_pp
+ | Tpointer _ , Tint _ _ => cmp_case_ipip
+ | Tarray _ _ , Tint _ _ => cmp_case_ipip
+ | Tpointer _ , Tpointer _ => cmp_case_ipip
+ | Tpointer _ , Tarray _ _ => cmp_case_ipip
+ | Tarray _ _ ,Tpointer _ => cmp_case_ipip
+ | Tarray _ _ ,Tarray _ _ => cmp_case_ipip
| _ , _ => cmp_default
end.
--
GitLab