Port model generation code from KEVM into APRFailureInfo (runtimeverification/pyk#604)

I realized we still weren't using the new `APRFailureInfo` class to
handle the printing of failure info in KEVM. And since that has been
added @palinatolmach added counterexample/model printing to the failure
info code in KEVM. Since this code is not KEVM-specific, I thought we
should port that code over to the APRFailureInfo class to support
switching over to using this class in KEVM.
Also refactors the existing fields of `APRFailureInfo` a bit to reduce
large nested types.

---------

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

Author: 2 people

pyk/package/version

@@ -1 +1 @@
-0.1.413
+0.1.414

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.413"
+version = "0.1.414"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

pyk/src/pyk/proof/reachability.py

@@ -8,7 +8,7 @@
 from pyk.kore.rpc import LogEntry
 
 from ..cterm import CTerm
-from ..kast.inner import KRewrite, KSort
+from ..kast.inner import KInner, KRewrite, KSort, Subst
 from ..kast.manip import flatten_label, ml_pred_to_bool
 from ..kast.outer import KClaim
 from ..kcfg import KCFG
@@ -23,7 +23,6 @@
     from pathlib import Path
     from typing import Any, Final, TypeVar
 
-    from ..kast.inner import KInner
     from ..kast.outer import KDefinition
     from ..kcfg import KCFGExplore
     from ..kcfg.kcfg import NodeIdLike
@@ -781,27 +780,61 @@ def lines(self) -> list[str]:
 
 @dataclass(frozen=True)
 class APRFailureInfo:
-    failing_nodes: FrozenDict[int, tuple[str, str]]
     pending_nodes: frozenset[int]
+    failing_nodes: frozenset[int]
+    path_conditions: FrozenDict[int, str]
+    failure_reasons: FrozenDict[int, str]
+    models: FrozenDict[int, frozenset[tuple[str, str]]]
 
-    def __init__(self, failing_nodes: Mapping[int, tuple[str, str]], pending_nodes: Iterable[int]):
-        object.__setattr__(self, 'failing_nodes', FrozenDict(failing_nodes))
+    def __init__(
+        self,
+        failing_nodes: Iterable[int],
+        pending_nodes: Iterable[int],
+        path_conditions: Mapping[int, str],
+        failure_reasons: Mapping[int, str],
+        models: Mapping[int, Iterable[tuple[str, str]]],
+    ):
+        object.__setattr__(self, 'failing_nodes', frozenset(failing_nodes))
         object.__setattr__(self, 'pending_nodes', frozenset(pending_nodes))
+        object.__setattr__(self, 'path_conditions', FrozenDict(path_conditions))
+        object.__setattr__(self, 'failure_reasons', FrozenDict(failure_reasons))
+        object.__setattr__(
+            self, 'models', FrozenDict({node_id: frozenset(model) for (node_id, model) in models.items()})
+        )
 
     @staticmethod
-    def from_proof(proof: APRProof, kcfg_explore: KCFGExplore) -> APRFailureInfo:
+    def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> APRFailureInfo:
         target = proof.kcfg.node(proof.target)
         pending_nodes = {node.id for node in proof.pending}
-        failing_nodes = {}
+        failing_nodes = {node.id for node in proof.failing}
+        path_conditions = {}
+        failure_reasons = {}
+        models = {}
         for node in proof.failing:
             simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm)
             simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm)
             node_cterm = CTerm.from_kast(simplified_node)
             target_cterm = CTerm.from_kast(simplified_target)
             _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
             path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))
-            failing_nodes[node.id] = (reason, path_condition)
-        return APRFailureInfo(failing_nodes=failing_nodes, pending_nodes=pending_nodes)
+            failure_reasons[node.id] = reason
+            path_conditions[node.id] = path_condition
+            if counterexample_info:
+                model_subst = kcfg_explore.cterm_get_model(node.cterm)
+                if type(model_subst) is Subst:
+                    model: list[tuple[str, str]] = []
+                    for var, term in model_subst.to_dict().items():
+                        term_kast = KInner.from_dict(term)
+                        term_pretty = kcfg_explore.kprint.pretty_print(term_kast)
+                        model.append((var, term_pretty))
+                    models[node.id] = model
+        return APRFailureInfo(
+            failing_nodes=failing_nodes,
+            pending_nodes=pending_nodes,
+            path_conditions=path_conditions,
+            failure_reasons=failure_reasons,
+            models=models,
+        )
 
     def print(self) -> list[str]:
         res_lines: list[str] = []
