Adapt to the change in CompCert semantics between CompCert 3.7 and 3.8

.github/workflows/coq-action.yml

@@ -21,7 +21,6 @@ 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
-          - '9.0'
           - '9.1'
           - 'dev'
         bit_size:
@@ -54,9 +53,7 @@ jobs:
               opam install -y coq-flocq
               opam install -y ${{ matrix.coq_version == '9.0' && matrix.bit_size == 64 && 'coq-compcert.3.16' }} || exit_code=$?
               # Required by test2
-              opam install -y coq-ext-lib
-              # can simplify next line once the coq-paco opam package is available for rocq 9.1 
-              opam install -y ${{ matrix.coq_version != '9.1' && 'coq-paco' }} || exit_code=$?
+              opam install -y coq-ext-lib coq-itree
             endGroup
           # See https://github.com/coq-community/docker-coq-action/tree/v1#permissions
           before_script: |
@@ -91,7 +88,6 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '9.0'
           - '9.1'
           - 'dev' 
         make_target:
@@ -143,7 +139,7 @@ jobs:
           script: |
             startGroup "Build & Install"
               make -f util/make-touch  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
-              # put the first version back once CompCert 3.16 is in the Coq Platform
+              # use the first version only when coq-released has a version of CompCert compatible with this VST
               # 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

Makefile

@@ -304,9 +304,9 @@ CGFLAGS =  -DCOMPCERT -short-idents
 # ##### Interaction Trees Flags #####
 
 # as of 1 July 2025, coq-itree package seems not compatible with rocq 9.2+alpha, so still using submodule
-ifneq ($(wildcard InteractionTrees/theories),)
-EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
-endif
+# ifneq ($(wildcard InteractionTrees/theories),)
+# EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
+# endif
 
 # ##### FCF (Foundational Cryptography Framework) Flags #####
 

compcert/Makefile.config

@@ -7,7 +7,7 @@ SHAREDIR=$(PREFIX)/share
 COQDEVDIR=$(PREFIX)/lib/compcert/coq
 OCAML_NATIVE_COMP=true
 OCAML_OPT_COMP=true
-MENHIR_DIR=/Users/appel/.opam/coq9.1/lib/menhirLib
+MENHIR_DIR=/Users/appel/.opam/rocq9.1/lib/menhirLib
 COMPFLAGS=-bin-annot
 ABI=apple
 ARCH=aarch64
@@ -33,4 +33,4 @@ PIC_SUPPORTED=true
 SYSTEM=macos
 RESPONSEFILE=gnu
 LIBRARY_FLOCQ=external
-LIBRARY_MENHIRLIB=local
+LIBRARY_MENHIRLIB=external

compcert/README.md

@@ -2,9 +2,8 @@
 The formally-verified C compiler.
 
 ## Overview
-The CompCert C verified compiler is a compiler for a large subset of the
-C programming language that generates code for the PowerPC, ARM, x86 and
-RISC-V processors.
+The CompCert C verified compiler is a compiler for the core C language 
+that generates code for the ARM, PowerPC, RISC-V and x86 processors.
 
 The distinguishing feature of CompCert is that it has been formally
 verified using the Coq proof assistant: the generated assembly code is
@@ -21,7 +20,7 @@ CompCert is not free software.  This non-commercial release can only
 be used for evaluation, research, educational and personal purposes.
 A commercial version of CompCert, without this restriction and with
 professional support and extra features, can be purchased from
