Allow --temp-dir option for test-prove (#77)

- Introduced a `--temp-dir <debug-dir-path>` option to save temporary
files in a debug directory.
- Enhanced the `test_specs` function to write proof results to a file in
the temp directory.

---------

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: devops <devops@runtimeverification.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.58
+0.1.59

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.58"
+version = "0.1.59"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

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

@@ -3,7 +3,7 @@ requires "riscv-semantics/riscv.md"
 module ADD-SPEC
   imports RISCV
 
-  claim [add]:
+  claim [id]:
     <instrs> (.K => #HALT) ~> #EXECUTE ... </instrs>
     <regs>
       1 |-> X

src/tests/integration/test_prove.py

@@ -5,6 +5,7 @@
 
 import pytest
 from pyk.proof import ProofStatus
+from pyk.proof.show import APRProofShow
 
 from kriscv.symtools import SymTools
 
@@ -16,6 +17,7 @@
 
 
 SPEC_DIR: Final = TEST_DATA_DIR / 'specs'
+SPEC_TESTS: Final = list(SPEC_DIR.glob('*.k'))
 
 
 @dataclass
@@ -31,28 +33,40 @@ def __call__(self, file_name: str) -> Path:
 
 
 @pytest.fixture
-def load_spec(tmp_path: Path) -> SpecLoader:
-    return SpecLoader(temp_dir=tmp_path)
+def load_spec(temp_dir: Path) -> SpecLoader:
+    return SpecLoader(temp_dir=temp_dir)
 
 
 @pytest.fixture
-def symtools(tmp_path: Path) -> SymTools:
-    return SymTools.default(proof_dir=tmp_path)
+def symtools(temp_dir: Path) -> SymTools:
+    return SymTools.default(proof_dir=temp_dir, bug_report=temp_dir / 'bug-reports')
 
 
-def test_add(
+@pytest.mark.parametrize(
+    'spec_file',
+    SPEC_TESTS,
+    ids=[str(test.relative_to(SPEC_DIR)) for test in SPEC_TESTS],
+)
+def test_specs(
     load_spec: SpecLoader,
     symtools: SymTools,
+    temp_dir: Path,
+    spec_file: Path,
 ) -> None:
     # Given
-    spec_file = load_spec('add-spec.k')
+    spec_file = load_spec(spec_file.name)
 
     # When
     proof = symtools.prove(
         spec_file=spec_file,
-        spec_module='ADD-SPEC',
-        claim_id='ADD-SPEC.add',
+        spec_module=spec_file.stem.upper(),
+        claim_id=f'{spec_file.stem.upper()}.id',
+        max_depth=1000,
     )
 
+    proof_show_file = temp_dir / f'{spec_file.stem}-proof.txt'
+    proof_show_lines = APRProofShow(symtools.kprove).show(proof, nodes=[node.id for node in proof.kcfg.nodes])
+    proof_show_file.write_text('\n'.join(proof_show_lines))
+
     # Then
-    assert proof.status == ProofStatus.PASSED
+    assert proof.status == ProofStatus.PASSED, f'Proof failed: {proof.failure_info}'