mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
963 lines
38 KiB
Python
963 lines
38 KiB
Python
# 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 io
|
|
import os
|
|
import pprint
|
|
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
|
|
|
|
def sorted_headers_by_component(l):
|
|
"""
|
|
Take a list of header files and sort them by the
|
|
path after ``src/``. E.g. for ``src/ast/fpa/fpa2bv_converter.h`` the sorting
|
|
key is ``ast/fpa/fpa2bv_converter.h``.
|
|
|
|
The sort is done this way because for the CMake build
|
|
there are two directories for every component (e.g.
|
|
``<src_dir>/src/ast/fpa`` and ``<build_dir>/src/ast/fpa``).
|
|
We don't want to sort based on different ``<src_dir>``
|
|
and ``<build_dir>`` prefixes so that we can match the Python build
|
|
system's behaviour.
|
|
"""
|
|
assert isinstance(l, list)
|
|
def get_key(path):
|
|
_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('/')
|
|
# 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
|
|
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
|
|
# path
|
|
r = '/'.join(path_components)
|
|
_logger.debug("return key:'{}'".format(r))
|
|
return r
|
|
sorted_headers = sorted(l, key=get_key)
|
|
_logger.debug('sorted headers:{}'.format(pprint.pformat(sorted_headers)))
|
|
return sorted_headers
|
|
|
|
|
|
|
|
###############################################################################
|
|
# 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, 'z3', '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)
|
|
# Iterate over key-value pairs ordered by value
|
|
for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
|
|
z3consts.write('%s = %s\n' % (k, v))
|
|
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
|
|
|
|
def mk_z3consts_dotnet_internal(api_files, output_dir):
|
|
"""
|
|
Generate ``Enumerations.cs`` 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("}.*;")
|
|
|
|
DeprecatedEnums = [ 'Z3_search_failure' ]
|
|
z3consts = open(os.path.join(output_dir, 'Enumerations.cs'), 'w')
|
|
z3consts_output_path = z3consts.name
|
|
z3consts.write('// Automatically generated file\n\n')
|
|
z3consts.write('using System;\n\n'
|
|
'#pragma warning disable 1591\n\n'
|
|
'namespace Microsoft.Z3\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]
|
|
if name not in DeprecatedEnums:
|
|
z3consts.write(' /// <summary>%s</summary>\n' % name)
|
|
z3consts.write(' public enum %s {\n' % name)
|
|
z3consts.write
|
|
# Iterate over key-value pairs ordered by value
|
|
for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
|
|
z3consts.write(' %s = %s,\n' % (k, v))
|
|
z3consts.write(' }\n\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.write('}\n');
|
|
z3consts.close()
|
|
return z3consts_output_path
|
|
|
|
|
|
def mk_z3consts_java_internal(api_files, package_name, output_dir):
|
|
"""
|
|
Generate "com.microsoft.z3.enumerations" package from the list of API
|
|
header files in ``api_files`` and write the package directory into
|
|
the ``output_dir`` directory
|
|
|
|
Returns a list of the generated java source files.
|
|
"""
|
|
blank_pat = re.compile("^ *$")
|
|
comment_pat = re.compile("^ *//.*$")
|
|
typedef_pat = re.compile("typedef enum *")
|
|
typedef2_pat = re.compile("typedef enum { *")
|
|
openbrace_pat = re.compile("{ *")
|
|
closebrace_pat = re.compile("}.*;")
|
|
|
|
DeprecatedEnums = [ 'Z3_search_failure' ]
|
|
gendir = os.path.join(output_dir, "enumerations")
|
|
if not os.path.exists(gendir):
|
|
os.mkdir(gendir)
|
|
|
|
generated_enumeration_files = []
|
|
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]
|
|
if name not in DeprecatedEnums:
|
|
efile = open('%s.java' % os.path.join(gendir, name), 'w')
|
|
generated_enumeration_files.append(efile.name)
|
|
efile.write('/**\n * Automatically generated file\n **/\n\n')
|
|
efile.write('package %s.enumerations;\n\n' % package_name)
|
|
efile.write('import java.util.HashMap;\n')
|
|
efile.write('import java.util.Map;\n')
|
|
efile.write('\n')
|
|
|
|
efile.write('/**\n')
|
|
efile.write(' * %s\n' % name)
|
|
efile.write(' **/\n')
|
|
efile.write('public enum %s {\n' % name)
|
|
efile.write
|
|
first = True
|
|
# Iterate over key-value pairs ordered by value
|
|
for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
|
|
if first:
|
|
first = False
|
|
else:
|
|
efile.write(',\n')
|
|
efile.write(' %s (%s)' % (k, v))
|
|
efile.write(";\n")
|
|
efile.write('\n private final int intValue;\n\n')
|
|
efile.write(' %s(int v) {\n' % name)
|
|
efile.write(' this.intValue = v;\n')
|
|
efile.write(' }\n\n')
|
|
efile.write(' // Cannot initialize map in constructor, so need to do it lazily.\n')
|
|
efile.write(' // Easiest thread-safe way is the initialization-on-demand holder pattern.\n')
|
|
efile.write(' private static class %s_MappingHolder {\n' % name)
|
|
efile.write(' private static final Map<Integer, %s> intMapping = new HashMap<>();\n' % name)
|
|
efile.write(' static {\n')
|
|
efile.write(' for (%s k : %s.values())\n' % (name, name))
|
|
efile.write(' intMapping.put(k.toInt(), k);\n')
|
|
efile.write(' }\n')
|
|
efile.write(' }\n\n')
|
|
efile.write(' public static final %s fromInt(int v) {\n' % name)
|
|
efile.write(' %s k = %s_MappingHolder.intMapping.get(v);\n' % (name, name))
|
|
efile.write(' if (k != null) return k;\n')
|
|
efile.write(' throw new IllegalArgumentException("Illegal value " + v + " for %s");\n' % name)
|
|
efile.write(' }\n\n')
|
|
efile.write(' public final int toInt() { return this.intValue; }\n')
|
|
# efile.write(';\n %s(int v) {}\n' % name)
|
|
efile.write('}\n\n')
|
|
efile.close()
|
|
mode = SEARCHING
|
|
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()
|
|
return generated_enumeration_files
|
|
|
|
# Extract enumeration types from z3_api.h, and add ML definitions
|
|
def mk_z3consts_ml_internal(api_files, output_dir):
|
|
"""
|
|
Generate ``z3enums.ml`` 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("^ *$")
|
|
comment_pat = re.compile("^ *//.*$")
|
|
typedef_pat = re.compile("typedef enum *")
|
|
typedef2_pat = re.compile("typedef enum { *")
|
|
openbrace_pat = re.compile("{ *")
|
|
closebrace_pat = re.compile("}.*;")
|
|
|
|
|
|
DeprecatedEnums = [ 'Z3_search_failure' ]
|
|
if not os.path.exists(output_dir):
|
|
os.mkdir(output_dir)
|
|
|
|
efile = open('%s.ml' % os.path.join(output_dir, "z3enums"), 'w')
|
|
z3consts_output_path = efile.name
|
|
efile.write('(* Automatically generated file *)\n\n')
|
|
efile.write('(** The enumeration types of Z3. *)\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]
|
|
if name not in DeprecatedEnums:
|
|
sorted_decls = sorted(decls.items(), key=lambda pair: pair[1])
|
|
efile.write('(** %s *)\n' % name[3:])
|
|
efile.write('type %s =\n' % name[3:]) # strip Z3_
|
|
for k, i in sorted_decls:
|
|
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
|
efile.write('\n')
|
|
efile.write('(** Convert %s to int*)\n' % name[3:])
|
|
efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_
|
|
efile.write(' match x with\n')
|
|
for k, i in sorted_decls:
|
|
efile.write(' | %s -> %d\n' % (k[3:], i))
|
|
efile.write('\n')
|
|
efile.write('(** Convert int to %s*)\n' % name[3:])
|
|
efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_
|
|
efile.write(' match x with\n')
|
|
for k, i in sorted_decls:
|
|
efile.write(' | %d -> %s\n' % (i, k[3:]))
|
|
# use Z3.Exception?
|
|
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
|
|
mode = SEARCHING
|
|
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()
|
|
efile.close()
|
|
return z3consts_output_path
|
|
# efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
|
|
# efile.write('(* Automatically generated file *)\n\n')
|
|
# efile.write('(** The enumeration types of Z3. *)\n\n')
|
|
# for api_file in api_files:
|
|
# api_file_c = ml.find_file(api_file, ml.name)
|
|
# api_file = os.path.join(api_file_c.src_dir, api_file)
|
|
|
|
# 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]
|
|
# if name not in DeprecatedEnums:
|
|
# efile.write('(** %s *)\n' % name[3:])
|
|
# efile.write('type %s =\n' % name[3:]) # strip Z3_
|
|
# for k, i in sorted(decls.items(), key=lambda pair: pair[1]):
|
|
# efile.write(' | %s \n' % k[3:]) # strip Z3_
|
|
# efile.write('\n')
|
|
# efile.write('(** Convert %s to int*)\n' % name[3:])
|
|
# efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
|
|
# efile.write('(** Convert int to %s*)\n' % name[3:])
|
|
# efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
|
|
# efile.write('\n')
|
|
# mode = SEARCHING
|
|
# 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()
|
|
# efile.close()
|
|
# if VERBOSE:
|
|
# print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
|
|
|
|
|
|
###############################################################################
|
|
# Functions for generating a "module definition file" for MSVC
|
|
###############################################################################
|
|
|
|
def mk_def_file_internal(defname, dll_name, export_header_files):
|
|
"""
|
|
Writes to a module definition file to a file named ``defname``.
|
|
|
|
``dll_name`` is the name of the dll (without the ``.dll`` suffix).
|
|
``export_header_file`` is a list of header files to scan for symbols
|
|
to include in the module definition file.
|
|
"""
|
|
assert isinstance(export_header_files, list)
|
|
pat1 = re.compile(".*Z3_API.*")
|
|
fout = open(defname, 'w')
|
|
fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name)
|
|
num = 1
|
|
for export_header_file in export_header_files:
|
|
api = open(export_header_file, 'r')
|
|
for line in api:
|
|
m = pat1.match(line)
|
|
if m:
|
|
words = re.split(r'\W+', line)
|
|
i = 0
|
|
for w in words:
|
|
if w == 'Z3_API':
|
|
f = words[i+1]
|
|
fout.write('\t%s @%s\n' % (f, num))
|
|
i = i + 1
|
|
num = num + 1
|
|
api.close()
|
|
fout.close()
|
|
|
|
###############################################################################
|
|
# Functions for generating ``gparams_register_modules.cpp``
|
|
###############################################################################
|
|
|
|
def path_after_src(h_file):
|
|
h_file = h_file.replace("\\","/")
|
|
idx = h_file.rfind("src/")
|
|
if idx == -1:
|
|
return h_file
|
|
return h_file[idx + 4:]
|
|
|
|
def mk_gparams_register_modules_internal(h_files_full_path, path):
|
|
"""
|
|
Generate a ``gparams_register_modules.cpp`` file in the directory ``path``.
|
|
Returns the path to the generated file.
|
|
|
|
This file implements the procedure
|
|
|
|
```
|
|
void gparams_register_modules()
|
|
```
|
|
|
|
This procedure is invoked by gparams::init()
|
|
"""
|
|
assert isinstance(h_files_full_path, list)
|
|
assert check_dir_exists(path)
|
|
cmds = []
|
|
mod_cmds = []
|
|
mod_descrs = []
|
|
fullname = os.path.join(path, 'gparams_register_modules.cpp')
|
|
fout = open(fullname, 'w')
|
|
fout.write('// Automatically generated file.\n')
|
|
fout.write('#include "util/gparams.h"\n')
|
|
reg_pat = re.compile(r'[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
|
|
reg_mod_pat = re.compile(r'[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
|
|
reg_mod_descr_pat = re.compile(r'[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
|
|
for h_file in sorted_headers_by_component(h_files_full_path):
|
|
added_include = False
|
|
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
|
for line in fin:
|
|
m = reg_pat.match(line)
|
|
if m:
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
cmds.append((m.group(1)))
|
|
m = reg_mod_pat.match(line)
|
|
if m:
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
mod_cmds.append((m.group(1), m.group(2)))
|
|
m = reg_mod_descr_pat.match(line)
|
|
if m:
|
|
mod_descrs.append((m.group(1), m.group(2)))
|
|
fout.write('void gparams_register_modules() {\n')
|
|
for code in cmds:
|
|
fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code)
|
|
for (mod, code) in mod_cmds:
|
|
fout.write('{ auto f = []() { auto* d = alloc(param_descrs); %s(*d); return d; }; gparams::register_module("%s", f); }\n' % (code, mod))
|
|
for (mod, descr) in mod_descrs:
|
|
fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr))
|
|
fout.write('}\n')
|
|
fout.close()
|
|
return fullname
|
|
|
|
###############################################################################
|
|
# Functions/data structures for generating ``install_tactics.cpp``
|
|
###############################################################################
|
|
|
|
def mk_install_tactic_cpp_internal(h_files_full_path, path):
|
|
"""
|
|
Generate a ``install_tactics.cpp`` file in the directory ``path``.
|
|
Returns the path the generated file.
|
|
|
|
This file implements the procedure
|
|
|
|
```
|
|
void install_tactics(tactic_manager & ctx)
|
|
```
|
|
|
|
It installs all tactics declared in the given header files
|
|
``h_files_full_path`` The procedure looks for ``ADD_TACTIC`` and
|
|
``ADD_PROBE``commands in the ``.h`` and ``.hpp`` files of these
|
|
components.
|
|
"""
|
|
ADD_TACTIC_DATA = []
|
|
ADD_SIMPLIFIER_DATA = []
|
|
ADD_PROBE_DATA = []
|
|
def ADD_TACTIC(name, descr, cmd):
|
|
ADD_TACTIC_DATA.append((name, descr, cmd))
|
|
|
|
def ADD_PROBE(name, descr, cmd):
|
|
ADD_PROBE_DATA.append((name, descr, cmd))
|
|
|
|
def ADD_SIMPLIFIER(name, descr, cmd):
|
|
ADD_SIMPLIFIER_DATA.append((name, descr, cmd))
|
|
|
|
eval_globals = {
|
|
'ADD_TACTIC': ADD_TACTIC,
|
|
'ADD_PROBE': ADD_PROBE,
|
|
'ADD_SIMPLIFIER': ADD_SIMPLIFIER
|
|
}
|
|
|
|
assert isinstance(h_files_full_path, list)
|
|
assert check_dir_exists(path)
|
|
fullname = os.path.join(path, 'install_tactic.cpp')
|
|
fout = open(fullname, 'w')
|
|
fout.write('// Automatically generated file.\n')
|
|
fout.write('#include "tactic/tactic.h"\n')
|
|
fout.write('#include "cmd_context/tactic_cmds.h"\n')
|
|
fout.write('#include "cmd_context/simplifier_cmds.h"\n')
|
|
fout.write('#include "cmd_context/cmd_context.h"\n')
|
|
tactic_pat = re.compile(r'[ \t]*ADD_TACTIC\(.*\)')
|
|
probe_pat = re.compile(r'[ \t]*ADD_PROBE\(.*\)')
|
|
simplifier_pat = re.compile(r'[ \t]*ADD_SIMPLIFIER\(.*\)')
|
|
for h_file in sorted_headers_by_component(h_files_full_path):
|
|
added_include = False
|
|
try:
|
|
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
|
for line in fin:
|
|
if tactic_pat.match(line):
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
try:
|
|
eval(line.strip('\n '), eval_globals, None)
|
|
except Exception as e:
|
|
_logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format(
|
|
fullname, line))
|
|
raise e
|
|
if probe_pat.match(line):
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
try:
|
|
eval(line.strip('\n '), eval_globals, None)
|
|
except Exception as e:
|
|
_logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format(
|
|
fullname, line))
|
|
raise e
|
|
if simplifier_pat.match(line):
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
try:
|
|
eval(line.strip('\n '), eval_globals, None)
|
|
except Exception as e:
|
|
_logger.error("Failed processing ADD_SIMPLIFIER command at '{}'\n{}".format(
|
|
fullname, line))
|
|
raise e
|
|
|
|
except Exception as e:
|
|
_logger.error("Failed to read file {}\n".format(h_file))
|
|
raise e
|
|
# First pass will just generate the tactic factories
|
|
fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n')
|
|
fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n')
|
|
fout.write('#define ADD_SIMPLIFIER_CMD(NAME, DESCR, CODE) ctx.insert(alloc(simplifier_cmd, symbol(NAME), DESCR, [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return CODE; }))\n')
|
|
fout.write('void install_tactics(tactic_manager & ctx) {\n')
|
|
for data in ADD_TACTIC_DATA:
|
|
fout.write(' ADD_TACTIC_CMD("%s", "%s", %s);\n' % data)
|
|
for data in ADD_PROBE_DATA:
|
|
fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data)
|
|
for data in ADD_SIMPLIFIER_DATA:
|
|
fout.write(' ADD_SIMPLIFIER_CMD("%s", "%s", %s);\n' % data)
|
|
fout.write('}\n')
|
|
fout.close()
|
|
return fullname
|
|
|
|
###############################################################################
|
|
# Functions for generating ``mem_initializer.cpp``
|
|
###############################################################################
|
|
|
|
def mk_mem_initializer_cpp_internal(h_files_full_path, path):
|
|
"""
|
|
Generate a ``mem_initializer.cpp`` file in the directory ``path``.
|
|
Returns the path to the generated file.
|
|
|
|
This file implements the procedures
|
|
|
|
```
|
|
void mem_initialize()
|
|
void mem_finalize()
|
|
```
|
|
|
|
These procedures are invoked by the Z3 memory_manager
|
|
"""
|
|
assert isinstance(h_files_full_path, list)
|
|
assert check_dir_exists(path)
|
|
initializer_cmds = []
|
|
finalizer_cmds = []
|
|
fullname = os.path.join(path, 'mem_initializer.cpp')
|
|
fout = open(fullname, 'w')
|
|
fout.write('// Automatically generated file.\n')
|
|
initializer_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
|
|
# ADD_INITIALIZER with priority
|
|
initializer_prio_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
|
|
finalizer_pat = re.compile(r'[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
|
|
for h_file in sorted_headers_by_component(h_files_full_path):
|
|
added_include = False
|
|
with io.open(h_file, encoding='utf-8', mode='r') as fin:
|
|
for line in fin:
|
|
m = initializer_pat.match(line)
|
|
if m:
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
initializer_cmds.append((m.group(1), 0))
|
|
m = initializer_prio_pat.match(line)
|
|
if m:
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
initializer_cmds.append((m.group(1), int(m.group(2))))
|
|
m = finalizer_pat.match(line)
|
|
if m:
|
|
if not added_include:
|
|
added_include = True
|
|
fout.write('#include "%s"\n' % path_after_src(h_file))
|
|
finalizer_cmds.append(m.group(1))
|
|
initializer_cmds.sort(key=lambda tup: tup[1])
|
|
fout.write('void mem_initialize() {\n')
|
|
for (cmd, prio) in initializer_cmds:
|
|
fout.write(cmd)
|
|
fout.write('\n')
|
|
fout.write('}\n')
|
|
fout.write('void mem_finalize() {\n')
|
|
for cmd in finalizer_cmds:
|
|
fout.write(cmd)
|
|
fout.write('\n')
|
|
fout.write('}\n')
|
|
fout.close()
|
|
return fullname
|
|
|
|
###############################################################################
|
|
# Functions for generating ``database.h``
|
|
###############################################################################
|
|
|
|
def mk_pat_db_internal(inputFilePath, outputFilePath):
|
|
"""
|
|
Generate ``g_pattern_database[]`` declaration header file.
|
|
"""
|
|
with open(inputFilePath, 'r') as fin:
|
|
with open(outputFilePath, 'w') as fout:
|
|
fout.write('static char const g_pattern_database[] =\n')
|
|
for line in fin:
|
|
fout.write('"%s\\n"\n' % line.strip('\n'))
|
|
fout.write(';\n')
|
|
|
|
###############################################################################
|
|
# Functions and data structures for generating ``*_params.hpp`` files from
|
|
# ``*.pyg`` files
|
|
###############################################################################
|
|
|
|
UINT = 0
|
|
BOOL = 1
|
|
DOUBLE = 2
|
|
STRING = 3
|
|
SYMBOL = 4
|
|
UINT_MAX = 4294967295
|
|
|
|
TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' }
|
|
TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' }
|
|
TYPE2GETTER = { UINT : 'get_uint', BOOL : 'get_bool', DOUBLE : 'get_double', STRING : 'get_str', SYMBOL : 'get_sym' }
|
|
|
|
def pyg_default(p):
|
|
if p[1] == BOOL:
|
|
if p[2]:
|
|
return "true"
|
|
else:
|
|
return "false"
|
|
return p[2]
|
|
|
|
def pyg_default_as_c_literal(p):
|
|
if p[1] == BOOL:
|
|
if p[2]:
|
|
return "true"
|
|
else:
|
|
return "false"
|
|
elif p[1] == STRING:
|
|
return '"%s"' % p[2]
|
|
elif p[1] == SYMBOL:
|
|
return 'symbol("%s")' % p[2]
|
|
elif p[1] == UINT:
|
|
return '%su' % p[2]
|
|
else:
|
|
return p[2]
|
|
|
|
def to_c_method(s):
|
|
return s.replace('.', '_')
|
|
|
|
|
|
def max_memory_param():
|
|
return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes')
|
|
|
|
def max_steps_param():
|
|
return ('max_steps', UINT, UINT_MAX, 'maximum number of steps')
|
|
|
|
def mk_hpp_from_pyg(pyg_file, output_dir):
|
|
"""
|
|
Generates the corresponding header file for the input pyg file
|
|
at the path ``pyg_file``. The file is emitted into the directory
|
|
``output_dir``.
|
|
|
|
Returns the path to the generated file
|
|
"""
|
|
CURRENT_PYG_HPP_DEST_DIR = output_dir
|
|
# Note OUTPUT_HPP_FILE cannot be a string as we need a mutable variable
|
|
# for the nested function to modify
|
|
OUTPUT_HPP_FILE = [ ]
|
|
# The function below has been nested so that it can use closure to capture
|
|
# the above variables that aren't global but instead local to this
|
|
# function. This avoids use of global state which makes this function safer.
|
|
def def_module_params(module_name, export, params, class_name=None, description=None):
|
|
dirname = CURRENT_PYG_HPP_DEST_DIR
|
|
assert(os.path.exists(dirname))
|
|
if class_name is None:
|
|
class_name = '%s_params' % module_name
|
|
hpp = os.path.join(dirname, '%s.hpp' % class_name)
|
|
out = open(hpp, 'w')
|
|
out.write('// Automatically generated file\n')
|
|
out.write('#pragma once\n')
|
|
out.write('#include "util/params.h"\n')
|
|
if export:
|
|
out.write('#include "util/gparams.h"\n')
|
|
out.write('struct %s {\n' % class_name)
|
|
out.write(' params_ref const & p;\n')
|
|
if export:
|
|
out.write(' params_ref g;\n')
|
|
out.write(' %s(params_ref const & _p = params_ref::get_empty()):\n' % class_name)
|
|
out.write(' p(_p)')
|
|
if export:
|
|
out.write(', g(gparams::get_module("%s"))' % module_name)
|
|
out.write(' {}\n')
|
|
out.write(' static void collect_param_descrs(param_descrs & d) {\n')
|
|
for param in params:
|
|
out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name))
|
|
out.write(' }\n')
|
|
if export:
|
|
out.write(' /*\n')
|
|
out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name))
|
|
if description is not None:
|
|
out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description))
|
|
out.write(' */\n')
|
|
# Generated accessors
|
|
for param in params:
|
|
if export:
|
|
out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' %
|
|
(TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
|
|
else:
|
|
out.write(' %s %s() const { return p.%s("%s", %s); }\n' %
|
|
(TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
|
|
out.write('};\n')
|
|
out.close()
|
|
OUTPUT_HPP_FILE.append(hpp)
|
|
|
|
# Globals to use when executing the ``.pyg`` file.
|
|
pyg_globals = {
|
|
'UINT' : UINT,
|
|
'BOOL' : BOOL,
|
|
'DOUBLE' : DOUBLE,
|
|
'STRING' : STRING,
|
|
'SYMBOL' : SYMBOL,
|
|
'UINT_MAX' : UINT_MAX,
|
|
'max_memory_param' : max_memory_param,
|
|
'max_steps_param' : max_steps_param,
|
|
# Note that once this function is entered that function
|
|
# executes with respect to the globals of this module and
|
|
# not the globals defined here
|
|
'def_module_params' : def_module_params,
|
|
}
|
|
with open(pyg_file, 'r') as fh:
|
|
eval(fh.read() + "\n", pyg_globals, None)
|
|
assert len(OUTPUT_HPP_FILE) == 1
|
|
return OUTPUT_HPP_FILE[0]
|