From 61d1cd524ea1cfd73b0554071ebdb7b891701b4a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 25 Nov 2015 18:33:59 +0000 Subject: [PATCH 1/2] Teach the build system to build and install the ".NET bindings" under non Windows systems (i.e. Using mono). Building these bindings is unfortunately on by default because I didn't want to change the command line interface (i.e. ``--nodotnet``) which people might be relying on. This should really be changed to match the other binding flags (e.g. ``--java``) but I will leave this for now. To perform the build a C# compiler and the GAC utility are required. The script will try to automatically detect them but the user can override this by setting the ``CSC`` and ``GACUTIL`` environment variables. In order for the ".NET bindings" to be installed the assembly (``Microsoft.Z3.dll``) needs to have a strong name which means we need a Strong name key file which is what the ``Microsoft.Z3.mono.snk`` is for. This is the public and private key so this key **must never** be used for checking integrity. Instead its only purpose is to avoid any name clashes in the GAC. It is also worth noting that slightly different flags needs to be passed to the C# compiler on non Windows platforms. I don't understand why some of the flags are being used on Windows but I left a comment there that hopefully someone can fix... --- scripts/mk_util.py | 203 ++++++++++++++++++++++----- src/api/dotnet/Microsoft.Z3.mono.snk | Bin 0 -> 596 bytes 2 files changed, 167 insertions(+), 36 deletions(-) create mode 100644 src/api/dotnet/Microsoft.Z3.mono.snk diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3e5590d5e..4c959d0af 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -34,6 +34,8 @@ 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") @@ -71,7 +73,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 +145,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 +391,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 +572,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 +604,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,6 +628,8 @@ 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") @@ -764,6 +803,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. @@ -1295,36 +1337,86 @@ class DotNetDLLComponent(Component): self.assembly_info_dir = assembly_info_dir 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)) + return def main_component(self): return DOTNET_ENABLED @@ -1350,6 +1442,40 @@ class DotNetDLLComponent(Component): # Do nothing return + def mk_install_deps(self, out): + if not DOTNET_ENABLED: + return + out.write('%s' % self.name) + + def _install_or_uninstall_to_gac(self, out, install): + gacUtilFlags = ['/package {}'.format(self.dll_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) + + + def mk_uninstall(self, out): + if not DOTNET_ENABLED or IS_WINDOWS: + return + self._install_or_uninstall_to_gac(out, install=False) + class JavaDLLComponent(Component): def __init__(self, name, dll_name, package_name, manifest_file, path, deps): Component.__init__(self, name, path, deps) @@ -1662,7 +1788,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 +2155,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 +2732,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 +2747,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): diff --git a/src/api/dotnet/Microsoft.Z3.mono.snk b/src/api/dotnet/Microsoft.Z3.mono.snk new file mode 100644 index 0000000000000000000000000000000000000000..bfd0b3fce33b18365bd122d6a0d62ff6d3009d9c GIT binary patch literal 596 zcmV-a0;~N80ssI2Bme+XQ$aES1ONaL0001Y34hdwvy+iiZ#CZ+ujhi)%r=<6Q8y{p zWd(E&Kd0wt3Gt#xDja-EY{bN8$?%f*Rp`ZE>13cTF5+QMo#08Lf2%cIGKqZ`K@4-+ zTsjW>z5Q=C!`0b2I^O^9xuwZgq@m6o0~CGwC7U}EXF#LI{aB?AFSD)=GNImE@n47~ zNfnUXCH#^;ihK;ZpH4gXY6$99SG%}$g$X)=M29Z?DsM9Xid1^sFniHkOAny+!WZU5 zv@$Vn;aJ~QDk_p|YrCkbZcQ|OhS7JHvo?JOn~$4$*ben1%g8fHQm<11=P#P?n8HL% zCbebljs}XZIdt6+=HHQtn)3IzxpGLJ0!*4%1>)`S7G?b_#L!sU{>e8SN$prW{{PZI%Uww-Cr=*B1%Hm z6HcqPj(4hdqKzWmY)bnLDd!j zMNM!Wwmxd*8!TNDY;m|h{ih0qrCNLuT_OLx+KU-Ys3Rlb72$ziy_Ny1G7=uXUmQ5K i?izOc;@RNPcI)+#xXX8XY(Q literal 0 HcmV?d00001 From c8a2b6645a96ca20fe38cf80f1550a008640db20 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 26 Nov 2015 17:34:02 +0000 Subject: [PATCH 2/2] Teach the build system to generate and install a pkg-config file for the ".NET" bindings. This file is required for Monodevelop to find the bindings because Monodevelop uses pkg-config to find packages (it doesn't use the GAC). For lack of a better name the GAC (and pkg-config) package name is now ``Microsoft.Z3.Sharp``. I don't want to call it ``Microsoft.Z3`` because someone may want to create a ``Microsoft.Z3.pc`` file in the future for the native Z3 library (i.e. C++ or C bindings). In addition there is a new utility function ``configure_file()`` which reads a template file, applies some substitutions and writes the result to another file. This very similar to what CMake does. There is a new environment variable ``Z3_INSTALL_PKGCONFIG_DIR`` which allows pkgconfig directory to be controlled for the install. --- scripts/mk_util.py | 75 ++++++++++++++++++++++++- src/api/dotnet/Microsoft.Z3.Sharp.pc.in | 7 +++ 2 files changed, 81 insertions(+), 1 deletion(-) create mode 100644 src/api/dotnet/Microsoft.Z3.Sharp.pc.in diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4c959d0af..e882e4a39 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -40,6 +40,7 @@ GACUTIL=getenv("GACUTIL", None) 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'] @@ -633,6 +634,7 @@ def display_help(exit_code): 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 @@ -1336,6 +1338,29 @@ 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 not DOTNET_ENABLED: return @@ -1416,6 +1441,9 @@ class DotNetDLLComponent(Component): # 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): @@ -1447,8 +1475,11 @@ class DotNetDLLComponent(Component): 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.dll_name), + gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()), '/root', '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR) ] @@ -1470,11 +1501,18 @@ class DotNetDLLComponent(Component): 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): @@ -3494,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