add no-stack-checks to kontrol.toml file (#867)

* add no stack changes * fix typo * Inverse dest for `--no-...` flags * Update src/kontrol/options.py --------- Co-authored-by: palinatolmach <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
runtimeverification · Oct 16, 2024 · 1bc7712 · 1bc7712
1 parent d1b8b8e
commit 1bc7712
Show file tree

Hide file tree

Showing 9 changed files with 35 additions and 34 deletions.
diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py
@@ -324,23 +324,23 @@ def parse(s: str) -> list[T]:
     )
     build.add_argument(
         '--no-forge-build',
-        dest='no_forge_build',
+        dest='forge_build',
         default=None,
-        action='store_true',
+        action='store_false',
         help="Do not call 'forge build' during kompilation.",
     )
     build.add_argument(
         '--no-silence-warnings',
-        dest='no_silence_warnings',
+        dest='silence_warnings',
         default=None,
-        action='store_true',
+        action='store_false',
         help='Do not silence K compiler warnings.',
     )
     build.add_argument(
         '--no-metadata',
-        dest='no_metadata',
+        dest='metadata',
         default=None,
-        action='store_true',
+        action='store_false',
         help='Do not append cbor or bytecode_hash metadata to bytecode.',
     )
     build.add_argument(
@@ -580,9 +580,9 @@ def parse(s: str) -> list[T]:
     )
     prove_args.add_argument(
         '--no-stack-checks',
-        dest='no_stack_checks',
+        dest='stack_checks',
         default=None,
-        action='store_true',
+        action='store_false',
         help=(
             'Optimize KEVM execution by removing stack overflow/underflow checks.'
             'Assumes running Solidity-compiled bytecode cannot result in a stack overflow/underflow.'

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -399,7 +399,7 @@ def custom_view(self, contract_name: str, element: KCFGElem, compilation_unit: C
             return list(element.rules)
         return ['NO DATA']
 
-    def build(self, no_metadata: bool) -> None:
+    def build(self, metadata: bool) -> None:
         forge_build_args = [
             'forge',
             'build',
@@ -410,7 +410,7 @@ def build(self, no_metadata: bool) -> None:
             'evm.deployedBytecode.generatedSources',
             '--root',
             str(self._root),
-        ] + (['--no-metadata'] if no_metadata else [])
+        ] + (['--no-metadata'] if not metadata else [])
         try:
             run_process_2(
                 forge_build_args,

diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py
@@ -45,10 +45,10 @@ def foundry_kompile(
 
     requires_paths: dict[str, str] = {}
 
-    if not options.no_forge_build:
-        foundry.build(options.no_metadata)
+    if options.forge_build:
+        foundry.build(options.metadata)
 
-    if not options.no_silence_warnings:
+    if options.silence_warnings:
         options.ignore_warnings = _silenced_warnings()
 
     regen = options.regen

diff --git a/src/kontrol/options.py b/src/kontrol/options.py
@@ -378,7 +378,7 @@ class ProveOptions(
     hide_status_bar: bool
     remove_old_proofs: bool
     optimize_performance: int | None
-    no_stack_checks: bool
+    stack_checks: bool
 
     def __init__(self, args: dict[str, Any]) -> None:
         super().__init__(args)
@@ -407,7 +407,7 @@ def default() -> dict[str, Any]:
             'hide_status_bar': False,
             'remove_old_proofs': False,
             'optimize_performance': None,
-            'no_stack_checks': False,
+            'stack_checks': True,
         }
 
     @staticmethod
@@ -471,7 +471,7 @@ def apply_optimizations(self) -> None:
             self.smt_retry_limit = 0
             self.max_depth = 100000
             self.max_iterations = 10000
-            self.no_stack_checks = True
+            self.stack_checks = False
 
     def __str__(self) -> str:
         """
@@ -842,9 +842,9 @@ def get_argument_type() -> dict[str, Callable]:
 class BuildOptions(LoggingOptions, KOptions, KGenOptions, KompileOptions, FoundryOptions, KompileTargetOptions):
     regen: bool
     rekompile: bool
-    no_forge_build: bool
-    no_silence_warnings: bool
-    no_metadata: bool
+    forge_build: bool
+    silence_warnings: bool
+    metadata: bool
     keccak_lemmas: bool
     auxiliary_lemmas: bool
 
@@ -853,9 +853,9 @@ def default() -> dict[str, Any]:
         return {
             'regen': False,
             'rekompile': False,
-            'no_forge_build': False,
-            'no_silence_warnings': False,
-            'no_metadata': False,
+            'forge_build': True,
+            'silence_warnings': True,
+            'metadata': True,
             'keccak_lemmas': True,
             'auxiliary_lemmas': False,
         }

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -425,7 +425,7 @@ def create_kcfg_explore() -> KCFGExplore:
                             'usegas': options.usegas,
                         }
                     ),
-                    no_stack_checks=options.no_stack_checks,
+                    stack_checks=options.stack_checks,
                     trace_options=TraceOptions(
                         {
                             'active_tracing': options.active_tracing,
@@ -568,7 +568,7 @@ def method_to_apr_proof(
     kcfg_explore: KCFGExplore,
     config_type: ConfigType,
     evm_chain_options: EVMChainOptions,
-    no_stack_checks: bool,
+    stack_checks: bool,
     bmc_depth: int | None = None,
     run_constructor: bool = False,
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None = None,
@@ -596,7 +596,7 @@ def method_to_apr_proof(
         setup_proof=setup_proof,
         graft_setup_proof=((setup_proof is not None) and not setup_proof_is_constructor),
         evm_chain_options=evm_chain_options,
-        no_stack_checks=no_stack_checks,
+        stack_checks=stack_checks,
         recorded_state_entries=recorded_state_entries,
         active_symbolik=active_symbolik,
         hevm=hevm,
@@ -640,7 +640,7 @@ def _method_to_initialized_cfg(
     kcfg_explore: KCFGExplore,
     config_type: ConfigType,
     evm_chain_options: EVMChainOptions,
-    no_stack_checks: bool,
+    stack_checks: bool,
     *,
     setup_proof: APRProof | None = None,
     graft_setup_proof: bool = False,
@@ -663,7 +663,7 @@ def _method_to_initialized_cfg(
         recorded_state_entries,
         active_symbolik,
         config_type=config_type,
-        no_stack_checks=no_stack_checks,
+        stack_checks=stack_checks,
         hevm=hevm,
         trace_options=trace_options,
     )
@@ -697,7 +697,7 @@ def _method_to_cfg(
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None,
     active_symbolik: bool,
     config_type: ConfigType,
-    no_stack_checks: bool,
+    stack_checks: bool,
     hevm: bool = False,
     trace_options: TraceOptions | None = None,
 ) -> tuple[KCFG, list[int], int, int, Iterable[int]]:
@@ -735,7 +735,7 @@ def _method_to_cfg(
         trace_options=trace_options,
         config_type=config_type,
         additional_accounts=external_libs,
-        no_stack_checks=no_stack_checks,
+        stack_checks=stack_checks,
     )
     new_node_ids = []
     bounded_node_ids = []
@@ -990,7 +990,7 @@ def _init_cterm(
     active_symbolik: bool,
     evm_chain_options: EVMChainOptions,
     additional_accounts: list[KInner],
-    no_stack_checks: bool,
+    stack_checks: bool,
     *,
     calldata: KInner | None = None,
     callvalue: KInner | None = None,
@@ -1007,7 +1007,7 @@ def _init_cterm(
     init_subst = {
         'MODE_CELL': KApply(evm_chain_options.mode),
         'USEGAS_CELL': boolToken(evm_chain_options.usegas),
-        'STACKCHECKS_CELL': boolToken(not no_stack_checks),
+        'STACKCHECKS_CELL': boolToken(stack_checks),
         'SCHEDULE_CELL': schedule,
         'CHAINID_CELL': intToken(evm_chain_options.chainid),
         'STATUSCODE_CELL': KVariable('STATUSCODE'),

diff --git a/src/kontrol/utils.py b/src/kontrol/utils.py
@@ -230,6 +230,7 @@ def kontrol_toml_file_contents() -> str:
 break-on-basic-blocks      = false
 break-on-cheatcodes        = false
 run-constructor            = false
+no-stack-checks            = true
 
 [show.default]
 foundry-project-root       = '.'

diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py
@@ -91,7 +91,7 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
                             'ImmutableVarsTest:SYMBOLIC-BYTES-LEMMAS',
                         ],
                         'enum_constraints': True,
-                        'no_metadata': True,
+                        'metadata': False,
                     }
                 ),
                 foundry=Foundry(foundry_root, add_enum_constraints=True),

diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py
@@ -67,7 +67,7 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath
                     {
                         'require': str(foundry_root / 'lemmas.k'),
                         'module-import': 'TestBase:KONTROL-LEMMAS',
-                        'no_metadata': True,
+                        'metadata': False,
                     }
                 ),
                 foundry=Foundry(foundry_root),

diff --git a/src/tests/profiling/test_foundry_prove.py b/src/tests/profiling/test_foundry_prove.py
@@ -29,7 +29,7 @@ def test_foundy_prove(
     with profile('kompile.prof', sort_keys=('cumtime', 'tottime'), limit=15):
         foundry_kompile(
             BuildOptions(
-                {'includes': (), 'no_metadata': True},
+                {'includes': (), 'metadata': False},
             ),
             foundry=foundry,
         )