Small build updates for LLVM backend, timing updates (#2098)

* kevm-pyk/{kompile,__main__}: do not turn on debug symbols by default * kevm-pyk/dist: parallelize plugin build * kevm-pyk/__main__: add proof timing information to info log * Set Version: 1.0.308 * kevm-pyk/dist: typo --------- Co-authored-by: devops <[email protected]>
runtimeverification · Oct 27, 2023 · fa4e8e0 · fa4e8e0
1 parent 2bfe71d
commit fa4e8e0
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 7 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -6,6 +6,7 @@
 import logging
 import os
 import sys
+import time
 from argparse import ArgumentParser
 from pathlib import Path
 from typing import TYPE_CHECKING
@@ -98,9 +99,10 @@ def exec_kompile(
     o1: bool = False,
     o2: bool = False,
     o3: bool = False,
-    debug: bool = False,
     enable_llvm_debug: bool = False,
     llvm_library: bool = False,
+    debug_build: bool = False,
+    debug: bool = False,
     verbose: bool = False,
     **kwargs: Any,
 ) -> None:
@@ -116,6 +118,8 @@ def exec_kompile(
         optimization = 2
     if o3:
         optimization = 3
+    if debug_build:
+        optimization = 0
 
     kevm_kompile(
         target,
@@ -130,6 +134,7 @@ def exec_kompile(
         optimization=optimization,
         enable_llvm_debug=enable_llvm_debug,
         llvm_kompile_type=LLVMKompileType.C if llvm_library else LLVMKompileType.MAIN,
+        debug_build=debug_build,
         debug=debug,
         verbose=verbose,
     )
@@ -333,6 +338,7 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                         subproof_ids=claims_graph[claim.label],
                     )
 
+            start_time = time.time()
             passed = kevm_prove(
                 kevm,
                 proof_problem,
@@ -343,6 +349,8 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                 break_on_jumpi=break_on_jumpi,
                 break_on_calls=break_on_calls,
             )
+            end_time = time.time()
+            _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s')
             failure_log = None
             if not passed:
                 failure_log = print_failure_info(proof_problem, kcfg_explore)
@@ -604,6 +612,9 @@ def parse(s: str) -> list[T]:
     kevm_kompile_args.add_argument(
         '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.'
     )
+    kevm_kompile_args.add_argument(
+        '--debug-build', dest='debug_build', default=False, help='Enable debug symbols in LLVM builds.'
+    )
 
     prove_args = command_parser.add_parser(
         'prove',

diff --git a/kevm-pyk/src/kevm_pyk/dist.py b/kevm-pyk/src/kevm_pyk/dist.py
@@ -163,7 +163,7 @@ def _do_build_plugin(*, verbose: bool) -> None:
 
     with _plugin_build_env() as build_dir:
         try:
-            run_process(['make', 'libcryptopp', 'libff', 'libsecp256k1'], cwd=build_dir, pipe_stdout=not verbose)
+            run_process(['make', 'libcryptopp', 'libff', 'libsecp256k1', '-j3'], cwd=build_dir, pipe_stdout=not verbose)
         except CalledProcessError:
             clean_plugin()
             raise
@@ -217,7 +217,7 @@ def _exec_build(
     verbose: bool,
     debug: bool,
 ) -> None:
-    _LOGGER.info(f"Building tagets: {', '.join(targets)}")
+    _LOGGER.info(f"Building targets: {', '.join(targets)}")
 
     verbose = verbose or debug
 

diff --git a/kevm-pyk/src/kevm_pyk/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py
@@ -58,6 +58,7 @@ def kevm_kompile(
     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:
@@ -85,7 +86,7 @@ def kevm_kompile(
     try:
         match target:
             case KompileTarget.LLVM:
-                ccopts = list(ccopts) + _lib_ccopts(kernel)
+                ccopts = list(ccopts) + _lib_ccopts(kernel, debug_build=debug_build)
                 kompile = LLVMKompile(
                     base_args=base_args,
                     ccopts=ccopts,
@@ -103,7 +104,7 @@ def kevm_kompile(
                 return kompile(output_dir=output_dir, debug=debug, verbose=verbose)
 
             case KompileTarget.HASKELL_BOOSTER:
-                ccopts = list(ccopts) + _lib_ccopts(kernel)
+                ccopts = list(ccopts) + _lib_ccopts(kernel, debug_build=debug_build)
                 base_args_llvm = KompileArgs(
                     main_file=main_file,
                     main_module=main_module,
@@ -145,10 +146,13 @@ def _kompile_haskell() -> None:
         raise
 
 
-def _lib_ccopts(kernel: str) -> list[str]:
+def _lib_ccopts(kernel: str, debug_build: bool = False) -> list[str]:
     from . import dist
 
-    ccopts = ['-g', '-std=c++17']
+    ccopts = ['-std=c++17']
+
+    if debug_build:
+        ccopts += ['-g']
 
     ccopts += ['-lssl', '-lcrypto']