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. --- .depend | 8 +- Makefile | 1 + backend/Debugvar.v | 378 ++++++++++++++++++++++++++++++++++++++++ backend/Debugvarproof.v | 402 +++++++++++++++++++++++++++++++++++++++++++ backend/PrintAsmaux.ml | 28 ++- backend/RTLtyping.v | 23 ++- cfrontend/SimplLocals.v | 46 ++++- cfrontend/SimplLocalsproof.v | 174 ++++++++++++++++--- driver/Compiler.v | 8 +- driver/Compopts.v | 3 + extraction/extraction.v | 2 + ia32/TargetPrinter.ml | 2 +- 12 files changed, 1030 insertions(+), 45 deletions(-) create mode 100644 backend/Debugvar.v create mode 100644 backend/Debugvarproof.v 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 -- cgit