Merge remote-tracking branch 'upstream/master' into more-kcfg-logs

Author: ehildenb

deps/k_release

@@ -1 +1 @@
-6.1.94
+6.1.96

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.594'
-release = '0.1.594'
+version = '0.1.595'
+release = '0.1.595'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.594
+0.1.595

pyproject.toml

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

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.1.94'
+K_VERSION: Final = '6.1.96'

src/pyk/kore/prelude.py

@@ -142,6 +142,7 @@ def le_int(left: Pattern, right: Pattern) -> Pattern:
 SORT_K: Final = SortApp('SortK')
 SORT_K_ITEM: Final = SortApp('SortKItem')
 SORT_K_CONFIG_VAR: Final = SortApp('SortKConfigVar')
+SORT_GENERATED_TOP_CELL: Final = SortApp('SortGeneratedTopCell')
 
 LBL_INIT_GENERATED_TOP_CELL: Final = SymbolId('LblinitGeneratedTopCell')
 LBL_GENERATED_TOP: Final = SymbolId("Lbl'-LT-'generatedTop'-GT-'")

src/pyk/kore/rpc.py

@@ -370,14 +370,37 @@ def __init__(self, error: str, context: Iterable[str]):
 
 @final
 @dataclass
-class ModuleError(KoreClientError):
+class UnknownModuleError(KoreClientError):
     module_name: str
 
     def __init__(self, module_name: str):
         self.module_name = module_name
         super().__init__(f'Could not find module: {self.module_name}')
 
 
+@final
+@dataclass
+class InvalidModuleError(KoreClientError):
+    error: str
+    context: tuple[str, ...] | None
+
+    def __init__(self, error: str, context: Iterable[str] | None):
+        self.error = error
+        self.context = tuple(context) if context else None
+        context_str = ' Context: ' + ' ;; '.join(self.context) if self.context else ''
+        super().__init__(f'Could not verify module: {self.error}{context_str}')
+
+
+@final
+@dataclass
+class DuplicateModuleError(KoreClientError):
+    module_name: str
+
+    def __init__(self, module_name: str):
+        self.module_name = module_name
+        super().__init__(f'Duplicate module name: {self.module_name}')
+
+
 @final
 @dataclass
 class ImplicationError(KoreClientError):
@@ -875,9 +898,13 @@ def _error(self, err: JsonRpcError) -> KoreClientError:
             case 2:
                 return PatternError(error=err.data['error'], context=err.data['context'])
             case 3:
-                return ModuleError(module_name=err.data)
+                return UnknownModuleError(module_name=err.data)
             case 4:
                 return ImplicationError(error=err.data['error'], context=err.data['context'])
+            case 8:
+                return InvalidModuleError(error=err.data['error'], context=err.data.get('context'))
+            case 9:
+                return DuplicateModuleError(module_name=err.data)
             case _:
                 return DefaultError(message=err.message, code=err.code, data=err.data)
 
@@ -981,8 +1008,14 @@ def get_model(self, pattern: Pattern, module_name: str | None = None) -> GetMode
         result = self._request('get-model', **params)
         return GetModelResult.from_dict(result)
 
-    def add_module(self, module: Module) -> str:
-        result = self._request('add-module', module=module.text)
+    def add_module(self, module: Module, *, name_as_id: bool | None = None) -> str:
+        params = filter_none(
+            {
+                'module': module.text,
+                'name-as-id': name_as_id,
+            }
+        )
+        result = self._request('add-module', **params)
         return result['module']
 
 

src/pyk/proof/reachability.py

@@ -643,7 +643,7 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike
             _kore_module = kflatmodule_to_kore(
                 self.kcfg_explore.kprint.definition, self.kcfg_explore.kprint.kompiled_kore, _module
             )
-            self.kcfg_explore._kore_client.add_module(_kore_module)
+            self.kcfg_explore._kore_client.add_module(_kore_module, name_as_id=True)
 
         super().__init__(kcfg_explore)
         self.proof = proof

src/tests/integration/k-files/int-config.k

@@ -0,0 +1,8 @@
+module INT-CONFIG-SYNTAX
+  imports INT-SYNTAX
+endmodule
+
+module INT-CONFIG
+  imports INT-CONFIG-SYNTAX
+  configuration <k> $PGM:Int </k>
+endmodule