Add cterm_get_model to KCFGExplore for counterexample generation (#519)

Closes the pyk-related part of runtimeverification/evm-semantics#1927,
which is aimed to generate and output concrete assignment to variables
corresponding to the failed Foundry test.

Adds `cterm_get_model(cterm: CTerm) -> Subst | None` function to
`KCFGExplore`, which returns a variable substitution identified via the
`get-model` RPC request. Also adds two IMP tests that check the output
of `cterm_get_model(cterm)` (one of a successful call, one of an
unsuccessful).

---------

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

Author: palinatolmach

package/version

@@ -1 +1 @@
-0.1.357
+0.1.358

pyproject.toml

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

src/pyk/kcfg/explore.py

@@ -18,7 +18,7 @@
 )
 from ..kast.outer import KRule
 from ..konvert import krule_to_kore
-from ..kore.rpc import KoreClient, KoreServer, StopReason
+from ..kore.rpc import KoreClient, KoreServer, SatResult, StopReason, UnknownResult, UnsatResult
 from ..kore.syntax import Import, Module
 from ..ktool.kprove import KoreExecLogFormat
 from ..prelude import k
@@ -176,6 +176,32 @@ def kast_simplify(self, kast: KInner) -> tuple[KInner, tuple[LogEntry, ...]]:
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
         return kast_simplified, logs
 
+    def cterm_get_model(self, cterm: CTerm, module_name: str | None = None) -> Subst | None:
+        _LOGGER.info(f'Getting model: {cterm}')
+        kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL)
+        _, kore_client = self._kore_rpc
+        result = kore_client.get_model(kore, module_name=module_name)
+        if type(result) is UnknownResult:
+            _LOGGER.debug('Result is Unknown')
+            return None
+        elif type(result) is UnsatResult:
+            _LOGGER.debug('Result is UNSAT')
+            return None
+        elif type(result) is SatResult:
+            _LOGGER.debug('Result is SAT')
+            model_subst = self.kprint.kore_to_kast(result.model)
+            _subst: dict[str, KInner] = {}
+            for subst_pred in flatten_label('#And', model_subst):
+                subst_pattern = mlEquals(KVariable('###VAR'), KVariable('###TERM'))
+                m = subst_pattern.match(subst_pred)
+                if m is not None and type(m['###VAR']) is KVariable:
+                    _subst[m['###VAR'].name] = m['###TERM']
+                else:
+                    raise AssertionError(f'Received a non-substitution from get-model endpoint: {subst_pred}')
+            return Subst(_subst)
+        else:
+            raise AssertionError('Received an invalid response from get-model endpoint')
+
     def cterm_implies(
         self,
         antecedent: CTerm,

src/tests/integration/kcfg/test_imp.py

@@ -263,6 +263,36 @@
     ),
 )
 
+GET_MODEL_TEST_DATA: Final = (
+    (
+        'get-model-sat',
+        (
+            'int $n ; $n = X ;',
+            '.Map',
+            mlAnd(
+                [
+                    mlEqualsTrue(KApply('_==Int_', [KVariable('X'), intToken(3)])),
+                ]
+            ),
+        ),
+        Subst({'X': intToken(3)}),
+    ),
+    (
+        'get-model-unsat',
+        (
+            'int $n ; $n = X ;',
+            '.Map',
+            mlAnd(
+                [
+                    mlEqualsTrue(KApply('_<Int_', [KVariable('X'), intToken(4)])),
+                    mlEqualsTrue(KApply('_>Int_', [KVariable('X'), intToken(4)])),
+                ]
+            ),
+        ),
+        None,
+    ),
+)
+
 APR_PROVE_TEST_DATA: Iterable[tuple[str, Path, str, str, int | None, int | None, Iterable[str], ProofStatus, int]] = (
     (
         'imp-simple-addition-1',
@@ -707,6 +737,27 @@ def test_execute(
         assert actual_depth == expected_depth
         assert set(actual_next_states) == set(expected_next_states)
 
+    @pytest.mark.parametrize(
+        'test_id,cterm,expected',
+        GET_MODEL_TEST_DATA,
+        ids=[test_id for test_id, *_ in GET_MODEL_TEST_DATA],
+    )
+    def test_get_model(
+        self,
+        kcfg_explore: KCFGExplore,
+        cterm: CTerm,
+        test_id: str,
+        expected: Subst | None,
+    ) -> None:
+        # Given
+        cterm_term = self.config(kcfg_explore.kprint, *cterm)
+
+        # When
+        actual = kcfg_explore.cterm_get_model(cterm_term)
+
+        # Then
+        assert actual == expected
+
     @pytest.mark.parametrize(
         'test_id,antecedent,consequent,expected',
         IMPLIES_TEST_DATA,