diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Debugvar.v | 378 | ||||
| -rw-r--r-- | backend/Debugvarproof.v | 402 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 28 | ||||
| -rw-r--r-- | backend/RTLtyping.v | 23 |
4 files changed, 817 insertions, 14 deletions
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. |