diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-01-27 11:19:58 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-01-27 11:19:58 +0000 |
| commit | 877b4347139b187bb2e5151526ae17307d246a12 (patch) | |
| tree | e9e61f8de6ff2fe6c786554b64cd29f22562b456 /backend | |
| parent | e431dcf84d7e1a1106a501d53492b672c9d0b86e (diff) | |
Ajout license, README, copyright notices
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
55 files changed, 663 insertions, 0 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index eab5233..3a5960b 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Register allocation. *) Require Import Coqlib. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1b5a415..68d6868 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 [Allocation] pass (translation from RTL to LTL). *) diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index c0abf0d..469fd3c 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Preservation of typing during register allocation. *) Require Import Coqlib. diff --git a/backend/Bounds.v b/backend/Bounds.v index a0f09ce..0e8b9fa 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 resource bounds forr Linear code. *) Require Import Coqlib. diff --git a/backend/CSE.v b/backend/CSE.v index a7901d6..b7e19c1 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Common subexpression elimination over RTL. This optimization proceeds by value numbering over extended basic blocks. *) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index d46a39f..a87cd75 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 common subexpression elimination. *) Require Import Coqlib. diff --git a/backend/Cminor.v b/backend/Cminor.v index 1d2eea7..df541a1 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + (** Abstract syntax and semantics for the Cminor language. *) Require Import Coqlib. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 859c46e..3578868 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The Cminor language after instruction selection. *) Require Import Coqlib. diff --git a/backend/Coloring.v b/backend/Coloring.v index 57f7d59..5e91b03 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Construction and coloring of the interference graph. *) Require Import Coqlib. diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index ce24030..cea4ce5 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 of graph coloring. *) Require Import SetoidList. diff --git a/backend/Constprop.v b/backend/Constprop.v index fecfb19..18fa589 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Constant propagation over RTL. This is the first of the two optimizations performed at RTL level. It proceeds by a standard dataflow analysis and the corresponding code transformation. *) diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index dfa828b..e16f322 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 constant propagation. *) Require Import Coqlib. diff --git a/backend/Conventions.v b/backend/Conventions.v index 9d005b3..ea7d448 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Function calling conventions and other conventions regarding the use of machine registers and stack slots. *) diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index 5dc4fe9..c9891c2 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Representation of interference graphs for register allocation. *) Require Import Coqlib. diff --git a/backend/Kildall.v b/backend/Kildall.v index 41011f2..b4445ae 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Solvers for dataflow inequations. *) Require Import Coqlib. diff --git a/backend/LTL.v b/backend/LTL.v index db996ba..e99e016 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The LTL intermediate language: abstract syntax and semantics. LTL (``Location Transfer Language'') is the target language diff --git a/backend/LTLin.v b/backend/LTLin.v index da8719a..6cf2eb5 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The LTLin intermediate language: abstract syntax and semantcs *) (** The LTLin language is a variant of LTL where control-flow is not diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 06c50f8..1c0c3f3 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Typing rules for LTLin. *) Require Import Coqlib. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 646edc8..18308b8 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Typing rules for LTL. *) Require Import Coqlib. diff --git a/backend/Linear.v b/backend/Linear.v index a6e31fb..b9880ff 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The Linear intermediate language: abstract syntax and semantcs *) (** The Linear language is a variant of LTLin where arithmetic diff --git a/backend/Linearize.v b/backend/Linearize.v index 57919b8..42330ed 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Linearization of the control-flow graph: translation from LTL to LTLin *) diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index a625ba7..12d0a1f 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 code linearization *) Require Import Coqlib. diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 473b342..ba54723 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 Linearize pass *) Require Import Coqlib. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index baf522a..0f5a1ec 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Typing rules for Linear. *) Require Import Coqlib. diff --git a/backend/Locations.v b/backend/Locations.v index aaefc08..1373887 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Locations are a refinement of RTL pseudo-registers, used to reflect the results of register allocation (file [Allocation]). *) diff --git a/backend/Mach.v b/backend/Mach.v index 05805ec..f727504 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: abstract syntax. Mach is the last intermediate language before generation of assembly diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 0abdd1e..32a316a 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: abstract semantics. *) Require Import Coqlib. diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 5349fb5..ffdfb33 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Simulation between the two semantics for the Mach language. *) Require Import Coqlib. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5a095d7..2eb3d47 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The Mach intermediate language: concrete semantics. *) Require Import Coqlib. diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 28037ce..5e5f03c 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 system for the Mach intermediate language. *) Require Import Coqlib. diff --git a/backend/Op.v b/backend/Op.v index 698b433..51b5e53 100644 --- a/backend/Op.v +++ b/backend/Op.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Operators and addressing modes. The abstract syntax and dynamic semantics for the CminorSel, RTL, LTL and Mach languages depend on the following types, defined in this library: diff --git a/backend/PPC.v b/backend/PPC.v index 244c595..8af2c9b 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Abstract syntax and semantics for PowerPC assembly language *) Require Import Coqlib. diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 171945d..805d039 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Translation from Mach to PPC. *) Require Import Coqlib. diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 8d6d934..2b00cfc 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 PPC generation: main proof. *) Require Import Coqlib. diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v index c0125fc..107ea05 100644 --- a/backend/PPCgenproof1.v +++ b/backend/PPCgenproof1.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 PPC generation: auxiliary results. *) Require Import Coqlib. diff --git a/backend/PPCgenretaddr.v b/backend/PPCgenretaddr.v index f2802ec..3526865 100644 --- a/backend/PPCgenretaddr.v +++ b/backend/PPCgenretaddr.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Predictor for return addresses in generated PPC code. The [return_address_offset] predicate defined here is used in the diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index 3d77b57..baab207 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Translation of parallel moves into sequences of individual moves. In this file, we adapt the generic "parallel move" algorithm diff --git a/backend/RTL.v b/backend/RTL.v index b1afc94..abecd4a 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** The RTL intermediate language: abstract syntax and semantics. RTL stands for "Register Transfer Language". This is the first diff --git a/backend/RTLbigstep.v b/backend/RTLbigstep.v index 0ad6e68..182f593 100644 --- a/backend/RTLbigstep.v +++ b/backend/RTLbigstep.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** An alternate, mixed-step semantics for the RTL intermediate language. *) Require Import Coqlib. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 52a6c8a..3cc0eeb 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Translation from CminorSel to RTL. *) Require Import Coqlib. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index dd8728f..e02463a 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 RTL generation. *) Require Import Coqlib. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 94afff8..b8061a3 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Abstract specification of RTL generation *) (** In this module, we define inductive predicates that specify the diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 4056749..a30f9e5 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Typing rules and a type inference algorithm for RTL. *) Require Import Coqlib. diff --git a/backend/Registers.v b/backend/Registers.v index e4b7b00..c3d04d6 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Pseudo-registers and register states. This library defines the type of pseudo-registers (also known as diff --git a/backend/Reload.v b/backend/Reload.v index 58e17ff..c5559e3 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Reloading, spilling, and explication of calling conventions. *) Require Import Coqlib. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index e9ced51..401ae46 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 [Reload] pass. *) Require Import Coqlib. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 155c174..3f0ff1e 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Proof of type preservation for Reload and of correctness of computation of stack bounds for Linear. *) diff --git a/backend/Selection.v b/backend/Selection.v index 0183ee7..8a69ade 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Instruction selection *) (** The instruction selection pass recognizes opportunities for using diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 177e321..e28bfaf 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 of instruction selection *) Require Import Coqlib. diff --git a/backend/Stacking.v b/backend/Stacking.v index c19e293..16595e5 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Layout of activation records; translation from Linear to Mach. *) Require Import Coqlib. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 905570e..46e19ca 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 translation from Linear to Mach. *) (** This file proves semantic preservation for the [Stacking] pass. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index fa8a3e2..aa534ff 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 [Stacking] pass. *) Require Import Coqlib. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 15f4676..2f520c6 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + (** Branch tunneling (optimization of branches to branches). *) Require Import Coqlib. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 3777eaa..d0c9546 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 branch tunneling optimization. *) Require Import Coqlib. diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index c611067..57e1271 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -1,3 +1,15 @@ +(* *********************************************************************) +(* *) +(* 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 Tunneling pass *) Require Import Coqlib. |