From 0e3f7bf4b3a09fcb58f97f4f890e496befa991d4 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Sat, 15 Jul 2023 03:43:58 -0700 Subject: [PATCH 01/30] switch to pytest for regression testing --- .github/workflows/test.yml | 8 +- src/halmos/__main__.py | 92 +- tests/expected/all.json | 1771 ++++++++++++++++++++++++++ tests/expected/counter-symbolic.json | 244 ++++ tests/expected/list-symbolic.json | 52 + tests/expected/storage-symbolic.json | 100 ++ tests/test/Arith.t.sol | 6 +- tests/test/AssertTest.sol | 30 + tests/test/Block.t.sol | 12 +- tests/test/Byte.t.sol | 20 +- tests/test/Console.t.sol | 2 +- tests/test/Const.t.sol | 4 +- tests/test/Counter.t.sol | 36 +- tests/test/Create.t.sol | 12 +- tests/test/Deal.t.sol | 6 +- tests/test/Foundry.t.sol | 16 +- tests/test/Getter.t.sol | 13 + tests/test/HalmosCheatCode.t.sol | 22 +- tests/test/Invalid.t.sol | 10 +- tests/test/Library.t.sol | 2 +- tests/test/LibraryLinking.t.sol | 19 + tests/test/List.t.sol | 14 +- tests/test/Math.t.sol | 12 + tests/test/Opcode.t.sol | 24 +- tests/test/Prank.t.sol | 22 +- tests/test/Revert.t.sol | 40 + tests/test/Send.t.sol | 4 +- tests/test/Setup.t.sol | 2 +- tests/test/SetupPlus.t.sol | 4 +- tests/test/SetupSymbolic.t.sol | 12 + tests/test/SignExtend.t.sol | 2 +- tests/test/Solver.t.sol | 22 + tests/test/Storage.t.sol | 14 +- tests/test/Store.t.sol | 10 +- tests/test/Struct.t.sol | 5 +- tests/test/TestConstructor.t.sol | 12 + tests/test/UnsupportedOpcode.t.sol | 39 + tests/test/Warp.t.sol | 14 +- tests/test_halmos.py | 69 + 39 files changed, 2647 insertions(+), 151 deletions(-) create mode 100644 tests/expected/all.json create mode 100644 tests/expected/counter-symbolic.json create mode 100644 tests/expected/list-symbolic.json create mode 100644 tests/expected/storage-symbolic.json create mode 100644 tests/test/AssertTest.sol create mode 100644 tests/test/Getter.t.sol create mode 100644 tests/test/LibraryLinking.t.sol create mode 100644 tests/test/Math.t.sol create mode 100644 tests/test/Revert.t.sol create mode 100644 tests/test/SetupSymbolic.t.sol create mode 100644 tests/test/Solver.t.sol create mode 100644 tests/test/TestConstructor.t.sol create mode 100644 tests/test/UnsupportedOpcode.t.sol create mode 100644 tests/test_halmos.py diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index b6d92b33..57d2d18e 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -14,7 +14,6 @@ jobs: matrix: os: ["ubuntu-latest", "windows-2022"] python-version: ["3.8", "3.9", "3.10", "3.11", "3.8.13", "3.9.13", "3.10.6"] - parallel: ["", "--test-parallel", "--solver-parallel", "--test-parallel --solver-parallel"] exclude: # python 3.8.13 is not available in windows-2022 - os: "windows-2022" @@ -37,12 +36,7 @@ jobs: run: | python -m pip install --upgrade pip pip install pytest - - - name: Install Halmos - run: pip install -e . + pip install -r requirements.txt - name: Run pytest run: pytest - - - name: Test Halmos - run: halmos --root tests --symbolic-storage --function test ${{ matrix.parallel }} diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index a511e9cd..f452ab1b 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -9,7 +9,7 @@ import re import traceback -from dataclasses import dataclass +from dataclasses import dataclass, asdict from timeit import default_timer as timer from importlib import metadata @@ -101,6 +101,9 @@ def parse_args(args=None) -> argparse.Namespace: group_debug.add_argument( "--log", metavar="LOG_FILE_PATH", help="log every execution steps in JSON" ) + group_debug.add_argument( + "--json", metavar="JSON_FILE_PATH", help="output test results in JSON" + ) group_debug.add_argument( "--print-steps", action="store_true", help="print every execution steps" ) @@ -532,12 +535,22 @@ class ModelWithContext: result: CheckSatResult +@dataclass(frozen=True) +class TestResult: + name: str # test function name + exitcode: int # 0: passed, 1: failed, 2: setup failed, ... + num_models: int = None + num_paths: Tuple[int, int, int] = None # number of paths: [total, success, blocked] + time: Tuple[int, int, int] = None # time: [total, paths, models] + num_bounded_loops: int = None # number of incomplete loops + + def run( setup_ex: Exec, abi: List, fun_info: FunctionInfo, args: argparse.Namespace, -) -> int: +) -> TestResult: funname, funsig, funselector = fun_info.name, fun_info.sig, fun_info.selector if args.verbose >= 1: print(f"Executing {funname}") @@ -654,9 +667,10 @@ def run( passed = no_counterexample and normal > 0 and len(stuck) == 0 passfail = color_good("[PASS]") if passed else color_warn("[FAIL]") - time_info = f"{end - start:0.2f}s" + time_total, time_paths, time_models = end - start, mid - start, end - mid + time_info = f"{time_total:0.2f}s" if args.statistics: - time_info += f" (paths: {mid - start:0.2f}s, models: {end - mid:0.2f}s)" + time_info += f" (paths: {time_paths:0.2f}s, models: {time_models:0.2f}s)" # print result print( @@ -713,8 +727,14 @@ def run( with open(args.log, "w") as json_file: json.dump(steps, json_file) - # exitcode - return 0 if passed else 1 + return TestResult( + funsig, + 0 if passed else 1, # exitcode + sum(m.result == sat for m in models), + (len(exs), normal, len(stuck)), + (time_total, time_paths, time_models), + len(bounded_loops), + ) @dataclass(frozen=True) @@ -726,7 +746,7 @@ class SetupAndRunSingleArgs: args: argparse.Namespace -def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> int: +def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> List[TestResult]: try: setup_ex = setup( fn_args.hexcode, @@ -742,10 +762,10 @@ def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> int: ) if args.debug: traceback.print_exc() - return SETUP_FAILED + return [] try: - exitcode = run( + test_result = run( setup_ex, fn_args.abi, fn_args.fun_info, @@ -756,9 +776,9 @@ def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> int: print(color_warn(f"{type(err).__name__}: {err}")) if args.debug: traceback.print_exc() - return TEST_FAILED + return [TestResult(fn_args.fun_info.sig, 2)] - return exitcode + return [test_result] def extract_setup(methodIdentifiers: Dict[str, str]) -> FunctionInfo: @@ -790,7 +810,7 @@ class RunArgs: methodIdentifiers: Dict[str, str] -def run_parallel(run_args: RunArgs) -> Tuple[int, int]: +def run_parallel(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: hexcode, abi, methodIdentifiers = ( run_args.hexcode, run_args.abi, @@ -811,15 +831,16 @@ def run_parallel(run_args: RunArgs) -> Tuple[int, int]: ] # dispatch to the shared process pool - exitcodes = list(process_pool.map(setup_and_run_single, single_run_args)) + test_results = list(process_pool.map(setup_and_run_single, single_run_args)) + test_results = sum(test_results, []) # flatten lists - num_passed = exitcodes.count(0) - num_failed = len(exitcodes) - num_passed + num_passed = sum(r.exitcode == 0 for r in test_results) + num_failed = len(test_results) - num_passed - return num_passed, num_failed + return num_passed, num_failed, test_results -def run_sequential(run_args: RunArgs) -> Tuple[int, int]: +def run_sequential(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: setup_info = extract_setup(run_args.methodIdentifiers) if setup_info.sig and args.verbose >= 1: print(f"Running {setup_info.sig}") @@ -832,28 +853,32 @@ def run_sequential(run_args: RunArgs) -> Tuple[int, int]: ) if args.debug: traceback.print_exc() - return (0, 0) + return (0, 0, []) num_passed, num_failed = 0, 0 + test_results = [] for funsig in run_args.funsigs: fun_info = FunctionInfo( funsig.split("(")[0], funsig, run_args.methodIdentifiers[funsig] ) try: - exitcode = run(setup_ex, run_args.abi, fun_info, args) + test_result = run(setup_ex, run_args.abi, fun_info, args) except Exception as err: print(f"{color_warn('[SKIP]')} {funsig}") print(color_warn(f"{type(err).__name__}: {err}")) if args.debug: traceback.print_exc() num_failed += 1 + test_results.append(TestResult(funsig, 2)) continue - if exitcode == 0: + + test_results.append(test_result) + if test_result.exitcode == 0: num_passed += 1 else: num_failed += 1 - return (num_passed, num_failed) + return (num_passed, num_failed, test_results) @dataclass(frozen=True) @@ -1089,7 +1114,7 @@ def parse_build_out(args: argparse.Namespace) -> Dict: return result -def main() -> int: +def main(argv=None, test_results_map=None) -> int: main_start = timer() # @@ -1105,7 +1130,7 @@ def main() -> int: # global args - args = parse_args() + args = parse_args(argv) if args.version: print(f"Halmos {metadata.version('halmos')}") @@ -1153,6 +1178,9 @@ def main() -> int: total_failed = 0 total_found = 0 + if args.json and test_results_map is None: + test_results_map = {} + for compiler_version in sorted(build_out): build_out_map = build_out[compiler_version] for filename in sorted(build_out_map): @@ -1176,14 +1204,15 @@ def main() -> int: if funsigs: total_found += len(funsigs) - print( - f"\nRunning {len(funsigs)} tests for {contract_json['ast']['absolutePath']}:{contract_name}" + contract_path = ( + f"{contract_json['ast']['absolutePath']}:{contract_name}" ) + print(f"\nRunning {len(funsigs)} tests for {contract_path}") contract_start = timer() run_args = RunArgs(funsigs, hexcode, abi, methodIdentifiers) enable_parallel = args.test_parallel and len(funsigs) > 1 - num_passed, num_failed = ( + num_passed, num_failed, test_results = ( run_parallel(run_args) if enable_parallel else run_sequential(run_args) @@ -1195,8 +1224,19 @@ def main() -> int: total_passed += num_passed total_failed += num_failed + if test_results_map is not None: + if contract_path in test_results_map: + raise ValueError("already exists", contract_path) + test_results_map[contract_path] = list( + map(asdict, test_results) + ) + main_end = timer() + if args.json: + with open(args.json, "w") as json_file: + json.dump(test_results_map, json_file) + if args.statistics: print( f"\n[time] total: {main_end - main_start:0.2f}s (build: {main_mid - main_start:0.2f}s, tests: {main_end - main_mid:0.2f}s)" diff --git a/tests/expected/all.json b/tests/expected/all.json new file mode 100644 index 00000000..c394837f --- /dev/null +++ b/tests/expected/all.json @@ -0,0 +1,1771 @@ +{ + "test/Invalid.t.sol:OldCompilerTest": [ + { + "name": "checkAssert(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.006792041007429361, + 0.006783832999644801, + 8.208007784560323e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkMyAssert(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.007092082989402115, + 0.006427499989513308, + 0.0006645829998888075 + ], + "num_bounded_loops": 0 + } + ], + "test/Arith.t.sol:ArithTest": [ + { + "name": "checkExp(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.007170666998717934, + 0.0071627919969614595, + 7.875001756474376e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkMod(uint256,uint256,address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.01046979200327769, + 0.010462334001203999, + 7.458002073690295e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/AssertTest.sol:CTest": [ + { + "name": "checkBar()", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 2, + 0, + 0 + ], + "time": [ + 0.10647333299857564, + 0.10532550001516938, + 0.0011478329834062606 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkFoo()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02516283400473185, + 0.025157959025818855, + 4.8749789129942656e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Block.t.sol:BlockCheatCodeTest": [ + { + "name": "checkChainId(uint64)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.012892416008980945, + 0.012884875002782792, + 7.5410061981529e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkCoinbase(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.012101457978133112, + 0.012094707984942943, + 6.749993190169334e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkDifficulty(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.009351707994937897, + 0.009346916020149365, + 4.791974788531661e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkFee(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.008611708995886147, + 0.008606417017290369, + 5.291978595778346e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkRoll(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.008901083987439051, + 0.008895249979104847, + 5.8340083342045546e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarp(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.00978820800082758, + 0.0097822499810718, + 5.958019755780697e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Byte.t.sol:ByteTest": [ + { + "name": "checkByte(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 6, + 2, + 0 + ], + "time": [ + 0.10002066701417789, + 0.05631445799372159, + 0.0437062090204563 + ], + "num_bounded_loops": 0 + } + ], + "test/Byte.t.sol:SymbolicByteTest": [ + { + "name": "checkSymbolicByteIndex(uint8,uint8)", + "exitcode": 1, + "num_models": 2, + "num_paths": [ + 6, + 1, + 0 + ], + "time": [ + 0.028774250007700175, + 0.02722508300212212, + 0.001549167005578056 + ], + "num_bounded_loops": 0 + } + ], + "test/Console.t.sol:ConsoleTest": [ + { + "name": "checkLog()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.010688374983146787, + 0.01068245799979195, + 5.916983354836702e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Const.t.sol:ConstTest": [ + { + "name": "checkConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.003543416998581961, + 0.0035386669915169477, + 4.750007065013051e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Const.t.sol:ConstTestTest": [ + { + "name": "checkConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.00376158399740234, + 0.003757500002393499, + 4.083995008841157e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Counter.t.sol:CounterTest": [ + { + "name": "checkDiv1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 2, + 0 + ], + "time": [ + 0.008028250013012439, + 0.008022708003409207, + 5.542009603232145e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkDiv2(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 2, + 0 + ], + "time": [ + 0.008344333997229114, + 0.008339084015460685, + 5.249981768429279e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkFoo(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 17, + 16, + 0 + ], + "time": [ + 0.0931020829884801, + 0.09307670799898915, + 2.5374989490956068e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkInc()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.007204166991868988, + 0.007199874991783872, + 4.292000085115433e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkIncBy(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.006024375004926696, + 0.006020500004524365, + 3.875000402331352e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkIncOpt()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.00583899999037385, + 0.005834999989019707, + 4.0000013541430235e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkLoopConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.009400084003573284, + 0.009396250010468066, + 3.8339931052178144e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkLoopConstIf()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02649008299340494, + 0.026484457979677245, + 5.62501372769475e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkLoopDoWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 6, + 4, + 0 + ], + "time": [ + 0.023103666986571625, + 0.023094042000593618, + 9.624985978007317e-06 + ], + "num_bounded_loops": 1 + }, + { + "name": "checkLoopFor(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 3, + 0 + ], + "time": [ + 0.018659833003766835, + 0.01864958298392594, + 1.025001984089613e-05 + ], + "num_bounded_loops": 1 + }, + { + "name": "checkLoopWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 3, + 0 + ], + "time": [ + 0.018609833990922198, + 0.018600874987896532, + 8.95900302566588e-06 + ], + "num_bounded_loops": 1 + }, + { + "name": "checkMulDiv(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 4, + 0 + ], + "time": [ + 0.07291600000462495, + 0.0729067079955712, + 9.292009053751826e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSet(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.005909416999202222, + 0.005904332996578887, + 5.084002623334527e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetString(uint256,string,uint256,string,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02962820799439214, + 0.029622333007864654, + 5.874986527487636e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetSum(uint248,uint248)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 1, + 0 + ], + "time": [ + 0.024045666999882087, + 0.024035166978137568, + 1.0500021744519472e-05 + ], + "num_bounded_loops": 0 + } + ], + "test/Create.t.sol:CreateTest": [ + { + "name": "checkConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.016407249990152195, + 0.016401541011873633, + 5.7089782785624266e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkImmutable()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.015087000007042661, + 0.015082625002833083, + 4.375004209578037e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkInitialized()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.014679749991046265, + 0.014675749989692122, + 4.0000013541430235e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSet(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.030553457996575162, + 0.03054887501639314, + 4.582980182021856e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Deal.t.sol:DealTest": [ + { + "name": "checkDeal1(address,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.013186916999984533, + 0.013181042013457045, + 5.874986527487636e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkDeal2(address,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.016927541990298778, + 0.0169214999768883, + 6.04201341047883e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkDealNew()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.016635584004689008, + 0.016630625003017485, + 4.959001671522856e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Foundry.t.sol:FoundryTest": [ + { + "name": "checkAssume(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.009323125006631017, + 0.009317625022958964, + 5.499983672052622e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkEtchConcrete()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.016670041979523376, + 0.01666495797690004, + 5.084002623334527e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkEtchOverwrite()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02786154198111035, + 0.027856041997438297, + 5.499983672052622e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkGetCode(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.46927079098531976, + 0.4692655830003787, + 5.207984941080213e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Getter.t.sol:GetterTest": [ + { + "name": "checkGetter(uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 3, + 0, + 1 + ], + "time": [ + 0.006775084009859711, + 0.006768666993593797, + 6.417016265913844e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/HalmosCheatCode.t.sol:HalmosCheatCodeTest": [ + { + "name": "checkFailUnknownCheatcode()", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 2, + 0, + 1 + ], + "time": [ + 0.0063777079922147095, + 0.006372917006956413, + 4.790985258296132e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolLabel()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 1, + 0 + ], + "time": [ + 0.051910667010815814, + 0.05190024999319576, + 1.0417017620056868e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolicAddress()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.011195333005161956, + 0.011190958000952378, + 4.375004209578037e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolicBool()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 2, + 0 + ], + "time": [ + 0.012926708004670218, + 0.012920708017190918, + 5.999987479299307e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolicBytes()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02052141699823551, + 0.02051549998577684, + 5.917012458667159e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolicBytes32()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.00990520798950456, + 0.009900542005198076, + 4.665984306484461e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolicUint()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.024763166991760954, + 0.02475808298913762, + 5.084002623334527e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSymbolicUint256()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.010339250002289191, + 0.010333915997762233, + 5.3340045269578695e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Library.t.sol:LibraryTest": [ + { + "name": "checkAdd(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.004304542002500966, + 0.004299583000829443, + 4.959001671522856e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/LibraryLinking.t.sol:LibTest": [], + "test/LibraryLinking.t.sol:LibTest2": [ + { + "name": "checkBar()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.0032639590208418667, + 0.0032595000229775906, + 4.458997864276171e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/List.t.sol:ListTest": [ + { + "name": "checkAdd(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.01591579199885018, + 0.015911082999082282, + 4.708999767899513e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkRemove()", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 1, + 0, + 0 + ], + "time": [ + 0.007327958010137081, + 0.007324333011638373, + 3.6249984987080097e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSet(uint256,uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 1, + 0, + 0 + ], + "time": [ + 0.00863666701479815, + 0.00863216700963676, + 4.5000051613897085e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/List.t.sol:ListTestTest": [ + { + "name": "checkAdd(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.08320020799874328, + 0.08319529198342934, + 4.91601531393826e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkRemove()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.054968792013823986, + 0.054963958013104275, + 4.8340007197111845e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSet(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.06289233299321495, + 0.06288745798519813, + 4.875008016824722e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Math.t.sol:MathTest": [ + { + "name": "checkAvg(uint256,uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.07157470801030286, + 0.01126283299527131, + 0.060311875015031546 + ], + "num_bounded_loops": 0 + } + ], + "test/Opcode.t.sol:OpcodeTest": [ + { + "name": "checkPush0()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02399954100837931, + 0.02399524999782443, + 4.291010554879904e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "check_SIGNEXTEND(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 33, + 32, + 0 + ], + "time": [ + 0.28771620901534334, + 0.28766833400004543, + 4.787501529790461e-05 + ], + "num_bounded_loops": 0 + } + ], + "test/Prank.t.sol:PrankSetUpTest": [ + { + "name": "checkPrank(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.040319375024409965, + 0.04031275000306778, + 6.62502134218812e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Prank.t.sol:PrankTest": [ + { + "name": "checkPrank(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.061628583003766835, + 0.061621666012797505, + 6.916990969330072e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkPrankExternal(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.05262120798579417, + 0.05261449998943135, + 6.707996362820268e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkPrankExternalSelf(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.05366733399569057, + 0.0536605000088457, + 6.833986844867468e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkPrankInternal(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.03688741699443199, + 0.03687945901765488, + 7.957976777106524e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkPrankNew(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.04577312499168329, + 0.04576516701490618, + 7.957976777106524e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkPrankReset1(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.03653045801911503, + 0.03652370799682103, + 6.750022293999791e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkPrankReset2(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.03804066698648967, + 0.03803404199425131, + 6.624992238357663e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkStartPrank(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.1221603750018403, + 0.12215379098779522, + 6.584014045074582e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkStopPrank1(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.04132283298531547, + 0.041314665984828025, + 8.167000487446785e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkStopPrank2()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.031720458006020635, + 0.03171566600212827, + 4.792003892362118e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Revert.t.sol:CTest": [ + { + "name": "checkRevert1(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 3, + 0, + 0 + ], + "time": [ + 0.04121337499236688, + 0.0408095839957241, + 0.0004037909966427833 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkRevert2(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.03911733301356435, + 0.039110417012125254, + 6.9160014390945435e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Send.t.sol:SendTest": [ + { + "name": "checkSend(address,uint256,address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 8, + 1, + 0 + ], + "time": [ + 0.03954100000555627, + 0.03952391701750457, + 1.7082988051697612e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSendSelf(address,uint256,address)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 8, + 1, + 0 + ], + "time": [ + 0.03625720800482668, + 0.036242500005755574, + 1.4707999071106315e-05 + ], + "num_bounded_loops": 0 + } + ], + "test/Setup.t.sol:SetupTest": [ + { + "name": "checkTrue()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.04295708300196566, + 0.04295220799394883, + 4.875008016824722e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/SetupPlus.t.sol:SetupPlusTest": [ + { + "name": "checkSetup()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.034146124991821125, + 0.03414112501195632, + 4.999979864805937e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/SetupPlus.t.sol:SetupPlusTestB": [ + { + "name": "checkSetup()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.049622124992311, + 0.049617707991274074, + 4.417001036927104e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/SetupSymbolic.t.sol:SetupSymbolicTest": [ + { + "name": "checkFoo()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.003194707998773083, + 0.0031905829964671284, + 4.125002305954695e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/SignExtend.t.sol:SignExtendTest": [ + { + "name": "checkSignExtend(int16)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.061022916983347386, + 0.06101416700403206, + 8.749979315325618e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Solver.t.sol:SolverTest": [ + { + "name": "checkFoo(uint256,uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 9, + 4, + 0 + ], + "time": [ + 1.0501290000102017, + 0.04364512499887496, + 1.0064838750113267 + ], + "num_bounded_loops": 0 + } + ], + "test/SrcMap.t.sol:SrcMapTest": [ + { + "name": "checkIf(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.008314832986798137, + 0.008048832998611033, + 0.00026599998818710446 + ], + "num_bounded_loops": 0 + } + ], + "test/Storage.t.sol:StorageTest": [ + { + "name": "checkAddArr1(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.010458083997946233, + 0.010453750001033768, + 4.3339969124644995e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkAddArr2(uint256,uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 2, + 0, + 0 + ], + "time": [ + 0.006222666008397937, + 0.0062180410022847354, + 4.62500611320138e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkAddMap1Arr1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.017453957989346236, + 0.01744825000059791, + 5.707988748326898e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetMap1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.006097791017964482, + 0.006093916017562151, + 3.875000402331352e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetMap2(uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.008013749989913777, + 0.008009665994904935, + 4.083995008841157e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetMap3(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.009471625002333894, + 0.00946745800320059, + 4.1669991333037615e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Store.t.sol:StoreTest": [ + { + "name": "checkStoreArray(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.0750039579870645, + 0.07499720799387433, + 6.749993190169334e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkStoreMapping(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.045630125008756295, + 0.04562462499598041, + 5.5000127758830786e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkStoreScalar(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.02935466601047665, + 0.029350249998969957, + 4.416011506691575e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Struct.t.sol:StructTest": [ + { + "name": "checkStruct((uint256,uint256))", + "exitcode": 2, + "num_models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/TestConstructor.t.sol:TestConstructorTest": [ + { + "name": "checkValue()", + "exitcode": 1, + "num_models": 1, + "num_paths": [ + 2, + 0, + 0 + ], + "time": [ + 0.005449541989946738, + 0.005120167013956234, + 0.000329374975990504 + ], + "num_bounded_loops": 0 + } + ], + "test/UnsupportedOpcode.t.sol:X": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 2, + 0, + 1 + ], + "time": [ + 0.00361879201955162, + 0.0036138340074103326, + 4.958012141287327e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/UnsupportedOpcode.t.sol:Y": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 2, + 0, + 1 + ], + "time": [ + 0.010356249986216426, + 0.010351292003178969, + 4.95798303745687e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/UnsupportedOpcode.t.sol:Z": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 0, + "num_paths": [ + 2, + 0, + 1 + ], + "time": [ + 0.021697415999369696, + 0.02169258298818022, + 4.8330111894756556e-06 + ], + "num_bounded_loops": 0 + } + ], + "test/Warp.t.sol:WarpTest": [ + { + "name": "checkWarp(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.011706249992130324, + 0.011701832991093397, + 4.417001036927104e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarpExternal(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.028597750002518296, + 0.028592999995453283, + 4.750007065013051e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarpExternalSelf(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.03017012498457916, + 0.030165417003445327, + 4.7079811338335276e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarpInternal(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.013198832981288433, + 0.013193124992540106, + 5.707988748326898e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarpNew(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.03445437498157844, + 0.03444954098085873, + 4.8340007197111845e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarpReset(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.017815165978390723, + 0.017809415992815048, + 5.749985575675964e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkWarpSetUp()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.007120875001419336, + 0.007116541994037107, + 4.3330073822289705e-06 + ], + "num_bounded_loops": 0 + } + ] +} diff --git a/tests/expected/counter-symbolic.json b/tests/expected/counter-symbolic.json new file mode 100644 index 00000000..824c812b --- /dev/null +++ b/tests/expected/counter-symbolic.json @@ -0,0 +1,244 @@ +{ + "test/Counter.t.sol:CounterTest": [ + { + "name": "checkDiv1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 2, + 0 + ], + "time": [ + 0.009959374991012737, + 0.009951167012332007, + 8.207978680729866e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkDiv2(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 2, + 0 + ], + "time": [ + 0.00888091602246277, + 0.008866500022122636, + 1.4416000340133905e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkFoo(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 47, + 16, + 0 + ], + "time": [ + 0.21995554098975845, + 0.21987691600224935, + 7.862498750910163e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkInc()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.027028792013879865, + 0.01539937499910593, + 0.011629417014773935 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkIncBy(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 2, + 0 + ], + "time": [ + 0.016327749995980412, + 0.01632145798066631, + 6.292015314102173e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkIncOpt()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.025245500000892207, + 0.013565540983108804, + 0.011679959017783403 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkLoopConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 1, + 0 + ], + "time": [ + 0.030433334002736956, + 0.02264291699975729, + 0.007790417002979666 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkLoopConstIf()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 77, + 16, + 0 + ], + "time": [ + 1.538891167001566, + 0.6547999999893364, + 0.8840911670122296 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkLoopDoWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 20, + 5, + 0 + ], + "time": [ + 0.14874658299959265, + 0.09308420799789019, + 0.05566237500170246 + ], + "num_bounded_loops": 1 + }, + { + "name": "checkLoopFor(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 19, + 5, + 0 + ], + "time": [ + 0.1373970830172766, + 0.08692545801750384, + 0.05047162499977276 + ], + "num_bounded_loops": 1 + }, + { + "name": "checkLoopWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 19, + 5, + 0 + ], + "time": [ + 0.1446185829991009, + 0.08712587499758229, + 0.05749270800151862 + ], + "num_bounded_loops": 1 + }, + { + "name": "checkMulDiv(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 4, + 0 + ], + "time": [ + 0.07496475000516511, + 0.07495608300087042, + 8.66700429469347e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSet(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.00604049998219125, + 0.006035083992173895, + 5.415990017354488e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetString(uint256,string,uint256,string,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.03229575001751073, + 0.03228700000909157, + 8.750008419156075e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetSum(uint248,uint248)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 1, + 0 + ], + "time": [ + 0.023321624990785494, + 0.02331225000671111, + 9.374984074383974e-06 + ], + "num_bounded_loops": 0 + } + ] +} diff --git a/tests/expected/list-symbolic.json b/tests/expected/list-symbolic.json new file mode 100644 index 00000000..38c86e38 --- /dev/null +++ b/tests/expected/list-symbolic.json @@ -0,0 +1,52 @@ +{ + "test/List.t.sol:ListTest": [ + { + "name": "checkAdd(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.054170040995813906, + 0.0343787909951061, + 0.019791250000707805 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkRemove()", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 3, + 1, + 0 + ], + "time": [ + 0.06059570799698122, + 0.019172542000887915, + 0.0414231659960933 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSet(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.014601791015593335, + 0.01459545799298212, + 6.333022611215711e-06 + ], + "num_bounded_loops": 0 + } + ] +} diff --git a/tests/expected/storage-symbolic.json b/tests/expected/storage-symbolic.json new file mode 100644 index 00000000..21104590 --- /dev/null +++ b/tests/expected/storage-symbolic.json @@ -0,0 +1,100 @@ +{ + "test/Storage.t.sol:StorageTest": [ + { + "name": "checkAddArr1(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.022341417003190145, + 0.022330749983666465, + 1.066701952368021e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkAddArr2(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 5, + 1, + 0 + ], + "time": [ + 0.07018687500385568, + 0.07016733300406486, + 1.95419997908175e-05 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkAddMap1Arr1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 4, + 1, + 0 + ], + "time": [ + 0.028902583988383412, + 0.02889408401097171, + 8.499977411702275e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetMap1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.006448500003898516, + 0.006442875019274652, + 5.624984623864293e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetMap2(uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.008583459013607353, + 0.008578334003686905, + 5.125009920448065e-06 + ], + "num_bounded_loops": 0 + }, + { + "name": "checkSetMap3(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": [ + 2, + 1, + 0 + ], + "time": [ + 0.0095768750179559, + 0.009572500013746321, + 4.375004209578037e-06 + ], + "num_bounded_loops": 0 + } + ] +} diff --git a/tests/test/Arith.t.sol b/tests/test/Arith.t.sol index a17ca944..7b0cfce6 100644 --- a/tests/test/Arith.t.sol +++ b/tests/test/Arith.t.sol @@ -9,7 +9,7 @@ contract ArithTest { } } - function testMod(uint x, uint y, address addr) public pure { + function checkMod(uint x, uint y, address addr) public pure { unchecked { assert(unchecked_mod(x, 0) == 0); // compiler rejects `x % 0` assert(x % 1 == 0); @@ -17,14 +17,14 @@ contract ArithTest { assert(x % 4 < 4); uint x_mod_y = unchecked_mod(x, y); - // assert(x_mod_y == 0 || x_mod_y < y); + // assert(x_mod_y == 0 || x_mod_y < y); // not supported // TODO: support more axioms assert(x_mod_y <= y); assert(uint256(uint160(addr)) % (2**160) == uint256(uint160(addr))); } } - function testExp(uint x) public pure { + function checkExp(uint x) public pure { unchecked { assert(x ** 0 == 1); // 0 ** 0 == 1 assert(x ** 1 == x); diff --git a/tests/test/AssertTest.sol b/tests/test/AssertTest.sol new file mode 100644 index 00000000..e1b21d10 --- /dev/null +++ b/tests/test/AssertTest.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; + +contract C is Test { + function foo() public pure { + assert(false); // not propagated + } + + function bar() public { + fail(); // propagated + } +} + +contract CTest is Test { + C c; + + function setUp() public { + c = new C(); + } + + function checkFoo() public { + address(c).call(abi.encodeWithSelector(C.foo.selector, bytes(""))); // pass + } + + function checkBar() public { + address(c).call(abi.encodeWithSelector(C.bar.selector, bytes(""))); // fail + } +} diff --git a/tests/test/Block.t.sol b/tests/test/Block.t.sol index 2f842c95..531a3d88 100644 --- a/tests/test/Block.t.sol +++ b/tests/test/Block.t.sol @@ -4,32 +4,32 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; contract BlockCheatCodeTest is Test { - function testFee(uint x) public { + function checkFee(uint x) public { vm.fee(x); assert(block.basefee == x); } - function testChainId(uint64 x) public { + function checkChainId(uint64 x) public { vm.chainId(x); assert(block.chainid == x); } - function testCoinbase(address x) public { + function checkCoinbase(address x) public { vm.coinbase(x); assert(block.coinbase == x); } - function testDifficulty(uint x) public { + function checkDifficulty(uint x) public { vm.difficulty(x); assert(block.difficulty == x); } - function testRoll(uint x) public { + function checkRoll(uint x) public { vm.roll(x); assert(block.number == x); } - function testWarp(uint x) public { + function checkWarp(uint x) public { vm.warp(x); assert(block.timestamp == x); } diff --git a/tests/test/Byte.t.sol b/tests/test/Byte.t.sol index 6557cab5..29a8219b 100644 --- a/tests/test/Byte.t.sol +++ b/tests/test/Byte.t.sol @@ -2,27 +2,37 @@ pragma solidity >=0.8.0 <0.9.0; contract ByteTest { - function byte1(uint i, uint x) public returns (uint r) { + function byte1(uint i, uint x) public pure returns (uint r) { assembly { r := byte(i, x) } } - function byte2(uint i, uint x) public returns (uint) { + function byte2(uint i, uint x) public pure returns (uint) { if (i >= 32) return 0; return (x >> (248-i*8)) & 0xff; } - function byte3(uint i, uint x) public returns (uint) { + function byte3(uint i, uint x) public pure returns (uint) { if (i >= 32) return 0; bytes memory b = new bytes(32); assembly { mstore(add(b, 32), x) } return uint(uint8(bytes1(b[i]))); // TODO: Not supported: MLOAD symbolic memory offset: 160 + p_i_uint256 } - function testByte(uint i, uint x) public { + function checkByte(uint i, uint x) pure public { uint r1 = byte1(i, x); uint r2 = byte2(i, x); - // uint r3 = byte3(i, x); + // uint r3 = byte3(i, x); // not supported assert(r1 == r2); // assert(r1 == r3); } } + +contract SymbolicByteTest { + function checkSymbolicByteIndex(uint8 x, uint8 i) public pure returns (uint r) { + if (x > 10) assert(false); // expected to fail + assembly { + r := byte(i, x) + } + assert(r == 0); // expected to fail with counterexample + } +} diff --git a/tests/test/Console.t.sol b/tests/test/Console.t.sol index 2c6cc662..f6cde7d5 100644 --- a/tests/test/Console.t.sol +++ b/tests/test/Console.t.sol @@ -4,7 +4,7 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; contract ConsoleTest is Test { - function testLog() public { + function checkLog() public view { console.log(0); console.log(1); } diff --git a/tests/test/Const.t.sol b/tests/test/Const.t.sol index 712206e9..e729d544 100644 --- a/tests/test/Const.t.sol +++ b/tests/test/Const.t.sol @@ -5,13 +5,13 @@ import "forge-std/Test.sol"; import "../src/Const.sol"; contract ConstTest is Const { - function testConst() public pure { + function checkConst() public pure { assert(const == 11); } } contract ConstTestTest is Const, Test { - function testConst() public { + function checkConst() public { assertEq(const, 11); } } diff --git a/tests/test/Counter.t.sol b/tests/test/Counter.t.sol index beddeb0c..9fa9b9e8 100644 --- a/tests/test/Counter.t.sol +++ b/tests/test/Counter.t.sol @@ -1,22 +1,24 @@ // SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0; +// NOTE: required options: --loop 4 --symbolic-storage + import "../src/Counter.sol"; contract CounterTest is Counter { - function testSet(uint n) public { + function checkSet(uint n) public { set(n); assert(cnt == n); } - function testInc() public { + function checkInc() public { uint oldCnt = cnt; inc(); assert(cnt > oldCnt); assert(cnt == oldCnt + 1); } - function testIncOpt() public { + function checkIncOpt() public { uint oldCnt = cnt; require(cnt < type(uint).max); incOpt(); @@ -24,7 +26,7 @@ contract CounterTest is Counter { assert(cnt == oldCnt + 1); } - function testIncBy(uint n) public { + function checkIncBy(uint n) public { uint oldCnt = cnt; incBy(n); assert(cnt < oldCnt || cnt == oldCnt + n); // cnt >= oldCnt ==> cnt == oldCnt + n @@ -36,7 +38,7 @@ contract CounterTest is Counter { assert(cnt >= oldCnt); assert(cnt == oldCnt + n); } - function testLoopFor(uint8 k) public { + function checkLoopFor(uint8 k) public { specLoopFor(k); } @@ -46,7 +48,7 @@ contract CounterTest is Counter { assert(cnt >= oldCnt); assert(cnt == oldCnt + n); } - function testLoopWhile(uint8 k) public { + function checkLoopWhile(uint8 k) public { specLoopWhile(k); } @@ -57,18 +59,18 @@ contract CounterTest is Counter { if (n == 0) assert(cnt == oldCnt + 1); else assert(cnt == oldCnt + n); } - function testLoopDoWhile(uint8 k) public { + function checkLoopDoWhile(uint8 k) public { specLoopDoWhile(k); } - function testLoopConst() public { + function checkLoopConst() public { uint oldCnt = cnt; loopConst(); assert(cnt >= oldCnt); assert(cnt == oldCnt + 2); } - function testLoopConstIf() public { + function checkLoopConstIf() public { uint oldCnt = cnt; loopConstIf(); assert(cnt >= oldCnt); @@ -79,36 +81,36 @@ contract CounterTest is Counter { setSum(arr); assert(cnt == arr[0] + arr[1]); } - function testSetSum(uint248 a, uint248 b) public { + function checkSetSum(uint248 a, uint248 b) public { specSetSum([uint(a), b]); } - function testSetString(uint, string memory s, uint, string memory r, uint) public { + function checkSetString(uint, string memory s, uint, string memory r, uint) public { uint oldCnt = cnt; setString(s); setString(r); assert(cnt == oldCnt + bytes(s).length + bytes(r).length); } - function testFoo(uint a, uint b, uint c, uint d) public { + function checkFoo(uint a, uint b, uint c, uint d) public { uint oldCnt = cnt; foo(a, b, c, d); assert(cnt == oldCnt + 4); } - function testDiv1(uint x, uint y) public pure { + function checkDiv1(uint x, uint y) public pure { if (y > 0) { assert(x / y <= x); } } - function testDiv2(uint x, uint y) public pure { + function checkDiv2(uint x, uint y) public pure { if (y > 0) { assert(x / y == x / y); } } - function testMulDiv(uint x, uint y) public pure { + function checkMulDiv(uint x, uint y) public pure { unchecked { if (x > 0 && y > 0) { uint z = x * y; @@ -120,8 +122,8 @@ contract CounterTest is Counter { } } - /* TODO: support testFail prefix - function testFail() public pure { + /* TODO: support checkFail prefix + function checkFail() public pure { require(false); // deadcode } diff --git a/tests/test/Create.t.sol b/tests/test/Create.t.sol index dd019630..59d6d7f8 100644 --- a/tests/test/Create.t.sol +++ b/tests/test/Create.t.sol @@ -11,26 +11,26 @@ contract CreateTest is Test { create = new Create(0x220E); } - /* TODO: support testFail prefix - function testFailSetUp() public { + /* TODO: support checkFail prefix + function checkFailSetUp() public { assertEq(create.value(), 0); } */ - function testSet(uint x) public { + function checkSet(uint x) public { create.set(x); assertEq(create.value(), x); } - function testImmutable() public { + function checkImmutable() public { assertEq(create.halmos(), 0x220E); } - function testInitialized() public { + function checkInitialized() public { assertEq(create.initialized(), 7); } - function testConst() public { + function checkConst() public { assertEq(create.const(), 11); } } diff --git a/tests/test/Deal.t.sol b/tests/test/Deal.t.sol index 49470e1b..81a395a6 100644 --- a/tests/test/Deal.t.sol +++ b/tests/test/Deal.t.sol @@ -6,18 +6,18 @@ import "forge-std/Test.sol"; contract DealTest is Test { C c; - function testDeal1(address payable receiver, uint amount) public { + function checkDeal1(address payable receiver, uint amount) public { vm.deal(receiver, amount); assert(receiver.balance == amount); } - function testDeal2(address payable receiver, uint amount1, uint amount2) public { + function checkDeal2(address payable receiver, uint amount1, uint amount2) public { vm.deal(receiver, amount1); vm.deal(receiver, amount2); // reset the balance, not increasing assert(receiver.balance == amount2); } - function testDealNew() public { + function checkDealNew() public { vm.deal(address(this), 3 ether); c = new C{value: 3 ether}(); diff --git a/tests/test/Foundry.t.sol b/tests/test/Foundry.t.sol index 955dd184..d46924fe 100644 --- a/tests/test/Foundry.t.sol +++ b/tests/test/Foundry.t.sol @@ -7,18 +7,18 @@ import "forge-std/StdCheats.sol"; import "../src/Counter.sol"; contract FoundryTest is Test { - /* TODO: support testFail prefix - function testFail() public { + /* TODO: support checkFail prefix + function checkFail() public { assertTrue(false); } */ - function testAssume(uint x) public { + function checkAssume(uint x) public { vm.assume(x < 10); assertLt(x, 100); } - function testGetCode(uint x) public { + function checkGetCode(uint x) public { Counter counter = Counter(deployCode("./out/Counter.sol/Counter.json")); counter.set(x); assertEq(counter.cnt(), x); @@ -28,7 +28,7 @@ contract FoundryTest is Test { assertEq(counter2.cnt(), x); } - function testEtchConcrete() public { + function checkEtchConcrete() public { vm.etch(address(0x42), hex"60425f526001601ff3"); (bool success, bytes memory retval) = address(0x42).call(""); @@ -37,7 +37,7 @@ contract FoundryTest is Test { assertEq(uint256(uint8(retval[0])), 0x42); } - function testEtchOverwrite() public { + function checkEtchOverwrite() public { vm.etch(address(0x42), hex"60425f526001601ff3"); (, bytes memory retval) = address(0x42).call(""); @@ -52,7 +52,7 @@ contract FoundryTest is Test { } /// @notice etching to a symbolic address is not supported - // function testEtchSymbolicAddr(address who) public { + // function checkEtchSymbolicAddr(address who) public { // vm.etch(who, hex"60425f526001601ff3"); // (bool success, bytes memory retval) = who.call(""); @@ -62,7 +62,7 @@ contract FoundryTest is Test { // } /// @notice etching symbolic code is not supported - // function testEtchFullSymbolic(address who, bytes memory code) public { + // function checkEtchFullSymbolic(address who, bytes memory code) public { // vm.etch(who, code); // assertEq(code, who.code); // } diff --git a/tests/test/Getter.t.sol b/tests/test/Getter.t.sol new file mode 100644 index 00000000..831db4f5 --- /dev/null +++ b/tests/test/Getter.t.sol @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +// from https://github.com/a16z/halmos/issues/82 + +contract GetterTest { + uint256[3] v; + uint w; + + function checkGetter(uint256 i) public view { + assert(v[i] >= 0); // unsupported static storage arrays + } +} diff --git a/tests/test/HalmosCheatCode.t.sol b/tests/test/HalmosCheatCode.t.sol index 41993945..72310b33 100644 --- a/tests/test/HalmosCheatCode.t.sol +++ b/tests/test/HalmosCheatCode.t.sol @@ -29,7 +29,7 @@ abstract contract SymTest { } contract HalmosCheatCodeTest is SymTest { - function testSymbolicUint() public { + function checkSymbolicUint() public { uint x = svm.createUint(256, 'x'); uint y = svm.createUint(160, 'y'); uint z = svm.createUint(8, 'z'); @@ -38,7 +38,7 @@ contract HalmosCheatCodeTest is SymTest { assert(0 <= z && z <= type(uint8).max); } - function testSymbolicBytes() public { + function checkSymbolicBytes() public { bytes memory data = svm.createBytes(2, 'data'); uint x = uint(uint8(data[0])); uint y = uint(uint8(data[1])); @@ -46,35 +46,43 @@ contract HalmosCheatCodeTest is SymTest { assert(0 <= y && y <= type(uint8).max); } - function testSymbolicUint256() public { + function checkSymbolicUint256() public { uint x = svm.createUint256('x'); assert(0 <= x && x <= type(uint256).max); } - function testSymbolicBytes32() public { + function checkSymbolicBytes32() public { bytes32 x = svm.createBytes32('x'); assert(0 <= uint(x) && uint(x) <= type(uint256).max); uint y; assembly { y := x } assert(0 <= y && y <= type(uint256).max); } - function testSymbolicAddress() public { + function checkSymbolicAddress() public { address x = svm.createAddress('x'); uint y; assembly { y := x } assert(0 <= y && y <= type(uint160).max); } - function testSymbolicBool() public { + function checkSymbolicBool() public { bool x = svm.createBool('x'); uint y; assembly { y := x } assert(y == 0 || y == 1); } - function testSymbolLabel() public returns (uint256) { + function checkSymbolLabel() public returns (uint256) { uint x = svm.createUint256(''); uint y = svm.createUint256(' '); uint z = svm.createUint256(' a '); uint w = svm.createUint256(' a b '); return x + y + z + w; } + + function checkFailUnknownCheatcode() public { + Dummy(address(svm)).foo(); // expected to fail with unknown cheatcode + } +} + +interface Dummy { + function foo() external; } diff --git a/tests/test/Invalid.t.sol b/tests/test/Invalid.t.sol index 069377e6..2088bb67 100644 --- a/tests/test/Invalid.t.sol +++ b/tests/test/Invalid.t.sol @@ -3,13 +3,17 @@ pragma solidity ^0.5.2; contract OldCompilerTest { - function testAssert(uint x) public { + function checkAssert(uint x) public pure { if (x == 0) return; assert(false); // old compiler versions don't revert with panic; instead, they run invalid opcode, which halmos ignores, resulting in no error here. - //myAssert(false); // you can use your own assertion that panic-reverts if assertion fails, when using halmos for old version code. } - function myAssert(bool cond) internal { + function checkMyAssert(uint x) public pure { + if (x == 0) return; + myAssert(false); // you can use your own assertion that panic-reverts if assertion fails, when using halmos for old version code. + } + + function myAssert(bool cond) internal pure { if (!cond) { assembly { mstore(0x00, 0x4e487b71) diff --git a/tests/test/Library.t.sol b/tests/test/Library.t.sol index 662d7790..b22b6a8e 100644 --- a/tests/test/Library.t.sol +++ b/tests/test/Library.t.sol @@ -14,7 +14,7 @@ library Math { } contract LibraryTest { - function testAdd(uint x, uint y) public pure { + function checkAdd(uint x, uint y) public pure { unchecked { assert(Math._add(x,y) == x+y); /* TODO: support public library functions (library linking) diff --git a/tests/test/LibraryLinking.t.sol b/tests/test/LibraryLinking.t.sol new file mode 100644 index 00000000..3f10b83b --- /dev/null +++ b/tests/test/LibraryLinking.t.sol @@ -0,0 +1,19 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +library Lib { + function foo() public pure returns (uint) { return 1; } + function bar() internal pure returns (uint) { return 2; } +} + +contract LibTest { + function checkFoo() public pure { + assert(Lib.foo() == 1); // library linking placeholder error + } +} + +contract LibTest2 { + function checkBar() public pure { + assert(Lib.bar() == 2); // this is fine because internal library functions are inlined + } +} diff --git a/tests/test/List.t.sol b/tests/test/List.t.sol index 8a9130a3..f93b307f 100644 --- a/tests/test/List.t.sol +++ b/tests/test/List.t.sol @@ -1,11 +1,13 @@ // SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0; +// NOTE: required options: --symbolic-storage + import "forge-std/Test.sol"; import "../src/List.sol"; contract ListTest is Test, List { - function testAdd(uint x) public { + function checkAdd(uint x) public { uint oldSize = arr.length; vm.assume(oldSize < type(uint).max); add(x); @@ -15,7 +17,7 @@ contract ListTest is Test, List { assert(arr[newSize-1] == x); } - function testRemove() public { + function checkRemove() public { uint oldSize = arr.length; vm.assume(oldSize > 0); remove(); @@ -24,7 +26,7 @@ contract ListTest is Test, List { assert(oldSize == newSize + 1); } - function testSet(uint i, uint x) public { + function checkSet(uint i, uint x) public { vm.assume(i < arr.length); set(i, x); assert(arr[i] == x); @@ -39,7 +41,7 @@ contract ListTestTest is Test { list.add(1); } - function testAdd(uint x) public { + function checkAdd(uint x) public { uint oldSize = list.size(); vm.assume(oldSize < type(uint).max); list.add(x); @@ -49,7 +51,7 @@ contract ListTestTest is Test { assert(list.arr(newSize-1) == x); } - function testRemove() public { + function checkRemove() public { uint oldSize = list.size(); vm.assume(oldSize > 0); list.remove(); @@ -58,7 +60,7 @@ contract ListTestTest is Test { assert(oldSize == newSize + 1); } - function testSet(uint i, uint x) public { + function checkSet(uint i, uint x) public { vm.assume(i < list.size()); list.set(i, x); assert(list.arr(i) == x); diff --git a/tests/test/Math.t.sol b/tests/test/Math.t.sol new file mode 100644 index 00000000..67dda853 --- /dev/null +++ b/tests/test/Math.t.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +contract MathTest { + function checkAvg(uint a, uint b) public pure { + unchecked { + uint r1 = (a & b) + (a ^ b) / 2; + uint r2 = (a + b) / 2; + assert(r1 == r2); + } + } +} diff --git a/tests/test/Opcode.t.sol b/tests/test/Opcode.t.sol index 06ce427f..f445902d 100644 --- a/tests/test/Opcode.t.sol +++ b/tests/test/Opcode.t.sol @@ -13,23 +13,23 @@ library Opcode { contract OpcodeTest is Test { - function test_SIGNEXTEND(uint value) public { - _test_SIGNEXTEND(0, value); - _test_SIGNEXTEND(1, value); - _test_SIGNEXTEND(2, value); - _test_SIGNEXTEND(30, value); - _test_SIGNEXTEND(31, value); - _test_SIGNEXTEND(32, value); - _test_SIGNEXTEND(33, value); + function check_SIGNEXTEND(uint value) public { + _check_SIGNEXTEND(0, value); + _check_SIGNEXTEND(1, value); + _check_SIGNEXTEND(2, value); + _check_SIGNEXTEND(30, value); + _check_SIGNEXTEND(31, value); + _check_SIGNEXTEND(32, value); + _check_SIGNEXTEND(33, value); } /* TODO: support symbolic size - function test_SIGNEXTEND(uint size, uint value) public { - _test_SIGNEXTEND(size, value); + function check_SIGNEXTEND(uint size, uint value) public { + _check_SIGNEXTEND(size, value); } */ - function _test_SIGNEXTEND(uint size, uint value) public { + function _check_SIGNEXTEND(uint size, uint value) public { uint result1 = Opcode.SIGNEXTEND(size, value); uint result2; if (size > 31) { @@ -46,7 +46,7 @@ contract OpcodeTest is Test { assertEq(result1, result2); } - function testPush0() public { + function checkPush0() public { // target bytecode is 0x365f5f37365ff3 // 36 CALLDATASIZE // 5F PUSH0 diff --git a/tests/test/Prank.t.sol b/tests/test/Prank.t.sol index 7f0ac003..8fe8f1b9 100644 --- a/tests/test/Prank.t.sol +++ b/tests/test/Prank.t.sol @@ -31,7 +31,7 @@ contract PrankSetUpTest is Test { vm.prank(address(target)); // prank is reset after setUp() } - function testPrank(address user) public { + function checkPrank(address user) public { vm.prank(user); target.recordCaller(); assert(target.caller() == user); @@ -52,7 +52,7 @@ contract PrankTest is Test { vm.prank(user); } - function testPrank(address user) public { + function checkPrank(address user) public { vm.prank(user); target.recordCaller(); assert(target.caller() == user); @@ -61,7 +61,7 @@ contract PrankTest is Test { assert(target.caller() == address(this)); } - function testStartPrank(address user) public { + function checkStartPrank(address user) public { vm.startPrank(user); target.recordCaller(); @@ -79,25 +79,25 @@ contract PrankTest is Test { assert(target.caller() == address(this)); } - function testPrankInternal(address user) public { + function checkPrankInternal(address user) public { prank(user); // indirect prank target.recordCaller(); assert(target.caller() == user); } - function testPrankExternal(address user) public { + function checkPrankExternal(address user) public { ext.prank(user); // prank isn't propagated beyond the vm boundry target.recordCaller(); assert(target.caller() == address(this)); } - function testPrankExternalSelf(address user) public { + function checkPrankExternalSelf(address user) public { this.prank(user); // prank isn't propagated beyond the vm boundry target.recordCaller(); assert(target.caller() == address(this)); } - function testPrankNew(address user) public { + function checkPrankNew(address user) public { vm.prank(user); dummy = new Dummy(); // contract creation also consumes prank vm.prank(user); @@ -105,28 +105,28 @@ contract PrankTest is Test { assert(target.caller() == user); } - function testPrankReset1(address user) public { + function checkPrankReset1(address user) public { // vm.prank(address(target)); // overwriting active prank is not allowed vm.prank(user); target.recordCaller(); assert(target.caller() == user); } - function testPrankReset2(address user) public { + function checkPrankReset2(address user) public { // vm.prank(address(target)); // overwriting active prank is not allowed vm.startPrank(user); target.recordCaller(); assert(target.caller() == user); } - function testStopPrank1(address user) public { + function checkStopPrank1(address user) public { vm.prank(user); vm.stopPrank(); // stopPrank can be used to disable both startPrank() and prank() target.recordCaller(); assert(target.caller() == address(this)); } - function testStopPrank2() public { + function checkStopPrank2() public { vm.stopPrank(); // stopPrank is allowed even when no active prank exists! target.recordCaller(); assert(target.caller() == address(this)); diff --git a/tests/test/Revert.t.sol b/tests/test/Revert.t.sol new file mode 100644 index 00000000..c5705e6a --- /dev/null +++ b/tests/test/Revert.t.sol @@ -0,0 +1,40 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +// from https://github.com/a16z/halmos/issues/109 + +contract C { + uint256 public num; + + function set1(uint256 x) public { + num = x; + revert("blah"); + } + + function set2(uint256 x) public { + revert("blah"); + num = x; + } +} + +contract CTest { + C c; + + function setUp() public { + c = new C(); + } + + function checkRevert1(uint256 x) public { + require(x != 0); + (bool result, ) = address(c).call(abi.encodeWithSignature("set1(uint256)", x)); + assert(!result); + assert(c.num() != x); // fail // TODO: fix reverting semantics + } + + function checkRevert2(uint256 x) public { + require(x != 0); + (bool result, ) = address(c).call(abi.encodeWithSignature("set2(uint256)", x)); + assert(!result); + assert(c.num() != x); + } +} diff --git a/tests/test/Send.t.sol b/tests/test/Send.t.sol index 71f0e437..65e37bd2 100644 --- a/tests/test/Send.t.sol +++ b/tests/test/Send.t.sol @@ -3,7 +3,7 @@ pragma solidity >=0.8.0 <0.9.0; contract SendTest { - function testSend(address payable receiver, uint amount, address others) public { + function checkSend(address payable receiver, uint amount, address others) public { require(others != address(this) && others != receiver); require(address(this) != receiver); @@ -26,7 +26,7 @@ contract SendTest { } } - function testSendSelf(address payable receiver, uint amount, address others) public { + function checkSendSelf(address payable receiver, uint amount, address others) public { require(others != address(this) && others != receiver); require(address(this) == receiver); diff --git a/tests/test/Setup.t.sol b/tests/test/Setup.t.sol index bf814e9d..68e83b03 100644 --- a/tests/test/Setup.t.sol +++ b/tests/test/Setup.t.sol @@ -15,7 +15,7 @@ contract SetupTest is Test { } } - function testTrue() public { + function checkTrue() public { assertEq(users[0], address(bytes20(keccak256("test")))); assertEq(users[1], address(uint160(users[0]) + 1)); assertEq(users[2], address(0)); diff --git a/tests/test/SetupPlus.t.sol b/tests/test/SetupPlus.t.sol index 3ff140d5..b7976b2a 100644 --- a/tests/test/SetupPlus.t.sol +++ b/tests/test/SetupPlus.t.sol @@ -34,7 +34,7 @@ contract SetupPlusTest { a = new A(x, x); } - function testSetup() public { + function checkSetup() public view { assert(a.x() > 10); assert(a.y() > 100); } @@ -87,7 +87,7 @@ contract SetupPlusTestB { mk(); } - function testSetup() public { + function checkSetup() public view { assert(b.x1() == init[0]); assert(b.y1() == init[1]); assert(b.x2() == init[2]); diff --git a/tests/test/SetupSymbolic.t.sol b/tests/test/SetupSymbolic.t.sol new file mode 100644 index 00000000..4e038e08 --- /dev/null +++ b/tests/test/SetupSymbolic.t.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +contract SetupSymbolicTest { + function setUpSymbolic(uint x) public pure { + if (x > 0) return; // generate multiple setup output states + } + + function checkFoo() public pure { + assert(true); // ensure setUp succeeds + } +} diff --git a/tests/test/SignExtend.t.sol b/tests/test/SignExtend.t.sol index ec56c455..b22fbd3c 100644 --- a/tests/test/SignExtend.t.sol +++ b/tests/test/SignExtend.t.sol @@ -5,7 +5,7 @@ import "forge-std/Test.sol"; import "../src/SignExtend.sol"; contract SignExtendTest is SignExtend { - function testSignExtend(int16 _x) public pure { + function checkSignExtend(int16 _x) public pure { int16 x = changeMySign(_x); assert(x == -_x); } diff --git a/tests/test/Solver.t.sol b/tests/test/Solver.t.sol new file mode 100644 index 00000000..538b5520 --- /dev/null +++ b/tests/test/Solver.t.sol @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +// from https://github.com/a16z/halmos/issues/57 + +// NOTE: required options: --print-potential-counterexample + +contract SolverTest { + + function foo(uint x) public pure returns (uint) { + if(x < type(uint128).max) + return x * 42; + else return x; + } + + function checkFoo(uint a, uint b) public pure { + if(b > a) { + assert(foo(b) > foo(a)); + } + } + +} diff --git a/tests/test/Storage.t.sol b/tests/test/Storage.t.sol index 3b0372fe..c783f832 100644 --- a/tests/test/Storage.t.sol +++ b/tests/test/Storage.t.sol @@ -1,40 +1,42 @@ // SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0; +// NOTE: required options: --symbolic-storage + import "forge-std/Test.sol"; import "../src/Storage.sol"; contract StorageTest is Storage { - function testSetMap1(uint k, uint v) public { + function checkSetMap1(uint k, uint v) public { setMap1(k, v); assert(map1[k] == v); } - function testSetMap2(uint k1, uint k2, uint v) public { + function checkSetMap2(uint k1, uint k2, uint v) public { setMap2(k1, k2, v); assert(map2[k1][k2] == v); } - function testSetMap3(uint k1, uint k2, uint k3, uint v) public { + function checkSetMap3(uint k1, uint k2, uint k3, uint v) public { setMap3(k1, k2, k3, v); assert(map3[k1][k2][k3] == v); } - function testAddArr1(uint v) public { + function checkAddArr1(uint v) public { uint size = arr1.length; addArr1(v); assert(arr1.length == size + 1); assert(arr1[size] == v); } - function testAddArr2(uint i, uint v) public { + function checkAddArr2(uint i, uint v) public { uint size = arr2[i].length; addArr2(i, v); assert(arr2[i].length == size + 1); assert(arr2[i][size] == v); } - function testAddMap1Arr1(uint k, uint v) public { + function checkAddMap1Arr1(uint k, uint v) public { uint size = map1Arr1[k].length; addMap1Arr1(k, v); assert(map1Arr1[k].length == size + 1); diff --git a/tests/test/Store.t.sol b/tests/test/Store.t.sol index 7d896933..56967a36 100644 --- a/tests/test/Store.t.sol +++ b/tests/test/Store.t.sol @@ -17,30 +17,30 @@ contract StoreTest is Test { } // TODO: support symbolic base slot -// function testStore(bytes32 key, bytes32 value) public { +// function checkStore(bytes32 key, bytes32 value) public { // vm.store(address(c), key, value); // assert(vm.load(address(c), key) == value); // } // TODO: support uninitialized accounts -// function testStoreUninit(bytes32 value) public { +// function checkStoreUninit(bytes32 value) public { // vm.store(address(0), 0, value); // assert(vm.load(address(0), 0) == value); // } - function testStoreScalar(uint value) public { + function checkStoreScalar(uint value) public { vm.store(address(c), 0, bytes32(value)); assert(c.x() == value); assert(uint(vm.load(address(c), 0)) == value); } - function testStoreMapping(uint key, uint value) public { + function checkStoreMapping(uint key, uint value) public { vm.store(address(c), keccak256(abi.encode(key, 1)), bytes32(value)); assert(c.m(key) == value); assert(uint(vm.load(address(c), keccak256(abi.encode(key, 1)))) == value); } - function testStoreArray(uint key, uint value) public { + function checkStoreArray(uint key, uint value) public { vm.assume(key < 2**32); // to avoid overflow vm.store(address(c), bytes32(uint(2)), bytes32(uint(1) + key)); vm.store(address(c), bytes32(uint(keccak256(abi.encode(2))) + key), bytes32(value)); diff --git a/tests/test/Struct.t.sol b/tests/test/Struct.t.sol index 5f1c6fbf..d48f8be3 100644 --- a/tests/test/Struct.t.sol +++ b/tests/test/Struct.t.sol @@ -7,9 +7,8 @@ contract StructTest { uint y; } - /* TODO: support struct parameter - function testStruct(Point memory p) public { + // TODO: support struct parameter + function checkStruct(Point memory) public pure { assert(true); } - */ } diff --git a/tests/test/TestConstructor.t.sol b/tests/test/TestConstructor.t.sol new file mode 100644 index 00000000..493b1e2e --- /dev/null +++ b/tests/test/TestConstructor.t.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +contract TestConstructorTest { + + uint public value = 1; + + function checkValue() public view { + assert(value == 1); // fail // TODO: consider test contract constructor + } + +} diff --git a/tests/test/UnsupportedOpcode.t.sol b/tests/test/UnsupportedOpcode.t.sol new file mode 100644 index 00000000..75d0068f --- /dev/null +++ b/tests/test/UnsupportedOpcode.t.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +contract X { + function foo() public { + assembly { + selfdestruct(0) // unsupported opcode + } + } + + function checkFoo() public { + foo(); // unsupported error + } +} + +contract Y { + X x; + + function setUp() public { + x = new X(); + } + + function checkFoo() public { + x.foo(); // unsupported error + } +} + +contract Z { + Y y; + + function setUp() public { + y = new Y(); + y.setUp(); + } + + function checkFoo() public { + y.checkFoo(); // unsupported error + } +} diff --git a/tests/test/Warp.t.sol b/tests/test/Warp.t.sol index da208365..2f41919e 100644 --- a/tests/test/Warp.t.sol +++ b/tests/test/Warp.t.sol @@ -28,39 +28,39 @@ contract WarpTest is Test { vm.warp(time); } - function testWarp(uint time) public { + function checkWarp(uint time) public { vm.warp(time); assert(block.timestamp == time); } - function testWarpInternal(uint time) public { + function checkWarpInternal(uint time) public { warp(time); assert(block.timestamp == time); } - function testWarpExternal(uint time) public { + function checkWarpExternal(uint time) public { ext.warp(time); assert(block.timestamp == time); } - function testWarpExternalSelf(uint time) public { + function checkWarpExternalSelf(uint time) public { this.warp(time); assert(block.timestamp == time); } - function testWarpNew(uint time) public { + function checkWarpNew(uint time) public { c = new C(time); assert(block.timestamp == time); } - function testWarpReset(uint time1, uint time2) public { + function checkWarpReset(uint time1, uint time2) public { vm.warp(time1); assert(block.timestamp == time1); vm.warp(time2); assert(block.timestamp == time2); } - function testWarpSetUp() public { + function checkWarpSetUp() public view { assert(block.timestamp == 1000); } } diff --git a/tests/test_halmos.py b/tests/test_halmos.py new file mode 100644 index 00000000..3166de02 --- /dev/null +++ b/tests/test_halmos.py @@ -0,0 +1,69 @@ +import pytest +import json + +from typing import Dict + +from halmos.__main__ import main + + +@pytest.mark.parametrize( + "cmd, expected_path", + [ + ( + ["--root", "tests"], + "tests/expected/all.json", + ), + ( + [ + "--root", + "tests", + "--contract", + "CounterTest", + "--loop", + "4", + "--symbolic-storage", + ], + "tests/expected/counter-symbolic.json", + ), + ( + ["--root", "tests", "--contract", "ListTest", "--symbolic-storage"], + "tests/expected/list-symbolic.json", + ), + ( + ["--root", "tests", "--contract", "StorageTest", "--symbolic-storage"], + "tests/expected/storage-symbolic.json", + ), + ], +) +@pytest.mark.parametrize( + "parallel_options", + [ + [], + ["--test-parallel"], + ["--solver-parallel"], + ["--test-parallel", "--solver-parallel"], + ], +) +def test_main(cmd, expected_path, parallel_options): + test_results_map = {} + main(cmd + parallel_options, test_results_map) + with open(expected_path, encoding="utf8") as f: + expected = json.load(f) + assert_eq(expected, test_results_map) + + +def assert_eq(m1: Dict, m2: Dict) -> int: + assert m1.keys() == m2.keys() + for c in m1: + l1 = sorted(m1[c], key=lambda x: x["name"]) + l2 = sorted(m2[c], key=lambda x: x["name"]) + assert len(l1) == len(l2) + assert all(eq_test_result(r1, r2) for r1, r2 in zip(l1, l2)) + + +def eq_test_result(r1: Dict, r2: Dict) -> bool: + return ( + r1["name"] == r2["name"] + and r1["exitcode"] == r2["exitcode"] + and r1["num_models"] == r2["num_models"] + ) From ab799d256e86a26df57a31e2fe322f561422bb79 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 03:11:47 -0700 Subject: [PATCH 02/30] fix ci --- .github/workflows/test.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 57d2d18e..244abeab 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -36,7 +36,9 @@ jobs: run: | python -m pip install --upgrade pip pip install pytest - pip install -r requirements.txt + + - name: Install Halmos + run: pip install -e . - name: Run pytest run: pytest From 18b1ec687cc8b8a57d4c9776c7c07d4e9b56fa79 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 03:27:16 -0700 Subject: [PATCH 03/30] fix expected --- tests/expected/all.json | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/tests/expected/all.json b/tests/expected/all.json index c394837f..69ce7fbf 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1406,24 +1406,6 @@ "num_bounded_loops": 0 } ], - "test/SrcMap.t.sol:SrcMapTest": [ - { - "name": "checkIf(uint256)", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.008314832986798137, - 0.008048832998611033, - 0.00026599998818710446 - ], - "num_bounded_loops": 0 - } - ], "test/Storage.t.sol:StorageTest": [ { "name": "checkAddArr1(uint256)", From 475eaae84b025d8a1be511ce5f2e6b7dfd65afd0 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 20:35:47 -0700 Subject: [PATCH 04/30] address comments --- src/halmos/__main__.py | 77 +++++++++++++++++++++--------------------- tests/test_halmos.py | 7 ++-- 2 files changed, 43 insertions(+), 41 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index f452ab1b..f7fc9d00 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -102,7 +102,7 @@ def parse_args(args=None) -> argparse.Namespace: "--log", metavar="LOG_FILE_PATH", help="log every execution steps in JSON" ) group_debug.add_argument( - "--json", metavar="JSON_FILE_PATH", help="output test results in JSON" + "--json-output", metavar="JSON_FILE_PATH", help="output test results in JSON" ) group_debug.add_argument( "--print-steps", action="store_true", help="print every execution steps" @@ -810,7 +810,7 @@ class RunArgs: methodIdentifiers: Dict[str, str] -def run_parallel(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: +def run_parallel(run_args: RunArgs) -> List[TestResult]: hexcode, abi, methodIdentifiers = ( run_args.hexcode, run_args.abi, @@ -834,13 +834,10 @@ def run_parallel(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: test_results = list(process_pool.map(setup_and_run_single, single_run_args)) test_results = sum(test_results, []) # flatten lists - num_passed = sum(r.exitcode == 0 for r in test_results) - num_failed = len(test_results) - num_passed + return test_results - return num_passed, num_failed, test_results - -def run_sequential(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: +def run_sequential(run_args: RunArgs) -> List[TestResult]: setup_info = extract_setup(run_args.methodIdentifiers) if setup_info.sig and args.verbose >= 1: print(f"Running {setup_info.sig}") @@ -853,9 +850,8 @@ def run_sequential(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: ) if args.debug: traceback.print_exc() - return (0, 0, []) + return [] - num_passed, num_failed = 0, 0 test_results = [] for funsig in run_args.funsigs: fun_info = FunctionInfo( @@ -868,17 +864,12 @@ def run_sequential(run_args: RunArgs) -> Tuple[int, int, List[TestResult]]: print(color_warn(f"{type(err).__name__}: {err}")) if args.debug: traceback.print_exc() - num_failed += 1 test_results.append(TestResult(funsig, 2)) continue test_results.append(test_result) - if test_result.exitcode == 0: - num_passed += 1 - else: - num_failed += 1 - return (num_passed, num_failed, test_results) + return test_results @dataclass(frozen=True) @@ -1114,7 +1105,15 @@ def parse_build_out(args: argparse.Namespace) -> Dict: return result -def main(argv=None, test_results_map=None) -> int: +def main(argv=None) -> Tuple[int, Dict]: + """Run Halmos. + + Args: + argv: alternative list of commandline arguments. + + Returns: + (int, Dict): exitcode and test results. + """ main_start = timer() # @@ -1134,12 +1133,12 @@ def main(argv=None, test_results_map=None) -> int: if args.version: print(f"Halmos {metadata.version('halmos')}") - return 0 + return (0, None) # quick bytecode execution mode if args.bytecode is not None: run_bytecode(args.bytecode) - return 0 + return (0, None) # # compile @@ -1160,13 +1159,13 @@ def main(argv=None, test_results_map=None) -> int: if build_exitcode: print(color_warn(f"build failed: {build_cmd}")) - return 1 + return (1, None) try: build_out = parse_build_out(args) except Exception as err: print(color_warn(f"build output parsing failed: {err}")) - return 1 + return (1, None) main_mid = timer() @@ -1178,8 +1177,7 @@ def main(argv=None, test_results_map=None) -> int: total_failed = 0 total_found = 0 - if args.json and test_results_map is None: - test_results_map = {} + test_results_map = {} for compiler_version in sorted(build_out): build_out_map = build_out[compiler_version] @@ -1212,30 +1210,33 @@ def main(argv=None, test_results_map=None) -> int: run_args = RunArgs(funsigs, hexcode, abi, methodIdentifiers) enable_parallel = args.test_parallel and len(funsigs) > 1 - num_passed, num_failed, test_results = ( + test_results = ( run_parallel(run_args) if enable_parallel else run_sequential(run_args) ) + num_passed = sum(r.exitcode == 0 for r in test_results) + num_failed = len(test_results) - num_passed + print( f"Symbolic test result: {num_passed} passed; {num_failed} failed; time: {timer() - contract_start:0.2f}s" ) total_passed += num_passed total_failed += num_failed - if test_results_map is not None: - if contract_path in test_results_map: - raise ValueError("already exists", contract_path) - test_results_map[contract_path] = list( - map(asdict, test_results) - ) + if contract_path in test_results_map: + raise ValueError("already exists", contract_path) + test_results_map[contract_path] = test_results main_end = timer() - if args.json: - with open(args.json, "w") as json_file: - json.dump(test_results_map, json_file) + if args.json_output: + with open(args.json_output, "w") as json_file: + json.dump( + {c: [asdict(r) for r in test_results_map[c]] for c in test_results_map}, + json_file, + ) if args.statistics: print( @@ -1247,14 +1248,12 @@ def main(argv=None, test_results_map=None) -> int: if args.contract is not None: error_msg += f" in {args.contract}" print(color_warn(error_msg)) - return 1 + return (1, None) - # exitcode - if total_failed == 0: - return 0 - else: - return 1 + exitcode = 0 if total_failed == 0 else 1 + + return (exitcode, test_results_map) if __name__ == "__main__": - sys.exit(main()) + sys.exit(main()[0]) diff --git a/tests/test_halmos.py b/tests/test_halmos.py index 3166de02..ad573878 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -2,6 +2,7 @@ import json from typing import Dict +from dataclasses import asdict from halmos.__main__ import main @@ -45,8 +46,10 @@ ], ) def test_main(cmd, expected_path, parallel_options): - test_results_map = {} - main(cmd + parallel_options, test_results_map) + test_results_map = main(cmd + parallel_options)[1] + test_results_map = { + c: [asdict(r) for r in test_results_map[c]] for c in test_results_map + } with open(expected_path, encoding="utf8") as f: expected = json.load(f) assert_eq(expected, test_results_map) From fd678a12c6e9487ce16eb88d12c5896af276cd4e Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 21:53:18 -0700 Subject: [PATCH 05/30] remove time info from expected json --- src/halmos/__main__.py | 68 +- tests/expected/all.json | 2673 +++++++++----------------- tests/expected/counter-symbolic.json | 367 ++-- tests/expected/list-symbolic.json | 79 +- tests/expected/storage-symbolic.json | 151 +- tests/test_halmos.py | 10 +- 6 files changed, 1172 insertions(+), 2176 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index f7fc9d00..e40181bd 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -104,6 +104,9 @@ def parse_args(args=None) -> argparse.Namespace: group_debug.add_argument( "--json-output", metavar="JSON_FILE_PATH", help="output test results in JSON" ) + group_debug.add_argument( + "--extended-json-output", action="store_true", help="include more information in test results" + ) group_debug.add_argument( "--print-steps", action="store_true", help="print every execution steps" ) @@ -727,14 +730,20 @@ def run( with open(args.log, "w") as json_file: json.dump(steps, json_file) - return TestResult( - funsig, - 0 if passed else 1, # exitcode - sum(m.result == sat for m in models), - (len(exs), normal, len(stuck)), - (time_total, time_paths, time_models), - len(bounded_loops), - ) + # return test result + exitcode = 0 if passed else 1 + num_counterexamples = sum(m.result == sat for m in models) + if args.extended_json_output: + return TestResult( + funsig, + exitcode, + num_counterexamples, + (len(exs), normal, len(stuck)), + (time_total, time_paths, time_models), + len(bounded_loops), + ) + else: + return TestResult(funsig, exitcode, num_counterexamples) @dataclass(frozen=True) @@ -1105,15 +1114,14 @@ def parse_build_out(args: argparse.Namespace) -> Dict: return result -def main(argv=None) -> Tuple[int, Dict]: - """Run Halmos. +@dataclass(frozen=True) +class MainResult: + exitcode: int + # contract path -> list of test results + test_results: Dict[str, List[TestResult]] = None - Args: - argv: alternative list of commandline arguments. - Returns: - (int, Dict): exitcode and test results. - """ +def _main(argv=None) -> MainResult: main_start = timer() # @@ -1133,12 +1141,12 @@ def main(argv=None) -> Tuple[int, Dict]: if args.version: print(f"Halmos {metadata.version('halmos')}") - return (0, None) + return MainResult(0) # quick bytecode execution mode if args.bytecode is not None: run_bytecode(args.bytecode) - return (0, None) + return MainResult(0) # # compile @@ -1159,13 +1167,13 @@ def main(argv=None) -> Tuple[int, Dict]: if build_exitcode: print(color_warn(f"build failed: {build_cmd}")) - return (1, None) + return MainResult(1) try: build_out = parse_build_out(args) except Exception as err: print(color_warn(f"build output parsing failed: {err}")) - return (1, None) + return MainResult(1) main_mid = timer() @@ -1231,13 +1239,6 @@ def main(argv=None) -> Tuple[int, Dict]: main_end = timer() - if args.json_output: - with open(args.json_output, "w") as json_file: - json.dump( - {c: [asdict(r) for r in test_results_map[c]] for c in test_results_map}, - json_file, - ) - if args.statistics: print( f"\n[time] total: {main_end - main_start:0.2f}s (build: {main_mid - main_start:0.2f}s, tests: {main_end - main_mid:0.2f}s)" @@ -1248,12 +1249,21 @@ def main(argv=None) -> Tuple[int, Dict]: if args.contract is not None: error_msg += f" in {args.contract}" print(color_warn(error_msg)) - return (1, None) + return MainResult(1) exitcode = 0 if total_failed == 0 else 1 + result = MainResult(exitcode, test_results_map) + + if args.json_output: + with open(args.json_output, "w") as json_file: + json.dump(asdict(result), json_file, indent=4) + + return result + - return (exitcode, test_results_map) +def main() -> int: + return _main().exitcode if __name__ == "__main__": - sys.exit(main()[0]) + sys.exit(main()) diff --git a/tests/expected/all.json b/tests/expected/all.json index 69ce7fbf..edd1483a 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1,1753 +1,924 @@ { - "test/Invalid.t.sol:OldCompilerTest": [ - { - "name": "checkAssert(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.006792041007429361, - 0.006783832999644801, - 8.208007784560323e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkMyAssert(uint256)", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.007092082989402115, - 0.006427499989513308, - 0.0006645829998888075 - ], - "num_bounded_loops": 0 - } - ], - "test/Arith.t.sol:ArithTest": [ - { - "name": "checkExp(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.007170666998717934, - 0.0071627919969614595, - 7.875001756474376e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkMod(uint256,uint256,address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.01046979200327769, - 0.010462334001203999, - 7.458002073690295e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/AssertTest.sol:CTest": [ - { - "name": "checkBar()", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 2, - 0, - 0 - ], - "time": [ - 0.10647333299857564, - 0.10532550001516938, - 0.0011478329834062606 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkFoo()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02516283400473185, - 0.025157959025818855, - 4.8749789129942656e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Block.t.sol:BlockCheatCodeTest": [ - { - "name": "checkChainId(uint64)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.012892416008980945, - 0.012884875002782792, - 7.5410061981529e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkCoinbase(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.012101457978133112, - 0.012094707984942943, - 6.749993190169334e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkDifficulty(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.009351707994937897, - 0.009346916020149365, - 4.791974788531661e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkFee(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.008611708995886147, - 0.008606417017290369, - 5.291978595778346e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkRoll(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.008901083987439051, - 0.008895249979104847, - 5.8340083342045546e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarp(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.00978820800082758, - 0.0097822499810718, - 5.958019755780697e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Byte.t.sol:ByteTest": [ - { - "name": "checkByte(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 6, - 2, - 0 - ], - "time": [ - 0.10002066701417789, - 0.05631445799372159, - 0.0437062090204563 - ], - "num_bounded_loops": 0 - } - ], - "test/Byte.t.sol:SymbolicByteTest": [ - { - "name": "checkSymbolicByteIndex(uint8,uint8)", - "exitcode": 1, - "num_models": 2, - "num_paths": [ - 6, - 1, - 0 - ], - "time": [ - 0.028774250007700175, - 0.02722508300212212, - 0.001549167005578056 - ], - "num_bounded_loops": 0 - } - ], - "test/Console.t.sol:ConsoleTest": [ - { - "name": "checkLog()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.010688374983146787, - 0.01068245799979195, - 5.916983354836702e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Const.t.sol:ConstTest": [ - { - "name": "checkConst()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.003543416998581961, - 0.0035386669915169477, - 4.750007065013051e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Const.t.sol:ConstTestTest": [ - { - "name": "checkConst()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.00376158399740234, - 0.003757500002393499, - 4.083995008841157e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Counter.t.sol:CounterTest": [ - { - "name": "checkDiv1(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 2, - 0 - ], - "time": [ - 0.008028250013012439, - 0.008022708003409207, - 5.542009603232145e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkDiv2(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 2, - 0 - ], - "time": [ - 0.008344333997229114, - 0.008339084015460685, - 5.249981768429279e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkFoo(uint256,uint256,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 17, - 16, - 0 - ], - "time": [ - 0.0931020829884801, - 0.09307670799898915, - 2.5374989490956068e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkInc()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.007204166991868988, - 0.007199874991783872, - 4.292000085115433e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkIncBy(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.006024375004926696, - 0.006020500004524365, - 3.875000402331352e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkIncOpt()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.00583899999037385, - 0.005834999989019707, - 4.0000013541430235e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkLoopConst()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.009400084003573284, - 0.009396250010468066, - 3.8339931052178144e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkLoopConstIf()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02649008299340494, - 0.026484457979677245, - 5.62501372769475e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkLoopDoWhile(uint8)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 6, - 4, - 0 - ], - "time": [ - 0.023103666986571625, - 0.023094042000593618, - 9.624985978007317e-06 - ], - "num_bounded_loops": 1 - }, - { - "name": "checkLoopFor(uint8)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 3, - 0 - ], - "time": [ - 0.018659833003766835, - 0.01864958298392594, - 1.025001984089613e-05 - ], - "num_bounded_loops": 1 - }, - { - "name": "checkLoopWhile(uint8)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 3, - 0 - ], - "time": [ - 0.018609833990922198, - 0.018600874987896532, - 8.95900302566588e-06 - ], - "num_bounded_loops": 1 - }, - { - "name": "checkMulDiv(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 4, - 0 - ], - "time": [ - 0.07291600000462495, - 0.0729067079955712, - 9.292009053751826e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSet(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.005909416999202222, - 0.005904332996578887, - 5.084002623334527e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetString(uint256,string,uint256,string,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02962820799439214, - 0.029622333007864654, - 5.874986527487636e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetSum(uint248,uint248)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 1, - 0 - ], - "time": [ - 0.024045666999882087, - 0.024035166978137568, - 1.0500021744519472e-05 - ], - "num_bounded_loops": 0 - } - ], - "test/Create.t.sol:CreateTest": [ - { - "name": "checkConst()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.016407249990152195, - 0.016401541011873633, - 5.7089782785624266e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkImmutable()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.015087000007042661, - 0.015082625002833083, - 4.375004209578037e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkInitialized()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.014679749991046265, - 0.014675749989692122, - 4.0000013541430235e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSet(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.030553457996575162, - 0.03054887501639314, - 4.582980182021856e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Deal.t.sol:DealTest": [ - { - "name": "checkDeal1(address,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.013186916999984533, - 0.013181042013457045, - 5.874986527487636e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkDeal2(address,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.016927541990298778, - 0.0169214999768883, - 6.04201341047883e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkDealNew()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.016635584004689008, - 0.016630625003017485, - 4.959001671522856e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Foundry.t.sol:FoundryTest": [ - { - "name": "checkAssume(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.009323125006631017, - 0.009317625022958964, - 5.499983672052622e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkEtchConcrete()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.016670041979523376, - 0.01666495797690004, - 5.084002623334527e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkEtchOverwrite()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02786154198111035, - 0.027856041997438297, - 5.499983672052622e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkGetCode(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.46927079098531976, - 0.4692655830003787, - 5.207984941080213e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Getter.t.sol:GetterTest": [ - { - "name": "checkGetter(uint256)", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 3, - 0, - 1 - ], - "time": [ - 0.006775084009859711, - 0.006768666993593797, - 6.417016265913844e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/HalmosCheatCode.t.sol:HalmosCheatCodeTest": [ - { - "name": "checkFailUnknownCheatcode()", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 2, - 0, - 1 - ], - "time": [ - 0.0063777079922147095, - 0.006372917006956413, - 4.790985258296132e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolLabel()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 1, - 0 - ], - "time": [ - 0.051910667010815814, - 0.05190024999319576, - 1.0417017620056868e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolicAddress()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.011195333005161956, - 0.011190958000952378, - 4.375004209578037e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolicBool()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 2, - 0 - ], - "time": [ - 0.012926708004670218, - 0.012920708017190918, - 5.999987479299307e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolicBytes()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02052141699823551, - 0.02051549998577684, - 5.917012458667159e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolicBytes32()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.00990520798950456, - 0.009900542005198076, - 4.665984306484461e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolicUint()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.024763166991760954, - 0.02475808298913762, - 5.084002623334527e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSymbolicUint256()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.010339250002289191, - 0.010333915997762233, - 5.3340045269578695e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Library.t.sol:LibraryTest": [ - { - "name": "checkAdd(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.004304542002500966, - 0.004299583000829443, - 4.959001671522856e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/LibraryLinking.t.sol:LibTest": [], - "test/LibraryLinking.t.sol:LibTest2": [ - { - "name": "checkBar()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.0032639590208418667, - 0.0032595000229775906, - 4.458997864276171e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/List.t.sol:ListTest": [ - { - "name": "checkAdd(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.01591579199885018, - 0.015911082999082282, - 4.708999767899513e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkRemove()", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 1, - 0, - 0 - ], - "time": [ - 0.007327958010137081, - 0.007324333011638373, - 3.6249984987080097e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSet(uint256,uint256)", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 1, - 0, - 0 - ], - "time": [ - 0.00863666701479815, - 0.00863216700963676, - 4.5000051613897085e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/List.t.sol:ListTestTest": [ - { - "name": "checkAdd(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.08320020799874328, - 0.08319529198342934, - 4.91601531393826e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkRemove()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.054968792013823986, - 0.054963958013104275, - 4.8340007197111845e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSet(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.06289233299321495, - 0.06288745798519813, - 4.875008016824722e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Math.t.sol:MathTest": [ - { - "name": "checkAvg(uint256,uint256)", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.07157470801030286, - 0.01126283299527131, - 0.060311875015031546 - ], - "num_bounded_loops": 0 - } - ], - "test/Opcode.t.sol:OpcodeTest": [ - { - "name": "checkPush0()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02399954100837931, - 0.02399524999782443, - 4.291010554879904e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "check_SIGNEXTEND(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 33, - 32, - 0 - ], - "time": [ - 0.28771620901534334, - 0.28766833400004543, - 4.787501529790461e-05 - ], - "num_bounded_loops": 0 - } - ], - "test/Prank.t.sol:PrankSetUpTest": [ - { - "name": "checkPrank(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.040319375024409965, - 0.04031275000306778, - 6.62502134218812e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Prank.t.sol:PrankTest": [ - { - "name": "checkPrank(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.061628583003766835, - 0.061621666012797505, - 6.916990969330072e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkPrankExternal(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.05262120798579417, - 0.05261449998943135, - 6.707996362820268e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkPrankExternalSelf(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.05366733399569057, - 0.0536605000088457, - 6.833986844867468e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkPrankInternal(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.03688741699443199, - 0.03687945901765488, - 7.957976777106524e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkPrankNew(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.04577312499168329, - 0.04576516701490618, - 7.957976777106524e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkPrankReset1(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.03653045801911503, - 0.03652370799682103, - 6.750022293999791e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkPrankReset2(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.03804066698648967, - 0.03803404199425131, - 6.624992238357663e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkStartPrank(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.1221603750018403, - 0.12215379098779522, - 6.584014045074582e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkStopPrank1(address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.04132283298531547, - 0.041314665984828025, - 8.167000487446785e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkStopPrank2()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.031720458006020635, - 0.03171566600212827, - 4.792003892362118e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Revert.t.sol:CTest": [ - { - "name": "checkRevert1(uint256)", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 3, - 0, - 0 - ], - "time": [ - 0.04121337499236688, - 0.0408095839957241, - 0.0004037909966427833 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkRevert2(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.03911733301356435, - 0.039110417012125254, - 6.9160014390945435e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Send.t.sol:SendTest": [ - { - "name": "checkSend(address,uint256,address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 8, - 1, - 0 - ], - "time": [ - 0.03954100000555627, - 0.03952391701750457, - 1.7082988051697612e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSendSelf(address,uint256,address)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 8, - 1, - 0 - ], - "time": [ - 0.03625720800482668, - 0.036242500005755574, - 1.4707999071106315e-05 - ], - "num_bounded_loops": 0 - } - ], - "test/Setup.t.sol:SetupTest": [ - { - "name": "checkTrue()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.04295708300196566, - 0.04295220799394883, - 4.875008016824722e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/SetupPlus.t.sol:SetupPlusTest": [ - { - "name": "checkSetup()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.034146124991821125, - 0.03414112501195632, - 4.999979864805937e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/SetupPlus.t.sol:SetupPlusTestB": [ - { - "name": "checkSetup()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.049622124992311, - 0.049617707991274074, - 4.417001036927104e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/SetupSymbolic.t.sol:SetupSymbolicTest": [ - { - "name": "checkFoo()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.003194707998773083, - 0.0031905829964671284, - 4.125002305954695e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/SignExtend.t.sol:SignExtendTest": [ - { - "name": "checkSignExtend(int16)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.061022916983347386, - 0.06101416700403206, - 8.749979315325618e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Solver.t.sol:SolverTest": [ - { - "name": "checkFoo(uint256,uint256)", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 9, - 4, - 0 - ], - "time": [ - 1.0501290000102017, - 0.04364512499887496, - 1.0064838750113267 - ], - "num_bounded_loops": 0 - } - ], - "test/Storage.t.sol:StorageTest": [ - { - "name": "checkAddArr1(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.010458083997946233, - 0.010453750001033768, - 4.3339969124644995e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkAddArr2(uint256,uint256)", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 2, - 0, - 0 - ], - "time": [ - 0.006222666008397937, - 0.0062180410022847354, - 4.62500611320138e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkAddMap1Arr1(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.017453957989346236, - 0.01744825000059791, - 5.707988748326898e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetMap1(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.006097791017964482, - 0.006093916017562151, - 3.875000402331352e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetMap2(uint256,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.008013749989913777, - 0.008009665994904935, - 4.083995008841157e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetMap3(uint256,uint256,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.009471625002333894, - 0.00946745800320059, - 4.1669991333037615e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Store.t.sol:StoreTest": [ - { - "name": "checkStoreArray(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.0750039579870645, - 0.07499720799387433, - 6.749993190169334e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkStoreMapping(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.045630125008756295, - 0.04562462499598041, - 5.5000127758830786e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkStoreScalar(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.02935466601047665, - 0.029350249998969957, - 4.416011506691575e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Struct.t.sol:StructTest": [ - { - "name": "checkStruct((uint256,uint256))", - "exitcode": 2, - "num_models": null, - "num_paths": null, - "time": null, - "num_bounded_loops": null - } - ], - "test/TestConstructor.t.sol:TestConstructorTest": [ - { - "name": "checkValue()", - "exitcode": 1, - "num_models": 1, - "num_paths": [ - 2, - 0, - 0 - ], - "time": [ - 0.005449541989946738, - 0.005120167013956234, - 0.000329374975990504 - ], - "num_bounded_loops": 0 - } - ], - "test/UnsupportedOpcode.t.sol:X": [ - { - "name": "checkFoo()", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 2, - 0, - 1 - ], - "time": [ - 0.00361879201955162, - 0.0036138340074103326, - 4.958012141287327e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/UnsupportedOpcode.t.sol:Y": [ - { - "name": "checkFoo()", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 2, - 0, - 1 - ], - "time": [ - 0.010356249986216426, - 0.010351292003178969, - 4.95798303745687e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/UnsupportedOpcode.t.sol:Z": [ - { - "name": "checkFoo()", - "exitcode": 1, - "num_models": 0, - "num_paths": [ - 2, - 0, - 1 - ], - "time": [ - 0.021697415999369696, - 0.02169258298818022, - 4.8330111894756556e-06 - ], - "num_bounded_loops": 0 - } - ], - "test/Warp.t.sol:WarpTest": [ - { - "name": "checkWarp(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.011706249992130324, - 0.011701832991093397, - 4.417001036927104e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarpExternal(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.028597750002518296, - 0.028592999995453283, - 4.750007065013051e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarpExternalSelf(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.03017012498457916, - 0.030165417003445327, - 4.7079811338335276e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarpInternal(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.013198832981288433, - 0.013193124992540106, - 5.707988748326898e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarpNew(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.03445437498157844, - 0.03444954098085873, - 4.8340007197111845e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarpReset(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.017815165978390723, - 0.017809415992815048, - 5.749985575675964e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkWarpSetUp()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.007120875001419336, - 0.007116541994037107, - 4.3330073822289705e-06 - ], - "num_bounded_loops": 0 - } - ] + "exitcode": 1, + "test_results": { + "test/Invalid.t.sol:OldCompilerTest": [ + { + "name": "checkAssert(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkMyAssert(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Arith.t.sol:ArithTest": [ + { + "name": "checkExp(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkMod(uint256,uint256,address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/AssertTest.sol:CTest": [ + { + "name": "checkBar()", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkFoo()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Block.t.sol:BlockCheatCodeTest": [ + { + "name": "checkChainId(uint64)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkCoinbase(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkDifficulty(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkFee(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkRoll(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarp(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Byte.t.sol:ByteTest": [ + { + "name": "checkByte(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Byte.t.sol:SymbolicByteTest": [ + { + "name": "checkSymbolicByteIndex(uint8,uint8)", + "exitcode": 1, + "num_models": 2, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Console.t.sol:ConsoleTest": [ + { + "name": "checkLog()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Const.t.sol:ConstTest": [ + { + "name": "checkConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Const.t.sol:ConstTestTest": [ + { + "name": "checkConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Counter.t.sol:CounterTest": [ + { + "name": "checkDiv1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkDiv2(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkFoo(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkInc()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkIncBy(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkIncOpt()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopConstIf()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopDoWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopFor(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkMulDiv(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSet(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetString(uint256,string,uint256,string,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetSum(uint248,uint248)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Create.t.sol:CreateTest": [ + { + "name": "checkConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkImmutable()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkInitialized()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSet(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Deal.t.sol:DealTest": [ + { + "name": "checkDeal1(address,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkDeal2(address,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkDealNew()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Foundry.t.sol:FoundryTest": [ + { + "name": "checkAssume(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkEtchConcrete()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkEtchOverwrite()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkGetCode(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Getter.t.sol:GetterTest": [ + { + "name": "checkGetter(uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/HalmosCheatCode.t.sol:HalmosCheatCodeTest": [ + { + "name": "checkFailUnknownCheatcode()", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolLabel()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolicAddress()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolicBool()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolicBytes()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolicBytes32()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolicUint()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSymbolicUint256()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Library.t.sol:LibraryTest": [ + { + "name": "checkAdd(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/LibraryLinking.t.sol:LibTest": [], + "test/LibraryLinking.t.sol:LibTest2": [ + { + "name": "checkBar()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/List.t.sol:ListTest": [ + { + "name": "checkAdd(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkRemove()", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSet(uint256,uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/List.t.sol:ListTestTest": [ + { + "name": "checkAdd(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkRemove()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSet(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Math.t.sol:MathTest": [ + { + "name": "checkAvg(uint256,uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Opcode.t.sol:OpcodeTest": [ + { + "name": "checkPush0()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_SIGNEXTEND(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Prank.t.sol:PrankSetUpTest": [ + { + "name": "checkPrank(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Prank.t.sol:PrankTest": [ + { + "name": "checkPrank(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkPrankExternal(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkPrankExternalSelf(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkPrankInternal(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkPrankNew(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkPrankReset1(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkPrankReset2(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkStartPrank(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkStopPrank1(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkStopPrank2()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Revert.t.sol:CTest": [ + { + "name": "checkRevert1(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkRevert2(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Send.t.sol:SendTest": [ + { + "name": "checkSend(address,uint256,address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSendSelf(address,uint256,address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Setup.t.sol:SetupTest": [ + { + "name": "checkTrue()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/SetupPlus.t.sol:SetupPlusTest": [ + { + "name": "checkSetup()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/SetupPlus.t.sol:SetupPlusTestB": [ + { + "name": "checkSetup()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/SetupSymbolic.t.sol:SetupSymbolicTest": [ + { + "name": "checkFoo()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/SignExtend.t.sol:SignExtendTest": [ + { + "name": "checkSignExtend(int16)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Solver.t.sol:SolverTest": [ + { + "name": "checkFoo(uint256,uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Storage.t.sol:StorageTest": [ + { + "name": "checkAddArr1(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkAddArr2(uint256,uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkAddMap1Arr1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetMap1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetMap2(uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetMap3(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Store.t.sol:StoreTest": [ + { + "name": "checkStoreArray(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkStoreMapping(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkStoreScalar(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Struct.t.sol:StructTest": [ + { + "name": "checkStruct((uint256,uint256))", + "exitcode": 2, + "num_models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/TestConstructor.t.sol:TestConstructorTest": [ + { + "name": "checkValue()", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/UnsupportedOpcode.t.sol:X": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/UnsupportedOpcode.t.sol:Y": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/UnsupportedOpcode.t.sol:Z": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Warp.t.sol:WarpTest": [ + { + "name": "checkWarp(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarpExternal(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarpExternalSelf(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarpInternal(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarpNew(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarpReset(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkWarpSetUp()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ] + } } diff --git a/tests/expected/counter-symbolic.json b/tests/expected/counter-symbolic.json index 824c812b..766804a6 100644 --- a/tests/expected/counter-symbolic.json +++ b/tests/expected/counter-symbolic.json @@ -1,244 +1,127 @@ { - "test/Counter.t.sol:CounterTest": [ - { - "name": "checkDiv1(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 2, - 0 - ], - "time": [ - 0.009959374991012737, - 0.009951167012332007, - 8.207978680729866e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkDiv2(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 2, - 0 - ], - "time": [ - 0.00888091602246277, - 0.008866500022122636, - 1.4416000340133905e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkFoo(uint256,uint256,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 47, - 16, - 0 - ], - "time": [ - 0.21995554098975845, - 0.21987691600224935, - 7.862498750910163e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkInc()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.027028792013879865, - 0.01539937499910593, - 0.011629417014773935 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkIncBy(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 2, - 0 - ], - "time": [ - 0.016327749995980412, - 0.01632145798066631, - 6.292015314102173e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkIncOpt()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.025245500000892207, - 0.013565540983108804, - 0.011679959017783403 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkLoopConst()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 1, - 0 - ], - "time": [ - 0.030433334002736956, - 0.02264291699975729, - 0.007790417002979666 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkLoopConstIf()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 77, - 16, - 0 - ], - "time": [ - 1.538891167001566, - 0.6547999999893364, - 0.8840911670122296 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkLoopDoWhile(uint8)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 20, - 5, - 0 - ], - "time": [ - 0.14874658299959265, - 0.09308420799789019, - 0.05566237500170246 - ], - "num_bounded_loops": 1 - }, - { - "name": "checkLoopFor(uint8)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 19, - 5, - 0 - ], - "time": [ - 0.1373970830172766, - 0.08692545801750384, - 0.05047162499977276 - ], - "num_bounded_loops": 1 - }, - { - "name": "checkLoopWhile(uint8)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 19, - 5, - 0 - ], - "time": [ - 0.1446185829991009, - 0.08712587499758229, - 0.05749270800151862 - ], - "num_bounded_loops": 1 - }, - { - "name": "checkMulDiv(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 4, - 0 - ], - "time": [ - 0.07496475000516511, - 0.07495608300087042, - 8.66700429469347e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSet(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.00604049998219125, - 0.006035083992173895, - 5.415990017354488e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetString(uint256,string,uint256,string,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.03229575001751073, - 0.03228700000909157, - 8.750008419156075e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetSum(uint248,uint248)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 1, - 0 - ], - "time": [ - 0.023321624990785494, - 0.02331225000671111, - 9.374984074383974e-06 - ], - "num_bounded_loops": 0 - } - ] + "exitcode": 0, + "test_results": { + "test/Counter.t.sol:CounterTest": [ + { + "name": "checkDiv1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkDiv2(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkFoo(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkInc()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkIncBy(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkIncOpt()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopConst()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopConstIf()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopDoWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopFor(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoopWhile(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkMulDiv(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSet(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetString(uint256,string,uint256,string,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetSum(uint248,uint248)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ] + } } diff --git a/tests/expected/list-symbolic.json b/tests/expected/list-symbolic.json index 38c86e38..31d64c93 100644 --- a/tests/expected/list-symbolic.json +++ b/tests/expected/list-symbolic.json @@ -1,52 +1,31 @@ { - "test/List.t.sol:ListTest": [ - { - "name": "checkAdd(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.054170040995813906, - 0.0343787909951061, - 0.019791250000707805 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkRemove()", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 3, - 1, - 0 - ], - "time": [ - 0.06059570799698122, - 0.019172542000887915, - 0.0414231659960933 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSet(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.014601791015593335, - 0.01459545799298212, - 6.333022611215711e-06 - ], - "num_bounded_loops": 0 - } - ] + "exitcode": 0, + "test_results": { + "test/List.t.sol:ListTest": [ + { + "name": "checkAdd(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkRemove()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSet(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ] + } } diff --git a/tests/expected/storage-symbolic.json b/tests/expected/storage-symbolic.json index 21104590..4bda94f9 100644 --- a/tests/expected/storage-symbolic.json +++ b/tests/expected/storage-symbolic.json @@ -1,100 +1,55 @@ { - "test/Storage.t.sol:StorageTest": [ - { - "name": "checkAddArr1(uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.022341417003190145, - 0.022330749983666465, - 1.066701952368021e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkAddArr2(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 5, - 1, - 0 - ], - "time": [ - 0.07018687500385568, - 0.07016733300406486, - 1.95419997908175e-05 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkAddMap1Arr1(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 4, - 1, - 0 - ], - "time": [ - 0.028902583988383412, - 0.02889408401097171, - 8.499977411702275e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetMap1(uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.006448500003898516, - 0.006442875019274652, - 5.624984623864293e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetMap2(uint256,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.008583459013607353, - 0.008578334003686905, - 5.125009920448065e-06 - ], - "num_bounded_loops": 0 - }, - { - "name": "checkSetMap3(uint256,uint256,uint256,uint256)", - "exitcode": 0, - "num_models": 0, - "num_paths": [ - 2, - 1, - 0 - ], - "time": [ - 0.0095768750179559, - 0.009572500013746321, - 4.375004209578037e-06 - ], - "num_bounded_loops": 0 - } - ] + "exitcode": 0, + "test_results": { + "test/Storage.t.sol:StorageTest": [ + { + "name": "checkAddArr1(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkAddArr2(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkAddMap1Arr1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetMap1(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetMap2(uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkSetMap3(uint256,uint256,uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ] + } } diff --git a/tests/test_halmos.py b/tests/test_halmos.py index ad573878..cc8afd72 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -4,7 +4,7 @@ from typing import Dict from dataclasses import asdict -from halmos.__main__ import main +from halmos.__main__ import _main @pytest.mark.parametrize( @@ -46,13 +46,11 @@ ], ) def test_main(cmd, expected_path, parallel_options): - test_results_map = main(cmd + parallel_options)[1] - test_results_map = { - c: [asdict(r) for r in test_results_map[c]] for c in test_results_map - } + actual = asdict(_main(cmd + parallel_options)) with open(expected_path, encoding="utf8") as f: expected = json.load(f) - assert_eq(expected, test_results_map) + assert expected["exitcode"] == actual["exitcode"] + assert_eq(expected["test_results"], actual["test_results"]) def assert_eq(m1: Dict, m2: Dict) -> int: From 14e1619692106c90bbb0a1ee7d56b7237f38b988 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:05:01 -0700 Subject: [PATCH 06/30] add comments --- src/halmos/__main__.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index e40181bd..6ea8b22f 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1261,9 +1261,11 @@ def _main(argv=None) -> MainResult: return result +# entrypoint for the `halmos` script def main() -> int: return _main().exitcode +# entrypoint for `python -m halmos` if __name__ == "__main__": sys.exit(main()) From 0b878184ecfe60dab856bf8588f7c291c00863b8 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:08:20 -0700 Subject: [PATCH 07/30] fix lint error --- src/halmos/__main__.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 6ea8b22f..7cbdc0b9 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -105,7 +105,9 @@ def parse_args(args=None) -> argparse.Namespace: "--json-output", metavar="JSON_FILE_PATH", help="output test results in JSON" ) group_debug.add_argument( - "--extended-json-output", action="store_true", help="include more information in test results" + "--extended-json-output", + action="store_true", + help="include more information in test results", ) group_debug.add_argument( "--print-steps", action="store_true", help="print every execution steps" From 0f367298a06089a6b5b87d816218bb61139ff8c0 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:24:24 -0700 Subject: [PATCH 08/30] add examples in the pytest --- tests/expected/examples.json | 55 ++++++++++++++++++++++++++++++++++++ tests/test_halmos.py | 4 +++ 2 files changed, 59 insertions(+) create mode 100644 tests/expected/examples.json diff --git a/tests/expected/examples.json b/tests/expected/examples.json new file mode 100644 index 00000000..b0a94b46 --- /dev/null +++ b/tests/expected/examples.json @@ -0,0 +1,55 @@ +{ + "exitcode": 1, + "test_results": { + "test/Example.t.sol:ExampleTest": [ + { + "name": "testIsPowerOfTwo(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "testIsPowerOfTwo(uint8)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "testIsPowerOfTwoEq(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "testTotalPriceBuggy(uint96,uint32)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "testTotalPriceFixed(uint96,uint32)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "testTotalPriceFixedEqualsToConservative(uint96,uint32)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ] + } +} \ No newline at end of file diff --git a/tests/test_halmos.py b/tests/test_halmos.py index cc8afd72..172c45e6 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -34,6 +34,10 @@ ["--root", "tests", "--contract", "StorageTest", "--symbolic-storage"], "tests/expected/storage-symbolic.json", ), + ( + ["--root", "examples", "--loop", "256", "--solver-fresh", "--function", "test"], + "tests/expected/examples.json", + ), ], ) @pytest.mark.parametrize( From c65f3f2b2f23fb5805285a04d7fff49d1de535f0 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:34:08 -0700 Subject: [PATCH 09/30] add proxy test --- tests/test/Proxy.t.sol | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/test/Proxy.t.sol diff --git a/tests/test/Proxy.t.sol b/tests/test/Proxy.t.sol new file mode 100644 index 00000000..be9126d7 --- /dev/null +++ b/tests/test/Proxy.t.sol @@ -0,0 +1,28 @@ +pragma solidity ^0.8.19; + +import "forge-std/Test.sol"; + +import {ERC1967Proxy} from "openzeppelin-contracts/contracts/proxy/ERC1967/ERC1967Proxy.sol"; + +contract C { + uint public num; + function foo(uint x) public { + num = x; + } +} + +contract ProxyTest is Test { + C cImpl; + C c; + + function setUp() public { + cImpl = new C(); + c = C(address(new ERC1967Proxy(address(cImpl), ""))); + } + + function checkFoo(uint x) public { + c.foo(x); + assert(c.num() == x); // currently unsupported // TODO: support DELEGATECALL + assert(cImpl.num() == 0); + } +} From c302e75436f3a48114a2a7e62da4d27bcc57e22e Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:41:05 -0700 Subject: [PATCH 10/30] add submodule openzeppelin-contracts --- .gitmodules | 3 +++ tests/lib/openzeppelin-contracts | 1 + 2 files changed, 4 insertions(+) create mode 160000 tests/lib/openzeppelin-contracts diff --git a/.gitmodules b/.gitmodules index 589dc660..0472303c 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "tests/lib/forge-std"] path = tests/lib/forge-std url = https://github.com/foundry-rs/forge-std +[submodule "tests/lib/openzeppelin-contracts"] + path = tests/lib/openzeppelin-contracts + url = https://github.com/OpenZeppelin/openzeppelin-contracts.git diff --git a/tests/lib/openzeppelin-contracts b/tests/lib/openzeppelin-contracts new file mode 160000 index 00000000..21bb89ef --- /dev/null +++ b/tests/lib/openzeppelin-contracts @@ -0,0 +1 @@ +Subproject commit 21bb89ef5bfc789b9333eb05e3ba2b7b284ac77c From 58c4643511ab62e235d532e9fd2d2cb088a3ed7b Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:41:18 -0700 Subject: [PATCH 11/30] update expected --- tests/expected/all.json | 12 +++++++++++- tests/expected/counter-symbolic.json | 2 +- tests/expected/list-symbolic.json | 2 +- tests/expected/storage-symbolic.json | 2 +- 4 files changed, 14 insertions(+), 4 deletions(-) diff --git a/tests/expected/all.json b/tests/expected/all.json index edd1483a..ea1b4f2b 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -640,6 +640,16 @@ "num_bounded_loops": null } ], + "test/Proxy.t.sol:ProxyTest": [ + { + "name": "checkFoo(uint256)", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Revert.t.sol:CTest": [ { "name": "checkRevert1(uint256)", @@ -921,4 +931,4 @@ } ] } -} +} \ No newline at end of file diff --git a/tests/expected/counter-symbolic.json b/tests/expected/counter-symbolic.json index 766804a6..47aeab59 100644 --- a/tests/expected/counter-symbolic.json +++ b/tests/expected/counter-symbolic.json @@ -124,4 +124,4 @@ } ] } -} +} \ No newline at end of file diff --git a/tests/expected/list-symbolic.json b/tests/expected/list-symbolic.json index 31d64c93..58a42fa4 100644 --- a/tests/expected/list-symbolic.json +++ b/tests/expected/list-symbolic.json @@ -28,4 +28,4 @@ } ] } -} +} \ No newline at end of file diff --git a/tests/expected/storage-symbolic.json b/tests/expected/storage-symbolic.json index 4bda94f9..89fa8c91 100644 --- a/tests/expected/storage-symbolic.json +++ b/tests/expected/storage-symbolic.json @@ -52,4 +52,4 @@ } ] } -} +} \ No newline at end of file From a59a9a53e02a8e8ed4866871d751060d501b74a2 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:46:31 -0700 Subject: [PATCH 12/30] add submodule halmos-cheatcodes --- .gitmodules | 3 +++ tests/lib/halmos-cheatcodes | 1 + 2 files changed, 4 insertions(+) create mode 160000 tests/lib/halmos-cheatcodes diff --git a/.gitmodules b/.gitmodules index 0472303c..988272f1 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "tests/lib/openzeppelin-contracts"] path = tests/lib/openzeppelin-contracts url = https://github.com/OpenZeppelin/openzeppelin-contracts.git +[submodule "tests/lib/halmos-cheatcodes"] + path = tests/lib/halmos-cheatcodes + url = https://github.com/a16z/halmos-cheatcodes diff --git a/tests/lib/halmos-cheatcodes b/tests/lib/halmos-cheatcodes new file mode 160000 index 00000000..d988df8e --- /dev/null +++ b/tests/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit d988df8e812d43df84095febf09e7dd9402c3fbb From 5d47f02a319aa4abdc7a67ec9cc608436463318b Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:50:29 -0700 Subject: [PATCH 13/30] update tests --- tests/test/HalmosCheatCode.t.sol | 27 +-------------------------- 1 file changed, 1 insertion(+), 26 deletions(-) diff --git a/tests/test/HalmosCheatCode.t.sol b/tests/test/HalmosCheatCode.t.sol index 72310b33..0df41e5c 100644 --- a/tests/test/HalmosCheatCode.t.sol +++ b/tests/test/HalmosCheatCode.t.sol @@ -1,32 +1,7 @@ // SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0; -interface SVM { - // Create a new symbolic uint value ranging over [0, 2**bitSize - 1] (inclusive) - function createUint(uint256 bitSize, string memory name) external returns (uint256 value); - - // Create a new symbolic byte array with the given byte size - function createBytes(uint256 byteSize, string memory name) external returns (bytes memory value); - - // Create a new symbolic uint256 value - function createUint256(string memory name) external returns (uint256 value); - - // Create a new symbolic bytes32 value - function createBytes32(string memory name) external returns (bytes32 value); - - // Create a new symbolic address value - function createAddress(string memory name) external returns (address value); - - // Create a new symbolic boolean value - function createBool(string memory name) external returns (bool value); -} - -abstract contract SymTest { - // SVM cheat code address: 0xf3993a62377bcd56ae39d773740a5390411e8bc9 - address internal constant SVM_ADDRESS = address(uint160(uint256(keccak256("svm cheat code")))); - - SVM internal constant svm = SVM(SVM_ADDRESS); -} +import {SymTest} from "halmos-cheatcodes/SymTest.sol"; contract HalmosCheatCodeTest is SymTest { function checkSymbolicUint() public { From 06f1dee197f143e0127ef51c0039cacee47a5128 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:53:01 -0700 Subject: [PATCH 14/30] update forge-std submodule --- tests/lib/forge-std | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lib/forge-std b/tests/lib/forge-std index 066ff16c..74cfb77e 160000 --- a/tests/lib/forge-std +++ b/tests/lib/forge-std @@ -1 +1 @@ -Subproject commit 066ff16c5c03e6f931cd041fd366bc4be1fae82a +Subproject commit 74cfb77e308dd188d2f58864aaf44963ae6b88b1 From 56d751690d98cc33804370bc7caef905aec42380 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 22:55:40 -0700 Subject: [PATCH 15/30] fix lint error --- tests/test_halmos.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/tests/test_halmos.py b/tests/test_halmos.py index 172c45e6..da5cfc46 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -35,7 +35,15 @@ "tests/expected/storage-symbolic.json", ), ( - ["--root", "examples", "--loop", "256", "--solver-fresh", "--function", "test"], + [ + "--root", + "examples", + "--loop", + "256", + "--solver-fresh", + "--function", + "test", + ], "tests/expected/examples.json", ), ], From 901d96ca0dcbb42bbd850ac6309eb02604d8758d Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 23:06:26 -0700 Subject: [PATCH 16/30] add reset test --- tests/expected/all.json | 10 ++++++++++ tests/expected/reset.json | 15 +++++++++++++++ tests/test/Reset.t.sol | 23 +++++++++++++++++++++++ 3 files changed, 48 insertions(+) create mode 100644 tests/expected/reset.json create mode 100644 tests/test/Reset.t.sol diff --git a/tests/expected/all.json b/tests/expected/all.json index ea1b4f2b..d2d2f9f6 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -650,6 +650,16 @@ "num_bounded_loops": null } ], + "test/Reset.t.sol:ResetTest": [ + { + "name": "checkFoo()", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Revert.t.sol:CTest": [ { "name": "checkRevert1(uint256)", diff --git a/tests/expected/reset.json b/tests/expected/reset.json new file mode 100644 index 00000000..b435296e --- /dev/null +++ b/tests/expected/reset.json @@ -0,0 +1,15 @@ +{ + "exitcode": 0, + "test_results": { + "test/Reset.t.sol:ResetTest": [ + { + "name": "checkFoo()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ] + } +} \ No newline at end of file diff --git a/tests/test/Reset.t.sol b/tests/test/Reset.t.sol new file mode 100644 index 00000000..1905e9db --- /dev/null +++ b/tests/test/Reset.t.sol @@ -0,0 +1,23 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +// NOTE: required options: --reset-bytecode '0xaaaa0002=0x6080604052348015600f57600080fd5b506004361060285760003560e01c8063c298557814602d575b600080fd5b600260405190815260200160405180910390f3fea2646970667358221220c2880ecd3d663c2d8a036163ee7c5d65b9a7d1749e1132fd8ff89646c6621d5764736f6c63430008130033' + +contract C { + function foo() public pure returns (uint) { + return 1; + } +} + +contract ResetTest { + C c; + + function setUp() public { + c = new C(); + } + + function checkFoo() public view { + assert(c.foo() == 2); // for testing --reset-bytecode option + } + +} From 4e6937fee3bc18f8f5e9f33f06667701646b8961 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 23:12:41 -0700 Subject: [PATCH 17/30] add own reset test --- tests/test_halmos.py | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/tests/test_halmos.py b/tests/test_halmos.py index da5cfc46..2c08ee4f 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -46,6 +46,17 @@ ], "tests/expected/examples.json", ), + ( + [ + "--root", + "tests", + "--contract", + "ResetTest", + "--reset-bytecode", + "0xaaaa0002=0x6080604052348015600f57600080fd5b506004361060285760003560e01c8063c298557814602d575b600080fd5b600260405190815260200160405180910390f3fea2646970667358221220c2880ecd3d663c2d8a036163ee7c5d65b9a7d1749e1132fd8ff89646c6621d5764736f6c63430008130033", + ], + "tests/expected/reset.json", + ), ], ) @pytest.mark.parametrize( From 284f3104c009c64434fcfc88b865f0567d38da5a Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 23:27:26 -0700 Subject: [PATCH 18/30] add pytest -v -s options --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 244abeab..cfd8a5a7 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -41,4 +41,4 @@ jobs: run: pip install -e . - name: Run pytest - run: pytest + run: pytest -v -s From a36e7c573482007db10e30cc80702d237d2daadd Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 17 Jul 2023 23:41:07 -0700 Subject: [PATCH 19/30] add halmos -v -st options --- tests/test_halmos.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_halmos.py b/tests/test_halmos.py index 2c08ee4f..f731a941 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -69,7 +69,7 @@ ], ) def test_main(cmd, expected_path, parallel_options): - actual = asdict(_main(cmd + parallel_options)) + actual = asdict(_main(["-v", "-st"] + cmd + parallel_options)) with open(expected_path, encoding="utf8") as f: expected = json.load(f) assert expected["exitcode"] == actual["exitcode"] From 67ba4d4f3aef8cd086ec5de957763b7048a5308e Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 01:57:59 -0700 Subject: [PATCH 20/30] add external repo tests --- .github/workflows/test-external.yml | 48 +++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 .github/workflows/test-external.yml diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml new file mode 100644 index 00000000..1024dd58 --- /dev/null +++ b/.github/workflows/test-external.yml @@ -0,0 +1,48 @@ +name: Test external projects + +on: + push: + branches: [main] + pull_request: + branches: [main] + +jobs: + test: + runs-on: ubuntu-latest + + strategy: + matrix: + parallel: ["", "--test-parallel", "--solver-parallel", "--test-parallel --solver-parallel"] + + steps: + - name: Checkout + uses: actions/checkout@v3 + with: + path: halmos + submodules: recursive + + - name: Checkout external repo + uses: actions/checkout@v3 + with: + repository: morpho-org/morpho-data-structures + path: morpho-data-structures + submodules: recursive + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: "3.11" + + - name: Install dependencies + run: python -m pip install --upgrade pip + + - name: Install Halmos + run: python -m pip install -e . + working-directory: ./halmos + + - name: Test external repo + run: halmos --function testProve --loop 4 --symbolic-storage --solver-timeout-assertion 60000 ${{ matrix.parallel }} + working-directory: ./morpho-data-structures From 4aafa7e738f13a82da82a2b3612774128c2631e0 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 02:28:33 -0700 Subject: [PATCH 21/30] parameterize external tests workflow --- .github/workflows/test-external.yml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 1024dd58..a1b163fd 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -13,6 +13,10 @@ jobs: strategy: matrix: parallel: ["", "--test-parallel", "--solver-parallel", "--test-parallel --solver-parallel"] + include: + - repo: "morpho-org/morpho-data-structures" + dir: "morpho-data-structures" + cmd: "halmos --function testProve --loop 4 --symbolic-storage --solver-timeout-assertion 60000" steps: - name: Checkout @@ -24,8 +28,8 @@ jobs: - name: Checkout external repo uses: actions/checkout@v3 with: - repository: morpho-org/morpho-data-structures - path: morpho-data-structures + repository: ${{ matrix.repo }} + path: ${{ matrix.dir }} submodules: recursive - name: Install Foundry @@ -44,5 +48,5 @@ jobs: working-directory: ./halmos - name: Test external repo - run: halmos --function testProve --loop 4 --symbolic-storage --solver-timeout-assertion 60000 ${{ matrix.parallel }} - working-directory: ./morpho-data-structures + run: ${{ matrix.cmd }} ${{ matrix.parallel }} + working-directory: ${{ matrix.dir }} From 331ce864060165bd72cf55e0b19bd6efa80e4f1c Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 03:12:04 -0700 Subject: [PATCH 22/30] add cicada external tests --- .github/workflows/test-external.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index a1b163fd..93d35d8e 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -17,6 +17,9 @@ jobs: - repo: "morpho-org/morpho-data-structures" dir: "morpho-data-structures" cmd: "halmos --function testProve --loop 4 --symbolic-storage --solver-timeout-assertion 60000" + - repo: "a16z/cicada" + dir: "cicada" + cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 60000" steps: - name: Checkout @@ -44,8 +47,7 @@ jobs: run: python -m pip install --upgrade pip - name: Install Halmos - run: python -m pip install -e . - working-directory: ./halmos + run: python -m pip install -e ./halmos - name: Test external repo run: ${{ matrix.cmd }} ${{ matrix.parallel }} From 9e32f1cca4d34c65ba1a32b0dda98be9eaf09bab Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 03:22:38 -0700 Subject: [PATCH 23/30] update external test ci --- .github/workflows/test-external.yml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 93d35d8e..338e7b3c 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -12,14 +12,19 @@ jobs: strategy: matrix: - parallel: ["", "--test-parallel", "--solver-parallel", "--test-parallel --solver-parallel"] include: - repo: "morpho-org/morpho-data-structures" dir: "morpho-data-structures" - cmd: "halmos --function testProve --loop 4 --symbolic-storage --solver-timeout-assertion 60000" + cmd: "halmos --function testProve --loop 4 --symbolic-storage --test-parallel --solver-parallel --solver-timeout-assertion 60000" + branch: "" - repo: "a16z/cicada" dir: "cicada" - cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 60000" + cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 80000" + branch: "test/halmos" + - repo: "a16z/cicada" + dir: "cicada" + cmd: "halmos -v -st --contract LibPrimeTest --function testProve --loop 256 --test-parallel" + branch: "test/halmos" steps: - name: Checkout @@ -33,6 +38,7 @@ jobs: with: repository: ${{ matrix.repo }} path: ${{ matrix.dir }} + ref: ${{ matrix.branch }} submodules: recursive - name: Install Foundry @@ -50,5 +56,5 @@ jobs: run: python -m pip install -e ./halmos - name: Test external repo - run: ${{ matrix.cmd }} ${{ matrix.parallel }} + run: ${{ matrix.cmd }} working-directory: ${{ matrix.dir }} From eb9432966bfed385c37fcc2c7be8c8947a1b1642 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 03:48:52 -0700 Subject: [PATCH 24/30] increase timeout --- .github/workflows/test-external.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 338e7b3c..fda787dc 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -19,7 +19,7 @@ jobs: branch: "" - repo: "a16z/cicada" dir: "cicada" - cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 80000" + cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 200000" branch: "test/halmos" - repo: "a16z/cicada" dir: "cicada" From 4fc00fbf509f685aa2e9410647c3ef4548190e8b Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 04:18:34 -0700 Subject: [PATCH 25/30] improve json parsing fail handler --- src/halmos/__main__.py | 84 +++++++++++++++++++++++------------------- 1 file changed, 46 insertions(+), 38 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 7cbdc0b9..d71e3b4c 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1074,44 +1074,50 @@ def parse_build_out(args: argparse.Namespace) -> Dict: continue for json_filename in os.listdir(sol_path): # for each contract name - if not json_filename.endswith(".json"): - continue - if json_filename.startswith("."): - continue + try: + if not json_filename.endswith(".json"): + continue + if json_filename.startswith("."): + continue - json_path = os.path.join(sol_path, json_filename) - with open(json_path, encoding="utf8") as f: - json_out = json.load(f) - - compiler_version = json_out["metadata"]["compiler"]["version"] - if compiler_version not in result: - result[compiler_version] = {} - if sol_dirname not in result[compiler_version]: - result[compiler_version][sol_dirname] = {} - contract_map = result[compiler_version][sol_dirname] - - # cut off compiler version number as well - contract_name = json_filename.split(".")[0] - - contract_type = None - for node in json_out["ast"]["nodes"]: - if ( - node["nodeType"] == "ContractDefinition" - and node["name"] == contract_name - ): - abstract = "abstract " if node.get("abstract") else "" - contract_type = abstract + node["contractKind"] - break - if contract_type is None: - raise ValueError("no contract type", contract_name) - - if contract_name in contract_map: - raise ValueError( - "duplicate contract names in the same file", - contract_name, - sol_dirname, - ) - contract_map[contract_name] = (json_out, contract_type) + json_path = os.path.join(sol_path, json_filename) + with open(json_path, encoding="utf8") as f: + json_out = json.load(f) + + compiler_version = json_out["metadata"]["compiler"]["version"] + if compiler_version not in result: + result[compiler_version] = {} + if sol_dirname not in result[compiler_version]: + result[compiler_version][sol_dirname] = {} + contract_map = result[compiler_version][sol_dirname] + + # cut off compiler version number as well + contract_name = json_filename.split(".")[0] + + contract_type = None + for node in json_out["ast"]["nodes"]: + if ( + node["nodeType"] == "ContractDefinition" + and node["name"] == contract_name + ): + abstract = "abstract " if node.get("abstract") else "" + contract_type = abstract + node["contractKind"] + break + if contract_type is None: + raise ValueError("no contract type", contract_name) + + if contract_name in contract_map: + raise ValueError( + "duplicate contract names in the same file", + contract_name, + sol_dirname, + ) + contract_map[contract_name] = (json_out, contract_type) + except Exception as err: + print(color_warn(f"skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}")) + if args.debug: + traceback.print_exc() + continue return result @@ -1174,7 +1180,9 @@ def _main(argv=None) -> MainResult: try: build_out = parse_build_out(args) except Exception as err: - print(color_warn(f"build output parsing failed: {err}")) + print(color_warn(f"build output parsing failed: {type(err).__name__}: {err}")) + if args.debug: + traceback.print_exc() return MainResult(1) main_mid = timer() From 308b5a22dce8bb8503861e0bf76ebeef3b2e6140 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 04:37:25 -0700 Subject: [PATCH 26/30] add farcaster tests --- .github/workflows/test-external.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index fda787dc..17ca545d 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -25,6 +25,10 @@ jobs: dir: "cicada" cmd: "halmos -v -st --contract LibPrimeTest --function testProve --loop 256 --test-parallel" branch: "test/halmos" + - repo: "farcasterxyz/contracts" + dir: "farcaster-contracts" + cmd: "halmos -v -st --test-parallel --solver-parallel --solver-timeout-assertion 60000" + branch: "halmos/symtest" steps: - name: Checkout From e771713334793b5f52a49908a0877e54e28de7cd Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 05:53:26 -0700 Subject: [PATCH 27/30] update ci --- .github/workflows/test-external.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 17ca545d..60860fa1 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -19,7 +19,7 @@ jobs: branch: "" - repo: "a16z/cicada" dir: "cicada" - cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 200000" + cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 300000" branch: "test/halmos" - repo: "a16z/cicada" dir: "cicada" @@ -28,7 +28,7 @@ jobs: - repo: "farcasterxyz/contracts" dir: "farcaster-contracts" cmd: "halmos -v -st --test-parallel --solver-parallel --solver-timeout-assertion 60000" - branch: "halmos/symtest" + branch: "test/halmos" steps: - name: Checkout From fadf77c64b832074dfb96a80459f617884f4ddb6 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 06:08:32 -0700 Subject: [PATCH 28/30] try running external tests in macos --- .github/workflows/test-external.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 60860fa1..9b45a6e0 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -8,7 +8,7 @@ on: jobs: test: - runs-on: ubuntu-latest + runs-on: macos-latest strategy: matrix: From 1ef16c1f395ec33b4a78b894ca7b53aa326e5fb9 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 06:47:10 -0700 Subject: [PATCH 29/30] ci: increase timeout --- .github/workflows/test-external.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 9b45a6e0..682c8dfb 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -19,7 +19,7 @@ jobs: branch: "" - repo: "a16z/cicada" dir: "cicada" - cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 300000" + cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 400000" branch: "test/halmos" - repo: "a16z/cicada" dir: "cicada" From a2ac789616bd68123a13dfd4bd0e30e81940ae96 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 18 Jul 2023 07:15:15 -0700 Subject: [PATCH 30/30] ci: increase timeout --- .github/workflows/test-external.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 682c8dfb..7e395c61 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -19,7 +19,7 @@ jobs: branch: "" - repo: "a16z/cicada" dir: "cicada" - cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 400000" + cmd: "halmos -v -st --contract LibUint1024Test --function testProve --loop 256 --test-parallel --solver-parallel --solver-timeout-assertion 1000000" branch: "test/halmos" - repo: "a16z/cicada" dir: "cicada"