From 380e96d965f4d09a9685547a87bcb8f113fcef97 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Fri, 23 Oct 2026 14:37:27 +0200 Subject: [PATCH 1/3] Use shared support for running cpp2v via docker --- .gitignore | 3 - README.md | 28 ++--- dune.disabled | 22 ---- rocq-brick-libstdcpp/cpp2v_docker.in | 103 ------------------ rocq-brick-libstdcpp/dune | 27 ++--- rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh | 26 ++++- rocq-brick-libstdcpp/proof/dune-gen.sh | 2 +- rocq-brick-libstdcpp/proof/dune.inc | 57 ++++------ rocq-brick-libstdcpp/test/dune-gen.sh | 2 +- rocq-brick-libstdcpp/test/dune.inc | 105 +++++++------------ 10 files changed, 91 insertions(+), 284 deletions(-) delete mode 100644 dune.disabled delete mode 100644 rocq-brick-libstdcpp/cpp2v_docker.in diff --git a/.gitignore b/.gitignore index af745d27..1589c7dd 100644 --- a/.gitignore +++ b/.gitignore @@ -14,6 +14,3 @@ mutexes.pdf mutexes.synctex.gz comment.cut _RocqProject - -# Only at the root, since it comes from enabling `dune.disabled` locally -/dune diff --git a/README.md b/README.md index 4ed26062..034b6873 100644 --- a/README.md +++ b/README.md @@ -7,30 +7,14 @@ Specifications of the C++ standard library in BRiCk. To develop on these specifications, you'll need clang, the GNU C++ library (not clang's own version), and Skylabs AI's verification toolchain. -With access to our release image, you can: -- Open this repo in a devcontainer using our Docker release image; see `.devcontainer/README.md`. - If you have access to our automation sources, you can check this out as part of https://github.com/SkyLabsAI/workspace. After `make vendored-pull fmdeps-pull`, -you'll find a copy of this repository in `fmdeps/brick-libcpp`. Then: - -- on Linux with a suitable clang + GNU C++ library toolchain, you can build this - directly. -- on any platform, you can route AST generation through our Docker image. Use - this route when local AST generation fails because libstdc++ headers such as - `` cannot be found. +you'll find a copy of this repository in `fmdeps/brick-libcpp`. Build from the +composed workspace root: -To enable Docker-backed AST generation in the composed workspace, go to -`workspace` and run +```sh +dune build fmdeps/brick-libcpp ``` -cd fmdeps/brick-libcpp; cp dune.disabled dune -``` - -The copied `dune` file is a local, ignored opt-in. It makes Dune use -`rocq-brick-libstdcpp/cpp2v_docker` as `cpp2v` for the libstdc++ specs and -tests, so Docker must be running and accessible to the build. -The setup can be especially useful when one needs to use `libstdc++` -which is not available on all platforms. To reduce demands on the -docker virtual machines, one can enable its use selectively. See -`rocq-brick-libstdcpp/cpp2v_docker.in` for more details. +For Docker-backed builds, see the +[BRiCk Docker setup documentation](https://github.com/SkyLabsAI/BRiCk/blob/main/rocq-skylabs-cpp2v/scripts/README.md). diff --git a/dune.disabled b/dune.disabled deleted file mode 100644 index b26dfde8..00000000 --- a/dune.disabled +++ /dev/null @@ -1,22 +0,0 @@ -; Copy as dune to enable - -(subdir rocq-brick-libstdcpp - ; hack: we can't add (env) here, so we only add it to subfolders - (subdir proof - (env - (_ - (binaries - (../cpp2v_docker as cpp2v)) - (env-vars - ; (CPP2V_DOCKER_ENABLED "if-libstdc++") ; This will call `cpp2v` through `docker` only for files that require `libstdc++` - (CPP2V_DOCKER_ENABLED "y") ; This will use docker for all calls of `cpp2v` - )))) - - (subdir test - (env - (_ - (binaries - (../cpp2v_docker as cpp2v)) - (env-vars - ; (CPP2V_DOCKER_ENABLED "if-libstdc++") - (CPP2V_DOCKER_ENABLED "y")))))) diff --git a/rocq-brick-libstdcpp/cpp2v_docker.in b/rocq-brick-libstdcpp/cpp2v_docker.in deleted file mode 100644 index a40cc1c3..00000000 --- a/rocq-brick-libstdcpp/cpp2v_docker.in +++ /dev/null @@ -1,103 +0,0 @@ -#!/usr/bin/env bash - -REALPATH=$(which grealpath || which realpath) -REL_PATH="$($REALPATH `pwd` --relative-to "$DUNE_SOURCEROOT")" - -map_absolute_paths () { - while [[ $# -gt 0 ]]; do - if [[ $1 =~ ^/.*\.(v|cpp|hpp|h|c) ]] && [[ -f "$1" ]]; then - local dir="$(dirname "$1")" - echo "--volume" "$dir:$dir" - fi - shift - done -} - -check_lib_cpp_flag () { - while [[ $# -gt 0 ]]; do - if [[ $1 == -stdlib=libstdc++ ]]; then - return 0 - fi - shift - done - return 1 -} - -if [ -n "$IN_CPP2V_DOCKER" ]; then - echo "Error: recursive invocation of \"cpp2v_docker\" as $0 from outer cpp2v_docker as ${IN_CPP2V_DOCKER}" - echo "(PATH is $PATH)." - exit 1 -fi - -CMD_LINE="$(printf "%q %q " "$0" "$@")" - -verbose () { - local cmd="$1" ; shift - if ! "$cmd" "$@" ; then - local r="$?" - cat 1>&2 < /dev/null; then - # Here we could warn - : -fi - -if [ "$CPP2V_DOCKER_ENABLED" = "y" ] && which docker > /dev/null; then - if [ -z "$CPP2V_DOCKER_IMAGE" ]; then - # We skip the warning if no docker is available - echo "Misconfiguration: CPP2V_DOCKER_ENABLED = y and docker available, but CPP2V_DOCKER_IMAGE is empty" - exit 2 - fi - - BRICK_LIBCPP=/home/coq/worktree - ARGS=() - - docker_user="${CPP2V_DOCKER_USER:-$(id -u):$(id -g)}" - ARGS+=( "--rm" ) - ARGS+=( "--user" "$docker_user" ) - ARGS+=( "--env" "HOME=/tmp" ) - ARGS+=( "--platform" "linux/amd64" ) - ARGS+=( "--volume" "${HOME}/.cache/remote_dune:/home/coq/.cache/dune:cached" ) - ARGS+=( "--volume" "$DUNE_SOURCEROOT:$BRICK_LIBCPP" ) - ARGS+=( "--workdir" "$BRICK_LIBCPP/$REL_PATH" ) - ARGS+=( $(map_absolute_paths "$@") ) - - cpp2v_args="$( printf '"%q" ' "$@" )" # ensure each argument is quoted as a whole. - verbose docker run "${ARGS[@]}" "$CPP2V_DOCKER_IMAGE" \ - /bin/bash -c 'eval $(opam env)'"; cpp2v $cpp2v_args" -else - export IN_CPP2V_DOCKER="$0" - next=$DUNE_SOURCEROOT/_build/install/default/bin/cpp2v - [ -e $next ] || next='opam exec -- cpp2v' - exec $next "$@" -fi - -# We embed these hashes just to track dependencies. -# CPP2V_SHA1="@CPP2V_SHA1@" -# CPP2V_DOCKER_IMAGE_ID="@CPP2V_DOCKER_IMAGE_ID@" diff --git a/rocq-brick-libstdcpp/dune b/rocq-brick-libstdcpp/dune index fda57052..31e9aa5c 100644 --- a/rocq-brick-libstdcpp/dune +++ b/rocq-brick-libstdcpp/dune @@ -1,35 +1,24 @@ (rule - (target cpp2v_docker) + (target cpp_environment) (deps (universe) - (:sha1sum %{bin:sha1sum}) - (:template cpp2v_docker.in)) + (env_var CPP2V_DOCKER_ENABLED) + (env_var CPP2V_DOCKER_IMAGE) + (env_var CPP2V_DOCKER_USER)) (action - (progn - (with-stdout-to - %{target} - (bash - "set -eu -hash=$(%{sha1sum} %{bin:cpp2v} | cut -d ' ' -f 1) -image_id= -if command -v docker >/dev/null 2>&1; then - image_id=$(docker inspect --format='{{.Id}}' %{env:CPP2V_DOCKER_IMAGE=} 2>/dev/null || true) -fi -sed -e \"s/@CPP2V_SHA1@/$hash/g\" -e \"s/@CPP2V_DOCKER_IMAGE_ID@/$image_id/g\" %{template}")) - (run chmod +x %{target})))) + (with-stdout-to %{target} + (run %{bin:cpp2v-toolchain} configure + --default-image skylabsai/fm-releases:fm-release-nightly + --platform linux/amd64 --opam)))) (env (sl_timing (binaries (../../BRiCk/rocq-tools/bin/rocq_perf.exe as rocq)) - (env-vars - (CPP2V_DOCKER_IMAGE "skylabsai/fm-releases:fm-release-nightly")) (rocq (rocqdep_flags :standard -w +all) (flags :standard %{read-lines:flags/coqc} -w +sl-transparent-constants))) ; Same, but without rocq_perf (_ - (env-vars - (CPP2V_DOCKER_IMAGE "skylabsai/fm-releases:fm-release-nightly")) (rocq (rocqdep_flags :standard -w +all) (flags :standard %{read-lines:flags/coqc} -w +sl-transparent-constants)))) diff --git a/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh b/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh index af360836..8d5a13a3 100755 --- a/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh +++ b/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh @@ -3,7 +3,7 @@ usage() { cat >&2 <<-EOF - usage: $(basename "$0") [ -t ] . -- [ ] + usage: $(basename "$0") [ --toolchain CONFIG ] [ -t ] . -- [ ] This will output (to stdout) dune rules for building ., passing to cpp2v. Redirect output to dune.inc and @@ -39,7 +39,13 @@ outRule() { # if [ "$system" = 1 ]; then # universe=" (universe)" # fi - local cpp2v="cpp2v -v %{input} -o ${module} --no-elaborate" + local cpp2v="cpp2v" + local action_indent=$'\t ' + if [ -n "$toolchain" ]; then + action_indent=" " + cpp2v="%{bin:cpp2v-run} --config %{dep:${toolchain}} --host-tool %{bin:cpp2v} --container-tool cpp2v --" + fi + cpp2v="${cpp2v} -v %{input} -o ${module} --no-elaborate" if [ "$gen_names" = 1 ]; then local names="${name}_${ext}_names.v" @@ -61,10 +67,9 @@ outRule() { (alias test_ast) (deps (:input ${name}.${ext}) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ${prefix}*.hpp)${universe}) (action - (with-stderr-to ${module}.stderr ${action}))) + ${action_indent}(with-stderr-to ${module}.stderr ${action}))) (alias (name srcs) (deps ${name}.${ext})) EOF # TODO: maybe drop @srcs alias, seems leftover from !2613 @@ -85,7 +90,12 @@ traverse() { #echo DIR $firstDir #echo REST $rest echo "${indent}(subdir ${firstDir}" - (cd "${firstDir}"; traverse " $indent" "$rest" "$@") + ( + cd "${firstDir}" || exit + # Resolve CONFIG relative to each generated subdir scope. + case "$toolchain" in ""|/*) ;; *) toolchain="../$toolchain" ;; esac + traverse " $indent" "$rest" "$@" + ) || return echo "${indent})" fi } @@ -94,9 +104,15 @@ gen_names=0 templates=0 system=0 prefix="../" +toolchain="" while : do case "$1" in + --toolchain) + [ $# -ge 2 ] && [ -n "$2" ] || usage + toolchain="$2" + shift 2 + ;; -n) gen_names=1 shift diff --git a/rocq-brick-libstdcpp/proof/dune-gen.sh b/rocq-brick-libstdcpp/proof/dune-gen.sh index 430c67e1..0ba3b5ac 100755 --- a/rocq-brick-libstdcpp/proof/dune-gen.sh +++ b/rocq-brick-libstdcpp/proof/dune-gen.sh @@ -24,5 +24,5 @@ while read i; do if [[ $i =~ ^./(algorithms|vector)/.* ]]; then args+="-t" fi - ./cpp2v-dune-gen.sh -t -s ${args} -- $i -- -std=c++20 -stdlib=libstdc++ + ./cpp2v-dune-gen.sh --toolchain ../cpp_environment -t -s ${args} -- $i -- -std=c++20 -stdlib=libstdc++ done diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index b173654d..707d3d7d 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/rocq-brick-libstdcpp/proof/dune.inc @@ -5,10 +5,9 @@ (alias test_ast) (deps (:input inc_algorithms.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_algorithms_cpp.v.stderr (run cpp2v -v %{input} -o inc_algorithms_cpp.v --no-elaborate --templates=inc_algorithms_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_algorithms_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_algorithms_cpp.v --no-elaborate --templates=inc_algorithms_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_algorithms.cpp)) ) (subdir array @@ -17,10 +16,9 @@ (alias test_ast) (deps (:input inc_array.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_array_cpp.v.stderr (run cpp2v -v %{input} -o inc_array_cpp.v --no-elaborate --templates=inc_array_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_array_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_array_cpp.v --no-elaborate --templates=inc_array_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_array.cpp)) ) (subdir atomic @@ -41,10 +39,9 @@ (alias test_ast) (deps (:input inc_cassert.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_cassert_cpp.v.stderr (run cpp2v -v %{input} -o inc_cassert_cpp.v --no-elaborate --templates=inc_cassert_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_cassert_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_cassert_cpp.v --no-elaborate --templates=inc_cassert_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_cassert.cpp)) ) (subdir cctype @@ -53,10 +50,9 @@ (alias test_ast) (deps (:input inc_cctype.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_cctype_cpp.v.stderr (run cpp2v -v %{input} -o inc_cctype_cpp.v --no-elaborate --templates=inc_cctype_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_cctype_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_cctype_cpp.v --no-elaborate --templates=inc_cctype_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_cctype.cpp)) ) (subdir compare @@ -65,10 +61,9 @@ (alias test_ast) (deps (:input inc_compare.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_compare_cpp.v.stderr (run cpp2v -v %{input} -o inc_compare_cpp.v --no-elaborate --templates=inc_compare_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_compare_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_compare_cpp.v --no-elaborate --templates=inc_compare_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_compare.cpp)) ) (subdir cstdlib @@ -77,10 +72,9 @@ (alias test_ast) (deps (:input inc_cstdlib.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_cstdlib_cpp.v.stderr (run cpp2v -v %{input} -o inc_cstdlib_cpp.v --no-elaborate --templates=inc_cstdlib_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_cstdlib_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_cstdlib_cpp.v --no-elaborate --templates=inc_cstdlib_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_cstdlib.cpp)) ) (subdir cstring @@ -89,10 +83,9 @@ (alias test_ast) (deps (:input inc_cstring.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_cstring_cpp.v.stderr (run cpp2v -v %{input} -o inc_cstring_cpp.v --no-elaborate --templates=inc_cstring_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_cstring_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_cstring_cpp.v --no-elaborate --templates=inc_cstring_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_cstring.cpp)) ) (subdir initializer_list @@ -101,10 +94,9 @@ (alias test_ast) (deps (:input inc_initializer_list.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_initializer_list_cpp.v.stderr (run cpp2v -v %{input} -o inc_initializer_list_cpp.v --no-elaborate --templates=inc_initializer_list_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_initializer_list_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_initializer_list_cpp.v --no-elaborate --templates=inc_initializer_list_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_initializer_list.cpp)) ) (subdir iostream @@ -113,10 +105,9 @@ (alias test_ast) (deps (:input inc_iostream.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_iostream_cpp.v.stderr (run cpp2v -v %{input} -o inc_iostream_cpp.v --no-elaborate --templates=inc_iostream_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_iostream_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_iostream_cpp.v --no-elaborate --templates=inc_iostream_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_iostream.cpp)) ) (subdir iostream_trace @@ -125,10 +116,9 @@ (alias test_ast) (deps (:input inc_iostream.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_iostream_cpp.v.stderr (run cpp2v -v %{input} -o inc_iostream_cpp.v --no-elaborate --templates=inc_iostream_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_iostream_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_iostream_cpp.v --no-elaborate --templates=inc_iostream_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_iostream.cpp)) ) (subdir memory @@ -137,10 +127,9 @@ (alias test_ast) (deps (:input inc.hpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_hpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc.hpp)) ) (subdir mutex @@ -149,10 +138,9 @@ (alias test_ast) (deps (:input demo.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v --no-elaborate --templates=demo_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to demo_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o demo_cpp.v --no-elaborate --templates=demo_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps demo.cpp)) ) (subdir mutex @@ -161,10 +149,9 @@ (alias test_ast) (deps (:input inc.hpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_hpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc.hpp)) ) (subdir new @@ -173,10 +160,9 @@ (alias test_ast) (deps (:input inc_new.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v --no-elaborate --templates=inc_new_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_new_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_new_cpp.v --no-elaborate --templates=inc_new_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_new.cpp)) ) (subdir semaphore @@ -185,10 +171,9 @@ (alias test_ast) (deps (:input inc.hpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_hpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc.hpp)) ) (subdir semaphore @@ -197,10 +182,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate --templates=test_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate --templates=test_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir shared_mutex @@ -209,10 +193,9 @@ (alias test_ast) (deps (:input inc.hpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_hpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_hpp.v --no-elaborate --templates=inc_hpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc.hpp)) ) (subdir string @@ -221,10 +204,9 @@ (alias test_ast) (deps (:input inc_string.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_string_cpp.v.stderr (run cpp2v -v %{input} -o inc_string_cpp.v --no-elaborate --templates=inc_string_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_string_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_string_cpp.v --no-elaborate --templates=inc_string_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_string.cpp)) ) (subdir vector @@ -233,9 +215,8 @@ (alias test_ast) (deps (:input inc_vector.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_vector_cpp.v.stderr (run cpp2v -v %{input} -o inc_vector_cpp.v --no-elaborate --templates=inc_vector_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_vector_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_vector_cpp.v --no-elaborate --templates=inc_vector_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_vector.cpp)) ) diff --git a/rocq-brick-libstdcpp/test/dune-gen.sh b/rocq-brick-libstdcpp/test/dune-gen.sh index afdc9fa2..a8fae731 100755 --- a/rocq-brick-libstdcpp/test/dune-gen.sh +++ b/rocq-brick-libstdcpp/test/dune-gen.sh @@ -20,5 +20,5 @@ echo "; DO NOT EDIT: Generated by \"$0${1+ $*}\"" find . -name '*.[ch]pp' | LC_ALL=C sort | while read i; do - ./cpp2v-dune-gen.sh -s -- $i -- -std=c++20 -stdlib=libstdc++ + ./cpp2v-dune-gen.sh --toolchain ../cpp_environment -s -- $i -- -std=c++20 -stdlib=libstdc++ done diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 43e3a819..53425f58 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -5,10 +5,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir atomic @@ -29,10 +28,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir compare @@ -41,10 +39,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir cstdlib @@ -53,10 +50,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir cstring @@ -65,10 +61,9 @@ (alias test_ast) (deps (:input null_ub.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to null_ub_cpp.v.stderr (run cpp2v -v %{input} -o null_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to null_ub_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o null_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps null_ub.cpp)) ) (subdir cstring @@ -77,10 +72,9 @@ (alias test_ast) (deps (:input strncmp_ub.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to strncmp_ub_cpp.v.stderr (run cpp2v -v %{input} -o strncmp_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to strncmp_ub_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o strncmp_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps strncmp_ub.cpp)) ) (subdir cstring @@ -89,10 +83,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir g4g @@ -101,10 +94,9 @@ (alias test_ast) (deps (:input N12_area.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N12_area_cpp.v.stderr (run cpp2v -v %{input} -o N12_area_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N12_area_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N12_area_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N12_area.cpp)) ) (subdir g4g @@ -113,10 +105,9 @@ (alias test_ast) (deps (:input N1_hello_world.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N1_hello_world_cpp.v.stderr (run cpp2v -v %{input} -o N1_hello_world_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N1_hello_world_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N1_hello_world_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N1_hello_world.cpp)) ) (subdir g4g @@ -125,10 +116,9 @@ (alias test_ast) (deps (:input N4_sum.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N4_sum_cpp.v.stderr (run cpp2v -v %{input} -o N4_sum_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N4_sum_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N4_sum_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N4_sum.cpp)) ) (subdir g4g @@ -137,10 +127,9 @@ (alias test_ast) (deps (:input N4_sum_a.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N4_sum_a_cpp.v.stderr (run cpp2v -v %{input} -o N4_sum_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N4_sum_a_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N4_sum_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N4_sum_a.cpp)) ) (subdir g4g @@ -149,10 +138,9 @@ (alias test_ast) (deps (:input N5_swap.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N5_swap_cpp.v.stderr (run cpp2v -v %{input} -o N5_swap_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N5_swap_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N5_swap_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N5_swap.cpp)) ) (subdir g4g @@ -161,10 +149,9 @@ (alias test_ast) (deps (:input N5_swap_a.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N5_swap_a_cpp.v.stderr (run cpp2v -v %{input} -o N5_swap_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N5_swap_a_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N5_swap_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N5_swap_a.cpp)) ) (subdir g4g @@ -173,10 +160,9 @@ (alias test_ast) (deps (:input N6_print_sizeof.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N6_print_sizeof_cpp.v.stderr (run cpp2v -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N6_print_sizeof_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N6_print_sizeof.cpp)) ) (subdir g4g_trace @@ -185,10 +171,9 @@ (alias test_ast) (deps (:input N12_area.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N12_area_cpp.v.stderr (run cpp2v -v %{input} -o N12_area_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N12_area_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N12_area_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N12_area.cpp)) ) (subdir g4g_trace @@ -197,10 +182,9 @@ (alias test_ast) (deps (:input N1_hello_world.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N1_hello_world_cpp.v.stderr (run cpp2v -v %{input} -o N1_hello_world_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N1_hello_world_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N1_hello_world_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N1_hello_world.cpp)) ) (subdir g4g_trace @@ -209,10 +193,9 @@ (alias test_ast) (deps (:input N4_sum.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N4_sum_cpp.v.stderr (run cpp2v -v %{input} -o N4_sum_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N4_sum_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N4_sum_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N4_sum.cpp)) ) (subdir g4g_trace @@ -221,10 +204,9 @@ (alias test_ast) (deps (:input N4_sum_a.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N4_sum_a_cpp.v.stderr (run cpp2v -v %{input} -o N4_sum_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N4_sum_a_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N4_sum_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N4_sum_a.cpp)) ) (subdir g4g_trace @@ -233,10 +215,9 @@ (alias test_ast) (deps (:input N5_swap.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N5_swap_cpp.v.stderr (run cpp2v -v %{input} -o N5_swap_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N5_swap_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N5_swap_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N5_swap.cpp)) ) (subdir g4g_trace @@ -245,10 +226,9 @@ (alias test_ast) (deps (:input N5_swap_a.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N5_swap_a_cpp.v.stderr (run cpp2v -v %{input} -o N5_swap_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N5_swap_a_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N5_swap_a_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N5_swap_a.cpp)) ) (subdir g4g_trace @@ -257,10 +237,9 @@ (alias test_ast) (deps (:input N6_print_sizeof.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to N6_print_sizeof_cpp.v.stderr (run cpp2v -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to N6_print_sizeof_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps N6_print_sizeof.cpp)) ) (subdir initializer_list @@ -269,10 +248,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir limits @@ -281,10 +259,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir memory @@ -293,10 +270,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir mutex @@ -305,10 +281,9 @@ (alias test_ast) (deps (:input custom_mutex.hpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to custom_mutex_hpp.v.stderr (run cpp2v -v %{input} -o custom_mutex_hpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to custom_mutex_hpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o custom_mutex_hpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps custom_mutex.hpp)) ) (subdir mutex @@ -317,10 +292,9 @@ (alias test_ast) (deps (:input custom_recursive_mutex.hpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to custom_recursive_mutex_hpp.v.stderr (run cpp2v -v %{input} -o custom_recursive_mutex_hpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to custom_recursive_mutex_hpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o custom_recursive_mutex_hpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps custom_recursive_mutex.hpp)) ) (subdir mutex @@ -329,10 +303,9 @@ (alias test_ast) (deps (:input guard_recursive.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to guard_recursive_cpp.v.stderr (run cpp2v -v %{input} -o guard_recursive_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to guard_recursive_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o guard_recursive_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps guard_recursive.cpp)) ) (subdir mutex @@ -341,10 +314,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir new @@ -353,10 +325,9 @@ (alias test_ast) (deps (:input demo.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to demo_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o demo_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps demo.cpp)) ) (subdir shared_mutex @@ -365,10 +336,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir string @@ -377,10 +347,9 @@ (alias test_ast) (deps (:input erase_out_of_range.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to erase_out_of_range_cpp.v.stderr (run cpp2v -v %{input} -o erase_out_of_range_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to erase_out_of_range_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o erase_out_of_range_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps erase_out_of_range.cpp)) ) (subdir string @@ -389,10 +358,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir vector @@ -401,10 +369,9 @@ (alias test_ast) (deps (:input data_ub.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to data_ub_cpp.v.stderr (run cpp2v -v %{input} -o data_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to data_ub_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o data_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps data_ub.cpp)) ) (subdir vector @@ -413,10 +380,9 @@ (alias test_ast) (deps (:input erase_ub.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to erase_ub_cpp.v.stderr (run cpp2v -v %{input} -o erase_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to erase_ub_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o erase_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps erase_ub.cpp)) ) (subdir vector @@ -425,9 +391,8 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) From 6bc5d91898ddaa7c7d7dd7cb0e192fc72822c4c1 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Mon, 26 Oct 2026 18:08:45 +0100 Subject: [PATCH 2/3] Do not inline cpp code that depends on system headers --- rocq-brick-libstdcpp/proof/dune.inc | 3 +- rocq-brick-libstdcpp/test/dune.inc | 36 +++++++++++++++++-- .../test/iostream/two_ints.cpp | 18 ++++++++++ rocq-brick-libstdcpp/test/iostream/two_ints.v | 20 ++--------- .../test/iostream_trace/extract.cpp | 17 +++++++++ .../test/iostream_trace/extract.v | 16 +-------- .../test/vector/iter_bounds.cpp | 27 ++++++++++++++ .../test/vector/iter_bounds.v | 26 +------------- 8 files changed, 102 insertions(+), 61 deletions(-) create mode 100644 rocq-brick-libstdcpp/test/iostream/two_ints.cpp create mode 100644 rocq-brick-libstdcpp/test/iostream_trace/extract.cpp create mode 100644 rocq-brick-libstdcpp/test/vector/iter_bounds.cpp diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index 707d3d7d..2791a84e 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/rocq-brick-libstdcpp/proof/dune.inc @@ -27,10 +27,9 @@ (alias test_ast) (deps (:input inc_int.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to inc_int_cpp.v.stderr (run cpp2v -v %{input} -o inc_int_cpp.v --no-elaborate --templates=inc_int_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to inc_int_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o inc_int_cpp.v --no-elaborate --templates=inc_int_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_int.cpp)) ) (subdir cassert diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 53425f58..d49363c6 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -16,10 +16,9 @@ (alias test_ast) (deps (:input test.cpp) - (env_var CPP2V_DOCKER_ENABLED) (glob_files_rec ../*.hpp)) (action - (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) (subdir cctype @@ -253,6 +252,28 @@ (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) +(subdir iostream + (rule + (targets two_ints_cpp.v.stderr two_ints_cpp.v) + (alias test_ast) + (deps + (:input two_ints.cpp) + (glob_files_rec ../*.hpp)) + (action + (with-stderr-to two_ints_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o two_ints_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps two_ints.cpp)) +) +(subdir iostream_trace + (rule + (targets extract_cpp.v.stderr extract_cpp.v) + (alias test_ast) + (deps + (:input extract.cpp) + (glob_files_rec ../*.hpp)) + (action + (with-stderr-to extract_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o extract_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps extract.cpp)) +) (subdir limits (rule (targets test_cpp.v.stderr test_cpp.v) @@ -385,6 +406,17 @@ (with-stderr-to erase_ub_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o erase_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps erase_ub.cpp)) ) +(subdir vector + (rule + (targets iter_bounds_cpp.v.stderr iter_bounds_cpp.v) + (alias test_ast) + (deps + (:input iter_bounds.cpp) + (glob_files_rec ../*.hpp)) + (action + (with-stderr-to iter_bounds_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o iter_bounds_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps iter_bounds.cpp)) +) (subdir vector (rule (targets test_cpp.v.stderr test_cpp.v) diff --git a/rocq-brick-libstdcpp/test/iostream/two_ints.cpp b/rocq-brick-libstdcpp/test/iostream/two_ints.cpp new file mode 100644 index 00000000..aded0cac --- /dev/null +++ b/rocq-brick-libstdcpp/test/iostream/two_ints.cpp @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + */ +#include + +int second(std::istream &in) { + int a = 0, b = 0; + in >> a; + in >> b; + return b; +} +int first(std::istream &in) { + int a = 5; + in >> a; + return a; +} diff --git a/rocq-brick-libstdcpp/test/iostream/two_ints.v b/rocq-brick-libstdcpp/test/iostream/two_ints.v index e836b2fc..2f63da91 100644 --- a/rocq-brick-libstdcpp/test/iostream/two_ints.v +++ b/rocq-brick-libstdcpp/test/iostream/two_ints.v @@ -4,7 +4,7 @@ * See the LICENSE-BedRock file in the repository root for details. *) Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +Require Import skylabs.brick.libstdcpp.test.iostream.two_ints_cpp. Require Import skylabs.brick.libstdcpp.iostream.spec. Import istream. @@ -12,23 +12,9 @@ Import istream. On the input "12-34 ", [second] returns -34 with libstdc++: the first extraction stops at '-' and leaves it in the stream, as the read-ahead of - [istream.R]. *) -cpp.prog source flags "-std=c++20 -stdlib=libstdc++" prog cpp:{{ - #include - int second(std::istream &in) { - int a = 0, b = 0; - in >> a; - in >> b; - return b; - } - int first(std::istream &in) { - int a = 5; - in >> a; - return a; - } -}}. + [istream.R]. -(** On the inputs "x" and "99999999999 ", [first] returns 0 and 2147483647 + On the inputs "x" and "99999999999 ", [first] returns 0 and 2147483647 with libstdc++, and the extraction sets [failbit]. *) Definition chars (s : String.string) : list N := diff --git a/rocq-brick-libstdcpp/test/iostream_trace/extract.cpp b/rocq-brick-libstdcpp/test/iostream_trace/extract.cpp new file mode 100644 index 00000000..7cc8760c --- /dev/null +++ b/rocq-brick-libstdcpp/test/iostream_trace/extract.cpp @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + */ +#include + +int init(std::istream &in) { + int b = 0; + in >> b; + return b; +} +int uninit(std::istream &in) { + int b; + in >> b; + return b; +} diff --git a/rocq-brick-libstdcpp/test/iostream_trace/extract.v b/rocq-brick-libstdcpp/test/iostream_trace/extract.v index 649918a9..84781108 100644 --- a/rocq-brick-libstdcpp/test/iostream_trace/extract.v +++ b/rocq-brick-libstdcpp/test/iostream_trace/extract.v @@ -4,7 +4,7 @@ * See the LICENSE-BedRock file in the repository root for details. *) Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +Require Import skylabs.brick.libstdcpp.test.iostream_trace.extract_cpp. Require Import skylabs.brick.libstdcpp.iostream_trace.spec. (** * [in >> b] may store nothing @@ -15,20 +15,6 @@ Require Import skylabs.brick.libstdcpp.iostream_trace.spec. empty input, which is undefined behavior (no clang sanitizer reports it: libstdc++ is not instrumented for MSan). The spec takes an initialized argument, so [init] verifies and [uninit] does not. *) -cpp.prog source flags "-std=c++20 -stdlib=libstdc++" prog cpp:{{ - #include - int init(std::istream &in) { - int b = 0; - in >> b; - return b; - } - int uninit(std::istream &in) { - int b; - in >> b; - return b; - } -}}. - Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. diff --git a/rocq-brick-libstdcpp/test/vector/iter_bounds.cpp b/rocq-brick-libstdcpp/test/vector/iter_bounds.cpp new file mode 100644 index 00000000..e2d2f8e0 --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/iter_bounds.cpp @@ -0,0 +1,27 @@ +/* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + */ +#include + +int deref_first() { + std::vector v; + v.push_back(7); + return *v.begin(); +} +void inc_to_end() { + std::vector v; + v.push_back(7); + auto it = v.begin(); + ++it; +} +bool deref_empty() { + std::vector v; + return &*v.begin() == nullptr; +} +void inc_past_end() { + std::vector v; + auto e = v.end(); + ++e; +} diff --git a/rocq-brick-libstdcpp/test/vector/iter_bounds.v b/rocq-brick-libstdcpp/test/vector/iter_bounds.v index e180be3b..df29fc0c 100644 --- a/rocq-brick-libstdcpp/test/vector/iter_bounds.v +++ b/rocq-brick-libstdcpp/test/vector/iter_bounds.v @@ -4,7 +4,7 @@ * See the LICENSE-BedRock file in the repository root for details. *) Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +Require Import skylabs.brick.libstdcpp.test.vector.iter_bounds_cpp. Require Import skylabs.brick.libstdcpp.allocator.spec. Require Import skylabs.brick.libstdcpp.vector.spec. @@ -15,30 +15,6 @@ Require Import skylabs.brick.libstdcpp.vector.spec. past-the-end values are dereferenceable"). [deref_empty] and [inc_past_end] violate this; [_GLIBCXX_DEBUG] reports both, and UBSan reports both here because an empty vector's iterators are null. *) -cpp.prog source flags "-std=c++20 -stdlib=libstdc++" prog cpp:{{ - #include - int deref_first() { - std::vector v; - v.push_back(7); - return *v.begin(); - } - void inc_to_end() { - std::vector v; - v.push_back(7); - auto it = v.begin(); - ++it; - } - bool deref_empty() { - std::vector v; - return &*v.begin() == nullptr; - } - void inc_past_end() { - std::vector v; - auto e = v.end(); - ++e; - } -}}. - Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. From 3878fd37f75224654a9e233e1cf0c285b18a5f5e Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Wed, 28 Oct 2026 23:05:12 +0100 Subject: [PATCH 3/3] Undo cpp.prog removal --- rocq-brick-libstdcpp/proof/dune | 11 +++++++ rocq-brick-libstdcpp/test/dune.inc | 33 ------------------- .../test/iostream/two_ints.cpp | 18 ---------- rocq-brick-libstdcpp/test/iostream/two_ints.v | 22 +++++++++++-- .../test/iostream_trace/extract.cpp | 17 ---------- .../test/iostream_trace/extract.v | 18 +++++++++- .../test/vector/iter_bounds.cpp | 27 --------------- .../test/vector/iter_bounds.v | 28 +++++++++++++++- 8 files changed, 74 insertions(+), 100 deletions(-) delete mode 100644 rocq-brick-libstdcpp/test/iostream/two_ints.cpp delete mode 100644 rocq-brick-libstdcpp/test/iostream_trace/extract.cpp delete mode 100644 rocq-brick-libstdcpp/test/vector/iter_bounds.cpp diff --git a/rocq-brick-libstdcpp/proof/dune b/rocq-brick-libstdcpp/proof/dune index 55024d2c..2f5f64fe 100644 --- a/rocq-brick-libstdcpp/proof/dune +++ b/rocq-brick-libstdcpp/proof/dune @@ -37,6 +37,17 @@ )) (include dune.inc) +; Expose the existing configuration once for configured inline quotations in +; this theory and its clients. The .v target orders generation before rocq dep. +(rule + (targets cpp_environment cpp_environment_dependency.v) + (deps (:config ../cpp_environment)) + (action + (progn + (copy %{config} cpp_environment) + (write-file cpp_environment_dependency.v + "(* Builds the inline toolchain configuration before rocq dep. *)\n")))) + (rule (action (with-stdout-to dune.inc.gen (run ./dune-gen.sh))) (deps (glob_files_rec *.{h,c,hpp,cpp,sh}))) diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index d49363c6..e0cf45ab 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -252,28 +252,6 @@ (with-stderr-to test_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) -(subdir iostream - (rule - (targets two_ints_cpp.v.stderr two_ints_cpp.v) - (alias test_ast) - (deps - (:input two_ints.cpp) - (glob_files_rec ../*.hpp)) - (action - (with-stderr-to two_ints_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o two_ints_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) - (alias (name srcs) (deps two_ints.cpp)) -) -(subdir iostream_trace - (rule - (targets extract_cpp.v.stderr extract_cpp.v) - (alias test_ast) - (deps - (:input extract.cpp) - (glob_files_rec ../*.hpp)) - (action - (with-stderr-to extract_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o extract_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) - (alias (name srcs) (deps extract.cpp)) -) (subdir limits (rule (targets test_cpp.v.stderr test_cpp.v) @@ -406,17 +384,6 @@ (with-stderr-to erase_ub_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o erase_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps erase_ub.cpp)) ) -(subdir vector - (rule - (targets iter_bounds_cpp.v.stderr iter_bounds_cpp.v) - (alias test_ast) - (deps - (:input iter_bounds.cpp) - (glob_files_rec ../*.hpp)) - (action - (with-stderr-to iter_bounds_cpp.v.stderr (run %{bin:cpp2v-run} --config %{dep:../../cpp_environment} --host-tool %{bin:cpp2v} --container-tool cpp2v -- -v %{input} -o iter_bounds_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) - (alias (name srcs) (deps iter_bounds.cpp)) -) (subdir vector (rule (targets test_cpp.v.stderr test_cpp.v) diff --git a/rocq-brick-libstdcpp/test/iostream/two_ints.cpp b/rocq-brick-libstdcpp/test/iostream/two_ints.cpp deleted file mode 100644 index aded0cac..00000000 --- a/rocq-brick-libstdcpp/test/iostream/two_ints.cpp +++ /dev/null @@ -1,18 +0,0 @@ -/* - * Copyright (c) 2026 SkyLabs AI, Inc. - * This software is distributed under the terms of the BedRock Open-Source License. - * See the LICENSE-BedRock file in the repository root for details. - */ -#include - -int second(std::istream &in) { - int a = 0, b = 0; - in >> a; - in >> b; - return b; -} -int first(std::istream &in) { - int a = 5; - in >> a; - return a; -} diff --git a/rocq-brick-libstdcpp/test/iostream/two_ints.v b/rocq-brick-libstdcpp/test/iostream/two_ints.v index 2f63da91..5bf35949 100644 --- a/rocq-brick-libstdcpp/test/iostream/two_ints.v +++ b/rocq-brick-libstdcpp/test/iostream/two_ints.v @@ -4,7 +4,8 @@ * See the LICENSE-BedRock file in the repository root for details. *) Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.test.iostream.two_ints_cpp. +Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +From skylabs.brick.libstdcpp Extra Dependency "cpp_environment" as cpp_environment. Require Import skylabs.brick.libstdcpp.iostream.spec. Import istream. @@ -12,9 +13,24 @@ Import istream. On the input "12-34 ", [second] returns -34 with libstdc++: the first extraction stops at '-' and leaves it in the stream, as the read-ahead of - [istream.R]. + [istream.R]. *) +#[environment="cpp_environment"] +cpp.prog source flags "-std=c++20 -stdlib=libstdc++" prog cpp:{{ + #include + int second(std::istream &in) { + int a = 0, b = 0; + in >> a; + in >> b; + return b; + } + int first(std::istream &in) { + int a = 5; + in >> a; + return a; + } +}}. - On the inputs "x" and "99999999999 ", [first] returns 0 and 2147483647 +(** On the inputs "x" and "99999999999 ", [first] returns 0 and 2147483647 with libstdc++, and the extraction sets [failbit]. *) Definition chars (s : String.string) : list N := diff --git a/rocq-brick-libstdcpp/test/iostream_trace/extract.cpp b/rocq-brick-libstdcpp/test/iostream_trace/extract.cpp deleted file mode 100644 index 7cc8760c..00000000 --- a/rocq-brick-libstdcpp/test/iostream_trace/extract.cpp +++ /dev/null @@ -1,17 +0,0 @@ -/* - * Copyright (c) 2026 SkyLabs AI, Inc. - * This software is distributed under the terms of the BedRock Open-Source License. - * See the LICENSE-BedRock file in the repository root for details. - */ -#include - -int init(std::istream &in) { - int b = 0; - in >> b; - return b; -} -int uninit(std::istream &in) { - int b; - in >> b; - return b; -} diff --git a/rocq-brick-libstdcpp/test/iostream_trace/extract.v b/rocq-brick-libstdcpp/test/iostream_trace/extract.v index 84781108..d59efa9b 100644 --- a/rocq-brick-libstdcpp/test/iostream_trace/extract.v +++ b/rocq-brick-libstdcpp/test/iostream_trace/extract.v @@ -4,7 +4,8 @@ * See the LICENSE-BedRock file in the repository root for details. *) Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.test.iostream_trace.extract_cpp. +Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +From skylabs.brick.libstdcpp Extra Dependency "cpp_environment" as cpp_environment. Require Import skylabs.brick.libstdcpp.iostream_trace.spec. (** * [in >> b] may store nothing @@ -15,6 +16,21 @@ Require Import skylabs.brick.libstdcpp.iostream_trace.spec. empty input, which is undefined behavior (no clang sanitizer reports it: libstdc++ is not instrumented for MSan). The spec takes an initialized argument, so [init] verifies and [uninit] does not. *) +#[environment="cpp_environment"] +cpp.prog source flags "-std=c++20 -stdlib=libstdc++" prog cpp:{{ + #include + int init(std::istream &in) { + int b = 0; + in >> b; + return b; + } + int uninit(std::istream &in) { + int b; + in >> b; + return b; + } +}}. + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. diff --git a/rocq-brick-libstdcpp/test/vector/iter_bounds.cpp b/rocq-brick-libstdcpp/test/vector/iter_bounds.cpp deleted file mode 100644 index e2d2f8e0..00000000 --- a/rocq-brick-libstdcpp/test/vector/iter_bounds.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/* - * Copyright (c) 2026 SkyLabs AI, Inc. - * This software is distributed under the terms of the BedRock Open-Source License. - * See the LICENSE-BedRock file in the repository root for details. - */ -#include - -int deref_first() { - std::vector v; - v.push_back(7); - return *v.begin(); -} -void inc_to_end() { - std::vector v; - v.push_back(7); - auto it = v.begin(); - ++it; -} -bool deref_empty() { - std::vector v; - return &*v.begin() == nullptr; -} -void inc_past_end() { - std::vector v; - auto e = v.end(); - ++e; -} diff --git a/rocq-brick-libstdcpp/test/vector/iter_bounds.v b/rocq-brick-libstdcpp/test/vector/iter_bounds.v index df29fc0c..113d0509 100644 --- a/rocq-brick-libstdcpp/test/vector/iter_bounds.v +++ b/rocq-brick-libstdcpp/test/vector/iter_bounds.v @@ -4,7 +4,8 @@ * See the LICENSE-BedRock file in the repository root for details. *) Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.test.vector.iter_bounds_cpp. +Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +From skylabs.brick.libstdcpp Extra Dependency "cpp_environment" as cpp_environment. Require Import skylabs.brick.libstdcpp.allocator.spec. Require Import skylabs.brick.libstdcpp.vector.spec. @@ -15,6 +16,31 @@ Require Import skylabs.brick.libstdcpp.vector.spec. past-the-end values are dereferenceable"). [deref_empty] and [inc_past_end] violate this; [_GLIBCXX_DEBUG] reports both, and UBSan reports both here because an empty vector's iterators are null. *) +#[environment="cpp_environment"] +cpp.prog source flags "-std=c++20 -stdlib=libstdc++" prog cpp:{{ + #include + int deref_first() { + std::vector v; + v.push_back(7); + return *v.begin(); + } + void inc_to_end() { + std::vector v; + v.push_back(7); + auto it = v.begin(); + ++it; + } + bool deref_empty() { + std::vector v; + return &*v.begin() == nullptr; + } + void inc_past_end() { + std::vector v; + auto e = v.end(); + ++e; + } +}}. + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}.