-[AbsInt](https://www.absint.com).  See the file `LICENSE` for more
+[AbsInt](https://www.absint.com).  See the file [LICENSE](LICENSE) for more
 information.
 
 ## Copyright

compcert/cfrontend/Ctypes.v

@@ -942,9 +942,9 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
   | Tint I16 _ _ => 2
   | Tint I32 _ _ => 4
   | Tint IBool _ _ => 1
-  | Tlong _ _ => 8
+  | Tlong _ _ => Archi.align_int64
   | Tfloat F32 _ => 4
-  | Tfloat F64 _ => 8
+  | Tfloat F64 _ => Archi.align_float64
   | Tpointer _ _ => if Archi.ptr64 then 8 else 4
   | Tarray t' _ _ => alignof_blockcopy env t'
   | Tfunction _ _ _ => 1
@@ -1005,15 +1005,30 @@ Proof.
     apply Z.divide_refl.
   }
   induction ty; simpl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_mul_l. auto.
-  apply Z.divide_refl.
-  destruct (env!i). apply X. apply Z.divide_0_r.
-  destruct (env!i). apply X. apply Z.divide_0_r.
+- auto with divide.
+- destruct i; auto with divide.
+- auto with divide.
+- destruct f; auto with divide.
+- auto with divide.
+- apply Z.divide_mul_l; auto.
+- auto with divide.
+- destruct (env!i). apply X. apply Z.divide_0_r.
+- destruct (env!i). apply X. apply Z.divide_0_r.
+Qed.
+
+Lemma alignof_alignof_blockcopy_compat:
+  forall env ty, naturally_aligned ty -> alignof_blockcopy env ty = Z.min 8 (alignof env ty).
+Proof.
+  induction ty; intros [A B]; unfold alignof, align_attr; rewrite A; simpl.
+- auto.
+- destruct i; auto.
+- auto.
+- destruct f; auto.
+- destruct Archi.ptr64; auto.
+- apply IHty; auto.
+- auto.
+- destruct (env!i); auto.
+- destruct (env!i); auto.
 Qed.
 
 (** Type ranks *)

compcert/common/Events.v

@@ -565,7 +565,7 @@ Inductive volatile_load (ge: Senv.t):
                       (Val.load_result chunk v)
   | volatile_load_nonvol: forall chunk m b ofs v,
       Senv.block_is_volatile ge b = false ->
-      Mem.load chunk m b (Ptrofs.unsigned ofs) = Some v ->
+      Mem.loadv chunk m (Vptr b ofs) = Some v ->
       volatile_load ge chunk m b ofs E0 v.
 
 Inductive volatile_store (ge: Senv.t):
@@ -579,7 +579,7 @@ Inductive volatile_store (ge: Senv.t):
                       m
   | volatile_store_nonvol: forall chunk m b ofs v m',
       Senv.block_is_volatile ge b = false ->
-      Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m' ->
+      Mem.storev chunk m (Vptr b ofs) v = Some m' ->
       volatile_store ge chunk m b ofs v E0 m'.
 
 (** * Semantics of external functions *)
@@ -733,7 +733,7 @@ Lemma volatile_load_extends:
 Proof.
   intros. inv H.
   econstructor; split; eauto. econstructor; eauto.
-  exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto.
 Qed.
 
 Lemma volatile_load_inject:
@@ -754,7 +754,7 @@ Proof.
   erewrite D; eauto.
   apply Val.load_result_inject. auto.
 - (* normal load *)
-  exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y).
+  exploit Mem.loadv_inject; eauto. intros (v2 & X & Y).
   exists v2; split; auto.
   constructor; auto.
   inv VI. erewrite D; eauto.
@@ -779,7 +779,7 @@ Proof.
   intros; constructor; intros.
 (* well typed *)
 - inv H. inv H0. apply Val.load_result_xtype.
-  eapply Mem.load_xtype; eauto.
+  eapply Mem.load_xtype; eauto with mem.
 (* symbols *)
 - inv H0. constructor. eapply volatile_load_preserved; eauto.
 (* valid blocks *)
@@ -856,8 +856,8 @@ Lemma volatile_store_readonly:
 Proof.
   intros. inv H.
 - apply Mem.unchanged_on_refl.
-- eapply Mem.store_unchanged_on; eauto.
-  exploit Mem.store_valid_access_3; eauto. intros [P Q].
+- eapply Mem.storev_unchanged_on; eauto.
+  exploit Mem.store_valid_access_3; eauto with mem. intros [P Q].
   intros. unfold loc_not_writable. red; intros. elim H2.
   apply Mem.perm_cur_max. apply P. auto.
 Qed.
@@ -876,14 +876,14 @@ Proof.
 - econstructor; split. econstructor; eauto.
   eapply eventval_match_lessdef; eauto. apply Val.load_result_lessdef; auto.
   auto with mem.
-- exploit Mem.store_within_extends; eauto. intros [m2' [A B]].
+- exploit Mem.storev_extends; eauto. intros [m2' [A B]].
   exists m2'; intuition auto with mem.
 + econstructor; eauto.
-+ eapply Mem.store_unchanged_on; eauto.
++ eapply Mem.storev_unchanged_on; eauto.
   unfold loc_out_of_bounds; intros.
   assert (Mem.perm m1 b i Max Nonempty).
   { apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
-    exploit Mem.store_valid_access_3. eexact H3. intros [P Q]. eauto. }
+    exploit Mem.store_valid_access_3. eapply Mem.storev_store. eexact H3. intros [P Q]. eauto. }
   tauto.
 Qed.
 
@@ -911,19 +911,18 @@ Proof.
   intuition auto with mem.
 - (* normal store *)
   inversion AI; subst.
-  assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto.
   exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
   exists m2'; intuition auto.
 + constructor; auto. erewrite S; eauto.
-+ eapply Mem.store_unchanged_on; eauto.
++ eapply Mem.storev_unchanged_on; eauto.
   unfold loc_unmapped; intros. inv AI; congruence.
-+ eapply Mem.store_unchanged_on; eauto.
-  unfold loc_out_of_reach; intros. red; intros. simpl in A.
-  assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta)) = Ptrofs.unsigned ofs + delta)
-  by (eapply Mem.address_inject; eauto with mem).
++ eapply Mem.storev_unchanged_on; eauto.
+  unfold loc_out_of_reach; intros. red; intros.
+  assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta)) = Ptrofs.unsigned ofs + delta).
+  { eapply Mem.address_inject' with (m1 := m1); eauto with mem. }
   rewrite EQ in *.
-  eelim H3; eauto.
-  exploit Mem.store_valid_access_3. eexact H0. intros [X Y].
+  eelim H2; eauto.
+  exploit Mem.store_valid_access_3. eapply Mem.storev_store. eexact H0. intros [X Y].
   apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
   apply X. lia.
 Qed.

compcert/common/Globalenvs.v

@@ -37,6 +37,7 @@
 From Coq Require Import Recdef Zwf.
 Require Import Axioms Coqlib Errors Maps AST Linking.
 Require Import Integers Floats Values Memory.
+Require Archi.
 
 Declare Scope pair_scope.
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
@@ -1460,9 +1461,9 @@ Definition init_data_alignment (i: init_data) : Z :=
   | Init_int8 n => 1
   | Init_int16 n => 2
   | Init_int32 n => 4
-  | Init_int64 n => 8
+  | Init_int64 n => Archi.align_int64
   | Init_float32 n => 4
-  | Init_float64 n => 4
+  | Init_float64 n => Archi.align_float64
   | Init_addrof symb ofs => if Archi.ptr64 then 8 else 4
   | Init_space n => 1
   end.
@@ -1491,7 +1492,7 @@ Proof.
   destruct i; simpl in H; eauto.
   simpl. apply Z.divide_1_l.
   destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption.
-  unfold Mptr, init_data_alignment; destruct Archi.ptr64; auto.
+  rewrite align_chunk_Mptr. reflexivity.
 Qed.
 
 Lemma store_init_data_list_aligned:
@@ -1579,8 +1580,8 @@ Proof.
   destruct i; eauto.
   simpl. exists m; auto.
   simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL.
-  unfold init_data_size, Mptr. destruct Archi.ptr64; auto.
-  unfold init_data_alignment, Mptr. destruct Archi.ptr64; auto.
+  rewrite size_chunk_Mptr; auto.
+  rewrite align_chunk_Mptr; auto.
 Qed.
 
 Lemma store_init_data_list_exists: