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.

1 files changed, 402 insertions, 0 deletions

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.