Add symbolic execution support (#67)

Co-authored-by: Copilot <[email protected]>
Co-authored-by: devops <[email protected]>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.53
+0.1.54

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.53"
+version = "0.1.54"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kriscv/kdist/plugin.py

@@ -8,7 +8,7 @@
 from pyk.kbuild.utils import k_version
 from pyk.kdist.api import Target
 from pyk.kllvm.compiler import compile_kllvm, compile_runtime
-from pyk.ktool.kompile import kompile
+from pyk.ktool.kompile import LLVMKompileType, PykBackend, kompile
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Mapping
@@ -84,6 +84,26 @@ def context(self) -> dict[str, str]:
             'warnings_to_errors': True,
         },
     ),
+    'llvm-lib': KompileTarget(
+        lambda src_dir: {
+            'main_file': src_dir / 'riscv-semantics/riscv.md',
+            'include_dirs': [src_dir],
+            'syntax_module': 'RISCV',
+            'llvm_kompile_type': LLVMKompileType.C,
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
+    'haskell': KompileTarget(
+        lambda src_dir: {
+            'main_file': src_dir / 'riscv-semantics/riscv.md',
+            'backend': PykBackend.HASKELL,
+            'include_dirs': [src_dir],
+            'syntax_module': 'RISCV',
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
     'func-test': KompileTarget(
         lambda src_dir: {
             'main_file': src_dir / 'riscv-semantics/func-test.md',

src/kriscv/kdist/riscv-semantics/riscv.md

@@ -50,7 +50,7 @@ As we do not model the surrounding environment, for testing purposes we add our
 This is done with three components:
 - A `HaltCondition` value stored in the configuation indicating under which conditions we should halt.
 - A `#CHECK_HALT` operation indicating that the halt condition should be checked.
-- A `#HALT` operation which terminates the simulation by consuming all following operations in the pipeline without executing them.
+- A `#HALT` operation which terminates the simulation by not matching any semantic rule.
 ```k
 module RISCV-TERMINATION
   imports RISCV-CONFIGURATION
@@ -61,8 +61,6 @@ module RISCV-TERMINATION
       "#HALT"
     | "#CHECK_HALT"
 
-  rule <instrs> #HALT ~> (_ => .K) ...</instrs>
-
   syntax HaltCondition ::=
       "NEVER"                [symbol(HaltNever)]
     | "ADDRESS" "(" Word ")" [symbol(HaltAtAddress)]

src/kriscv/symtools.py

@@ -0,0 +1,101 @@
+from __future__ import annotations
+
+from contextlib import contextmanager
+from dataclasses import dataclass
+from functools import cached_property
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+from pyk.cterm.symbolic import CTermSymbolic
+from pyk.kcfg.explore import KCFGExplore
+from pyk.ktool.kprove import KProve
+from pyk.proof.reachability import APRProof
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable, Iterator
+
+
+@dataclass
+class SymTools:
+    haskell_dir: Path
+    llvm_lib_dir: Path
+    proof_dir: Path
+    source_dirs: tuple[Path, ...]
+
+    @staticmethod
+    def default(*, proof_dir: Path) -> SymTools:
+        from pyk.kdist import kdist
+
+        return SymTools(
+            haskell_dir=kdist.get('riscv-semantics.haskell'),
+            llvm_lib_dir=kdist.get('riscv-semantics.llvm-lib'),
+            source_dirs=(kdist.get('riscv-semantics.source'),),
+            proof_dir=proof_dir,
+        )
+
+    @cached_property
+    def kprove(self) -> KProve:
+        return KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir)
+
+    @contextmanager
+    def explore(self, *, id: str) -> Iterator[KCFGExplore]:
+        from pyk.kore.rpc import BoosterServer, KoreClient
+
+        with BoosterServer(
+            {
+                'kompiled_dir': self.haskell_dir,
+                'llvm_kompiled_dir': self.llvm_lib_dir,
+                'module_name': self.kprove.main_module,
+            }
+        ) as server:
+            with KoreClient('localhost', server.port) as client:
+                cterm_symbolic = CTermSymbolic(
+                    kore_client=client,
+                    definition=self.kprove.definition,
+                )
+                yield KCFGExplore(
+                    id=id,
+                    cterm_symbolic=cterm_symbolic,
+                )
+
+    def prove(
+        self,
+        *,
+        spec_file: str | Path,
+        spec_module: str,
+        claim_id: str,
+        reinit: bool | None = None,
+        max_depth: int | None = None,
+        max_iterations: int | None = None,
+        includes: Iterable[str | Path] | None = None,
+    ) -> APRProof:
+        from pyk.ktool.claim_loader import ClaimLoader
+        from pyk.proof.reachability import APRProver
+
+        spec_file = Path(spec_file)
+        include_dirs = self.source_dirs + (tuple(Path(include) for include in includes) if includes is not None else ())
+
+        claims = ClaimLoader(self.kprove).load_claims(
+            spec_file=spec_file,
+            spec_module_name=spec_module,
+            claim_labels=[claim_id],
+            include_dirs=include_dirs,
+        )
+        (claim,) = claims
+        spec_label = f'{spec_module}.{claim_id}'
+
+        if not reinit and APRProof.proof_data_exists(spec_label, self.proof_dir):
+            # load an existing proof (to continue work on it)
+            proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
+        else:
+            # ignore existing proof data and reinitialize it from a claim
+            proof = APRProof.from_claim(self.kprove.definition, claim=claim, logs={}, proof_dir=self.proof_dir)
+
+        with self.explore(id=spec_label) as kcfg_explore:
+            prover = APRProver(
+                kcfg_explore=kcfg_explore,
+                execute_depth=max_depth,
+            )
+            prover.advance_proof(proof, max_iterations=max_iterations)
+
+        return proof

src/tests/integration/test-data/specs/add-spec.k

@@ -0,0 +1,21 @@
+requires "riscv-semantics/riscv.md"
+
+module ADD-SPEC
+  imports RISCV
+
+  claim [add]:
+    <instrs> (.K => #HALT) ~> #EXECUTE ... </instrs>
+    <regs>
+      1 |-> X
+      2 |-> Y
+      3 |-> (_ => Y +Word X)
+    </regs>
+    <pc> W ( 0 => 4 ) </pc>
+    <mem>
+      #bytes ( b"\xb3\x01\x11\x00" )  // add x3, x2, x1
+      .SparseBytes
+    </mem>
+    <test>
+      <haltCond> ADDRESS ( W ( 4 ) ) </haltCond>
+    </test>
+endmodule

src/tests/integration/test_prove.py

@@ -0,0 +1,58 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TYPE_CHECKING
+
+import pytest
+from pyk.proof import ProofStatus
+
+from kriscv.symtools import SymTools
+
+from .utils import TEST_DATA_DIR
+
+if TYPE_CHECKING:
+    from pathlib import Path
+    from typing import Final
+
+
+SPEC_DIR: Final = TEST_DATA_DIR / 'specs'
+
+
+@dataclass
+class SpecLoader:
+    temp_dir: Path
+
+    def __call__(self, file_name: str) -> Path:
+        import shutil
+
+        res = self.temp_dir / file_name
+        shutil.copy(SPEC_DIR / file_name, res)
+        return res
+
+
+@pytest.fixture
+def load_spec(tmp_path: Path) -> SpecLoader:
+    return SpecLoader(temp_dir=tmp_path)
+
+
+@pytest.fixture
+def symtools(tmp_path: Path) -> SymTools:
+    return SymTools.default(proof_dir=tmp_path)
+
+
+def test_add(
+    load_spec: SpecLoader,
+    symtools: SymTools,
+) -> None:
+    # Given
+    spec_file = load_spec('add-spec.k')
+
+    # When
+    proof = symtools.prove(
+        spec_file=spec_file,
+        spec_module='ADD-SPEC',
+        claim_id='ADD-SPEC.add',
+    )
+
+    # Then
+    assert proof.status == ProofStatus.PASSED

src/tests/integration/utils.py

@@ -0,0 +1,10 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from typing import Final
+
+
+TEST_DATA_DIR: Final = Path(__file__).parent / 'test-data'