Pass llvm_definition_dir to KCFGExplore in foundry-prove (#1957)

* Update foundry-kompile, passing llvm_definition_dir to KCFGExplore when using booster * Set Version: 1.0.235 * Set Version: 1.0.237 * Set Version: 1.0.238 * Set Version: 1.0.239 * Set Version: 1.0.240 * Set Version: 1.0.241 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Jul 26, 2023 · 8960441 · 8960441
1 parent c467120
commit 8960441
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 13 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.240"
+version = "1.0.241"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -525,7 +525,7 @@ def exec_foundry_prove(
     implication_every_block: bool = True,
     bmc_depth: int | None = None,
     bug_report: bool = False,
-    kore_rpc_command: str | Iterable[str] = ('kore-rpc',),
+    kore_rpc_command: str | Iterable[str] | None = None,
     use_booster: bool = False,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -261,7 +261,7 @@ def explore_args(self) -> ArgumentParser:
             '--kore-rpc-command',
             dest='kore_rpc_command',
             type=str,
-            default='kore-rpc',
+            default=None,
             help='Custom command to start RPC server',
         )
         args.add_argument(

diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py
@@ -423,7 +423,7 @@ def foundry_prove(
     implication_every_block: bool = True,
     bmc_depth: int | None = None,
     bug_report: bool = False,
-    kore_rpc_command: str | Iterable[str] = ('kore-rpc',),
+    kore_rpc_command: str | Iterable[str] | None = None,
     use_booster: bool = False,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,
@@ -451,13 +451,8 @@ def foundry_prove(
                 "Couldn't locate the kore-rpc-booster RPC binary. Please put 'kore-rpc-booster' on PATH manually or using kup install/kup shell."
             ) from None
 
-        if foundry.llvm_dylib:
-            kore_rpc_command = ('kore-rpc-booster', '--llvm-backend-library', str(foundry.llvm_dylib))
-        else:
-            foundry_llvm_dir = foundry.out / 'kompiled-llvm'
-            raise ValueError(
-                f"Could not find the LLVM dynamic library in {foundry_llvm_dir}. Please re-run foundry-kompile with the '--with-llvm-library' flag"
-            )
+    if kore_rpc_command is None:
+        kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',)
 
     all_tests = [
         f'{contract.name}.{method.name}'
@@ -516,11 +511,14 @@ def foundry_prove(
 
     def _init_and_run_proof(_init_problem: tuple[str, str]) -> tuple[bool, list[str] | None]:
         proof_id = f'{_init_problem[0]}.{_init_problem[1]}'
+        llvm_definition_dir = foundry.out / 'kompiled-llvm' if use_booster else None
+
         with KCFGExplore(
             foundry.kevm,
             id=proof_id,
             bug_report=br,
             kore_rpc_command=kore_rpc_command,
+            llvm_definition_dir=llvm_definition_dir,
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
             trace_rewrites=trace_rewrites,

diff --git a/package/debian/changelog b/package/debian/changelog
@@ -1,4 +1,4 @@
-kevm (1.0.240) unstable; urgency=medium
+kevm (1.0.241) unstable; urgency=medium
 
   * Initial Release.
 

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.240
+1.0.241