diff options
| -rw-r--r-- | .depend | 5 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | backend/CleanupLabels.v | 75 | ||||
| -rw-r--r-- | backend/CleanupLabelsproof.v | 336 | ||||
| -rw-r--r-- | backend/CleanupLabelstyping.v | 60 | ||||
| -rw-r--r-- | cparser/Ceval.ml | 1 | ||||
| -rw-r--r-- | driver/Compiler.v | 14 | ||||
| -rw-r--r-- | ia32/Asm.v | 23 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 19 |
9 files changed, 507 insertions, 27 deletions
@@ -65,6 +65,9 @@ backend/LTLintyping.vo backend/LTLintyping.glob: backend/LTLintyping.v lib/Coqli backend/Linearize.vo backend/Linearize.glob: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo backend/Linearizeproof.vo backend/Linearizeproof.glob: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.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/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo backend/Linearizetyping.vo backend/Linearizetyping.glob: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo +backend/CleanupLabels.vo backend/CleanupLabels.glob: backend/CleanupLabels.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/LTLin.vo +backend/CleanupLabelsproof.vo backend/CleanupLabelsproof.glob: backend/CleanupLabelsproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.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/LTLin.vo backend/CleanupLabels.vo +backend/CleanupLabelstyping.vo backend/CleanupLabelstyping.glob: backend/CleanupLabelstyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/CleanupLabels.vo backend/LTLintyping.vo backend/Linear.vo backend/Linear.glob: backend/Linear.v lib/Coqlib.vo lib/Maps.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/LTL.vo backend/Conventions.vo backend/Lineartyping.vo backend/Lineartyping.glob: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Conventions.vo backend/Parallelmove.vo backend/Parallelmove.glob: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo @@ -98,5 +101,5 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.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 backend/Cminor.vo common/Smallstep.vo cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: 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/Memdata.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/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo driver/Complements.glob: 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/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -60,6 +60,7 @@ BACKEND=\ Tunneling.v Tunnelingproof.v Tunnelingtyping.v \ LTLin.v LTLintyping.v \ Linearize.v Linearizeproof.v Linearizetyping.v \ + CleanupLabels.v CleanupLabelsproof.v CleanupLabelstyping.v \ Linear.v Lineartyping.v \ Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \ Mach.v Machtyping.v \ diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v new file mode 100644 index 0000000..7401abc --- /dev/null +++ b/backend/CleanupLabels.v @@ -0,0 +1,75 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Removal of useless labels introduced by the linearization pass. + + The linearization pass introduces one label for each node of the + control-flow graph. Many of these labels are never branched to, + which can complicate further optimizations over linearized code. + (There are no such optimizations yet.) In preparation for these + further optimizations, and to make the generated LTLin code + better-looking, the present pass removes labels that cannot be + branched to. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Ordered. +Require Import FSets. +Require FSetAVL. +Require Import LTLin. + +Module Labelset := FSetAVL.Make(OrderedPositive). + +(** Compute the set of labels that are mentioned in branch instructions. *) + +Definition add_label_branched_to (ls: Labelset.t) (i: instruction) := + match i with + | Lgoto lbl => Labelset.add lbl ls + | Lcond cond args lbl => Labelset.add lbl ls + | Ljumptable arg tbl => List.fold_right Labelset.add ls tbl + | _ => ls + end. + +Definition labels_branched_to (c: code) : Labelset.t := + List.fold_left add_label_branched_to c Labelset.empty. + +(** Remove label declarations for labels that are not in + the [bto] (branched-to) set. *) + +Fixpoint remove_unused_labels (bto: Labelset.t) (c: code) : code := + match c with + | nil => nil + | Llabel lbl :: c' => + if Labelset.mem lbl bto + then Llabel lbl :: remove_unused_labels bto c' + else remove_unused_labels bto c' + | i :: c' => + i :: remove_unused_labels bto c' + end. + +Definition cleanup_labels (c: code) := + remove_unused_labels (labels_branched_to c) c. + +(** Entry points *) + +Definition transf_function (f: function) : function := + mkfunction + (fn_sig f) + (fn_params f) + (fn_stacksize f) + (cleanup_labels (fn_code f)). + +Definition transf_fundef (f: fundef) : fundef := + AST.transf_fundef transf_function f. + +Definition transf_program (p: program) : program := + AST.transform_program transf_fundef p. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v new file mode 100644 index 0000000..6201306 --- /dev/null +++ b/backend/CleanupLabelsproof.v @@ -0,0 +1,336 @@ +(* *********************************************************************) +(* *) +(* 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 clean-up of labels *) + +Require Import Coqlib. +Require Import Maps. +Require Import Ordered. +Require Import FSets. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Errors. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import LTLin. +Require Import CleanupLabels. + +Module LabelsetFacts := FSetFacts.Facts(Labelset). + +Section CLEANUP. + +Variable prog: program. +Let tprog := transf_program prog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.find_symbol_transf. +Qed. + +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.find_var_info_transf. +Qed. + +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_transf transf_fundef _ _ H). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: fundef), + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). +Qed. + +Lemma sig_function_translated: + forall f, + funsig (transf_fundef f) = funsig f. +Proof. + intros. destruct f; reflexivity. +Qed. + +Lemma find_function_translated: + forall ros ls f, + find_function ge ros ls = Some f -> + find_function tge ros ls = Some (transf_fundef f). +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. + +(** Correctness of [labels_branched_to]. *) + +Definition instr_branches_to (i: instruction) (lbl: label) : Prop := + match i with + | Lgoto lbl' => lbl = lbl' + | Lcond cond args lbl' => lbl = lbl' + | Ljumptable arg tbl => In lbl tbl + | _ => False + end. + +Remark add_label_branched_to_incr: + forall ls i, Labelset.Subset ls (add_label_branched_to ls i). +Proof. + intros; red; intros; destruct i; simpl; auto. + apply Labelset.add_2; auto. + apply Labelset.add_2; auto. + revert H; induction l0; simpl. auto. intros; apply Labelset.add_2; auto. +Qed. + +Remark add_label_branched_to_contains: + forall ls i lbl, + instr_branches_to i lbl -> + Labelset.In lbl (add_label_branched_to ls i). +Proof. + destruct i; simpl; intros; try contradiction. + apply Labelset.add_1; auto. + apply Labelset.add_1; auto. + revert H. induction l0; simpl; intros. + contradiction. + destruct H. apply Labelset.add_1; auto. apply Labelset.add_2; auto. +Qed. + +Lemma labels_branched_to_correct: + forall c i lbl, + In i c -> instr_branches_to i lbl -> Labelset.In lbl (labels_branched_to c). +Proof. + intros. + assert (forall c' bto, + Labelset.Subset bto (fold_left add_label_branched_to c' bto)). + induction c'; intros; simpl; red; intros. + auto. + apply IHc'. apply add_label_branched_to_incr; auto. + + assert (forall c' bto, + In i c' -> Labelset.In lbl (fold_left add_label_branched_to c' bto)). + induction c'; simpl; intros. + contradiction. + destruct H2. + subst a. apply H1. apply add_label_branched_to_contains; auto. + apply IHc'; auto. + + unfold labels_branched_to. auto. +Qed. + +(** Commutation with [find_label]. *) + +Lemma find_label_commut: + forall lbl bto, + Labelset.In lbl bto -> + forall c c', + find_label lbl c = Some c' -> + find_label lbl (remove_unused_labels bto c) = Some (remove_unused_labels bto c'). +Proof. + induction c; simpl; intros. + congruence. + unfold is_label in H0. destruct a; simpl; auto. + destruct (peq lbl l). subst l. inv H0. + rewrite Labelset.mem_1; auto. + simpl. rewrite peq_true. auto. + destruct (Labelset.mem l bto); auto. simpl. rewrite peq_false; auto. +Qed. + +Corollary find_label_translated: + forall f i c' lbl c, + incl (i :: c') (fn_code f) -> + find_label lbl (fn_code f) = Some c -> + instr_branches_to i lbl -> + find_label lbl (fn_code (transf_function f)) = + Some (remove_unused_labels (labels_branched_to (fn_code f)) c). +Proof. + intros. unfold transf_function; unfold cleanup_labels; simpl. + apply find_label_commut. eapply labels_branched_to_correct; eauto. + apply H; auto with coqlib. + auto. +Qed. + +Lemma find_label_incl: + forall lbl c c', find_label lbl c = Some c' -> incl c' c. +Proof. + induction c; simpl; intros. + discriminate. + destruct (is_label lbl a). inv H; auto with coqlib. auto with coqlib. +Qed. + +(** Correctness of clean-up *) + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro: + forall res f sp ls c, + incl c f.(fn_code) -> + match_stackframes + (Stackframe res f sp ls c) + (Stackframe res (transf_function f) sp ls + (remove_unused_labels (labels_branched_to f.(fn_code)) c)). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s f sp c ls m ts + (STACKS: list_forall2 match_stackframes s ts) + (INCL: incl c f.(fn_code)), + match_states (State s f sp c ls m) + (State ts (transf_function f) sp (remove_unused_labels (labels_branched_to f.(fn_code)) c) ls m) + | match_states_call: + forall s f ls m ts, + list_forall2 match_stackframes s ts -> + match_states (Callstate s f ls m) + (Callstate ts (transf_fundef f) ls m) + | match_states_return: + forall s ls m ts, + list_forall2 match_stackframes s ts -> + match_states (Returnstate s ls m) + (Returnstate ts ls m). + +Definition measure (st: state) : nat := + match st with + | State s f sp c ls m => List.length c + | _ => O + end. + +Theorem transf_step_correct: + forall s1 t s2, step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + (exists s2', step tge s1' t s2' /\ match_states s2 s2') + \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. +Proof. + induction 1; intros; inv MS; simpl. +(* Lop *) + left; econstructor; split. + econstructor; eauto. instantiate (1 := v). rewrite <- H. + apply eval_operation_preserved. exact symbols_preserved. + econstructor; eauto with coqlib. +(* Lload *) + left; econstructor; split. + econstructor; eauto. rewrite <- H. + apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto with coqlib. +(* Lstore *) + left; econstructor; split. + econstructor; eauto. rewrite <- H. + apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto with coqlib. +(* Lcall *) + left; econstructor; split. + econstructor. eapply find_function_translated; eauto. + symmetry; apply sig_function_translated. + econstructor; eauto. constructor; auto. constructor; eauto with coqlib. +(* Ltailcall *) + left; econstructor; split. + econstructor. eapply find_function_translated; eauto. + symmetry; apply sig_function_translated. + simpl. eauto. + econstructor; eauto. +(* Lbuiltin *) + left; econstructor; split. + econstructor; eauto. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. +(* Llabel *) + case_eq (Labelset.mem lbl (labels_branched_to (fn_code f))); intros. + (* not eliminated *) + left; econstructor; split. + constructor. + econstructor; eauto with coqlib. + (* eliminated *) + right. split. omega. split. auto. econstructor; eauto with coqlib. +(* Lgoto *) + left; econstructor; split. + econstructor. eapply find_label_translated; eauto. red; auto. + econstructor; eauto. eapply find_label_incl; eauto. +(* Lcond taken *) + left; econstructor; split. + econstructor. auto. eapply find_label_translated; eauto. red; auto. + econstructor; eauto. eapply find_label_incl; eauto. +(* Lcond not taken *) + left; econstructor; split. + eapply exec_Lcond_false; eauto. + econstructor; eauto with coqlib. +(* Ljumptable *) + left; econstructor; split. + econstructor. eauto. eauto. eapply find_label_translated; eauto. + red. eapply list_nth_z_in; eauto. + econstructor; eauto. eapply find_label_incl; eauto. +(* Lreturn *) + left; econstructor; split. + econstructor; eauto. + econstructor; eauto with coqlib. +(* internal function *) + left; econstructor; split. + econstructor; simpl; eauto. + econstructor; eauto with coqlib. +(* external function *) + left; econstructor; split. + econstructor; eauto. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. +(* return *) + inv H3. inv H1. left; econstructor; split. + econstructor; eauto. + econstructor; eauto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inv H. + econstructor; split. + eapply initial_state_intro with (f := transf_fundef f). + eapply Genv.init_mem_transf; eauto. + rewrite symbols_preserved; eauto. + apply function_ptr_translated; auto. + rewrite sig_function_translated. auto. + constructor; auto. constructor. +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 H4. constructor. +Qed. + +Theorem transf_program_correct: + forall (beh: program_behavior), not_wrong beh -> + exec_program prog beh -> LTLin.exec_program tprog beh. +Proof. + unfold exec_program; intros. + eapply simulation_opt_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. +Qed. + +End CLEANUP. + diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v new file mode 100644 index 0000000..ea9de86 --- /dev/null +++ b/backend/CleanupLabelstyping.v @@ -0,0 +1,60 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Type preservation for the CleanupLabels pass *) + +Require Import Coqlib. +Require Import Maps. +Require Import Errors. +Require Import AST. +Require Import Op. +Require Import Locations. +Require Import LTLin. +Require Import CleanupLabels. +Require Import LTLintyping. + +Lemma in_remove_unused_labels: + forall bto i c, In i (remove_unused_labels bto c) -> In i c. +Proof. + induction c; simpl. + auto. + destruct a; simpl; intuition. + destruct (Labelset.mem l bto); simpl in H; intuition. +Qed. + +Lemma wt_transf_function: + forall f, + wt_function f -> + wt_function (transf_function f). +Proof. + intros. inv H. constructor; simpl; auto. + unfold cleanup_labels; red; intros. + apply wt_instrs. eapply in_remove_unused_labels; eauto. +Qed. + +Lemma wt_transf_fundef: + forall f, + wt_fundef f -> + wt_fundef (transf_fundef f). +Proof. + induction 1. constructor. constructor. apply wt_transf_function; auto. +Qed. + +Lemma program_typing_preserved: + forall p, + wt_program p -> + wt_program (transf_program p). +Proof. + intros; red; intros. + exploit transform_program_function; eauto. intros [f1 [A B]]. subst f. + apply wt_transf_fundef. eapply H; eauto. +Qed. diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 1630503..87b50e0 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -116,6 +116,7 @@ let unop env op tyres ty v = | Oplus, TInt _, I n -> I n | Oplus, TFloat _, F n -> F n | Olognot, _, _ -> if boolean_value v then I 0L else I 1L + | Onot, _, I n -> I (Int64.lognot n) | _ -> raise Notconst in cast env ty tyres res diff --git a/driver/Compiler.v b/driver/Compiler.v index cf05b3c..bde6308 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -49,6 +49,7 @@ Require CSE. Require Allocation. Require Tunneling. Require Linearize. +Require CleanupLabels. Require Reload. Require Stacking. Require Asmgen. @@ -74,6 +75,8 @@ Require Tunnelingproof. Require Tunnelingtyping. Require Linearizeproof. Require Linearizetyping. +Require CleanupLabelsproof. +Require CleanupLabelstyping. Require Reloadproof. Require Reloadtyping. Require Stackingproof. @@ -142,6 +145,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@@ Allocation.transf_fundef @@ Tunneling.tunnel_fundef @@@ Linearize.transf_fundef + @@ CleanupLabels.transf_fundef @@ print print_LTLin @@ Reload.transf_fundef @@@ Stacking.transf_fundef @@ -305,13 +309,17 @@ Proof. repeat rewrite transform_program_print_identity in *. subst. exploit transform_partial_program_identity; eauto. intro EQ. subst. - generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved - Linearizetyping.program_typing_preserved Reloadtyping.program_typing_preserved + generalize Alloctyping.program_typing_preserved + Tunnelingtyping.program_typing_preserved + Linearizetyping.program_typing_preserved + CleanupLabelstyping.program_typing_preserved + Reloadtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. eapply Asmgenproof.transf_program_correct; eauto 6. - eapply Stackingproof.transf_program_correct; eauto. + eapply Stackingproof.transf_program_correct; eauto 6. eapply Reloadproof.transf_program_correct; eauto. + eapply CleanupLabelsproof.transf_program_correct; eauto. eapply Linearizeproof.transf_program_correct; eauto. eapply Tunnelingproof.transf_program_correct; eauto. eapply Allocproof.transf_program_correct; eauto. @@ -399,7 +399,9 @@ Inductive outcome: Type := | Stuck: outcome. (** Manipulations over the [PC] register: continuing with the next - instruction ([nextinstr]) or branching to a label ([goto_label]). *) + instruction ([nextinstr]) or branching to a label ([goto_label]). + [nextinstr_nf] is a variant of [nextinstr] that sets condition flags + to [Vundef] in addition to incrementing the [PC]. *) Definition nextinstr (rs: regset) := rs#PC <- (Val.add rs#PC Vone). @@ -438,11 +440,18 @@ Definition exec_store (chunk: memory_chunk) (m: mem) that correspond to actual IA32 instructions, the cases are straightforward transliterations of the informal descriptions given in the IA32 reference manuals. For pseudo-instructions, - refer to the informal descriptions given above. Note that - we set to [Vundef] the registers used as temporaries by the - expansions of the pseudo-instructions, so that the IA32 code - we generate cannot use those registers to hold values that - must survive the execution of the pseudo-instruction. + refer to the informal descriptions given above. + + Note that we set to [Vundef] the registers used as temporaries by + the expansions of the pseudo-instructions, so that the IA32 code + we generate cannot use those registers to hold values that must + survive the execution of the pseudo-instruction. + + Concerning condition flags, the comparison instructions set them + accurately; other instructions (moves, [lea]) preserve them; + and all other instruction set those flags to [Vundef], to reflect + the fact that the processor updates some or all of those flags, + but we do not need to model this precisely. *) Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := @@ -451,7 +460,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pmov_rr rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m | Pmov_ri rd n => - Next (nextinstr (rs#rd <- (Vint n))) m + Next (nextinstr_nf (rs#rd <- (Vint n))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd | Pmov_mr a r1 => diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 969b3b3..a7a5f1a 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -355,14 +355,12 @@ let print_annotation oc txt args res = (* Printing of instructions *) -module Labelset = Set.Make(struct type t = label let compare = compare end) - let float_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] (* Reminder on AT&T syntax: op source, dest *) -let print_instruction oc labels = function +let print_instruction oc = function (* Moves *) | Pmov_rr(rd, r1) -> fprintf oc " movl %a, %a\n" ireg r1 ireg rd @@ -568,8 +566,7 @@ let print_instruction oc labels = function fprintf oc " ret\n" (** Pseudo-instructions *) | Plabel(l) -> - if Labelset.mem l labels then - fprintf oc "%a:\n" label (transl_label l) + fprintf oc "%a:\n" label (transl_label l) | Pallocframe(sz, ofs_ra, ofs_link) -> let sz = sp_adjustment sz in let ofs_link = camlint_of_coqint ofs_link in @@ -594,16 +591,6 @@ let print_jumptable oc (lbl, tbl) = (fun l -> fprintf oc " .long %a\n" label (transl_label l)) tbl -let rec labels_of_code accu = function - | [] -> - accu - | (Pjmp_l lbl | Pjcc(_, lbl)) :: c -> - labels_of_code (Labelset.add lbl accu) c - | Pjmptbl(_, tbl) :: c -> - labels_of_code (List.fold_right Labelset.add tbl accu) c - | _ :: c -> - labels_of_code accu c - let print_function oc name code = Hashtbl.clear current_function_labels; float_literals := []; @@ -614,7 +601,7 @@ let print_function oc name code = if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; - List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code; + List.iter (print_instruction oc) code; if target = ELF then begin fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name |