From 708b1bccae2b9a95e8958f570d19248b60fb82b2 Mon Sep 17 00:00:00 2001 From: sudo rm -rf --no-preserve-root / Date: Sat, 1 Jun 2024 11:20:52 +0200 Subject: [PATCH 1/4] =?UTF-8?q?=F0=9F=94=A8=20Add=20Missing=20Error=20Code?= =?UTF-8?q?=20in=20`parse=5Fbuild=5Fout`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/halmos/__main__.py | 1 + src/halmos/warnings.py | 7 ++++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index e67b5f69..9a15cdb4 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1288,6 +1288,7 @@ def parse_build_out(args: HalmosConfig) -> Dict: contract_map[contract_name] = (json_out, contract_type, natspec) except Exception as err: warn( + PARSING_ERROR, f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}" ) if args.debug: diff --git a/src/halmos/warnings.py b/src/halmos/warnings.py index b589307e..bb8d684e 100644 --- a/src/halmos/warnings.py +++ b/src/halmos/warnings.py @@ -18,13 +18,14 @@ def url(self) -> str: return f"{WARNINGS_BASE_URL}#{self.code}" +PARSING_ERROR = ErrorCode("parsing-error") +INTERNAL_ERROR = ErrorCode("internal-error") +LIBRARY_PLACEHOLDER = ErrorCode("library-placeholder") + COUNTEREXAMPLE_INVALID = ErrorCode("counterexample-invalid") COUNTEREXAMPLE_UNKNOWN = ErrorCode("counterexample-unknown") -INTERNAL_ERROR = ErrorCode("internal-error") UNSUPPORTED_OPCODE = ErrorCode("unsupported-opcode") -LIBRARY_PLACEHOLDER = ErrorCode("library-placeholder") REVERT_ALL = ErrorCode("revert-all") - LOOP_BOUND = ErrorCode("loop-bound") UNINTERPRETED_UNKNOWN_CALLS = ErrorCode("uninterpreted-unknown-calls") From 84e580e9bb047f05e8d0556e9406f2f19caf3b54 Mon Sep 17 00:00:00 2001 From: Pascal Marco Caversaccio Date: Sat, 1 Jun 2024 20:45:32 +0200 Subject: [PATCH 2/4] =?UTF-8?q?=F0=9F=92=84=20Prettify?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Pascal Marco Caversaccio --- src/halmos/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 9a15cdb4..5601db6e 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1289,7 +1289,7 @@ def parse_build_out(args: HalmosConfig) -> Dict: except Exception as err: warn( PARSING_ERROR, - f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}" + f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}", ) if args.debug: traceback.print_exc() From 27c781b3679fac764cfb9fced69fd79f3ad7f90f Mon Sep 17 00:00:00 2001 From: karmacoma Date: Sat, 1 Jun 2024 11:54:38 -0700 Subject: [PATCH 3/4] warnings: rename warn() to warn_code() name conflict was bad all along --- src/halmos/__main__.py | 60 ++++++++++++++++++------------------------ src/halmos/sevm.py | 11 +++++--- src/halmos/utils.py | 2 +- src/halmos/warnings.py | 5 ++-- 4 files changed, 36 insertions(+), 42 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 5601db6e..6421eaa3 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -16,7 +16,7 @@ from enum import Enum from importlib import metadata -from .bytevec import Chunk, ByteVec +from .bytevec import ByteVec from .calldata import Calldata from .config import ( arg_parser, @@ -28,10 +28,6 @@ from .sevm import * from .utils import ( NamedTimer, - color_error, - color_good, - color_info, - color_warn, create_solver, cyan, error, @@ -233,7 +229,7 @@ def rendered_initcode(context: CallContext) -> str: else: initcode_str = hexify(data) - return f"{initcode_str}({color_info(args_str)})" + return f"{initcode_str}({cyan(args_str)})" def render_output(context: CallContext, file=sys.stdout) -> None: @@ -271,10 +267,9 @@ def render_output(context: CallContext, file=sys.stdout) -> None: def rendered_log(log: EventLog) -> str: opcode_str = f"LOG{len(log.topics)}" topics = [ - f"{color_info(f'topic{i}')}={hexify(topic)}" - for i, topic in enumerate(log.topics) + f"{cyan(f'topic{i}')}={hexify(topic)}" for i, topic in enumerate(log.topics) ] - data_str = f"{color_info('data')}={hexify(log.data)}" + data_str = f"{cyan('data')}={hexify(log.data)}" args_str = ", ".join(topics + [data_str]) return f"{opcode_str}({args_str})" @@ -372,7 +367,7 @@ def run_bytecode(hexcode: str, args: HalmosConfig) -> List[Exec]: returndata = ex.context.output.data if error: - warn( + warn_code( INTERNAL_ERROR, f"{mnemonic(opcode)} failed, error={error}, returndata={returndata}", ) @@ -519,7 +514,7 @@ def setup( else: if opcode not in [EVM.REVERT, EVM.INVALID]: - warn( + warn_code( INTERNAL_ERROR, f"Warning: {setup_sig} execution encountered an issue at {mnemonic(opcode)}: {error}", ) @@ -563,7 +558,7 @@ def setup( print(setup_ex) if sevm.logs.bounded_loops: - warn( + warn_code( LOOP_BOUND, f"{setup_sig}: paths have not been fully explored due to the loop unrolling bound: {args.loop}", ) @@ -716,13 +711,13 @@ def future_callback(future_model): print(red(f"Counterexample: {render_model(model)}")) counterexamples.append(model) else: - warn( + warn_code( COUNTEREXAMPLE_INVALID, f"Counterexample (potentially invalid): {render_model(model)}", ) counterexamples.append(model) else: - warn(COUNTEREXAMPLE_UNKNOWN, f"Counterexample: {result}") + warn_code(COUNTEREXAMPLE_UNKNOWN, f"Counterexample: {result}") if args.print_failed_states: print(f"# {idx+1}") @@ -798,23 +793,23 @@ def future_callback(future_model): counter = Counter(str(m.result) for m in models) if counter["sat"] > 0: - passfail = color_warn("[FAIL]") + passfail = red("[FAIL]") exitcode = Exitcode.COUNTEREXAMPLE.value elif counter["unknown"] > 0: - passfail = color_warn("[TIMEOUT]") + passfail = yellow("[TIMEOUT]") exitcode = Exitcode.TIMEOUT.value elif len(stuck) > 0: - passfail = color_warn("[ERROR]") + passfail = red("[ERROR]") exitcode = Exitcode.STUCK.value elif normal == 0: - passfail = color_warn("[ERROR]") + passfail = red("[ERROR]") exitcode = Exitcode.REVERT_ALL.value - warn( + warn_code( REVERT_ALL, f"{funsig}: all paths have been reverted; the setup state or inputs may have been too restrictive.", ) else: - passfail = color_good("[PASS]") + passfail = green("[PASS]") exitcode = Exitcode.PASS.value timer.stop() @@ -826,13 +821,13 @@ def future_callback(future_model): ) for idx, ex, err in stuck: - warn(INTERNAL_ERROR, f"Encountered {err}") + warn_code(INTERNAL_ERROR, f"Encountered {err}") if args.print_blocked_states: print(f"\nPath #{idx+1}") print(traces[idx], end="") if logs.bounded_loops: - warn( + warn_code( LOOP_BOUND, f"{funsig}: paths have not been fully explored due to the loop unrolling bound: {args.loop}", ) @@ -840,7 +835,7 @@ def future_callback(future_model): print("\n".join(logs.bounded_loops)) if logs.unknown_calls: - warn( + warn_code( UNINTERPRETED_UNKNOWN_CALLS, f"{funsig}: unknown calls have been assumed to be static: {', '.join(logs.unknown_calls)}", ) @@ -911,7 +906,7 @@ def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> List[TestResult]: fn_args.args, ) except Exception as err: - print(f"{color_warn('[ERROR]')} {fn_args.fun_info.sig}") + print(f"{color_error('[ERROR]')} {fn_args.fun_info.sig}") error(f"{type(err).__name__}: {err}") if args.debug: traceback.print_exc() @@ -1008,9 +1003,7 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: run_args.libs, ) except Exception as err: - print( - color_warn(f"Error: {setup_info.sig} failed: {type(err).__name__}: {err}") - ) + error(f"Error: {setup_info.sig} failed: {type(err).__name__}: {err}") if args.debug: traceback.print_exc() return [] @@ -1026,8 +1019,8 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: debug(f"{test_config.formatted_layers()}") test_result = run(setup_ex, run_args.abi, fun_info, test_config) except Exception as err: - print(f"{color_warn('[ERROR]')} {funsig}") - print(color_warn(f"{type(err).__name__}: {err}")) + print(f"{color_error('[ERROR]')} {funsig}") + error(f"{type(err).__name__}: {err}") if args.debug: traceback.print_exc() test_results.append(TestResult(funsig, Exitcode.EXCEPTION.value)) @@ -1287,7 +1280,7 @@ def parse_build_out(args: HalmosConfig) -> Dict: ) contract_map[contract_name] = (json_out, contract_type, natspec) except Exception as err: - warn( + warn_code( PARSING_ERROR, f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}", ) @@ -1435,14 +1428,14 @@ def _main(_args=None) -> MainResult: build_exitcode = subprocess.run(build_cmd).returncode if build_exitcode: - print(color_warn(f"Build failed: {build_cmd}")) + error(f"Build failed: {build_cmd}") return MainResult(1) timer.create_subtimer("load") try: build_out = parse_build_out(args) except Exception as err: - print(color_warn(f"Build output parsing failed: {type(err).__name__}: {err}")) + error(f"Build output parsing failed: {type(err).__name__}: {err}") if args.debug: traceback.print_exc() return MainResult(1) @@ -1547,12 +1540,11 @@ def on_signal(signum, frame): print(f"\n[time] {timer.report()}") if total_found == 0: - error_msg = ( + error( f"Error: No tests with" + f" --match-contract '{contract_regex(args)}'" + f" --match-test '{test_regex(args)}'" ) - print(color_warn(error_msg)) return MainResult(1) exitcode = 0 if total_failed == 0 else 1 diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index c1795cc0..e6d7be72 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -29,7 +29,7 @@ from .exceptions import * from .utils import * from .warnings import ( - warn, + warn_code, LIBRARY_PLACEHOLDER, ) @@ -393,7 +393,9 @@ def from_hexcode(hexcode: str): raise ValueError(hexcode) if "__" in hexcode: - warn(LIBRARY_PLACEHOLDER, f"contract hexcode contains library placeholder") + warn_code( + LIBRARY_PLACEHOLDER, f"contract hexcode contains library placeholder" + ) try: bytecode = bytes.fromhex(stripped(hexcode)) @@ -2429,8 +2431,9 @@ def finalize(ex: Exec): ) else: if self.options.debug: - print( - f"Warning: the use of symbolic BYTE indexing may potentially impact the performance of symbolic reasoning: BYTE {idx} {w}" + warn( + f"Warning: the use of symbolic BYTE indexing may potentially " + f"impact the performance of symbolic reasoning: BYTE {idx} {w}" ) ex.st.push(self.sym_byte_of(idx, w)) diff --git a/src/halmos/utils.py b/src/halmos/utils.py index f07b6397..3ead9b10 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -464,7 +464,7 @@ def color_error(text: str) -> str: def color_warn(text: str) -> str: - return red(text) + return yellow(text) def color_info(text: str) -> str: diff --git a/src/halmos/warnings.py b/src/halmos/warnings.py index bb8d684e..521d17a9 100644 --- a/src/halmos/warnings.py +++ b/src/halmos/warnings.py @@ -4,7 +4,7 @@ from .utils import color_warn -logger = logging.getLogger("Halmos") +logger = logging.getLogger("halmos") logging.basicConfig() WARNINGS_BASE_URL = "https://github.com/a16z/halmos/wiki/warnings" @@ -21,7 +21,6 @@ def url(self) -> str: PARSING_ERROR = ErrorCode("parsing-error") INTERNAL_ERROR = ErrorCode("internal-error") LIBRARY_PLACEHOLDER = ErrorCode("library-placeholder") - COUNTEREXAMPLE_INVALID = ErrorCode("counterexample-invalid") COUNTEREXAMPLE_UNKNOWN = ErrorCode("counterexample-unknown") UNSUPPORTED_OPCODE = ErrorCode("unsupported-opcode") @@ -30,5 +29,5 @@ def url(self) -> str: UNINTERPRETED_UNKNOWN_CALLS = ErrorCode("uninterpreted-unknown-calls") -def warn(error_code: ErrorCode, msg: str): +def warn_code(error_code: ErrorCode, msg: str): logger.warning(f"{color_warn(msg)}\n(see {error_code.url()})") From 2040b07677c6784f314ba97640fef8c6b9c6a25a Mon Sep 17 00:00:00 2001 From: karmacoma Date: Sat, 1 Jun 2024 11:57:40 -0700 Subject: [PATCH 4/4] utils: simplify color funcs --- src/halmos/utils.py | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 3ead9b10..6c444f6f 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -455,24 +455,11 @@ def magenta(text: str) -> str: return f"\033[35m{text}\033[0m" -def color_good(text: str) -> str: - return green(text) - - -def color_error(text: str) -> str: - return red(text) - - -def color_warn(text: str) -> str: - return yellow(text) - - -def color_info(text: str) -> str: - return cyan(text) - - -def color_debug(text: str) -> str: - return magenta(text) +color_good = green +color_debug = magenta +color_info = cyan +color_warn = yellow +color_error = red def error(text: str) -> None: