diff options
Diffstat (limited to 'backend')
45 files changed, 6 insertions, 90 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 508bc13d..4a4c2198 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -17,16 +17,12 @@ Require Import Errors. Require Import Maps. Require Import Lattice. Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. Require Import RTLtyping. Require Import Kildall. Require Import Locations. -Require Import Conventions. Require Import Coloring. (** * Liveness analysis over RTL *) diff --git a/backend/Allocproof.v b/backend/Allocproof.v index a9477e02..20114852 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -14,7 +14,6 @@ RTL to LTL). *) Require Import FSets. -Require Import SetoidList. Require Import Coqlib. Require Import Errors. Require Import Maps. diff --git a/backend/Bounds.v b/backend/Bounds.v index 23fa3b56..ef78b2ef 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -13,7 +13,6 @@ (** Computation of resource bounds for Linear code. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Op. Require Import Locations. diff --git a/backend/CSE.v b/backend/CSE.v index 85f46e2b..1888fb84 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -21,7 +21,6 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 49b213bd..55691235 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -16,8 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Errors. -Require Import Integers. -Require Import Floats. Require Import Values. Require Import Memory. Require Import Events. diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v index 7401abc6..0ed2be10 100644 --- a/backend/CleanupLabels.v +++ b/backend/CleanupLabels.v @@ -21,7 +21,6 @@ branched to. *) Require Import Coqlib. -Require Import Maps. Require Import Ordered. Require Import FSets. Require FSetAVL. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index a7a60f6c..dbd33c16 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -13,7 +13,6 @@ (** Correctness proof for clean-up of labels *) Require Import Coqlib. -Require Import Maps. Require Import Ordered. Require Import FSets. Require Import AST. @@ -22,7 +21,6 @@ Require Import Values. Require Import Memory. Require Import Events. Require Import Globalenvs. -Require Import Errors. Require Import Smallstep. Require Import Op. Require Import Locations. diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v index ea9de868..f58a910f 100644 --- a/backend/CleanupLabelstyping.v +++ b/backend/CleanupLabelstyping.v @@ -14,7 +14,6 @@ Require Import Coqlib. Require Import Maps. -Require Import Errors. Require Import AST. Require Import Op. Require Import Locations. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index a063544d..b5a0d39b 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. Require Import Events. Require Import Values. Require Import Memory. diff --git a/backend/Constprop.v b/backend/Constprop.v index fc242e18..fe16240e 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -19,8 +19,6 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index f14e87af..1b906668 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. Require Import Values. Require Import Events. Require Import Memory. diff --git a/backend/Inlining.v b/backend/Inlining.v index 3ddfe9a4..5075fd6f 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -18,7 +18,6 @@ Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. Require Import Op. Require Import Registers. Require Import RTL. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 84bcdcd9..014986d7 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -18,7 +18,6 @@ Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. Require Import Globalenvs. Require Import Op. Require Import Registers. diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index ec64e99b..9a5522d8 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -15,7 +15,6 @@ Require Import Coqlib. Require Import FSets. Require Import FSetAVL. -Require Import Maps. Require Import Ordered. Require Import Registers. Require Import Locations. diff --git a/backend/LTLin.v b/backend/LTLin.v index 390c4cf8..e0d5ca29 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -17,7 +17,6 @@ instructions with explicit labels and ``goto'' instructions. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. @@ -28,7 +27,6 @@ Require Import Smallstep. Require Import Op. Require Import Locations. Require Import LTL. -Require Import Conventions. (** * Abstract syntax *) diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index e9cc2df3..0338667b 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -13,12 +13,9 @@ (** Typing rules for LTLin. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. -Require Import Memdata. Require Import Op. -Require Import RTL. Require Import Locations. Require Import LTLin. Require LTLtyping. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 2e627e90..0c905141 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -16,9 +16,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Memdata. Require Import Op. -Require Import RTL. Require Import Locations. Require Import LTL. Require Import Conventions. diff --git a/backend/Linear.v b/backend/Linear.v index b2185315..52f5fd71 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -18,7 +18,6 @@ [Lsetstack] are provided to access stack slots. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. diff --git a/backend/Linearize.v b/backend/Linearize.v index fd350c71..636cb224 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -19,8 +19,6 @@ 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. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index da73b00b..32d60459 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -13,7 +13,6 @@ (** Typing rules for Linear. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. diff --git a/backend/Locations.v b/backend/Locations.v index 0b538fdb..ba2fb063 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -14,7 +14,6 @@ the results of register allocation (file [Allocation]). *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Values. Require Export Machregs. diff --git a/backend/Mach.v b/backend/Mach.v index 669d35e7..56c03699 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -21,10 +21,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Memory. -Require Import Events. Require Import Globalenvs. -Require Import Smallstep. Require Import Op. Require Import Locations. Require Import Conventions. diff --git a/backend/Machsem.v b/backend/Machsem.v index a802323f..6d5f1cfc 100644 --- a/backend/Machsem.v +++ b/backend/Machsem.v @@ -13,7 +13,6 @@ (** The Mach intermediate language: operational semantics. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. diff --git a/backend/Machtyping.v b/backend/Machtyping.v index b9d8009e..2dc19be0 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -13,14 +13,8 @@ (** Type system for the Mach intermediate language. *) Require Import Coqlib. -Require Import Maps. Require Import AST. -Require Import Memory. Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Conventions. diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index d7a42173..4930ccd0 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -24,7 +24,6 @@ Require Import Coqlib. Require Parmov. Require Import Values. -Require Import Events. Require Import AST. Require Import Locations. Require Import Conventions. diff --git a/backend/RRE.v b/backend/RRE.v index 95eadce9..ece60517 100644 --- a/backend/RRE.v +++ b/backend/RRE.v @@ -13,10 +13,7 @@ (** Redundant Reloads Elimination *) Require Import Coqlib. -Require Import Maps. Require Import AST. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Conventions. diff --git a/backend/RREproof.v b/backend/RREproof.v index d70a1fde..8926fe4f 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -14,7 +14,6 @@ Require Import Axioms. Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Values. Require Import Globalenvs. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 62df254b..007191a0 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -17,7 +17,6 @@ Require Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. Require Import Switch. Require Import Op. Require Import Registers. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1b8e853f..690611c0 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -617,9 +617,10 @@ Proof. edestruct Mem.loadv_extends as [v' []]; eauto. exists (rs1#rd <- v'). (* Exec *) - split. eapply star_right. eexact EX1. eapply exec_Iload; eauto. - rewrite (@eval_addressing_preserved _ _ _ _ ge tge). eauto. - exact symbols_preserved. traceEq. + split. eapply star_right. eexact EX1. eapply exec_Iload. eauto. + instantiate (1 := vaddr'). rewrite <- H3. + apply eval_addressing_preserved. exact symbols_preserved. + auto. traceEq. (* Match-env *) split. eauto with rtlg. (* Result *) @@ -1049,9 +1050,9 @@ Proof. edestruct Mem.storev_extends as [tm' []]; eauto. econstructor; split. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. - eapply exec_Istore with (a := vaddr'); eauto. + eapply exec_Istore with (a := vaddr'). eauto. rewrite <- H4. apply eval_addressing_preserved. exact symbols_preserved. - traceEq. + eauto. traceEq. econstructor; eauto. constructor. (* call *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 5114390a..c50c7023 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -25,10 +25,6 @@ Require Errors. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. -Require Import Events. -Require Import Memory. -Require Import Globalenvs. Require Import Switch. Require Import Op. Require Import Registers. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index a14e944c..f8dbfe49 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -20,10 +20,8 @@ Require Import Op. Require Import Registers. Require Import Globalenvs. Require Import Values. -Require Import Memory. Require Import Integers. Require Import Events. -Require Import Smallstep. Require Import RTL. Require Import Conventions. diff --git a/backend/Registers.v b/backend/Registers.v index fceb7c24..47e10fa4 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -21,7 +21,6 @@ Require Import Coqlib. Require Import AST. Require Import Maps. Require Import Ordered. -Require Import FSets. Require FSetAVL. Definition reg: Type := positive. diff --git a/backend/Reload.v b/backend/Reload.v index 0ad53e6e..31bddcd0 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -13,11 +13,8 @@ (** Reloading, spilling, and explication of calling conventions. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. -Require Import Values. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import LTLin. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 75c7dade..1d499092 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -13,7 +13,6 @@ (** Correctness proof for the [Reload] pass. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. @@ -24,7 +23,6 @@ Require Import Smallstep. Require Import Op. Require Import Locations. Require Import Conventions. -Require Import Allocproof. Require Import RTLtyping. Require Import LTLin. Require Import LTLintyping. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index eba5ad62..99c89ab1 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -14,7 +14,6 @@ correctness of computation of stack bounds for Linear. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Op. Require Import Locations. diff --git a/backend/Renumber.v b/backend/Renumber.v index b933bba7..c8623185 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -15,7 +15,6 @@ Require Import Coqlib. Require Import Maps. Require Import Postorder. -Require Import AST. Require Import RTL. (** CompCert's dataflow analyses (module [Kildall]) are more precise diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 5ec29e25..d0860106 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -15,10 +15,7 @@ Require Import Coqlib. Require Import Maps. Require Import Postorder. -Require Import AST. -Require Import Values. Require Import Events. -Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Op. diff --git a/backend/Selection.v b/backend/Selection.v index ff4d8639..29bdabcc 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -23,12 +23,8 @@ The source language is Cminor and the target language is CminorSel. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. Require Import Globalenvs. Require Cminor. Require Import Op. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 2fd92190..09dc0ff0 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -16,7 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. -Require Import Floats. Require Import Values. Require Import Memory. Require Import Events. diff --git a/backend/Stacking.v b/backend/Stacking.v index 23a112ce..732443bf 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -13,12 +13,10 @@ (** Layout of activation records; translation from Linear to Mach. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. Require Import Op. -Require Import RTL. Require Import Locations. Require Import Linear. Require Import Bounds. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1d87ad34..6c4e43fd 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -15,7 +15,6 @@ (** This file proves semantic preservation for the [Stacking] pass. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index 27de5571..2324cd54 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -13,7 +13,6 @@ (** Type preservation for the [Stacking] pass. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import Integers. Require Import AST. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 158002e8..917ec83c 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -15,7 +15,6 @@ Require Import Coqlib. Require Import Maps. Require Import AST. -Require Import Globalenvs. Require Import Registers. Require Import Op. Require Import RTL. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 8dd1fe2b..18414a89 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -16,10 +16,6 @@ Require Import Coqlib. Require Import Maps. Require Import UnionFind. Require Import AST. -Require Import Values. -Require Import Globalenvs. -Require Import Op. -Require Import Locations. Require Import LTL. (** Branch tunneling shortens sequences of branches (with no intervening diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index 743b4681..dfc36b60 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -14,13 +14,7 @@ Require Import Coqlib. Require Import Maps. -Require Import UnionFind. Require Import AST. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Op. -Require Import Locations. Require Import LTL. Require Import LTLtyping. Require Import Tunneling. |