From a2376b1016e6aed4a76869b735179239cffd65cb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Mar 2016 22:22:20 +0000 Subject: [PATCH 1/3] Try to fix #510. The breakage was caused by #498. The issue here is that in Python2 ``exec`` is a statement and ``exec`` is a function in Python3. For the ``exec`` statement to work we would need to write ``` exec line.strip(' \n') in exec_globals, None ``` We could write a wrapper function to do the right thing depending on the Python version but a better approach is to actually just use ``eval()`` rather than ``exec()`` because * ``eval()`` is less "evil" than ``exec()`` because it only evaluates a single expression. My testing so far seems to indicate that this is sufficient. * ``eval()`` is function in both Python 2 and 3 so we don't need to specialise the code based on Python version. --- scripts/mk_genfile_common.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 790ce7205..dbb09539e 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -246,7 +246,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): def ADD_PROBE(name, descr, cmd): ADD_PROBE_DATA.append((name, descr, cmd)) - exec_globals = { + eval_globals = { 'ADD_TACTIC': ADD_TACTIC, 'ADD_PROBE': ADD_PROBE, } @@ -272,7 +272,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), exec_globals) + eval(line.strip('\n '), eval_globals, None) except Exception as e: _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( fullname, line)) @@ -282,7 +282,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), exec_globals) + eval(line.strip('\n '), eval_globals, None) except Exception as e: _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( fullname, line)) @@ -514,6 +514,6 @@ def mk_hpp_from_pyg(pyg_file, output_dir): 'def_module_params' : def_module_params, } with open(pyg_file, 'r') as fh: - exec(fh.read() + "\n", pyg_globals, None) + eval(fh.read() + "\n", pyg_globals, None) assert len(OUTPUT_HPP_FILE) == 1 return OUTPUT_HPP_FILE[0] From 75af362b2562e792873584a9b043ee656acfcaf0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Mar 2016 23:27:26 +0000 Subject: [PATCH 2/3] Fix inconsistent emission of ``z3consts.py``. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary's keys being iterated over which has no defined order. This has been fixed by iterating over the dictionary's items and ordering by values. We could order by key rather than the values but seeing as these represent an enum, ordering by value makes more sense. --- scripts/mk_genfile_common.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index dbb09539e..7ac52738b 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -105,9 +105,9 @@ def mk_z3consts_py_internal(api_files, output_dir): 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)) + # 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: From 4814555c469bc64821dc01c59abad5cdd4698b06 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 13 Mar 2016 23:00:40 +0000 Subject: [PATCH 3/3] Fix inconsistent emission of ``gparams_register_modules.cpp``, ``install_tactics.cpp`` and ``mem_initialiszer.cpp`` files between the CMake and Python build systems. The problem was that the generated files were * Senstive to the order component directories were traversed * For CMake there are two directories (a source and build directory) for every component rather than a single directory like the Python build system has. To fix this a new function ``sorted_headers_by_component()`` has been added which defines a order that is consistent between both build systems. This function is then used on lists of paths to discovered header files. --- scripts/mk_genfile_common.py | 86 +++++++++++++++++++++++++++--------- 1 file changed, 65 insertions(+), 21 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 7ac52738b..2e2978a61 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -9,6 +9,7 @@ # to avoid having this code depend on the # of the Python build system. import os +import pprint import logging import re import sys @@ -38,6 +39,43 @@ def check_files_exist(files): 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/ast/fpa`` and ``/src/ast/fpa``). + We don't want to sort based on different ```` + and ```` 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) + # 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 ############################################################################### @@ -186,28 +224,30 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') + h_files_full_path = [] for component_src_dir in component_src_dirs: h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') + h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) + h_files_full_path.extend(h_files) + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with open(h_file, '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' % h_file) + fout.write('#include"%s"\n' % os.path.basename(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' % h_file) + fout.write('#include"%s"\n' % os.path.basename(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))) - fin.close() fout.write('void gparams_register_modules() {\n') for code in cmds: fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) @@ -261,16 +301,19 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): fout.write('#include"cmd_context.h"\n') tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') - for component_src_dir in component_src_dirs: + h_files_full_path = [] + for component_src_dir in sorted(component_src_dirs): h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') + h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) + h_files_full_path.extend(h_files) + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with open(h_file, 'r') as fin: for line in fin: if tactic_pat.match(line): if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) try: eval(line.strip('\n '), eval_globals, None) except Exception as e: @@ -280,14 +323,13 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): if probe_pat.match(line): if not added_include: added_include = True - fout.write('#include"%s"\n' % h_file) + fout.write('#include"%s"\n' % os.path.basename(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 - fin.close() # First pass will just generate the tactic factories idx = 0 for data in ADD_TACTIC_DATA: @@ -335,31 +377,33 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path): # ADD_INITIALIZER with priority initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - for component_src_dir in component_src_dirs: + h_files_full_path = [] + for component_src_dir in sorted(component_src_dirs): h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') + h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) + h_files_full_path.extend(h_files) + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with open(h_file, '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' % h_file) + fout.write('#include"%s"\n' % os.path.basename(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' % h_file) + fout.write('#include"%s"\n' % os.path.basename(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' % h_file) + fout.write('#include"%s"\n' % os.path.basename(h_file)) finalizer_cmds.append(m.group(1)) - fin.close() initializer_cmds.sort(key=lambda tup: tup[1]) fout.write('void mem_initialize() {\n') for (cmd, prio) in initializer_cmds: