Fixed some coq-8.18 deprecation warnings; speed up forward_call by apply change_compspecs parsimoniously

.github/workflows/coq-action.yml

@@ -23,6 +23,7 @@ jobs:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
           - '8.16'
           - '8.17'
+          - '8.18'
           - 'dev'
         bit_size:
           - 32
@@ -32,6 +33,8 @@ jobs:
         exclude:   
           - coq_version: 8.16
             bit_size: 32
+          - coq_version: 8.17
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
     steps:
@@ -50,7 +53,7 @@ jobs:
             endGroup
           install: |
             startGroup "Install dependencies"
-              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.12' || 'coq-compcert.3.12' }}
+              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13' || 'coq-compcert.3.13' }}
               # Required by test2
               opam install -y coq-ext-lib
             endGroup
@@ -61,7 +64,7 @@ jobs:
             endGroup
           script: |
             startGroup "Build & Install"
-              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true
+              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
             endGroup
           after_script: |
             startGroup 'Copy Opam coq/user-contrib and coq-variant'
@@ -88,6 +91,7 @@ jobs:
         coq_version:
           - '8.16'
           - '8.17'
+          - '8.18'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -102,6 +106,8 @@ jobs:
         exclude:
           - coq_version: 8.16
             bit_size: 32
+          - coq_version: 8.17
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
           - bit_size: 64
@@ -134,7 +140,7 @@ jobs:
             endGroup
           script: |
             startGroup "Build & Install"
-              make -f util/make-touch  IGNORECOQVERSION=true
-              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }}  IGNORECOQVERSION=true
+              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
             endGroup
           uninstall:

CHANGES

@@ -1,4 +1,4 @@
-CHANGES IN NEXT RELEASE (after 2.12)
+CHANGES IN RELEASE 2.13 (October 2023)
 
 - Improved error diagnostics when compspecs mismatch
 - Improved error diagnostics when change_compspecs fails
@@ -7,6 +7,10 @@ CHANGES IN NEXT RELEASE (after 2.12)
 - forward tactic is slightly more careful about not simplifying user's terms
 - bug fixes and improved diagnostic messages in list_solve tactic
 - field_compatible0_Tarray_offset no longer requires naturally_aligned hypothesis
