From f9efd9467d3a0e0f8e8a6c3b8c57cc03eaa53b3a Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 20 Dec 2024 17:53:09 -0800 Subject: [PATCH] actually parse external solver output using smtlib --- src/halmos/__main__.py | 92 ++++++++++++------------------------------ src/halmos/smtlib.py | 44 +++++++++++--------- 2 files changed, 51 insertions(+), 85 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 7a7b1133..bbafcad5 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -22,7 +22,6 @@ from z3 import ( BitVec, CheckSatResult, - ModelRef, Solver, sat, set_option, @@ -75,6 +74,7 @@ jumpid_str, mnemonic, ) +from .smtlib import ModelVariables, parse_string from .traces import render_trace, rendered_trace from .utils import ( NamedTimer, @@ -91,9 +91,6 @@ yellow, ) -StrModel = dict[str, str] -AnyModel = StrModel | str - # Python version >=3.8.14, >=3.9.14, >=3.10.7, or >=3.11 if hasattr(sys, "set_int_max_str_digits"): sys.set_int_max_str_digits(0) @@ -113,26 +110,27 @@ @dataclass class PotentialModel: - model: AnyModel - is_valid: bool - - def __init__(self, model: ModelRef | str, args: HalmosConfig) -> None: - # convert model into string to avoid pickling errors for z3 (ctypes) objects containing pointers - self.model = ( - to_str_model(model, args.print_full_model) - if isinstance(model, ModelRef) - else model - ) - self.is_valid = is_model_valid(model) + model: ModelVariables | str | None def __str__(self) -> str: # expected to be a filename if isinstance(self.model, str): return f"see {self.model}" - formatted = [f"\n {decl} = {val}" for decl, val in self.model.items()] + formatted = [] + for v in self.model.values(): + stringified = stringify(v.full_name, v.value) + formatted.append(f"\n {v.full_name} = {stringified}") return "".join(sorted(formatted)) if formatted else "∅" + @property + def is_valid(self) -> bool: + if self.model is None: + return False + + needs_refinement = any(name.startswith("f_evm_") for name in self.model) + return not needs_refinement + @dataclass(frozen=True) class ContractContext: @@ -527,6 +525,7 @@ def setup(ctx: FunctionContext) -> Exec: setup_exs.append(setup_exs_no_error[0][0]) case _: for setup_ex, query in setup_exs_no_error: + # XXX fix with new interface res, _, _ = solve(query, args) if res != unsat: setup_exs.append(setup_ex) @@ -689,7 +688,13 @@ def run_test(ctx: FunctionContext) -> TestResult: print(" Already proven unsat") continue - solve(path_ctx) + try: + solve(path_ctx) + except RuntimeError: + # XXX use more specific exception + # XXX notify sevm that we're done + # if the thread pool is shut down, here + break # XXX handle refinement # XXX handle timeout @@ -731,6 +736,8 @@ def run_test(ctx: FunctionContext) -> TestResult: # display assertion solving progress # + # XXX clashes with the exploration progress status + if not args.no_status or args.early_exit: with Status("") as status: while True: @@ -986,7 +993,7 @@ def solver_callback(future: PopenFuture): unsat_core = parse_unsat_core(stdout) if args.cache_solver else None solver_output = SolverOutput(unsat, path_id, unsat_core=unsat_core) case "sat": - model = PotentialModel(f"{smt2_filename}.out", args) + model = PotentialModel(parse_string(stdout)) solver_output = SolverOutput(sat, path_id, model=model) case _: solver_output = SolverOutput(unknown, path_id) @@ -1048,55 +1055,6 @@ def refine(query: SMTQuery) -> SMTQuery: return SMTQuery(smtlib, query.assertions) -# def package_result( -# model: PotentialModel | None, -# idx: int, -# result: CheckSatResult, -# unsat_core: list | None, -# args: HalmosConfig, -# ) -> ModelWithContext: -# if result == unsat: -# if args.verbose >= 1: -# print(f" Invalid path; ignored (path id: {idx+1})") -# return ModelWithContext(None, idx, result, unsat_core) - -# if result == sat: -# if args.verbose >= 1: -# print(f" Valid path; counterexample generated (path id: {idx+1})") -# return ModelWithContext(model, idx, result, None) - -# else: -# if args.verbose >= 1: -# print(f" Timeout (path id: {idx+1})") -# return ModelWithContext(None, idx, result, None) - - -def is_model_valid(model: ModelRef | str) -> bool: - # TODO: evaluate the path condition against the given model after excluding f_evm_* symbols, - # since the f_evm_* symbols may still appear in valid models. - - # model is a filename, containing solver output - if isinstance(model, str): - with open(model) as f: - for line in f: - if "f_evm_" in line: - return False - return True - - # z3 model object - else: - return all(not str(decl).startswith("f_evm_") for decl in model) - - -def to_str_model(model: ModelRef, print_full_model: bool) -> StrModel: - def select(var): - name = str(var) - return name.startswith("p_") or name.startswith("halmos_") - - select_model = filter(select, model) if not print_full_model else model - return {str(decl): stringify(str(decl), model[decl]) for decl in select_model} - - def get_contract_type( ast_nodes: list, contract_name: str ) -> tuple[str | None, str | None]: diff --git a/src/halmos/smtlib.py b/src/halmos/smtlib.py index f20b2ca8..61eb23fe 100644 --- a/src/halmos/smtlib.py +++ b/src/halmos/smtlib.py @@ -3,6 +3,19 @@ from halmos.logs import logger + +@dataclass +class ModelVariable: + full_name: str + variable_name: str + solidity_type: str + smt_type: str + size_bits: int + value: int + + +ModelVariables = dict[str, ModelVariable] + # Regular expression for capturing halmos variables halmos_pattern = re.compile( r""" @@ -20,21 +33,6 @@ ) -@dataclass -class ModelVariable: - full_name: str - variable_name: str - solidity_type: str - smt_type: str - size_bits: int - value: int - - -def parse_file(file_path: str) -> dict: - with open(file_path) as file: - return parse_string(file.read()) - - def parse_const_value(value: str) -> int: if value.startswith("#b"): return int(value[2:], 2) @@ -51,7 +49,7 @@ def parse_const_value(value: str) -> int: raise ValueError(f"unknown value format: {value}") -def parse_match(match: re.Match) -> ModelVariable: +def _parse_match(match: re.Match) -> ModelVariable: full_name = match.group(1).strip() smt_type = f"{match.group(2)} {match.group(3)}" size_bits = int(match.group(3)) @@ -72,7 +70,12 @@ def parse_match(match: re.Match) -> ModelVariable: ) -def parse_string(smtlib_str: str) -> dict[str, ModelVariable]: +def parse_string(smtlib_str: str) -> ModelVariables: + """Expects a whole smtlib model output file, as produced by a solver + in response to a `(check-sat)` + `(get-model)` command. + + Extracts halmos variables and returns them grouped by their full name""" + model_variables: dict[str, ModelVariable] = {} # use a regex to find all the variables @@ -83,10 +86,15 @@ def parse_string(smtlib_str: str) -> dict[str, ModelVariable]: for match in halmos_pattern.finditer(smtlib_str): try: - variable = parse_match(match) + variable = _parse_match(match) model_variables[variable.full_name] = variable except Exception as e: logger.error(f"error parsing smtlib string '{match.string.strip()}': {e}") raise e return model_variables + + +def parse_file(file_path: str) -> ModelVariables: + with open(file_path) as file: + return parse_string(file.read())