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.

12 files changed, 1030 insertions, 45 deletions

diff --git a/.depend b/.depend
index 4286b08c..889d6a1a 100644
--- a/.depend
+++ b/.depend
@@ -59,7 +59,7 @@ backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified
 $(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/ValueDomain.vo backend/RTL.vo
 backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo
 $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo
-backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo $(ARCH)/SelectOp.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo
+backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo
 $(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo
 backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo
 backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo
@@ -88,6 +88,8 @@ backend/Linearize.vo backend/Linearize.glob backend/Linearize.v.beautified: back
 backend/Linearizeproof.vo backend/Linearizeproof.glob backend/Linearizeproof.v.beautified: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo
 backend/CleanupLabels.vo backend/CleanupLabels.glob backend/CleanupLabels.v.beautified: backend/CleanupLabels.v lib/Coqlib.vo lib/Ordered.vo backend/Linear.vo
 backend/CleanupLabelsproof.vo backend/CleanupLabelsproof.glob backend/CleanupLabelsproof.v.beautified: backend/CleanupLabelsproof.v lib/Coqlib.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/CleanupLabels.vo
+backend/Debugvar.vo backend/Debugvar.glob backend/Debugvar.v.beautified: backend/Debugvar.v lib/Coqlib.vo lib/Axioms.vo lib/Maps.vo lib/Iteration.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Errors.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo
+backend/Debugvarproof.vo backend/Debugvarproof.glob backend/Debugvarproof.v.beautified: backend/Debugvarproof.v lib/Coqlib.vo lib/Axioms.vo lib/Maps.vo lib/Iteration.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo common/Errors.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Debugvar.vo
 backend/Mach.vo backend/Mach.glob backend/Mach.v.beautified: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo
 backend/Bounds.vo backend/Bounds.glob backend/Bounds.v.beautified: backend/Bounds.v lib/Coqlib.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo
 $(ARCH)/Stacklayout.vo $(ARCH)/Stacklayout.glob $(ARCH)/Stacklayout.v.beautified: $(ARCH)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo
@@ -112,7 +114,7 @@ cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.
 cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob cfrontend/SimplExprproof.v.beautified: cfrontend/SimplExprproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
 cfrontend/Clight.vo cfrontend/Clight.glob cfrontend/Clight.v.beautified: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
 cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob cfrontend/ClightBigstep.v.beautified: cfrontend/ClightBigstep.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo
-cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob cfrontend/SimplLocals.v.beautified: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo
+cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob cfrontend/SimplLocals.v.beautified: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo driver/Compopts.vo
 cfrontend/SimplLocalsproof.vo cfrontend/SimplLocalsproof.glob cfrontend/SimplLocalsproof.v.beautified: cfrontend/SimplLocalsproof.v lib/Coqlib.vo common/Errors.vo lib/Ordered.vo common/AST.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/SimplLocals.vo
 cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob cfrontend/Cshmgen.v.beautified: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo
 cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob cfrontend/Cshmgenproof.v.beautified: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo
@@ -120,7 +122,7 @@ cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob cfrontend/Csharpminor.v.beau
 cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob cfrontend/Cminorgen.v.beautified: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo cfrontend/Csharpminor.vo backend/Cminor.vo
 cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob cfrontend/Cminorgenproof.v.beautified: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
 driver/Compopts.vo driver/Compopts.glob driver/Compopts.v.beautified: driver/Compopts.v
-driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Unusedglobproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo driver/Compopts.vo
+driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Debugvar.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Unusedglobproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Debugvarproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo driver/Compopts.vo
 driver/Complements.vo driver/Complements.glob driver/Complements.v.beautified: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
 flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob flocq/Core/Fcore_Raux.v.beautified: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo
 flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob flocq/Core/Fcore_Zaux.v.beautified: flocq/Core/Fcore_Zaux.v
diff --git a/Makefile b/Makefile
index 0a13bf4b..1bf53bff 100644
--- a/Makefile
+++ b/Makefile
@@ -83,6 +83,7 @@ BACKEND=\
   Linear.v Lineartyping.v \
   Linearize.v Linearizeproof.v \
   CleanupLabels.v CleanupLabelsproof.v \
+  Debugvar.v Debugvarproof.v \
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
diff --git a/backend/Debugvar.v b/backend/Debugvar.v
new file mode 100644
index 00000000..314f43fd
--- /dev/null
+++ b/backend/Debugvar.v
@@ -0,0 +1,378 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Computation of live ranges for local variables that carry 
+    debugging information. *)
+
+Require Import Coqlib.
+Require Import Axioms.
+Require Import Maps.
+Require Import Iteration.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Errors.
+Require Import Machregs.
+Require Import Locations.
+Require Import Conventions.
+Require Import Linear.
+
+(** A debug info is a [builtin_arg loc] expression that safely evaluates
+   in any context. *)
+
+Fixpoint safe_builtin_arg {A: Type} (a: builtin_arg A) : Prop :=
+  match a with
+  | BA _ | BA_int _ | BA_long _ | BA_float _ | BA_single _ => True
+  | BA_splitlong hi lo => safe_builtin_arg hi /\ safe_builtin_arg lo
+  | _ => False
+  end.
+
+Definition debuginfo := { a : builtin_arg loc | safe_builtin_arg a }.
+
+(** Normalization of debug info.  Prefer an actual location to a constant.
+    Make sure that the debug info is safe to evaluate in any context. *)
+
+Definition normalize_debug_1 (a: builtin_arg loc) : option debuginfo :=
+  match a with
+  | BA x => Some (exist _ (BA x) I)
+  | BA_int n => Some (exist _ (BA_int n) I)
+  | BA_long n => Some (exist _ (BA_long n) I)
+  | BA_float n => Some (exist _ (BA_float n) I)
+  | BA_single n => Some (exist _ (BA_single n) I)
+  | BA_splitlong (BA hi) (BA lo) => Some (exist _ (BA_splitlong (BA hi) (BA lo)) (conj I I))
+  | _ => None
+  end.
+
+Fixpoint normalize_debug (l: list (builtin_arg loc)) : option debuginfo :=
+  match l with
+  | nil => None
+  | a :: l' =>
+      match a with
+      | BA_int _ | BA_long _ | BA_float _ | BA_single _ =>
+          match normalize_debug l' with
+          | Some i => Some i
+          | None => normalize_debug_1 a
+          end
+      | _ => normalize_debug_1 a
+      end
+  end.
+
+(** * Availability analysis *)
+
+(** This static analysis tracks which locations (registers and stack slots)
+    contain the values of which C local variables.
+
+    The abstraction of the program state at a program point is a list of
+    pairs (variable name, location).  It is kept sorted by increasing name.
+    The location is represented by a safe [builtin_arg loc] expression. *)
+
+Definition avail : Type := list (ident * debuginfo).
+
+(** Operations on [avail] abstract states. *)
+
+Fixpoint set_state (v: ident) (i: debuginfo) (s: avail) : avail :=
+  match s with
+  | nil => (v, i) :: nil
+  | (v', i') as vi' :: s' =>
+      match Pos.compare v v' with
+      | Eq => (v, i) :: s'
+      | Lt => (v, i) :: s
+      | Gt => vi' :: set_state v i s'
+      end
+  end.
+
+Fixpoint remove_state (v: ident) (s: avail) : avail :=
+  match s with
+  | nil => nil
+  | (v', i') as vi' :: s' =>
+      match Pos.compare v v' with
+      | Eq => s'
+      | Lt => s
+      | Gt => vi' :: remove_state v s'
+      end
+  end.
+
+Fixpoint set_debug_info (v: ident) (info: list (builtin_arg loc)) (s: avail) :=
+  match normalize_debug info with
+  | Some a => set_state v a s
+  | None   => remove_state v s
+  end.
+
+(** When the program writes to a register or stack location, some
+  availability information is invalidated. *)
+
+Fixpoint arg_no_overlap (a: builtin_arg loc) (l: loc) : bool :=
+  match a with
+  | BA l' => Loc.diff_dec l' l
+  | BA_splitlong hi lo => arg_no_overlap hi l && arg_no_overlap lo l
+  | _ => true
+  end.
+
+Definition kill (l: loc) (s: avail) : avail :=
+  List.filter (fun vi => arg_no_overlap (proj1_sig (snd vi)) l) s.
+
+Fixpoint kill_res (r: builtin_res mreg) (s: avail) : avail :=
+  match r with
+  | BR r => kill (R r) s
+  | BR_none => s
+  | BR_splitlong hi lo => kill_res hi (kill_res lo s)
+  end.
+
+(** Likewise when a function call takes place. *)
+
+Fixpoint arg_preserved (a: builtin_arg loc) : bool :=
+  match a with
+  | BA (R r) => negb (List.In_dec mreg_eq r destroyed_at_call)
+  | BA (S _ _ _) => true
+  | BA_splitlong hi lo => arg_preserved hi && arg_preserved lo
+  | _ => true
+  end.
+
+Definition kill_at_call (s: avail) : avail :=
+  List.filter (fun vi => arg_preserved (proj1_sig(snd vi))) s.
+
+(** The join of two availability states is the intersection of the
+    corresponding lists. *)
+
+Definition eq_arg (a1 a2: builtin_arg loc) : {a1=a2} + {a1<>a2}.
+Proof.
+  generalize Loc.eq ident_eq Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec chunk_eq;
+  decide equality.
+Defined.
+Global Opaque eq_arg.
+
+Definition eq_debuginfo (i1 i2: debuginfo) : {i1=i2} + {i1 <> i2}.
+Proof.
+  destruct (eq_arg (proj1_sig i1) (proj1_sig i2)).
+  left. destruct i1, i2; simpl in *. subst x0. f_equal. apply proof_irr.
+  right. congruence. 
+Defined.
+Global Opaque eq_debuginfo.
+
+Fixpoint join (s1: avail) (s2: avail) {struct s1} : avail :=
+  match s1 with
+  | nil => nil
+  | (v1, i1) as vi1 :: s1' =>
+      let fix join2 (s2: avail) : avail :=
+        match s2 with
+        | nil => nil
+        | (v2, i2) as vi2 :: s2' =>
+            match Pos.compare v1 v2 with
+            | Eq => if eq_debuginfo i1 i2 then vi1 :: join s1' s2' else join s1' s2'
+            | Lt => join s1' s2
+            | Gt => join2 s2'
+            end
+        end
+      in join2 s2
+  end.
+
+Definition eq_state (s1 s2: avail) : {s1=s2} + {s1<>s2}.
+Proof.
+  apply list_eq_dec. decide equality. apply eq_debuginfo. apply ident_eq. 
+Defined.
+Global Opaque eq_state.
+
+Definition top : avail := nil.
+
+(** Record availability information at labels. *)
+
+Definition labelmap := (PTree.t avail * bool)%type.
+
+Definition get_label (lbl: label) (lm: labelmap) : option avail :=
+  PTree.get lbl (fst lm).
+
+Definition update_label (lbl: label) (s1: avail) (lm: labelmap) :
+                                  labelmap * avail :=
+  match get_label lbl lm with
+  | None =>
+      ((PTree.set lbl s1 (fst lm), true), s1)
+  | Some s2 =>
+      let s := join s1 s2 in
+      if eq_state s s2
+      then (lm, s2)
+      else ((PTree.set lbl s (fst lm), true), s)
+  end.
+
+Fixpoint update_labels (lbls: list label) (s: avail) (lm: labelmap) :
+                                  labelmap :=
+  match lbls with
+  | nil => lm
+  | lbl1 :: lbls =>
+      update_labels lbls s (fst (update_label lbl1 s lm))
+  end.
+
+(** Classification of builtins *)
+
+Definition is_debug_setvar (ef: external_function) :=
+  match ef with
+  | EF_debug 2%positive txt targs => Some txt
+  | _ => None
+  end.
+
+Definition is_builtin_debug_setvar (i: instruction) :=
+  match i with
+  | Lbuiltin ef args BR_none => is_debug_setvar ef
+  | _ => None
+  end.
+
+(** The transfer function for the forward dataflow analysis. *)
+
+Definition transfer (lm: labelmap) (before: option avail) (i: instruction):
+                                      labelmap * option avail :=
+  match before with
+  | None =>
+      match i with
+      | Llabel lbl => (lm, get_label lbl lm)
+      | _ => (lm, None)
+      end
+  | Some s =>
+      match i with
+      | Lgetstack sl ofs ty rd =>
+          (lm, Some (kill (R rd) s))
+      | Lsetstack rs sl ofs ty =>
+          (lm, Some (kill (S sl ofs ty) s))
+      | Lop op args dst =>
+          (lm, Some (kill (R dst) s))
+      | Lload chunk addr args dst =>
+          (lm, Some (kill (R dst) s))
+      | Lstore chunk addr args src =>
+          (lm, before)
+      | Lcall sg ros =>
+          (lm, Some (kill_at_call s))
+      | Ltailcall sg ros =>
+          (lm, None)
+      | Lbuiltin ef args res =>
+          let s' :=
+            match is_debug_setvar ef with
+            | Some v => set_debug_info v args s
+            | None   => s
+            end in
+          (lm, Some (kill_res res s'))
+      | Llabel lbl =>
+          let (lm1, s1) := update_label lbl s lm in
+          (lm1, Some s1)
+      | Lgoto lbl =>
+          let (lm1, s1) := update_label lbl s lm in
+          (lm1, None)
+      | Lcond cond args lbl =>
+          let (lm1, s1) := update_label lbl s lm in
+          (lm1, before)
+      | Ljumptable r lbls =>
+          (update_labels lbls s lm, None)
+      | Lreturn =>
+          (lm, None)
+      end
+  end.
+
+(** One pass of forward analysis over the code [c].  
+    Return an updated label map. *)
+
+Fixpoint ana_code (lm: labelmap) (before: option avail) (c: code) : labelmap :=
+  match c with
+  | nil => lm
+  | i :: c =>
+      let (lm1, after) := transfer lm before i in
+      ana_code lm1 after c
+  end.
+
+(** Iterate [ana_code] until the label map is stable. *)
+
+Definition ana_iter (c: code) (lm: labelmap) : labelmap + labelmap :=
+  let lm' := ana_code (fst lm, false) (Some top) c in
+  if snd lm' then inr _ lm' else inl _ lm.
+
+Definition ana_function (f: function) : option labelmap :=
+  PrimIter.iterate _ _ (ana_iter f.(fn_code)) (PTree.empty _, false).
+
+(** * Code transformation *)
+
+(** Compute the changes between two abstract states *)
+
+Fixpoint diff (s1 s2: avail) {struct s1} : avail :=
+  match s1 with
+  | nil => nil
+  | (v1, i1) as vi1 :: s1' =>
+      let fix diff2 (s2: avail) : avail :=
+        match s2 with
+        | nil => s1
+        | (v2, i2) :: s2' =>
+            match Pos.compare v1 v2 with
+            | Eq => if eq_debuginfo i1 i2 then diff s1' s2' else vi1 :: diff s1' s2'
+            | Lt => vi1 :: diff s1' s2
+            | Gt => diff2 s2'
+            end
+        end
+      in diff2 s2
+  end.
+
+Definition delta_state (before after: option avail) : avail * avail :=
+  match before, after with
+  | None, None => (nil, nil)
+  | Some b, None => (b, nil)
+  | None, Some a => (nil, a)
+  | Some b, Some a => (diff b a, diff a b)
+  end.
+
+(** Insert debug annotations at the beginning and end of live ranges
+    of locations that correspond to source local variables. *)
+
+Definition add_start_range (vi: ident * debuginfo) (c: code) : code :=
+  let (v, i) := vi in
+  Lbuiltin (EF_debug 3%positive v nil) (proj1_sig i :: nil) BR_none :: c.
+
+Definition add_end_range (vi: ident * debuginfo) (c: code) : code :=
+  let (v, i) := vi in
+  Lbuiltin (EF_debug 4%positive v nil) nil BR_none :: c.
+
+Definition add_delta_ranges (before after: option avail) (c: code) : code :=
+  let (killed, born) := delta_state before after in
+  List.fold_right add_end_range (List.fold_right add_start_range c born) killed.
+
+Fixpoint skip_debug_setvar (lm: labelmap) (before: option avail) (c: code) :=
+  match c with
+  | nil => before
+  | i :: c' =>
+      match is_builtin_debug_setvar i with
+      | Some _ => skip_debug_setvar lm (snd (transfer lm before i)) c'
+      | None => before
+      end
+  end.
+
+Fixpoint transf_code (lm: labelmap) (before: option avail) (c: code) : code :=
+  match c with
+  | nil => nil
+  | Lgoto lbl1 :: Llabel lbl2 :: c' =>
+      (* This special case avoids some redundant start/end annotations *)
+      let after := get_label lbl2 lm in
+      Lgoto lbl1 :: Llabel lbl2 ::
+      add_delta_ranges before after (transf_code lm after c')
+  | i :: c' =>
+      let after := skip_debug_setvar lm (snd (transfer lm before i)) c' in
+      i :: add_delta_ranges before after (transf_code lm after c')
+  end.
+
+Local Open Scope string_scope.
+
+Definition transf_function (f: function) : res function :=
+  match ana_function f with
+  | None => Error (msg "Debugvar: analysis diverges")
+  | Some lm =>
+      OK (mkfunction f.(fn_sig) f.(fn_stacksize)
+                     (transf_code lm (Some top) f.(fn_code)))
+  end.
+
+Definition transf_fundef (fd: fundef) : res fundef :=
+  AST.transf_partial_fundef transf_function fd.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
+
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.
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 883b5477..67e53aea 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -263,16 +263,28 @@ let print_annot_text print_preg sp_reg_name oc txt args =
 let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
 
 let print_debug_info comment print_line print_preg sp_name oc kind txt args =
-  if kind = 1 && Str.string_match re_file_line txt 0 then begin
-    print_line oc (Str.matched_group 1 txt)
-                  (int_of_string (Str.matched_group 2 txt))
-  end else begin
-    fprintf oc "%s debug%d: %s" comment kind txt;
+  let print_debug_args oc args =
     List.iter
       (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a)
-      args;
-    fprintf oc "\n"
-  end
+      args in
+  match kind with
+  | 1 ->  (* line number *)
+      if Str.string_match re_file_line txt 0 then
+        print_line oc (Str.matched_group 1 txt)
+                      (int_of_string (Str.matched_group 2 txt))
+  | 2 ->  (* assignment to local variable, not useful *)
+      ()
+  | 3 ->  (* beginning of live range for local variable *)
+      fprintf oc "%s debug: start live range %s =%a\n"
+                 comment txt print_debug_args args
+  | 4 ->  (* end of live range for local variable *)
+      fprintf oc "%s debug: end live range %s\n"
+                 comment txt
+  | 5 ->  (* local variable preallocated in stack *)
+      fprintf oc "%s debug: %s resides at%a\n"
+                 comment txt print_debug_args args
+  | _ ->
+      ()
 					    
 (** Inline assembly *)
 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 8b30b44f..effb0c7d 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -130,7 +130,10 @@ Inductive wt_instr : instruction -> Prop :=
       wt_instr (Itailcall sig ros args)
   | wt_Ibuiltin:
       forall ef args res s,
-      map type_of_builtin_arg args = (ef_sig ef).(sig_args) ->
+      match ef with
+      | EF_annot _ _ | EF_debug _ _ _ => True
+      | _ => map type_of_builtin_arg args = (ef_sig ef).(sig_args)
+      end ->
       type_of_builtin_res res = proj_sig_res (ef_sig ef) ->
       valid_successor s ->
       wt_instr (Ibuiltin ef args res s)
@@ -301,7 +304,11 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
   | Ibuiltin ef args res s =>
       let sig := ef_sig ef in
       do x <- check_successor s;
-      do e1 <- type_builtin_args e args sig.(sig_args);
+      do e1 <- 
+        match ef with
+        | EF_annot _ _ | EF_debug _ _ _ => OK e
+        | _ => type_builtin_args e args sig.(sig_args)
+        end;
       type_builtin_res e1 res (proj_sig_res sig)
  | Icond cond args s1 s2 =>
       do x1 <- check_successor s1;
@@ -462,6 +469,8 @@ Proof.
   destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
   destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
   eauto with ty.
+- (* builtin *)
+  destruct e0; try monadInv EQ1; eauto with ty.
 - (* jumptable *)
   destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2.
   eauto with ty.
@@ -517,7 +526,7 @@ Proof.
   apply tailcall_is_possible_correct; auto.
 - (* builtin *)
   constructor.
-  eapply type_builtin_args_sound; eauto with ty.
+  destruct e0; auto; eapply type_builtin_args_sound; eauto with ty.
   eapply type_builtin_res_sound; eauto.
   eauto with ty.
 - (* cond *)
@@ -691,10 +700,12 @@ Proof.
 - (* builtin *)
   exploit type_builtin_args_complete; eauto. instantiate (1 := args). intros [e1 [A B]].
   exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]].
-  exists e2; split; auto. 
+  exploit type_builtin_res_complete. eexact H. instantiate (1 := res). intros [e3 [E F]].
   rewrite check_successor_complete by auto. simpl.
-  rewrite <- H0; rewrite A; simpl.
-  rewrite <- H1; auto.
+  exists (match ef with EF_annot _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split.
+  rewrite H1 in C, E. 
+  destruct ef; try (rewrite <- H0; rewrite A); simpl; auto.
+  destruct ef; auto.
 - (* cond *)
   exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
   exists e1; split; auto.
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 52ee8377..7fc69324 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -22,6 +22,7 @@ Require Import AST.
 Require Import Ctypes.
 Require Import Cop.
 Require Import Clight.
+Require Compopts.
 
 Open Scope error_monad_scope.
 Open Scope string_scope.
@@ -54,6 +55,23 @@ Definition make_cast (a: expr) (tto: type) : expr :=
   | _ => Ecast a tto
   end.
 
+(** Insertion of debug annotations *)
+
+Definition Sdebug_temp (id: ident) (ty: type) :=
+  Sbuiltin None (EF_debug 2%positive id (typ_of_type ty :: nil))
+                (Tcons (typeconv ty) Tnil)
+                (Etempvar id ty :: nil).
+
+Definition Sdebug_var (id: ident) (ty: type) :=
+  Sbuiltin None (EF_debug 5%positive id (AST.Tint :: nil))
+                (Tcons (Tpointer ty noattr) Tnil)
+                (Eaddrof (Evar id ty) (Tpointer ty noattr) :: nil).
+
+Definition Sset_debug (id: ident) (ty: type) (a: expr) :=
+  if Compopts.debug tt
+  then Ssequence (Sset id (make_cast a ty)) (Sdebug_temp id ty)
+  else Sset id (make_cast a ty).
+
 (** Rewriting of expressions and statements. *)
 
 Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr :=
@@ -94,7 +112,7 @@ Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement :=
   | Sassign a1 a2 =>
       match is_liftable_var cenv a1 with
       | Some id =>
-          OK (Sset id (make_cast (simpl_expr cenv a2) (typeof a1)))
+          OK (Sset_debug id (typeof a1) (simpl_expr cenv a2))
       | None =>
           OK (Sassign (simpl_expr cenv a1) (simpl_expr cenv a2))
       end
@@ -225,6 +243,22 @@ Definition cenv_for (f: function) : compilenv :=
 
 (** Transform a function *)
 
+Definition add_debug_var (id_ty: ident * type) (s: statement) :=
+  let (id, ty) := id_ty in Ssequence (Sdebug_var id ty) s.
+
+Definition add_debug_vars (vars: list (ident * type)) (s: statement) :=
+  if Compopts.debug tt
+  then List.fold_right add_debug_var s vars
+  else s.
+
+Definition add_debug_param (id_ty: ident * type) (s: statement) :=
+  let (id, ty) := id_ty in Ssequence (Sdebug_temp id ty) s.
+
+Definition add_debug_params (params: list (ident * type)) (s: statement) :=
+  if Compopts.debug tt
+  then List.fold_right add_debug_param s params
+  else s.
+
 Definition remove_lifted (cenv: compilenv) (vars: list (ident * type)) :=
   List.filter (fun id_ty => negb (VSet.mem (fst id_ty) cenv)) vars.
 
@@ -235,12 +269,16 @@ Definition transf_function (f: function) : res function :=
   let cenv := cenv_for f in
   assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps)));
   do body' <- simpl_stmt cenv f.(fn_body);
+  let vars' := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars)) in
+  let temps' := add_lifted cenv f.(fn_vars) f.(fn_temps) in
   OK {| fn_return := f.(fn_return);
         fn_callconv := f.(fn_callconv);
         fn_params := f.(fn_params);
-        fn_vars := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars));
-        fn_temps := add_lifted cenv f.(fn_vars) f.(fn_temps);
-        fn_body := store_params cenv f.(fn_params) body' |}.
+        fn_vars := vars';
+        fn_temps := temps';
+        fn_body := add_debug_params f.(fn_params) 
+                      (store_params cenv f.(fn_params)
+                        (add_debug_vars vars' body')) |}.
 
 (** Whole-program transformation *)
 
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). 
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.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index ecd2853a..6327f871 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -100,6 +100,8 @@ Extract Constant Compopts.optim_redundancy =>
   "fun _ -> !Clflags.option_fredundancy".
 Extract Constant Compopts.thumb =>
   "fun _ -> !Clflags.option_mthumb".
+Extract Constant Compopts.debug =>
+  "fun _ -> !Clflags.option_g".
 
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 9e4babb7..439dd2b0 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -648,7 +648,7 @@ module Target(System: SYSTEM):TARGET =
           begin match ef with
           | EF_annot(txt, targs) ->
               fprintf oc "%s annotation: " comment;
-              print_annot_text preg_annot "%esp" oc (extern_atom txt) args
+              print_annot_text preg "%esp" oc (extern_atom txt) args
           | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg "%esp" oc
                                (P.to_int kind) (extern_atom txt) args