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. --- backend/Debugvarproof.v | 402 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 402 insertions(+) create mode 100644 backend/Debugvarproof.v (limited to 'backend/Debugvarproof.v') diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v new file mode 100644 index 00000000..21d8d029 --- /dev/null +++ b/backend/Debugvarproof.v @@ -0,0 +1,402 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for the [Debugvar] pass. *) + +Require Import Coqlib. +Require Import Axioms. +Require Import Maps. +Require Import Iteration. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Op. +Require Import Errors. +Require Import Machregs. +Require Import Locations. +Require Import Conventions. +Require Import Linear. +Require Import Debugvar. + +(** * Relational characterization of the transformation *) + +Inductive match_code: code -> code -> Prop := + | match_code_nil: + match_code nil nil + | match_code_cons: forall i before after c c', + match_code c c' -> + match_code (i :: c) (i :: add_delta_ranges before after c'). + +Remark diff_same: + forall s, diff s s = nil. +Proof. + induction s as [ | [v i] s]; simpl. + auto. + rewrite Pos.compare_refl. rewrite dec_eq_true. auto. +Qed. + +Remark delta_state_same: + forall s, delta_state s s = (nil, nil). +Proof. + destruct s; simpl. rewrite ! diff_same; auto. auto. +Qed. + +Lemma transf_code_match: + forall lm c before, match_code c (transf_code lm before c). +Proof. + intros lm. fix REC 1. destruct c; intros before; simpl. +- constructor. +- assert (DEFAULT: forall before after, + match_code (i :: c) + (i :: add_delta_ranges before after (transf_code lm after c))). + { intros. constructor. apply REC. } + destruct i; auto. destruct c; auto. destruct i; auto. + set (after := get_label l0 lm). + set (c1 := Llabel l0 :: add_delta_ranges before after (transf_code lm after c)). + replace c1 with (add_delta_ranges before before c1). + constructor. constructor. apply REC. + unfold add_delta_ranges. rewrite delta_state_same. auto. +Qed. + +Inductive match_function: function -> function -> Prop := + | match_function_intro: forall f c, + match_code f.(fn_code) c -> + match_function f (mkfunction f.(fn_sig) f.(fn_stacksize) c). + +Lemma transf_function_match: + forall f tf, transf_function f = OK tf -> match_function f tf. +Proof. + unfold transf_function; intros. + destruct (ana_function f) as [lm|]; inv H. + constructor. apply transf_code_match. +Qed. + +Remark find_label_add_delta_ranges: + forall lbl c before after, find_label lbl (add_delta_ranges before after c) = find_label lbl c. +Proof. + intros. unfold add_delta_ranges. + destruct (delta_state before after) as [killed born]. + induction killed as [ | [v i] l]; simpl; auto. + induction born as [ | [v i] l]; simpl; auto. +Qed. + +Lemma find_label_match_rec: + forall lbl c' c tc, + match_code c tc -> + find_label lbl c = Some c' -> + exists before after tc', find_label lbl tc = Some (add_delta_ranges before after tc') /\ match_code c' tc'. +Proof. + induction 1; simpl; intros. +- discriminate. +- destruct (is_label lbl i). + inv H0. econstructor; econstructor; econstructor; eauto. + rewrite find_label_add_delta_ranges. auto. +Qed. + +Lemma find_label_match: + forall f tf lbl c, + match_function f tf -> + find_label lbl f.(fn_code) = Some c -> + exists before after tc, find_label lbl tf.(fn_code) = Some (add_delta_ranges before after tc) /\ match_code c tc. +Proof. + intros. inv H. eapply find_label_match_rec; eauto. +Qed. + +(** * Semantic preservation *) + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. + +Hypothesis TRANSF: transf_program prog = OK tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). + +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (Genv.public_symbol_transf_partial transf_fundef _ TRANSF). + +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). + +Lemma sig_preserved: + forall f tf, + transf_fundef f = OK tf -> + funsig tf = funsig f. +Proof. + unfold transf_fundef, transf_partial_fundef; intros. + destruct f. monadInv H. + exploit transf_function_match; eauto. intros M; inv M; auto. + inv H. reflexivity. +Qed. + +Lemma find_function_translated: + forall ros ls f, + find_function ge ros ls = Some f -> + exists tf, + find_function tge ros ls = Some tf /\ transf_fundef f = OK tf. +Proof. + unfold find_function; intros; destruct ros; simpl. + apply functions_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + apply function_ptr_translated; auto. + congruence. +Qed. + +(** Evaluation of the debug annotations introduced by the transformation. *) + +Lemma can_eval_safe_arg: + forall (rs: locset) sp m (a: builtin_arg loc), + safe_builtin_arg a -> exists v, eval_builtin_arg tge rs sp m a v. +Proof. + induction a; simpl; intros; try contradiction; + try (econstructor; now eauto with barg). + destruct H as [S1 S2]. + destruct (IHa1 S1) as [v1 E1]. destruct (IHa2 S2) as [v2 E2]. + exists (Val.longofwords v1 v2); auto with barg. +Qed. + +Lemma eval_add_delta_ranges: + forall s f sp c rs m before after, + star step tge (State s f sp (add_delta_ranges before after c) rs m) + E0 (State s f sp c rs m). +Proof. + intros. unfold add_delta_ranges. + destruct (delta_state before after) as [killed born]. + induction killed as [ | [v i] l]; simpl. +- induction born as [ | [v i] l]; simpl. ++ apply star_refl. ++ destruct i as [a SAFE]; simpl. + exploit can_eval_safe_arg; eauto. intros [v1 E1]. + eapply star_step; eauto. + econstructor. + constructor. eexact E1. constructor. + simpl; constructor. + simpl; auto. + traceEq. +- eapply star_step; eauto. + econstructor. + constructor. + simpl; constructor. + simpl; auto. + traceEq. +Qed. + +(** Matching between program states. *) + +Inductive match_stackframes: Linear.stackframe -> Linear.stackframe -> Prop := + | match_stackframe_intro: + forall f sp rs c tf tc before after, + match_function f tf -> + match_code c tc -> + match_stackframes + (Stackframe f sp rs c) + (Stackframe tf sp rs (add_delta_ranges before after tc)). + +Inductive match_states: Linear.state -> Linear.state -> Prop := + | match_states_instr: + forall s f sp c rs m tf ts tc + (STACKS: list_forall2 match_stackframes s ts) + (TRF: match_function f tf) + (TRC: match_code c tc), + match_states (State s f sp c rs m) + (State ts tf sp tc rs m) + | match_states_call: + forall s f rs m tf ts, + list_forall2 match_stackframes s ts -> + transf_fundef f = OK tf -> + match_states (Callstate s f rs m) + (Callstate ts tf rs m) + | match_states_return: + forall s rs m ts, + list_forall2 match_stackframes s ts -> + match_states (Returnstate s rs m) + (Returnstate ts rs m). + +Lemma parent_locset_match: + forall s ts, + list_forall2 match_stackframes s ts -> + parent_locset ts = parent_locset s. +Proof. + induction 1; simpl. auto. inv H; auto. +Qed. + +(** The simulation diagram. *) + +Theorem transf_step_correct: + forall s1 t s2, step ge s1 t s2 -> + forall ts1 (MS: match_states s1 ts1), + exists ts2, plus step tge ts1 t ts2 /\ match_states s2 ts2. +Proof. + induction 1; intros ts1 MS; inv MS; try (inv TRC). +- (* getstack *) + econstructor; split. + eapply plus_left. constructor; auto. apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* setstack *) + econstructor; split. + eapply plus_left. constructor; auto. apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* op *) + econstructor; split. + eapply plus_left. + econstructor; eauto. + instantiate (1 := v). rewrite <- H; apply eval_operation_preserved; exact symbols_preserved. + apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* load *) + econstructor; split. + eapply plus_left. + econstructor; eauto. + rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* store *) + econstructor; split. + eapply plus_left. + econstructor; eauto. + rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* call *) + exploit find_function_translated; eauto. intros (tf' & A & B). + econstructor; split. + apply plus_one. + econstructor. eexact A. symmetry; apply sig_preserved; auto. traceEq. + constructor; auto. constructor; auto. constructor; auto. +- (* tailcall *) + exploit find_function_translated; eauto. intros (tf' & A & B). + exploit parent_locset_match; eauto. intros PLS. + econstructor; split. + apply plus_one. + econstructor. eauto. rewrite PLS. eexact A. + symmetry; apply sig_preserved; auto. + inv TRF; eauto. traceEq. + rewrite PLS. constructor; auto. +- (* builtin *) + econstructor; split. + eapply plus_left. + econstructor; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved. eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* label *) + econstructor; split. + eapply plus_left. constructor; auto. apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* goto *) + exploit find_label_match; eauto. intros (before' & after' & tc' & A & B). + econstructor; split. + eapply plus_left. constructor; eauto. apply eval_add_delta_ranges; eauto. traceEq. + constructor; auto. +- (* cond taken *) + exploit find_label_match; eauto. intros (before' & after' & tc' & A & B). + econstructor; split. + eapply plus_left. eapply exec_Lcond_true; eauto. apply eval_add_delta_ranges; eauto. traceEq. + constructor; auto. +- (* cond not taken *) + econstructor; split. + eapply plus_left. eapply exec_Lcond_false; auto. apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* jumptable *) + exploit find_label_match; eauto. intros (before' & after' & tc' & A & B). + econstructor; split. + eapply plus_left. econstructor; eauto. + apply eval_add_delta_ranges. reflexivity. traceEq. + constructor; auto. +- (* return *) + econstructor; split. + apply plus_one. constructor. inv TRF; eauto. traceEq. + rewrite (parent_locset_match _ _ STACKS). constructor; auto. +- (* internal function *) + monadInv H7. rename x into tf. + assert (MF: match_function f tf) by (apply transf_function_match; auto). + inversion MF; subst. + econstructor; split. + apply plus_one. constructor. simpl; eauto. reflexivity. + constructor; auto. +- (* external function *) + monadInv H8. econstructor; split. + apply plus_one. econstructor; eauto. + eapply external_call_symbols_preserved'. eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + constructor; auto. +- (* return *) + inv H3. inv H1. + econstructor; split. + eapply plus_left. econstructor. apply eval_add_delta_ranges. traceEq. + constructor; auto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + exists (Callstate nil tf (Locmap.init Vundef) m0); split. + econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). + rewrite <- H3. apply sig_preserved. auto. + constructor. constructor. auto. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. inv H6. econstructor; eauto. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_plus. + eexact public_preserved. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. +Qed. + +End PRESERVATION. -- cgit