Enable booster backend (#40)

* Add `llvm-library` kompile target * Enable booster * Set Version: 0.1.34 * format * Set Version: 0.1.36 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Oct 22, 2024 · c0e6284 · c0e6284
1 parent 3b0992b
commit c0e6284
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 4 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.35
+0.1.36
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.35"
+version = "0.1.36"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/komet/kdist/plugin.py b/src/komet/kdist/plugin.py
@@ -6,7 +6,7 @@
 
 from pyk.kbuild.utils import k_version
 from pyk.kdist.api import Target
-from pyk.ktool.kompile import kompile
+from pyk.ktool.kompile import LLVMKompileType, kompile
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Mapping
@@ -56,6 +56,17 @@ def deps(self) -> tuple[str]:
             'warnings_to_errors': True,
         },
     ),
+    'llvm-library': KompileTarget(
+        lambda src_dir: {
+            'backend': 'llvm',
+            'llvm_kompile_type': LLVMKompileType.C,
+            'main_file': src_dir / 'soroban-semantics/kasmer.md',
+            'syntax_module': 'KASMER-SYNTAX',
+            'include_dirs': [src_dir],
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
     'haskell': KompileTarget(
         lambda src_dir: {
             'backend': 'haskell',

diff --git a/src/komet/proof.py b/src/komet/proof.py
@@ -8,7 +8,7 @@
 from pyk.kcfg.semantics import DefaultSemantics
 from pyk.proof import APRProof, APRProver
 
-from .utils import symbolic_definition
+from .utils import library_definition, symbolic_definition
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
@@ -23,6 +23,7 @@ def _explore_context(id: str, bug_report: BugReport | None) -> Iterator[KCFGExpl
     with cterm_symbolic(
         definition=symbolic_definition.kdefinition,
         definition_dir=symbolic_definition.path,
+        llvm_definition_dir=library_definition.path,
         id=id if bug_report else None,
         bug_report=bug_report,
     ) as cts:

diff --git a/src/komet/utils.py b/src/komet/utils.py
@@ -64,4 +64,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any)
 
 
 concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm'))
+library_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm-library'))
 symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell'))
Original file line number	Diff line number	Diff line change
Expand Up		@@ -64,4 +64,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort \| None = None, **kwargs: Any)


		concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm'))
		library_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm-library'))
		symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell'))