From 5736832b383a4e882e82a4925b335dfc401e39c2 Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Wed, 8 Jan 2025 11:49:36 -0500 Subject: [PATCH] Update vst/lib to VST 2.15 and CompCert 3.15 (#804) --- InteractionTrees | 2 +- fcf | 2 +- lib/Makefile | 4 ++-- lib/proof/spec_threads.v | 2 +- lib/proof/src/math_extern.c | 3 --- lib/proof/verif_SC_atomics.v | 18 +++++++++--------- lib/proof/verif_locks.v | 6 +----- lib/proof/verif_math.v | 2 +- lib/test/testmath.c | 3 --- lib/test/verif_incr.v | 2 +- lib/test/verif_incr_main.v | 2 +- util/RELEASE | 10 ++++++++++ 12 files changed, 28 insertions(+), 28 deletions(-) diff --git a/InteractionTrees b/InteractionTrees index dda104937d..e7fed212b1 160000 --- a/InteractionTrees +++ b/InteractionTrees @@ -1 +1 @@ -Subproject commit dda104937d79e2052d1a26f6cbe89429245ff743 +Subproject commit e7fed212b1061b358428b57e11ee489184e241a2 diff --git a/fcf b/fcf index 291f50057c..d0f5432b90 160000 --- a/fcf +++ b/fcf @@ -1 +1 @@ -Subproject commit 291f50057cfbb7c96e58ff11ca9b9f4778467ec1 +Subproject commit d0f5432b902f452dcb2c85dc1981243dd4963977 diff --git a/lib/Makefile b/lib/Makefile index c086a315b7..c7fb0621dc 100644 --- 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 index e357138c40..1426542567 100644 --- 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 index 0a17ead099..3b12d5a13c 100644 --- 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 /* Note regard 'long double': diff --git a/lib/proof/verif_SC_atomics.v b/lib/proof/verif_SC_atomics.v index e9c0283add..66684c8a86 100644 --- a/lib/proof/verif_SC_atomics.v +++ b/lib/proof/verif_SC_atomics.v @@ -12,50 +12,50 @@ 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. @@ -63,7 +63,7 @@ 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 index 08121beec2..bfdc4dce53 100755 --- 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 index b82b6d8c60..22c3edbe78 100644 --- 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 index cb1ea957ca..a6ba824916 100644 --- 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 double f(double t) { diff --git a/lib/test/verif_incr.v b/lib/test/verif_incr.v index 6bd50382fd..b7feae0737 100644 --- 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 index f76ed8973f..781f1d4016 100644 --- 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 index b633aeb2bb..950951ea39 100644 --- 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