Update vst/lib to VST 2.15 and CompCert 3.15 (#804)

andrew-appel · web-flow · commit 5736832b383a · 2025-01-08T11:49:36.000-05:00
diff --git a/InteractionTrees b/InteractionTrees
@@ -1 +1 @@
-Subproject commit dda104937d79e2052d1a26f6cbe89429245ff743
+Subproject commit e7fed212b1061b358428b57e11ee489184e241a2
diff --git a/fcf b/fcf
@@ -1 +1 @@
-Subproject commit 291f50057cfbb7c96e58ff11ca9b9f4778467ec1
+Subproject commit d0f5432b902f452dcb2c85dc1981243dd4963977
diff --git a/lib/Makefile b/lib/Makefile
@@ -23,14 +23,14 @@ endif
 ##                      Your targets here                         ##
 ####################################################################
 
-run-clightgen: proof/math_extern.v proof/malloc_extern.v proof/SC_atomics_extern.v
+run-clightgen: proof/math_extern.v proof/malloc_extern.v proof/SC_atomics_extern.v proof/threads.v
 
 include CoqMakefile.local
 
 clean:
 	rm -f CoqMakefile CoqMakefile.conf
 	rm -f proof/{*.vo,*.vos,*.vok,*.glob} 
-	rm -f proof/{math_extern.v,malloc_extern.v,SC_atomics_extern.v}
+	rm -f proof/{math_extern.v,malloc_extern.v,SC_atomics_extern.v,threads.v}
 	rm -f test/{*.vo,*.vos,*.vok,*.glob} 
 	rm -f test/{incr.v,incr_main.v,testmath.v}
 
diff --git a/lib/proof/spec_threads.v b/lib/proof/spec_threads.v
@@ -115,7 +115,7 @@ Proof.
   destruct x as [[[]] pre]; auto.
 Qed.
 
-Definition spawned_funtype := Tfunction (Tcons (tptr tvoid) Tnil) tint cc_default.
+Definition spawned_funtype := Tfunction (tptr tvoid :: nil) tint cc_default.
 
 Definition spawn_spec := mk_funspec
   ((tptr spawned_funtype) :: (tptr tvoid) :: nil, tvoid)
diff --git a/lib/proof/src/math_extern.c b/lib/proof/src/math_extern.c
@@ -1,6 +1,3 @@
-#ifdef COMPCERT
-typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
-#endif
 #include <math.h>
 
 /* Note regard 'long double':
diff --git a/lib/proof/verif_SC_atomics.v b/lib/proof/verif_SC_atomics.v
@@ -12,58 +12,58 @@ Definition Vprog : varspecs. mk_varspecs prog. Defined.
 Parameter body_make_atomic: 
  forall {Espec: OracleKind} ,
    VST.floyd.library.body_lemma_of_funspec 
-        (EF_external "make_atomic" (mksignature (AST.Tint :: nil) AST.Tlong cc_default))
+        (EF_external "make_atomic" (mksignature (Xint :: nil) Xptr cc_default))
        make_atomic_spec. 
 
 Parameter body_make_atomic_ptr:
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
        (EF_external "make_atomic_ptr"
-                   (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
+                   (mksignature (Xptr :: nil) Xptr cc_default))
        make_atomic_ptr_spec.
 
 Parameter body_free_atomic: 
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
         (EF_external "free_atomic"
-                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
+                   (mksignature (Xptr :: nil) Xvoid cc_default))
        free_atomic_int_spec.
 
 Parameter body_free_atomic_ptr: 
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
         (EF_external "free_atomic_ptr"
-                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
+                   (mksignature (Xptr :: nil) Xvoid cc_default))
        free_atomic_ptr_spec.
 
 Parameter body_atom_load: 
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
         (EF_external "atom_load"
-                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+                   (mksignature (Xptr :: nil) Xint cc_default))
        atomic_load_spec.
 
 Parameter body_atom_store: 
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
         (EF_external "atom_store"
-                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid cc_default))
+                   (mksignature (Xptr :: Xint :: nil) Xvoid cc_default))
        atomic_store_spec.
 
 Parameter body_atom_CAS: 
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
         (EF_external "atom_CAS"
-                   (mksignature (AST.Tlong :: AST.Tlong :: AST.Tint :: nil)
-                     AST.Tint cc_default))
+                   (mksignature (Xptr :: Xptr :: Xint :: nil)
+                     Xint cc_default))
        atomic_CAS_spec.
 
 
 Parameter body_atom_exchange: 
  forall {Espec: OracleKind}  ,
    VST.floyd.library.body_lemma_of_funspec 
         (EF_external "atom_exchange"
-                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tint
+                   (mksignature (Xptr :: Xint :: nil) Xint
                      cc_default))
        atomic_exchange_spec.
 
diff --git a/lib/proof/verif_locks.v b/lib/proof/verif_locks.v
@@ -210,11 +210,7 @@ Opaque inv_for_lock.
     - Intros r. if_tac; forward_if; try discriminate; try contradiction.
       + forward. simpl spec_locks.lock_inv; entailer!.
       + forward. simpl spec_locks.lock_inv; entailer!.
-Unshelve.
-apply Build_change_composite_env with (coeq := Maps.PTree.empty bool).
-intros. inv H1. intros. unfold cenv_cs; simpl. rewrite !Maps.PTree.gempty.
-split; intros [? ?]; discriminate.
-  Qed.
+Qed.
 
 #[global] Opaque M.
 
diff --git a/lib/proof/verif_math.v b/lib/proof/verif_math.v
@@ -63,7 +63,7 @@ assert (match ret with
        | None => False
        end); [ | destruct t; try contradiction; auto].
 assert (match rettype_of_type t with
-               | AST.Tvoid =>
+               | Xvoid =>
                    mkEnviron gx (Map.empty (block * type))
                      (Map.empty val)
                | _ =>
diff --git a/lib/test/testmath.c b/lib/test/testmath.c
@@ -1,6 +1,3 @@
-#ifdef COMPCERT
-typedef float _Float16;  /* _Float16 is a MacOS thing that CompCert doesn't support */
-#endif
 #include <math.h>
 
 double f(double t) {
diff --git a/lib/test/verif_incr.v b/lib/test/verif_incr.v
@@ -80,7 +80,7 @@ Definition SpawnASI_without_exit :=
 
 Definition incrImports := LockASI ++ SpawnASI_without_exit.
 Definition incrInternals := [incr_spec; read_spec; thread_func_spec; compute2_spec].
-Definition Gprog : funspecs :=   incrInternals ++ incrImports.
+Definition Gprog : funspecs :=   incrImports ++ incrInternals.
 
 Lemma ctr_inv_exclusive : forall g1 g2 p,
   exclusive_mpred (cptr_lock_inv g1 g2 p).
diff --git a/lib/test/verif_incr_main.v b/lib/test/verif_incr_main.v
@@ -47,7 +47,7 @@ Definition main_spec :=
   PRE  [] main_pre whole_prog tt gv
   POST [ tint ] PROP() RETURN (Vint (Int.repr 2)) SEP (TT).
 
-Definition Gprog :=  [main_spec] ++ Main_imports.
+Definition Gprog :=  Main_imports ++ [main_spec].
 
 Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
 Proof.
diff --git a/util/RELEASE b/util/RELEASE
@@ -1,3 +1,13 @@
+How to generate a release:
+
+1. cd .../vst; git tag -a vX.Y -m "VST release X.Y"; git push origin vX.Y
+2. In a fork of the opam-coq-archive,
+      https://github.com/coq/opam
+   within directory released/packages/coq-vst
+
+
+
+---------THE FOLLOWING INSTRUCTIONS ARE OBSOLETE, from before opam--------
 ***** reminder about how to generate a release
 
 1. in some other directory, run .../vst/util/PACKAGE
