From 842190a7a7c85b15f663fdf299a1f015a774f416 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 20 Feb 2014 09:52:30 +0000 Subject: 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 --- cfrontend/Cexec.v | 10 +++------- cfrontend/Clight.v | 14 -------------- cfrontend/Csem.v | 14 -------------- cfrontend/Cstrategy.v | 3 +-- cfrontend/Initializersproof.v | 1 - cfrontend/SimplExprproof.v | 14 -------------- cfrontend/SimplLocalsproof.v | 13 +------------ 7 files changed, 5 insertions(+), 64 deletions(-) (limited to 'cfrontend') 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 *) -- cgit v1.2.3