Add CLI option that disables verification cache

This also adds model verification caching to the validator.

Ref. eng/recordflux/RecordFlux#1488

CHANGELOG.md

@@ -10,6 +10,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 
 - Pragma marking all generated files as Ada 2012 (eng/recordflux/RecordFlux#1509, AdaCore/RecordFlux#1293)
+- `--no-caching` option to `rflx` (eng/recordflux/RecordFlux#1488)
+- Model verification caching to validator
 
 ### Fixed
 

doc/user_guide/90-rflx--help.txt

@@ -1,5 +1,5 @@
-usage: rflx [-h] [-q] [--version] [--no-verification] [--max-errors NUM]
-            [--workers NUM] [--unsafe]
+usage: rflx [-h] [-q] [--version] [--no-caching] [--no-verification]
+            [--max-errors NUM] [--workers NUM] [--unsafe]
             {check,generate,graph,validate,install,convert,run_ls} ...
 
 positional arguments:
@@ -18,6 +18,7 @@ options:
   -h, --help            show this help message and exit
   -q, --quiet           disable logging to standard output
   --version
+  --no-caching          ignore verification cache
   --no-verification     skip time-consuming verification of model
   --max-errors NUM      exit after at most NUM errors
   --workers NUM         parallelize proofs among NUM workers (default: NPROC)

examples/apps/ping/ping.py

@@ -9,6 +9,7 @@
 import sys
 import time
 
+from rflx.model import NeverVerify
 from rflx.pyrflx import MessageValue, PyRFLX, utils
 
 
@@ -33,7 +34,7 @@ def icmp_checksum(message: bytes, **kwargs: object) -> int:
     return utils.internet_checksum(checksum_bytes)
 
 
-PYRFLX = PyRFLX.from_specs(["specs/ipv4.rflx"], skip_model_verification=True)
+PYRFLX = PyRFLX.from_specs(["specs/ipv4.rflx"], NeverVerify())
 ICMP = PYRFLX.package("ICMP")
 ICMP.set_checksum_functions({"Message": {"Checksum": icmp_checksum}})
 IP = PYRFLX.package("IPv4")

rflx/cli.py

@@ -35,7 +35,7 @@
 from rflx.identifier import ID
 from rflx.integration import Integration
 from rflx.ls.server import server
-from rflx.model import Message, Model, Session
+from rflx.model import AlwaysVerify, Cache, Message, Model, NeverVerify, Session
 from rflx.pyrflx import PyRFLXError
 from rflx.specification import Parser
 from rflx.validator import ValidationError, Validator
@@ -139,6 +139,11 @@ def main(  # noqa: PLR0915
         help="disable logging to standard output",
     )
     parser.add_argument("--version", action="store_true")
+    parser.add_argument(
+        "--no-caching",
+        action="store_true",
+        help=("ignore verification cache"),
+    )
     parser.add_argument(
         "--no-verification",
         action="store_true",
@@ -483,7 +488,7 @@ def __init__(self, string: str) -> None:
 
 
 def check(args: argparse.Namespace) -> None:
-    parse(args.files, args.no_verification, args.workers)
+    parse(args.files, args.no_caching, args.no_verification, args.workers)
 
 
 def generate(args: argparse.Namespace) -> None:
@@ -498,6 +503,7 @@ def generate(args: argparse.Namespace) -> None:
 
     model, integration = parse(
         args.files,
+        args.no_caching,
         args.no_verification,
         args.workers,
         args.integration_files_dir,
@@ -524,13 +530,13 @@ def generate(args: argparse.Namespace) -> None:
 
 def parse(
     files: Sequence[Path],
-    skip_verification: bool = False,
+    no_caching: bool,
+    no_verification: bool,
     workers: int = 1,
     integration_files_dir: Optional[Path] = None,
 ) -> tuple[Model, Integration]:
     parser = Parser(
-        skip_verification,
-        cached=True,
+        cache(no_caching, no_verification),
         workers=workers,
         integration_files_dir=integration_files_dir,
     )
@@ -562,7 +568,7 @@ def graph(args: argparse.Namespace) -> None:
     if not args.output_directory.is_dir():
         fail(f'directory not found: "{args.output_directory}"', Subsystem.CLI)
 
-    model, _ = parse(args.files, args.no_verification)
+    model, _ = parse(args.files, args.no_caching, args.no_verification)
 
     for d in model.declarations:
         filename = args.output_directory.joinpath(d.identifier.flat).with_suffix(f".{args.format}")
@@ -599,7 +605,7 @@ def validate(args: argparse.Namespace) -> None:
         Validator(
             [args.specification],
             args.checksum_module,
-            args.no_verification,
+            cache(args.no_caching, args.no_verification),
             split_disjunctions=args.split_disjunctions,
         ).validate(
             identifier,
@@ -657,3 +663,7 @@ def vscode_extension() -> Traversable:
     path = importlib_resources.files("rflx_ide") / "vscode" / "recordflux.vsix"
     assert isinstance(path, Traversable)
     return path
+
+
+def cache(no_caching: bool, no_verification: bool) -> Cache:
+    return NeverVerify() if no_verification else (AlwaysVerify() if no_caching else Cache())

rflx/ls/server.py

@@ -141,7 +141,7 @@ def update(self, document_uri: str) -> None:
         document_path = Path(unquote(urlparse(document_uri).path))
         directory = document_path.parent
         workspace_files = self._workspace_files()
-        parser = Parser(cached=True, workers=self.workers)
+        parser = Parser(self._cache, workers=self.workers)
 
         self._error = error.RecordFluxError()
 

rflx/model/__init__.py

@@ -1,4 +1,9 @@
-from .cache import Cache as Cache, Digest as Digest
+from .cache import (
+    AlwaysVerify as AlwaysVerify,
+    Cache as Cache,
+    Digest as Digest,
+    NeverVerify as NeverVerify,
+)
 from .message import (
     FINAL as FINAL,
     INITIAL as INITIAL,

rflx/model/cache.py

@@ -24,27 +24,17 @@ class Cache:
     verified. The state of the cache is persisted on disk and restored on initialization.
     """
 
-    def __init__(self, file: Path = DEFAULT_FILE, enabled: bool = True) -> None:
+    def __init__(self, file: Path = DEFAULT_FILE) -> None:
         self._file = file
-        self._enabled = enabled
-
-        if not enabled:
-            return
 
         self._verified: dict[str, list[str]] = {}
 
         self._load_cache()
 
     def is_verified(self, digest: Digest) -> bool:
-        if not self._enabled:
-            return False
-
         return digest.key in self._verified and digest.value in self._verified[digest.key]
 
     def add_verified(self, digest: Digest) -> None:
-        if not self._enabled:
-            return
-
         if not digest.value:
             return
 
@@ -78,6 +68,28 @@ def _write_cache(self) -> None:
             json.dump(self._verified, f)
 
 
+class AlwaysVerify(Cache):
+    def __init__(self) -> None:
+        pass
+
+    def is_verified(self, digest: Digest) -> bool:  # noqa: ARG002
+        return False
+
+    def add_verified(self, digest: Digest) -> None:
+        pass
+
+
+class NeverVerify(Cache):
+    def __init__(self) -> None:
+        warn("model verification skipped", Subsystem.MODEL)
+
+    def is_verified(self, digest: Digest) -> bool:  # noqa: ARG002
+        return True
+
+    def add_verified(self, digest: Digest) -> None:
+        pass
+
+
 class Digest:
     def __init__(self, declaration: TopLevelDeclaration) -> None:
         components = _digest_components(declaration)

rflx/model/model.py

@@ -27,7 +27,6 @@ class UncheckedModel(Base):
     def checked(
         self,
         cache: Cache,
-        skip_verification: bool = False,
         workers: int = 1,
     ) -> Model:
         error = RecordFluxError(self.error)
@@ -40,7 +39,7 @@ def checked(
                 digest = Digest(unverified)
                 checked = (
                     unverified
-                    if skip_verification or cache.is_verified(digest)
+                    if cache.is_verified(digest)
                     else d.checked(declarations, workers=workers)
                 )
                 declarations.append(checked)

rflx/pyrflx/pyrflx.py

@@ -7,7 +7,7 @@
 
 from rflx.error import FatalError
 from rflx.identifier import ID, StrID
-from rflx.model import Model
+from rflx.model import Cache, Model
 from rflx.specification import Parser
 
 from .error import PyRFLXError
@@ -46,14 +46,14 @@ def __init__(
     def from_specs(
         cls,
         files: Iterable[Union[str, Path]],
-        skip_model_verification: bool = False,
+        cache: Optional[Cache] = None,
         skip_message_verification: bool = False,
     ) -> PyRFLX:
         paths = list(map(Path, files))
         for p in paths:
             if not p.is_file():
                 raise FileNotFoundError(f'file not found: "{p}"')
-        parser = Parser(skip_model_verification)
+        parser = Parser(cache)
         parser.parse(*paths)
         model = parser.create_model()
         return cls(model, None, skip_message_verification)

rflx/specification/parser.py

@@ -13,10 +13,10 @@
 import rflx.typing_ as rty
 from rflx import expression as expr, model
 from rflx.common import STDIN, unique
-from rflx.error import Location, RecordFluxError, Severity, Subsystem, fail, warn
+from rflx.error import Location, RecordFluxError, Severity, Subsystem, fail
 from rflx.identifier import ID, StrID
 from rflx.integration import Integration
-from rflx.model import Cache, declaration as decl, statement as stmt
+from rflx.model import AlwaysVerify, Cache, declaration as decl, statement as stmt
 from rflx.specification.const import RESERVED_WORDS
 
 from . import style
@@ -1609,18 +1609,14 @@ def package(self) -> ID:
 class Parser:
     def __init__(
         self,
-        skip_verification: bool = False,
-        cached: bool = False,
+        cache: Optional[Cache] = None,
         workers: int = 1,
         integration_files_dir: Optional[Path] = None,
     ) -> None:
-        if skip_verification:
-            warn("model verification skipped", Subsystem.MODEL)
-        self.skip_verification = skip_verification
+        self._cache = AlwaysVerify() if cache is None else cache
         self._workers = workers
         self._specifications: OrderedDict[ID, SpecificationFile] = OrderedDict()
         self._integration: Integration = Integration(integration_files_dir)
-        self._cache = Cache(enabled=not skip_verification and cached)
 
     def parse(self, *specfiles: Path) -> None:
         error = RecordFluxError()
@@ -1696,7 +1692,10 @@ def create_unchecked_model(self) -> model.UncheckedModel:
     def create_model(self) -> model.Model:
         unchecked_model = self.create_unchecked_model()
         error = unchecked_model.error
-        checked_model = unchecked_model.checked(self._cache, self.skip_verification, self._workers)
+        checked_model = unchecked_model.checked(
+            self._cache,
+            self._workers,
+        )
         self._integration.validate(checked_model, error)
         error.propagate()
         return checked_model

rflx/validator.py

@@ -14,7 +14,7 @@
 
 from rflx import expression as expr
 from rflx.identifier import ID, StrID
-from rflx.model import Link, Message, Model, Refinement, type_ as mty
+from rflx.model import AlwaysVerify, Cache, Link, Message, Model, Refinement, type_ as mty
 from rflx.pyrflx import ChecksumFunction, Package, PyRFLX, PyRFLXError
 from rflx.pyrflx.typevalue import MessageValue
 from rflx.specification import Parser
@@ -25,13 +25,13 @@ def __init__(
         self,
         files: Iterable[Union[str, Path]],
         checksum_module: Optional[str] = None,
-        skip_model_verification: bool = False,
+        cache: Optional[Cache] = None,
         skip_message_verification: bool = False,
         split_disjunctions: bool = False,
     ):
         model = self._create_model(
             [Path(f) for f in files],
-            skip_model_verification,
+            AlwaysVerify() if cache is None else cache,
             split_disjunctions,
         )
         checksum_functions = self._parse_checksum_module(checksum_module)
@@ -177,13 +177,13 @@ def _check_arguments(
     def _create_model(
         self,
         files: Sequence[Path],
-        skip_model_verification: bool,
+        cache: Cache,
         split_disjunctions: bool,
     ) -> Model:
         for f in files:
             if not f.is_file():
                 raise ValidationError(f'specification file not found: "{f}"')
-        parser = Parser(skip_model_verification)
+        parser = Parser(cache)
         parser.parse(*files)
         model = parser.create_model()
         if split_disjunctions:

tests/data/fixtures/pyrflx.py

@@ -31,7 +31,7 @@ def fixture_pyrflx() -> pyrflx.PyRFLX:
             f"{SPEC_DIR}/low_order.rflx",
             f"{SPEC_DIR}/aggregate_in_relation.rflx",
         ],
-        skip_model_verification=True,
+        model.NeverVerify(),
     )
 
 

tests/examples/specs_test.py

@@ -7,6 +7,7 @@
 import pytest
 
 from rflx.converter import iana
+from rflx.model import NeverVerify
 from rflx.validator import Validator
 from tests.const import EX_SPEC_DIR
 
@@ -16,9 +17,8 @@
 
 @pytest.mark.parametrize("spec", EX_SPEC_DIR.glob("*.rflx"))
 def test_spec(spec: Path, tmp_path: Path) -> None:
-    # TODO(eng/recordflux/RecordFlux#1485): Ensure reproducible test results by disabling caching
     subprocess.run(
-        ["rflx", "generate", "--ignore-unsupported-checksum", "-d", tmp_path, spec],
+        ["rflx", "--no-caching", "generate", "--ignore-unsupported-checksum", "-d", tmp_path, spec],
         check=True,
     )
     subprocess.run(["gprbuild", "-U", "-j0"], check=True, cwd=tmp_path)
@@ -42,7 +42,7 @@ def test_iana_specs_synchronized(registry_file: Path) -> None:
 
 @pytest.mark.parametrize("spec", EX_SPEC_DIR.glob("*.rflx"))
 def test_validate_spec(spec: Path) -> None:
-    validator = Validator([spec], "examples.specs.checksum", skip_model_verification=True)
+    validator = Validator([spec], "examples.specs.checksum", NeverVerify())
 
     # Eng/RecordFlux/RecordFlux#833
     for package in validator._pyrflx:  # noqa: SLF001

tests/integration/cli_test.py

@@ -59,4 +59,4 @@ def test_parse_no_subsequent_errors_caused_by_style_errors(tmp_path: Path) -> No
             r"$"
         ),
     ):
-        cli.parse([a])
+        cli.parse([a], no_caching=True, no_verification=False)

tests/integration/pyrflx_test.py

@@ -26,6 +26,7 @@
 )
 from rflx.identifier import ID
 from rflx.model import FINAL, Link, Message
+from rflx.model.cache import NeverVerify
 from rflx.model.message import INITIAL, Field
 from rflx.model.model import Model
 from rflx.model.type_ import OPAQUE
@@ -265,7 +266,7 @@ def test_no_verification_ethernet(ethernet_frame_value: MessageValue) -> None:
     assert ethernet_frame_value.valid_message
     pyrflx_ = PyRFLX.from_specs(
         [SPEC_DIR / "ethernet.rflx"],
-        skip_model_verification=True,
+        NeverVerify(),
         skip_message_verification=True,
     )
     frame_unv = pyrflx_.package("Ethernet").new_message("Frame")
@@ -293,7 +294,7 @@ def test_no_verification_sequence_nested_messages(
 
     pyrflx_ = PyRFLX.from_specs(
         [SPEC_DIR / "sequence_message.rflx"],
-        skip_model_verification=True,
+        NeverVerify(),
         skip_message_verification=True,
     )
     sequence_message_package_unv = pyrflx_.package("Sequence_Message")