Merge pull request #781 from PrincetonUniversity/compcert3.15

Port VST 2.x to CompCert master
PrincetonUniversity · Jul 28, 2024 · 6c978e6 · 6c978e6
2 parents 0eed04f + 8c76515
commit 6c978e6
Show file tree

Hide file tree

Showing 228 changed files with 21,301 additions and 22,637 deletions.
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
@@ -21,7 +21,7 @@ jobs:
         # except for the "make_target" field and make_target related excludes
         coq_version:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
-          - '8.17'
+#          - '8.17'
           - '8.18'
           - '8.19'
           - 'dev'
@@ -31,8 +31,8 @@ jobs:
         make_target:
           - vst
         exclude:   
-          - coq_version: 8.17
-            bit_size: 32
+#         - coq_version: 8.17
+#            bit_size: 32
           - coq_version: 8.18
             bit_size: 32
           - coq_version: dev
@@ -64,7 +64,9 @@ jobs:
             endGroup
           script: |
             startGroup "Build & Install"
-              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
+              # put the first version back once CompCert 3.15 is in the Coq Platform
+              # make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
+              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=bundled IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
             endGroup
           after_script: |
             startGroup 'Copy Opam coq/user-contrib and coq-variant'
@@ -89,7 +91,7 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.17'
+#          - '8.17'
           - '8.18'
           - '8.19'
           - 'dev' 
@@ -104,8 +106,8 @@ jobs:
           - 32
           - 64
         exclude:
-          - coq_version: 8.17
-            bit_size: 32
+#          - coq_version: 8.17
+#            bit_size: 32
           - coq_version: 8.18
             bit_size: 32
           - coq_version: dev
@@ -114,7 +116,7 @@ jobs:
             make_target: test3
           - bit_size: 32
             make_target: test4
-          - bit_size: 64
+          - bit_size: 32
             make_target: test5
 
     steps:
@@ -141,6 +143,8 @@ jobs:
           script: |
             startGroup "Build & Install"
               make -f util/make-touch  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
-              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }}  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
+              # put the first version back once CompCert 3.15 is in the Coq Platform
+              # make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }}  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
+              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=bundled IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
             endGroup
           uninstall:
diff --git a/Makefile b/Makefile
@@ -762,19 +762,19 @@ vst: _CoqProject msl veric floyd simpleconc
 
 ifeq ($(BITSIZE),64)
 test: vst progs64
-	@# need this tab here to turn of special behavior of 'test' target
+	@# need this tab here to turn off special behavior of 'test' target
 test2: io
 test4: mailbox 
-test6: VSUpile64
-tests: test test2 test4 test6
+test5: VSUpile64
+tests: test test2 test4 test5
 all: tests
 else
 test: vst progs
-	@# need this tab here to turn of special behavior of 'test' target
+	@# need this tab here to turn off special behavior of 'test' target
 test2: io
 test3: sha hmac 
 test5: VSUpile
-tests: test test2 test3 test5 test6
+tests: test test2 test3 test5
 all: vst files tests hmacdrbg tweetnacl aes
 endif
 
@@ -860,13 +860,13 @@ ifdef CLIGHTGEN
 all-cv-files: $(patsubst %.c,$(PROGSDIR)/%.v, $(SINGLE_C_FILES) even.c odd.c) \
               $(patsubst %.c,%.v, $(SHA_C_FILES)) \
               aes/aes.v tweetnacl20140427/tweetnaclVerifiableC.v \
-              mailbox/mailbox.v concurrency/threads.v atomics/SC_atomics.v
+              mailbox/mailbox.v atomics/SC_atomics.v # concurrency/threads.v 
 ifneq (, $(findstring -short-idents, $(CGFLAGS)))
 $(patsubst %.c,%.v, $(SHA_C_FILES)) &: $(SHA_C_FILES)
 	$(CLIGHTGEN) ${CGFLAGS} $^
 $(PROGSDIR)/odd.v: $(PROGSDIR)/even.v
 mailbox/mailbox.v: mailbox/atomic_exchange.c mailbox/mailbox.c
-	$(CLIGHTGEN) ${CGFLAGS} $^
+	$(CLIGHTGEN) -DCOMPCERT -normalize -canonical-idents $^
 else
 ifeq (, $(findstring -canonical-idents, $(CGFLAGS)))
   $(warning CGFLAGS contains neither -short-idents nor -canonical-idents, using default which is probably -canonical-idents)

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-2.13
+2.15