!!! wip: changes for debugging

Author: ehildenb

src/kontrol/kompile.py

@@ -150,6 +150,7 @@ def should_rekompile() -> bool:
         if options.o3:
             optimization = 3
 
+        _LOGGER.warning('Invoking kompile')
         kevm_kompile(
             target=options.target,
             output_dir=output_dir,

src/kontrol/prove.py

@@ -436,7 +436,12 @@ def create_kcfg_explore() -> KCFGExplore:
                     rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules
                 )
 
-            lemmas_module = foundry.load_lemmas(options.lemmas)
+            try:
+                lemmas_module = foundry.load_lemmas(options.lemmas)
+            except CalledProcessError as e:
+                _LOGGER.warning(f'stdout: {e.stdout}')
+                _LOGGER.warning(f'stderr: {e.stderr}')
+                raise
 
             if progress is not None and task is not None:
                 progress.update(

src/tests/integration/test-data/cse-lemmas.k

@@ -5,7 +5,7 @@ module CSE-LEMMAS
     rule X xorInt maxUInt256 => maxUInt256 -Int X
       requires #rangeUInt ( 256 , X )
       [simplification]
-
+/*
     // Set equality needed for discharging `#Not ( #Exists ( ... )` on `<accessedAccounts>` unification
     rule { S1:Set #Equals S2:Set |Set SetItem ( X ) } =>
          { X in S1 } #And
@@ -26,7 +26,7 @@ module CSE-LEMMAS
     rule { B:Bytes #Equals B1:Bytes +Bytes B2:Bytes } => {#range(B, 4, lengthBytes(B) -Int 4) #Equals B2}
       requires 4 <=Int lengthBytes(B) andBool #range(B, 0, 4) ==K B1
       [simplification(60), concrete(B, B1)]
-
+*/
     // Bitwise inequalities
     rule [bitwise-and-maxUInt-lt-l]:
       A <Int X &Int Y => false

src/tests/integration/test-data/show/foundry.k.expected

@@ -1,11 +1,4 @@
 requires "contracts.k"
-requires "requires/lemmas.k"
-requires "requires/cse-lemmas.k"
-requires "requires/pausability-lemmas.k"
-requires "requires/symbolic-bytes-lemmas.k"
-requires "requires/keccak.md"
-requires "requires/no_stack_checks.md"
-requires "requires/no_code_size_checks.md"
 
 module FOUNDRY-MAIN
     imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION
@@ -234,7 +227,6 @@ endmodule
 
 module S2KtestZModArithmeticCallTest-VERIFICATION
     imports public S2KtestZModArithmeticCallTest-CONTRACT
-    imports public CSE-LEMMAS
 
 
 
@@ -368,7 +360,6 @@ endmodule
 
 module S2KtestZModCSETest-VERIFICATION
     imports public S2KtestZModCSETest-CONTRACT
-    imports public CSE-LEMMAS
 
 
 
@@ -712,7 +703,6 @@ endmodule
 
 module S2KtestZModImmutableVarsTest-VERIFICATION
     imports public S2KtestZModImmutableVarsTest-CONTRACT
-    imports public SYMBOLIC-BYTES-LEMMAS
 
 
 
@@ -804,7 +794,6 @@ endmodule
 
 module S2KtestZModLoopsTest-VERIFICATION
     imports public S2KtestZModLoopsTest-CONTRACT
-    imports public SUM-TO-N-INVARIANT
 
 
 
@@ -994,7 +983,6 @@ endmodule
 
 module S2KtestZModPortalTest-VERIFICATION
     imports public S2KtestZModPortalTest-CONTRACT
-    imports public PAUSABILITY-LEMMAS
 
 
 

src/tests/integration/test_kontrol.py

@@ -1,7 +1,9 @@
 from __future__ import annotations
 
+import logging
 import sys
 from shutil import copytree
+from subprocess import CalledProcessError
 from typing import TYPE_CHECKING
 
 import pytest
@@ -30,6 +32,9 @@
 sys.setrecursionlimit(10**7)
 
 
+_LOGGER: Final = logging.getLogger(__name__)
+
+
 @pytest.fixture(scope='module')
 def server_end_to_end(foundry_end_to_end: Foundry, no_use_booster: bool) -> Iterator[KoreServer]:
     llvm_definition_dir = foundry_end_to_end.out / 'kompiled' / 'llvm-library' if not no_use_booster else None
@@ -56,21 +61,31 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath
         root_tmp_dir = tmp_path_factory.getbasetemp().parent
 
     foundry_root = root_tmp_dir / 'kontrol-test-project'
+    _LOGGER.warning(f'foundry_end_to_end worker_id: {worker_id}')
+    _LOGGER.warning(f'foundry_end_to_end foundry_root: {foundry_root}')
     with FileLock(str(foundry_root) + '.lock'):
         if not foundry_root.is_dir():
             init_project(project_root=foundry_root, skip_forge=False)
             copytree(str(TEST_DATA_DIR / 'src'), str(foundry_root / 'test'), dirs_exist_ok=True)
             append_to_file(foundry_root / 'foundry.toml', foundry_toml_cancun_schedule())
 
-            foundry_kompile(
-                BuildOptions(
-                    {
-                        'metadata': False,
-                        'auxiliary_lemmas': True,
-                    }
-                ),
-                foundry=Foundry(foundry_root),
-            )
+            try:
+                foundry_kompile(
+                    BuildOptions(
+                        {
+                            'metadata': False,
+                            'auxiliary_lemmas': True,
+                            'verbose': True,
+                            'debug': True,
+                        }
+                    ),
+                    foundry=Foundry(foundry_root),
+                )
+            except CalledProcessError as e:
+                _LOGGER.warning(e)
+                _LOGGER.warning(e.stdout)
+                _LOGGER.warning(e.stderr)
+                raise
 
     session_foundry_root = tmp_path_factory.mktemp('kontrol-test-project')
     copytree(str(foundry_root), str(session_foundry_root), dirs_exist_ok=True)