diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-05-04 16:35:45 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-05-04 16:35:45 +0200 |
| commit | c22a1828063756fdc11876993e6f1e2ca3bba04d (patch) | |
| tree | f1d61e5ae919097062343e9309d1b96b6ca80dd1 | |
| parent | 4f6c5833a149d0659f4bffaaeb464cd9864b3a9b (diff) | |
| download | compcert-kvx-c22a1828063756fdc11876993e6f1e2ca3bba04d.tar.gz compcert-kvx-c22a1828063756fdc11876993e6f1e2ca3bba04d.zip | |
Adding copyrights
108 files changed, 1392 insertions, 460 deletions
diff --git a/aarch64/CSE2deps.v b/aarch64/CSE2deps.v index 90b514a2..a23e41a8 100644 --- a/aarch64/CSE2deps.v +++ b/aarch64/CSE2deps.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v index 4aac23af..dbd46142 100644 --- a/aarch64/CSE2depsproof.v +++ b/aarch64/CSE2depsproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/aarch64/DuplicateOpcodeHeuristic.ml b/aarch64/DuplicateOpcodeHeuristic.ml index 5fc2156c..3a3b87fc 100644 --- a/aarch64/DuplicateOpcodeHeuristic.ml +++ b/aarch64/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + open Op open Integers diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v index 9db51bbb..d48dabf3 100644 --- a/arm/CSE2deps.v +++ b/arm/CSE2deps.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v index 61fe5980..28ef41ca 100644 --- a/arm/CSE2depsproof.v +++ b/arm/CSE2depsproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/arm/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml index 9b6a6409..41996028 100644 --- a/arm/DuplicateOpcodeHeuristic.ml +++ b/arm/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + open Op open Integers diff --git a/backend/Allnontrap.v b/backend/Allnontrap.v index acf03eca..fedf14f7 100644 --- a/backend/Allnontrap.v +++ b/backend/Allnontrap.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/Allnontrapproof.v b/backend/Allnontrapproof.v index 92e5a88c..157c5de2 100644 --- a/backend/Allnontrapproof.v +++ b/backend/Allnontrapproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import FunInd. Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. diff --git a/backend/Asmaux.v b/backend/Asmaux.v index 51e94f6b..1167c34c 100644 --- a/backend/Asmaux.v +++ b/backend/Asmaux.v @@ -1,5 +1,19 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Asm. Require Import AST. (* Constant only needed by Asmexpandaux.ml *) -Definition dummy_function := {| fn_code := nil; fn_sig := signature_main |}.
\ No newline at end of file +Definition dummy_function := {| fn_code := nil; fn_sig := signature_main |}. diff --git a/backend/CSE2.v b/backend/CSE2.v index 00b1821e..3042645e 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* Replace available expressions by the register containing their value. diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index f9c7b400..49dbd409 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* Replace available expressions by the register containing their value. diff --git a/backend/CSE3.v b/backend/CSE3.v index 2203ad14..df1c2bfc 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps CSE2deps. diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index ef487c86..b5fdbd63 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps CSE2deps. diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 3f7d5bb9..3e4a6b9e 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + open CSE3analysis open Maps open HashedSet diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index c65a6d9e..0c2aeb8e 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1,3 +1,14 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index ccbfd198..6e489066 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* Replace available expressions by the register containing their value. diff --git a/backend/Duplicate.v b/backend/Duplicate.v index af85efe4..0e04b07d 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** RTL node duplication using external oracle. Used to form superblock structures *) diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 89f187da..00819834 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* Oracle for Duplicate pass. * - Add static prediction information to Icond nodes * - Performs tail duplication on interesting traces to form superblocks diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 6b598dc7..62455076 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** Correctness proof for code duplication *) Require Import AST Linking Errors Globalenvs Smallstep. Require Import Coqlib Maps Events Values. diff --git a/backend/FirstNop.v b/backend/FirstNop.v index f7e5261e..b3c765e4 100644 --- a/backend/FirstNop.v +++ b/backend/FirstNop.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v index a5d63c25..5a1c5acf 100644 --- a/backend/FirstNopproof.v +++ b/backend/FirstNopproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Values Memory Globalenvs Events Smallstep. diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 7cfd411f..1b375532 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 826d4250..f3e572e0 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import FunInd. Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. diff --git a/backend/Inject.v b/backend/Inject.v index 971a5423..a24fef50 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 75fed25f..dd5e72f8 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Globalenvs Values Events. diff --git a/backend/LICM.v b/backend/LICM.v index 0a0a1c7d..787ce256 100644 --- a/backend/LICM.v +++ b/backend/LICM.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 4ebc7844..c3907809 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + open RTL;; open Camlcoq;; open Maps;; diff --git a/backend/LICMproof.v b/backend/LICMproof.v index 2b76b668..e3f0c2b8 100644 --- a/backend/LICMproof.v +++ b/backend/LICMproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 9d5a5ba6..3f1a8b6e 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -1,4 +1,4 @@ - +(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v index b9b97903..7f8af39b 100644 --- a/backend/OpHelpers.v +++ b/backend/OpHelpers.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import AST Integers Floats. Require Import Op CminorSel. diff --git a/backend/OpHelpersproof.v b/backend/OpHelpersproof.v index 08da8a36..63199520 100644 --- a/backend/OpHelpersproof.v +++ b/backend/OpHelpersproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import Maps. Require Import AST. @@ -75,4 +87,4 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) /\ helper_declared p i32_umod "__compcert_i32_umod" sig_ii_i /\ helper_declared p f32_div "__compcert_f32_div" sig_ss_s /\ helper_declared p f64_div "__compcert_f64_div" sig_ff_f -.
\ No newline at end of file +. diff --git a/backend/Profiling.v b/backend/Profiling.v index 4cba49ee..83e96311 100644 --- a/backend/Profiling.v +++ b/backend/Profiling.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/ProfilingExploit.v b/backend/ProfilingExploit.v index cfca1a12..2325f582 100644 --- a/backend/ProfilingExploit.v +++ b/backend/ProfilingExploit.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v index bc68c38e..78de09af 100644 --- a/backend/ProfilingExploitproof.v +++ b/backend/ProfilingExploitproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import FunInd. Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. diff --git a/backend/Profilingaux.ml b/backend/Profilingaux.ml index ec0ae304..6ecea9e6 100644 --- a/backend/Profilingaux.ml +++ b/backend/Profilingaux.ml @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + open Camlcoq open RTL open Maps diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index fc04c77e..abb86bdb 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Values Memory Globalenvs Events Smallstep. diff --git a/lib/HashedSet.v b/lib/HashedSet.v index 00e01612..cb2ee1b2 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import ZArith. Require Import Bool. Require Import List. diff --git a/lib/HashedSetaux.ml b/lib/HashedSetaux.ml index 8329c249..501475d6 100644 --- a/lib/HashedSetaux.ml +++ b/lib/HashedSetaux.ml @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + type uid = int let uid_base = min_int diff --git a/lib/HashedSetaux.mli b/lib/HashedSetaux.mli index 14beac41..e3426eb4 100644 --- a/lib/HashedSetaux.mli +++ b/lib/HashedSetaux.mli @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + type pset val qnode : pset -> bool -> pset -> pset val node : pset * bool * pset -> pset diff --git a/lib/extra/HashedMap.v b/lib/extra/HashedMap.v index df724867..a7d6f589 100644 --- a/lib/extra/HashedMap.v +++ b/lib/extra/HashedMap.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import ZArith. Require Import Bool. Require Import List. diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index 587f768e..1a15b733 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -1,18 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* Jacques-Henri Jourdan, INRIA Paris *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *) @@ -33,7 +32,7 @@ Proof. unfold splitlong. congruence. Qed. -(** THIS IS NOT CHECKED ! NONE OF THIS ! *) +(** FIXME - Check the properties below *) (** Section 7.3: "Except when otherwise stated, if the result of a floating-point operation is NaN, it is the canonical NaN. The diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 189e0c76..c8c0bc1c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** * Abstract syntax for K1c textual assembly language. diff --git a/mppa_k1c/Asmaux.v b/mppa_k1c/Asmaux.v index 891d1068..2abd445e 100644 --- a/mppa_k1c/Asmaux.v +++ b/mppa_k1c/Asmaux.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Asm. Require Import AST. diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index a05d4726..885ac6bc 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1,19 +1,16 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Sequential block semantics for K1c assembly. The syntax is given in AsmVLIW *) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 01eda623..1881e7e9 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** * Translation from Asmblock to AbstractBB We define a specific instance of AbstractBB, named L, translate bblocks from Asmblock into this instance diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 36269954..f57b596b 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** * Translation from Machblock to K1c assembly language (Asmblock) Inspired from the Mach->Asm pass of other backends, but adapted to the block structure *) diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 1a427112..5cb498bc 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Correctness proof for RISC-V generation: main proof. *) diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 9c836037..74b9b62b 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** * Proof of correctness for individual instructions *) diff --git a/mppa_k1c/Asmblockprops.v b/mppa_k1c/Asmblockprops.v index 3c6ba534..bc14b231 100644 --- a/mppa_k1c/Asmblockprops.v +++ b/mppa_k1c/Asmblockprops.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** Common definition and proofs on Asmblock required by various modules *) Require Import Coqlib. diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index e388d2aa..785887b2 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -1,20 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (* Expanding built-ins and some pseudo-instructions by rewriting of the RISC-V assembly code. *) diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 8875a4ac..61856acf 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Integers. Require Import Mach Asm Asmblock Asmblockgen Machblockgen. diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 7388f6da..f43acd37 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Correctness proof for Asmgen *) diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 819120a0..b085fb1d 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *) diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v index 3b5cd419..eeb578d0 100644 --- a/mppa_k1c/Builtins1.v +++ b/mppa_k1c/Builtins1.v @@ -1,17 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and Inria Paris *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Platform-specific built-in functions *) diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index a91119b1..6dc3e938 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -1,17 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (* Processor-dependent builtin C functions *) diff --git a/mppa_k1c/CSE2deps.v b/mppa_k1c/CSE2deps.v index 8ab9242a..b4b80e2f 100644 --- a/mppa_k1c/CSE2deps.v +++ b/mppa_k1c/CSE2deps.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. diff --git a/mppa_k1c/CSE2depsproof.v b/mppa_k1c/CSE2depsproof.v index a3811e78..f283c8ac 100644 --- a/mppa_k1c/CSE2depsproof.v +++ b/mppa_k1c/CSE2depsproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/mppa_k1c/Chunks.v b/mppa_k1c/Chunks.v index 40778877..86d4f0ac 100644 --- a/mppa_k1c/Chunks.v +++ b/mppa_k1c/Chunks.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import AST. Require Import Values. Require Import Integers. diff --git a/mppa_k1c/CombineOp.v b/mppa_k1c/CombineOp.v index 6236f38f..ff1db3cd 100644 --- a/mppa_k1c/CombineOp.v +++ b/mppa_k1c/CombineOp.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Recognition of combined operations, addressing modes and conditions during the [CSE] phase. *) diff --git a/mppa_k1c/CombineOpproof.v b/mppa_k1c/CombineOpproof.v index a24de1e5..dafc90df 100644 --- a/mppa_k1c/CombineOpproof.v +++ b/mppa_k1c/CombineOpproof.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Recognition of combined operations, addressing modes and conditions during the [CSE] phase. *) diff --git a/mppa_k1c/ConstpropOp.vp b/mppa_k1c/ConstpropOp.vp index 7ee3dfe8..2a428020 100644 --- a/mppa_k1c/ConstpropOp.vp +++ b/mppa_k1c/ConstpropOp.vp @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Strength reduction for operators and conditions. This is the machine-dependent part of [Constprop]. *) diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index 4dd0441d..05bbdde1 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Correctness proof for operator strength reduction. *) diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 48346a6d..ab30ded9 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. 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/mppa_k1c/DecBoolOps.v b/mppa_k1c/DecBoolOps.v index 7f6f7c87..1e0a6187 100644 --- a/mppa_k1c/DecBoolOps.v +++ b/mppa_k1c/DecBoolOps.v @@ -1,3 +1,18 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Set Implicit Arguments. Theorem and_dec : forall A B C D : Prop, @@ -12,4 +27,4 @@ Proof. - right. tauto. Qed. -
\ No newline at end of file + diff --git a/mppa_k1c/DuplicateOpcodeHeuristic.ml b/mppa_k1c/DuplicateOpcodeHeuristic.ml index 2ec314c1..38702e1b 100644 --- a/mppa_k1c/DuplicateOpcodeHeuristic.ml +++ b/mppa_k1c/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* open Camlcoq *) open Op open Integers diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v index d9b9d3a6..9849c35d 100644 --- a/mppa_k1c/ExtFloats.v +++ b/mppa_k1c/ExtFloats.v @@ -1,3 +1,18 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Floats Integers ZArith. Module ExtFloat. diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 5a890f3c..3664c00a 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -1,3 +1,18 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import Integers. Require Import Values. diff --git a/mppa_k1c/InstructionScheduler.ml b/mppa_k1c/InstructionScheduler.ml index 9d3503e2..e4dc3f97 100644 --- a/mppa_k1c/InstructionScheduler.ml +++ b/mppa_k1c/InstructionScheduler.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** Schedule instructions on a synchronized pipeline @author David Monniaux, CNRS, VERIMAG *) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index cff1164c..a242fce2 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import String. Require Import Coqlib. diff --git a/mppa_k1c/Machregsaux.ml b/mppa_k1c/Machregsaux.ml index 9c4175ed..76956959 100644 --- a/mppa_k1c/Machregsaux.ml +++ b/mppa_k1c/Machregsaux.ml @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Auxiliary functions on machine registers *) diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 7111c48b..4c354d5a 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib. Require Import AST Integers Floats. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 012d67d0..544bb081 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. 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 diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 0611fdda..35f4bbd9 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import Asmvliw. Require Import Values. diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 31180cea..7518866d 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -1,14 +1,16 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 686979a6..325f70e5 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + open Asmvliw open Asmblock open Printf diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 8cc7f0ab..c290387b 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -1,14 +1,16 @@ -(* *********************************************************************) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml index 67f87000..da7d6c32 100644 --- a/mppa_k1c/PrintOp.ml +++ b/mppa_k1c/PrintOp.ml @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Pretty-printing of operators, conditions, addressing modes *) diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 981c796c..b3638eca 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Instruction selection for 64-bit integer operations *) @@ -462,4 +460,4 @@ End SELECT. (* Local Variables: *) (* mode: coq *) -(* End: *)
\ No newline at end of file +(* End: *) diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 5e4f3ed6..fb38bbce 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Correctness of instruction selection for 64-bit integer operations *) diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index bd481cbb..9e5d45a0 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Instruction selection for operators *) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 28294934..d1d0b95c 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Correctness of instruction selection for operators *) diff --git a/mppa_k1c/Stacklayout.v b/mppa_k1c/Stacklayout.v index d0c6a526..46202e03 100644 --- a/mppa_k1c/Stacklayout.v +++ b/mppa_k1c/Stacklayout.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (** Machine- and ABI-dependent layout information for activation records. *) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 01751f19..e85b5ef3 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -1,19 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Prashanth Mundkur, SRI International *) -(* *) -(* 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 contributions by Prashanth Mundkur are reused and adapted *) -(* under the terms of a Contributor License Agreement between *) -(* SRI International and INRIA. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (* Printing RISC-V assembly code in asm syntax *) diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 901908b5..e634fdc0 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -1,14 +1,17 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* 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 Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index cf46072f..0b1c502d 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** Syntax and Sequential Semantics of Abstract Basic Blocks. *) Require Import Setoid. diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v index 7a77ec15..c914eee1 100644 --- a/mppa_k1c/abstractbb/ImpSimuTest.v +++ b/mppa_k1c/abstractbb/ImpSimuTest.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks with imperative hash-consing, and rewriting. diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v index e49a4611..dd9785b5 100644 --- a/mppa_k1c/abstractbb/Impure/ImpConfig.v +++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v @@ -82,4 +82,4 @@ Extract Inlined Constant bind => "(|>)". Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *) Extraction Inline t. -Global Opaque t.
\ No newline at end of file +Global Opaque t. diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index f1abaf7a..508b3f19 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -193,4 +193,4 @@ Ltac wlp_xsimplify hint := Create HintDb wlp discriminated. -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file +Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp). diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index 30904b5d..feebeee5 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** Parallel Semantics of Abstract Basic Blocks and parallelizability test. *) diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v index e234883f..61f8f2ec 100644 --- a/mppa_k1c/abstractbb/SeqSimuTheory.v +++ b/mppa_k1c/abstractbb/SeqSimuTheory.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** A theory for checking/proving simulation by symbolic execution. *) diff --git a/mppa_k1c/extractionMachdep.v b/mppa_k1c/extractionMachdep.v index fdecd2a3..2e409931 100644 --- a/mppa_k1c/extractionMachdep.v +++ b/mppa_k1c/extractionMachdep.v @@ -1,17 +1,17 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) (* Additional extraction directives specific to the RISC-V port *) diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 58455ada..1af59238 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -1,3 +1,18 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (** * "block" version of Asmgenproof0 This module is largely adapted from Asmgenproof0.v of the other backends diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v index 224eda0a..f79814f2 100644 --- a/mppa_k1c/lib/ForwardSimulationBlock.v +++ b/mppa_k1c/lib/ForwardSimulationBlock.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (*** Auxiliary lemmas on starN and forward_simulation diff --git a/mppa_k1c/lib/Machblock.v b/mppa_k1c/lib/Machblock.v index 5a7f1782..08e0eba2 100644 --- a/mppa_k1c/lib/Machblock.v +++ b/mppa_k1c/lib/Machblock.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import Maps. Require Import AST. diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v index 2ba42814..287e4f7b 100644 --- a/mppa_k1c/lib/Machblockgen.v +++ b/mppa_k1c/lib/Machblockgen.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import Maps. Require Import AST. diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v index 0de2df52..dfb97bfe 100644 --- a/mppa_k1c/lib/Machblockgenproof.v +++ b/mppa_k1c/lib/Machblockgenproof.v @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib. Require Import Maps. Require Import AST. @@ -807,4 +821,4 @@ Proof. eapply ra_exists; eauto. Qed. -End Mach_Return_Address.
\ No newline at end of file +End Mach_Return_Address. diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v index 9db51bbb..d48dabf3 100644 --- a/powerpc/CSE2deps.v +++ b/powerpc/CSE2deps.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. diff --git a/powerpc/CSE2depsproof.v b/powerpc/CSE2depsproof.v index fdded9b6..123341da 100644 --- a/powerpc/CSE2depsproof.v +++ b/powerpc/CSE2depsproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml index 33be79e8..c48fdfba 100644 --- a/powerpc/DuplicateOpcodeHeuristic.ml +++ b/powerpc/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* open Camlcoq *) open Op open Integers diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v index 8ab9242a..b4b80e2f 100644 --- a/riscV/CSE2deps.v +++ b/riscV/CSE2deps.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v index a3811e78..f283c8ac 100644 --- a/riscV/CSE2depsproof.v +++ b/riscV/CSE2depsproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/riscV/DuplicateOpcodeHeuristic.ml b/riscV/DuplicateOpcodeHeuristic.ml index 2ec314c1..38702e1b 100644 --- a/riscV/DuplicateOpcodeHeuristic.ml +++ b/riscV/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* open Camlcoq *) open Op open Integers diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 0ce7a948..f8f46306 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -1,3 +1,15 @@ +/* *************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* David Monniaux CNRS, VERIMAG */ +/* */ +/* Copyright VERIMAG. All rights reserved. */ +/* This file is distributed under the terms of the INRIA */ +/* Non-Commercial License Agreement. */ +/* */ +/* *************************************************************/ + #include <stdint.h> #include <stdio.h> #include <stdlib.h> diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h index 7f111742..c884ae23 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_k1c_fixes.h @@ -1,3 +1,18 @@ +/* *************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* Sylvain Boulmé Grenoble-INP, VERIMAG */ +/* David Monniaux CNRS, VERIMAG */ +/* Cyril Six Kalray */ +/* */ +/* Copyright Kalray. Copyright VERIMAG. All rights reserved. */ +/* This file is distributed under the terms of the INRIA */ +/* Non-Commercial License Agreement. */ +/* */ +/* *************************************************************/ + + #ifndef __CCOMP_KIC_FIXES_H #define __CCOMP_KIC_FIXES_H diff --git a/runtime/include/math.h b/runtime/include/math.h index 01b8d8d8..422787e1 100644 --- a/runtime/include/math.h +++ b/runtime/include/math.h @@ -1,3 +1,17 @@ +/* *************************************************************/ +/* */ +/* The Compcert verified compiler */ +/* */ +/* Sylvain Boulmé Grenoble-INP, VERIMAG */ +/* David Monniaux CNRS, VERIMAG */ +/* Cyril Six Kalray */ +/* */ +/* Copyright Kalray. Copyright VERIMAG. All rights reserved. */ +/* This file is distributed under the terms of the INRIA */ +/* Non-Commercial License Agreement. */ +/* */ +/* *************************************************************/ + #ifndef _COMPCERT_MATH_H #define _COMPCERT_MATH_H diff --git a/x86/CSE2deps.v b/x86/CSE2deps.v index f4d9e254..a4b47a5c 100644 --- a/x86/CSE2deps.v +++ b/x86/CSE2deps.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. diff --git a/x86/CSE2depsproof.v b/x86/CSE2depsproof.v index 1e913254..fd088962 100644 --- a/x86/CSE2depsproof.v +++ b/x86/CSE2depsproof.v @@ -1,3 +1,15 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL Maps. diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml index 2ec314c1..38702e1b 100644 --- a/x86/DuplicateOpcodeHeuristic.ml +++ b/x86/DuplicateOpcodeHeuristic.ml @@ -1,3 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + (* open Camlcoq *) open Op open Integers |