From 92d684e942ba4da508b04e7a2ec64cbe3df6769e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 18 Feb 2026 00:42:55 +0000 Subject: [PATCH] Fix Priority 1 ASSERT_FAIL bugs - replace assertions with proper error handling Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- scripts/mk_genfile_common.py | 51 ++++++++++++++++++++++++------------ scripts/mk_util.py | 7 ++--- scripts/update_api.py | 7 +++-- src/api/python/z3/z3util.py | 3 ++- 4 files changed, 43 insertions(+), 25 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 3be314a53..364580550 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -58,12 +58,17 @@ def sorted_headers_by_component(l): _logger.debug("get_key({})".format(path)) path_components = [] stripped_path = path - assert 'src' in stripped_path.split(os.path.sep) or 'src' in stripped_path.split('/') + if not ('src' in stripped_path.split(os.path.sep) or 'src' in stripped_path.split('/')): + raise ValueError(f"Path '{path}' does not contain 'src' directory component") # Keep stripping off directory components until we hit ``src`` while os.path.basename(stripped_path) != 'src': path_components.append(os.path.basename(stripped_path)) stripped_path = os.path.dirname(stripped_path) - assert len(path_components) > 0 + # Prevent infinite loop if 'src' is never found + if not stripped_path or stripped_path == os.path.dirname(stripped_path): + raise ValueError(f"Could not find 'src' directory in path '{path}'") + if len(path_components) == 0: + raise ValueError(f"Path '{path}' has no components after 'src' directory") path_components.reverse() # For consistency across platforms use ``/`` rather than ``os.sep``. # This is a sorting key so it doesn't need to a platform suitable @@ -136,9 +141,11 @@ def mk_z3consts_py_internal(api_files, output_dir): decls = {} idx = 0 else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) + raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) else: - assert mode == IN_ENUM + if mode != IN_ENUM: + + raise ValueError(f"Expected IN_ENUM mode, got mode {mode} in {api_file}, line: {linenum}") words = re.split('[^-a-zA-Z0-9_]+', line) m = closebrace_pat.match(line) if m: @@ -150,7 +157,7 @@ def mk_z3consts_py_internal(api_files, output_dir): z3consts.write('\n') mode = SEARCHING elif len(words) <= 2: - assert False, "Invalid %s, line: %s" % (api_file, linenum) + raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': @@ -224,9 +231,11 @@ def mk_z3consts_dotnet_internal(api_files, output_dir): decls = {} idx = 0 else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) + raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) else: - assert mode == IN_ENUM + if mode != IN_ENUM: + + raise ValueError(f"Expected IN_ENUM mode, got mode {mode} in {api_file}, line: {linenum}") words = re.split('[^-a-zA-Z0-9_]+', line) m = closebrace_pat.match(line) if m: @@ -241,7 +250,7 @@ def mk_z3consts_dotnet_internal(api_files, output_dir): z3consts.write(' }\n\n') mode = SEARCHING elif len(words) <= 2: - assert False, "Invalid %s, line: %s" % (api_file, linenum) + raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) else: if words[2] != '': if len(words[2]) > 1 and words[2][1] == 'x': @@ -312,9 +321,11 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir): decls = {} idx = 0 else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) + raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) else: - assert mode == IN_ENUM + if mode != IN_ENUM: + + raise ValueError(f"Expected IN_ENUM mode, got mode {mode} in {api_file}, line: {linenum}") words = re.split('[^-a-zA-Z0-9_]+', line) m = closebrace_pat.match(line) if m: @@ -438,9 +449,11 @@ def mk_z3consts_ml_internal(api_files, output_dir): decls = {} idx = 0 else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) + raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) else: - assert mode == IN_ENUM + if mode != IN_ENUM: + + raise ValueError(f"Expected IN_ENUM mode, got mode {mode} in {api_file}, line: {linenum}") words = re.split('[^-a-zA-Z0-9_]+', line) m = closebrace_pat.match(line) if m: @@ -518,9 +531,10 @@ def mk_z3consts_ml_internal(api_files, output_dir): # decls = {} # idx = 0 # else: - # assert False, "Invalid %s, line: %s" % (api_file, linenum) + # raise ValueError("Invalid %s, line: %s" % (api_file, linenum)) # else: - # assert mode == IN_ENUM + # if mode != IN_ENUM: + raise ValueError(f"Expected IN_ENUM mode, got mode {mode} in {api_file}, line: {linenum}") # words = re.split('[^\-a-zA-Z0-9_]+', line) # m = closebrace_pat.match(line) # if m: @@ -610,7 +624,8 @@ def mk_gparams_register_modules_internal(h_files_full_path, path): This procedure is invoked by gparams::init() """ assert isinstance(h_files_full_path, list) - assert check_dir_exists(path) + if not check_dir_exists(path): + raise ValueError(f"Output directory '{path}' does not exist") cmds = [] mod_cmds = [] mod_descrs = [] @@ -690,7 +705,8 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path): } assert isinstance(h_files_full_path, list) - assert check_dir_exists(path) + if not check_dir_exists(path): + raise ValueError(f"Output directory '{path}' does not exist") fullname = os.path.join(path, 'install_tactic.cpp') fout = open(fullname, 'w') fout.write('// Automatically generated file.\n') @@ -774,7 +790,8 @@ def mk_mem_initializer_cpp_internal(h_files_full_path, path): These procedures are invoked by the Z3 memory_manager """ assert isinstance(h_files_full_path, list) - assert check_dir_exists(path) + if not check_dir_exists(path): + raise ValueError(f"Output directory '{path}' does not exist") initializer_cmds = [] finalizer_cmds = [] fullname = os.path.join(path, 'mem_initializer.cpp') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index aa1069a5e..1af384242 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3594,10 +3594,11 @@ class MakeRuleCmd(object): def strip_path_prefix(path, prefix): if path.startswith(prefix): stripped_path = path[len(prefix):] - stripped_path.replace('//','/') - if stripped_path[0] == '/': + stripped_path = stripped_path.replace('//','/') + if len(stripped_path) > 0 and stripped_path[0] == '/': stripped_path = stripped_path[1:] - assert not os.path.isabs(stripped_path) + if os.path.isabs(stripped_path): + raise ValueError(f"Path '{path}' after stripping prefix '{prefix}' is still absolute: '{stripped_path}'") return stripped_path else: return path diff --git a/scripts/update_api.py b/scripts/update_api.py index b74203e3f..92cb7738c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -561,9 +561,7 @@ def param2java(p): elif param_type(p) == BOOL: return "BoolPtr" else: - print("ERROR: unreachable code") - assert(False) - exit(1) + raise ValueError(f"ERROR: unreachable code - unexpected param_type: {param_type(p)}") elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s[]" % type2java(param_type(p)) elif k == OUT_MANAGED_ARRAY: @@ -2024,7 +2022,8 @@ def generate_files(api_files, # existing code is designed to always emit these files. def mk_file_or_temp(output_dir, file_name, mode='w'): if output_dir != None: - assert os.path.exists(output_dir) and os.path.isdir(output_dir) + if not (os.path.exists(output_dir) and os.path.isdir(output_dir)): + raise ValueError(f"Output directory '{output_dir}' does not exist or is not a directory") return open(os.path.join(output_dir, file_name), mode) else: # Return a file that we can write to without caring diff --git a/src/api/python/z3/z3util.py b/src/api/python/z3/z3util.py index b60038f2f..993abef58 100644 --- a/src/api/python/z3/z3util.py +++ b/src/api/python/z3/z3util.py @@ -78,7 +78,8 @@ def ehash(v): """ if z3_debug(): - assert is_expr(v) + if not is_expr(v): + raise ValueError(f"ehash expects a Z3 expression, got {type(v)}") return "{}_{}_{}".format(str(v), v.hash(), v.sort_kind())