Remove useless checks on type_of_global in dynamic semantics

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7 files changed, 5 insertions, 64 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index d585760..bc85efd 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -732,8 +732,6 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
           topred (Lred (Eloc b Int.zero ty) m)
       | None =>
           do b <- Genv.find_symbol ge x;
-          do ty' <- type_of_global ge b;
-          check type_eq ty ty';
           topred (Lred (Eloc b Int.zero ty) m)
       end
   | LV, Ederef r ty =>
@@ -985,7 +983,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Evar x ty =>
       exists b,
       e!x = Some(b, ty)
-      \/ (e!x = None /\ Genv.find_symbol ge x = Some b /\ type_of_global ge b = Some ty)
+      \/ (e!x = None /\ Genv.find_symbol ge x = Some b)
   | Ederef (Eval v ty1) ty =>
       exists b, exists ofs, v = Vptr b ofs
   | Efield (Eval v ty1) f ty =>
@@ -1381,9 +1379,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence;
   destruct (type_eq ty ty')...
   subst. apply topred_ok; auto. apply red_var_local; auto.
   destruct (Genv.find_symbol ge x) as [b|] eqn:?...
-  destruct (type_of_global ge b) as [ty'|] eqn:?...
-  destruct (type_eq ty ty')...
-  subst. apply topred_ok; auto. apply red_var_global; auto.
+  apply topred_ok; auto. apply red_var_global; auto.
 (* Efield *)
   destruct (is_val a) as [[v ty'] | ] eqn:?.
   rewrite (is_val_inv _ _ _ Heqo).
@@ -1590,7 +1586,7 @@ Proof.
 (* var local *)
   rewrite H. rewrite dec_eq_true; auto.
 (* var global *)
-  rewrite H; rewrite H0; rewrite H1. rewrite dec_eq_true; auto.
+  rewrite H; rewrite H0. auto.
 (* deref *) 
   auto.
 (* field struct *)
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 59c056d..f2ba240 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -335,19 +335,6 @@ Section SEMANTICS.
 
 Variable ge: genv.
 
-(** [type_of_global b] returns the type of the global variable or function
-  at address [b]. *)
-
-Definition type_of_global (b: block) : option type :=
-  match Genv.find_var_info ge b with
-  | Some gv => Some gv.(gvar_info)
-  | None =>
-      match Genv.find_funct_ptr ge b with
-      | Some fd => Some(type_of_fundef fd)
-      | None => None
-      end
-  end.
-
 (** ** Evaluation of expressions *)
 
 Section EXPR.
@@ -402,7 +389,6 @@ with eval_lvalue: expr -> block -> int -> Prop :=
   | eval_Evar_global: forall id l ty,
       e!id = None ->
       Genv.find_symbol ge id = Some l ->
-      type_of_global l = Some ty ->
       eval_lvalue (Evar id ty) l Int.zero
   | eval_Ederef: forall a ty l ofs,
       eval_expr a (Vptr l ofs) ->
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 2eedbd8..5acf23f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -189,19 +189,6 @@ Section SEMANTICS.
 
 Variable ge: genv.
 
-(** [type_of_global b] returns the type of the global variable or function
-  at address [b]. *)
-
-Definition type_of_global (b: block) : option type :=
-  match Genv.find_var_info ge b with
-  | Some gv => Some gv.(gvar_info)
-  | None =>
-      match Genv.find_funct_ptr ge b with
-      | Some fd => Some(type_of_fundef fd)
-      | None => None
-      end
-  end.
-
 (** ** Reduction semantics for expressions *)
 
 Section EXPR.
@@ -223,7 +210,6 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop :=
   | red_var_global: forall x ty m b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      type_of_global b = Some ty ->
       lred (Evar x ty) m
            (Eloc b Int.zero ty) m
   | red_deref: forall b ofs ty1 ty m,
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index b1fbebe..386169a 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -93,7 +93,6 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
   | esl_var_global: forall x ty b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      type_of_global ge b = Some ty ->
       eval_simple_lvalue (Evar x ty) b Int.zero
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
@@ -520,7 +519,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Evar x ty =>
       exists b,
       e!x = Some(b, ty)
-      \/ (e!x = None /\ Genv.find_symbol ge x = Some b /\ type_of_global ge b = Some ty)
+      \/ (e!x = None /\ Genv.find_symbol ge x = Some b)
   | Ederef (Eval v ty1) ty =>
       exists b, exists ofs, v = Vptr b ofs
   | Efield (Eval v ty1) f ty =>
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index ca2a40c..c276008 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -86,7 +86,6 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
   | esl_var_global: forall x ty b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      type_of_global ge b = Some ty ->
       eval_simple_lvalue (Evar x ty) b Int.zero
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 9134e11..0a77b19 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -105,19 +105,6 @@ Proof.
   intros. inv H; auto. 
 Qed.
 
-Lemma type_of_global_preserved:
-  forall b ty,
-  Csem.type_of_global ge b = Some ty ->
-  type_of_global tge b = Some ty.
-Proof.
-  intros until ty. unfold Csem.type_of_global, type_of_global.
-  rewrite varinfo_preserved. destruct (Genv.find_var_info ge b). auto. 
-  case_eq (Genv.find_funct_ptr ge b); intros. 
-  inv H0. exploit function_ptr_translated; eauto. intros [tf [A B]]. 
-  rewrite A. decEq. apply type_of_fundef_preserved; auto.
-  congruence.
-Qed.
-
 (** Translation of simple expressions. *)
 
 Lemma tr_simple_nil:
@@ -269,7 +256,6 @@ Opaque makeif.
 (* var global *)
   split; auto. split; auto. apply eval_Evar_global; auto.
     rewrite symbols_preserved; auto.
-    eapply type_of_global_preserved; eauto. 
 (* deref *)
   exploit H0; eauto. intros [A [B C]]. subst sl1.
   split; auto. split; auto. constructor; auto.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 9b97b3b..6eec8cc 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -78,16 +78,6 @@ Proof.
   monadInv EQ. simpl; unfold type_of_function; simpl. auto.  
 Qed.
 
-Lemma type_of_global_preserved:
-  forall id ty, type_of_global ge id = Some ty -> type_of_global tge id = Some ty.
-Proof.
-  unfold type_of_global; intros.
-  rewrite varinfo_preserved. destruct (Genv.find_var_info ge id). auto. 
-  destruct (Genv.find_funct_ptr ge id) as [fd|] eqn:?; inv H.
-  exploit function_ptr_translated; eauto. intros [tf [A B]]. rewrite A. 
-  decEq. apply type_of_fundef_preserved; auto.
-Qed.
-
 (** Matching between environments before and after *)
 
 Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (tle: temp_env) (id: ident) : Prop :=
@@ -1481,11 +1471,10 @@ Proof.
   apply eval_Evar_local; auto.
   econstructor; eauto.
 (* global var *)
-  rewrite H3.
+  rewrite H2.
   exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence.
   exists l; exists Int.zero; split.
   apply eval_Evar_global. auto. rewrite <- H0. apply symbols_preserved. 
-  eapply type_of_global_preserved; eauto. 
   destruct GLOB as [bound GLOB1]. inv GLOB1.
   econstructor; eauto. 
 (* deref *)