Merge remote-tracking branch 'origin/master' into docker-tweaks

Author: jberthold

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.129"
+version = "0.3.130"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.129'
+VERSION: Final = '0.3.130'

kmir/src/kmir/rust/cargo.py

@@ -1,9 +1,21 @@
 from __future__ import annotations
 
 import json
+import logging
 import subprocess
 from functools import cached_property
 from pathlib import Path
+from typing import TYPE_CHECKING
+
+from pyk.utils import run_process_2
+
+if TYPE_CHECKING:
+    from typing import Any, Final
+
+_LOGGER: Final = logging.getLogger(__name__)
+_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+
+SMIR_JSON_DIR: Final = Path(__file__).parents[4] / 'deps/stable-mir-json/'
 
 
 class CargoProject:
@@ -80,3 +92,13 @@ def default_target(self) -> str:
             )
 
         return bin_targets[0]
+
+
+def cargo_get_smir_json(rs_file: Path) -> dict[str, Any]:
+    smir_json_result = SMIR_JSON_DIR / rs_file.with_suffix('.smir.json').name
+    run_process_2(['cargo', 'run', '--', '-Zno-codegen', str(rs_file)], cwd=SMIR_JSON_DIR)
+    json_smir = json.loads(smir_json_result.read_text())
+    _LOGGER.info(f'Loaded: {smir_json_result}')
+    smir_json_result.unlink()
+    _LOGGER.info(f'Deleted: {smir_json_result}')
+    return json_smir

kmir/src/tests/integration/data/prove-rs/arith.rs

@@ -0,0 +1,25 @@
+fn add(x: i32, y: i32) -> i32 {
+    x + y
+}
+
+fn sub(x: i32, y: i32) -> i32 {
+    x - y
+}
+
+fn mul(x: i32, y: i32) -> i32 {
+    x * y
+}
+
+fn div(x: i32, y: i32) -> i32 {
+    x / y
+}
+
+fn main() {
+    assert!(add(3, 4) == 7);
+
+    // assert!(sub(3, 4) == -1); // FAILING
+
+    assert!(mul(3, 4) == 12);
+
+    // assert!(div(12, 4) == 3); // FAILING
+}

kmir/src/tests/integration/data/prove-rs/assert-false-fail.rs

@@ -0,0 +1,3 @@
+fn main() {
+    assert!(false)
+}

kmir/src/tests/integration/data/prove-rs/assert-true.rs

@@ -0,0 +1,3 @@
+fn main() {
+    assert!(true)
+}

kmir/src/tests/integration/data/prove-rs/cmp.rs

@@ -0,0 +1,47 @@
+fn cmp_lt(x: i32, y: i32) -> bool {
+    x < y
+}
+
+fn cmp_le(x: i32, y: i32) -> bool {
+    x <= y
+}
+
+fn cmp_gt(x: i32, y: i32) -> bool {
+    x > y
+}
+
+fn cmp_ge(x: i32, y: i32) -> bool {
+    x >= y
+}
+
+fn cmp_eq(x: i32, y: i32) -> bool {
+    x == y
+}
+
+fn cmp_neq(x: i32, y: i32) -> bool {
+    x != y
+}
+
+fn main() {
+    assert!( cmp_lt(3, 4));
+    assert!(!cmp_lt(4, 3));
+    assert!(!cmp_lt(4, 4));
+
+    assert!( cmp_le(3, 4));
+    assert!(!cmp_le(4, 3));
+    assert!( cmp_le(4, 4));
+
+    assert!(!cmp_gt(3, 4));
+    assert!( cmp_gt(4, 3));
+    assert!(!cmp_gt(4, 4));
+
+    assert!(!cmp_ge(3, 4));
+    assert!( cmp_ge(4, 3));
+    assert!( cmp_ge(4, 4));
+
+    assert!(!cmp_eq(4, 3));
+    assert!( cmp_eq(4, 4));
+
+    assert!( cmp_neq(4, 3));
+    assert!(!cmp_neq(4, 4));
+}

kmir/src/tests/integration/data/prove-rs/else.rs

@@ -0,0 +1,11 @@
+fn ite(flag: bool) {
+    if flag {
+        assert!(false)
+    } else {
+        assert!(true)
+    }
+}
+
+fn main() {
+    ite(false)
+}

kmir/src/tests/integration/data/prove-rs/if.rs

@@ -0,0 +1,11 @@
+fn ite(flag: bool) {
+    if flag {
+        assert!(true)
+    } else {
+        assert!(false)
+    }
+}
+
+fn main() {
+    ite(true)
+}

kmir/src/tests/integration/test_prove_rs.py

@@ -0,0 +1,57 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+import pytest
+from pyk.cterm import CTerm
+from pyk.kast.inner import KInner, Subst
+from pyk.kast.manip import split_config_from
+from pyk.kcfg import KCFG
+from pyk.proof.reachability import APRProof, APRProver
+
+from kmir.kmir import KMIR
+from kmir.parse.parser import Parser
+from kmir.rust.cargo import cargo_get_smir_json
+
+if TYPE_CHECKING:
+    from kmir.tools import Tools
+
+
+PROVING_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
+PROVING_FILES = list(PROVING_DIR.glob('*.rs'))
+
+
+@pytest.mark.parametrize(
+    'rs_file',
+    PROVING_FILES,
+    ids=[spec.stem for spec in PROVING_FILES],
+)
+def test_prove_rs(rs_file: Path, tmp_path: Path, kmir: KMIR, tools: Tools) -> None:
+    should_fail = rs_file.stem.endswith('fail')
+    smir_json = cargo_get_smir_json(rs_file)
+
+    parser = Parser(kmir.definition)
+    parse_result = parser.parse_mir_json(smir_json, 'Pgm')
+    assert parse_result is not None
+    kmir_kast, _ = parse_result
+    assert isinstance(kmir_kast, KInner)
+
+    config = tools.make_init_config(kmir_kast, 'main')
+    config_with_cell_vars, _ = split_config_from(config)
+
+    lhs = CTerm(config)
+
+    rhs_subst = Subst({'K_CELL': KMIR.Symbols.END_PROGRAM})
+    rhs = CTerm(rhs_subst(config_with_cell_vars))
+    kcfg = KCFG()
+    init_node = kcfg.create_node(lhs)
+    target_node = kcfg.create_node(rhs)
+    apr_proof = APRProof('PROOF', kcfg, [], init_node.id, target_node.id, {})
+    with kmir.kcfg_explore('PROOF-TEST') as kcfg_explore:
+        prover = APRProver(kcfg_explore)
+        prover.advance_proof(apr_proof)
+        if not should_fail:
+            assert apr_proof.passed
+        else:
+            assert apr_proof.failed