From e882493e2c4b91024b42f0603ca6869e95695e85 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 27 Oct 2007 10:23:16 +0000 Subject: Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Linearize.v | 107 ++++++++++------ backend/Linearizeproof.v | 280 ++++++++++++++++++++++++++---------------- backend/Linearizetyping.v | 28 +++-- caml/Linearizeaux.ml | 83 +++++++++++++ common/Main.v | 8 +- extraction/.depend | 27 ++-- extraction/Linearize.ml.patch | 22 ---- extraction/Makefile | 2 +- extraction/extraction.v | 3 + 9 files changed, 363 insertions(+), 197 deletions(-) create mode 100644 caml/Linearizeaux.ml delete mode 100644 extraction/Linearize.ml.patch diff --git a/backend/Linearize.v b/backend/Linearize.v index 305473ba..57919b87 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -3,9 +3,13 @@ Require Import Coqlib. Require Import Maps. +Require Import Ordered. +Require Import FSets. +Require FSetAVL. Require Import AST. Require Import Values. Require Import Globalenvs. +Require Import Errors. Require Import Op. Require Import Locations. Require Import LTL. @@ -13,10 +17,12 @@ Require Import LTLin. Require Import Kildall. Require Import Lattice. -(** To translate from LTL to LTLin, we must lay out the basic blocks +Open Scope error_monad_scope. + +(** To translate from LTL to LTLin, we must lay out the nodes of the LTL control-flow graph in some linear order, and insert explicit branches and conditional branches to make sure that - each basic block jumps to its successors as prescribed by the + each node jumps to its successors as prescribed by the LTL control-flow graph. However, branches are not necessary if the fall-through behaviour of LTLin instructions already implements the desired flow of control. For instance, @@ -39,29 +45,28 @@ Require Import Lattice. L2: ... >> The main challenge in code linearization is therefore to pick a - ``good'' order for the basic blocks that exploits well the + ``good'' order for the nodes that exploits well the fall-through behavior. Many clever trace picking heuristics have been developed for this purpose. In this file, we present linearization in a way that clearly separates the heuristic part (choosing an order for the basic blocks) from the actual code transformation parts. We proceed in three passes: -- Choosing an order for the basic blocks. This returns an enumeration - of CFG nodes stating that the basic blocks must be laid out in - the order shown in the list. -- Generate LTLin code where each basic block branches explicitly - to its successors, except if one of these successors is the - immediately following instruction. +- Choosing an order for the nodes. This returns an enumeration of CFG + nodes stating that they must be laid out in the order shown in the + list. +- Generate LTLin code where each node branches explicitly to its + successors, except if one of these successors is the immediately + following instruction. The beauty of this approach is that correct code is generated under surprisingly weak hypotheses on the enumeration of CFG nodes: it suffices that every reachable instruction occurs - exactly once in the enumeration. While the enumeration heuristic we use - is quite trivial, it is easy to implement more sophisticated - trace picking heuristics: as long as they satisfy the property above, - we do not need to re-do the proof of semantic preservation. - The enumeration could even be performed by external, untrusted - Caml code, then verified (for the property above) by certified Coq code. + exactly once in the enumeration. We therefore follow an approach + based on validation a posteriori: a piece of untrusted Caml code + implements the node enumeration heuristics, and the resulting + enumeration is checked for correctness by Coq functions that are + proved to be sound. *) (** * Determination of the order of basic blocks *) @@ -88,21 +93,44 @@ Definition reachable (f: LTL.function) : PMap.t bool := | Some rs => rs end. -(** We then enumerate the nodes of reachable basic blocks. The heuristic - we take is trivial: nodes are enumerated in decreasing numerical - order. Remember that CFG nodes are positive integers, and that - the [RTLgen] pass allocated fresh nodes 1, 2, 3, ..., but generated - instructions in roughly reverse control-flow order: often, - a basic block at label [n] has [n-1] as its only successor. - Therefore, by enumerating reachable nodes in decreasing order, - we recover a reasonable layout of basic blocks that globally respects - the structure of the original Cminor code. *) - -Definition enumerate (f: LTL.function) : list node := +(** We then enumerate the nodes of reachable instructions. + This task is performed by external, untrusted Caml code. *) + +Parameter enumerate_aux: LTL.function -> PMap.t bool -> list node. + +(** Now comes the validation of an enumeration a posteriori. *) + +Module Nodeset := FSetAVL.Make(OrderedPositive). + +(** Build a Nodeset.t from a list of nodes, checking that the list + contains no duplicates. *) + +Fixpoint nodeset_of_list (l: list node) (s: Nodeset.t) + {struct l}: res Nodeset.t := + match l with + | nil => OK s + | hd :: tl => + if Nodeset.mem hd s + then Error (msg "Linearize: duplicates in enumeration") + else nodeset_of_list tl (Nodeset.add hd s) + end. + +Definition check_reachable_aux + (reach: PMap.t bool) (s: Nodeset.t) + (ok: bool) (pc: node) (i: LTL.instruction) : bool := + if reach!!pc then ok && Nodeset.mem pc s else ok. + +Definition check_reachable + (f: LTL.function) (reach: PMap.t bool) (s: Nodeset.t) : bool := + PTree.fold (check_reachable_aux reach s) f.(LTL.fn_code) true. + +Definition enumerate (f: LTL.function) : res (list node) := let reach := reachable f in - positive_rec (list node) nil - (fun pc nodes => if reach!!pc then pc :: nodes else nodes) - f.(fn_nextpc). + let enum := enumerate_aux f reach in + do s <- nodeset_of_list enum Nodeset.empty; + if check_reachable f reach s + then OK enum + else Error (msg "Linearize: wrong enumeration"). (** * Translation from LTL to LTLin *) @@ -172,15 +200,16 @@ Fixpoint linearize_body (f: LTL.function) (enum: list node) (** * Entry points for code linearization *) -Definition transf_function (f: LTL.function) : LTLin.function := - mkfunction - (LTL.fn_sig f) - (LTL.fn_params f) - (LTL.fn_stacksize f) - (add_branch (LTL.fn_entrypoint f) (linearize_body f (enumerate f))). +Definition transf_function (f: LTL.function) : res LTLin.function := + do enum <- enumerate f; + OK (mkfunction + (LTL.fn_sig f) + (LTL.fn_params f) + (LTL.fn_stacksize f) + (add_branch (LTL.fn_entrypoint f) (linearize_body f enum))). -Definition transf_fundef (f: LTL.fundef) : LTLin.fundef := - AST.transf_fundef transf_function f. +Definition transf_fundef (f: LTL.fundef) : res LTLin.fundef := + AST.transf_partial_fundef transf_function f. -Definition transf_program (p: LTL.program) : LTLin.program := - transform_program transf_fundef p. +Definition transf_program (p: LTL.program) : res LTLin.program := + transform_partial_program transf_fundef p. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index c7299085..a625ba75 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -2,12 +2,15 @@ Require Import Coqlib. Require Import Maps. +Require Import Ordered. +Require Import FSets. Require Import AST. Require Import Integers. Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Import Errors. Require Import Smallstep. Require Import Op. Require Import Locations. @@ -17,10 +20,14 @@ Require Import LTLin. Require Import Linearize. Require Import Lattice. +Module NodesetFacts := FSetFacts.Facts(Nodeset). + Section LINEARIZATION. Variable prog: LTL.program. -Let tprog := transf_program prog. +Variable tprog: LTLin.program. + +Hypothesis TRANSF: transf_program prog = OK tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. @@ -28,33 +35,40 @@ Let tge := Genv.globalenv tprog. Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog). + 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 -> - Genv.find_funct_ptr tge v = Some (transf_fundef f). -Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog). + 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 _ _ _ transf_fundef prog). +Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). Lemma sig_preserved: - forall f, funsig (transf_fundef f) = LTL.funsig f. + forall f tf, + transf_fundef f = OK tf -> + LTLin.funsig tf = LTL.funsig f. Proof. - destruct f; reflexivity. + unfold transf_fundef, transf_partial_fundef; intros. + destruct f. monadInv H. monadInv EQ. reflexivity. + inv H. reflexivity. Qed. Lemma find_function_translated: forall ros ls f, LTL.find_function ge ros ls = Some f -> - find_function tge ros ls = Some (transf_fundef f). + exists tf, + find_function tge ros ls = Some tf /\ transf_fundef f = OK tf. Proof. - intros until f. destruct ros; simpl. - intro. apply functions_translated; auto. + unfold LTL.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. @@ -102,54 +116,84 @@ Qed. - All nodes for reachable basic blocks must be in the list. - The list is without repetition (so that no code duplication occurs). -We prove that our [enumerate] function satisfies all three. *) +We prove that our [enumerate] function satisfies both conditions. *) + + +Lemma nodeset_of_list_correct: + forall l s s', + nodeset_of_list l s = OK s' -> + list_norepet l + /\ (forall pc, Nodeset.In pc s' <-> Nodeset.In pc s \/ In pc l) + /\ (forall pc, In pc l -> ~Nodeset.In pc s). +Proof. + induction l; simpl; intros. + inv H. split. constructor. split. intro; tauto. intros; tauto. + generalize H; clear H; caseEq (Nodeset.mem a s); intros. + inv H0. + exploit IHl; eauto. intros [A [B C]]. + split. constructor; auto. red; intro. elim (C a H1). apply Nodeset.add_1. hnf. auto. + split. intros. rewrite B. rewrite NodesetFacts.add_iff. + unfold Nodeset.E.eq. unfold OrderedPositive.eq. tauto. + intros. destruct H1. subst pc. rewrite NodesetFacts.not_mem_iff. auto. + generalize (C pc H1). rewrite NodesetFacts.add_iff. tauto. +Qed. + +Lemma check_reachable_correct: + forall f reach s pc i, + check_reachable f reach s = true -> + f.(LTL.fn_code)!pc = Some i -> + reach!!pc = true -> + Nodeset.In pc s. +Proof. + intros f reach s. + assert (forall l ok, + List.fold_left (fun a p => check_reachable_aux reach s a (fst p) (snd p)) l ok = true -> + ok = true /\ + (forall pc i, + In (pc, i) l -> + reach!!pc = true -> + Nodeset.In pc s)). + induction l; simpl; intros. + split. auto. intros. destruct H0. + destruct a as [pc1 i1]. simpl in H. + exploit IHl; eauto. intros [A B]. + unfold check_reachable_aux in A. + split. destruct (reach!!pc1). elim (andb_prop _ _ A). auto. auto. + intros. destruct H0. inv H0. rewrite H1 in A. destruct (andb_prop _ _ A). + apply Nodeset.mem_2; auto. + eauto. + + intros pc i. unfold check_reachable. rewrite PTree.fold_spec. intros. + exploit H; eauto. intros [A B]. eapply B; eauto. + apply PTree.elements_correct. eauto. +Qed. Lemma enumerate_complete: - forall f pc i, + forall f enum pc i, + enumerate f = OK enum -> f.(LTL.fn_code)!pc = Some i -> (reachable f)!!pc = true -> - In pc (enumerate f). + In pc enum. Proof. - intros. - assert (forall p, - Plt p f.(fn_nextpc) -> - (reachable f)!!p = true -> - In p (enumerate f)). - unfold enumerate. pattern (fn_nextpc f). - apply positive_Peano_ind. - intros. compute in H1. destruct p; discriminate. - intros. rewrite positive_rec_succ. elim (Plt_succ_inv _ _ H2); intro. - case (reachable f)!!x. apply in_cons. auto. auto. - subst x. rewrite H3. apply in_eq. - elim (LTL.fn_code_wf f pc); intro. auto. congruence. -Qed. + intros until i. unfold enumerate. + set (reach := reachable f). + intros. monadInv H. + generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0. + exploit check_reachable_correct; eauto. intro. + exploit nodeset_of_list_correct; eauto. intros [A [B C]]. + rewrite B in H2. destruct H2. elim (Nodeset.empty_1 pc H2). auto. +Qed. Lemma enumerate_norepet: - forall f, list_norepet (enumerate f). -Proof. - intro. - unfold enumerate. pattern (fn_nextpc f). - apply positive_Peano_ind. - rewrite positive_rec_base. constructor. - intros. rewrite positive_rec_succ. - case (reachable f)!!x. - constructor. - assert (forall y, - In y (positive_rec - (list node) nil - (fun (pc : positive) (nodes : list node) => - if (reachable f) !! pc then pc :: nodes else nodes) x) -> - Plt y x). - pattern x. apply positive_Peano_ind. - rewrite positive_rec_base. intros. elim H0. - intros until y. rewrite positive_rec_succ. - case (reachable f)!!x0. - simpl. intros [A|B]. - subst x0. apply Plt_succ. - apply Plt_trans_succ. auto. - intro. apply Plt_trans_succ. auto. - red; intro. generalize (H0 x H1). exact (Plt_strict x). auto. - auto. + forall f enum, + enumerate f = OK enum -> + list_norepet enum. +Proof. + intros until enum. unfold enumerate. + set (reach := reachable f). + intros. monadInv H. + generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0. + exploit nodeset_of_list_correct; eauto. intros [A [B C]]. auto. Qed. (** * Properties related to labels *) @@ -243,23 +287,34 @@ Proof. auto. Qed. +(* +Lemma transf_function_inv: + forall f tf, transf_function f = OK tf -> + exists enum, enumerate f = OK enum /\ fn_code tf = add_branch (LTL.fn_entrypoint f) (linearize_body f enum). +Proof. + intros. monadInv H. exists x; auto. +Qed. +*) + Lemma find_label_lin: - forall f pc b, + forall f tf pc b, + transf_function f = OK tf -> f.(LTL.fn_code)!pc = Some b -> (reachable f)!!pc = true -> exists k, - find_label pc (fn_code (transf_function f)) = Some (linearize_instr b k). + find_label pc (fn_code tf) = Some (linearize_instr b k). Proof. - intros. unfold transf_function; simpl. + intros. monadInv H. simpl. rewrite find_label_add_branch. apply find_label_lin_rec. eapply enumerate_complete; eauto. auto. Qed. Lemma find_label_lin_inv: - forall f pc b k , + forall f tf pc b k, + transf_function f = OK tf -> f.(LTL.fn_code)!pc = Some b -> (reachable f)!!pc = true -> - find_label pc (fn_code (transf_function f)) = Some k -> + find_label pc (fn_code tf) = Some k -> exists k', k = linearize_instr b k'. Proof. intros. exploit find_label_lin; eauto. intros [k' FIND]. @@ -267,13 +322,14 @@ Proof. Qed. Lemma find_label_lin_succ: - forall f s, + forall f tf s, + transf_function f = OK tf -> valid_successor f s -> (reachable f)!!s = true -> exists k, - find_label s (fn_code (transf_function f)) = Some k. + find_label s (fn_code tf) = Some k. Proof. - intros. destruct H as [i AT]. + intros. destruct H0 as [i AT]. exploit find_label_lin; eauto. intros [k FIND]. exists (linearize_instr i k); auto. Qed. @@ -344,12 +400,13 @@ Proof. Qed. Lemma unique_labels_transf_function: - forall f, - unique_labels (fn_code (transf_function f)). + forall f tf, + transf_function f = OK tf -> + unique_labels (fn_code tf). Proof. - intros. unfold transf_function; simpl. + intros. monadInv H. simpl. apply unique_labels_add_branch. - apply unique_labels_lin_rec. apply enumerate_norepet. + apply unique_labels_lin_rec. eapply enumerate_norepet; eauto. Qed. (** Correctness of [add_branch]. *) @@ -373,16 +430,17 @@ Proof. Qed. Lemma add_branch_correct: - forall lbl c k s f sp ls m, - is_tail k (transf_function f).(fn_code) -> - find_label lbl (transf_function f).(fn_code) = Some c -> - plus step tge (State s (transf_function f) sp (add_branch lbl k) ls m) - E0 (State s (transf_function f) sp c ls m). + forall lbl c k s f tf sp ls m, + transf_function f = OK tf -> + is_tail k tf.(fn_code) -> + find_label lbl tf.(fn_code) = Some c -> + plus step tge (State s tf sp (add_branch lbl k) ls m) + E0 (State s tf sp c ls m). Proof. intros. unfold add_branch. caseEq (starts_with lbl k); intro SW. eapply starts_with_correct; eauto. - apply unique_labels_transf_function. + eapply unique_labels_transf_function; eauto. apply plus_one. apply exec_Lgoto. auto. Qed. @@ -407,30 +465,33 @@ Qed. Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop := | match_stackframe_intro: - forall res f sp pc ls c, + forall res f sp pc ls tf c, + transf_function f = OK tf -> (reachable f)!!pc = true -> valid_successor f pc -> - is_tail c (fn_code (transf_function f)) -> + is_tail c (fn_code tf) -> wt_function f -> match_stackframes (LTL.Stackframe res f sp ls pc) - (LTLin.Stackframe res (transf_function f) sp ls (add_branch pc c)). + (LTLin.Stackframe res tf sp ls (add_branch pc c)). Inductive match_states: LTL.state -> LTLin.state -> Prop := | match_states_intro: - forall s f sp pc ls m ts c + forall s f sp pc ls m tf ts c (STACKS: list_forall2 match_stackframes s ts) + (TRF: transf_function f = OK tf) (REACH: (reachable f)!!pc = true) - (AT: find_label pc (fn_code (transf_function f)) = Some c) + (AT: find_label pc (fn_code tf) = Some c) (WTF: wt_function f), match_states (LTL.State s f sp pc ls m) - (LTLin.State ts (transf_function f) sp c ls m) + (LTLin.State ts tf sp c ls m) | match_states_call: - forall s f ls m ts, + forall s f ls m tf ts, list_forall2 match_stackframes s ts -> + transf_fundef f = OK tf -> wt_fundef f -> match_states (LTL.Callstate s f ls m) - (LTLin.Callstate ts (transf_fundef f) ls m) + (LTLin.Callstate ts tf ls m) | match_states_return: forall s sig ls m ts, list_forall2 match_stackframes s ts -> @@ -455,7 +516,7 @@ Proof. induction 1; intros; try (inv MS); try (generalize (wt_instrs _ WTF _ _ H); intro WTI). (* Lnop *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). eapply reachable_successors; eauto. @@ -466,7 +527,7 @@ Proof. eapply is_tail_add_branch. eapply is_tail_find_label. eauto. econstructor; eauto. (* Lop *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). eapply reachable_successors; eauto. @@ -482,7 +543,7 @@ Proof. traceEq. econstructor; eauto. (* Lload *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). eapply reachable_successors; eauto. @@ -498,7 +559,7 @@ Proof. traceEq. econstructor; eauto. (* Lstore *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). eapply reachable_successors; eauto. @@ -516,16 +577,16 @@ Proof. (* Lcall *) unfold rs1 in *. inv MS. fold rs1. generalize (wt_instrs _ WTF _ _ H); intro WTI. - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). eapply reachable_successors; eauto. unfold successors; rewrite H; auto with coqlib. assert (VALID: valid_successor f pc'). inv WTI; auto. + exploit find_function_translated; eauto. intros [tf' [A B]]. econstructor; split. - apply plus_one. eapply exec_Lcall with (f' := transf_fundef f'); eauto. - apply find_function_translated; auto. - symmetry; apply sig_preserved. + apply plus_one. eapply exec_Lcall with (f' := tf'); eauto. + symmetry; apply sig_preserved; auto. econstructor; eauto. constructor; auto. econstructor; eauto. eapply is_tail_add_branch. eapply is_tail_cons_left. @@ -537,12 +598,12 @@ Proof. (* Ltailcall *) unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2. - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. + exploit find_function_translated; eauto. intros [tf' [A B]]. econstructor; split. - apply plus_one. eapply exec_Ltailcall with (f' := transf_fundef f'); eauto. - apply find_function_translated; auto. - symmetry; apply sig_preserved. + apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto. + symmetry; apply sig_preserved; auto. rewrite (parent_locset_match _ _ STACKS). econstructor; eauto. destruct ros; simpl in H0. @@ -551,7 +612,7 @@ Proof. eapply Genv.find_funct_ptr_prop; eauto. (* Lalloc *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!pc' = true). eapply reachable_successors; eauto. @@ -565,8 +626,9 @@ Proof. eapply is_tail_find_label. eauto. traceEq. econstructor; eauto. + (* Lcond true *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!ifso = true). eapply reachable_successors; eauto. @@ -585,8 +647,9 @@ Proof. econstructor; split. apply plus_one. eapply exec_Lcond_true; eauto. econstructor; eauto. + (* Lcond false *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. assert (REACH': (reachable f)!!ifnot = true). eapply reachable_successors; eauto. @@ -605,29 +668,33 @@ Proof. eapply is_tail_find_label. eauto. traceEq. econstructor; eauto. + (* Lreturn *) - destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. econstructor; split. apply plus_one. eapply exec_Lreturn; eauto. rewrite (parent_locset_match _ _ STACKS). - econstructor; eauto. + monadInv TRF. simpl. econstructor; eauto. + (* internal function *) assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true). apply reachable_entrypoint. - inv H6. + inv H7. monadInv H6. exploit find_label_lin_succ; eauto. inv H1; auto. intros [c'' AT']. - simpl. econstructor; split. + generalize EQ; intro. monadInv EQ0. econstructor; simpl; split. eapply plus_left'. eapply exec_function_internal; eauto. - simpl. eapply add_branch_correct. + simpl. eapply add_branch_correct. eauto. simpl. eapply is_tail_add_branch. constructor. eauto. traceEq. econstructor; eauto. + (* external function *) - simpl. econstructor; split. + monadInv H6. econstructor; split. apply plus_one. eapply exec_function_external; eauto. econstructor; eauto. + (* return *) inv H4. inv H1. exploit find_label_lin_succ; eauto. intros [c' AT]. @@ -642,17 +709,18 @@ Lemma transf_initial_states: forall st1, LTL.initial_state prog st1 -> exists st2, LTLin.initial_state tprog st2 /\ match_states st1 st2. Proof. - intros. inversion H. - exists (Callstate nil (transf_fundef f) (Locmap.init Vundef) (Genv.init_mem tprog)); split. + intros. inversion H. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + exists (Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split. econstructor; eauto. - change (prog_main tprog) with (prog_main prog). + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. - apply function_ptr_translated; auto. - rewrite <- H2. apply sig_preserved. + symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). + rewrite <- H2. apply sig_preserved. auto. replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. + constructor. constructor. auto. eapply Genv.find_funct_ptr_prop; eauto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. + symmetry. apply Genv.init_mem_transf_partial with transf_fundef. auto. Qed. Lemma transf_final_states: diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index c930ca52..473b3421 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import AST. Require Import Op. Require Import Locations. @@ -65,33 +66,34 @@ Proof. Qed. Lemma wt_transf_function: - forall f, + forall f tf, LTLtyping.wt_function f -> - wt_function (transf_function f). + transf_function f = OK tf -> + wt_function tf. Proof. - intros. inv H. constructor; auto. + intros. inv H. monadInv H0. constructor; auto. simpl. apply wt_add_branch. apply wt_linearize_body. auto. Qed. Lemma wt_transf_fundef: - forall f, + forall f tf, LTLtyping.wt_fundef f -> - wt_fundef (transf_fundef f). + transf_fundef f = OK tf -> + wt_fundef tf. Proof. - induction 1; simpl. - constructor; assumption. - constructor; apply wt_transf_function; assumption. + induction 1; intros. monadInv H. constructor. + monadInv H0. constructor; eapply wt_transf_function; eauto. Qed. Lemma program_typing_preserved: - forall (p: LTL.program), + forall (p: LTL.program) (tp: LTLin.program), LTLtyping.wt_program p -> - LTLintyping.wt_program (transf_program p). + transf_program p = OK tp -> + LTLintyping.wt_program tp. Proof. intros; red; intros. - generalize (transform_program_function transf_fundef p i f H0). + generalize (transform_partial_program_function transf_fundef _ _ _ H0 H1). intros [f0 [IN TR]]. - subst f. apply wt_transf_fundef; auto. - apply (H i f0 IN). + eapply wt_transf_fundef; eauto. Qed. diff --git a/caml/Linearizeaux.ml b/caml/Linearizeaux.ml new file mode 100644 index 00000000..8a4297f4 --- /dev/null +++ b/caml/Linearizeaux.ml @@ -0,0 +1,83 @@ +open BinPos +open Coqlib +open Datatypes +open LTL +open Lattice +open CList +open Maps +open Camlcoq + +(* Trivial enumeration, in decreasing order of PC *) + +(*** +let enumerate_aux f reach = + positive_rec + Coq_nil + (fun pc nodes -> + if PMap.get pc reach + then Coq_cons (pc, nodes) + else nodes) + f.fn_nextpc +***) + +(* More clever enumeration that flattens basic blocks *) + +let rec int_of_pos = function + | Coq_xI p -> (int_of_pos p lsl 1) + 1 + | Coq_xO p -> int_of_pos p lsl 1 + | Coq_xH -> 1 + +(* Count the reachable predecessors for each node *) + +let reachable_predecessors f reach = + let count = Array.make (int_of_pos f.fn_nextpc) 0 in + let increment pc = + let i = int_of_pos pc in + count.(i) <- count.(i) + 1 in + positive_rec + () + (fun pc _ -> + if PMap.get pc reach then coqlist_iter increment (successors f pc)) + f.fn_nextpc; + count + +(* Recognize instructions with only one successor *) + +let single_successor f pc = + match PTree.get pc f.fn_code with + | Some i -> + (match i with + | Lnop s -> Some s + | Lop (op, args, res, s) -> Some s + | Lload (chunk, addr, args, dst, s) -> Some s + | Lstore (chunk, addr, args, src, s) -> Some s + | Lcall (sig0, ros, args, res, s) -> Some s + | Ltailcall (sig0, ros, args) -> None + | Lalloc (arg, res, s) -> Some s + | Lcond (cond, args, ifso, ifnot) -> None + | Lreturn optarg -> None) + | None -> None + +(* Build the enumeration *) + +let enumerate_aux f reach = + let preds = reachable_predecessors f reach in + let enum = ref Coq_nil in + let emitted = Array.make (int_of_pos f.fn_nextpc) false in + let rec emit_basic_block pc = + enum := Coq_cons(pc, !enum); + emitted.(int_of_pos pc) <- true; + match single_successor f pc with + | None -> () + | Some pc' -> + let npc' = int_of_pos pc' in + if preds.(npc') <= 1 && not emitted.(npc') then emit_basic_block pc' in + let rec emit_all pc = + if pc <> Coq_xH then begin + let pc = coq_Ppred pc in + if not emitted.(int_of_pos pc) && PMap.get pc reach + then emit_basic_block pc; + emit_all pc + end in + emit_all f.fn_nextpc; + CList.rev !enum diff --git a/common/Main.v b/common/Main.v index db159298..bfee3ff3 100644 --- a/common/Main.v +++ b/common/Main.v @@ -100,7 +100,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res PPC.fundef := @@ CSE.transf_fundef @@@ Allocation.transf_fundef @@ Tunneling.tunnel_fundef - @@ Linearize.transf_fundef + @@@ Linearize.transf_fundef @@ Reload.transf_fundef @@@ Stacking.transf_fundef @@@ PPCgen.transf_fundef. @@ -224,7 +224,7 @@ Proof. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]]. clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]]. - clear H5. generalize (transform_program_partial_program _ _ _ _ _ _ P4). clear P4. intro P4. + clear H5. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]]. clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. @@ -240,7 +240,7 @@ Proof. assert (WT4 : LTLtyping.wt_program p4). subst p4. apply Tunnelingtyping.program_typing_preserved. auto. assert (WT5 : LTLintyping.wt_program p5). - subst p5. apply Linearizetyping.program_typing_preserved. auto. + apply Linearizetyping.program_typing_preserved with p4. auto. auto. assert (WT6 : Lineartyping.wt_program p6). subst p6. apply Reloadtyping.program_typing_preserved. auto. assert (WT7: Machtyping.wt_program p7). @@ -250,7 +250,7 @@ Proof. apply Machabstr2concr.exec_program_equiv; auto. apply Stackingproof.transf_program_correct with p6; auto. subst p6; apply Reloadproof.transf_program_correct; auto. - subst p5; apply Linearizeproof.transf_program_correct; auto. + apply Linearizeproof.transf_program_correct with p4; auto. subst p4; apply Tunnelingproof.transf_program_correct. apply Allocproof.transf_program_correct with p2; auto. subst p2; apply CSEproof.transf_program_correct. diff --git a/extraction/.depend b/extraction/.depend index 6ed07d8b..60534fdd 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -42,10 +42,10 @@ ../caml/CMlexer.cmx ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx -../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ - ../caml/Camlcoq.cmo CList.cmi AST.cmi -../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ - ../caml/Camlcoq.cmx CList.cmx AST.cmx +../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \ + Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi +../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \ + Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ @@ -129,8 +129,9 @@ Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \ BinPos.cmi BinInt.cmi Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ BinPos.cmi -Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi +Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \ + Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \ + CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi @@ -351,12 +352,14 @@ Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ BinPos.cmi Lattice.cmi Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \ BinPos.cmx Lattice.cmi -Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \ - Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \ - Linearize.cmi -Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \ - Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \ - Linearize.cmi +Linearize.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \ + ../caml/Linearizeaux.cmo Lattice.cmi LTLin.cmi LTL.cmi Kildall.cmi \ + FSetAVL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi \ + BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linearize.cmi +Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \ + ../caml/Linearizeaux.cmx Lattice.cmx LTLin.cmx LTL.cmx Kildall.cmx \ + FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \ + BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi Linear.cmi diff --git a/extraction/Linearize.ml.patch b/extraction/Linearize.ml.patch deleted file mode 100644 index 47b6cc9b..00000000 --- a/extraction/Linearize.ml.patch +++ /dev/null @@ -1,22 +0,0 @@ -*** Linearize.ml.orig 2006-02-09 11:47:55.000000000 +0100 ---- Linearize.ml 2006-02-09 11:58:42.000000000 +0100 -*************** -*** 28,35 **** - (** val enumerate : LTL.coq_function -> node list **) - - let enumerate f = - positive_rec Coq_nil (fun pc nodes -> -! match Maps.PMap.get pc (reachable f) with - | true -> Coq_cons (pc, nodes) - | false -> nodes) (coq_Psucc f.fn_entrypoint) - ---- 28,36 ---- - (** val enumerate : LTL.coq_function -> node list **) - - let enumerate f = -+ let reach = reachable f in - positive_rec Coq_nil (fun pc nodes -> -! match Maps.PMap.get pc reach with - | true -> Coq_cons (pc, nodes) - | false -> nodes) (coq_Psucc f.fn_entrypoint) - diff --git a/extraction/Makefile b/extraction/Makefile index 4274e8e1..513577c0 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -23,7 +23,7 @@ FILES=\ LTL.ml LTLin.ml \ InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ Allocation.ml \ - Tunneling.ml Linear.ml Linearize.ml \ + Tunneling.ml Linear.ml ../caml/Linearizeaux.ml Linearize.ml \ Parallelmove.ml Reload.ml \ Mach.ml Bounds.ml Stacking.ml \ PPC.ml PPCgen.ml \ diff --git a/extraction/extraction.v b/extraction/extraction.v index cc33c981..e0f965d7 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -47,6 +47,9 @@ Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_en (* Coloring *) Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". +(* Linearize *) +Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". + (* PPC *) Extract Constant PPC.low_half_signed => "fun _ -> assert false". Extract Constant PPC.high_half_signed => "fun _ -> assert false". -- cgit