Inject ccopts directly into kevm_kompile and fix some tests (#2164)

* Makefile: make sure evm-optimizations-spec is rebuilt on changes to optimizations.md * kproj/optimizations: remove symbolic attribute on evm-optimizations-lemmas * tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM backend * tests/specs/functional/infinite-gas-spec.k: allow import of main module in symbolic module for LLVM * kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => kompile-spec} for more accurate usage * README: update documentation * kevm-pyk/: all builds require plugin_dir, compute it directly * kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in ccopts directly * kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec * VERIFICATION: update documentation * Makefile: bring back --target argument * Set Version: 1.0.343 * test_prove: only add ccopts if were using the booster * Set Version: 1.0.355 * package/test-package: add previously failing test of using booster due to plugin_dir being missing * kevm-pyk/__main__: use correct target for kompile-spec * Set Version: 1.0.356 * Set Version: 1.0.356 * kevm-pyk/plugin: correction from code review * kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets * kevm-pyk/: factor out generic run_kompile from kevm_kompile * kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts * Set Version: 1.0.357 * kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenndency * Set Version: 1.0.357 * kdist/plugin: drop self._deps * Set Version: 1.0.358 * Set Version: 1.0.358 --------- Co-authored-by: devops <devops@runtimeverification.com>
runtimeverification · Nov 20, 2023 · 52365cc · 52365cc
1 parent 5f20200
commit 52365cc
Show file tree

Hide file tree

Showing 14 changed files with 93 additions and 41 deletions.
diff --git a/Makefile b/Makefile
@@ -59,7 +59,7 @@ test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_kprove_prove"
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
-tests/specs/opcodes/evm-optimizations-spec.md:
+tests/specs/opcodes/evm-optimizations-spec.md: kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
 	cat kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
 
 
@@ -108,7 +108,7 @@ tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$
 		--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
 
 tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT)
-	$(POETRY_RUN) kevm-pyk kompile                                                                             \
+	$(POETRY_RUN) kevm-pyk kompile-spec                                                                         \
 		$<                                                                                                      \
 		--target $(word 3, $(subst /, , $*))                                                                    \
 		--output-definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \

diff --git a/README.md b/README.md
@@ -207,7 +207,7 @@ Finally, you can build the semantics.
 poetry -C kevm-pyk run kevm-dist --verbose build -j4
 ```
 
-You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone}`, e.g.:
+You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone,plugin}`, e.g.:
 
 ```sh
 poetry -C kevm-pyk run kevm-dist build -j2 evm-semantics.llvm evm-semantics.haskell

diff --git a/VERIFICATION.md b/VERIFICATION.md
@@ -18,13 +18,12 @@ It has two modules:
 The first step is kompiling the `.k` file with the below command.
 
 ```sh
-kevm kompile sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile-spec sum-to-n-spec.k --target haskell-booster --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
 ```
 
 In this example, the arguments used are:
 
-  - `—-pyk`: a flag that enables the pyk library.
-  - `—-backend haskell`: used to kompile the definition with the Haskell backend, enabling the symbolic execution ([more about it here]).
+  - `--target haskell-booster`: specify which symbolic backend to use for reasoning.
   - `--syntax-module VERIFICATION`: explicitly state the syntax module.
   - `--main-module VERIFICATION`: explicitly state the main module.
   - `--definition sum-to-n-spec/haskell`: the path where the kompiled definition is stored.
@@ -61,7 +60,7 @@ These rules are then used in the claims. As an example, the `#binRuntime(ERC20)`
 Following this, we can compile the Markdown file with:
 
 ```sh
-kevm kompile erc20-spec.md --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
+kevm kompile-spec erc20-spec.md --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
 ```
 
 Next, run the prover with:
@@ -101,7 +100,7 @@ A running example:
 
 ```sh
 mkdir kcfgs
-kevm kompile --target haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm kompile-spec tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
 kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --verbose --save-directory kcfgs
 kevm view-kcfg --verbose kcfgs tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell
 ```

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.357"
+version = "1.0.358"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.357'
+VERSION: Final = '1.0.358'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -87,7 +87,7 @@ def exec_version(**kwargs: Any) -> None:
     print(f'KEVM Version: {VERSION}')
 
 
