mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Fix Priority 1 ASSERT_FAIL bugs - replace assertions with proper error handling

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-18 00:42:55 +00:00
parent ac19bdb9a7
commit ae328dc006
4 changed files with 43 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

51
scripts/mk_genfile_common.py
View file

@ -58,12 +58,17 @@ def sorted_headers_by_component(l):
_logger.debug("get_key({})".format(path)) _logger.debug("get_key({})".format(path))
path_components = [] path_components = []
stripped_path = path 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`` # Keep stripping off directory components until we hit ``src``
while os.path.basename(stripped_path) != 'src': while os.path.basename(stripped_path) != 'src':
path_components.append(os.path.basename(stripped_path)) path_components.append(os.path.basename(stripped_path))
stripped_path = os.path.dirname(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() path_components.reverse()
# For consistency across platforms use ``/`` rather than ``os.sep``. # For consistency across platforms use ``/`` rather than ``os.sep``.
# This is a sorting key so it doesn't need to a platform suitable # 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 = {} decls = {}
idx = 0 idx = 0
else: else:
assert False, "Invalid %s, line: %s" % (api_file, linenum) raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
else: 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) words = re.split('[^-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line) m = closebrace_pat.match(line)
if m: if m:
@ -150,7 +157,7 @@ def mk_z3consts_py_internal(api_files, output_dir):
z3consts.write('\n') z3consts.write('\n')
mode = SEARCHING mode = SEARCHING
elif len(words) <= 2: elif len(words) <= 2:
assert False, "Invalid %s, line: %s" % (api_file, linenum) raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
else: else:
if words[2] != '': if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x': if len(words[2]) > 1 and words[2][1] == 'x':
@ -224,9 +231,11 @@ def mk_z3consts_dotnet_internal(api_files, output_dir):
decls = {} decls = {}
idx = 0 idx = 0
else: else:
assert False, "Invalid %s, line: %s" % (api_file, linenum) raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
else: 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) words = re.split('[^-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line) m = closebrace_pat.match(line)
if m: if m:
@ -241,7 +250,7 @@ def mk_z3consts_dotnet_internal(api_files, output_dir):
z3consts.write(' }\n\n') z3consts.write(' }\n\n')
mode = SEARCHING mode = SEARCHING
elif len(words) <= 2: elif len(words) <= 2:
assert False, "Invalid %s, line: %s" % (api_file, linenum) raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
else: else:
if words[2] != '': if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x': 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 = {} decls = {}
idx = 0 idx = 0
else: else:
assert False, "Invalid %s, line: %s" % (api_file, linenum) raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
else: 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) words = re.split('[^-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line) m = closebrace_pat.match(line)
if m: if m:
@ -438,9 +449,11 @@ def mk_z3consts_ml_internal(api_files, output_dir):
decls = {} decls = {}
idx = 0 idx = 0
else: else:
assert False, "Invalid %s, line: %s" % (api_file, linenum) raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
else: 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) words = re.split('[^-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line) m = closebrace_pat.match(line)
if m: if m:
@ -518,9 +531,10 @@ def mk_z3consts_ml_internal(api_files, output_dir):
# decls = {} # decls = {}
# idx = 0 # idx = 0
# else: # else:
# assert False, "Invalid %s, line: %s" % (api_file, linenum) # raise ValueError("Invalid %s, line: %s" % (api_file, linenum))
# else: # 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) # words = re.split('[^\-a-zA-Z0-9_]+', line)
# m = closebrace_pat.match(line) # m = closebrace_pat.match(line)
# if m: # if m:
@ -610,7 +624,8 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
This procedure is invoked by gparams::init() This procedure is invoked by gparams::init()
""" """
assert isinstance(h_files_full_path, list) 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 = [] cmds = []
mod_cmds = [] mod_cmds = []
mod_descrs = [] 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 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') fullname = os.path.join(path, 'install_tactic.cpp')
fout = open(fullname, 'w') fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n') 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 These procedures are invoked by the Z3 memory_manager
""" """
assert isinstance(h_files_full_path, list) 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 = [] initializer_cmds = []
finalizer_cmds = [] finalizer_cmds = []
fullname = os.path.join(path, 'mem_initializer.cpp') fullname = os.path.join(path, 'mem_initializer.cpp')

7
scripts/mk_util.py
View file

@ -3594,10 +3594,11 @@ class MakeRuleCmd(object):
def strip_path_prefix(path, prefix): def strip_path_prefix(path, prefix):
if path.startswith(prefix): if path.startswith(prefix):
stripped_path = path[len(prefix):] stripped_path = path[len(prefix):]
stripped_path.replace('//','/') stripped_path = stripped_path.replace('//','/')
if stripped_path[0] == '/': if len(stripped_path) > 0 and stripped_path[0] == '/':
stripped_path = stripped_path[1:] 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 return stripped_path
else: else:
return path return path

7
scripts/update_api.py
View file

@ -561,9 +561,7 @@ def param2java(p):
elif param_type(p) == BOOL: elif param_type(p) == BOOL:
return "BoolPtr" return "BoolPtr"
else: else:
print("ERROR: unreachable code") raise ValueError(f"ERROR: unreachable code - unexpected param_type: {param_type(p)}")
assert(False)
exit(1)
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s[]" % type2java(param_type(p)) return "%s[]" % type2java(param_type(p))
elif k == OUT_MANAGED_ARRAY: elif k == OUT_MANAGED_ARRAY:
@ -2024,7 +2022,8 @@ def generate_files(api_files,
# existing code is designed to always emit these files. # existing code is designed to always emit these files.
def mk_file_or_temp(output_dir, file_name, mode='w'): def mk_file_or_temp(output_dir, file_name, mode='w'):
if output_dir != None: 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) return open(os.path.join(output_dir, file_name), mode)
else: else:
# Return a file that we can write to without caring # Return a file that we can write to without caring

3
src/api/python/z3/z3util.py
View file

@ -78,7 +78,8 @@ def ehash(v):
""" """
if z3_debug(): 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()) return "{}_{}_{}".format(str(v), v.hash(), v.sort_kind())