From 095ec29088ede2c5ca7db813d56001efb63aa97e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 23 Aug 2015 14:28:29 +0200 Subject: Track the locations of local variables using EF_debug annotations. SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known. --- cfrontend/SimplLocalsproof.v | 174 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 152 insertions(+), 22 deletions(-) (limited to 'cfrontend/SimplLocalsproof.v') diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 2a50f985..73092ab9 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -334,6 +334,13 @@ Proof. inv H0; constructor. Qed. +Lemma forall2_val_casted_inject: + forall f vl vl', Val.inject_list f vl vl' -> + forall tyl, list_forall2 val_casted vl tyl -> list_forall2 val_casted vl' tyl. +Proof. + induction 1; intros tyl F; inv F; constructor; eauto. eapply val_casted_inject; eauto. +Qed. + Inductive val_casted_list: list val -> typelist -> Prop := | vcl_nil: val_casted_list nil Tnil @@ -376,6 +383,116 @@ Proof. inv H0; auto. Qed. +(** Debug annotations. *) + +Lemma cast_typeconv: + forall v ty, + val_casted v ty -> + sem_cast v ty (typeconv ty) = Some v. +Proof. + induction 1; simpl; auto. +- destruct sz; auto. +- unfold sem_cast. simpl. rewrite dec_eq_true; auto. +- unfold sem_cast. simpl. rewrite dec_eq_true; auto. +Qed. + +Lemma step_Sdebug_temp: + forall f id ty k e le m v, + le!id = Some v -> + val_casted v ty -> + step2 tge (State f (Sdebug_temp id ty) k e le m) + E0 (State f Sskip k e le m). +Proof. + intros. unfold Sdebug_temp. eapply step_builtin with (optid := None). + econstructor. constructor. eauto. simpl. eapply cast_typeconv; eauto. constructor. + simpl. constructor. +Qed. + +Lemma step_Sdebug_var: + forall f id ty k e le m b, + e!id = Some(b, ty) -> + step2 tge (State f (Sdebug_var id ty) k e le m) + E0 (State f Sskip k e le m). +Proof. + intros. unfold Sdebug_var. eapply step_builtin with (optid := None). + econstructor. constructor. constructor. eauto. + simpl. reflexivity. constructor. + simpl. constructor. +Qed. + +Lemma step_Sset_debug: + forall f id ty a k e le m v v', + eval_expr tge e le m a v -> + sem_cast v (typeof a) ty = Some v' -> + plus step2 tge (State f (Sset_debug id ty a) k e le m) + E0 (State f Sskip k e (PTree.set id v' le) m). +Proof. + intros; unfold Sset_debug. + assert (forall k, step2 tge (State f (Sset id (make_cast a ty)) k e le m) + E0 (State f Sskip k e (PTree.set id v' le) m)). + { intros. apply step_set. eapply make_cast_correct; eauto. } + destruct (Compopts.debug tt). +- eapply plus_left. constructor. + eapply star_left. apply H1. + eapply star_left. constructor. + apply star_one. apply step_Sdebug_temp with (v := v'). + apply PTree.gss. eapply cast_val_is_casted; eauto. + reflexivity. reflexivity. reflexivity. +- apply plus_one. apply H1. +Qed. + +Lemma step_add_debug_vars: + forall f s e le m vars k, + (forall id ty, In (id, ty) vars -> exists b, e!id = Some (b, ty)) -> + star step2 tge (State f (add_debug_vars vars s) k e le m) + E0 (State f s k e le m). +Proof. + unfold add_debug_vars. destruct (Compopts.debug tt). +- induction vars; simpl; intros. + + apply star_refl. + + destruct a as [id ty]. + exploit H; eauto. intros (b & TE). + simpl. eapply star_left. constructor. + eapply star_left. eapply step_Sdebug_var; eauto. + eapply star_left. constructor. + apply IHvars; eauto. + reflexivity. reflexivity. reflexivity. +- intros. apply star_refl. +Qed. + +Remark bind_parameter_temps_inv: + forall id params args le le', + bind_parameter_temps params args le = Some le' -> + ~In id (var_names params) -> + le'!id = le!id. +Proof. + induction params; simpl; intros. + destruct args; inv H. auto. + destruct a as [id1 ty1]. destruct args; try discriminate. + transitivity ((PTree.set id1 v le)!id). + eapply IHparams; eauto. apply PTree.gso. intuition. +Qed. + +Lemma step_add_debug_params: + forall f s k e le m params vl le1, + list_norepet (var_names params) -> + list_forall2 val_casted vl (map snd params) -> + bind_parameter_temps params vl le1 = Some le -> + star step2 tge (State f (add_debug_params params s) k e le m) + E0 (State f s k e le m). +Proof. + unfold add_debug_params. destruct (Compopts.debug tt). +- induction params as [ | [id ty] params ]; simpl; intros until le1; intros NR CAST BIND; inv CAST; inv NR. + + apply star_refl. + + assert (le!id = Some a1). { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. } + eapply star_left. constructor. + eapply star_left. eapply step_Sdebug_temp; eauto. + eapply star_left. constructor. + eapply IHparams; eauto. + reflexivity. reflexivity. reflexivity. +- intros; apply star_refl. +Qed. + (** Preservation by assignment to lifted variable. *) Lemma match_envs_assign_lifted: @@ -909,7 +1026,8 @@ Theorem match_envs_alloc_variables: /\ Mem.inject j' m' tm' /\ inject_incr j j' /\ (forall b, Mem.valid_block m b -> j' b = j b) - /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b). + /\ (forall b b' delta, j' b = Some(b', delta) -> Mem.valid_block tm b' -> j' b = j b) + /\ (forall id ty, In (id, ty) vars -> VSet.mem id cenv = false -> exists b, te!id = Some(b, ty)). Proof. intros. exploit (match_alloc_variables cenv); eauto. instantiate (1 := empty_env). @@ -988,6 +1106,10 @@ Proof. (* incr *) eapply alloc_variables_nextblock; eauto. eapply alloc_variables_nextblock; eauto. + + (* other properties *) + intuition auto. edestruct F as (b & X & Y); eauto. rewrite H5 in Y. + destruct Y as (tb & U & V). exists tb; auto. Qed. Lemma assign_loc_inject: @@ -1067,19 +1189,6 @@ Proof. left. congruence. Qed. -Remark bind_parameter_temps_inv: - forall id params args le le', - bind_parameter_temps params args le = Some le' -> - ~In id (var_names params) -> - le'!id = le!id. -Proof. - induction params; simpl; intros. - destruct args; inv H. auto. - destruct a as [id1 ty1]. destruct args; try discriminate. - transitivity ((PTree.set id1 v le)!id). - eapply IHparams; eauto. apply PTree.gso. intuition. -Qed. - Lemma assign_loc_nextblock: forall ge ty m b ofs v m', assign_loc ge ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m. @@ -1917,6 +2026,7 @@ Proof. monadInv TS; auto. (* var *) destruct (is_liftable_var cenv e); monadInv TS; auto. + unfold Sset_debug. destruct (Compopts.debug tt); auto. (* set *) monadInv TS; auto. (* call *) @@ -1975,12 +2085,26 @@ Proof. Qed. Lemma find_label_store_params: - forall lbl s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k. + forall s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k. Proof. induction params; simpl. auto. destruct a as [id ty]. destruct (VSet.mem id cenv); auto. Qed. +Lemma find_label_add_debug_vars: + forall s k vars, find_label lbl (add_debug_vars vars s) k = find_label lbl s k. +Proof. + unfold add_debug_vars. destruct (Compopts.debug tt); auto. + induction vars; simpl; auto. destruct a as [id ty]; simpl. auto. +Qed. + +Lemma find_label_add_debug_params: + forall s k vars, find_label lbl (add_debug_params vars s) k = find_label lbl s k. +Proof. + unfold add_debug_params. destruct (Compopts.debug tt); auto. + induction vars; simpl; auto. destruct a as [id ty]; simpl. auto. +Qed. + End FIND_LABEL. @@ -1999,8 +2123,8 @@ Proof. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv H. (* local variable *) - econstructor; split. - apply plus_one. econstructor. eapply make_cast_correct. eexact A. rewrite typeof_simpl_expr. eexact C. + econstructor; split. + eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto. econstructor; eauto with compat. eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto. eapply match_cont_assign_loc; eauto. exploit me_range; eauto. xomega. @@ -2154,7 +2278,8 @@ Proof. apply compat_cenv_for. rewrite H. intros [ts' [tk' [A [B [C D]]]]]. econstructor; split. - apply plus_one. econstructor; eauto. simpl. rewrite find_label_store_params. eexact A. + apply plus_one. econstructor; eauto. simpl. + rewrite find_label_add_debug_params. rewrite find_label_store_params. rewrite find_label_add_debug_vars. eexact A. econstructor; eauto. (* internal function *) @@ -2166,11 +2291,13 @@ Proof. instantiate (1 := cenv_for_gen (addr_taken_stmt f.(fn_body)) (fn_params f ++ fn_vars f)). intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H4. intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H3. - intros [j' [te [tm0 [A [B [C [D [E F]]]]]]]]. + intros [j' [te [tm0 [A [B [C [D [E [F G]]]]]]]]]. + assert (K: list_forall2 val_casted vargs (map snd (fn_params f))). + { apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. } exploit store_params_correct. eauto. eapply list_norepet_append_left; eauto. - apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. + eexact K. apply val_inject_list_incr with j'; eauto. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. @@ -2184,8 +2311,11 @@ Proof. econstructor; split. eapply plus_left. econstructor. econstructor. exact Y. exact X. exact Z. simpl. eexact A. simpl. eexact Q. - simpl. eexact P. - traceEq. + simpl. eapply star_trans. eapply step_add_debug_params. auto. eapply forall2_val_casted_inject; eauto. eexact Q. + eapply star_trans. eexact P. eapply step_add_debug_vars. + unfold remove_lifted; intros. rewrite List.filter_In in H3. destruct H3. + apply negb_true_iff in H4. eauto. + reflexivity. reflexivity. traceEq. econstructor; eauto. eapply match_cont_invariant; eauto. intros. transitivity (Mem.load chunk m0 b 0). -- cgit