-def exec_kompile(
+def exec_kompile_spec(
     output_dir: Path | None,
     main_file: Path,
     emit_json: bool,
@@ -109,7 +109,12 @@ def exec_kompile(
     **kwargs: Any,
 ) -> None:
     if target is None:
-        target = KompileTarget.LLVM
+        target = KompileTarget.HASKELL_BOOSTER
+
+    if target not in [KompileTarget.HASKELL, KompileTarget.HASKELL_BOOSTER, KompileTarget.MAUDE]:
+        raise ValueError(
+            f'Can only call kevm kompile-spec with --target [haskell,haskell-booster,maude], got: {target.value}'
+        )
 
     output_dir = output_dir or Path()
 
@@ -671,17 +676,17 @@ def parse(s: str) -> list[T]:
 
     command_parser.add_parser('version', help='Print KEVM version and exit.', parents=[kevm_cli_args.logging_args])
 
-    kevm_kompile_args = command_parser.add_parser(
-        'kompile',
+    kevm_kompile_spec_args = command_parser.add_parser(
+        'kompile-spec',
         help='Kompile KEVM specification.',
         parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args],
     )
-    kevm_kompile_args.add_argument('main_file', type=file_path, help='Path to file with main module.')
-    kevm_kompile_args.add_argument('--target', type=KompileTarget, help='[llvm|haskell|haskell-booster]')
-    kevm_kompile_args.add_argument(
+    kevm_kompile_spec_args.add_argument('main_file', type=file_path, help='Path to file with main module.')
+    kevm_kompile_spec_args.add_argument('--target', type=KompileTarget, help='[haskell|haskell-booster|maude]')
+    kevm_kompile_spec_args.add_argument(
         '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.'
     )
-    kevm_kompile_args.add_argument(
+    kevm_kompile_spec_args.add_argument(
         '--debug-build', dest='debug_build', default=False, help='Enable debug symbols in LLVM builds.'
     )
 

diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py
@@ -11,33 +11,34 @@
 from .api import Target
 
 if TYPE_CHECKING:
-    from collections.abc import Iterable, Mapping
+    from collections.abc import Mapping
     from pathlib import Path
     from typing import Any, Final
 
 
 class KEVMTarget(Target):
     _kompile_args: dict[str, Any]
-    _deps: tuple[str, ...]
 
-    def __init__(self, kompile_args: Mapping[str, Any], *, deps: Iterable[str] | None = None):
+    def __init__(self, kompile_args: Mapping[str, Any]):
         self._kompile_args = dict(kompile_args)
-        self._deps = tuple(deps) if deps is not None else ()
 
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any]) -> None:
         verbose = args.get('verbose', False)
         enable_llvm_debug = args.get('enable_llvm_debug', False)
+        debug_build = args.get('debug_build', False)
+        ccopts = args.get('ccopts', [])
 
         kevm_kompile(
             output_dir=output_dir,
             enable_llvm_debug=enable_llvm_debug,
             verbose=verbose,
-            plugin_dir=deps.get('evm-semantics.plugin'),
+            ccopts=ccopts,
+            debug_build=debug_build,
             **self._kompile_args,
         )
 
     def deps(self) -> tuple[str, ...]:
-        return self._deps
+        return ('evm-semantics.plugin',)
 
 
 class PluginTarget(Target):
@@ -76,7 +77,6 @@ def build(self, output_dir: Path, deps: dict[str, Any], args: dict[str, Any]) ->
             'syntax_module': 'ETHEREUM-SIMULATION',
             'optimization': 2,
         },
-        deps=('evm-semantics.plugin',),
     ),
     'haskell': KEVMTarget(
         {

diff --git a/kevm-pyk/src/kevm_pyk/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py
@@ -10,7 +10,7 @@
 from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType, MaudeKompile
 from pyk.utils import run_process
 
-from . import config
+from . import config, kdist
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
@@ -45,8 +45,49 @@ def md_selector(self) -> str:
 def kevm_kompile(
     target: KompileTarget,
     output_dir: Path,
+    main_file: Path,
     *,
+    main_module: str | None,
+    syntax_module: str | None,
+    includes: Iterable[str] = (),
+    emit_json: bool = True,
+    read_only: bool = False,
+    ccopts: Iterable[str] = (),
+    optimization: int = 0,
+    llvm_kompile_type: LLVMKompileType | None = None,
+    enable_llvm_debug: bool = False,
+    llvm_library: Path | None = None,
+    debug_build: bool = False,
+    debug: bool = False,
+    verbose: bool = False,
+) -> Path:
+    plugin_dir = kdist.get('evm-semantics.plugin')
+    ccopts = list(ccopts) + _lib_ccopts(plugin_dir, debug_build=debug_build)
+    return run_kompile(
+        target,
+        output_dir,
+        main_file,
+        main_module=main_module,
+        syntax_module=syntax_module,
+        includes=includes,
+        emit_json=emit_json,
+        read_only=read_only,
+        ccopts=ccopts,
+        optimization=optimization,
+        llvm_kompile_type=llvm_kompile_type,
+        enable_llvm_debug=enable_llvm_debug,
+        llvm_library=llvm_library,
+        debug_build=debug_build,
+        debug=debug,
+        verbose=verbose,
+    )
+
+
+def run_kompile(
+    target: KompileTarget,
+    output_dir: Path,
     main_file: Path,
+    *,
     main_module: str | None,
     syntax_module: str | None,
     includes: Iterable[str] = (),
@@ -57,17 +98,13 @@ def kevm_kompile(
     llvm_kompile_type: LLVMKompileType | None = None,
     enable_llvm_debug: bool = False,
     llvm_library: Path | None = None,
-    plugin_dir: Path | None = None,
     debug_build: bool = False,
     debug: bool = False,
     verbose: bool = False,
 ) -> Path:
     if llvm_library is None:
         llvm_library = output_dir / 'llvm-library'
 
-    if target in [KompileTarget.LLVM, KompileTarget.HASKELL_BOOSTER] and not plugin_dir:
-        raise ValueError(f'Parameter plugin_dir is required for target: {target.value}')
-
     include_dirs = [Path(include) for include in includes]
     include_dirs += config.INCLUDE_DIRS
 
@@ -89,8 +126,6 @@ def kevm_kompile(
     try:
         match target:
             case KompileTarget.LLVM:
-                assert plugin_dir
-                ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build)
                 kompile = LLVMKompile(
                     base_args=base_args,
                     ccopts=ccopts,
@@ -129,9 +164,8 @@ def _kompile_haskell() -> None:
                     [future.result() for future in futures]
 
                 return output_dir
+
             case KompileTarget.HASKELL_BOOSTER:
-                assert plugin_dir
-                ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build)
                 base_args_llvm = KompileArgs(
                     main_file=main_file,
                     main_module=main_module,
@@ -173,7 +207,9 @@ def _kompile_haskell() -> None:
         raise
 
 
-def _lib_ccopts(plugin_dir: Path, kernel: str, debug_build: bool = False) -> list[str]:
+def _lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]:
+    kernel = sys.platform
+
     ccopts = ['-std=c++17']
 
     if debug_build:

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -7,7 +7,7 @@ These optimizations work on the LLVM and Haskell backend and are generated by th
 requires "evm.md"
 requires "lemmas/int-simplification.k"
 
-module EVM-OPTIMIZATIONS-LEMMAS [kore, symbolic]
+module EVM-OPTIMIZATIONS-LEMMAS [kore]
     imports EVM
 
     rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                [simplification]

diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
@@ -9,7 +9,7 @@
 from pyk.cterm import CTerm
 from pyk.proof.reachability import APRProof
 
-from kevm_pyk import config, kdist
+from kevm_pyk import config
 from kevm_pyk.__main__ import exec_prove
 from kevm_pyk.kevm import KEVM
 from kevm_pyk.kompile import KompileTarget, kevm_kompile
@@ -117,16 +117,13 @@ class Target(NamedTuple):
     def __call__(self, output_dir: Path) -> Path:
         definition_subdir = 'kompiled' if not self.use_booster else 'kompiled-booster'
         definition_dir = output_dir / definition_subdir
-        plugin_dir = kdist.get('evm-semantics.plugin') if self.use_booster else None
         target = KompileTarget.HASKELL if not self.use_booster else KompileTarget.HASKELL_BOOSTER
         return kevm_kompile(
             output_dir=definition_dir,
             target=target,
             main_file=self.main_file,
             main_module=self.main_module_name,
             syntax_module=self.main_module_name,
-            includes=[],
-            plugin_dir=plugin_dir,
             debug=True,
         )
 

diff --git a/package/test-package.sh b/package/test-package.sh
@@ -30,3 +30,16 @@ if ! ${APPLE_SILICON:-false}; then
         || git --no-pager diff --no-index --ignore-all-space -R tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.llvm-out tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
     rm -rf tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.llvm-out
 fi
+
+kevm kompile-spec tests/specs/benchmarks/verification.k             \
+    --output-definition tests/specs/benchmarks/verification/haskell \
+    --main-module VERIFICATION                                      \
+    --syntax-module VERIFICATION                                    \
+    --target haskell-booster                                        \
+    --verbose
+
+kevm prove tests/specs/benchmarks/structarg00-spec.k         \
+    --definition tests/specs/benchmarks/verification/haskell \
+    --save-directory proofs                                  \
+    --verbose                                                \
+    --use-booster
diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.357
+1.0.358
diff --git a/tests/specs/examples/sum-to-n-foundry-spec.k b/tests/specs/examples/sum-to-n-foundry-spec.k
@@ -4,6 +4,7 @@ requires "gas.md"
 module VERIFICATION
     imports LEMMAS
     imports INFINITE-GAS
+    imports EVM
 
     rule N xorInt maxUInt256 => maxUInt256 -Int N
     requires #rangeUInt(256, N)

diff --git a/tests/specs/functional/infinite-gas-spec.k b/tests/specs/functional/infinite-gas-spec.k
@@ -4,6 +4,7 @@ requires "lemmas/lemmas.k"
 module VERIFICATION
     imports INFINITE-GAS
     imports LEMMAS
+    imports EVM
 endmodule
 
 module INFINITE-GAS-SPEC