diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a7d7848c..44856cc1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -32,12 +32,9 @@ jobs: py-version: ["3.8", "3.9", "3.10", "3.11", "3.12", "3.13", "3.14"] include: - os: ubuntu-24.04 - cvc5-plat: "linux" - os: windows-2022 - cvc5-plat: "windows" - os: macos-14 brew: "/opt/homebrew" - cvc5-plat: "osx14" runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v4 @@ -60,10 +57,6 @@ jobs: run: | brew install make echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH - - name: Fetch CVC5 - run: | - util/fetch_cvc5.py ${{ matrix.cvc5-plat }} - echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH - name: Executing unit tests run: | make unit-tests diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 698e5a99..534ab8fa 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -43,13 +43,6 @@ jobs: pip install bmw-lobster-core==0.14.4 bmw-lobster-tool-python==0.14.4 pip install --no-deps bmw-lobster-tool-trlc sudo apt-get install -y graphviz - - name: Fetch CVC5 - run: | - util/fetch_cvc5.py linux - echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH - - name: Test CVC5 - run: | - cvc5 --version - name: Generate docs run: | make docs diff --git a/.gitignore b/.gitignore index 495fb5cd..8934aa7a 100644 --- a/.gitignore +++ b/.gitignore @@ -26,7 +26,3 @@ settings.json # Build-System ignores bazel-* - -# Special ignores for CI -cvc5 -cvc5.exe diff --git a/BUILD b/BUILD index d1adf96e..34fd86d5 100644 --- a/BUILD +++ b/BUILD @@ -15,8 +15,6 @@ py_binary( srcs = [ "trlc.py", ], - args = ["--use-cvc5-binary $(location //:cvc5)"], - data = ["//:cvc5"], main = "trlc.py", visibility = ["//visibility:public"], deps = [ @@ -24,16 +22,6 @@ py_binary( ], ) -alias( - name = "cvc5", - actual = select({ - "@bazel_tools//src/conditions:windows": "@cvc5_windows//:cvc5", - "@bazel_tools//src/conditions:darwin": "@cvc5_mac//:cvc5", - "//conditions:default": "@cvc5_linux//:cvc5", - }), - visibility = ["//visibility:public"], -) - # Run: bazel run //:requirements.update compile_pip_requirements( name = "requirements", diff --git a/CHANGELOG.md b/CHANGELOG.md index e5fac82b..b20ec485 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,6 +26,11 @@ generated in the following situations: ### 2.0.6-dev +* [TRLC, BAZEL] Removed the support for the CVC5 binary, and hence the + `--use-cvc5-binary` option is no longer available. + The option `--verify` now uses the CVC5 Python package + on all OS, and the CVC5 binary is no longer needed. + * [Sphinx] TRLC Plugin: fix parallel parsing: extension declareds parallel_read_safe -> only merge if worker actually owns the document diff --git a/MODULE.bazel b/MODULE.bazel index d450fdef..8f704cdf 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -83,33 +83,3 @@ pip_dev.parse( use_repo(pip_dev, "trlc_dev_dependencies") -http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive") - -# --------------------------------------------------------------------------- -# CVC5 binary archives -# Keep in synch with CVC5_DEFAULT_VERSION in util/fetch_cvc5.py -# and requirements.txt / requirements_dev.txt -# --------------------------------------------------------------------------- -http_archive( - name = "cvc5_linux", - build_file = "@trlc//:cvc5.BUILD", - sha256 = "30abf22d8042f3c4d3eb1120c595abd461f92f276a6d1264895fb4403b5fb3fd", - strip_prefix = "cvc5-Linux-x86_64-static-gpl", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-Linux-x86_64-static-gpl.zip", -) - -http_archive( - name = "cvc5_mac", - build_file = "@trlc//:cvc5.BUILD", - sha256 = "6c63ba3bd174d026be161be75f64df8d200c8a284012c49e91807f3ede5afc44", - strip_prefix = "cvc5-macOS-arm64-static-gpl", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-macOS-arm64-static-gpl.zip", -) - -http_archive( - name = "cvc5_windows", - build_file = "@trlc//:cvc5.BUILD", - sha256 = "206d55380f9a0ccf43541756b5ce2be487efcbbf322b93dc1de662856c70e5cc", - strip_prefix = "cvc5-Win64-x86_64-static", - url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-Win64-x86_64-static.zip", -) diff --git a/README.md b/README.md index 25cc8737..808c48cf 100644 --- a/README.md +++ b/README.md @@ -65,14 +65,9 @@ The Python implementation can be used for several purposes: ### Run-time * 3.8 <= Python3 <= 3.14 * [PyVCG](https://pypi.org/project/PyVCG) -* [PyPI CVC5](https://pypi.org/project/cvc5) +* [PyPI CVC5](https://pypi.org/project/cvc5)(GNU/Linux only) (required when using the `--verify` option) -Optional dependency (not installed automatically): -* [Binary CVC5](https://github.com/cvc5/cvc5/releases/tag/cvc5-1.3.2) - (An alternative to PyPI CVC5, make sure to rename the binary to - `cvc5` and put it on your PATH). - ## Acknowledgements Special thanks to [Florian Schanda](https://github.com/florianschanda) diff --git a/bazel/_private/mode_test.py b/bazel/_private/mode_test.py index e71a079f..bdc830d4 100644 --- a/bazel/_private/mode_test.py +++ b/bazel/_private/mode_test.py @@ -6,7 +6,6 @@ sys.argv[1] root_dir -- workspace-relative path of the test root, e.g. "tests-system" or "tests-large-partial" sys.argv[2] test_dir -- subdirectory name within root_dir - sys.argv[3] cvc5_rloc -- runfiles-relative path of the cvc5 binary Available modes are discovered at runtime by listing the ``output*`` golden files present in the test directory. An optional ``options`` file in the @@ -27,7 +26,6 @@ _ROOT_DIR = sys.argv[1] _TEST_DIR = sys.argv[2] -_CVC5_RLOC = sys.argv[3] def _srcdir(*parts): @@ -67,13 +65,8 @@ def _run_mode(mode): args = ["trlc"] - if mode == "output": + if mode in ("output", "output.smtlib"): args += ["--verify"] - elif mode == "output.smtlib": - # _CVC5_RLOC is a runfiles-relative path produced by - # $(rlocationpath //:cvc5); resolve it via TEST_SRCDIR directly. - cvc5 = os.path.join(os.environ["TEST_SRCDIR"], _CVC5_RLOC) - args += ["--verify", "--use-cvc5-binary", cvc5] elif mode == "output.brief": args += ["--no-lint", "--brief"] elif mode == "output.json": diff --git a/bazel/_private/partial_test.bzl b/bazel/_private/partial_test.bzl index 775b9a99..9c803289 100644 --- a/bazel/_private/partial_test.bzl +++ b/bazel/_private/partial_test.bzl @@ -15,7 +15,6 @@ Args forwarded via Bazel ``args`` to ``mode_test.py``: argv[1] root_dir "tests-large-partial" argv[2] test_dir plain string, e.g. "partial-1" - argv[3] cvc5_rloc $(rlocationpath //:cvc5) """ def trlc_partial_test(test_name): @@ -40,10 +39,9 @@ def trlc_partial_test(test_name): args = [ "tests-large-partial", test_name, - "$(rlocationpath //:cvc5)", ], deps = ["//trlc:trlc"], - data = list(srcs) + native.glob(["large/**"]) + ["//:cvc5", "//:coverage"], + data = list(srcs) + native.glob(["large/**"]) + ["//:coverage"], size = "large", ) diff --git a/bazel/_private/system_test.bzl b/bazel/_private/system_test.bzl index 4fe90b36..2d10174e 100644 --- a/bazel/_private/system_test.bzl +++ b/bazel/_private/system_test.bzl @@ -12,7 +12,6 @@ def trlc_system_test(test_dir): """ srcs = native.glob([test_dir + "/**"]) - # cvc5 binary is always included for tests with an output.smtlib golden file. # The "_test" suffix avoids a runfiles symlink collision with the source dir; # a test_suite alias under the plain name allows: bazel test //tests-system: test_target = test_dir + "_test" @@ -24,10 +23,9 @@ def trlc_system_test(test_dir): args = [ "tests-system", test_dir, - "$(rlocationpath //:cvc5)", ], deps = ["//trlc:trlc"], - data = list(srcs) + ["//:cvc5", "//:coverage"], + data = list(srcs) + ["//:coverage"], ) native.test_suite( diff --git a/cvc5.BUILD b/cvc5.BUILD deleted file mode 100644 index f85f2c56..00000000 --- a/cvc5.BUILD +++ /dev/null @@ -1,8 +0,0 @@ -filegroup( - name = "cvc5", - srcs = select({ - "@bazel_tools//src/conditions:windows": ["bin/cvc5.exe"], - "//conditions:default": ["bin/cvc5"], - }), - visibility = ["//visibility:public"], -) diff --git a/documentation/TUTORIAL-BAZEL.md b/documentation/TUTORIAL-BAZEL.md index 3b609b23..0db44f1c 100644 --- a/documentation/TUTORIAL-BAZEL.md +++ b/documentation/TUTORIAL-BAZEL.md @@ -18,8 +18,6 @@ load("@trlc//:trlc.bzl", "trlc_specification_test") ``` -It includes the pre-built CVC5 binary for Linux, macOS, and Windows. - --- ## Public API diff --git a/documentation/TUTORIAL-LINT.md b/documentation/TUTORIAL-LINT.md index 86c55931..25e630bd 100644 --- a/documentation/TUTORIAL-LINT.md +++ b/documentation/TUTORIAL-LINT.md @@ -16,13 +16,6 @@ feature. $ trlc --verify DIRECTORIES_OR_FILES ``` -If the API for CVC5 isn't avialable on your platform, then you can -also download the CVC5 executables and ask TRLC to use them directly: - -```bash -$ trlc --verify --use-cvc5-binary=path/to/cvc5.exe DIRECTORIES_OR_FILES -``` - ## Sanity checks The linter can detect some questionable constructs, for example: @@ -106,10 +99,9 @@ Verified 1 model(s) and 0 check(s) and found no issues ### Caveat -Please keep in mind two limitations with the `--verify` +Please keep in mind the following limitation with the `--verify` feature: -* It is harder to use and much slower on Windows * Under some circumstances the counter-examples generated are impossible to achieve, due to how the underlying technology (SMT Solvers) works. The current limitations are documented in the diff --git a/documentation/dev_setup.md b/documentation/dev_setup.md index d4b24cf1..c60f6af5 100644 --- a/documentation/dev_setup.md +++ b/documentation/dev_setup.md @@ -12,14 +12,8 @@ the latest GNU make version. can install this from your package manager. On Debian the package is called `python3`. -* You also need an executable `cvc5` binary on your PATH. Download the - appropriate version from - https://github.com/cvc5/cvc5/releases/tag/cvc5-1.3.2 and rename - it. You can also build CVC5 from source if there is no pre-built - release available for your platform. - -* You need to install the `cvc5` PyPI package, or build it from - source. +* You need to install the `cvc5` Python package (PyPI), or build it + from source. * You need to install everything from [requirements.txt](../requirements.txt). diff --git a/tests-system/Makefile b/tests-system/Makefile index ef9e06db..7797eefb 100644 --- a/tests-system/Makefile +++ b/tests-system/Makefile @@ -20,8 +20,7 @@ all: $(TARGETS) bulk/output bulk/output.brief bulk/output.json %/output.smtlib: -@coverage run -p --rcfile=../coverage.cfg --branch \ --data-file ../.coverage \ - ../trlc.py --verify --use-cvc5-binary=cvc5 \ - $(file < $(dir $@)options) \ + ../trlc.py --verify $(file < $(dir $@)options) \ $(dir $@) > $@ 2>&1 %/output.brief: diff --git a/tests-system/lint-vcg-decimal/output.smtlib b/tests-system/lint-vcg-decimal/output.smtlib index 46c55267..a338f53f 100644 --- a/tests-system/lint-vcg-decimal/output.smtlib +++ b/tests-system/lint-vcg-decimal/output.smtlib @@ -2,7 +2,7 @@ x, "potato" ^ lint-vcg-decimal/test1.rsl:12: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { -| a = -1.0 +| a = 1.0 | b = 0.0 | /* x is null */ | } diff --git a/trlc.bzl b/trlc.bzl index 5b923e75..c91e9fdf 100644 --- a/trlc.bzl +++ b/trlc.bzl @@ -27,7 +27,7 @@ def trlc_specification_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc ["$(locations %s)" % req for req in reqs], main = main, deps = ["@trlc//trlc:trlc"], - data = ["@trlc//:cvc5"] + reqs, + data = reqs, **kwargs ) @@ -76,7 +76,7 @@ def trlc_requirements_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc. ["$(locations %s)" % req for req in reqs], main = main, deps = ["@trlc//trlc:trlc"], - data = ["@trlc//:cvc5"] + reqs, + data = reqs, **kwargs ) diff --git a/trlc/lint.py b/trlc/lint.py index 3c96ce8a..9002cb86 100644 --- a/trlc/lint.py +++ b/trlc/lint.py @@ -24,19 +24,17 @@ class Linter: - def __init__(self, mh, stab, verify_checks, debug_vcg, cvc5_binary): + def __init__(self, mh, stab, verify_checks, debug_vcg): # lobster-exclude: Not safety relevant assert isinstance(mh, Message_Handler) assert isinstance(stab, ast.Symbol_Table) assert isinstance(verify_checks, bool) assert isinstance(debug_vcg, bool) - assert isinstance(cvc5_binary, str) or cvc5_binary is None self.mh = mh self.stab = stab self.verify_checks = verify_checks self.debug_vcg = debug_vcg - self.cvc5_binary = cvc5_binary self.abstract_extensions = {} self.checked_types = set() @@ -162,9 +160,7 @@ def verify_tuple_type(self, n_tuple_type): if self.verify_checks: vcg = VCG(mh = self.mh, n_ctyp = n_tuple_type, - debug = self.debug_vcg, - use_api = self.cvc5_binary is None, - cvc5_binary = self.cvc5_binary) + debug = self.debug_vcg) vcg.analyze() def verify_record_type(self, n_record_type): @@ -191,9 +187,7 @@ def verify_record_type(self, n_record_type): if self.verify_checks: vcg = VCG(mh = self.mh, n_ctyp = n_record_type, - debug = self.debug_vcg, - use_api = self.cvc5_binary is None, - cvc5_binary = self.cvc5_binary) + debug = self.debug_vcg) vcg.analyze() def verify_array_type(self, n_typ): diff --git a/trlc/trlc.py b/trlc/trlc.py index f4d64c6e..5d7f5dd8 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -22,7 +22,6 @@ import json import os import re -import subprocess import sys from fractions import Fraction @@ -77,14 +76,12 @@ def __init__(self, mh, parse_trlc = True, verify_mode = False, debug_vcg = False, - error_recovery = True, - cvc5_binary = None): + error_recovery = True): assert isinstance(mh, Message_Handler) assert isinstance(lint_mode, bool) assert isinstance(parse_trlc, bool) assert isinstance(verify_mode, bool) assert isinstance(debug_vcg, bool) - assert isinstance(cvc5_binary, str) or cvc5_binary is None self.mh = mh self.mh.sm = self @@ -102,7 +99,6 @@ def __init__(self, mh, self.verify_mode = verify_mode self.debug_vcg = debug_vcg self.error_recovery = error_recovery - self.cvc5_binary = cvc5_binary self.exclude_patterns = [] self.common_root = None @@ -512,8 +508,7 @@ def process(self): linter = lint.Linter(mh = self.mh, stab = self.stab, verify_checks = self.verify_mode, - debug_vcg = self.debug_vcg, - cvc5_binary = self.cvc5_binary) + debug_vcg = self.debug_vcg) ok &= linter.perform_sanity_checks() # Stop here if we're not processing TRLC files. if not self.parse_trlc: # pragma: no cover @@ -579,11 +574,6 @@ def trlc(): " checks. Does not yet support all language" " constructs. Requires PyVCG to be " " installed.")) - og_lint.add_argument("--use-cvc5-binary", - default=None, - help=("[EXPERIMENTAL] Drive the given CVC5 solver" - " with SMTLIB2 input instead of using the" - " API.")) og_input = ap.add_argument_group("input options") og_input.add_argument("--include-bazel-dirs", @@ -680,27 +670,9 @@ def trlc(): print(TRLC_VERSION) sys.exit(0) - if options.verify and not (options.use_cvc5_binary or - VCG_API_AVAILABLE): # pragma: no cover + if options.verify and not VCG_API_AVAILABLE: # pragma: no cover ap.error("The --verify option requires the optional dependency" - " CVC5 or use of the --use-cvc5-binary option") - - if options.use_cvc5_binary: # pragma: no cover - if not options.verify: - ap.error("The --use-cvc5-binary requires the --verify option") - try: - result = subprocess.run([options.use_cvc5_binary, - "--version"], - check = True, - capture_output = True, - encoding = "UTF-8") - if not result.stdout.startswith("This is cvc5"): - ap.error("selected binary does not appear to be CVC5") - except OSError as err: - ap.error("cannot run %s: %s" % (options.use_cvc5_binary, - str(err))) - except subprocess.CalledProcessError: - ap.error("cannot run %s" % options.use_cvc5_binary) + " CVC5") mh = Message_Handler(options.brief, not options.no_detailed_info, @@ -715,8 +687,7 @@ def trlc(): parse_trlc = not options.skip_trlc_files, verify_mode = options.verify, debug_vcg = options.debug_vcg, - error_recovery = not options.no_error_recovery, - cvc5_binary = options.use_cvc5_binary) + error_recovery = not options.no_error_recovery) if not options.include_bazel_dirs: # pragma: no cover sm.exclude_patterns.append(re.compile("^bazel-.*$")) diff --git a/trlc/vcg.py b/trlc/vcg.py index 488897ae..5eee6ec4 100644 --- a/trlc/vcg.py +++ b/trlc/vcg.py @@ -29,7 +29,6 @@ from pyvcg import graph from pyvcg import vcg from pyvcg.driver.file_smtlib import SMTLIB_Generator - from pyvcg.driver.cvc5_smtlib import CVC5_File_Solver VCG_AVAILABLE = True except ImportError: # pragma: no cover VCG_AVAILABLE = False @@ -73,19 +72,15 @@ def __init__(self, node, message, kind, expect_unsat=True): class VCG: # lobster-exclude: Not safety relevant - def __init__(self, mh, n_ctyp, debug, use_api=True, cvc5_binary=None): + def __init__(self, mh, n_ctyp, debug): assert VCG_AVAILABLE assert isinstance(mh, Message_Handler) assert isinstance(n_ctyp, Composite_Type) assert isinstance(debug, bool) - assert isinstance(use_api, bool) - assert use_api or isinstance(cvc5_binary, str) - self.mh = mh - self.n_ctyp = n_ctyp - self.debug = debug - self.use_api = use_api - self.cvc5_bin = cvc5_binary + self.mh = mh + self.n_ctyp = n_ctyp + self.debug = debug self.vc_name = "trlc-%s-%s" % (n_ctyp.n_package.name, n_ctyp.name) @@ -384,10 +379,7 @@ def checks_on_composite_type(self, n_ctyp): vc["feedback"] in nok_validity_checks: continue - if self.use_api: - solver = CVC5_Solver() - else: - solver = CVC5_File_Solver(self.cvc5_bin) + solver = CVC5_Solver() for name, value in CVC5_OPTIONS.items(): solver.set_solver_option(name, value) diff --git a/util/fetch_cvc5.py b/util/fetch_cvc5.py deleted file mode 100755 index f84e1648..00000000 --- a/util/fetch_cvc5.py +++ /dev/null @@ -1,78 +0,0 @@ -#!/usr/bin/env python3 -# -# TRLC - Treat Requirements Like Code -# Copyright (C) 2024 Florian Schanda -# -# This file is part of the TRLC Python Reference Implementation. -# -# TRLC is free software: you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# TRLC is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with TRLC. If not, see . - -# This utility script fetches and unpacks CVC5 binaries for use in CI. - -import os -import urllib.request -import io -import zipfile -import argparse -import stat - -CVC5_RELEASES = "http://github.com/cvc5/cvc5/releases/download" -CVC5_BINARY = "cvc5" -CVC5_EXECUTABLE = True - -# ----------------------------------------------------------------------- -# Canonical CVC5 binary version used throughout this project. -# Bump this together with: -# * The http_archive URLs/sha256 hashes in MODULE.bazel -# * The "cvc5>=" lower-bound in requirements.txt / requirements_dev.txt -# ----------------------------------------------------------------------- -CVC5_DEFAULT_VERSION = "1.3.2" - -ap = argparse.ArgumentParser() -ap.add_argument("--version", default=CVC5_DEFAULT_VERSION, - help="CVC5 release tag (default: %(default)s)") -ap.add_argument("platform") - -options = ap.parse_args() - -CVC5_VERSION = options.version - -if options.platform == "linux": - CVC5_PLATFORM = "Linux-x86_64-static" -elif options.platform == "osx14": - CVC5_PLATFORM = "macOS-arm64-static" -elif options.platform == "windows": - CVC5_PLATFORM = "Win64-x86_64-static" - CVC5_BINARY = "cvc5.exe" - CVC5_EXECUTABLE = False -else: - ap.error("unknown platform") - -print ("Downloading CVC5 archive (%s, %s)" % (CVC5_VERSION, CVC5_PLATFORM)) -with urllib.request.urlopen("%s/cvc5-%s/cvc5-%s.zip" % - (CVC5_RELEASES, - CVC5_VERSION, - CVC5_PLATFORM)) as fd: - content = fd.read() - -print ("Extracting %s" % CVC5_BINARY) -with zipfile.ZipFile(io.BytesIO(content)) as zf: - with zf.open("cvc5-%s/bin/%s" % (CVC5_PLATFORM, - CVC5_BINARY)) as fd: - with open(CVC5_BINARY, "wb") as fd_out: - fd_out.write(fd.read()) - -if CVC5_EXECUTABLE: - print("Setting executable bit") - os.chmod(CVC5_BINARY, stat.S_IRUSR | stat.S_IWUSR | stat.S_IXUSR)