Merge pull request #1246 from MSoegtropIMC/compcert-3.7

Added latest CompCert version (3.7) and platform Flocq variant
coq · May 6, 2020 · 62a2628 · 62a2628
2 parents 7518f23 + 8e0602e
commit 62a2628
Show file tree

Hide file tree

Showing 14 changed files with 901 additions and 0 deletions.
diff --git a/released/packages/coq-compcert/coq-compcert.3.7/opam b/released/packages/coq-compcert/coq-compcert.3.7/opam
@@ -0,0 +1,40 @@
+opam-version: "2.0"
+authors: "Xavier Leroy <[email protected]>"
+maintainer: "Jacques-Henri Jourdan <[email protected]>"
+homepage: "http://compcert.inria.fr/"
+dev-repo: "git+https://github.com/AbsInt/CompCert.git"
+bug-reports: "https://github.com/AbsInt/CompCert/issues"
+license: "INRIA Non-Commercial License Agreement"
+build: [
+  ["./configure" "ia32-linux" {os = "linux"}
+  "ia32-macosx" {os = "macos"}
+  "ia32-cygwin" {os = "cygwin"}
+  "-bindir" "%{bin}%"
+  "-libdir" "%{lib}%/compcert"
+  "-install-coqdev"
+  "-clightgen"
+  "-coqdevdir" "%{lib}%/coq/user-contrib/compcert"
+  "-ignore-coq-version"]
+  [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" {>= "8.7.0" & < "8.12"}
+  "menhir" {>= "20190626" & < "20200123"}
+  "ocaml" {>= "4.05.0"}
+]
+synopsis: "The CompCert C compiler"
+tags: [
+  "category:CS/Semantics and Compilation/Compilation"
+  "category:CS/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "keyword:compiler"
+  "logpath:compcert"
+  "date:2020-03-21"
+]
+url {
+  src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz"
+  checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0"
+}
diff --git a/...rt.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/...rt.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
@@ -0,0 +1,82 @@
+From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001
+From: Xavier Leroy <[email protected]>
+Date: Wed, 29 Apr 2020 15:40:13 +0200
+Subject: [PATCH 01/12] Install "compcert.config" file along the Coq
+ development
+
+The file contains various parameters about the target processor and ABI,
+useful for VST and possibly other users of CompCert as a Coq library.
+
+It is in "var=val" syntax so that it can be included directly from
+a Makefile or a shell script.
+---
+ .gitignore |  1 +
+ Makefile   | 19 ++++++++++++++++++-
+ 2 files changed, 19 insertions(+), 1 deletion(-)
+
+diff --git a/.gitignore b/.gitignore
+index 6c10e1c3..b75ea5e7 100644
+--- a/.gitignore
++++ b/.gitignore
+@@ -31,6 +31,7 @@
+ /.depend
+ /.depend.extr
+ /compcert.ini
++/compcert.config
+ /x86/ConstpropOp.v
+ /x86/SelectOp.v
+ /x86/SelectLong.v
+diff --git a/Makefile b/Makefile
+index aed0da28..df5fb03f 100644
+--- a/Makefile
++++ b/Makefile
+@@ -147,6 +147,9 @@ endif
+ ifeq ($(CLIGHTGEN),true)
+ 	$(MAKE) clightgen
+ endif
++ifeq ($(INSTALL_COQDEV),true)
++	$(MAKE) compcert.config
++endif
+
+ proof: $(FILES:.v=.vo)
+
+@@ -224,6 +227,19 @@ compcert.ini: Makefile.config
+ 	 echo "response_file_style=$(RESPONSEFILE)";) \
+         > compcert.ini
+
++compcert.config: Makefile.config
++	(echo "# CompCert configuration parameters"; \
++        echo "COMPCERT_ARCH=$(ARCH)"; \
++        echo "COMPCERT_MODEL=$(MODEL)"; \
++        echo "COMPCERT_ABI=$(ABI)"; \
++        echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \
++        echo "COMPCERT_BITSIZE=$(BITSIZE)"; \
++        echo "COMPCERT_SYSTEM=$(SYSTEM)"; \
++        echo "COMPCERT_VERSION=$(BUILDVERSION)"; \
++        echo "COMPCERT_BUILDNR=$(BUILDNR)"; \
++        echo "COMPCERT_TAG=$(TAG)" \
++        ) > compcert.config
++
+ driver/Version.ml: VERSION
+ 	(echo 'let version = "$(BUILDVERSION)"'; \
+          echo 'let buildnr = "$(BUILDNR)"'; \
+@@ -258,6 +274,7 @@ ifeq ($(INSTALL_COQDEV),true)
+           install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
+ 	done
+ 	install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
++	install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
+ 	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
+ endif
+
+@@ -267,7 +284,7 @@ clean:
+ 	rm -f $(patsubst %, %/.*.aux, $(DIRS))
+ 	rm -rf doc/html doc/*.glob
+ 	rm -f driver/Version.ml
+-	rm -f compcert.ini
++	rm -f compcert.ini compcert.config
+ 	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
+ 	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
+ 	rm -f $(GENERATED) .depend
+-- 
+2.24.2 (Apple Git-127)
+
diff --git a/...rt.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/...rt.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
@@ -0,0 +1,60 @@
+From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001
+From: Xavier Leroy <[email protected]>
+Date: Sun, 3 May 2020 09:43:14 +0200
+Subject: [PATCH 07/12] Dual-license
+ aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}
+
+The corresponding files in all other ports are dual-licensed
+(GPL + non-commercial), there is no reason it should be different for
+aarch64.
+---
+ aarch64/Archi.v             | 3 +++
+ aarch64/CBuiltins.ml        | 3 +++
+ aarch64/extractionMachdep.v | 3 +++
+ 3 files changed, 9 insertions(+)
+
+diff --git a/aarch64/Archi.v b/aarch64/Archi.v
+index aef4ab77..24431cb2 100644
+--- a/aarch64/Archi.v
++++ b/aarch64/Archi.v
+@@ -6,6 +6,9 @@
+ (*                                                                     *)
+ (*  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.     *)
+ (*                                                                     *)
+ (* *********************************************************************)
+diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml
+index fdc1372d..dfd5b768 100644
+--- a/aarch64/CBuiltins.ml
++++ b/aarch64/CBuiltins.ml
+@@ -6,6 +6,9 @@
+ (*                                                                     *)
+ (*  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.     *)
+ (*                                                                     *)
+ (* *********************************************************************)
+diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
+index e82056e2..5f26dc28 100644
+--- a/aarch64/extractionMachdep.v
++++ b/aarch64/extractionMachdep.v
+@@ -6,6 +6,9 @@
+ (*                                                                     *)
+ (*  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.     *)
+ (*                                                                     *)
+ (* *********************************************************************)
+-- 
+2.24.2 (Apple Git-127)
+
diff --git a/...ert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch b/...ert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch
@@ -0,0 +1,28 @@
+From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001
+From: Xavier Leroy <[email protected]>
+Date: Mon, 4 May 2020 10:51:47 +0200
+Subject: [PATCH 08/12] Update the list of dual-licensed files
+
+Closes: #351
+---
+ LICENSE | 4 ++--
+ 1 file changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/LICENSE b/LICENSE
+index 5a7ae79f..61b84219 100644
+--- a/LICENSE
++++ b/LICENSE
+@@ -46,8 +46,8 @@ option) any later version:
+
+   all files in the exportclight/ directory
+
+-  the Archi.v, CBuiltins.ml, and extractionMachdep.v files
+-  in directories arm, powerpc, riscV, x86, x86_32, x86_64
++  the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files
++  in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64
+
+   extraction/extraction.v
+
+-- 
+2.24.2 (Apple Git-127)
+
diff --git a/...q-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch b/...q-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch
@@ -0,0 +1,123 @@
+From 05448adb7642b3c1189139cec18c914b116d5d40 Mon Sep 17 00:00:00 2001
+From: Michael Soegtrop <[email protected]>
+Date: Thu, 30 Apr 2020 16:25:19 +0200
+Subject: [PATCH 11/12] Use Coq platform supplied Flocq
+
+---
+ aarch64/Archi.v     | 2 +-
+ arm/Archi.v         | 2 +-
+ lib/Floats.v        | 2 +-
+ lib/IEEE754_extra.v | 2 +-
+ powerpc/Archi.v     | 2 +-
+ riscV/Archi.v       | 2 +-
+ x86_32/Archi.v      | 2 +-
+ x86_64/Archi.v      | 2 +-
+ 8 files changed, 8 insertions(+), 8 deletions(-)
+
+diff --git a/aarch64/Archi.v b/aarch64/Archi.v
+index 24431cb2..6c5655d8 100644
+--- a/aarch64/Archi.v
++++ b/aarch64/Archi.v
+@@ -16,7 +16,7 @@
+ (** Architecture-dependent parameters for AArch64 *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := true.
+diff --git a/arm/Archi.v b/arm/Archi.v
+index 16d6c71d..9b4cc96a 100644
+--- a/arm/Archi.v
++++ b/arm/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for ARM *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := false.
+diff --git a/lib/Floats.v b/lib/Floats.v
+index 6a126c3f..25a55620 100644
+--- a/lib/Floats.v
++++ b/lib/Floats.v
+@@ -17,7 +17,7 @@
+ (** Formalization of floating-point numbers, using the Flocq library. *)
+
+ Require Import Coqlib Zbits Integers.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits Core.
+ Require Import IEEE754_extra.
+ Require Import Program.
+diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
+index c23149be..d546c7d3 100644
+--- a/lib/IEEE754_extra.v
++++ b/lib/IEEE754_extra.v
+@@ -20,7 +20,7 @@
+ Require Import Psatz.
+ Require Import Bool.
+ Require Import Eqdep_dec.
+-(*From Flocq *)
++From Flocq
+ Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd.
+
+ Local Open Scope Z_scope.
+diff --git a/powerpc/Archi.v b/powerpc/Archi.v
+index 10f38391..5ada45f4 100644
+--- a/powerpc/Archi.v
++++ b/powerpc/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for PowerPC *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := false.
+diff --git a/riscV/Archi.v b/riscV/Archi.v
+index 61d129d0..4a929aac 100644
+--- a/riscV/Archi.v
++++ b/riscV/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for RISC-V *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Parameter ptr64 : bool.
+diff --git a/x86_32/Archi.v b/x86_32/Archi.v
+index e9d05c14..b5e4b638 100644
+--- a/x86_32/Archi.v
++++ b/x86_32/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for x86 in 32-bit mode *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := false.
+diff --git a/x86_64/Archi.v b/x86_64/Archi.v
+index 959d8dc1..59502b4a 100644
+--- a/x86_64/Archi.v
++++ b/x86_64/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for x86 in 64-bit mode *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := true.
+-- 
+2.24.2 (Apple Git-127)
+
diff --git a/...rt.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/...rt.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
@@ -0,0 +1,26 @@
+From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001
+From: Michael Soegtrop <[email protected]>
+Date: Tue, 5 May 2020 17:10:06 +0200
+Subject: [PATCH 12/12] Use platform supplied menhirlib as suggested by
+ jhjourdan
+
+---
+ Makefile | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/Makefile b/Makefile
+index 48770ebd..c4130630 100644
+--- a/Makefile
++++ b/Makefile
+@@ -265,7 +265,7 @@ driver/Version.ml: VERSION
+
+ cparser/Parser.v: cparser/Parser.vy
+ 	@rm -f $@
+-	$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
++	$(MENHIR) --coq cparser/Parser.vy
+ 	@chmod a-w $@
+
+ depend: $(GENERATED) depend1
+-- 
+2.24.2 (Apple Git-127)
+