From 285c4526e8ef24bec62b407ef6369a3b21afd9ba Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Thu, 7 May 2020 18:42:57 +0200 Subject: [PATCH 1/6] Changed build and CI system to use opam / coq-platform supplied CompCert - register opam-prerelease from VST git as local opam patch repo in Travis - install coq-compcert and coq-compcert-64 opam packages in Travis - Adjusted Makefile to use opam supplied CompCert (Support for building bundled CompCert is commented out and could be re-enabled with little effort) - Cleaned up and reorganized Makefile - Adjusted BUILD_ORGANIZATION.md to relfect these changes --- .travis.yml | 8 + BUILD_ORGANIZATION.md | 170 +++++++++++--------- Makefile | 352 ++++++++++++++++++++++++++---------------- 3 files changed, 322 insertions(+), 208 deletions(-) diff --git a/.travis.yml b/.travis.yml index 08c4675618..e6ee5e2c88 100644 --- a/.travis.yml +++ b/.travis.yml @@ -35,6 +35,7 @@ env: # - COMPILER="default" - COQ_VERSION="8.11.0" - NEXT_VERSION="8.11.0" + - COMPCERT_VERSION="3.7~coq-platform~open-source" branches: only: @@ -61,10 +62,17 @@ install: - opam config var root - opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev || true - opam repo add coq-released https://coq.inria.fr/opam/released +- opam repo add prerelease file://$(pwd)/opam-prerelease - opam update +- opam update prerelease +- opam repo list - opam show coq +- opam show coq-compcert +- opam show coq-compcert-64 - travis_wait 15 opam install -j ${NJOBS} -y coq=${COQ_VERSION} ${EXTRA_OPAM} - opam install -j ${NJOBS} -y coq=${COQ_VERSION} coq-ext-lib coq-flocq +- travis_wait 10 opam install -j ${NJOBS} -y coq-compcert=${COMPCERT_VERSION} +- travis_wait 10 opam install -j ${NJOBS} -y coq-compcert-64=${COMPCERT_VERSION} - opam list - file `which coqc` # - WC=`which coqc` diff --git a/BUILD_ORGANIZATION.md b/BUILD_ORGANIZATION.md index 3631fce31e..66ba300401 100644 --- a/BUILD_ORGANIZATION.md +++ b/BUILD_ORGANIZATION.md @@ -1,5 +1,11 @@ # HOW TO BUILD: +## Check compatibility + +If you install VST via opam, opam will take care of dependency versions. + +Otherwise please check: + 1. Make sure you have the right version of Coq. ```sh grep ^COQVERSION Makefile @@ -7,85 +13,105 @@ will tell you which versions are compatible. 2. Make sure you have the right version of CompCert. - VST 2.0 uses CompCert 3.2 for Coq 8.7.1 (or Coq 8.7 should work). - -### METHOD A [recommended] + VST 2.6 uses CompCert 3.7 for Coq 8.11 + +## Install Methods + +### Install via opam + +If you install VST via opam, opam will automatically install a +suitable version of CompCert, Flocq and other dependencies. +``` +opam install coq-vst +AND/OR +opam install coq-vst-64 +``` +You can install both the 32 bit and the 64 bit versions of VST and +CompCert in parallel. They will be installed in different folders. + +Please note that some opam supplied versions of CompCert use a version of +Flocq distributed with CompCert. This is problematic if you want to verify +numerical code which uses tools like CoqInterval or Gappa which also use +Flocq. The proofs these tools do might then not be compatible with VST +and CompCert. For CompCert 3.7 there is an opam version called +``` +coq-compcert.3.7~platform-flocq +coq-compcert-64.3.7~platform-flocq +``` +which uses the opam supplied version of Flocq. There is also a version +``` +coq-compcert.3.7~platform-flocq~open-source +coq-compcert-64.3.7~platform-flocq~open-source +``` +which only contains the dual licensed open source part of CompCert. This +is sufficient for learning VST using the example C programs provided and it +is the *default* dependency of VST. If you want to use VST for your own C code, +you need at least clightgen, which is *not* free software. Please clarify the +CompCert license conditions if you want to use clightgen. In case you want to +use clightgen, please use this install command: +``` +opam install coq-compcert.3.7~platform-flocq coq-vst +AND/OR +opam install coq-compcert-64.3.7~platform-flocq coq-vst +``` +VST can work with various installations of CompCert and this sequence ensures +you get the version you want. If you are an industrial user and want to +learn CompCert and ensure you only install open source software, please +use this install command: +``` +opam install coq-compcert.3.7~platform-flocq~open-source coq-vst +AND/OR +opam install coq-compcert-64.3.7~platform-flocq~open-source coq-vst +``` + +### Manual make with opam / coq-platform supplied CompCert + +For a manual make please follow this procedure: + +1. Make sure CompCert and Flocq Coq `.vo` files are installed in + ``` + /lib/coq/user-contrib/Flocq + /lib/coq/user-contrib/compcert + AND/OR + /lib/coq/user-contrib/compcert64 + ``` -This method bases the VST on a copy of certain CompCert specification files -distributed with VST, located in `VST/compcert`. +2. Make sure CompCert clightgen is installed in + ``` + /bin + ``` -1. Execute this command: +3. Execute this command: ``` make + OR + make BITSIZE=64 ``` (or, if you have a multicore computer, `make -j`) -2. *optional, only if you're going to run "clightgen"* - Unpack CompCert in the location of your choice (not under VST/), and in that - directory, - ``` - ./configure -clightgen x86_32-linux - make - ``` - -Use x86_32-macosx if you're on a Mac, x86_32-cygwin on Windows. -You may also use x86_64, but VST has not been as heavily tested in -64-bit configurations. You may also use other back ends besides x86, -but VST has not been much tested on those. - - -### METHOD B [alternate] - -This method bases the VST on the same specification files -that the CompCert compiler is built upon (in contrast to method A, -which uses verbatim copies of them). - -1. Unpack CompCert in a sibling directory to VST; - in that directory, build CompCert according to the instructions - ```sh - ./configure -clightgen x86_32-linux; - make - ``` -(Use x86_32-macosx if you're on a Mac, etc.) - -2. In the VST directory, create a file `CONFIGURE` containing exactly the text: - ``` - COMPCERT=../CompCert # or whatever is your path to compcert - ``` -3. In the VST directory, - ```sh - make - ``` - -Note on the Windows (cygwin) installation of CompCert: -To build CompCert you'll need an up to date version of the -menhir parser generator: http://gallium.inria.fr/~fpottier/menhir/ -To work around a cygwin incompatibility in the menhir build, -`touch src/.versioncheck` before doing `make`. - -### METHOD A64, METHOD B64: Sixty-four-bit (64 bit) build: -CompCert works with 64-bit architectures as well as 32-bit, -and VST now works with 64-bit or 32-bit CompCert. - -Using method A, put BITSIZE=64 (and nothing else) -in your CONFIGURE file, (do a fresh "make depend"), -and you'll get a 64-bit (x86_64) Verifiable C. - -Using method B, put COMPCERT=your-compcert-directory in your CONFIGURE file, -and in your-compcert-directory build with "./configure" specifying -a 64-bit architecture; and you'll get the corresponding 64-bit Verifiable C. -No need to specify BITSIZE in your CONFIGURE file. - -In the standard VST distribution, in the progs/ and sha/ directories -there are .v files built by clightgen from .c files. These are built -with a 32-bit clightgen, and will not be portable to 64-bit mode; -that is, they work if "make floyd" has been done with BITSIZE=32. - -The progs64/ directory contains a subset of the .c files from progs/, -compiled in 64-bit mode to the corresponding .v files. The files -progs64/verif_*.v are copied from progs/verif*.v with no change except -to replace "Import VST.progs.XXX" with "Import VST.progs64.XXX", -and will build only if "make floyd" has been done with BITSIZE=64. +Please note that in this case you should *not* have a file `CONFIGURE` in +the VST root folder as you would for method B and C below. + +### Manual make with advanced configuration + +If you want to use a different CompCert than teh default opam supplied +CompCert, you can configure the CompCert path by setting: +``` +COMPCERT=mycompcert +OR +COMPCERT_INST_PATH=/home/me/mycompcert +``` +`COMPCERT` names a Coq module path under `lib/coq/user-contrib`. +`COMPCERT_INST_PATH` names an arbitrary CompCert path, e.g. a local GIT build. + +Both variables can be set either on the make command line or in a file named +`CONFIGURE` in the VST source root folder which is read by the VST makefile. + +In addition you can define the variables `BITSIZE` and `ARCH`. If neither +`COMPCERT` nor `COMPCERT_INST_PATH` are set, `BITSIZE` can be used to +choose between `COMPCERT=compcert` and `COMPCERT=`compcert64`. In any case +it is checked if `BITSIZE` and `ARCH` match the configurazion information +found in `compcert-config` in the specified CompCert folder. -------------------------------------------------------------------------------- diff --git a/Makefile b/Makefile index ca3db05139..865d557aba 100755 --- a/Makefile +++ b/Makefile @@ -1,125 +1,234 @@ -# See the file BUILD_ORGANIZATION for -# explanations of why this is the way it is +# ########## Configuration ########## + +# See the file BUILD_ORGANIZATION.md +# for explanations of why this is the way it is. -COMPCERT ?= compcert -include CONFIGURE -#Note: You can make a CONFIGURE file with the definition -# COMPCERT=../compcert -# if, for example, you want to build from a compcert distribution -# that is sitting in a sister directory to vst. -# -# One can also add in CONFIGURE the line -# COQBIN=/path/to/bin/ -# to a directory containing the coqc/coqdep/... you wish to use, if it -# is not your path. -# -# You can override ARCH and BITSIZE in the configure file, too; -# otherwise ARCH and BITSIZE are taken from $(COMPCERT)/Makefile.config. -ifeq ($(BITSIZE),64) -PROGSDIR=progs64 -else -PROGSDIR=progs -endif +# ##### Configure Coq ##### -default_target: _CoqProject msl veric floyd $(PROGSDIR) +# ANNOTATE=true # label chatty output from coqc with file name +ANNOTATE=silent # suppress chatty output from coqc +# ANNOTATE=false # leave chatty output of coqc unchanged +# DO NOT DISABLE coqc WARNINGS! That would hinder the Coq team's continuous integration. +COQC=$(COQBIN)coqc +COQTOP=$(COQBIN)coqtop +COQDEP=$(COQBIN)coqdep -vos +COQDOC=$(COQBIN)coqdoc -d doc/html -g $(DEPFLAGS) +COQLIB=$(shell $(COQC) -where) +# Check Coq version -#Note2: By default, the rules for converting .c files to .v files -# are inactive. To activate them, do something like -#CLIGHTGEN=$(COMPCERT)/clightgen +COQVERSION= 8.11.0 or-else 8.11.1 or-else 8.11.2 or-else 8.12+beta1 or-else 8.12.0 -#Note3: for SSReflect, one solution is to install MathComp 1.6 -# somewhere add this line to a CONFIGURE file -# MATHCOMP=/my/path/to/mathcomp -# and on Windows, it might be MATHCOMP=c:/Coq/lib/user-contrib/mathcomp +COQV=$(shell $(COQC) -v) +ifneq ($(IGNORECOQVERSION),true) + ifeq ("$(filter $(COQVERSION),$(COQV))","") + $(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV)) + endif +endif -# ANNOTATE=true # label chatty output from coqc with file name -ANNOTATE=silent # suppress chatty output from coqc -# ANNOTATE=false # leave chatty output of coqc unchanged +# ##### Configure Compcert ##### -CC_TARGET= $(COMPCERT)/cfrontend/Clight.vo -CC_DIRS= lib common cfrontend exportclight -VSTDIRS= msl sepcomp veric floyd $(PROGSDIR) concurrency ccc26x86 -OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox atomics boringssl_fips_20180730 -DIRS = $(VSTDIRS) $(OTHERDIRS) -CONCUR = concurrency +# Note: You can make a CONFIGURE file with definitions like +# +# BITSIZE=64 (choose 64 bit compcert) +# ARCH=x86 (make sure compcert has architecture x86) +# +# COMPCERT=compcert (opam / coq-platform supplied compcert) +# COMPCERT=compcert64 (opam supplied 64 bit compcert) +# COMPCERT=mycompcert (private compcert installed in lib/coq/user-control) +# +# COMPCERT_INST_PATH=/home/me/compcert +# (user local compcert inplace build) +# +# COMPCERT_NEW (if defined enables compatibility options for +# new experimental compcert) +# +# Note: BITSIZE can be used to choose a 64 bit compcert but ARCH cannot be used +# to select non x86, because there is no standard name mapping. You need to +# set COMPCERT or COMPCERT_INST_PATH to choose a different architecture. +# But both will be chacked if you set COMPCERT or COMPCERT_INST_PATH, so you +# can set COMPCERT, BITSIZE and ARCH to make sure COMPCERT is what you want. +# +# Note: By default, the rules for converting .c files to .v files +# are inactive. To activate them, do something like +# CLIGHTGEN=$(my_local_bin_path)/clightgen + +BITSIZE ?= +ARCH ?= + +ifndef COMPCERT_INST_PATH + ifndef COMPCERT + ifeq ($(BITSIZE),) + COMPCERT ?= compcert + else ifeq ($(BITSIZE),32) + COMPCERT ?= compcert + else ifeq ($(BITSIZE),64) + COMPCERT ?= compcert64 + else + $(error ILLEGAL BITSIZE $(BITSIZE)) + endif + endif + COMPCERT_INST_PATH ?= $(COQLIB)/user-contrib/$(COMPCERT) +endif + +COMPCERT_CONFIG = $(COMPCERT_INST_PATH)/compcert.config + +# Verify that the version of the supplied compcert matches the version of the internal compcert CV1=$(shell cat compcert/VERSION) -CV2=$(shell cat $(COMPCERT)/VERSION) +CV2=$(shell cat $(COMPCERT_INST_PATH)/VERSION) -ifneq ($(COMPCERT), compcert_new) -ifneq ($(CV1), $(CV2)) - $(error COMPCERT_VERSION=$(CV1) but $(COMPCERT)/VERSION=$(CV2)) +ifndef COMPCERT_NEW + ifneq ($(CV1), $(CV2)) + $(error COMPCERT VERSION MISMATCH: COMPCERT_VERSION=$(CV1) but $(COMPCERT_INST_PATH)/VERSION=$(CV2)) + endif endif -ifeq ($(wildcard $(COMPCERT)/*/Clight.vo), ) -ifeq ($(COMPCERT), compcert) -else - $(error FIRST BUILD COMPCERT, by: cd $(COMPCERT); make clightgen) +# Verify that the version of the supplied clightgen matches the version of the internal compcert + +ifdef CLIGHTGEN + VERSION1= $(lastword $(shell $(CLIGHTGEN) --version)) + VERSION2= $(subst version=,,$(shell grep version compcert/VERSION)) + ifneq ($(VERSION1),$(VERSION2)) + $(warning clightgen version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2)) + endif endif + +# Verify that the supplied compcert folder is built (contains .vo files) + +ifeq ($(wildcard $(COMPCERT_INST_PATH)/*/Clight.vo), ) + $(error FIRST BUILD COMPCERT, by: cd $(COMPCERT_INST_PATH); make clightgen) endif + +# ##### Configure Architecture ##### + +ifeq ($(wildcard $(COMPCERT_CONFIG)),) + $(error Cannot find compcert.config in $(COMPCERT_INST_PATH)) endif -ARCH ?= $(shell awk 'BEGIN{FS="="}$$1=="ARCH"{print $$2}' $(COMPCERT)/Makefile.config) -BITSIZE ?= $(shell awk 'BEGIN{FS="="}$$1=="BITSIZE"{print $$2}' $(COMPCERT)/Makefile.config) +COMPCERT_ARCH ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_ARCH"{print $$2}' $(COMPCERT_CONFIG)) +COMPCERT_BITSIZE ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_BITSIZE"{print $$2}' $(COMPCERT_CONFIG)) -ifeq ($(COMPCERT), compcert_new) -BACKEND=backend -ifeq ($(wildcard $(COMPCERT)/$(ARCH)_$(BITSIZE)),) -ARCHDIRS=$(ARCH) +# Verify that the bitsize and architecture match + +ifneq ($(BITSIZE),) + ifneq ($(BITSIZE),$(COMPCERT_BITSIZE)) + $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_BITSIZE) but you requested $(BITSIZE)) + endif else -ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) + BITSIZE = $(COMPCERT_BITSIZE) endif + +ifneq ($(ARCH),) + ifneq ($(ARCH),$(COMPCERT_ARCH)) + $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_ARCH) but you requested $(ARCH)) + endif else -ifeq ($(wildcard $(COMPCERT)/$(ARCH)_$(BITSIZE)),) -ARCHDIRS=$(ARCH) + ARCH = $(COMPCERT_ARCH) +endif + +# Choose VST programs folder + +ifeq ($(BITSIZE),64) + PROGSDIR=progs64 else -ARCHDIRS=$(ARCH) $(ARCH)_$(BITSIZE) + PROGSDIR=progs endif + +ifdef COMPCERT_NEW + BACKEND=backend + ifeq ($(wildcard $(COMPCERT_INST_PATH)/$(ARCH)_$(BITSIZE)),) + ARCHDIRS=$(ARCH) + else + ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) + endif +else + ifeq ($(wildcard $(COMPCERT_INST_PATH)/$(ARCH)_$(BITSIZE)),) + ARCHDIRS=$(ARCH) + else + ARCHDIRS=$(ARCH) $(ARCH)_$(BITSIZE) + endif endif +# ##### Configure ssreflect / mathcomp ##### + +# This makefile assumes, that ssreflect / mathcomp is provided by the coq platform, +# that is found in $(coqc -where)/user-contrib/mathcomp. +# In case it is not, define in file CONFIGURE e.g.: + +# MATHCOMP=/my/path/to/mathcomp +# MATHCOMP=c:/Coq/lib/user-contrib/mathcomp + +# ##### Configure Flocq ##### -FLOCQ= # this mode to use the flocq packaged with Coq or opam +FLOCQ= # this mode to use the flocq packaged with Coq or opam # FLOCQ=flocq # this mode to use the flocq built into compcert + +# ########## Flags ########## + +VSTDIRS= msl sepcomp veric floyd $(PROGSDIR) concurrency ccc26x86 +OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox atomics boringssl_fips_20180730 +DIRS = $(VSTDIRS) $(OTHERDIRS) +CC_DIRS= lib common cfrontend exportclight + +# ##### Compcert Flags ##### + COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend exportclight $(BACKEND) $(FLOCQ) -COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d)) -EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) +COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) +EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) + +# Compcert Clightgen flags + +CGFLAGS = -DCOMPCERT + +#ifdef COMPCERT_NEW +#SHIM= -Q concurrency/shim VST.veric +#endif + +# ##### ExtLib Flags ##### + # ifneq ($(wildcard coq-ext-lib/theories),) # EXTFLAGS:=$(EXTFLAGS) -Q coq-ext-lib/theories ExtLib # endif + +# ##### Interaction Trees Flags ##### + ifneq ($(wildcard InteractionTrees/theories),) EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree endif + +# ##### FCF (Foundational Cryptography Framework) Flags ##### + ifneq ($(wildcard fcf/src/FCF),) EXTFLAGS:=$(EXTFLAGS) -Q fcf/src/FCF FCF -endif +endif# + +# ##### PaCo (Parameterized Coinduction) Flags ##### + ifneq ($(wildcard paco/src),) EXTFLAGS:=$(EXTFLAGS) -Q paco/src Paco endif -# for SSReflect +# ##### SSReflect Flags ##### + ifdef MATHCOMP - EXTFLAGS:=$(EXTFLAGS) -R $(MATHCOMP) mathcomp +EXTFLAGS:=$(EXTFLAGS) -R $(MATHCOMP) mathcomp endif -#ifeq ($(COMPCERT), compcert_new) -#SHIM= -Q concurrency/shim VST.veric -#endif +# ##### Flag summary ##### COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) #COQFLAGS= -Q . VST $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) DEPFLAGS:=$(COQFLAGS) -# DO NOT DISABLE coqc WARNINGS! That would hinder the Coq team's continuous integration. -COQC=$(COQBIN)coqc -COQTOP=$(COQBIN)coqtop -COQDEP=$(COQBIN)coqdep -vos -COQDOC=$(COQBIN)coqdoc -d doc/html -g $(DEPFLAGS) + +# ########## File Lists ########## MSL_FILES = \ Axioms.v Extensionality.v base.v eq_dec.v sig_isomorphism.v \ @@ -302,6 +411,7 @@ C64_ORDINARY = reverse.c revarray.c sumarray.c append.c bin_search.c \ global.c min.c nest2.c nest3.c \ logical_compare.c \ strlib.c switch.c union.c message.c + V64_ORDINARY = verif_reverse2.v verif_revarray.v verif_sumarray.v \ verif_append2.v verif_bin_search.v \ verif_bst.v verif_field_loadstore.v verif_float.v verif_object.v \ @@ -309,12 +419,6 @@ V64_ORDINARY = verif_reverse2.v verif_revarray.v verif_sumarray.v \ verif_logical_compare.v \ verif_strlib.v verif_switch.v verif_union.v verif_message.v -ifeq ($(BITSIZE),64) -PROGS_FILES=$(V64_ORDINARY) -else -PROGS_FILES=$(PROGS32_FILES) -endif - SHA_FILES= \ general_lemmas.v SHA256.v common_lemmas.v pure_lemmas.v sha_lemmas.v functional_prog.v \ sha.v spec_sha.v verif_sha_init.v \ @@ -416,14 +520,36 @@ FILES = \ # $(CONCUR_FILES:%=concurrency/%) \ # $(DRBG_FILES:%=verifiedDrbg/spec/%) +# ##### Derived file lists ##### + +CC_TARGET= $(COMPCERT_INST_PATH)/cfrontend/Clight.vo + +CVFILES = $(patsubst %.c,$(PROGSDIR)/%.v,$(C_FILES)) +CVOFILES = $(patsubst %.c,$(PROGSDIR)/%.vo,$(C_FILES)) + +ifeq ($(BITSIZE),64) +PROGS_FILES=$(V64_ORDINARY) +else +PROGS_FILES=$(PROGS32_FILES) +endif + +PROGS64_FILES= $(V64_ORDINARY) + + +# ########## Rules ########## + %_stripped.v: %.v # e.g., 'make progs/verif_reverse_stripped.v will remove the tutorial comments # from progs/verif_reverse.v grep -v '^.[*][*][ )]' $*.v >$@ - +# The check of compcert is only required for builds of bundled compcert. +# This is currently not supported, but keep it anyway until this is finally removed %.vo: COQF=$(if $(findstring compcert, $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS)) +# If CompCert changes, all .vo files need to be recompiled +%.vo: $(COMPCERT_CONFIG) + %.vo: %.v @echo COQC $*.v ifeq ($(TIMINGS), true) @@ -442,9 +568,6 @@ else # @util/annotate $(COQC) $(COQF) $*.v endif -# you can also write, COQVERSION= 8.6 or-else 8.6pl2 or-else 8.6pl3 (etc.) -COQVERSION= 8.11.0 or-else 8.11.1 or-else 8.11.2 or-else 8.12+beta1 or-else 8.12.0 - COQV=$(shell $(COQC) -v) ifeq ($(IGNORECOQVERSION),true) else @@ -453,27 +576,11 @@ else endif endif +# ########## Targets ########## +default_target: _CoqProject msl veric floyd $(PROGSDIR) -# This is causing problems, so commented out. -- Appel, Feb 23, 2017 -# $(COMPCERT)/lib/%.vo: $(COMPCERT)/lib/%.v -# @ -# $(COMPCERT)/common/%.vo: $(COMPCERT)/common/%.v -# @ -# $(COMPCERT)/cfrontend/%.vo: $(COMPCERT)/cfrontend/%.v -# @ -# $(COMPCERT)/exportclight/%.vo: $(COMPCERT)/exportclight/%.v -# @ -# $(COMPCERT)/flocq/Appli/%.vo: $(COMPCERT)/flocq/Appli/%.v -# @ -# $(COMPCERT)/flocq/Calc/%.vo: $(COMPCERT)/flocq/Calc/%.v -# @ -# $(COMPCERT)/flocq/Core/%.vo: $(COMPCERT)/flocq/Core/%.v -# @ -# $(COMPCERT)/flocq/Prop/%.vo: $(COMPCERT)/flocq/Prop/%.v -# @ -# $(COMPCERT)/flocq/%.vo: $(COMPCERT)/flocq/%.v -# @ +all: default_target files travis io hmacdrbg tweetnacl aes ifeq ($(BITSIZE),64) travis: default_target progs @@ -483,19 +590,6 @@ endif files: _CoqProject $(FILES:.v=.vo) -all: default_target files travis io hmacdrbg tweetnacl aes - - -# ifeq ($(COMPCERT), compcert) -# compcert: $(COMPCERT)/exportclight/Clightdefs.vo -# $(COMPCERT)/exportclight/Clightdefs.vo: -# cd $(COMPCERT) && $(MAKE) exportclight/Clightdefs.vo -# $(patsubst %.v,sepcomp/%.vo,$(SEPCOMP_FILES)): compcert -# $(patsubst %.v,veric/%.vo,$(VERIC_FILES)): compcert -# $(patsubst %.v,floyd/%.vo,$(FLOYD_FILES)): compcert -# msl/Coqlib2.vo: compcert -# endif - msl: _CoqProject $(MSL_FILES:%.v=msl/%.vo) sepcomp: _CoqProject $(CC_TARGET) $(SEPCOMP_FILES:%.v=sepcomp/%.vo) concurrency: _CoqProject $(CC_TARGET) $(SEPCOMP_FILES:%.v=sepcomp/%.vo) $(CONCUR_FILES:%.v=concurrency/%.vo) @@ -522,11 +616,7 @@ mailbox: _CoqProject mailbox/verif_mailbox_all.vo atomics: _CoqProject atomics/verif_kvnode_atomic.vo atomics/verif_kvnode_atomic_ra.vo atomics/verif_hashtable_atomic.vo atomics/verif_hashtable_atomic_ra.vo io: _CoqProject progs/verif_printf.vo progs/verif_io.vo progs/verif_io_mem.vo progs/io_specs.vo floyd/printf.vo InteractionTrees/theories/Events/Nondeterminism.vo -CGFLAGS = -DCOMPCERT - -$(patsubst %.c,$(PROGSDIR)/%.vo,$(C_FILES)): compcert - -CVFILES = $(patsubst %.c,$(PROGSDIR)/%.v,$(C_FILES)) +$(CVOFILES): compcert cvfiles: $(CVFILES) @@ -541,14 +631,8 @@ dochtml-full: clean_cvfiles: rm $(CVFILES) -ifdef CLIGHTGEN -VERSION1= $(lastword $(shell $(CLIGHTGEN) --version)) -VERSION2= $(subst version=,,$(shell grep version compcert/VERSION)) -ifneq ($(VERSION1),$(VERSION2)) -$(warning clightgen version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2)) -endif - # SPECIAL-CASE RULES FOR LINKED_C_FILES: +ifdef CLIGHTGEN sha/sha.v sha/hmac.v hmacdrbg/hmac_drbg.v sha/hkdf.v: sha/sha.c sha/hmac.c hmacdrbg/hmac_drbg.c sha/hkdf.c $(CLIGHTGEN) ${CGFLAGS} $^ $(PROGSDIR)/even.v: $(PROGSDIR)/even.c $(PROGSDIR)/odd.c @@ -569,7 +653,7 @@ endif veric/version.v: VERSION $(MSL_FILES:%=msl/%) $(SEPCOMP_FILES:%=sepcomp/%) $(VERIC_FILES:%=veric/%) $(FLOYD_FILES:%=floyd/%) sh util/make_version -_CoqProject _CoqProject-export: Makefile util/coqflags +_CoqProject _CoqProject-export: Makefile util/coqflags $(COMPCERT_CONFIG) echo $(COQFLAGS) > _CoqProject util/coqflags > _CoqProject-export @@ -577,20 +661,17 @@ floyd/floyd.coq: floyd/proofauto.vo coqtop $(COQFLAGS) -load-vernac-object floyd/proofauto -outputstate floyd/floyd -batch .depend depend: -# @echo "Copying Clight_core.v ... " -# ifeq ($(COMPCERT), compcert_new) -# @cp -p concurrency/shim/Clight_core.v veric/Clight_core.v -# else -# @cp -p veric/Clight_core_standard.v veric/Clight_core.v -# endif @echo 'coqdep ... >.depend' - $(COQDEP) $(COMPCERT_R_FLAGS) 2>&1 >.depend `find $(addprefix $(COMPCERT)/,$(COMPCERTDIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true -ifeq ($(COMPCERT), compcert_new) - $(COQDEP) $(COQFLAGS) 2>&1 >>.depend `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true +ifdef COMPCERT_NEW + $(COQDEP) $(COQFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true @echo "" >>.depend else - $(COQDEP) $(COQFLAGS) 2>&1 >>.depend `find $(addprefix $(COMPCERT)/,$(COMPCERTDIRS)) $(filter $(wildcard *), $(DIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true + $(COQDEP) $(COQFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true endif +# This version of the Makefile doesn't build compcert any more +# The build of compcert essentially works by analyzing and telling make the dependencies +# If this is desired, the below line can be enabled (conditionally) +# $(COQDEP) $(COMPCERT_R_FLAGS) 2>&1 >.depend `find $(addprefix $(COMPCERT_INST_PATH)/,$(COMPCERTDIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true # ifneq ($(wildcard coq-ext-lib/theories),) # $(COQDEP) -Q coq-ext-lib/theories ExtLib coq-ext-lib/theories >>.depend # endif @@ -605,6 +686,7 @@ endif ifneq ($(wildcard paco/src),) $(COQDEP) -Q paco/src Paco paco/src/*.v >>.depend endif + wc .depend clean: rm -f $(addprefix veric/version., v vo vos vok glob) .lia.cache .nia.cache floyd/floyd.coq .depend _CoqProject _CoqProject-export $(wildcard */.*.aux) $(wildcard */*.glob) $(wildcard */*.vo */*.vos */*.vok) compcert/*/*.{vo,vos,vok} compcert/*/*/*.{vo,vos,vok} compcert_new/*/*.{vo,vos,vok} compcert_new/*/*/*.{vo,vos,vok} @@ -639,8 +721,6 @@ FIX64= "BEGIN{print \"(* Do not edit this file, it was generated automatically * progs64/verif_%.v: progs/verif_%.v $(if $(findstring $(@F), $(V64_ORDINARY)), awk $(FIX64) < $< > $@) -PROGS64_FILES= $(V64_ORDINARY) - progs64c: $(C64_ORDINARY:%.c=progs64/%.c) progs64v: progs64c $(V64_ORDINARY:%.v=progs64/%.v) $(C64_ORDINARY:%.c=progs64/%.v) depend progs64: _CoqProject $(PROGS64_FILES:%.v=progs64/%.vo) From d598d0fcf691fb04dc19bc24d9e2011c7dbce08f Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Sat, 27 Jun 2020 12:51:04 +0200 Subject: [PATCH 2/6] Added opam patch repo e.g. for pre release CompCert opam files - Added 64 bit CompCert variant - Added 64 bit CompCert variant with coq-platform supplied Flocq and MenhirLib - Added 64 bit CompCert variant with only open source files --- .../coq-compcert-64/coq-compcert-64.3.7/opam | 40 ++++++ ....config-file-along-the-Coq-developme.patch | 82 ++++++++++++ ...ch64-Archi.v-Cbuiltins.ml-extraction.patch | 60 +++++++++ ...date-the-list-of-dual-licensed-files.patch | 28 ++++ ...0011-Use-Coq-platform-supplied-Flocq.patch | 123 ++++++++++++++++++ ...plied-menhirlib-as-suggested-by-jhjo.patch | 26 ++++ .../coq-compcert-64.3.7~coq-platform/opam | 57 ++++++++ ....config-file-along-the-Coq-developme.patch | 82 ++++++++++++ ...ch64-Archi.v-Cbuiltins.ml-extraction.patch | 60 +++++++++ ...date-the-list-of-dual-licensed-files.patch | 28 ++++ ...-Added-open-source-build-to-makefile.patch | 106 +++++++++++++++ ...0011-Use-Coq-platform-supplied-Flocq.patch | 123 ++++++++++++++++++ ...plied-menhirlib-as-suggested-by-jhjo.patch | 26 ++++ .../opam | 60 +++++++++ opam-prerelease/repo | 2 + opam-prerelease/version | 1 + 16 files changed, 904 insertions(+) create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch create mode 100644 opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam create mode 100644 opam-prerelease/repo create mode 100644 opam-prerelease/version diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam new file mode 100644 index 0000000000..89023dfc61 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam @@ -0,0 +1,40 @@ +opam-version: "2.0" +authors: "Xavier Leroy " +maintainer: "Jacques-Henri Jourdan " +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" "amd64-linux" {os = "linux"} + "amd64-macosx" {os = "macos"} + "amd64-cygwin" {os = "cygwin"} + "-bindir" "%{bin}%" + "-libdir" "%{lib}%/compcert" + "-install-coqdev" + "-clightgen" + "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64" + "-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:compcert64" + "date:2020-03-21" +] +url { + src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz" + checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0" +} diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch new file mode 100644 index 0000000000..d160e66e23 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.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 +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch new file mode 100644 index 0000000000..f74202a53c --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.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 +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch new file mode 100644 index 0000000000..57bef5e519 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.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 +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch new file mode 100644 index 0000000000..0dc512b457 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.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 <7895506+MSoegtropIMC@users.noreply.github.com> +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch new file mode 100644 index 0000000000..58a641f077 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.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 <7895506+MSoegtropIMC@users.noreply.github.com> +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) + diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam new file mode 100644 index 0000000000..3f2b5c1d05 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam @@ -0,0 +1,57 @@ +opam-version: "2.0" +authors: "Xavier Leroy " +maintainer: "Jacques-Henri Jourdan " +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" +version: "3.7" +build: [ + ["./configure" "amd64-linux" {os = "linux"} + "amd64-macosx" {os = "macos"} + "amd64-cygwin" {os = "cygwin"} + "-bindir" "%{bin}%" + "-libdir" "%{lib}%/compcert" + "-install-coqdev" + "-clightgen" + "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64" + "-ignore-coq-version"] + [make "-j%{jobs}%" {ocaml:version >= "4.06"}] +] +patches: [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "0008-Update-the-list-of-dual-licensed-files.patch" + "0011-Use-Coq-platform-supplied-Flocq.patch" + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" +] +extra-files: [ + ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] + ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] + ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] + ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] + ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] +] +install: [ + [make "install"] +] +depends: [ + "coq" {>= "8.7.0" & < "8.12"} + "coq-flocq" {>= "3.2.1"} + "coq-menhirlib" {>= "20190626" & < "20200123"} + "menhir" {>= "20190626" & < "20200123"} + "ocaml" {>= "4.05.0"} +] +synopsis: "The CompCert C compiler (using coq-platform supplied version of Flocq)" +tags: [ + "category:CS/Semantics and Compilation/Compilation" + "category:CS/Semantics and Compilation/Semantics" + "keyword:C" + "keyword:compiler" + "logpath:compcert64" + "date:2020-04-29" +] +url { + src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz" + checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0" +} diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch new file mode 100644 index 0000000000..d160e66e23 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/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 +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch new file mode 100644 index 0000000000..f74202a53c --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/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 +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch new file mode 100644 index 0000000000..57bef5e519 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/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 +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch new file mode 100644 index 0000000000..28dbd06878 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch @@ -0,0 +1,106 @@ +From b55c97d7930caec06d559faae4684761f258fd0f Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Thu, 30 Apr 2020 13:50:08 +0200 +Subject: [PATCH 10/12] Added open source build to makefile + +--- + Makefile | 36 +++++++++++++++++++++++++++++++++--- + 1 file changed, 33 insertions(+), 3 deletions(-) + +diff --git a/Makefile b/Makefile +index df5fb03f..48770ebd 100644 +--- a/Makefile ++++ b/Makefile +@@ -57,10 +57,14 @@ FLOCQ=\ + Relative.v Sterbenz.v Round_odd.v Double_rounding.v \ + Binary.v Bits.v + ++# Architecture files (in respective architecture folder) ++ ++ARCHFILES=Archi.v ++ + # General-purpose libraries (in lib/) + + VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ +- Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ ++ Iteration.v Zbits.v Integers.v IEEE754_extra.v Floats.v \ + Parmov.v UnionFind.v Wfsimpl.v \ + Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v + +@@ -101,6 +105,8 @@ BACKEND=\ + Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ + Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v + ++BACKEND_OPEN_SOURCE=Cminor.v ++ + # C front-end modules (in cfrontend/) + + CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ +@@ -110,6 +116,8 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ + Cshmgen.v Cshmgenproof.v \ + Csharpminor.v Cminorgen.v Cminorgenproof.v + ++CFRONTEND_OPEN_SOURCE=Clight.v ClightBigstep.v Cop.v Csem.v Cstrategy.v Csyntax.v Ctypes.v Ctyping.v ++ + # Parser + + PARSER=Cabs.v Parser.v +@@ -126,9 +134,17 @@ DRIVER=Compopts.v Compiler.v Complements.v + + # All source files + +-FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ ++FILES=$(ARCHFILES) $(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ + $(MENHIRLIB) $(PARSER) + ++# All open source source files (in the order given in LICENSE) ++ ++# ATTENTION: this also includes ./x86/Builtins1.vo - which is not open source but many files depend on it ++ ++FILES_OPEN_SOURCE=$(VLIB) $(COMMON) $(CFRONTEND_OPEN_SOURCE) $(BACKEND_OPEN_SOURCE) $(PARSER) Clightdefs.v $(ARCHFILES) ++ ++# These files have non open dependencies: extractionMachdep.v, extraction.v ++ + # Generated source files + + GENERATED=\ +@@ -153,6 +169,8 @@ endif + + proof: $(FILES:.v=.vo) + ++proof_open_source: $(FILES_OPEN_SOURCE:.v=.vo) compcert.config ++ + # Turn off some warnings for compiling Flocq + flocq/%.vo: COQCOPTS+=-w -compatibility-notation + +@@ -181,7 +199,7 @@ runtime: + + FORCE: + +-.PHONY: proof extraction runtime FORCE ++.PHONY: proof proof_open_source extraction runtime FORCE + + documentation: $(FILES) + mkdir -p doc/html +@@ -278,6 +296,18 @@ ifeq ($(INSTALL_COQDEV),true) + @(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README + endif + ++# ToDo: copy exactly the files in FILES_OPEN_SOURCE as soon as the issue with Builtins1 ins fixed ++install_open_source: ++ifeq ($(INSTALL_COQDEV),true) ++ install -d $(DESTDIR)$(COQDEVDIR) ++ for d in $(DIRS); do \ ++ install -d $(DESTDIR)$(COQDEVDIR)/$$d && \ ++ 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 + + clean: + rm -f $(patsubst %, %/*.vo*, $(DIRS)) +-- +2.24.2 (Apple Git-127) + diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch new file mode 100644 index 0000000000..0dc512b457 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch @@ -0,0 +1,123 @@ +From 05448adb7642b3c1189139cec18c914b116d5d40 Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +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/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch new file mode 100644 index 0000000000..58a641f077 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/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 <7895506+MSoegtropIMC@users.noreply.github.com> +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) + diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam new file mode 100644 index 0000000000..19e04fa9cc --- /dev/null +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam @@ -0,0 +1,60 @@ +opam-version: "2.0" +authors: "Xavier Leroy " +maintainer: "Jacques-Henri Jourdan " +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" +version: "3.7" +build: [ + ["./configure" "amd64-linux" {os = "linux"} + "amd64-macosx" {os = "macos"} + "amd64-cygwin" {os = "cygwin"} + "-bindir" "%{bin}%" + "-libdir" "%{lib}%/compcert" + "-install-coqdev" + "-clightgen" + "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64" + "-ignore-coq-version"] + [make "depend"] + [make "-j%{jobs}%" {ocaml:version >= "4.06"} "proof_open_source"] +] +patches: [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "0008-Update-the-list-of-dual-licensed-files.patch" + "0010-Added-open-source-build-to-makefile.patch" + "0011-Use-Coq-platform-supplied-Flocq.patch" + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" +] +extra-files: [ + ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] + ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] + ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] + ["0010-Added-open-source-build-to-makefile.patch" "sha256=fc3b8c1e097b53f209e7cf2e9b2e822609e8370857dbf1a4b34d909c37dcdfb5"] + ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] + ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] +] +install: [ + [make "install_open_source"] +] +depends: [ + "coq" {>= "8.7.0" & < "8.12"} + "coq-flocq" {>= "3.2.1"} + "coq-menhirlib" {>= "20190626" & < "20200123"} + "menhir" {>= "20190626" & < "20200123"} + "ocaml" {>= "4.05.0"} +] +synopsis: "The CompCert C compiler (only open source files + using coq-platform)" +tags: [ + "category:CS/Semantics and Compilation/Compilation" + "category:CS/Semantics and Compilation/Semantics" + "keyword:C" + "keyword:compiler" + "logpath:compcert64" + "date:2020-04-29" +] +url { + src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz" + checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0" +} diff --git a/opam-prerelease/repo b/opam-prerelease/repo new file mode 100644 index 0000000000..377582a773 --- /dev/null +++ b/opam-prerelease/repo @@ -0,0 +1,2 @@ +opam-version: "2.0" + diff --git a/opam-prerelease/version b/opam-prerelease/version new file mode 100644 index 0000000000..77d6f4ca23 --- /dev/null +++ b/opam-prerelease/version @@ -0,0 +1 @@ +0.0.0 From 4acb41a02a43678ea7e0cb4c14bfeeb89890909f Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Sat, 27 Jun 2020 21:54:51 +0200 Subject: [PATCH 3/6] Bundled COmpCert build works, but parameters need to be improved --- BUILD_ORGANIZATION.md | 45 ++++++++++++++-- Makefile | 123 ++++++++++++++++++++++++++---------------- 2 files changed, 116 insertions(+), 52 deletions(-) diff --git a/BUILD_ORGANIZATION.md b/BUILD_ORGANIZATION.md index 66ba300401..3eb2d44921 100644 --- a/BUILD_ORGANIZATION.md +++ b/BUILD_ORGANIZATION.md @@ -52,7 +52,7 @@ use clightgen, please use this install command: ``` opam install coq-compcert.3.7~platform-flocq coq-vst AND/OR -opam install coq-compcert-64.3.7~platform-flocq coq-vst +opam install coq-compcert-64.3.7~platform-flocq coq-vst-64 ``` VST can work with various installations of CompCert and this sequence ensures you get the version you want. If you are an industrial user and want to @@ -90,11 +90,46 @@ For a manual make please follow this procedure: (or, if you have a multicore computer, `make -j`) Please note that in this case you should *not* have a file `CONFIGURE` in -the VST root folder as you would for method B and C below. +the VST root folder as you might for the next method. -### Manual make with advanced configuration +### Manual make with bundled CompCert -If you want to use a different CompCert than teh default opam supplied +VST includes two bundled variants of CompCert, which in some releases of +VST might include changes to support new features of VST. The bundled +variants are in the VST root folder under +``` +/compcert +/compcert_new +``` +Please note that by default VST uses a platform supplied CompCert and +not the bundled CompCert. In case you want to use one of the bundled +CompCert variants, please use these options: +``` +COMPCERT_INST_PATH=/compcert +``` +OR +``` +COMPCERT_INST_PATH=/compcert_new +COMPCERT_NEW +``` +The COMPCERT_NEW flag sets a few additional makefile options required to +build the variant in `/compcert_new` and must be set if this +folder is specified for `COMPCERT_INST_PATH`. + +You can set the additional options `BITSIZE` and `ARCH`. The supported +variants are: +``` +ARCH=x86 BITSIZE=32 (default) +ARCH=x86 BITSIZE=64 +ARCH=aarch64 BITSIZE=64 +ARCH=powerpc BITSIZE=32 +``` +Both variables can be set either on the make command line or in a file named +`CONFIGURE` in the VST source root folder which is read by the VST makefile. + +### Manual make with private build of CompCert and/or advanced options + +If you want to use a different CompCert than the default opam supplied CompCert, you can configure the CompCert path by setting: ``` COMPCERT=mycompcert @@ -109,7 +144,7 @@ Both variables can be set either on the make command line or in a file named In addition you can define the variables `BITSIZE` and `ARCH`. If neither `COMPCERT` nor `COMPCERT_INST_PATH` are set, `BITSIZE` can be used to -choose between `COMPCERT=compcert` and `COMPCERT=`compcert64`. In any case +choose between `COMPCERT=compcert` and `COMPCERT=compcert64`. In any case it is checked if `BITSIZE` and `ARCH` match the configurazion information found in `compcert-config` in the specified CompCert folder. diff --git a/Makefile b/Makefile index 865d557aba..de294a9c7c 100755 --- a/Makefile +++ b/Makefile @@ -60,6 +60,7 @@ BITSIZE ?= ARCH ?= ifndef COMPCERT_INST_PATH + PLATFORM_COMPCERT = true ifndef COMPCERT ifeq ($(BITSIZE),) COMPCERT ?= compcert @@ -72,9 +73,12 @@ ifndef COMPCERT_INST_PATH endif endif COMPCERT_INST_PATH ?= $(COQLIB)/user-contrib/$(COMPCERT) + COMPCERT_CONFIG = $(COMPCERT_INST_PATH)/compcert.config +else + PLATFORM_COMPCERT = false + COMPCERT_CONFIG = endif -COMPCERT_CONFIG = $(COMPCERT_INST_PATH)/compcert.config # Verify that the version of the supplied compcert matches the version of the internal compcert @@ -99,35 +103,71 @@ endif # Verify that the supplied compcert folder is built (contains .vo files) -ifeq ($(wildcard $(COMPCERT_INST_PATH)/*/Clight.vo), ) +ifeq ($(PLATFORM_COMPCERT), true) + ifeq ($(wildcard $(COMPCERT_INST_PATH)/*/Clight.vo), ) $(error FIRST BUILD COMPCERT, by: cd $(COMPCERT_INST_PATH); make clightgen) + endif endif # ##### Configure Architecture ##### -ifeq ($(wildcard $(COMPCERT_CONFIG)),) +# Choose / test BITSIZE and ARCH + +ifeq ($(PLATFORM_COMPCERT), true) + + # We are using a platform supplied CompCert + + ifeq ($(wildcard $(COMPCERT_CONFIG)),) $(error Cannot find compcert.config in $(COMPCERT_INST_PATH)) -endif + endif + + COMPCERT_ARCH ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_ARCH"{print $$2}' $(COMPCERT_CONFIG)) + COMPCERT_BITSIZE ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_BITSIZE"{print $$2}' $(COMPCERT_CONFIG)) -COMPCERT_ARCH ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_ARCH"{print $$2}' $(COMPCERT_CONFIG)) -COMPCERT_BITSIZE ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_BITSIZE"{print $$2}' $(COMPCERT_CONFIG)) + # Verify that the bitsize and architecture match -# Verify that the bitsize and architecture match + ifneq ($(BITSIZE),) + ifneq ($(BITSIZE),$(COMPCERT_BITSIZE)) + $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_BITSIZE) but you requested $(BITSIZE)) + endif + else + BITSIZE = $(COMPCERT_BITSIZE) + endif -ifneq ($(BITSIZE),) - ifneq ($(BITSIZE),$(COMPCERT_BITSIZE)) - $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_BITSIZE) but you requested $(BITSIZE)) + ifneq ($(ARCH),) + ifneq ($(ARCH),$(COMPCERT_ARCH)) + $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_ARCH) but you requested $(ARCH)) + endif + else + ARCH = $(COMPCERT_ARCH) endif + else - BITSIZE = $(COMPCERT_BITSIZE) -endif -ifneq ($(ARCH),) - ifneq ($(ARCH),$(COMPCERT_ARCH)) - $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_ARCH) but you requested $(ARCH)) + # We are using a self build CompCert + + ifeq ($(BITSIZE),) + BITSIZE = 32 + endif + + ifeq ($(ARCH),) + ARCH = x86 endif + +endif + +# Choose CompCert architecture folder + +ifeq ($(wildcard $(COMPCERT_INST_PATH)/$(ARCH)_$(BITSIZE)),) + ARCHDIRS=$(ARCH) else - ARCH = $(COMPCERT_ARCH) + ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +endif + +# Add CompCert backend folder for COMPCERT_NEW + +ifdef COMPCERT_NEW + BACKEND=backend endif # Choose VST programs folder @@ -138,20 +178,6 @@ else PROGSDIR=progs endif -ifdef COMPCERT_NEW - BACKEND=backend - ifeq ($(wildcard $(COMPCERT_INST_PATH)/$(ARCH)_$(BITSIZE)),) - ARCHDIRS=$(ARCH) - else - ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) - endif -else - ifeq ($(wildcard $(COMPCERT_INST_PATH)/$(ARCH)_$(BITSIZE)),) - ARCHDIRS=$(ARCH) - else - ARCHDIRS=$(ARCH) $(ARCH)_$(BITSIZE) - endif -endif # ##### Configure ssreflect / mathcomp ##### @@ -173,14 +199,18 @@ FLOCQ= # this mode to use the flocq packaged with Coq or opam VSTDIRS= msl sepcomp veric floyd $(PROGSDIR) concurrency ccc26x86 OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox atomics boringssl_fips_20180730 DIRS = $(VSTDIRS) $(OTHERDIRS) -CC_DIRS= lib common cfrontend exportclight # ##### Compcert Flags ##### COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend exportclight $(BACKEND) $(FLOCQ) -COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) -EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) +ifeq ($(PLATFORM_COMPCERT),true) + COMPCERT_R_FLAGS= + EXTFLAGS= +else + COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) + EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) +endif # Compcert Clightgen flags @@ -224,9 +254,15 @@ endif COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) -#COQFLAGS= -Q . VST $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) DEPFLAGS:=$(COQFLAGS) +# ##### Print configuration summary ##### + +$(info ===== CONFIGURATION SUMMARY =====) +$(info BITSIZE=$(BITSIZE)) +$(info ARCH=$(ARCH)) +$(info COQFLAGS=$(COQFLAGS)) +$(info =================================) # ########## File Lists ########## @@ -543,8 +579,6 @@ PROGS64_FILES= $(V64_ORDINARY) # from progs/verif_reverse.v grep -v '^.[*][*][ )]' $*.v >$@ -# The check of compcert is only required for builds of bundled compcert. -# This is currently not supported, but keep it anyway until this is finally removed %.vo: COQF=$(if $(findstring compcert, $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS)) # If CompCert changes, all .vo files need to be recompiled @@ -568,13 +602,6 @@ else # @util/annotate $(COQC) $(COQF) $*.v endif -COQV=$(shell $(COQC) -v) -ifeq ($(IGNORECOQVERSION),true) -else - ifeq ("$(filter $(COQVERSION),$(COQV))","") - $(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV)) - endif -endif # ########## Targets ########## @@ -663,15 +690,17 @@ floyd/floyd.coq: floyd/proofauto.vo .depend depend: @echo 'coqdep ... >.depend' ifdef COMPCERT_NEW + # DEPENDENCIES VARIANT COMPCERT_NEW $(COQDEP) $(COQFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true @echo "" >>.depend else + # DEPENDENCIES DEFAULT $(COQDEP) $(COQFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true endif -# This version of the Makefile doesn't build compcert any more -# The build of compcert essentially works by analyzing and telling make the dependencies -# If this is desired, the below line can be enabled (conditionally) -# $(COQDEP) $(COMPCERT_R_FLAGS) 2>&1 >.depend `find $(addprefix $(COMPCERT_INST_PATH)/,$(COMPCERTDIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true +ifeq ($(PLATFORM_COMPCERT),false) + # DEPENDENCIES LOCAL COMPCERT + $(COQDEP) $(COMPCERT_R_FLAGS) 2>&1 >>.depend `find $(addprefix $(COMPCERT_INST_PATH)/,$(COMPCERTDIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true +endif # ifneq ($(wildcard coq-ext-lib/theories),) # $(COQDEP) -Q coq-ext-lib/theories ExtLib coq-ext-lib/theories >>.depend # endif From a984a95853ec2ba247d4d9624db886a277705a44 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Sun, 28 Jun 2020 20:43:45 +0200 Subject: [PATCH 4/6] Platform 32+64, bundled 32+64, external CompCert work --- Makefile | 213 +++++++++++------- .../coq-compcert-64/coq-compcert-64.3.7/opam | 19 +- .../coq-compcert-64.3.7~coq-platform/opam | 19 +- .../opam | 19 +- 4 files changed, 172 insertions(+), 98 deletions(-) diff --git a/Makefile b/Makefile index de294a9c7c..225aeec476 100755 --- a/Makefile +++ b/Makefile @@ -10,6 +10,7 @@ # ANNOTATE=true # label chatty output from coqc with file name ANNOTATE=silent # suppress chatty output from coqc # ANNOTATE=false # leave chatty output of coqc unchanged +# ANNOTATE=echo # like false, but in addition echo commands # DO NOT DISABLE coqc WARNINGS! That would hinder the Coq team's continuous integration. COQC=$(COQBIN)coqc @@ -31,104 +32,143 @@ endif # ##### Configure Compcert ##### -# Note: You can make a CONFIGURE file with definitions like +# Note: You can make a CONFIGURE file with the below definitions or give them +# on th emake command line # -# BITSIZE=64 (choose 64 bit compcert) -# ARCH=x86 (make sure compcert has architecture x86) +# # Choosing compcert # +# COMPCERT=platform (default, choose 32 or 64 bit platform supplied x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86) +# COMPCERT=bundled (build and use bundled 32 or 64 x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86) +# COMPCERT=nundled_new (build and use bundled compcert_new 32 or 64 x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86) +# COMPCERT=src_dir (build and use in source folder COMPCERT_SRC_DIR the variant specified by ARCH and BITSIZE) +# COMPCERT=inst_dir (use prebuilt CompCert in COMPCERT_INST_DIR - BITSIZE and ARCH can be left empty or must match) # -# COMPCERT=compcert (opam / coq-platform supplied compcert) -# COMPCERT=compcert64 (opam supplied 64 bit compcert) -# COMPCERT=mycompcert (private compcert installed in lib/coq/user-control) +# # Choosing BITSIZE # +# BITSIZE=32 +# BITSIZE=64 # -# COMPCERT_INST_PATH=/home/me/compcert -# (user local compcert inplace build) +# # Choosing ARCHITECTURE # +# ARCH=x86 +# ARCH=aarch64 +# ARCH=powerpc # -# COMPCERT_NEW (if defined enables compatibility options for -# new experimental compcert) +# # Choosing Flocq # +# FLOCQ_PLATFORM (default, except for COMPCERT_BUNDLED_NEW) +# FLOCQ_BUNDLED (require for COMPCERT_BUNDLED_NEW, valid for COMPCERT_BUNDLED, COMPCERT_SRC_DIR) # -# Note: BITSIZE can be used to choose a 64 bit compcert but ARCH cannot be used -# to select non x86, because there is no standard name mapping. You need to -# set COMPCERT or COMPCERT_INST_PATH to choose a different architecture. -# But both will be chacked if you set COMPCERT or COMPCERT_INST_PATH, so you -# can set COMPCERT, BITSIZE and ARCH to make sure COMPCERT is what you want. -# -# Note: By default, the rules for converting .c files to .v files -# are inactive. To activate them, do something like +# # Choosing Clightgen +# Note: By default, the rules for converting .c files to .v files are inactive. +# To activate them, define # CLIGHTGEN=$(my_local_bin_path)/clightgen +# # User settable variables # +COMPCERT ?= platform +ARCH ?= BITSIZE ?= -ARCH ?= - -ifndef COMPCERT_INST_PATH - PLATFORM_COMPCERT = true - ifndef COMPCERT - ifeq ($(BITSIZE),) - COMPCERT ?= compcert - else ifeq ($(BITSIZE),32) - COMPCERT ?= compcert - else ifeq ($(BITSIZE),64) - COMPCERT ?= compcert64 - else - $(error ILLEGAL BITSIZE $(BITSIZE)) - endif + +# # Internal variables # +# Set to true if the bundled CompCert is used +COMPCERT_NEW = false +# Relative path to bundled compcert for version comparison +COMPCERT_INFO_PATH_REF = compcert +# Set to true if the Coq module path for compcert needs to be set explicitly +COMPCERT_EXPLICIT_PATH = true +# Set to true if building from sources +COMPCERT_BUILD_FROM_SRC = false + +ifeq ($(COMPCERT),platform) + # Platform supplied CompCert + ifeq ($(BITSIZE),) + COMPCERT_INST_DIR = $(COQLIB)/user-contrib/compcert + COMPCERT_EXPLICIT_PATH = false + else ifeq ($(BITSIZE),32) + COMPCERT_INST_DIR = $(COQLIB)/user-contrib/compcert + COMPCERT_EXPLICIT_PATH = false + else ifeq ($(BITSIZE),64) + COMPCERT_INST_DIR = $(COQLIB)/../coq-variant/compcert64/compcert + else + $(error ILLEGAL BITSIZE $(BITSIZE)) + endif + COMPCERT_SRC_DIR = __NONE__ +else ifeq ($(COMPCERT),bundled) + # Bundled CompCert + COMPCERT_SRC_DIR = compcert + COMPCERT_INST_DIR = compcert + COMPCERT_BUILD_FROM_SRC = true +else ifeq ($(COMPCERT),bundled_new) + # Bundled CompCert (new variant) + COMPCERT_SRC_DIR = compcert_new + COMPCERT_INST_DIR = compcert_new + COMPCERT_NEW = true + COMPCERT_INFO_PATH_REF = compcert_new + COMPCERT_BUILD_FROM_SRC = true +else ifeq ($(COMPCERT),src_dir) + # Compile CompCert from source dir + ifeq ($(COMPCERT_SRC_DIR),) + $(error COMPCERT_SRC_DIR must not be empty if COMPCERT=src_dir) + endif + COMPCERT_INST_DIR = $(COMPCERT_SRC_DIR) + COMPCERT_BUILD_FROM_SRC = true +else ifeq ($(COMPCERT),inst_dir) + # Find CompCert in install dir + COMPCERT_SRC_DIR = __NONE__ + ifeq ($(COMPCERT_INST_DIR),) + $(error COMPCERT_INST_DIR must not be empty if COMPCERT=inst_dir) endif - COMPCERT_INST_PATH ?= $(COQLIB)/user-contrib/$(COMPCERT) - COMPCERT_CONFIG = $(COMPCERT_INST_PATH)/compcert.config -else - PLATFORM_COMPCERT = false - COMPCERT_CONFIG = endif - # Verify that the version of the supplied compcert matches the version of the internal compcert -CV1=$(shell cat compcert/VERSION) -CV2=$(shell cat $(COMPCERT_INST_PATH)/VERSION) +CV1=$(shell cat $(COMPCERT_INFO_PATH_REF)/VERSION) +CV2=$(shell cat $(COMPCERT_INST_DIR)/VERSION) -ifndef COMPCERT_NEW - ifneq ($(CV1), $(CV2)) - $(error COMPCERT VERSION MISMATCH: COMPCERT_VERSION=$(CV1) but $(COMPCERT_INST_PATH)/VERSION=$(CV2)) - endif +ifneq ($(CV1), $(CV2)) + $(error COMPCERT VERSION MISMATCH: COMPCERT_VERSION=$(CV1) but $(COMPCERT_INST_DIR)/VERSION=$(CV2)) endif # Verify that the version of the supplied clightgen matches the version of the internal compcert ifdef CLIGHTGEN VERSION1= $(lastword $(shell $(CLIGHTGEN) --version)) - VERSION2= $(subst version=,,$(shell grep version compcert/VERSION)) + VERSION2= $(subst version=,,$(shell grep version $(COMPCERT_INFO_PATH_REF)/VERSION)) ifneq ($(VERSION1),$(VERSION2)) - $(warning clightgen version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2)) + $(warning clightgen version $(VERSION1) does not match VST/$(COMPCERT_INFO_PATH_REF)/VERSION $(VERSION2)) endif endif # Verify that the supplied compcert folder is built (contains .vo files) -ifeq ($(PLATFORM_COMPCERT), true) - ifeq ($(wildcard $(COMPCERT_INST_PATH)/*/Clight.vo), ) - $(error FIRST BUILD COMPCERT, by: cd $(COMPCERT_INST_PATH); make clightgen) +ifeq ($(COMPCERT_BUILD_FROM_SRC),false) + ifeq ($(wildcard $(COMPCERT_INST_DIR)/*/Clight.vo), ) + $(error FIRST BUILD COMPCERT, by: cd $(COMPCERT_INST_DIR); make clightgen) endif endif # ##### Configure Architecture ##### -# Choose / test BITSIZE and ARCH +ifneq ($(COMPCERT_SRC_DIR),) + # We are building CompCert from source and can choose BITSIZE and ARCH -ifeq ($(PLATFORM_COMPCERT), true) + ifeq ($(BITSIZE),) + BITSIZE = 32 + endif + + ifeq ($(ARCH),) + ARCH = x86 + endif - # We are using a platform supplied CompCert +else + # We are using a pre-built CompCert, so verify that BITSIZE and ARCH match + # or extract them from the compcert settings if they are undefined - ifeq ($(wildcard $(COMPCERT_CONFIG)),) - $(error Cannot find compcert.config in $(COMPCERT_INST_PATH)) + ifeq ($(wildcard $(COMPCERT_INST_DIR)/compcert.config),) + $(error Cannot find compcert.config in $(COMPCERT_INST_DIR)) endif - COMPCERT_ARCH ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_ARCH"{print $$2}' $(COMPCERT_CONFIG)) - COMPCERT_BITSIZE ?= $(shell awk 'BEGIN{FS="="}$$1=="COMPCERT_BITSIZE"{print $$2}' $(COMPCERT_CONFIG)) - - # Verify that the bitsize and architecture match + include $(COMPCERT_INST_DIR)/compcert.config ifneq ($(BITSIZE),) ifneq ($(BITSIZE),$(COMPCERT_BITSIZE)) - $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_BITSIZE) but you requested $(BITSIZE)) + $(error The compcert found in $(COMPCERT_INST_DIR) has bitsize $(COMPCERT_BITSIZE) but you requested $(BITSIZE)) endif else BITSIZE = $(COMPCERT_BITSIZE) @@ -136,29 +176,16 @@ ifeq ($(PLATFORM_COMPCERT), true) ifneq ($(ARCH),) ifneq ($(ARCH),$(COMPCERT_ARCH)) - $(error The compcert found in $(COMPCERT_INST_PATH) has bitsize $(COMPCERT_ARCH) but you requested $(ARCH)) + $(error The compcert found in $(COMPCERT_INST_DIR) has bitsize $(COMPCERT_ARCH) but you requested $(ARCH)) endif else ARCH = $(COMPCERT_ARCH) endif - -else - - # We are using a self build CompCert - - ifeq ($(BITSIZE),) - BITSIZE = 32 - endif - - ifeq ($(ARCH),) - ARCH = x86 - endif - endif # Choose CompCert architecture folder -ifeq ($(wildcard $(COMPCERT_INST_PATH)/$(ARCH)_$(BITSIZE)),) +ifeq ($(wildcard $(COMPCERT_INST_DIR)/$(ARCH)_$(BITSIZE)),) ARCHDIRS=$(ARCH) else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) @@ -166,7 +193,7 @@ endif # Add CompCert backend folder for COMPCERT_NEW -ifdef COMPCERT_NEW +ifeq ($(COMPCERT_NEW),true) BACKEND=backend endif @@ -204,19 +231,19 @@ DIRS = $(VSTDIRS) $(OTHERDIRS) COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend exportclight $(BACKEND) $(FLOCQ) -ifeq ($(PLATFORM_COMPCERT),true) +ifeq ($(COMPCERT_EXPLICIT_PATH),true) + COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) + EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_DIR)/$(d) compcert.$(d)) +else COMPCERT_R_FLAGS= EXTFLAGS= -else - COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) - EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT_INST_PATH)/$(d) compcert.$(d)) endif # Compcert Clightgen flags CGFLAGS = -DCOMPCERT -#ifdef COMPCERT_NEW +#ifeq ($(COMPCERT_NEW),true) #SHIM= -Q concurrency/shim VST.veric #endif @@ -259,9 +286,18 @@ DEPFLAGS:=$(COQFLAGS) # ##### Print configuration summary ##### $(info ===== CONFIGURATION SUMMARY =====) +$(info COMPCERT=$(COMPCERT)) +$(info COMPCERT_SRC_DIR=$(COMPCERT_SRC_DIR)) +$(info COMPCERT_INST_DIR=$(COMPCERT_INST_DIR)) $(info BITSIZE=$(BITSIZE)) $(info ARCH=$(ARCH)) +$(info ===== DERIVED CONFIGURATION =====) +$(info COMPCERT_INFO_PATH_REF=$(COMPCERT_INFO_PATH_REF)) +$(info COMPCERT_EXPLICIT_PATH=$(COMPCERT_EXPLICIT_PATH)) +$(info COMPCERT_BUILD_FROM_SRC=$(COMPCERT_BUILD_FROM_SRC)) +$(info COMPCERT_NEW=$(COMPCERT_NEW)) $(info COQFLAGS=$(COQFLAGS)) +$(info COMPCERT_R_FLAGS=$(COMPCERT_R_FLAGS)) $(info =================================) # ########## File Lists ########## @@ -558,7 +594,7 @@ FILES = \ # ##### Derived file lists ##### -CC_TARGET= $(COMPCERT_INST_PATH)/cfrontend/Clight.vo +CC_TARGET= $(COMPCERT_INST_DIR)/cfrontend/Clight.vo CVFILES = $(patsubst %.c,$(PROGSDIR)/%.v,$(C_FILES)) CVOFILES = $(patsubst %.c,$(PROGSDIR)/%.vo,$(C_FILES)) @@ -579,7 +615,9 @@ PROGS64_FILES= $(V64_ORDINARY) # from progs/verif_reverse.v grep -v '^.[*][*][ )]' $*.v >$@ -%.vo: COQF=$(if $(findstring compcert, $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS)) +# This line sets COQF depending on the folder of the input file $< +# If the folder name contains compcert, $(COMPCERT_R_FLAGS) is added, otherwise not. +%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS)) # If CompCert changes, all .vo files need to be recompiled %.vo: $(COMPCERT_CONFIG) @@ -597,6 +635,8 @@ else ifeq ($(strip $(ANNOTATE)), true) @$(COQC) $(COQF) $*.v | awk '{printf "%s: %s\n", "'$*.v'", $$0}' else ifeq ($(strip $(ANNOTATE)), silent) @$(COQC) $(COQF) $*.v >/dev/null +else ifeq ($(strip $(ANNOTATE)), echo) + $(COQC) $(COQF) $*.v >/dev/null else @$(COQC) $(COQF) $*.v # @util/annotate $(COQC) $(COQF) $*.v @@ -689,7 +729,7 @@ floyd/floyd.coq: floyd/proofauto.vo .depend depend: @echo 'coqdep ... >.depend' -ifdef COMPCERT_NEW +ifeq ($(COMPCERT_NEW),true) # DEPENDENCIES VARIANT COMPCERT_NEW $(COQDEP) $(COQFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS) concurrency/common concurrency/compiler concurrency/juicy concurrency/util paco concurrency/sc_drf) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true @echo "" >>.depend @@ -697,9 +737,9 @@ else # DEPENDENCIES DEFAULT $(COQDEP) $(COQFLAGS) 2>&1 >.depend `find $(filter $(wildcard *), $(DIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true endif -ifeq ($(PLATFORM_COMPCERT),false) - # DEPENDENCIES LOCAL COMPCERT - $(COQDEP) $(COMPCERT_R_FLAGS) 2>&1 >>.depend `find $(addprefix $(COMPCERT_INST_PATH)/,$(COMPCERTDIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true +ifeq ($(COMPCERT_BUILD_FROM_SRC),true) + # DEPENDENCIES TO BUILD COMPCERT FROM SOURCE + $(COQDEP) $(COMPCERT_R_FLAGS) 2>&1 >>.depend `find $(addprefix $(COMPCERT_SRC_DIR)/,$(COMPCERTDIRS)) -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true endif # ifneq ($(wildcard coq-ext-lib/theories),) # $(COQDEP) -Q coq-ext-lib/theories ExtLib coq-ext-lib/theories >>.depend @@ -766,3 +806,4 @@ VSUpile: floyd/proofauto.vo floyd/VSU.vo floyd/VSU_addmain.vo # such problem, not sure exactly. -- Andrew) include .depend -include .depend-concur + diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam index 89023dfc61..4a72fb764f 100644 --- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam @@ -9,11 +9,10 @@ build: [ ["./configure" "amd64-linux" {os = "linux"} "amd64-macosx" {os = "macos"} "amd64-cygwin" {os = "cygwin"} - "-bindir" "%{bin}%" - "-libdir" "%{lib}%/compcert" + "-prefix" "%{prefix}%/variants/compcert64" "-install-coqdev" "-clightgen" - "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64" + "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert" "-ignore-coq-version"] [make "-j%{jobs}%" {ocaml:version >= "4.06"}] ] @@ -25,7 +24,19 @@ depends: [ "menhir" {>= "20190626" & < "20200123"} "ocaml" {>= "4.05.0"} ] -synopsis: "The CompCert C compiler" +synopsis: "The CompCert C compiler (64 bit)" +description: "This package installs the 64 bit version of CompCert. +For coexistence with the 32 bit version, the files are installed in: +%{prefix}%/variants/compcert64/bin (ccomp and clightgen binaries) +%{prefix}%/variants/compcert64/lib/compcert (C library) +%{lib}%/coq/user-contrib/compcert64 (Coq library) +Please note that the coq module path is compcert and not compcert64, +so the files cannot be directly Required as compcert64. +Instead -Q or -R options must be used to bind the compcert64 folder +to the module path compcert. This is more convenient if one development +uses both 32 and 64 bit versions. Otherwise all files would have to +be duplicated with module paths compcert and compcert64. +Please also note that the binary folder is usually not in the path." tags: [ "category:CS/Semantics and Compilation/Compilation" "category:CS/Semantics and Compilation/Semantics" diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam index 3f2b5c1d05..39e300c938 100644 --- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam @@ -10,11 +10,10 @@ build: [ ["./configure" "amd64-linux" {os = "linux"} "amd64-macosx" {os = "macos"} "amd64-cygwin" {os = "cygwin"} - "-bindir" "%{bin}%" - "-libdir" "%{lib}%/compcert" + "-prefix" "%{prefix}%/variants/compcert64" "-install-coqdev" "-clightgen" - "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64" + "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert" "-ignore-coq-version"] [make "-j%{jobs}%" {ocaml:version >= "4.06"}] ] @@ -42,7 +41,19 @@ depends: [ "menhir" {>= "20190626" & < "20200123"} "ocaml" {>= "4.05.0"} ] -synopsis: "The CompCert C compiler (using coq-platform supplied version of Flocq)" +synopsis: "The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)" +description: "This package installs the 64 bit version of CompCert. +For coexistence with the 32 bit version, the files are installed in: +%{prefix}%/variants/compcert64/bin (ccomp and clightgen binaries) +%{prefix}%/variants/compcert64/lib/compcert (C library) +%{lib}%/coq/user-contrib/compcert64 (Coq library) +Please note that the coq module path is compcert and not compcert64, +so the files cannot be directly Required as compcert64. +Instead -Q or -R options must be used to bind the compcert64 folder +to the module path compcert. This is more convenient if one development +uses both 32 and 64 bit versions. Otherwise all files would have to +be duplicated with module paths compcert and compcert64. +Please also note that the binary folder is usually not in the path." tags: [ "category:CS/Semantics and Compilation/Compilation" "category:CS/Semantics and Compilation/Semantics" diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam index 19e04fa9cc..ceca70c58c 100644 --- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam +++ b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam @@ -10,11 +10,10 @@ build: [ ["./configure" "amd64-linux" {os = "linux"} "amd64-macosx" {os = "macos"} "amd64-cygwin" {os = "cygwin"} - "-bindir" "%{bin}%" - "-libdir" "%{lib}%/compcert" + "-prefix" "%{prefix}%/variants/compcert64" "-install-coqdev" "-clightgen" - "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64" + "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert" "-ignore-coq-version"] [make "depend"] [make "-j%{jobs}%" {ocaml:version >= "4.06"} "proof_open_source"] @@ -45,7 +44,19 @@ depends: [ "menhir" {>= "20190626" & < "20200123"} "ocaml" {>= "4.05.0"} ] -synopsis: "The CompCert C compiler (only open source files + using coq-platform)" +synopsis: "The CompCert C compiler (64 bit, only open source files + using coq-platform)" +description: "This package installs the 64 bit version of CompCert. +For coexistence with the 32 bit version, the files are installed in: +%{prefix}%/variants/compcert64/bin (ccomp and clightgen binaries) +%{prefix}%/variants/compcert64/lib/compcert (C library) +%{lib}%/coq/user-contrib/compcert64 (Coq library) +Please note that the coq module path is compcert and not compcert64, +so the files cannot be directly Required as compcert64. +Instead -Q or -R options must be used to bind the compcert64 folder +to the module path compcert. This is more convenient if one development +uses both 32 and 64 bit versions. Otherwise all files would have to +be duplicated with module paths compcert and compcert64. +Please also note that the binary folder is usually not in the path." tags: [ "category:CS/Semantics and Compilation/Compilation" "category:CS/Semantics and Compilation/Semantics" From 956abae4581dcc1723ab471cd2e68afddcfc52f0 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 29 Jun 2020 09:33:12 +0200 Subject: [PATCH 5/6] Adjust build instructions to latest changes in Makefile --- BUILD_ORGANIZATION.md | 128 +++++++++++++++++++----------------------- 1 file changed, 58 insertions(+), 70 deletions(-) diff --git a/BUILD_ORGANIZATION.md b/BUILD_ORGANIZATION.md index 3eb2d44921..8fff030611 100644 --- a/BUILD_ORGANIZATION.md +++ b/BUILD_ORGANIZATION.md @@ -15,9 +15,7 @@ Otherwise please check: 2. Make sure you have the right version of CompCert. VST 2.6 uses CompCert 3.7 for Coq 8.11 -## Install Methods - -### Install via opam +## Install Method 1: use opam If you install VST via opam, opam will automatically install a suitable version of CompCert, Flocq and other dependencies. @@ -28,8 +26,15 @@ opam install coq-vst-64 ``` You can install both the 32 bit and the 64 bit versions of VST and CompCert in parallel. They will be installed in different folders. - -Please note that some opam supplied versions of CompCert use a version of +Please note that the 64 bit variants will be installed in non standard +locations and must be included explcitly with -Q or -R options: +``` +/lib/coq-variants/vst64/vst/ +/lib/coq-variants/compcert64/compcert/ +/variants/compcert64/bin/ +/variants/compcert64/lib/ +``` +Please also note that some opam supplied versions of CompCert use a version of Flocq distributed with CompCert. This is problematic if you want to verify numerical code which uses tools like CoqInterval or Gappa which also use Flocq. The proofs these tools do might then not be compatible with VST @@ -64,21 +69,23 @@ AND/OR opam install coq-compcert-64.3.7~platform-flocq~open-source coq-vst ``` -### Manual make with opam / coq-platform supplied CompCert +## Install Method 2: manual make with opam / coq-platform supplied CompCert For a manual make please follow this procedure: 1. Make sure CompCert and Flocq Coq `.vo` files are installed in ``` - /lib/coq/user-contrib/Flocq - /lib/coq/user-contrib/compcert + /lib/coq/user-contrib/Flocq + /lib/coq/user-contrib/compcert AND/OR - /lib/coq/user-contrib/compcert64 + /lib/coq-variants/compcert64/compcert ``` 2. Make sure CompCert clightgen is installed in ``` - /bin + /bin + AND/OR + /variants/compcert64/bin ``` 3. Execute this command: @@ -87,66 +94,47 @@ For a manual make please follow this procedure: OR make BITSIZE=64 ``` - (or, if you have a multicore computer, `make -j`) - -Please note that in this case you should *not* have a file `CONFIGURE` in -the VST root folder as you might for the next method. - -### Manual make with bundled CompCert - -VST includes two bundled variants of CompCert, which in some releases of -VST might include changes to support new features of VST. The bundled -variants are in the VST root folder under -``` -/compcert -/compcert_new -``` -Please note that by default VST uses a platform supplied CompCert and -not the bundled CompCert. In case you want to use one of the bundled -CompCert variants, please use these options: -``` -COMPCERT_INST_PATH=/compcert -``` -OR -``` -COMPCERT_INST_PATH=/compcert_new -COMPCERT_NEW -``` -The COMPCERT_NEW flag sets a few additional makefile options required to -build the variant in `/compcert_new` and must be set if this -folder is specified for `COMPCERT_INST_PATH`. - -You can set the additional options `BITSIZE` and `ARCH`. The supported -variants are: -``` -ARCH=x86 BITSIZE=32 (default) -ARCH=x86 BITSIZE=64 -ARCH=aarch64 BITSIZE=64 -ARCH=powerpc BITSIZE=32 -``` -Both variables can be set either on the make command line or in a file named -`CONFIGURE` in the VST source root folder which is read by the VST makefile. - -### Manual make with private build of CompCert and/or advanced options - -If you want to use a different CompCert than the default opam supplied -CompCert, you can configure the CompCert path by setting: -``` -COMPCERT=mycompcert -OR -COMPCERT_INST_PATH=/home/me/mycompcert -``` -`COMPCERT` names a Coq module path under `lib/coq/user-contrib`. -`COMPCERT_INST_PATH` names an arbitrary CompCert path, e.g. a local GIT build. - -Both variables can be set either on the make command line or in a file named -`CONFIGURE` in the VST source root folder which is read by the VST makefile. - -In addition you can define the variables `BITSIZE` and `ARCH`. If neither -`COMPCERT` nor `COMPCERT_INST_PATH` are set, `BITSIZE` can be used to -choose between `COMPCERT=compcert` and `COMPCERT=compcert64`. In any case -it is checked if `BITSIZE` and `ARCH` match the configurazion information -found in `compcert-config` in the specified CompCert folder. + (or, if you have a multicore computer, `make -j`). You may add the + target `floyd` to just build VSTs core without examples and tests. + +Please note that if you give options via teh make command line, you do +*not* have a file `CONFIGURE` in the VST root folder. + +## Install Method 3: advanced manual make, e.g. with bundled CompCert + +All options described in this section can be given in 3 ways: +- on the command line of make via `