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.

2 files changed, 10 insertions, 1 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index 0afa7bfb..3920665e 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -51,6 +51,7 @@ Require Allocation.
 Require Tunneling.
 Require Linearize.
 Require CleanupLabels.
+Require Debugvar.
 Require Stacking.
 Require Asmgen.
 (** Proofs of semantic preservation. *)
@@ -71,6 +72,7 @@ Require Allocproof.
 Require Tunnelingproof.
 Require Linearizeproof.
 Require CleanupLabelsproof.
+Require Debugvarproof.
 Require Stackingproof.
 Require Asmgenproof.
 (** Command-line flags. *)
@@ -144,6 +146,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ time "Branch tunneling" Tunneling.tunnel_program
   @@@ time "CFG linearization" Linearize.transf_program
    @@ time "Label cleanup" CleanupLabels.transf_program
+  @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program)
   @@@ time "Mach generation" Stacking.transf_program
    @@ print print_Mach
   @@@ time "Asm generation" Asmgen.transf_program.
@@ -253,7 +256,8 @@ Proof.
   set (p5 := Tunneling.tunnel_program p4) in *.
   destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate.
   set (p7 := CleanupLabels.transf_program p6) in *.
-  destruct (Stacking.transf_program p7) as [p8|] eqn:?; simpl in H; try discriminate.
+  destruct (partial_if debug Debugvar.transf_program p7) as [p71|] eqn:?; simpl in H; try discriminate.
+  destruct (Stacking.transf_program p71) as [p8|] eqn:?; simpl in H; try discriminate.
   apply compose_forward_simulation with (RTL.semantics p1).
     apply total_if_simulation. apply Tailcallproof.transf_program_correct. 
   apply compose_forward_simulation with (RTL.semantics p11).
@@ -278,6 +282,8 @@ Proof.
     apply Linearizeproof.transf_program_correct; auto.
   apply compose_forward_simulation with (Linear.semantics p7).
     apply CleanupLabelsproof.transf_program_correct. 
+  apply compose_forward_simulation with (Linear.semantics p71).
+    eapply partial_if_simulation; eauto. apply Debugvarproof.transf_program_correct.
   apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8).
     apply Stackingproof.transf_program_correct.
     exact Asmgenproof.return_address_exists.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index d0c6686e..2a213350 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -41,3 +41,6 @@ Parameter optim_redundancy: unit -> bool.
 
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
+
+(** Flag -g.  For insertion of debugging information. *)
+Parameter debug: unit -> bool.