From 1e70094155a23207b191e4f20e5b05f485fbf654 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 2 Mar 2010 16:20:07 +0000
Subject: [PATCH] Function types didn't always degrade to pointers like they
should. Introduced and used Csyntax.typeconv to address this issue and
reduce the number of cases in the classify functions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1266 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
cfrontend/Csem.v | 2 +-
cfrontend/Cshmgen.v | 4 ++--
cfrontend/Cshmgenproof2.v | 2 +-
cfrontend/Csyntax.v | 41 +++++++++++++++++++++------------------
4 files changed, 26 insertions(+), 23 deletions(-)
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 62e9dc708..f352df70c 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -96,7 +96,7 @@ Function sem_notint (v: val) : option val :=
end.
Function sem_notbool (v: val) (ty: type) : option val :=
- match ty with
+ match typeconv ty with
| Tint _ _ =>
match v with
| Vint n => Some (Val.of_bool (Int.eq n Int.zero))
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index acce971fc..b40b94c76 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -117,7 +117,7 @@ Definition make_neg (e: expr) (ty: type) :=
end.
Definition make_notbool (e: expr) (ty: type) :=
- match ty with
+ match typeconv ty with
| Tfloat _ => Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero)
| _ => Eunop Onotbool e
end.
@@ -197,7 +197,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type
| cmp_case_I32unsi => OK (Ebinop (Ocmpu c) e1 e2)
| cmp_case_ipip => OK (Ebinop (Ocmp c) e1 e2)
| cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
- | cmp_default => Error (msg "Cshmgen.make_shr")
+ | cmp_default => Error (msg "Cshmgen.make_cmp")
end.
Definition make_andbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 431467801..199192c14 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -126,7 +126,7 @@ Lemma make_notbool_correct:
eval_expr globenv e m c v.
Proof.
intros until m; intro SEM. unfold make_notbool.
- functional inversion SEM; intros; inversion H4; simpl;
+ functional inversion SEM; intros; rewrite H0 in H4; inversion H4; simpl;
eauto with cshm.
Qed.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index f66b5befe..48c326e1c 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -74,7 +74,7 @@ Inductive floatsize : Type :=
defined above in C is expressed by
<<
Tstruct "s1" (Fcons "n" (Tint I32 Signed)
- (Fcons "next" (Tcomp_ptr "id")
+ (Fcons "next" (Tcomp_ptr "s1")
Fnil))
>>
Note that the incorrect structure [s2] above cannot be expressed at
@@ -479,6 +479,18 @@ Definition access_mode (ty: type) : mode :=
| Tcomp_ptr _ => By_value Mint32
end.
+(** The usual unary conversion. Promotes small integer types to [signed int32]
+ and degrades array types and function types to pointer types. *)
+
+Definition typeconv (ty: type) : type :=
+ match ty with
+ | Tint I32 Unsigned => ty
+ | Tint _ _ => Tint I32 Signed
+ | Tarray t sz => Tpointer t
+ | Tfunction _ _ => Tpointer ty
+ | _ => ty
+ end.
+
(** Classification of arithmetic operations and comparisons.
The following [classify_] functions take as arguments the types
of the arguments of an operation. They return enough information
@@ -497,13 +509,11 @@ Inductive classify_add_cases : Type :=
| add_default: classify_add_cases. (**r other *)
Definition classify_add (ty1: type) (ty2: type) :=
- match ty1, ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint _ _, Tint _ _ => add_case_ii
| Tfloat _, Tfloat _ => add_case_ff
| Tpointer ty, Tint _ _ => add_case_pi ty
- | Tarray ty _, Tint _ _ => add_case_pi ty
| Tint _ _, Tpointer ty => add_case_ip ty
- | Tint _ _, Tarray ty _ => add_case_ip ty
| _, _ => add_default
end.
@@ -515,15 +525,11 @@ Inductive classify_sub_cases : Type :=
| sub_default: classify_sub_cases . (**r other *)
Definition classify_sub (ty1: type) (ty2: type) :=
- match ty1, ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint _ _ , Tint _ _ => sub_case_ii
| Tfloat _ , Tfloat _ => sub_case_ff
| Tpointer ty , Tint _ _ => sub_case_pi ty
- | Tarray ty _ , Tint _ _ => sub_case_pi ty
| Tpointer ty , Tpointer _ => sub_case_pp ty
- | Tpointer ty , Tarray _ _=> sub_case_pp ty
- | Tarray ty _ , Tpointer _ => sub_case_pp ty
- | Tarray ty _ , Tarray _ _ => sub_case_pp ty
| _ ,_ => sub_default
end.
@@ -533,7 +539,7 @@ Inductive classify_mul_cases : Type:=
| mul_default: classify_mul_cases . (**r other *)
Definition classify_mul (ty1: type) (ty2: type) :=
- match ty1,ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint _ _, Tint _ _ => mul_case_ii
| Tfloat _ , Tfloat _ => mul_case_ff
| _,_ => mul_default
@@ -546,7 +552,7 @@ Inductive classify_div_cases : Type:=
| div_default: classify_div_cases. (**r other *)
Definition classify_div (ty1: type) (ty2: type) :=
- match ty1,ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint I32 Unsigned, Tint _ _ => div_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => div_case_I32unsi
| Tint _ _ , Tint _ _ => div_case_ii
@@ -560,7 +566,7 @@ Inductive classify_mod_cases : Type:=
| mod_default: classify_mod_cases . (**r other *)
Definition classify_mod (ty1: type) (ty2: type) :=
- match ty1,ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint I32 Unsigned , Tint _ _ => mod_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => mod_case_I32unsi
| Tint _ _ , Tint _ _ => mod_case_ii
@@ -573,7 +579,7 @@ Inductive classify_shr_cases :Type:=
| shr_default : classify_shr_cases . (**r other *)
Definition classify_shr (ty1: type) (ty2: type) :=
- match ty1,ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint I32 Unsigned , Tint _ _ => shr_case_I32unsi
| Tint _ _ , Tint _ _ => shr_case_ii
| _ , _ => shr_default
@@ -586,17 +592,14 @@ Inductive classify_cmp_cases : Type:=
| cmp_default: classify_cmp_cases . (**r other *)
Definition classify_cmp (ty1: type) (ty2: type) :=
- match ty1,ty2 with
+ match typeconv ty1, typeconv ty2 with
| Tint I32 Unsigned , Tint _ _ => cmp_case_I32unsi
| Tint _ _ , Tint I32 Unsigned => cmp_case_I32unsi
| Tint _ _ , Tint _ _ => cmp_case_ipip
| Tfloat _ , Tfloat _ => cmp_case_ff
- | 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
+ | Tpointer _ , Tint _ _ => cmp_case_ipip
+ | Tint _ _, Tpointer _ => cmp_case_ipip
| _ , _ => cmp_default
end.
--
GitLab