From 0b922230380c042ed31ea8f8e29568a3f469e09a Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 20 Jul 2023 17:51:29 -0700 Subject: [PATCH] feat: support natspec annotations (#133) --- examples/test/Example.t.sol | 3 + src/halmos/__main__.py | 348 ++++++++++++------------------------ src/halmos/parser.py | 207 +++++++++++++++++++++ tests/expected/all.json | 132 +++++++++++++- tests/test/Counter.t.sol | 3 +- tests/test/List.t.sol | 4 +- tests/test/Natspec.t.sol | 108 +++++++++++ tests/test/Reset.t.sol | 3 +- tests/test/Storage.t.sol | 3 +- tests/test_cli.py | 2 +- tests/test_fixtures.py | 4 +- tests/test_halmos.py | 34 ---- 12 files changed, 563 insertions(+), 288 deletions(-) create mode 100644 src/halmos/parser.py create mode 100644 tests/test/Natspec.t.sol diff --git a/examples/test/Example.t.sol b/examples/test/Example.t.sol index be457df8..f8cd6c9d 100644 --- a/examples/test/Example.t.sol +++ b/examples/test/Example.t.sol @@ -3,6 +3,7 @@ pragma solidity >=0.8.0 <0.9.0; import "../src/Example.sol"; +/// @custom:halmos --solver-fresh contract ExampleTest is Example { function testTotalPriceBuggy(uint96 price, uint32 quantity) public pure { @@ -27,6 +28,7 @@ contract ExampleTest is Example { assert(result1 == result2); } + /// @custom:halmos --loop 256 function testIsPowerOfTwo(uint256 x) public pure { bool result1 = isPowerOfTwo(x); bool result2 = false; @@ -39,6 +41,7 @@ contract ExampleTest is Example { assert(result1 == result2); } + /// @custom:halmos --loop 256 function testIsPowerOfTwoEq(uint x) public pure { bool result1 = isPowerOfTwo(x); bool result2 = isPowerOfTwoIter(x); diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index d5e942e3..234a649a 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -5,10 +5,10 @@ import subprocess import uuid import json -import argparse import re import traceback +from argparse import Namespace from dataclasses import dataclass, asdict from timeit import default_timer as timer from importlib import metadata @@ -17,12 +17,9 @@ from .sevm import * from .utils import color_good, color_warn, hexify from .warnings import * +from .parser import mk_arg_parser -SETUP_FAILED = 127 -TEST_FAILED = 128 - -args: argparse.Namespace - +arg_parser = mk_arg_parser() # Python version >=3.8.14, >=3.9.14, >=3.10.7, or >=3.11 if hasattr(sys, "set_int_max_str_digits"): @@ -33,209 +30,6 @@ sys.stdout.reconfigure(encoding="utf-8") -def parse_args(args=None) -> argparse.Namespace: - parser = argparse.ArgumentParser( - prog="halmos", epilog="For more information, see https://github.com/a16z/halmos" - ) - - parser.add_argument( - "--root", - metavar="DIRECTORY", - default=os.getcwd(), - help="source root directory (default: current directory)", - ) - parser.add_argument( - "--contract", - metavar="CONTRACT_NAME", - help="run tests in the given contract only", - ) - parser.add_argument( - "--function", - metavar="FUNCTION_NAME_PREFIX", - default="check", - help="run tests matching the given prefix only (default: %(default)s)", - ) - - parser.add_argument( - "--loop", - metavar="MAX_BOUND", - type=int, - default=2, - help="set loop unrolling bounds (default: %(default)s)", - ) - parser.add_argument( - "--width", metavar="MAX_WIDTH", type=int, help="set the max number of paths" - ) - parser.add_argument( - "--depth", metavar="MAX_DEPTH", type=int, help="set the max path length" - ) - parser.add_argument( - "--array-lengths", - metavar="NAME1=LENGTH1,NAME2=LENGTH2,...", - help="set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound)", - ) - - parser.add_argument( - "--symbolic-storage", - action="store_true", - help="set default storage values to symbolic", - ) - parser.add_argument( - "--symbolic-msg-sender", action="store_true", help="set msg.sender symbolic" - ) - - parser.add_argument( - "--version", action="store_true", help="print the version number" - ) - - # debugging options - group_debug = parser.add_argument_group("Debugging options") - - group_debug.add_argument( - "-v", - "--verbose", - action="count", - default=0, - help="increase verbosity levels: -v, -vv, -vvv, ...", - ) - group_debug.add_argument( - "-st", "--statistics", action="store_true", help="print statistics" - ) - group_debug.add_argument("--debug", action="store_true", help="run in debug mode") - group_debug.add_argument( - "--log", metavar="LOG_FILE_PATH", help="log every execution steps in JSON" - ) - 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" - ) - group_debug.add_argument( - "--print-states", action="store_true", help="print all final execution states" - ) - group_debug.add_argument( - "--print-failed-states", - action="store_true", - help="print failed execution states", - ) - group_debug.add_argument( - "--print-blocked-states", - action="store_true", - help="print blocked execution states", - ) - group_debug.add_argument( - "--print-setup-states", action="store_true", help="print setup execution states" - ) - group_debug.add_argument( - "--print-full-model", - action="store_true", - help="print full counterexample model", - ) - - # build options - group_build = parser.add_argument_group("Build options") - - group_build.add_argument( - "--forge-build-out", - metavar="DIRECTORY_NAME", - default="out", - help="forge build artifacts directory name (default: %(default)s)", - ) - - # smt solver options - group_solver = parser.add_argument_group("Solver options") - - group_solver.add_argument( - "--no-smt-add", action="store_true", help="do not interpret `+`" - ) - group_solver.add_argument( - "--no-smt-sub", action="store_true", help="do not interpret `-`" - ) - group_solver.add_argument( - "--no-smt-mul", action="store_true", help="do not interpret `*`" - ) - group_solver.add_argument("--smt-div", action="store_true", help="interpret `/`") - group_solver.add_argument("--smt-mod", action="store_true", help="interpret `mod`") - group_solver.add_argument( - "--smt-div-by-const", action="store_true", help="interpret division by constant" - ) - group_solver.add_argument( - "--smt-mod-by-const", action="store_true", help="interpret constant modulo" - ) - group_solver.add_argument( - "--smt-exp-by-const", - metavar="N", - type=int, - default=2, - help="interpret constant power up to N (default: %(default)s)", - ) - - group_solver.add_argument( - "--solver-timeout-branching", - metavar="TIMEOUT", - type=int, - default=1, - help="set timeout (in milliseconds) for solving branching conditions (default: %(default)s)", - ) - group_solver.add_argument( - "--solver-timeout-assertion", - metavar="TIMEOUT", - type=int, - default=1000, - help="set timeout (in milliseconds) for solving assertion violation conditions (default: %(default)s)", - ) - group_solver.add_argument( - "--solver-fresh", - action="store_true", - help="run an extra solver with a fresh state for unknown", - ) - group_solver.add_argument( - "--solver-subprocess", - action="store_true", - help="run an extra solver in subprocess for unknown", - ) - group_solver.add_argument( - "--solver-parallel", - action="store_true", - help="run assertion solvers in parallel", - ) - - # internal options - group_internal = parser.add_argument_group("Internal options") - - group_internal.add_argument( - "--bytecode", metavar="HEX_STRING", help="execute the given bytecode" - ) - group_internal.add_argument( - "--reset-bytecode", - metavar="ADDR1=CODE1,ADDR2=CODE2,...", - help="reset the bytecode of given addresses after setUp()", - ) - group_internal.add_argument( - "--test-parallel", action="store_true", help="run tests in parallel" - ) - - # experimental options - group_experimental = parser.add_argument_group("Experimental options") - - group_experimental.add_argument( - "--symbolic-jump", action="store_true", help="support symbolic jump destination" - ) - group_experimental.add_argument( - "--print-potential-counterexample", - action="store_true", - help="print potentially invalid counterexamples", - ) - - return parser.parse_args(args) - - @dataclass(frozen=True) class FunctionInfo: name: Optional[str] = None @@ -276,7 +70,7 @@ def mk_calldata( fun_info: FunctionInfo, cd: List, dyn_param_size: List[str], - args: argparse.Namespace, + args: Namespace, ) -> None: item = find_abi(abi, fun_info) tba = [] @@ -374,7 +168,7 @@ def mk_addr(name: str) -> Address: return BitVec(name, 160) -def mk_caller(args: argparse.Namespace) -> Address: +def mk_caller(args: Namespace) -> Address: if args.symbolic_msg_sender: return mk_addr("msg_sender") else: @@ -385,14 +179,14 @@ def mk_this() -> Address: return con_addr(magic_address + 1) -def mk_solver(args: argparse.Namespace): +def mk_solver(args: Namespace): # quantifier-free bitvector + array theory; https://smtlib.cs.uiowa.edu/logics.shtml solver = SolverFor("QF_AUFBV") solver.set(timeout=args.solver_timeout_branching) return solver -def run_bytecode(hexcode: str) -> List[Exec]: +def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]: contract = Contract.from_hexcode(hexcode) storage = {} @@ -441,7 +235,7 @@ def setup( hexcode: str, abi: List, setup_info: FunctionInfo, - args: argparse.Namespace, + args: Namespace, ) -> Exec: setup_start = timer() @@ -474,6 +268,9 @@ def setup( setup_info.selector, ) if setup_sig: + if args.verbose >= 1: + print(f"Running {setup_sig}") + wstore(setup_ex.calldata, 0, 4, BitVecVal(int(setup_selector, 16), 32)) dyn_param_size = [] # TODO: propagate to run mk_calldata(abi, setup_info, setup_ex.calldata, dyn_param_size, args) @@ -558,7 +355,7 @@ def run( setup_ex: Exec, abi: List, fun_info: FunctionInfo, - args: argparse.Namespace, + args: Namespace, ) -> TestResult: funname, funsig, funselector = fun_info.name, fun_info.sig, fun_info.selector if args.verbose >= 1: @@ -758,16 +555,18 @@ class SetupAndRunSingleArgs: abi: List setup_info: FunctionInfo fun_info: FunctionInfo - args: argparse.Namespace + setup_args: Namespace + args: Namespace def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> List[TestResult]: + args = fn_args.args try: setup_ex = setup( fn_args.hexcode, fn_args.abi, fn_args.setup_info, - fn_args.args, + fn_args.setup_args, ) except Exception as err: print( @@ -824,8 +623,12 @@ class RunArgs: abi: List methodIdentifiers: Dict[str, str] + args: Namespace + contract_json: Dict + def run_parallel(run_args: RunArgs) -> List[TestResult]: + args = run_args.args hexcode, abi, methodIdentifiers = ( run_args.hexcode, run_args.abi, @@ -833,15 +636,20 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: ) setup_info = extract_setup(methodIdentifiers) - if setup_info.sig and args.verbose >= 1: - print(f"Running {setup_info.sig}") fun_infos = [ FunctionInfo(funsig.split("(")[0], funsig, methodIdentifiers[funsig]) for funsig in run_args.funsigs ] single_run_args = [ - SetupAndRunSingleArgs(hexcode, abi, setup_info, fun_info, args) + SetupAndRunSingleArgs( + hexcode, + abi, + setup_info, + fun_info, + extend_args(args, parse_devdoc(setup_info.sig, run_args.contract_json)), + extend_args(args, parse_devdoc(fun_info.sig, run_args.contract_json)), + ) for fun_info in fun_infos ] @@ -853,12 +661,14 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: def run_sequential(run_args: RunArgs) -> List[TestResult]: + args = run_args.args setup_info = extract_setup(run_args.methodIdentifiers) - if setup_info.sig and args.verbose >= 1: - print(f"Running {setup_info.sig}") try: - setup_ex = setup(run_args.hexcode, run_args.abi, setup_info, args) + setup_args = extend_args( + args, parse_devdoc(setup_info.sig, run_args.contract_json) + ) + setup_ex = setup(run_args.hexcode, run_args.abi, setup_info, setup_args) except Exception as err: print( color_warn(f"Error: {setup_info.sig} failed: {type(err).__name__}: {err}") @@ -873,7 +683,10 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: funsig.split("(")[0], funsig, run_args.methodIdentifiers[funsig] ) try: - test_result = run(setup_ex, run_args.abi, fun_info, args) + extended_args = extend_args( + args, parse_devdoc(funsig, run_args.contract_json) + ) + test_result = run(setup_ex, run_args.abi, fun_info, extended_args) except Exception as err: print(f"{color_warn('[SKIP]')} {funsig}") print(color_warn(f"{type(err).__name__}: {err}")) @@ -887,9 +700,18 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: return test_results +def extend_args(args: Namespace, more_opts: str) -> Namespace: + if more_opts: + new_args = deepcopy(args) + arg_parser.parse_args(more_opts.split(), new_args) + return new_args + else: + return args + + @dataclass(frozen=True) class GenModelArgs: - args: argparse.Namespace + args: Namespace idx: int sexpr: str @@ -911,7 +733,7 @@ def is_unknown(result: CheckSatResult, model: Model) -> bool: return result == unknown or (result == sat and not is_valid_model(model)) -def gen_model(args: argparse.Namespace, idx: int, ex: Exec) -> ModelWithContext: +def gen_model(args: Namespace, idx: int, ex: Exec) -> ModelWithContext: if args.verbose >= 1: print(f"Checking path condition (path id: {idx+1})") @@ -967,7 +789,7 @@ def package_result( model: UnionType[Model, str], idx: int, result: CheckSatResult, - args: argparse.Namespace, + args: Namespace, ) -> ModelWithContext: if result == unsat: if args.verbose >= 1: @@ -1003,7 +825,7 @@ def is_valid_model(model) -> bool: return True -def str_model(model, args: argparse.Namespace) -> str: +def str_model(model, args: Namespace) -> str: def select(var): name = str(var) return name.startswith("p_") or name.startswith("halmos_") @@ -1013,7 +835,7 @@ def select(var): return "".join(sorted(formatted)) if formatted else "∅" -def mk_options(args: argparse.Namespace) -> Dict: +def mk_options(args: Namespace) -> Dict: options = { "target": args.root, "verbose": args.verbose, @@ -1044,7 +866,7 @@ def mk_options(args: argparse.Namespace) -> Dict: return options -def mk_arrlen(args: argparse.Namespace) -> Dict[str, int]: +def mk_arrlen(args: Namespace) -> Dict[str, int]: arrlen = {} if args.array_lengths: for assign in [x.split("=") for x in args.array_lengths.split(",")]: @@ -1054,7 +876,7 @@ def mk_arrlen(args: argparse.Namespace) -> Dict[str, int]: return arrlen -def parse_build_out(args: argparse.Namespace) -> Dict: +def parse_build_out(args: Namespace) -> Dict: result = {} # compiler version -> source filename -> contract name -> (json, type) out_path = os.path.join(args.root, args.forge_build_out) @@ -1100,6 +922,7 @@ def parse_build_out(args: argparse.Namespace) -> Dict: ): abstract = "abstract " if node.get("abstract") else "" contract_type = abstract + node["contractKind"] + natspec = node.get("documentation") break if contract_type is None: raise ValueError("no contract type", contract_name) @@ -1110,7 +933,7 @@ def parse_build_out(args: argparse.Namespace) -> Dict: contract_name, sol_dirname, ) - contract_map[contract_name] = (json_out, contract_type) + contract_map[contract_name] = (json_out, contract_type, natspec) except Exception as err: print( color_warn( @@ -1124,6 +947,43 @@ def parse_build_out(args: argparse.Namespace) -> Dict: return result +def parse_devdoc(funsig: str, contract_json: Dict) -> str: + try: + return contract_json["metadata"]["output"]["devdoc"]["methods"][funsig][ + "custom:halmos" + ] + except KeyError as err: + return None + + +def parse_natspec(natspec: Dict) -> str: + # This parsing scheme is designed to handle: + # + # - multiline tags: + # /// @custom:halmos --x + # /// --y + # + # - multiple tags: + # /// @custom:halmos --x + # /// @custom:halmos --y + # + # - tags that start in the middle of line: + # /// blah blah @custom:halmos --x + # /// --y + # + # In all the above examples, this scheme returns "--x (whitespaces) --y" + isHalmosTag = False + result = "" + for item in re.split(r"(@\S+)", natspec.get("text", "")): + if item == "@custom:halmos": + isHalmosTag = True + elif re.match(r"^@\S", item): + isHalmosTag = False + elif isHalmosTag: + result += item + return result.strip() + + @dataclass(frozen=True) class MainResult: exitcode: int @@ -1131,7 +991,7 @@ class MainResult: test_results: Dict[str, List[TestResult]] = None -def _main(argv=None) -> MainResult: +def _main(_args=None) -> MainResult: main_start = timer() # @@ -1146,8 +1006,7 @@ def _main(argv=None) -> MainResult: # command line arguments # - global args - args = parse_args(argv) + args = arg_parser.parse_args(_args) if args.version: print(f"Halmos {metadata.version('halmos')}") @@ -1155,7 +1014,7 @@ def _main(argv=None) -> MainResult: # quick bytecode execution mode if args.bytecode is not None: - run_bytecode(args.bytecode) + run_bytecode(args.bytecode, args) return MainResult(0) # @@ -1206,7 +1065,9 @@ def _main(argv=None) -> MainResult: if args.contract and args.contract != contract_name: continue - (contract_json, contract_type) = build_out_map[filename][contract_name] + (contract_json, contract_type, natspec) = build_out_map[filename][ + contract_name + ] if contract_type != "contract": continue @@ -1228,7 +1089,18 @@ def _main(argv=None) -> MainResult: print(f"\nRunning {len(funsigs)} tests for {contract_path}") contract_start = timer() - run_args = RunArgs(funsigs, hexcode, abi, methodIdentifiers) + contract_args = ( + extend_args(args, parse_natspec(natspec)) if natspec else args + ) + + run_args = RunArgs( + funsigs, + hexcode, + abi, + methodIdentifiers, + contract_args, + contract_json, + ) enable_parallel = args.test_parallel and len(funsigs) > 1 test_results = ( run_parallel(run_args) diff --git a/src/halmos/parser.py b/src/halmos/parser.py new file mode 100644 index 00000000..b18b9c92 --- /dev/null +++ b/src/halmos/parser.py @@ -0,0 +1,207 @@ +# SPDX-License-Identifier: AGPL-3.0 + +import os +import argparse + + +def mk_arg_parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser( + prog="halmos", epilog="For more information, see https://github.com/a16z/halmos" + ) + + parser.add_argument( + "--root", + metavar="DIRECTORY", + default=os.getcwd(), + help="source root directory (default: current directory)", + ) + parser.add_argument( + "--contract", + metavar="CONTRACT_NAME", + help="run tests in the given contract only", + ) + parser.add_argument( + "--function", + metavar="FUNCTION_NAME_PREFIX", + default="check", + help="run tests matching the given prefix only (default: %(default)s)", + ) + + parser.add_argument( + "--loop", + metavar="MAX_BOUND", + type=int, + default=2, + help="set loop unrolling bounds (default: %(default)s)", + ) + parser.add_argument( + "--width", metavar="MAX_WIDTH", type=int, help="set the max number of paths" + ) + parser.add_argument( + "--depth", metavar="MAX_DEPTH", type=int, help="set the max path length" + ) + parser.add_argument( + "--array-lengths", + metavar="NAME1=LENGTH1,NAME2=LENGTH2,...", + help="set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound)", + ) + + parser.add_argument( + "--symbolic-storage", + action="store_true", + help="set default storage values to symbolic", + ) + parser.add_argument( + "--symbolic-msg-sender", action="store_true", help="set msg.sender symbolic" + ) + + parser.add_argument( + "--version", action="store_true", help="print the version number" + ) + + # debugging options + group_debug = parser.add_argument_group("Debugging options") + + group_debug.add_argument( + "-v", + "--verbose", + action="count", + default=0, + help="increase verbosity levels: -v, -vv, -vvv, ...", + ) + group_debug.add_argument( + "-st", "--statistics", action="store_true", help="print statistics" + ) + group_debug.add_argument("--debug", action="store_true", help="run in debug mode") + group_debug.add_argument( + "--log", metavar="LOG_FILE_PATH", help="log every execution steps in JSON" + ) + 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" + ) + group_debug.add_argument( + "--print-states", action="store_true", help="print all final execution states" + ) + group_debug.add_argument( + "--print-failed-states", + action="store_true", + help="print failed execution states", + ) + group_debug.add_argument( + "--print-blocked-states", + action="store_true", + help="print blocked execution states", + ) + group_debug.add_argument( + "--print-setup-states", action="store_true", help="print setup execution states" + ) + group_debug.add_argument( + "--print-full-model", + action="store_true", + help="print full counterexample model", + ) + + # build options + group_build = parser.add_argument_group("Build options") + + group_build.add_argument( + "--forge-build-out", + metavar="DIRECTORY_NAME", + default="out", + help="forge build artifacts directory name (default: %(default)s)", + ) + + # smt solver options + group_solver = parser.add_argument_group("Solver options") + + group_solver.add_argument( + "--no-smt-add", action="store_true", help="do not interpret `+`" + ) + group_solver.add_argument( + "--no-smt-sub", action="store_true", help="do not interpret `-`" + ) + group_solver.add_argument( + "--no-smt-mul", action="store_true", help="do not interpret `*`" + ) + group_solver.add_argument("--smt-div", action="store_true", help="interpret `/`") + group_solver.add_argument("--smt-mod", action="store_true", help="interpret `mod`") + group_solver.add_argument( + "--smt-div-by-const", action="store_true", help="interpret division by constant" + ) + group_solver.add_argument( + "--smt-mod-by-const", action="store_true", help="interpret constant modulo" + ) + group_solver.add_argument( + "--smt-exp-by-const", + metavar="N", + type=int, + default=2, + help="interpret constant power up to N (default: %(default)s)", + ) + + group_solver.add_argument( + "--solver-timeout-branching", + metavar="TIMEOUT", + type=int, + default=1, + help="set timeout (in milliseconds) for solving branching conditions (default: %(default)s)", + ) + group_solver.add_argument( + "--solver-timeout-assertion", + metavar="TIMEOUT", + type=int, + default=1000, + help="set timeout (in milliseconds) for solving assertion violation conditions (default: %(default)s)", + ) + group_solver.add_argument( + "--solver-fresh", + action="store_true", + help="run an extra solver with a fresh state for unknown", + ) + group_solver.add_argument( + "--solver-subprocess", + action="store_true", + help="run an extra solver in subprocess for unknown", + ) + group_solver.add_argument( + "--solver-parallel", + action="store_true", + help="run assertion solvers in parallel", + ) + + # internal options + group_internal = parser.add_argument_group("Internal options") + + group_internal.add_argument( + "--bytecode", metavar="HEX_STRING", help="execute the given bytecode" + ) + group_internal.add_argument( + "--reset-bytecode", + metavar="ADDR1=CODE1,ADDR2=CODE2,...", + help="reset the bytecode of given addresses after setUp()", + ) + group_internal.add_argument( + "--test-parallel", action="store_true", help="run tests in parallel" + ) + + # experimental options + group_experimental = parser.add_argument_group("Experimental options") + + group_experimental.add_argument( + "--symbolic-jump", action="store_true", help="support symbolic jump destination" + ) + group_experimental.add_argument( + "--print-potential-counterexample", + action="store_true", + help="print potentially invalid counterexamples", + ) + + return parser diff --git a/tests/expected/all.json b/tests/expected/all.json index d2d2f9f6..df893c7e 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -479,7 +479,7 @@ }, { "name": "checkRemove()", - "exitcode": 1, + "exitcode": 0, "num_models": 0, "num_paths": null, "time": null, @@ -487,7 +487,7 @@ }, { "name": "checkSet(uint256,uint256)", - "exitcode": 1, + "exitcode": 0, "num_models": 0, "num_paths": null, "time": null, @@ -530,6 +530,128 @@ "num_bounded_loops": null } ], + "test/Natspec.t.sol:NatspecTestContract": [ + { + "name": "checkLoop3(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop3Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Natspec.t.sol:NatspecTestFunction": [ + { + "name": "checkLoop2(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop2Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop3(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop3Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Natspec.t.sol:NatspecTestNone": [ + { + "name": "checkLoop2(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop2Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Natspec.t.sol:NatspecTestOverwrite": [ + { + "name": "checkLoop3(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop3Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop4(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop4Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], + "test/Natspec.t.sol:NatspecTestSetup": [ + { + "name": "checkLoop2(uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "checkLoop2Fail(uint256)", + "exitcode": 1, + "num_models": 1, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Opcode.t.sol:OpcodeTest": [ { "name": "checkPush0()", @@ -653,8 +775,8 @@ "test/Reset.t.sol:ResetTest": [ { "name": "checkFoo()", - "exitcode": 1, - "num_models": 1, + "exitcode": 0, + "num_models": 0, "num_paths": null, "time": null, "num_bounded_loops": null @@ -767,7 +889,7 @@ }, { "name": "checkAddArr2(uint256,uint256)", - "exitcode": 1, + "exitcode": 0, "num_models": 0, "num_paths": null, "time": null, diff --git a/tests/test/Counter.t.sol b/tests/test/Counter.t.sol index 9fa9b9e8..834d7576 100644 --- a/tests/test/Counter.t.sol +++ b/tests/test/Counter.t.sol @@ -1,10 +1,9 @@ // 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"; +/// @custom:halmos --loop 4 --symbolic-storage contract CounterTest is Counter { function checkSet(uint n) public { set(n); diff --git a/tests/test/List.t.sol b/tests/test/List.t.sol index f93b307f..2889cd1b 100644 --- a/tests/test/List.t.sol +++ b/tests/test/List.t.sol @@ -1,11 +1,10 @@ // 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"; +/// @custom:halmos --symbolic-storage contract ListTest is Test, List { function checkAdd(uint x) public { uint oldSize = arr.length; @@ -33,6 +32,7 @@ contract ListTest is Test, List { } } +/// @custom:halmos --symbolic-storage contract ListTestTest is Test { List list; diff --git a/tests/test/Natspec.t.sol b/tests/test/Natspec.t.sol new file mode 100644 index 00000000..6dbbc76a --- /dev/null +++ b/tests/test/Natspec.t.sol @@ -0,0 +1,108 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +contract NatspecTestNone { + Loop l; + + function setUp() public { + l = new Loop(); + } + + function checkLoop2(uint n) public view { + assert(l.iter(n) <= 2); // pass // default + } + function checkLoop2Fail(uint n) public view { + assert(l.iter(n) <= 1); // fail // default + } +} + +/// @custom:halmos --loop 3 +contract NatspecTestContract { + Loop l; + + function setUp() public { + l = new Loop(); + } + + function checkLoop3(uint n) public view { + assert(l.iter(n) <= 3); // pass // inherited from contract + } + function checkLoop3Fail(uint n) public view { + assert(l.iter(n) <= 2); // fail // inherited from contract + } +} + +contract NatspecTestSetup { + Loop l; + + /// @custom:halmos --loop 3 + function setUp() public { + l = new Loop(); + } + + function checkLoop2(uint n) public view { + assert(l.iter(n) <= 2); // pass // default + } + function checkLoop2Fail(uint n) public view { + assert(l.iter(n) <= 1); // fail // default + } +} + +contract NatspecTestFunction { + Loop l; + + function setUp() public { + l = new Loop(); + } + + /// @custom:halmos --loop 3 + function checkLoop3(uint n) public view { + assert(l.iter(n) <= 3); // pass + } + /// @custom:halmos --loop 3 + function checkLoop3Fail(uint n) public view { + assert(l.iter(n) <= 2); // fail + } + + function checkLoop2(uint n) public view { + assert(l.iter(n) <= 2); // pass // default + } + function checkLoop2Fail(uint n) public view { + assert(l.iter(n) <= 1); // fail // default + } +} + +/// @custom:halmos --loop 4 +contract NatspecTestOverwrite { + Loop l; + + function setUp() public { + l = new Loop(); + } + + function checkLoop4(uint n) public view { + assert(l.iter(n) <= 4); // pass // inherited from contract + } + function checkLoop4Fail(uint n) public view { + assert(l.iter(n) <= 3); // fail // inherited from contract + } + + /// @custom:halmos --loop 3 + function checkLoop3(uint n) public view { + assert(l.iter(n) <= 3); // pass // overwrite + } + /// @custom:halmos --loop 3 + function checkLoop3Fail(uint n) public view { + assert(l.iter(n) <= 2); // fail // overwrite + } +} + +contract Loop { + function iter(uint n) public pure returns (uint) { + uint cnt = 0; + for (uint i = 0; i < n; i++) { + cnt++; + } + return cnt; + } +} diff --git a/tests/test/Reset.t.sol b/tests/test/Reset.t.sol index 1905e9db..63981857 100644 --- a/tests/test/Reset.t.sol +++ b/tests/test/Reset.t.sol @@ -1,14 +1,13 @@ // 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; } } +/// @custom:halmos --reset-bytecode 0xaaaa0002=0x6080604052348015600f57600080fd5b506004361060285760003560e01c8063c298557814602d575b600080fd5b600260405190815260200160405180910390f3fea2646970667358221220c2880ecd3d663c2d8a036163ee7c5d65b9a7d1749e1132fd8ff89646c6621d5764736f6c63430008130033 contract ResetTest { C c; diff --git a/tests/test/Storage.t.sol b/tests/test/Storage.t.sol index c783f832..dfade2be 100644 --- a/tests/test/Storage.t.sol +++ b/tests/test/Storage.t.sol @@ -1,11 +1,10 @@ // 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"; +/// @custom:halmos --symbolic-storage contract StorageTest is Storage { function checkSetMap1(uint k, uint v) public { setMap1(k, v); diff --git a/tests/test_cli.py b/tests/test_cli.py index 4ad8c674..828ba42a 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -114,7 +114,7 @@ def test_run_bytecode(args): args.symbolic_jump = True hexcode = "34381856FDFDFDFDFDFD5B00" - exs = run_bytecode(hexcode) + exs = run_bytecode(hexcode, args) assert len(exs) == 1 assert exs[0].current_opcode() == EVM.STOP diff --git a/tests/test_fixtures.py b/tests/test_fixtures.py index b5948437..733309da 100644 --- a/tests/test_fixtures.py +++ b/tests/test_fixtures.py @@ -2,13 +2,13 @@ from halmos.sevm import SEVM -from halmos.__main__ import parse_args, mk_options +from halmos.__main__ import arg_parser, mk_options import halmos.__main__ @pytest.fixture def args(): - args = parse_args([]) + args = arg_parser.parse_args([]) # set the global args for the main module halmos.__main__.args = args diff --git a/tests/test_halmos.py b/tests/test_halmos.py index 106e0f0a..34a1b2f4 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -14,49 +14,15 @@ ["--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", - ), ( [ "--root", "examples", - "--loop", - "256", - "--solver-fresh", "--function", "test", ], "tests/expected/examples.json", ), - ( - [ - "--root", - "tests", - "--contract", - "ResetTest", - "--reset-bytecode", - "0xaaaa0002=0x6080604052348015600f57600080fd5b506004361060285760003560e01c8063c298557814602d575b600080fd5b600260405190815260200160405180910390f3fea2646970667358221220c2880ecd3d663c2d8a036163ee7c5d65b9a7d1749e1132fd8ff89646c6621d5764736f6c63430008130033", - ], - "tests/expected/reset.json", - ), ], ) @pytest.mark.parametrize(