Merge remote-tracking branch 'origin/develop'

runtimeverification · Jul 22, 2024 · 9918d54 · 9918d54
2 parents de70d79 + d10dd05
commit 9918d54
Show file tree

Hide file tree

Showing 2 changed files with 76 additions and 9 deletions.
diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py
@@ -8,7 +8,7 @@
 from pyk.utils import not_none
 
 from ..cterm import CSubst, CTerm
-from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst
+from ..kast.inner import KApply, KLabel, KRewrite, KToken, KVariable, Subst
 from ..kast.manip import flatten_label, is_spurious_constraint, sort_ac_collections
 from ..kast.pretty import PrettyPrinter
 from ..konvert import kast_to_kore, kore_to_kast
@@ -259,14 +259,18 @@ def implies(
                     curr_cell_match = Subst({})
                     for cell in antecedent.cells:
                         antecedent_cell = sort_ac_collections(antecedent.cell(cell))
-                        consequent_cell = sort_ac_collections(consequent.cell(cell))
-                        cell_match = consequent_cell.match(antecedent_cell)
-                        if cell_match is not None:
-                            _curr_cell_match = curr_cell_match.union(cell_match)
-                            if _curr_cell_match is not None:
-                                curr_cell_match = _curr_cell_match
-                                continue
-                        failing_cells.append((cell, KRewrite(antecedent_cell, consequent_cell)))
+
+                        if cell not in consequent.cells:
+                            failing_cells.append((cell, KRewrite(antecedent_cell, KToken('.K', sort='KItem'))))
+                        else:
+                            consequent_cell = sort_ac_collections(consequent.cell(cell))
+                            cell_match = consequent_cell.match(antecedent_cell)
+                            if cell_match is not None:
+                                _curr_cell_match = curr_cell_match.union(cell_match)
+                                if _curr_cell_match is not None:
+                                    curr_cell_match = _curr_cell_match
+                                    continue
+                            failing_cells.append((cell, KRewrite(antecedent_cell, consequent_cell)))
                 else:
                     consequent_constraints = list(
                         filter(

diff --git a/pyk/src/tests/integration/proof/test_mini_kevm.py b/pyk/src/tests/integration/proof/test_mini_kevm.py
@@ -6,7 +6,10 @@
 
 import pytest
 
+from pyk.cterm import CTerm
+from pyk.kast.inner import KApply, KVariable
 from pyk.kcfg.show import KCFGShow
+from pyk.prelude.kint import intToken
 from pyk.proof import APRProof, APRProver, ProofStatus
 from pyk.proof.show import APRProofNodePrinter
 from pyk.testing import KCFGExploreTest, KProveTest
@@ -100,3 +103,63 @@ def test_all_path_reachability_prove(
 
             assert proof.status == proof_status
             assert leaf_number(proof) == expected_leaf_number
+
+    def test_implication_failure_reason_cell_mismatch(
+        self,
+        kcfg_explore: KCFGExplore,
+        kprove: KProve,
+    ) -> None:
+
+        expected = (
+            'Matching failed.\n'
+            'The following cells failed matching individually (antecedent #Implies consequent):\n'
+            'ACCTID_CELL: 0 #Implies .K\n'
+            'STORAGE_CELL: .Map #Implies .K\n'
+            'ORIGSTORAGE_CELL: .Map #Implies .K'
+        )
+
+        antecedent_term = CTerm(
+            KApply(
+                '<generatedTop>',
+                [
+                    KApply('<k>', [intToken(0)]),
+                    KApply('<id>', [intToken(0)]),
+                    KApply(
+                        '<accounts>',
+                        [
+                            KApply(
+                                '<account>',
+                                [
+                                    KApply('<acctID>', [intToken(0)]),
+                                    KApply('<storage>', [KApply('.Map')]),
+                                    KApply('<origStorage>', [KApply('.Map')]),
+                                ],
+                            )
+                        ],
+                    ),
+                    KVariable('GENERATED_COUNTER_CELL'),
+                ],
+            ),
+        )
+
+        consequent_term = CTerm(
+            KApply(
+                '<generatedTop>',
+                [
+                    KApply('<k>', [intToken(0)]),
+                    KApply('<id>', [intToken(0)]),
+                    KApply(
+                        '<accounts>',
+                        [
+                            KApply('.AccountCellMap'),
+                        ],
+                    ),
+                    KVariable('GENERATED_COUNTER_CELL'),
+                ],
+            ),
+        )
+
+        passed, actual = kcfg_explore.implication_failure_reason(antecedent_term, consequent_term)
+
+        assert not passed
+        assert actual == expected