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 /backend | |
| parent | 4f6c5833a149d0659f4bffaaeb464cd9864b3a9b (diff) | |
| download | compcert-kvx-c22a1828063756fdc11876993e6f1e2ca3bba04d.tar.gz compcert-kvx-c22a1828063756fdc11876993e6f1e2ca3bba04d.zip | |
Adding copyrights
Diffstat (limited to 'backend')
30 files changed, 358 insertions, 3 deletions
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. |