From e9fa9cbdc761f8c033e9b702f7485982faed3f7d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 30 Apr 2015 19:26:11 +0200 Subject: Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Val.lessdef, etc. --- cfrontend/SimplLocalsproof.v | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'cfrontend/SimplLocalsproof.v') diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 3364ec6a..2a50f985 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -107,7 +107,7 @@ Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (t (MODE: access_mode ty = By_value chunk) (LOAD: Mem.load chunk m b 0 = Some v) (TLENV: tle!(id) = Some tv) - (VINJ: val_inject f v tv), + (VINJ: Val.inject f v tv), match_var f cenv e m te tle id | match_var_not_lifted: forall b ty b' (ENV: e!id = Some(b, ty)) @@ -130,7 +130,7 @@ Record match_envs (f: meminj) (cenv: compilenv) me_temps: forall id v, le!id = Some v -> - (exists tv, tle!id = Some tv /\ val_inject f v tv) + (exists tv, tle!id = Some tv /\ Val.inject f v tv) /\ (VSet.mem id cenv = true -> v = Vundef); me_inj: forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2; @@ -327,7 +327,7 @@ Qed. Lemma val_casted_inject: forall f v v' ty, - val_inject f v v' -> val_casted v ty -> val_casted v' ty. + Val.inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. intros. inv H; auto. inv H0; constructor. @@ -383,7 +383,7 @@ Lemma match_envs_assign_lifted: match_envs f cenv e le m lo hi te tle tlo thi -> e!id = Some(b, ty) -> val_casted v ty -> - val_inject f v tv -> + Val.inject f v tv -> assign_loc ge ty m b Int.zero v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. @@ -415,7 +415,7 @@ Qed. Lemma match_envs_set_temp: forall f cenv e le m lo hi te tle tlo thi id v tv x, match_envs f cenv e le m lo hi te tle tlo thi -> - val_inject f v tv -> + Val.inject f v tv -> check_temp cenv id = OK x -> match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi. Proof. @@ -436,7 +436,7 @@ Qed. Lemma match_envs_set_opttemp: forall f cenv e le m lo hi te tle tlo thi optid v tv x, match_envs f cenv e le m lo hi te tle tlo thi -> - val_inject f v tv -> + Val.inject f v tv -> check_opttemp cenv optid = OK x -> match_envs f cenv e (set_opttemp optid v le) m lo hi te (set_opttemp optid tv tle) tlo thi. Proof. @@ -993,8 +993,8 @@ Qed. Lemma assign_loc_inject: forall f ty m loc ofs v m' tm loc' ofs' v', assign_loc ge ty m loc ofs v m' -> - val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> - val_inject f v v' -> + Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> + Val.inject f v v' -> Mem.inject f m tm -> exists tm', assign_loc tge ty tm loc' ofs' v' tm' @@ -1095,7 +1095,7 @@ Theorem store_params_correct: forall s tm tle1 tle2 targs, list_norepet (var_names params) -> list_forall2 val_casted args (map snd params) -> - val_list_inject j args targs -> + Val.inject_list j args targs -> match_envs j cenv e le m lo hi te tle1 tlo thi -> Mem.inject j m tm -> (forall id, ~In id (var_names params) -> tle2!id = tle1!id) -> @@ -1388,8 +1388,8 @@ Qed. Lemma deref_loc_inject: forall ty loc ofs v loc' ofs', deref_loc ty m loc ofs v -> - val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> - exists tv, deref_loc ty tm loc' ofs' tv /\ val_inject f v tv. + Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> + exists tv, deref_loc ty tm loc' ofs' tv /\ Val.inject f v tv. Proof. intros. inv H. (* by value *) @@ -1405,14 +1405,14 @@ Lemma eval_simpl_expr: forall a v, eval_expr ge e le m a v -> compat_cenv (addr_taken_expr a) cenv -> - exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ val_inject f v tv + exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv with eval_simpl_lvalue: forall a b ofs, eval_lvalue ge e le m a b ofs -> compat_cenv (addr_taken_expr a) cenv -> match a with Evar id ty => VSet.mem id cenv = false | _ => True end -> - exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ val_inject f (Vptr b ofs) (Vptr b' ofs'). + exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ Val.inject f (Vptr b ofs) (Vptr b' ofs'). Proof. destruct 1; simpl; intros. @@ -1512,7 +1512,7 @@ Lemma eval_simpl_exprlist: val_casted_list vl tyl /\ exists tvl, eval_exprlist tge te tle tm (simpl_exprlist cenv al) tyl tvl - /\ val_list_inject f vl tvl. + /\ Val.inject_list f vl tvl. Proof. induction 1; simpl; intros. split. constructor. econstructor; split. constructor. auto. @@ -1729,7 +1729,7 @@ Lemma match_cont_find_funct: forall f cenv k tk m bound tbound vf fd tvf, match_cont f cenv k tk m bound tbound -> Genv.find_funct ge vf = Some fd -> - val_inject f vf tvf -> + Val.inject f vf tvf -> exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd. Proof. intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG. @@ -1761,7 +1761,7 @@ Inductive match_states: state -> state -> Prop := (TRFD: transf_fundef fd = OK tfd) (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) - (AINJ: val_list_inject j vargs tvargs) + (AINJ: Val.inject_list j vargs tvargs) (FUNTY: type_of_fundef fd = Tfunction targs tres cconv) (ANORM: val_casted_list vargs targs), match_states (Callstate fd vargs k m) @@ -1770,7 +1770,7 @@ Inductive match_states: state -> state -> Prop := forall v k m tv tk tm j (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) - (RINJ: val_inject j v tv), + (RINJ: Val.inject j v tv), match_states (Returnstate v k m) (Returnstate tv tk tm). @@ -2171,7 +2171,7 @@ Proof. eauto. eapply list_norepet_append_left; eauto. apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. - apply val_list_inject_incr with j'; eauto. + apply val_inject_list_incr with j'; eauto. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. -- cgit