@@ -819,10 +852,9 @@ def print(self) -> list[str]:
         if num_failing > 0:
             res_lines.append('')
             res_lines.append('Failing nodes:')
-            print(self.failing_nodes)
-            for node_id, info in self.failing_nodes.items():
-                print(info)
-                (reason, path_condition) = info
+            for node_id in self.failing_nodes:
+                reason = self.failure_reasons[node_id]
+                path_condition = self.path_conditions[node_id]
                 res_lines.append('')
                 res_lines.append(f'  Node id: {str(node_id)}')
 
@@ -832,6 +864,13 @@ def print(self) -> list[str]:
                 res_lines.append('  Path condition:')
                 res_lines += [f'    {path_condition}']
 
+                if node_id in self.models:
+                    res_lines.append('  Model:')
+                    for var, term in self.models[node_id]:
+                        res_lines.append(f'    {var} = {term}')
+                else:
+                    res_lines.append('  Failed to generate a model.')
+
             res_lines.append('')
             res_lines.append('Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN')
         return res_lines

pyk/src/tests/integration/kcfg/test_imp.py

@@ -1033,7 +1033,7 @@ def test_failure_info(
         assert expected_pending == actual_pending
         assert expected_failing == actual_failing
 
-        actual_path_conds = set({path_condition for _, (_, path_condition) in failure_info.failing_nodes.items()})
+        actual_path_conds = set({path_condition for _, path_condition in failure_info.path_conditions.items()})
         expected_path_conds = set({kprove.pretty_print(condition) for condition in path_conditions})
 
         assert actual_path_conds == expected_path_conds

pyk/src/tests/unit/test_proof.py

@@ -270,17 +270,31 @@ def test_aprbmc_proof_from_dict_heterogeneous_subproofs(proof_dir: Path) -> None
 
 
 def test_print_failure_info() -> None:
-    failing_nodes: dict[int, tuple[str, str]] = {}
-    failing_nodes[3] = (
-        'Structural matching failed, the following cells failed individually (antecedent #Implies consequent):\nSTATE_CELL: $n |-> 2 #Implies 1',
-        'true #Equals X <=Int 100',
-    )
-    failing_nodes[5] = (
-        'Structural matching failed, the following cells failed individually (antecedent #Implies consequent):\nSTATE_CELL: $n |-> 5 #Implies 6',
-        '#Top',
-    )
+    failing_nodes = [3, 5]
     pending_nodes = [6, 7, 8]
-    failure_info = APRFailureInfo(failing_nodes=failing_nodes, pending_nodes=pending_nodes)
+
+    path_conditions = {}
+    path_conditions[3] = 'true #Equals X <=Int 100'
+    path_conditions[5] = '#Top'
+
+    failure_reasons = {}
+    failure_reasons[
+        3
+    ] = 'Structural matching failed, the following cells failed individually (antecedent #Implies consequent):\nSTATE_CELL: $n |-> 2 #Implies 1'
+    failure_reasons[
+        5
+    ] = 'Structural matching failed, the following cells failed individually (antecedent #Implies consequent):\nSTATE_CELL: $n |-> 5 #Implies 6'
+
+    models: dict[int, list[tuple[str, str]]] = {}
+    models[5] = [('X', '101')]
+
+    failure_info = APRFailureInfo(
+        failing_nodes=failing_nodes,
+        pending_nodes=pending_nodes,
+        failure_reasons=failure_reasons,
+        path_conditions=path_conditions,
+        models=models,
+    )
 
     actual_output = '\n'.join(failure_info.print())
     expected_output = r"""5 Failure nodes. (3 pending and 2 failing)
@@ -295,13 +309,16 @@ def test_print_failure_info() -> None:
     STATE_CELL: $n |-> 2 #Implies 1
   Path condition:
     true #Equals X <=Int 100
+  Failed to generate a model.
 
   Node id: 5
   Failure reason:
     Structural matching failed, the following cells failed individually (antecedent #Implies consequent):
     STATE_CELL: $n |-> 5 #Implies 6
   Path condition:
     #Top
+  Model:
+    X = 101
 
 Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN"""