+- 'forward' now interacts better with 'localize/unlocalize' (#773)
+- Performance improvements in VSU system (#716)
+- VSU permits sharing of globals between compilation units (#713)
+- Compatible with Coq 8.18.0, 8.17.1, 8.16.1; with CompCert 3.13.1, 3.12, 3.11.
 
 CHANGES IN RELEASE 2.12 (March 2023)
 

Makefile

@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1
+COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1 or-else 8.18.0
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)

VERSION

@@ -1 +1 @@
-2.12
+2.13

atomics/verif_atomics.v

@@ -678,7 +678,7 @@ Lemma full_hist'_drop : forall h h' v (Hh : full_hist' h v)
   full_hist' h' v.
 Proof.
   intros ??? (l & Hl & Hv) ?.
-  revert dependent h'; revert dependent v; revert dependent h; induction l using rev_ind; intros.
+  generalize dependent h'; generalize dependent v; generalize dependent h; induction l using rev_ind; intros.
   - inv Hl; simpl in *.
     destruct h'.
     exists []; auto.
@@ -748,7 +748,7 @@ Corollary full_hist_nil' : forall n l (Hfull : Forall2 full_hist' (repeat [] n)
   (Hrep : Forall repable_signed l), l = repeat 0 n.
 Proof.
   intros; apply full_hist'_nil in Hfull.
-  revert dependent l; induction n; destruct l; auto; try discriminate; simpl; intros.
+  generalize dependent l; induction n; destruct l; auto; try discriminate; simpl; intros.
   inv Hrep; f_equal; [|apply IHn; inv Hfull; auto].
   apply repr_inj_signed; auto; congruence.
 Qed.

atomics/verif_hashtable1.v

@@ -1413,7 +1413,7 @@ Proof.
   rewrite Zlength_correct in H.
   assert (length h = Z.to_nat size) as Hlen by Omega0.
   forget (Z.to_nat size) as n; clear H.
-  revert dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
+  generalize dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
   destruct p; rewrite IHn; auto.
 Qed.
 
@@ -1502,7 +1502,7 @@ Proof.
   rewrite Zlength_correct in H.
   assert (length h = Z.to_nat size) as Hlen by Omega0.
   forget (Z.to_nat size) as n; clear H.
-  revert dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
+  generalize dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
   destruct p; rewrite IHn, !app_nil_r; auto.
 Qed.
 
@@ -1950,7 +1950,7 @@ Lemma one_CAS_succeeds : forall h v a t1 t2 b1 b2 (Hl : full_hist' h v) (Hin1 :
 Proof.
   intros.
   destruct Hl as (l & Hl & Hv).
-  revert dependent v; induction Hl; [contradiction|].
+  generalize dependent v; induction Hl; [contradiction|].
   subst; intros; rewrite !in_app in *; simpl in *.
   rewrite Forall_app in Ha; destruct Ha as (? & Ha); inv Ha.
   rewrite apply_hist_app in Hv.

atomics/verif_ptr_atomics.v

@@ -839,7 +839,7 @@ Lemma full_hist'_drop : forall h h' v (Hh : full_hist' h v)
   full_hist' h' v.
 Proof.
   intros ??? (l & Hl & Hv) ?.
-  revert dependent h'; revert dependent v; revert dependent h; induction l using rev_ind; intros.
+  generalize dependent h'; generalize dependent v; generalize dependent h; induction l using rev_ind; intros.
   - inv Hl; simpl in *.
     destruct h'.
     exists []; auto.

compcert/Makefile.config

@@ -6,7 +6,7 @@ SHAREDIR=$(PREFIX)/share
 COQDEVDIR=$(PREFIX)/lib/compcert/coq
 OCAML_NATIVE_COMP=true
 OCAML_OPT_COMP=true
-MENHIR_DIR=/usr/local/lib/menhirLib
+MENHIR_DIR=/Users/appel/.opam/CP.2023.03.0~8.18+beta1/lib/menhirLib
 COMPFLAGS=-bin-annot
 ABI=standard
 ARCH=x86
@@ -20,15 +20,15 @@ CLIGHTGEN=true
 CLINKER=gcc
 CLINKER_OPTIONS=-m64 -no-pie
 CPREPRO=gcc
-CPREPRO_OPTIONS=-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E
+CPREPRO_OPTIONS=-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E
 ARCHIVER=ar rcs
 ENDIANNESS=little
 HAS_RUNTIME_LIB=true
 HAS_STANDARD_HEADERS=true
 INSTALL_COQDEV=true
 LIBMATH=-lm
 MODEL=64
-SYSTEM=cygwin
+SYSTEM=linux
 RESPONSEFILE=gnu
-LIBRARY_FLOCQ=external
+LIBRARY_FLOCQ=local
 LIBRARY_MENHIRLIB=local

compcert/VERSION

@@ -1,4 +1,4 @@
-version=3.12
+version=3.13
 buildnr=
 tag=
 branch=

compcert/cfrontend/Cstrategy.v

@@ -1653,8 +1653,8 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Pro
   | _, _ => False
   end.
 
-(** [eval_expression ge e m1 a t m2 a'] describes the evaluation of the
-  complex expression e.  [v] is the resulting value, [m2] the final
+(** [eval_expression ge e m1 a t m2 v] describes the evaluation of the
+  complex expression [a].  [v] is the resulting value, [m2] the final
   memory state, and [t] the trace of input/output events performed
   during this evaluation.  *)
 

concurrency/ghosts.v

@@ -1548,7 +1548,7 @@ Lemma hist_list'_add : forall h1 h2 (l : list hist_el) (Hdisj : disjoint h1 h2),
 Proof.
   intros.
   remember (map_add h1 h2) as h.
-  revert dependent h2; revert h1; induction H; intros.
+  generalize dependent h2; revert h1; induction H; intros.
   - exists [], []; split; [reflexivity|].
     assert (h1 = empty_map /\ h2 = empty_map) as [].
     { split; extensionality k; apply equal_f with (x := k) in Heqh; unfold map_add in Heqh;

floyd/SeparationLogicAsLogic.v

@@ -109,7 +109,7 @@ with labeled_statements_ind (L: labeled_statements): all_suf_of_labeled_statemen
 End statement_ind.
 
 Ltac induction_stmt s :=
-  revert dependent s;
+  generalize dependent s;
   let s1 := fresh s "1" in
   let s2 := fresh s "2" in
   let IHs := fresh "IH" s in

floyd/VSU.v

@@ -2190,7 +2190,7 @@ eapply Comp_Exports_sub2;
 - symmetry in NOimports |- *.
    unfold JoinedImports in *.
    change (filter _ nil) with (@nil (ident*funspec)) in *.
-   rewrite <- app_nil_end in *.
+   rewrite app_nil_r in *.
    match goal with |- filter ?A (filter ?B ?C) = _ => forget A as F; forget B as G; forget C as al end.
    clear - NOimports.
    induction al as [|[i?]]; auto.
@@ -3051,7 +3051,7 @@ assert (H20: forall i fd, In (i,fd) (prog_funct' (map of_builtin (QP.prog_builti
 }
 
 assert (VG_LNR: list_norepet (map fst (QPvarspecs p) ++ map fst  G)). {
-  pose proof (Comp_LNR c). rewrite <- app_nil_end in H4.
+  pose proof (Comp_LNR c). rewrite app_nil_r in H4.
   auto.
 }
 forget (filter isGfun (PTree.elements (QP.prog_defs p))) as fs.

floyd/canon.v

@@ -37,7 +37,14 @@ Fixpoint fold_right_andp rho (l: list (environ -> Prop)) : Prop :=
  end.
 
 Declare Scope assert.  Delimit Scope assert with assert.
+Global Set Warnings "-overwriting-delimiting-key".
 Delimit Scope assert with argsassert.
+(* Ideally we would like to disable this warning only for this Delimit command,
+ and then do 
+   Set Warnings "+overwriting-delimiting-key".
+  afterward, but this doesn't really work, because we'd still
+ get the warning in every file that imports this file.
+*)
 Declare Scope assert3. Delimit Scope assert3 with assert3.
 Declare Scope assert4. Delimit Scope assert4 with assert4.
 Declare Scope assert5. Delimit Scope assert5 with assert5.
@@ -311,7 +318,7 @@ Proof.
   specialize (H0 n ts x rho).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as Q1 end.
-  revert dependent Q1; induction (Q ts x); intros; inv H0; destruct Q1; try discriminate.
+  generalize dependent Q1; induction (Q ts x); intros; inv H0; destruct Q1; try discriminate.
   + auto.
   + inv H3.
     simpl.
@@ -355,7 +362,7 @@ Proof.
   specialize (H0 n ts x rho).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as P1 end.
-  revert dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
+  generalize dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
   + auto.
   + inv H3.
     simpl.
@@ -1085,7 +1092,7 @@ Ltac frame_SEP' L :=  (* this should be generalized to permit framing on LOCAL p
  match goal with
  | |- @semax _ _ _ (PROPx _ (LOCALx ?Q (SEPx ?R))) _ _ =>
   rewrite <- (Floyd_firstn_skipn (length L) R);
-  rewrite (app_nil_end Q);
+  rewrite (app_nil_r Q);
     simpl length; unfold Floyd_firstn, Floyd_skipn;
     eapply (semax_frame_PQR);
       [ unfold closed_wrt_modvars;  auto 50 with closed
@@ -1494,7 +1501,7 @@ inv H.
 specialize (IHn _ H). clear H.
 simpl Floyd_firstn.
 change (m :: Floyd_firstn n R) with (app (m::nil) (Floyd_firstn n R)).
-rewrite app_ass. unfold app at 1.
+rewrite <- app_assoc. unfold app at 1.
 simpl.
 f_equal.
 auto.
@@ -2710,7 +2717,7 @@ Proof.
   specialize (H0 n ts x (Clight_seplog.mkEnv (fst gargs) nil nil)).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as Q1 end.
-  revert dependent Q1; induction (G ts x); intros; inv H0; destruct Q1; try discriminate.
+  generalize dependent Q1; induction (G ts x); intros; inv H0; destruct Q1; try discriminate.
   + auto.
   + inv H3.
     simpl.
@@ -2756,7 +2763,7 @@ Proof.
   specialize (H0 n ts x any_environ).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as P1 end.
-  revert dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
+  generalize dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
   + auto.
   + inv H3.
     simpl.

floyd/field_at.v

@@ -2758,7 +2758,7 @@ Proof.
   setoid_rewrite aggregate_pred.rangespec_ext at 4; [|intros; rewrite Z.sub_0_r; apply f_equal; auto].
   clear H3 H4.
   rewrite Z2Nat_max0 in *.
-  forget (offset_val 0 p) as p'; forget (Z.to_nat z) as n; forget 0 as lo; revert dependent lo; induction n; auto; simpl; intros.
+  forget (offset_val 0 p) as p'; forget (Z.to_nat z) as n; forget 0 as lo; generalize dependent lo; induction n; auto; simpl; intros.
  apply derives_refl.
   match goal with |- (?P1 * ?Q1) * (?P2 * ?Q2) |-- _ =>
     eapply derives_trans with (Q := (P1 * P2) * (Q1 * Q2)); [cancel|] end.
@@ -2825,8 +2825,7 @@ Qed.
 #[export] Hint Rewrite
   @field_at_data_at_cancel'
   @field_at_data_at
-  @field_at__data_at_
-  @data_at__data_at : cancel.
+  @field_at__data_at_ : cancel.
 
 (* END new experiments *)
 

floyd/forward.v

@@ -1173,19 +1173,40 @@ Ltac simplify_remove_localdef_temp :=
     change u with u'
   end.
 
+Ltac afc_error1 :=
+  fail 100 "Error: should not hit this case in after_forward_call.  To ignore this error and try anyway, do 'Ltac afc_error1 ::= idtac'".
+
 Ltac after_forward_call :=
     check_POSTCONDITION; 
     try match goal with |- context [remove_localdef_temp] =>
               simplify_remove_localdef_temp
      end;
-    unfold_app; 
     try (apply extract_exists_pre; intros _); 
     match goal with
         | |- semax _ _ _ _ => idtac
         | |- unit -> semax _ _ _ _ => intros _
     end;
     match goal with
-        | |- @semax ?CS _ _ _ _ _ => try change_compspecs CS
+        | |- @semax ?CS ?Espec ?Delta (exp ?F) ?c ?Post =>
+               lazymatch F with context [@app mpred _ ?x] =>
+                  let hide := fresh "hide" in set (hide := x);
+                  try change_compspecs CS;
+                  subst hide
+               end;
+               unfold_app
+        | |- @semax ?CS ?Espec ?Delta (PROPx (?P1 ++ ?P2) (LOCALx ?Q (SEPx (?A ++ ?B)))) ?c ?Post =>
+               let hide := fresh "hide" in
+               pose (hide x := @semax CS Espec Delta (PROPx (P1 ++ P2) 
+                                     (LOCALx Q (SEPx (x ++ B)))) c Post);
+               change (hide A);
+               try change_compspecs CS;
+               subst hide; 
+               cbv beta;
+               unfold_app
+        | |- @semax ?CS _ _ _ _ _ => 
+               afc_error1;
+               unfold_app;
+               try change_compspecs CS
     end;
     repeat (apply semax_extract_PROP; intro); 
     cleanup_no_post_exists; 
@@ -1346,7 +1367,10 @@ Ltac prove_call_setup_aux  ts witness :=
  | check_vl_eq_args
  | auto 50 with derives
  | check_gvars_spec
- | try change_compspecs CS; cancel_for_forward_call
+ | let lhs := fresh "lhs" in 
+   match goal with |- ?A |-- ?B => pose (lhs := A); change (lhs |-- B) end;
+   try change_compspecs CS; subst lhs;
+   cancel_for_forward_call
  |
  ])
   in strip1_later R' cR

floyd/freezer.v

@@ -576,7 +576,7 @@ induction n; destruct R; intros.
 + inv H.
   specialize (IHn _ H1). clear H1. simpl Floyd_firstn.
   change (m :: Floyd_firstn n R) with (app (m::nil) (Floyd_firstn n R)).
-  rewrite app_ass. unfold app at 1.
+  rewrite <- app_assoc. unfold app at 1.
   simpl; f_equal; auto.
 Qed.
 

floyd/globals_lemmas.v

@@ -111,7 +111,7 @@ Proof. induction xs; intros; simpl.
    apply sepcon_derives.
    + rewrite (data_at_singleton_array_eq Ews tint (Vint a)) by trivial.
      erewrite mapsto_data_at'; auto; trivial.
-     red; simpl; intuition.
+     red; simpl; intuition auto with *.
      econstructor. reflexivity. simpl; trivial.
    + eapply derives_trans. apply IHxs; clear IHxs.
      * rewrite ! Ptrofs.unsigned_repr; try rep_lia.
@@ -121,7 +121,7 @@ Proof. induction xs; intros; simpl.
        replace (Z.succ (Zlength xs) - 1) with (Zlength xs) by lia.
        apply derives_refl'. f_equal. list_solve.
        unfold field_address0. rewrite if_true; simpl; trivial.
-       red; intuition.
+       red; intuition auto with *.
        -- reflexivity.
        -- red. rewrite sizeof_Tarray, Z.max_r. simpl sizeof; rep_lia. list_solve.
        -- eapply align_compatible_rec_Tarray; intros.