diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3e5590d5e..e882e4a39 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -34,10 +34,13 @@ OCAMLC=getenv("OCAMLC", "ocamlc") OCAMLOPT=getenv("OCAMLOPT", "ocamlopt") OCAML_LIB=getenv("OCAML_LIB", None) OCAMLFIND=getenv("OCAMLFIND", "ocamlfind") +CSC=getenv("CSC", None) +GACUTIL=getenv("GACUTIL", None) # Standard install directories relative to PREFIX INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin") INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib") INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include") +INSTALL_PKGCONFIG_DIR=getenv("Z3_INSTALL_PKGCONFIG_DIR", os.path.join(INSTALL_LIB_DIR, 'pkgconfig')) CXX_COMPILERS=['g++', 'clang++'] C_COMPILERS=['gcc', 'clang'] @@ -71,7 +74,7 @@ ONLY_MAKEFILES = False Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False -DOTNET_ENABLED=False +DOTNET_ENABLED=True JAVA_ENABLED=False ML_ENABLED=False STATIC_LIB=False @@ -143,6 +146,7 @@ def which(program): exe_file = os.path.join(path, program) if is_exe(exe_file): return exe_file + return None class TempFile: def __init__(self, name): @@ -388,6 +392,43 @@ def check_java(): if JNI_HOME is None: raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.") +def check_dotnet(): + global CSC, GACUTIL + if IS_WINDOWS: + # Apparently building the dotnet bindings worked fine before + # so don't bother to try to detect anything + # FIXME: Shouldn't we be checking the supported version of .NET + # or something!? + if CSC == None: + CSC='csc.exe' + return + + # Check for the mono compiler + if CSC == None: + monoCompilerExecutable = 'mcs' + else: + monoCompilerExecutable = CSC + monoCompilerPath = which(monoCompilerExecutable) + if monoCompilerPath == None: + print(("ERROR: Could not find mono compiler ({}) in your PATH. " + "Either install it or disable building the dotnet bindings.").format( + monoCompilerExecutable)) + sys.exit(1) + CSC = monoCompilerPath + + # Check for gacutil (needed to install the dotnet bindings) + if GACUTIL == None: + gacutilExecutable = 'gacutil' + else: + gacutilExecutable = GACUTIL + gacutilPath = which(gacutilExecutable) + if gacutilPath == None: + print(("ERROR: Could not find the gacutil ({}) in your PATH. " + "Either install it or disable building the dotnet bindings.").format( + gacutilExecutable)) + sys.exit(1) + GACUTIL = gacutilPath + def check_ml(): t = TempFile('hello.ml') t.add('print_string "Hello world!\n";;') @@ -532,8 +573,6 @@ if os.name == 'nt': IS_WINDOWS=True # Visual Studio already displays the files being compiled SHOW_CPPS=False - # Enable .Net bindings by default on windows - DOTNET_ENABLED=True elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True @@ -566,8 +605,7 @@ def display_help(exit_code): print(" -m, --makefiles generate only makefiles.") if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") - if IS_WINDOWS: - print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") + print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") if IS_WINDOWS: print(" --optimize generate optimized code during linking.") print(" -j, --java generate Java bindings.") @@ -591,9 +629,12 @@ def display_help(exit_code): print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)") print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)") print(" OCAML_LIB Ocaml library directory (only relevant with --ml)") + print(" CSC C# Compiler (only relevant if dotnet bindings are enabled)") + print(" GACUTIL GAC Utility (only relevant if dotnet bindings are enabled)") print(" Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix") print(" Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix") print(" Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix") + print(" Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix") exit(exit_code) # Parse configuration option for mk_make script @@ -764,6 +805,9 @@ def is_java_enabled(): def is_ml_enabled(): return ML_ENABLED +def is_dotnet_enabled(): + return DOTNET_ENABLED + def is_compiler(given, expected): """ Return True if the 'given' compiler is the expected one. @@ -1294,37 +1338,113 @@ class DotNetDLLComponent(Component): self.dll_name = dll_name self.assembly_info_dir = assembly_info_dir + def mk_pkg_config_file(self): + """ + Create pkgconfig file for the dot net bindings. These + are needed by Monodevelop. + """ + pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) + substitutions = { 'PREFIX': PREFIX, + 'GAC_PKG_NAME': self.gac_pkg_name(), + 'VERSION': "{}.{}.{}.{}".format( + VER_MAJOR, + VER_MINOR, + VER_BUILD, + VER_REVISION) + } + pkg_config_output = os.path.join(BUILD_DIR, + self.build_dir, + '{}.pc'.format(self.gac_pkg_name())) + + # FIXME: Why isn't the build directory available? + mk_dir(os.path.dirname(pkg_config_output)) + # Configure file that will be installed by ``make install``. + configure_file(pkg_config_template, pkg_config_output, substitutions) + def mk_makefile(self, out): - if DOTNET_ENABLED: - cs_fp_files = [] - cs_files = [] - for cs_file in get_cs_files(self.src_dir): - cs_fp_files.append(os.path.join(self.to_src_dir, cs_file)) - cs_files.append(cs_file) - if self.assembly_info_dir != '.': - for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)): - cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file)) - cs_files.append(os.path.join(self.assembly_info_dir, cs_file)) - dllfile = '%s.dll' % self.dll_name - out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name)) - for cs_file in cs_fp_files: - out.write(' ') - out.write(cs_file) - out.write('\n') - out.write(' csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name)) - if DEBUG_MODE: - out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-') - else: - out.write(' /optimize+') - if VS_X64: - out.write(' /platform:x64') - else: - out.write(' /platform:x86') - for cs_file in cs_files: - out.write(' %s' % os.path.join(self.to_src_dir, cs_file)) - out.write('\n') - out.write('%s: %s\n\n' % (self.name, dllfile)) + if not DOTNET_ENABLED: return + cs_fp_files = [] + cs_files = [] + for cs_file in get_cs_files(self.src_dir): + cs_fp_files.append(os.path.join(self.to_src_dir, cs_file)) + cs_files.append(cs_file) + if self.assembly_info_dir != '.': + for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)): + cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file)) + cs_files.append(os.path.join(self.assembly_info_dir, cs_file)) + dllfile = '%s.dll' % self.dll_name + out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name)) + for cs_file in cs_fp_files: + out.write(' ') + out.write(cs_file) + out.write('\n') + + cscCmdLine = [CSC] + if IS_WINDOWS: + # Using these flags under the mono compiler results in build errors. + cscCmdLine.extend( [# What is the motivation for this? + '/noconfig+', + '/nostdlib+', + '/reference:mscorlib.dll', + # Under mono this isn't neccessary as mono will search the system + # library paths for libz3.so + '/linkresource:{}.dll'.format(get_component(Z3_DLL_COMPONENT).dll_name), + ] + ) + else: + # We need to give the assembly a strong name so that it + # can be installed into the GAC with ``make install`` + pathToSnk = os.path.join(self.to_src_dir, 'Microsoft.Z3.mono.snk') + cscCmdLine.append('/keyfile:{}'.format(pathToSnk)) + + cscCmdLine.extend( ['/unsafe+', + '/nowarn:1701,1702', + '/errorreport:prompt', + '/warn:4', + '/reference:System.Core.dll', + '/reference:System.dll', + '/reference:System.Numerics.dll', + '/filealign:512', # Why!? + '/out:{}.dll'.format(self.dll_name), + '/target:library', + '/doc:{}.xml'.format(self.dll_name), + ] + ) + if DEBUG_MODE: + cscCmdLine.extend( ['/define:DEBUG;TRACE', + '/debug+', + '/debug:full', + '/optimize-' + ] + ) + else: + cscCmdLine.extend(['/optimize+']) + if IS_WINDOWS: + if VS_X64: + cscCmdLine.extend(['/platform:x64']) + else: + cscCmdLine.extend(['/platform:x86']) + else: + # Just use default platform for now. + # If the dlls are run using mono then it + # ignores what the platform is set to anyway. + pass + + for cs_file in cs_files: + cscCmdLine.append('{}'.format(os.path.join(self.to_src_dir, cs_file))) + + # Now emit the command line + MakeRuleCmd.write_cmd(out, ' '.join(cscCmdLine)) + + # State that the high-level "dotnet" target depends on the .NET bindings + # dll we just created the build rule for + out.write('\n') + out.write('%s: %s\n\n' % (self.name, dllfile)) + + # Create pkg-config file + self.mk_pkg_config_file() + return def main_component(self): return DOTNET_ENABLED @@ -1350,6 +1470,50 @@ class DotNetDLLComponent(Component): # Do nothing return + def mk_install_deps(self, out): + if not DOTNET_ENABLED: + return + out.write('%s' % self.name) + + def gac_pkg_name(self): + return "{}.Sharp".format(self.dll_name) + + def _install_or_uninstall_to_gac(self, out, install): + gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()), + '/root', + '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR) + ] + if install: + install_or_uninstall_flag = '-i' + else: + # Note need use ``-us`` here which takes an assembly file name + # rather than ``-u`` which takes an assembly display name (e.g. + # ) + install_or_uninstall_flag = '-us' + MakeRuleCmd.write_cmd(out, '{gacutil} {install_or_uninstall_flag} {assembly_name}.dll -f {flags}'.format( + gacutil=GACUTIL, + install_or_uninstall_flag=install_or_uninstall_flag, + assembly_name=self.dll_name, + flags=' '.join(gacUtilFlags))) + + def mk_install(self, out): + if not DOTNET_ENABLED or IS_WINDOWS: + return + self._install_or_uninstall_to_gac(out, install=True) + + # Install pkg-config file. Monodevelop needs this to find Z3 + pkg_config_output = os.path.join(self.build_dir, + '{}.pc'.format(self.gac_pkg_name())) + MakeRuleCmd.make_install_directory(out, INSTALL_PKGCONFIG_DIR) + MakeRuleCmd.install_files(out, pkg_config_output, INSTALL_PKGCONFIG_DIR) + + def mk_uninstall(self, out): + if not DOTNET_ENABLED or IS_WINDOWS: + return + self._install_or_uninstall_to_gac(out, install=False) + pkg_config_file = os.path.join('lib','pkgconfig','{}.pc'.format(self.gac_pkg_name())) + MakeRuleCmd.remove_installed_files(out, pkg_config_file) + class JavaDLLComponent(Component): def __init__(self, name, dll_name, package_name, manifest_file, path, deps): Component.__init__(self, name, path, deps) @@ -1662,7 +1826,7 @@ class DotNetExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) out.write('\n') - out.write('\tcsc /out:%s /reference:%s /debug:full /reference:System.Numerics.dll' % (exefile, dll)) + out.write('\t%s /out:%s /reference:%s /debug:full /reference:System.Numerics.dll' % (CSC, exefile, dll)) if VS_X64: out.write(' /platform:x64') else: @@ -2029,6 +2193,9 @@ def mk_config(): print('OCaml Compiler: %s' % OCAMLC) print('OCaml Native: %s' % OCAMLOPT) print('OCaml Library: %s' % OCAML_LIB) + if is_dotnet_enabled(): + print('C# Compiler: %s' % CSC) + print('GAC utility: %s' % GACUTIL) config.close() @@ -2603,7 +2770,6 @@ def cp_z3py_to_build(): def mk_bindings(api_files): if not ONLY_MAKEFILES: mk_z3consts_py(api_files) - mk_z3consts_dotnet(api_files) new_api_files = [] api = get_component(API_COMPONENT) for api_file in api_files: @@ -2619,6 +2785,9 @@ def mk_bindings(api_files): if is_ml_enabled(): check_ml() mk_z3consts_ml(api_files) + if is_dotnet_enabled(): + check_dotnet() + mk_z3consts_dotnet(api_files) # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): @@ -3363,6 +3532,41 @@ def strip_path_prefix(path, prefix): assert not os.path.isabs(stripped_path) return stripped_path +def configure_file(template_file_path, output_file_path, substitutions): + """ + Read a template file ``template_file_path``, perform substitutions + found in the ``substitutions`` dictionary and write the result to + the output file ``output_file_path``. + + The template file should contain zero or more template strings of the + form ``@NAME@``. + + The substitutions dictionary maps old strings (without the ``@`` + symbols) to their replacements. + """ + assert isinstance(template_file_path, str) + assert isinstance(output_file_path, str) + assert isinstance(substitutions, dict) + assert len(template_file_path) > 0 + assert len(output_file_path) > 0 + print("Generating {} from {}".format(output_file_path, template_file_path)) + + if not os.path.exists(template_file_path): + raise MKException('Could not find template file "{}"'.format(template_file_path)) + + # Read whole template file into string + template_string = None + with open(template_file_path, 'r') as f: + template_string = f.read() + + # Do replacements + for (old_string, replacement) in substitutions.items(): + template_string = template_string.replace('@{}@'.format(old_string), replacement) + + # Write the string to the file + with open(output_file_path, 'w') as f: + f.write(template_string) + if __name__ == '__main__': import doctest doctest.testmod() diff --git a/src/api/dotnet/Microsoft.Z3.Sharp.pc.in b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in new file mode 100644 index 000000000..8ca4e788b --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in @@ -0,0 +1,7 @@ +prefix=@PREFIX@ +assemblies_dir=${prefix}/lib/mono/@GAC_PKG_NAME@ + +Name: @GAC_PKG_NAME@ +Description: .NET bindings for The Microsoft Z3 SMT solver +Version: @VERSION@ +Libs: -r:${assemblies_dir}/Microsoft.Z3.dll diff --git a/src/api/dotnet/Microsoft.Z3.mono.snk b/src/api/dotnet/Microsoft.Z3.mono.snk new file mode 100644 index 000000000..bfd0b3fce Binary files /dev/null and b/src/api/dotnet/Microsoft.Z3.mono.snk differ