mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Fix regular expression strings with escapes (#6797)

Browse source
This commit is contained in:
Jerry James 2023-07-07 10:57:07 -06:00 committed by GitHub
parent f645bcf605
commit f5c069f899
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 30 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
scripts/mk_genfile_common.py
View file

@ -139,7 +139,7 @@ def mk_z3consts_py_internal(api_files, output_dir):
assert False, "Invalid %s, line: %s" % (api_file, linenum) assert False, "Invalid %s, line: %s" % (api_file, linenum)
else: else:
assert mode == IN_ENUM assert mode == IN_ENUM
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:
name = words[1] name = words[1]
@ -227,7 +227,7 @@ def mk_z3consts_dotnet_internal(api_files, output_dir):
assert False, "Invalid %s, line: %s" % (api_file, linenum) assert False, "Invalid %s, line: %s" % (api_file, linenum)
else: else:
assert mode == IN_ENUM assert mode == IN_ENUM
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:
name = words[1] name = words[1]
@ -315,7 +315,7 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir):
assert False, "Invalid %s, line: %s" % (api_file, linenum) assert False, "Invalid %s, line: %s" % (api_file, linenum)
else: else:
assert mode == IN_ENUM assert mode == IN_ENUM
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:
name = words[1] name = words[1]
@ -441,7 +441,7 @@ def mk_z3consts_ml_internal(api_files, output_dir):
assert False, "Invalid %s, line: %s" % (api_file, linenum) assert False, "Invalid %s, line: %s" % (api_file, linenum)
else: else:
assert mode == IN_ENUM assert mode == IN_ENUM
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:
name = words[1] name = words[1]
@ -574,7 +574,7 @@ def mk_def_file_internal(defname, dll_name, export_header_files):
for line in api: for line in api:
m = pat1.match(line) m = pat1.match(line)
if m: if m:
words = re.split('\W+', line) words = re.split(r'\W+', line)
i = 0 i = 0
for w in words: for w in words:
if w == 'Z3_API': if w == 'Z3_API':
@ -618,9 +618,9 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
fout = open(fullname, 'w') fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n') fout.write('// Automatically generated file.\n')
fout.write('#include "util/gparams.h"\n') fout.write('#include "util/gparams.h"\n')
reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') reg_pat = re.compile(r'[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') reg_mod_pat = re.compile(r'[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') reg_mod_descr_pat = re.compile(r'[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
for h_file in sorted_headers_by_component(h_files_full_path): for h_file in sorted_headers_by_component(h_files_full_path):
added_include = False added_include = False
with io.open(h_file, encoding='utf-8', mode='r') as fin: with io.open(h_file, encoding='utf-8', mode='r') as fin:
@ -698,9 +698,9 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
fout.write('#include "cmd_context/tactic_cmds.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/simplifier_cmds.h"\n')
fout.write('#include "cmd_context/cmd_context.h"\n') fout.write('#include "cmd_context/cmd_context.h"\n')
tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') tactic_pat = re.compile(r'[ \t]*ADD_TACTIC\(.*\)')
probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') probe_pat = re.compile(r'[ \t]*ADD_PROBE\(.*\)')
simplifier_pat = re.compile('[ \t]*ADD_SIMPLIFIER\(.*\)') simplifier_pat = re.compile(r'[ \t]*ADD_SIMPLIFIER\(.*\)')
for h_file in sorted_headers_by_component(h_files_full_path): for h_file in sorted_headers_by_component(h_files_full_path):
added_include = False added_include = False
try: try:
@ -780,10 +780,10 @@ def mk_mem_initializer_cpp_internal(h_files_full_path, path):
fullname = os.path.join(path, 'mem_initializer.cpp') fullname = os.path.join(path, 'mem_initializer.cpp')
fout = open(fullname, 'w') fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n') fout.write('// Automatically generated file.\n')
initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') initializer_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
# ADD_INITIALIZER with priority # ADD_INITIALIZER with priority
initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') initializer_prio_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') finalizer_pat = re.compile(r'[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
for h_file in sorted_headers_by_component(h_files_full_path): for h_file in sorted_headers_by_component(h_files_full_path):
added_include = False added_include = False
with io.open(h_file, encoding='utf-8', mode='r') as fin: with io.open(h_file, encoding='utf-8', mode='r') as fin:

28
scripts/mk_util.py
View file

@ -395,7 +395,7 @@ def check_java():
else: else:
# Search for jni.h in the library directories... # Search for jni.h in the library directories...
t = open('errout', 'r') t = open('errout', 'r')
open_pat = re.compile("\[search path for class files: (.*)\]") open_pat = re.compile(r"\[search path for class files: (.*)\]")
cdirs = [] cdirs = []
for line in t: for line in t:
m = open_pat.match(line) m = open_pat.match(line)
@ -812,8 +812,8 @@ def parse_options():
def extract_c_includes(fname): def extract_c_includes(fname):
result = {} result = {}
# We look for well behaved #include directives # We look for well behaved #include directives
std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") std_inc_pat = re.compile(r"[ \t]*#include[ \t]*\"(.*)\"[ \t]*")
system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*") system_inc_pat = re.compile(r"[ \t]*#include[ \t]*\<.*\>[ \t]*")
# We should generate and error for any occurrence of #include that does not match the previous pattern. # We should generate and error for any occurrence of #include that does not match the previous pattern.
non_std_inc_pat = re.compile(".*#include.*") non_std_inc_pat = re.compile(".*#include.*")
@ -1720,7 +1720,7 @@ class DotNetDLLComponent(Component):
print("Version output to csproj:", version) print("Version output to csproj:", version)
core_csproj_str = """<Project Sdk="Microsoft.NET.Sdk"> core_csproj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup> <PropertyGroup>
<TargetFramework>netstandard1.4</TargetFramework> <TargetFramework>netstandard1.4</TargetFramework>
@ -2246,7 +2246,7 @@ class DotNetExampleComponent(ExampleComponent):
else: else:
platform = 'x86' platform = 'x86'
dotnet_proj_str = """<Project Sdk="Microsoft.NET.Sdk"> dotnet_proj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup> <PropertyGroup>
<OutputType>Exe</OutputType> <OutputType>Exe</OutputType>
<TargetFramework>netcoreapp2.0</TargetFramework> <TargetFramework>netcoreapp2.0</TargetFramework>
@ -3162,7 +3162,7 @@ def mk_vs_proj_property_groups(f, name, target_ext, type):
f.write(' <Keyword>Win32Proj</Keyword>\n') f.write(' <Keyword>Win32Proj</Keyword>\n')
f.write(' <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str()) f.write(' <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str())
f.write(' </PropertyGroup>\n') f.write(' </PropertyGroup>\n')
f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n') f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.Default.props" />\n')
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n') f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n')
f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type) f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type)
f.write(' <CharacterSet>Unicode</CharacterSet>\n') f.write(' <CharacterSet>Unicode</CharacterSet>\n')
@ -3173,24 +3173,24 @@ def mk_vs_proj_property_groups(f, name, target_ext, type):
f.write(' <CharacterSet>Unicode</CharacterSet>\n') f.write(' <CharacterSet>Unicode</CharacterSet>\n')
f.write(' <UseOfMfc>false</UseOfMfc>\n') f.write(' <UseOfMfc>false</UseOfMfc>\n')
f.write(' </PropertyGroup>\n') f.write(' </PropertyGroup>\n')
f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n') f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.props" />\n')
f.write(' <ImportGroup Label="ExtensionSettings" />\n') f.write(' <ImportGroup Label="ExtensionSettings" />\n')
f.write(' <ImportGroup Label="PropertySheets">\n') f.write(' <ImportGroup Label="PropertySheets">\n')
f.write(' <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n') f.write(' <Import Project="$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n')
f.write(' <PropertyGroup Label="UserMacros" />\n') f.write(' <PropertyGroup Label="UserMacros" />\n')
f.write(' <PropertyGroup>\n') f.write(' <PropertyGroup>\n')
f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n') f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name) f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name)
f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext) f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext)
f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n') f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name) f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name)
f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext) f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext)
f.write(' </PropertyGroup>\n') f.write(' </PropertyGroup>\n')
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n') f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n') f.write(' <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
f.write(' </PropertyGroup>\n') f.write(' </PropertyGroup>\n')
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n') f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n') f.write(' <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
f.write(' </PropertyGroup>\n') f.write(' </PropertyGroup>\n')
@ -3267,7 +3267,7 @@ def mk_vs_proj(name, components):
mk_vs_proj_link_exe(f, name, debug=False) mk_vs_proj_link_exe(f, name, debug=False)
f.write(' </ItemDefinitionGroup>\n') f.write(' </ItemDefinitionGroup>\n')
mk_vs_proj_dep_groups(f, name, components) mk_vs_proj_dep_groups(f, name, components)
f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n') f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
f.write(' <ImportGroup Label="ExtensionTargets">\n') f.write(' <ImportGroup Label="ExtensionTargets">\n')
f.write(' </ImportGroup>\n') f.write(' </ImportGroup>\n')
f.write('</Project>\n') f.write('</Project>\n')
@ -3308,7 +3308,7 @@ def mk_vs_proj_dll(name, components):
mk_vs_proj_link_dll(f, name, debug=False) mk_vs_proj_link_dll(f, name, debug=False)
f.write(' </ItemDefinitionGroup>\n') f.write(' </ItemDefinitionGroup>\n')
mk_vs_proj_dep_groups(f, name, components) mk_vs_proj_dep_groups(f, name, components)
f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n') f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
f.write(' <ImportGroup Label="ExtensionTargets">\n') f.write(' <ImportGroup Label="ExtensionTargets">\n')
f.write(' </ImportGroup>\n') f.write(' </ImportGroup>\n')
f.write('</Project>\n') f.write('</Project>\n')

4
scripts/update_api.py
View file

@ -116,8 +116,8 @@ class APITypes:
def def_Types(self, api_files): def def_Types(self, api_files):
global Closures global Closures
pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") pat1 = re.compile(r" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") pat2 = re.compile(r"Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)")
for api_file in api_files: for api_file in api_files:
with open(api_file, 'r') as api: with open(api_file, 'r') as api:
for line in api: for line in api: