Included #panic and #internalPanic in terminal rules. (#281)

* Included `#panic` and `#internalPanic` in terminal rules. This stops the verifier from potentially infinitely spinning on panics. * Set Version: 0.2.5 * replacing elif * added labels for panic rules * `advance_proof` correctly references `KMIRSemantics.terminal_rules()` * Added `cut_point_rules` (currently empty) as arg * Set Version: 0.2.6 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Dec 7, 2023 · 61ecb79 · 61ecb79
1 parent 4faa989
commit 61ecb79
Show file tree

Hide file tree

Showing 8 changed files with 31 additions and 16 deletions.
diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md
@@ -702,7 +702,7 @@ module MIR-FINALIZATION
 These are internal panics that are specific to KMIR.
 
 ```k
-  rule <k> #internalPanic(_FN_KEY, _PANIC, _MSG) ~> (_ITEM:KItem => .K) ... </k>
+  rule [iPanic]: <k> #internalPanic(_FN_KEY, _PANIC, _MSG) ~> (_ITEM:KItem => .K) ... </k>
        <returncode> 4 => 1 </returncode>
 ```
 
@@ -711,9 +711,7 @@ These are internal panics that are specific to KMIR.
 These panics are not specific to KMIR and caused by program-level reasons, i.e. assertion violations.
 
 ```k
-  rule <k> #panic(_FN_KEY, _PANIC, _MSG) ~> (_ITEM:KItem => .K) ... </k>
-       <returncode> 4 => 2 </returncode>
-  rule <k> #panic(_FN_KEY, _PANIC, _MSG) ... </k>
+  rule [panic]: <k> #panic(_FN_KEY, _PANIC, _MSG) ~> (_ITEM:KItem => .K) ... </k>
        <returncode> 4 => 2 </returncode>
 ```
 

diff --git a/kmir/poetry.lock b/kmir/poetry.lock
diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.2.5"
+version = "0.2.6"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
@@ -2,4 +2,4 @@
 
 from .kmir import KMIR
 
-VERSION: Final = '0.2.5'
+VERSION: Final = '0.2.6'
diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
@@ -213,6 +213,7 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                 proof_problem,
                 kcfg_explore,
                 max_depth=depth,
+                terminal_rules=KMIRSemantics.terminal_rules(),
             )
             failure_log = None
             if not passed:

diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py
@@ -12,7 +12,7 @@
 
 from pyk.cli.utils import check_dir_path, check_file_path
 from pyk.cterm import CTerm
-from pyk.kast.inner import KApply, KInner, KSequence, KVariable
+from pyk.kast.inner import KApply, KInner, KLabel, KSequence, KVariable
 from pyk.kcfg.semantics import KCFGSemantics
 from pyk.ktool.kprint import KAstInput, KAstOutput, _kast, gen_glr_parser
 from pyk.ktool.kprove import KProve
@@ -29,24 +29,27 @@ class KMIRSemantics(KCFGSemantics):
     def is_terminal(self, cterm: CTerm) -> bool:
         k_cell = cterm.cell('K_CELL')
         # <k> #halt </k>
-        if k_cell == KMIR.halt():
+        if k_cell == KMIR.halt() or KMIR.is_panic(k_cell):
             return True
         elif type(k_cell) is KSequence:
             # <k> . </k>
             if k_cell.arity == 0:
                 return True
             # <k> #halt </k>
-            elif k_cell.arity == 1 and k_cell[0] == KMIR.halt():
+            elif k_cell.arity == 1 and (k_cell[0] == KMIR.halt() or KMIR.is_panic(k_cell[0])):
                 return True
             elif (
-                k_cell.arity == 2 and k_cell[0] == KMIR.halt() and type(k_cell[1]) is KVariable and k_cell[1].sort == K
+                k_cell.arity == 2
+                and (k_cell[0] == KMIR.halt() or KMIR.is_panic(k_cell[0]))
+                and type(k_cell[1]) is KVariable
+                and k_cell[1].sort == K
             ):
                 return True
         return False
 
     @staticmethod
     def terminal_rules() -> list[str]:
-        terminal_rules = ['MIR.halt']
+        terminal_rules = ['MIR.halt', 'MIR.panic', 'MIR.iPanic']
 
         # TODO: break every step and add to terminal rules. Semantics does not support this currently
         return terminal_rules
@@ -212,3 +215,17 @@ def preprocess_and_run(program_file: Path, temp_file: Path) -> CompletedProcess:
     @staticmethod
     def halt() -> KApply:
         return KApply('#halt_MIR_KItem')
+
+    @staticmethod
+    def panic_label() -> KLabel:
+        return KLabel('#panic(_,_,_)_PANICS_KItem_FunctionLikeKey_Panic_KItem')
+
+    @staticmethod
+    def internal_panic_label() -> KLabel:
+        return KLabel('#internalPanic(_,_,_)_PANICS_KItem_FunctionLikeKey_InternalPanic_KItem')
+
+    @staticmethod
+    def is_panic(inner: KInner) -> bool:
+        return type(inner) is KApply and (
+            inner.label == KMIR.internal_panic_label() or inner.label == KMIR.panic_label()
+        )
diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py
@@ -62,13 +62,12 @@ def kmir_prove(
     kcfg_explore: KCFGExplore,
     max_depth: int | None = 1000,
     max_iterations: int | None = None,
-    is_terminal: Callable[[CTerm], bool] | None = None,
+    terminal_rules: Iterable[str] = (),
+    cut_point_rules: Iterable[str] = (),  # TODO
     extract_branches: Callable[[CTerm], Iterable[KInner]] | None = None,
     abstract_node: Callable[[CTerm], CTerm] | None = None,
 ) -> bool:
     proof = proof
-    terminal_rules: Iterable[str] = ['MIR.halt']
-    cut_point_rules: Iterable[str] = []  # TODO: cut point rules
     prover: APRBMCProver | APRProver | EqualityProver
     if type(proof) is APRBMCProof:
         prover = APRBMCProver(proof, kcfg_explore)

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.2.5
+0.2.6