From 1242bfaf4ef0dda183d0e11a45cb7a86baaea413 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 6 Jul 2022 18:20:52 +0200
Subject: [PATCH] [dune] cleaning wp-cache instructions
---
bin/test.sh | 24 +++--
src/plugins/wp/Makefile.in | 63 -----------
src/plugins/wp/tests/README.md | 185 ++++++++++-----------------------
3 files changed, 71 insertions(+), 201 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 9acea71ddac..24b8d54c77c 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -68,11 +68,15 @@ function Usage
echo ""
echo "VARIABLES"
echo ""
- echo " FRAMAC_WP_CACHE ($FRAMAC_WP_CACHE)"
- echo " Management mode of wp-cache"
+ echo " FRAMAC_WP_CACHE"
+ echo " Management mode of wp-cache ($FRAMAC_WP_CACHE)"
echo ""
- echo " FRAMAC_WP_CACHEDIR ($FRAMAC_WP_CACHEDIR)"
- echo " Use $FRAMAC_WP_CACHE_GIT"
+ echo " FRAMAC_WP_QUALIF"
+ echo " FRAMAC_WP_CACHEDIR"
+ echo " Location of wp-cache ($FRAMAC_WP_CACHEDIR)"
+ if [ ! -d $FRAMAC_WP_CACHEDIR ]; then
+ echo " About to clone from $FRAMAC_WP_CACHE_GIT"
+ fi
echo " Please, always push to master branch"
echo ""
}
@@ -126,12 +130,14 @@ function SetEnv
FRAMAC_WP_CACHE=offline
Echo "Set FRAMAC_WP_CACHE=$FRAMAC_WP_CACHE"
fi
-
- if [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
- FRAMAC_WP_CACHEDIR=./.wp-cache
- Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
+ if [ "$FRAMAC_WP_QUALIF" != "" ]; then
+ FRAMAC_WP_CACHEDIR=$FRAMAC_WP_QUALIF
+ else
+ if [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
+ FRAMAC_WP_CACHEDIR=./.wp-cache
+ Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
+ fi
fi
-
}
function CloneCache
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 6ce0a0bad6b..203ad4b1483 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -164,69 +164,6 @@ WP_CONFIGURE_MAKEFILE= \
$(Wp_DIR)/Makefile: $(WP_CONFIGURE_MAKEFILE)
@cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
-# --------------------------------------------------------------------------
-# --- Qualif Tests ---
-# --------------------------------------------------------------------------
-
-.PHONY: wp-qualif wp-qualif-update wp-qualif-upgrade wp-qualif-push wp-qualif-status
-
-WP_QUALIF_CACHE?=$(abspath $(Wp_DIR)/../wp-cache)
-WP_QUALIF_ENTRIES=git -C $(WP_QUALIF_CACHE) ls-files --others --exclude-standard | wc -l
-
-WP_CHECKOUT_CACHE=\
- echo "[CACHE] repo: $(WP_QUALIF_CACHE)" && \
- git -C $(WP_QUALIF_CACHE) checkout master
-
-wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
- $(WP_CHECKOUT_CACHE)
- FRAMAC_WP_CACHE=replay \
- FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
-
-WP_PULL_CACHE=\
- echo "[CACHE] pull cache" && \
- $(WP_CHECKOUT_CACHE) && \
- git -C $(WP_QUALIF_CACHE) pull --rebase --prune
-
-wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
- $(WP_PULL_CACHE)
- @echo "[TESTS] updating wp-qualif"
- FRAMAC_WP_CACHE=update \
- FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif
- @echo "[CACHE] cache status"
- git -C $(WP_QUALIF_CACHE) status -s -b -u no
- @echo "New entries: `$(WP_QUALIF_ENTRIES)`"
-
-wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt
- $(WP_PULL_CACHE)
- @echo "[TESTS] upgrading wp-qualif (cache & scripts)"
- FRAMAC_WP_CACHE=update \
- FRAMAC_WP_SCRIPT=update \
- FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif
- @echo "[CACHE] cache status"
- git -C $(WP_QUALIF_CACHE) status -s -b -u no
- @echo "New entries: `$(WP_QUALIF_ENTRIES)`"
-
-wp-qualif-push:
- @echo "[CACHE] pushing updates"
- $(WP_CHECKOUT_CACHE)
- git -C $(WP_QUALIF_CACHE) add -A
- git -C $(WP_QUALIF_CACHE) commit -m "[wp] cache updates"
- git -C $(WP_QUALIF_CACHE) push -f
-
-wp-qualif-status:
- @echo "[CACHE] status"
- $(WP_CHECKOUT_CACHE)
- git -C $(WP_QUALIF_CACHE) status -s -b -u no
- @echo "New entries: `$(WP_QUALIF_ENTRIES)`"
-
-$(WP_QUALIF_CACHE):
- @echo "[CACHE] cloning wp global at $(WP_QUALIF_CACHE)..."
- @echo "Use env. variable WP_QUALIF_CACHE to change this location."
- @git clone "git@git.frama-c.com:frama-c/wp-cache.git" $(WP_QUALIF_CACHE)
-
# --------------------------------------------------------------------------
# --- WP API ---
# --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 572734b69d1..3d90fddfa98 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -1,129 +1,56 @@
-# Running qualif tests
-
-- Be sure that you have installed the appropriate versions of
- alt-ergo and coq _before_ having compiled Frama-C.
-- use `make wp-qualif` in the toplevel Frama-C directory
-
-# Test Suites
-
-Here is a short description of the WP test suites:
-
-- `tests/wp` tests dedicated to the VC generation engine and proof strategy
-- `tests/wp_tip` tests associated to the script engine
-- `tests/wp_acsl` tests of generic C/ACSL concepts
-- `tests/wp_typed` tests dedicated to aliasing memory model
-- `tests/wp_hoare` tests dedicated to non-aliasing memory model
-- `tests/wp_region` tests dedicated to region memory model
-- `tests/wp_manual` tests for generating the examples of the reference manual
-- `tests/wp_gallery` non-regression tests for representative real size usage of WP
-- `tests/wp_plugin` general purpose WP plug-in options
-- `tests/wp_bts` non-regression tests associated to GitLab issues; eg. `issue_xxx.i`
-
-Deprecated test suites that shall be moved around:
-
-- `tests/wp_usage` mostly movable to `tests/wp_plugin`
-- `tests/wp_store` mostly movable to `tests/wp_typed`
-
-# Test Configurations
-
-There are two test configurations:
-- the default one requires _no_ prover execution;
-- the `qualif` configuration uses the `wp-cache` global cache, `Alt-Ergo` and `Coq`.
-
-The test configurations `tests/test_config` and `tests/test_config_qualif` are
-carefully crafted to fit with the constraints of the GitLab
-Continuous Integration system. In particular, the `qualif` configuration is
-designed for being used with a clone of the global WP cache, see
-installation instructions below.
-
-To re-run tests, use by default the following commands:
-- `make Wp_TESTS` for the default test configuration;
-- `make wp-qualif` for the `qualif` configuration.
-
-When using the `wp-qualif` target, it will clone the global wp-cache at `../wp-cache` by default,
-if not yet present. To choose another place, consult the « Global WP Cache »
-installation instructions below.
-The WP makefile provides several targets to automate cache management. It is highly
-recommanded to use them most of the time:
-
-- `make wp-qualif` re-runs qualif tests; no new cache entry is created, though.
-- `make wp-qualif-env` prints the environment variables for wp-qualif.
-- `make wp-qualif-update` re-runs and creates missing cache entries.
-- `make wp-qualif-upgrade` creates missing cache entries _and_ updates test scripts if necessary.
-- `make wp-qualif-push` commits and pushes all new cache entries to the GitLab repository.
-- `make wp-qualif-status` displays a very short git status of your local wp-cache.
-
-To execute a given test by hand in `qualif` configuration, use the following
-commands in a _local_ shell:
-
- $ export FRAMAC_WP_CACHE=update
- $ export FRAMAC_WP_CACHEDIR=<path-to-wp-cache>
- $ ./bin/ptests.opt src/plugins/wp/tests/xxx/yyy.i -config qualif [-show|-update]
-
-It is _highly_ recommanded to _not_ set the `FRAMAC_WP_xxx` variables globally;
-doing so would causing WP to add new cache entries to the global « qualif » cache
-from all your projects around. Consult the section « Global WP Cache Setup »
-below for details.
-
-Note that this cache is meant to be global, including for the different merge
-requests. Thus, when working on a new merge request for WP, **do not** create a
-branch (and MR) on the WP-cache repository: just push the new cache entries into
-the global cache using `make wp-qualif-push`.
-
-# Qualified Test Results
-
-To be accepted by Frama-CI, tests in « qualif » configuration must be easily
-reproducible on any platform. This is checked by running WP with flag
-`-wp-msg-key shell` which is set by the default in the qualif test
-configuration. Hence, a qualified test result only contains proof status that
-are either:
-- failed
-- valid for qed or script
-- cached for alt-ergo in all cases
-- valid, unknown or stepout for native Alt-Ergo
-- valid or unknown for (native) Coq
-
-This excludes any timeout with native Alt-Ergo, which must be turned into some
-reproducible stepout by setting `-wp-steps` and `-wp-timeout` options
-accordingly. Please choose a step limit that makes large enough to ensure the
-goal is provable, but small enough to make alt-ergo decide quickly.
-
-# Global WP Cache Setup (for wp-qualif)
-
-All prover results for test configuration `qualif` shall be cached in a dedicate
-GitLab repo. This considerally speed-up the process of running those tests,
-from hours downto minutes.
-
-To ease the management of cache entries accross merge requests,
-_all_ cache entries shall be merged into the _same_ master branch of a global
-repository, even if they come from _different_ Frama-C branches.
-This strategy prevents merge conflicts related to different cache
-entries and simplifies the review of MR, especially those modifying the VC
-generation process. The gitLab Frama-CI continuous integration system is aware of
-this strategy and always use the global cache.
-
-By default, the WP makefile will clone a local copy of the wp-cache in `../wp-cache`
-but you can choose another place with the following commands:
-
- $ git clone git@git.frama-c.com:frama-c/wp-cache.git <your-cache>
- $ export WP_QUALIF_CACHE=<absolute-path-to-your-cache>
-
-The WP makefile uses `WP_QUALIF_CACHE` environment variable to know where your
-local copy of cache has been installed. You shall put it in your global shell
-environment. To run individual tests, you may now use:
-
- $ export FRAMAC_WP_CACHE=update
- $ export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
- $ ./bin/ptests.opt src/plugins/wp/tests/xxx/yyy.i -config qualif [-show|-update]
-
-An utility script is provided to export the necessary environment variables
-(dont forget the `.` to execute the script in the current shell environment):
-
- $ . bin/wp_qualif.sh
-
-As mentionned above, it is _not_ recommanded to globally set the
-`FRAMAC_WP_XXX` variables in your default shell environment, because WP will
-use it by default and would merge any new cache entry there, even those
-non-related to the « qualif » test suite. For this reason,
-it is _highly_ recommended to use `WP_QUALIF_CACHE` globally
-and `FRAMAC_WP_CACHEDIR` locally.
+# Audience
+
+This manual is _only_ intended for Frama-C developpers who need to execute tests
+that are using WP with external provers.
+
+## WP Tests Configurations
+
+There are two configurations for WP tests:
+- the default configuration, which does not use external provers
+- the `qualif` configuration, which _does_ use external provers
+
+It is highly recommended to use the `./bin/test.sh` wrapper for executing WP tests.
+See section « WP Tests Recipes » below for details.
+
+Advanced users might consider managing the cache on their own.
+See section « Advanced Cache Management. »
+
+## WP Tests Recipes
+
+When using the `./bin/test.sh` test wrapper, you don't need to configure the
+environment variables mentionned above: the script automatically manages them for you.
+
+Before executing WP tests in qualif configuration, you shall initiate the WP-cache.
+This is done automatically by:
+
+ $ ./bin/test.sh -p
+
+The first time it is executed, it will clone the `wp-cache` Git repository in `./.wp-cache`.
+Next times, this same command will automatically pull the latest cache entries.
+
+You check tests are up-to-date with:
+
+ $ ./bin/tests.sh src/plugins/wp/tests
+
+When a test complains that a test result is missing from wp-cache, simply re-run
+the desired tests in « update » mode:
+
+ $ ./bin/tests.sh src/plugins/wp/tests/… -u
+
+If neceassary, you may `dune promote` the new oracles and, correspondly,
+you may `git commit` the new cache entries from `./.wp-cache` directory.
+
+## Advanced Cache Management
+
+It is possible to share the wp-cache repository among different plug-ins.
+The `./bin/test.sh` uses, in order of proprity:
+- `FRAMAC_WP_QUALIF` environment variable,
+- `FRAMAC_WP_CACHEDIR` environement variable,
+- local `./.wp-cache` directory.
+
+It is _not_ recommended to use the `FRAMAC_WP_CACHEDIR` variable in your default
+shell setup, unless is it a temporary directory (eg. `/tmp/wp-sandbox`) since
+_every_ run of `frama-c -wp` might then use it by default. Be carefull if you do so.
+
+However, it is _highly_ recommended for frama-c developpers to export the
+`FRAMAC_WP_QUALIF` variable in their default shell setup.
--
GitLab