diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index deaf98fd3..52ca811b6 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -575,7 +575,17 @@ def parse(s: str) -> list[T]: help=( 'Optimize performance for proof execution. Takes the number of parallel threads to be used.' "Will overwrite other settings of 'assume-defined', 'log-success-rewrites', 'max-frontier-parallel'," - "'maintenance-rate', 'smt-timeout', 'smt-retry-limit', 'max-depth', and 'max-iterations'." + "'maintenance-rate', 'smt-timeout', 'smt-retry-limit', 'max-depth', 'max-iterations', and 'no-stack-checks'." + ), + ) + prove_args.add_argument( + '--no-stack-checks', + dest='no_stack_checks', + default=None, + action='store_true', + 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 index 31c549d8d..caf2beb0a 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -865,7 +865,12 @@ def _remove_foundry_config(_cterm: CTerm) -> CTerm: [ KApply( '', - [KVariable('KEVM_CELL'), KVariable('CHEATCODES_CELL'), KVariable('KEVMTRACING_CELL')], + [ + KVariable('KEVM_CELL'), + KVariable('STACKCHECKS_CELL'), + KVariable('CHEATCODES_CELL'), + KVariable('KEVMTRACING_CELL'), + ], ), KVariable('GENERATEDCOUNTER_CELL'), ], diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index 3d50fd97b..1b6b9bc48 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -470,7 +470,7 @@ WThe `#checkRevert` will be used to compare the status code of the execution and CD ... - [priority(38)] + [priority(32)] rule [foundry.set.expectrevert.2]: #next [ _OP:CallSixOp ] ~> (.K => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... @@ -481,7 +481,7 @@ WThe `#checkRevert` will be used to compare the status code of the execution and CD ... - [priority(38)] + [priority(32)] rule [foundry.set.expectrevert.3]: #next [ OP:OpCode ] ~> (.K => #checkRevert) ~> #execute ... @@ -492,7 +492,7 @@ WThe `#checkRevert` will be used to compare the status code of the execution and ... requires (OP ==K CREATE orBool OP ==K CREATE2) - [priority(38)] + [priority(32)] ``` If the `expectRevert()` selector is matched, call the `#setExpectRevert` production to initialize the `` subconfiguration. @@ -656,7 +656,7 @@ The last point is required in order to prevent overwriting the caller for subcal requires ACCT =/=K NCL andBool ACCTTO =/=K #address(FoundryCheat) andBool (OP ==K CALL orBool OP ==K CALLCODE orBool OP ==K STATICCALL orBool OP ==K CREATE orBool OP ==K CREATE2) - [priority(40)] + [priority(34)] ``` #### `startPrank` - Sets `msg.sender` and `tx.origin` for all subsequent calls until `stopPrank` is called. diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md index 7b27399fa..2ac8861a7 100644 --- a/src/kontrol/kdist/foundry.md +++ b/src/kontrol/kdist/foundry.md @@ -30,6 +30,7 @@ module FOUNDRY configuration + true diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md index f9feb18e7..8e965c2fc 100644 --- a/src/kontrol/kdist/kontrol_lemmas.md +++ b/src/kontrol/kdist/kontrol_lemmas.md @@ -14,18 +14,6 @@ module KONTROL-AUX-LEMMAS imports MAP-SYMBOLIC imports SET-SYMBOLIC - syntax StepSort ::= Int - | Bool - | Bytes - | Map - | Set - // ------------------------- - - syntax KItem ::= runLemma ( StepSort ) - | doneLemma( StepSort ) - // -------------------------------------- - rule runLemma(T) => doneLemma(T) ... - syntax Int ::= "ethMaxWidth" [macro] syntax Int ::= "ethUpperBound" [macro] // -------------------------------------- diff --git a/src/kontrol/kdist/no_stack_checks.md b/src/kontrol/kdist/no_stack_checks.md new file mode 100644 index 000000000..0ca3a59dc --- /dev/null +++ b/src/kontrol/kdist/no_stack_checks.md @@ -0,0 +1,145 @@ +Optimized EVM rules +=================== + +The provided rules speed up execution by not performing stack overflow/underflow checks +and rely on the hypothesis that EVM bytecode that comes compiled from Solidity will not +result in a stack overflow/underflow. + +```k +requires "foundry.md" + +module NO-STACK-CHECKS + imports EVM + imports FOUNDRY + + rule [super.optimized.pushzero]: + ( #next[ PUSHZERO ] => .K ) ... + false + false + WS => 0 : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.push]: + ( #next[ PUSH(N) ] => .K ) ... + false + false + PGM + WS => #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS + PCOUNT => PCOUNT +Int N +Int 1 + [priority(30)] + + rule [super.optimized.dup]: + ( #next[ DUP(N) ] => .K ) ... + false + false + WS => WS [ ( N +Int -1 ) ] : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.swap]: + ( #next[ SWAP(N) ] => .K ) ... + false + false + W0 : WS => WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.add]: + ( #next[ ADD ] => .K ) ... + false + false + W0 : W1 : WS => chop ( W0 +Int W1 ) : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.sub]: + ( #next[ SUB ] => .K ) ... + false + false + W0 : W1 : WS => chop ( W0 -Int W1 ) : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.mul]: + ( #next[ MUL ] => .K ) ... + false + false + W0 : W1 : WS => chop ( W0 *Int W1 ) : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.and]: + ( #next[ AND ] => .K ) ... + false + false + W0 : W1 : WS => W0 &Int W1 : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.or]: + ( #next[ EVMOR ] => .K ) ... + false + false + W0 : W1 : WS => W0 |Int W1 : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.xor]: + ( #next[ XOR ] => .K ) ... + false + false + W0 : W1 : WS => W0 xorInt W1 : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.iszero]: + ( #next[ ISZERO ] => .K ) ... + false + false + W0 : WS => bool2Word ( W0 ==Int 0 ) : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.lt]: + ( #next[ LT ] => .K ) ... + false + false + W0 : W1 : WS => bool2Word ( W0 + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.gt]: + ( #next[ GT ] => .K ) ... + false + false + W0 : W1 : WS => bool2Word ( W1 + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.eq]: + ( #next[ EQ ] => .K ) ... + false + false + W0 : W1 : WS => bool2Word ( W0 ==Int W1 ) : WS + PCOUNT => PCOUNT +Int 1 + [priority(30)] + + rule [super.optimized.next.succ]: + ( #next [ OP:OpCode ] => #addr [ OP ] ~> #exec [ OP ] ~> #pc[ OP ] ) ... + false + WS + STATIC:Bool + requires notBool ( STATIC andBool #changesState(OP, WS) ) + [priority(36)] + + rule [super.optimized.next.smv]: + ( #next [ OP ] => #end EVMC_STATIC_MODE_VIOLATION ) ... + false + WS + STATIC:Bool + requires STATIC andBool #changesState(OP, WS) + [priority(38)] + +endmodule +``` \ No newline at end of file diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index c0a41d0c2..88a27f234 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -63,6 +63,7 @@ def foundry_kompile( options.requires + ([KSRC_DIR / 'keccak.md'] if options.keccak_lemmas else []) + ([KSRC_DIR / 'kontrol_lemmas.md'] if options.auxiliary_lemmas else []) + + ([KSRC_DIR / 'no_stack_checks.md']) ) for r in tuple(requires): req = Path(r) @@ -227,6 +228,7 @@ def _foundry_to_main_def( [KImport(mname) for mname in (_m.name for _m in modules)] + ([KImport('KECCAK-LEMMAS')] if keccak_lemmas else []) + ([KImport('KONTROL-AUX-LEMMAS')] if auxiliary_lemmas else []) + + ([KImport('NO-STACK-CHECKS')]) ), ) diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 3bf0b4d2f..d030c92e2 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -378,6 +378,7 @@ class ProveOptions( hide_status_bar: bool remove_old_proofs: bool optimize_performance: int | None + no_stack_checks: bool def __init__(self, args: dict[str, Any]) -> None: super().__init__(args) @@ -406,6 +407,7 @@ def default() -> dict[str, Any]: 'hide_status_bar': False, 'remove_old_proofs': False, 'optimize_performance': None, + 'no_stack_checks': False, } @staticmethod @@ -464,11 +466,12 @@ def apply_optimizations(self) -> None: self.assume_defined = True self.log_succ_rewrites = False self.max_frontier_parallel = self.optimize_performance - self.maintenance_rate = 2 * self.optimize_performance + self.maintenance_rate = 64 self.smt_timeout = 120000 self.smt_retry_limit = 0 self.max_depth = 100000 self.max_iterations = 10000 + self.no_stack_checks = True def __str__(self) -> str: """ diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 84aa15ecf..beb18a105 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -425,6 +425,7 @@ def create_kcfg_explore() -> KCFGExplore: 'usegas': options.usegas, } ), + no_stack_checks=options.no_stack_checks, trace_options=TraceOptions( { 'active_tracing': options.active_tracing, @@ -567,6 +568,7 @@ def method_to_apr_proof( kcfg_explore: KCFGExplore, config_type: ConfigType, evm_chain_options: EVMChainOptions, + no_stack_checks: bool, bmc_depth: int | None = None, run_constructor: bool = False, recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None = None, @@ -594,6 +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, recorded_state_entries=recorded_state_entries, active_symbolik=active_symbolik, hevm=hevm, @@ -637,6 +640,7 @@ def _method_to_initialized_cfg( kcfg_explore: KCFGExplore, config_type: ConfigType, evm_chain_options: EVMChainOptions, + no_stack_checks: bool, *, setup_proof: APRProof | None = None, graft_setup_proof: bool = False, @@ -659,6 +663,7 @@ def _method_to_initialized_cfg( recorded_state_entries, active_symbolik, config_type=config_type, + no_stack_checks=no_stack_checks, hevm=hevm, trace_options=trace_options, ) @@ -692,6 +697,7 @@ def _method_to_cfg( recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None, active_symbolik: bool, config_type: ConfigType, + no_stack_checks: bool, hevm: bool = False, trace_options: TraceOptions | None = None, ) -> tuple[KCFG, list[int], int, int, Iterable[int]]: @@ -729,6 +735,7 @@ def _method_to_cfg( trace_options=trace_options, config_type=config_type, additional_accounts=external_libs, + no_stack_checks=no_stack_checks, ) new_node_ids = [] bounded_node_ids = [] @@ -983,6 +990,7 @@ def _init_cterm( active_symbolik: bool, evm_chain_options: EVMChainOptions, additional_accounts: list[KInner], + no_stack_checks: bool, *, calldata: KInner | None = None, callvalue: KInner | None = None, @@ -999,6 +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), 'SCHEDULE_CELL': schedule, 'CHAINID_CELL': intToken(evm_chain_options.chainid), 'STATUSCODE_CELL': KVariable('STATUSCODE'), diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected index a80ce47c6..2b167bd20 100644 --- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected +++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected @@ -217,6 +217,9 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected index 70204a886..90f8dc503 100644 --- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected +++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected @@ -175,6 +175,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 ... + + true + @@ -351,6 +354,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected index 64ac0971a..fa455752b 100644 --- a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected +++ b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected @@ -177,6 +177,9 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected index 3362524ca..38ed21585 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected @@ -406,6 +406,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ... + + true + @@ -806,6 +809,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ... + + true + @@ -1188,6 +1194,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ... + + true + @@ -1572,6 +1581,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ... + + true + @@ -1957,6 +1969,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected index 2f4701df4..0ae760c1b 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected @@ -455,6 +455,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + @@ -855,6 +858,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + @@ -1237,6 +1243,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + @@ -1621,6 +1630,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + @@ -2006,6 +2018,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + @@ -2395,6 +2410,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + @@ -2786,6 +2804,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ... + + true + diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected index a10c9e8f9..58152a0b6 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected @@ -459,6 +459,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + @@ -844,6 +847,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + @@ -1246,6 +1252,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + @@ -1630,6 +1639,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + @@ -2020,6 +2032,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + @@ -2409,6 +2424,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + @@ -2800,6 +2818,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ... + + true + diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected index c7ce9bf0a..d79579de9 100644 --- a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected @@ -172,6 +172,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 ... + + true + @@ -347,6 +350,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected index 7e4195689..092c69f55 100644 --- a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected @@ -247,6 +247,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ... + + true + @@ -433,6 +436,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ... + + true + @@ -620,6 +626,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ... + + true + @@ -808,6 +817,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index 824a8d766..02d97d7ed 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -210,6 +210,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ... + + true + @@ -446,6 +449,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ... + + true + @@ -681,6 +687,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ... + + true + @@ -918,6 +927,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ... + + true + @@ -1155,6 +1167,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected index a10257853..bb12fb751 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected @@ -210,6 +210,9 @@ Node 10: ... + + true + @@ -450,6 +453,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ... + + true + @@ -686,6 +692,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ... + + true + @@ -921,6 +930,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ... + + true + @@ -1158,6 +1170,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ... + + true + @@ -1395,6 +1410,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index ff7acebaf..72e75126d 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -296,6 +296,9 @@ Node 20: ... + + true + @@ -541,6 +544,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -777,6 +783,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -1012,6 +1021,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -1249,6 +1261,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -1489,6 +1504,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -1733,6 +1751,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -2071,6 +2092,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -2407,6 +2431,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -2744,6 +2771,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -3084,6 +3114,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -3424,6 +3457,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -3767,6 +3803,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -4110,6 +4149,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -4352,6 +4394,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + @@ -4594,6 +4639,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index 8bc82d465..c98a79a22 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -207,6 +207,9 @@ Node 10: ... + + true + @@ -447,6 +450,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ... + + true + @@ -683,6 +689,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ... + + true + @@ -918,6 +927,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ... + + true + @@ -1155,6 +1167,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ... + + true + @@ -1392,6 +1407,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected index b6a054a98..984ed7556 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected @@ -213,6 +213,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ... + + true + @@ -449,6 +452,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ... + + true + @@ -684,6 +690,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ... + + true + @@ -921,6 +930,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ... + + true + @@ -1158,6 +1170,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected index 378d89bd6..37eedec14 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected @@ -270,6 +270,9 @@ Node 16: ... + + true + @@ -513,6 +516,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -749,6 +755,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -987,6 +996,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -1224,6 +1236,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -1462,6 +1477,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -1702,6 +1720,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -1942,6 +1963,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -2182,6 +2206,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -2422,6 +2449,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index 90831d44d..ee2e9cf2f 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -268,6 +268,9 @@ Node 16: ... + + true + @@ -513,6 +516,9 @@ Node 15: ... + + true + @@ -758,6 +764,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -994,6 +1003,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -1234,6 +1246,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -1473,6 +1488,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -1713,6 +1731,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -1955,6 +1976,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -2197,6 +2221,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -2439,6 +2466,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -2681,6 +2711,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index e0cb6f154..9589da935 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -208,6 +208,9 @@ Node 7: ... + + true + @@ -451,6 +454,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -693,6 +699,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -936,6 +945,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -1179,6 +1191,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -1420,6 +1435,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected index efc4bc42a..e0470aab7 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected @@ -234,6 +234,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -476,6 +479,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -718,6 +724,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -958,6 +967,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -1201,6 +1213,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -1445,6 +1460,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -1688,6 +1706,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + @@ -1931,6 +1952,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index e1bed70c0..ed9d487e9 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -232,6 +232,9 @@ Node 10: ... + + true + @@ -477,6 +480,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -719,6 +725,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -961,6 +970,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -1201,6 +1213,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -1444,6 +1459,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -1688,6 +1706,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -1931,6 +1952,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + @@ -2174,6 +2198,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected index 776e9693e..116a0d6a5 100644 --- a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected +++ b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected @@ -380,6 +380,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -621,6 +624,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -862,6 +868,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -1104,6 +1113,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -1347,6 +1359,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -1588,6 +1603,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -1830,6 +1848,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -2069,6 +2090,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -2309,6 +2333,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -2550,6 +2577,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -2792,6 +2822,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -3030,6 +3063,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -3269,6 +3305,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + @@ -3509,6 +3548,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ... + + true + diff --git a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected index 12634558e..d071b1842 100644 --- a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected +++ b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected @@ -177,6 +177,9 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected index 3e235f4c4..3304b8112 100644 --- a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected @@ -288,6 +288,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 ... + + true + @@ -597,6 +600,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 ... + + true + @@ -927,6 +933,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected index 1dce23e3f..211efc15d 100644 --- a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected @@ -284,6 +284,9 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 ... + + true + @@ -593,6 +596,9 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 ... + + true + @@ -921,6 +927,9 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected index 8cecd0b0e..9d277726d 100644 --- a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected +++ b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected @@ -178,6 +178,9 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 ... + + true + @@ -357,6 +360,9 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 ... + + true + diff --git a/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected b/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected index bbdae0801..183f66195 100644 --- a/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected +++ b/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected @@ -218,6 +218,9 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 ... + + true + diff --git a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected index f92e7b41c..de378c05e 100644 --- a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected +++ b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected @@ -218,6 +218,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0 ... + + true + diff --git a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected index 5aedc2472..38191a2a5 100644 --- a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected +++ b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected @@ -243,6 +243,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 ... + + true + diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected index 53f659d2f..5365fbc2e 100644 --- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected +++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected @@ -243,6 +243,9 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0 ... + + true + diff --git a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected index ffb7bd215..2df4e6e96 100644 --- a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected +++ b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected @@ -151,6 +151,9 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0 ... + + true + diff --git a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected index c0f1689d8..f6de1631b 100644 --- a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected +++ b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected @@ -210,6 +210,9 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 ... + + true + @@ -420,6 +423,9 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/Enum.init.cse.expected b/src/tests/integration/test-data/show/Enum.init.cse.expected index ce74733ad..3ae8d218c 100644 --- a/src/tests/integration/test-data/show/Enum.init.cse.expected +++ b/src/tests/integration/test-data/show/Enum.init.cse.expected @@ -126,6 +126,9 @@ module SUMMARY-TEST%ENUM.INIT:0 ... + + true + diff --git a/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected index 301980237..eba8e492d 100644 --- a/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected +++ b/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected @@ -181,6 +181,9 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 ... + + true + @@ -360,6 +363,9 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected b/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected index ec55d661a..baebcaa2d 100644 --- a/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected +++ b/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected @@ -127,6 +127,9 @@ module SUMMARY-SRC%CSE%IDENTITY.IDENTITY(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected index 1f8228cac..1c98af901 100644 --- a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected @@ -178,6 +178,9 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 ... + + true + @@ -359,6 +362,9 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected index 9dba4c635..f75a11a5a 100644 --- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected @@ -130,6 +130,9 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 ... + + true + diff --git a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected index 9a281653b..ac67e95af 100644 --- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected @@ -131,6 +131,9 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0 ... + + true + diff --git a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected index ae3e29fad..0264dbdaf 100644 --- a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected @@ -178,6 +178,9 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 ... + + true + @@ -357,6 +360,9 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected index f9008a595..59f7d8589 100644 --- a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected +++ b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected @@ -242,6 +242,9 @@ module SUMMARY-TEST%INTERFACETAGTEST.TESTINTERFACE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected index 50388a95f..0691827b9 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -254,6 +254,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ... + + true + @@ -511,6 +514,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ... + + true + @@ -767,6 +773,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ... + + true + @@ -1025,6 +1034,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ... + + true + @@ -1283,6 +1295,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected index fd52f3384..a908ac827 100644 --- a/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected +++ b/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected @@ -133,6 +133,9 @@ module SUMMARY-TEST%STATICCALLCONTRACT.SET(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected index f6fa3ddc7..a869046be 100644 --- a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected +++ b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected @@ -280,6 +280,9 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ... + + true + @@ -527,6 +530,9 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ... + + true + @@ -772,6 +778,9 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ... + + true + diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected index 31f7579ac..efa830fa6 100644 --- a/src/tests/integration/test-data/show/foundry.k.expected +++ b/src/tests/integration/test-data/show/foundry.k.expected @@ -4,6 +4,7 @@ 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" module FOUNDRY-MAIN imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION @@ -169,6 +170,7 @@ module FOUNDRY-MAIN imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION imports public KECCAK-LEMMAS + imports public NO-STACK-CHECKS diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected index 1ae5640b1..aea903c74 100644 --- a/src/tests/integration/test-data/show/gas-abstraction.expected +++ b/src/tests/integration/test-data/show/gas-abstraction.expected @@ -275,6 +275,9 @@ Node 6: + + true + @@ -549,6 +552,9 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 ... + + true + @@ -781,6 +787,9 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 ... + + true + @@ -1013,6 +1022,9 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 ... + + true + diff --git a/src/tests/integration/test-data/show/merge-loop-heads.expected b/src/tests/integration/test-data/show/merge-loop-heads.expected index 9b92e44f6..5121f2f27 100644 --- a/src/tests/integration/test-data/show/merge-loop-heads.expected +++ b/src/tests/integration/test-data/show/merge-loop-heads.expected @@ -350,6 +350,9 @@ Node 21: ... + + true + @@ -596,6 +599,9 @@ Node 22: ... + + true + @@ -842,6 +848,9 @@ Node 23: ... + + true + @@ -1085,6 +1094,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 ... + + true + @@ -1322,6 +1334,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 ... + + true + @@ -1560,6 +1575,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 ... + + true + @@ -1799,6 +1817,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 ... + + true + @@ -2040,6 +2061,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected index 3c95ee8d5..bf1239978 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected @@ -174,6 +174,9 @@ Node 20: ... + + true + @@ -419,6 +422,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ... + + true + diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected index 243bc04a1..43c0bc93d 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected @@ -173,6 +173,9 @@ Node 10: ... + + true + @@ -413,6 +416,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ... + + true + diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected index 0e7f2c536..5e3e79d84 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected @@ -218,6 +218,9 @@ Node 16: ... + + true + @@ -460,6 +463,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -701,6 +707,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + @@ -941,6 +950,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected index efb378b48..1950e7e11 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected @@ -216,6 +216,9 @@ Node 16: ... + + true + @@ -461,6 +464,9 @@ Node 15: ... + + true + @@ -705,6 +711,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -948,6 +957,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + @@ -1190,6 +1202,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected index 9d114eafd..854bb36cf 100644 --- a/src/tests/integration/test-data/show/node-refutation.expected +++ b/src/tests/integration/test-data/show/node-refutation.expected @@ -228,6 +228,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 ... + + true + @@ -466,6 +469,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 ... + + true + @@ -707,6 +713,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 ... + + true + @@ -948,6 +957,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 ... + + true + diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected index 45a4a0102..c5f9f03f8 100644 --- a/src/tests/integration/test-data/show/split-node.expected +++ b/src/tests/integration/test-data/show/split-node.expected @@ -430,6 +430,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -687,6 +690,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -946,6 +952,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -1206,6 +1215,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -1509,6 +1521,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -1808,6 +1823,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -2243,6 +2261,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -2676,6 +2697,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -3110,6 +3134,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -3547,6 +3574,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -3984,6 +4014,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -4424,6 +4457,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -4864,6 +4900,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -5165,6 +5204,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -5467,6 +5509,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -5765,6 +5810,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true + @@ -6063,6 +6111,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ... + + true +