mirror of
https://github.com/Z3Prover/z3
synced 2026-02-22 08:17:37 +00:00
Fix Priority 1 ASSERT_FAIL bugs - replace assertions with proper error handling
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
Nikolaj Bjorner
parent
b5b79343e4
commit
92d684e942
4 changed files with 43 additions and 25 deletions
|
|
@ -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')
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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())
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue