mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
Move `mk_z3consts_py_internal()
out of
mk_util.py
` into
``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_consts_files.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_z3consts_py_internal()`` now returns the path to the generated file. The motivation behind this is so that clients of the function know the path to the generated file. Whilst I'm here also reindent ``mk_consts_files.py`` and move some of its code into ``mk_genfile_common.py`` so it can be shared. Also update Z3_GENERATED_FILE_EXTRA_DEPENDENCIES in the CMake build so it knows about ``mk_genfile_common.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system.
This commit is contained in:
parent
a2e3788a20
commit
2b64729b21
|
@ -343,6 +343,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
|
|||
# FIXME: We should drop the dependency on ``mk_util.py``
|
||||
set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py"
|
||||
)
|
||||
|
||||
################################################################################
|
||||
|
|
|
@ -4,44 +4,38 @@ Reads a list of Z3 API header files and
|
|||
generate the constant declarations need
|
||||
by one or more Z3 language bindings
|
||||
"""
|
||||
import mk_util
|
||||
import mk_genfile_common
|
||||
import argparse
|
||||
import logging
|
||||
import os
|
||||
import sys
|
||||
|
||||
def check_dir(output_dir):
|
||||
if not os.path.isdir(output_dir):
|
||||
logging.error('"{}" is not an existing directory'.format(output_dir))
|
||||
return 1
|
||||
return 0
|
||||
|
||||
def main(args):
|
||||
logging.basicConfig(level=logging.INFO)
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument("api_files", nargs="+")
|
||||
parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
|
||||
pargs = parser.parse_args(args)
|
||||
logging.basicConfig(level=logging.INFO)
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument("api_files", nargs="+")
|
||||
parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
|
||||
pargs = parser.parse_args(args)
|
||||
|
||||
for api_file in pargs.api_files:
|
||||
if not os.path.exists(api_file):
|
||||
logging.error('"{}" does not exist'.format(api_file))
|
||||
return 1
|
||||
if not mk_genfile_common.check_files_exist(pargs.api_files):
|
||||
logging.error('One or more API files do not exist')
|
||||
return 1
|
||||
|
||||
count = 0
|
||||
count = 0
|
||||
|
||||
if pargs.z3py_output_dir:
|
||||
if check_dir(pargs.z3py_output_dir) != 0:
|
||||
return 1
|
||||
mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir)
|
||||
count += 1
|
||||
if pargs.z3py_output_dir:
|
||||
if not mk_genfile_common.check_dir_exists(pargs.z3py_output_dir):
|
||||
return 1
|
||||
output = mk_genfile_common.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir)
|
||||
logging.info('Generated "{}"'.format(output))
|
||||
count += 1
|
||||
|
||||
if count == 0:
|
||||
logging.info('No files generated. You need to specific an output directory'
|
||||
' for the relevant langauge bindings')
|
||||
# TODO: Add support for other bindings
|
||||
return 0
|
||||
if count == 0:
|
||||
logging.info('No files generated. You need to specific an output directory'
|
||||
' for the relevant langauge bindings')
|
||||
# TODO: Add support for other bindings
|
||||
return 0
|
||||
|
||||
if __name__ == '__main__':
|
||||
sys.exit(main(sys.argv[1:]))
|
||||
|
||||
sys.exit(main(sys.argv[1:]))
|
||||
|
|
126
scripts/mk_genfile_common.py
Normal file
126
scripts/mk_genfile_common.py
Normal file
|
@ -0,0 +1,126 @@
|
|||
# This file contains code that is common to
|
||||
# both the Python build system and the CMake
|
||||
# build system.
|
||||
#
|
||||
# The code here generally is involved in
|
||||
# generating files needed by Z3 at build time.
|
||||
#
|
||||
# You should **not** import ``mk_util`` here
|
||||
# to avoid having this code depend on the
|
||||
# of the Python build system.
|
||||
import os
|
||||
import logging
|
||||
import re
|
||||
import sys
|
||||
|
||||
# Logger for this module
|
||||
_logger = logging.getLogger(__name__)
|
||||
|
||||
|
||||
###############################################################################
|
||||
# Utility functions
|
||||
###############################################################################
|
||||
def check_dir_exists(output_dir):
|
||||
"""
|
||||
Returns ``True`` if ``output_dir`` exists, otherwise
|
||||
returns ``False``.
|
||||
"""
|
||||
if not os.path.isdir(output_dir):
|
||||
_logger.error('"{}" is not an existing directory'.format(output_dir))
|
||||
return False
|
||||
return True
|
||||
|
||||
def check_files_exist(files):
|
||||
assert isinstance(files, list)
|
||||
for f in files:
|
||||
if not os.path.exists(f):
|
||||
_logger.error('"{}" does not exist'.format(f))
|
||||
return False
|
||||
return True
|
||||
|
||||
###############################################################################
|
||||
# Functions for generating constant declarations for language bindings
|
||||
###############################################################################
|
||||
|
||||
def mk_z3consts_py_internal(api_files, output_dir):
|
||||
"""
|
||||
Generate ``z3consts.py`` from the list of API header files
|
||||
in ``api_files`` and write the output file into
|
||||
the ``output_dir`` directory
|
||||
|
||||
Returns the path to the generated file.
|
||||
"""
|
||||
assert os.path.isdir(output_dir)
|
||||
assert isinstance(api_files, list)
|
||||
|
||||
blank_pat = re.compile("^ *\r?$")
|
||||
comment_pat = re.compile("^ *//.*$")
|
||||
typedef_pat = re.compile("typedef enum *")
|
||||
typedef2_pat = re.compile("typedef enum { *")
|
||||
openbrace_pat = re.compile("{ *")
|
||||
closebrace_pat = re.compile("}.*;")
|
||||
|
||||
z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w')
|
||||
z3consts_output_path = z3consts.name
|
||||
z3consts.write('# Automatically generated file\n\n')
|
||||
for api_file in api_files:
|
||||
api = open(api_file, 'r')
|
||||
|
||||
SEARCHING = 0
|
||||
FOUND_ENUM = 1
|
||||
IN_ENUM = 2
|
||||
|
||||
mode = SEARCHING
|
||||
decls = {}
|
||||
idx = 0
|
||||
|
||||
linenum = 1
|
||||
for line in api:
|
||||
m1 = blank_pat.match(line)
|
||||
m2 = comment_pat.match(line)
|
||||
if m1 or m2:
|
||||
# skip blank lines and comments
|
||||
linenum = linenum + 1
|
||||
elif mode == SEARCHING:
|
||||
m = typedef_pat.match(line)
|
||||
if m:
|
||||
mode = FOUND_ENUM
|
||||
m = typedef2_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
elif mode == FOUND_ENUM:
|
||||
m = openbrace_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
else:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
z3consts.write('# enum %s\n' % name)
|
||||
for k in decls:
|
||||
i = decls[k]
|
||||
z3consts.write('%s = %s\n' % (k, i))
|
||||
z3consts.write('\n')
|
||||
mode = SEARCHING
|
||||
elif len(words) <= 2:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
if words[2] != '':
|
||||
if len(words[2]) > 1 and words[2][1] == 'x':
|
||||
idx = int(words[2], 16)
|
||||
else:
|
||||
idx = int(words[2])
|
||||
decls[words[1]] = idx
|
||||
idx = idx + 1
|
||||
linenum = linenum + 1
|
||||
api.close()
|
||||
z3consts.close()
|
||||
return z3consts_output_path
|
|
@ -12,6 +12,7 @@ import re
|
|||
import getopt
|
||||
import shutil
|
||||
from mk_exception import *
|
||||
import mk_genfile_common
|
||||
from fnmatch import fnmatch
|
||||
import distutils.sysconfig
|
||||
import compileall
|
||||
|
@ -3026,83 +3027,9 @@ def mk_z3consts_py(api_files):
|
|||
api_file_c = api_dll.find_file(api_file, api_dll.name)
|
||||
api_file = os.path.join(api_file_c.src_dir, api_file)
|
||||
full_path_api_files.append(api_file)
|
||||
mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)
|
||||
|
||||
def mk_z3consts_py_internal(api_files, output_dir):
|
||||
assert os.path.isdir(output_dir)
|
||||
assert isinstance(api_files, list)
|
||||
|
||||
blank_pat = re.compile("^ *\r?$")
|
||||
comment_pat = re.compile("^ *//.*$")
|
||||
typedef_pat = re.compile("typedef enum *")
|
||||
typedef2_pat = re.compile("typedef enum { *")
|
||||
openbrace_pat = re.compile("{ *")
|
||||
closebrace_pat = re.compile("}.*;")
|
||||
|
||||
z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w')
|
||||
z3consts.write('# Automatically generated file\n\n')
|
||||
for api_file in api_files:
|
||||
api = open(api_file, 'r')
|
||||
|
||||
SEARCHING = 0
|
||||
FOUND_ENUM = 1
|
||||
IN_ENUM = 2
|
||||
|
||||
mode = SEARCHING
|
||||
decls = {}
|
||||
idx = 0
|
||||
|
||||
linenum = 1
|
||||
for line in api:
|
||||
m1 = blank_pat.match(line)
|
||||
m2 = comment_pat.match(line)
|
||||
if m1 or m2:
|
||||
# skip blank lines and comments
|
||||
linenum = linenum + 1
|
||||
elif mode == SEARCHING:
|
||||
m = typedef_pat.match(line)
|
||||
if m:
|
||||
mode = FOUND_ENUM
|
||||
m = typedef2_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
elif mode == FOUND_ENUM:
|
||||
m = openbrace_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
else:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
z3consts.write('# enum %s\n' % name)
|
||||
for k in decls:
|
||||
i = decls[k]
|
||||
z3consts.write('%s = %s\n' % (k, i))
|
||||
z3consts.write('\n')
|
||||
mode = SEARCHING
|
||||
elif len(words) <= 2:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
if words[2] != '':
|
||||
if len(words[2]) > 1 and words[2][1] == 'x':
|
||||
idx = int(words[2], 16)
|
||||
else:
|
||||
idx = int(words[2])
|
||||
decls[words[1]] = idx
|
||||
idx = idx + 1
|
||||
linenum = linenum + 1
|
||||
api.close()
|
||||
z3consts.close()
|
||||
generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)
|
||||
if VERBOSE:
|
||||
print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py'))
|
||||
print("Generated '{}".format(generated_file))
|
||||
|
||||
|
||||
# Extract enumeration types from z3_api.h, and add .Net definitions
|
||||
|
|
Loading…
Reference in a new issue