diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 26c081ee2..5b10dadd0 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2159,6 +2159,8 @@ namespace test_mapi Console.WriteLine(Microsoft.Z3.Version.Major.ToString()); Console.Write("Z3 Full Version: "); Console.WriteLine(Microsoft.Z3.Version.ToString()); + Console.Write("Z3 Full Version String: "); + Console.WriteLine(Microsoft.Z3.Version.FullVersion); SimpleExample(); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 5c8a7508f..5810dab37 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2291,6 +2291,8 @@ class JavaExample System.out.println(Version.getMajor()); System.out.print("Z3 Full Version: "); System.out.println(Version.getString()); + System.out.print("Z3 Full Version String: "); + System.out.println(Version.getFullVersion()); p.simpleExample(); diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index bab0ba2fc..eb64f8ee8 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -323,6 +323,7 @@ let _ = else ( Printf.printf "Running Z3 version %s\n" Version.to_string ; + Printf.printf "Z3 full version string: %s\n" Version.full_version ; let cfg = [("model", "true"); ("proof", "false")] in let ctx = (mk_context cfg) in let is = (Symbol.mk_int ctx 42) in diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f7b832bb9..78bc290f8 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -88,7 +88,7 @@ def init_project_def(): dll_name='libz3', static=build_static_lib(), export_files=API_files) - add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties') + add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk') add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest') add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 591f748ec..66191e160 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -82,6 +82,7 @@ Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False DOTNET_ENABLED=False +DOTNET_KEY_FILE=None JAVA_ENABLED=False ML_ENABLED=False PYTHON_INSTALL_ENABLED=False @@ -99,6 +100,7 @@ VS_PAR=False VS_PAR_NUM=8 GPROF=False GIT_HASH=False +GIT_DESCRIBE=False SLOW_OPTIMIZE=False USE_OMP=True @@ -534,11 +536,14 @@ def find_c_compiler(): raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.') def set_version(major, minor, build, revision): - global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION + global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION, GIT_DESCRIBE VER_MAJOR = major VER_MINOR = minor VER_BUILD = build VER_REVISION = revision + if GIT_DESCRIBE: + branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD']) + VER_REVISION = int(check_output(['git', 'rev-list', '--count', 'HEAD'])) def get_version(): return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) @@ -621,6 +626,7 @@ def display_help(exit_code): print(" --pypkgdir= Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR) print(" -b , --build= subdirectory where Z3 will be built (default: %s)." % BUILD_DIR) print(" --githash=hash include the given hash in the binaries.") + print(" --git-describe include the output of 'git describe' in the version information.") print(" -d, --debug compile Z3 in debug mode.") print(" -t, --trace enable tracing in release mode.") if IS_WINDOWS: @@ -633,6 +639,7 @@ def display_help(exit_code): if IS_WINDOWS: print(" --optimize generate optimized code during linking.") print(" --dotnet generate .NET bindings.") + print(" --dotnet-key= sign the .NET assembly using the private key in .") print(" --java generate Java bindings.") print(" --ml generate OCaml bindings.") print(" --python generate Python bindings.") @@ -668,14 +675,14 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED + global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', - 'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin']) + 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', + 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin']) except: print("ERROR: Invalid command line option") display_help(1) @@ -708,6 +715,8 @@ def parse_options(): TRACE = True elif opt in ('-.net', '--dotnet'): DOTNET_ENABLED = True + elif opt in ('--dotnet-key'): + DOTNET_KEY_FILE = arg elif opt in ('--staticlib'): STATIC_LIB = True elif opt in ('--staticbin'): @@ -732,6 +741,8 @@ def parse_options(): GPROF = True elif opt == '--githash': GIT_HASH=arg + elif opt == '--git-describe': + GIT_DESCRIBE = True elif opt in ('', '--ml'): ML_ENABLED = True elif opt in ('', '--noomp'): @@ -1491,7 +1502,7 @@ class PythonInstallComponent(Component): return class DotNetDLLComponent(Component): - def __init__(self, name, dll_name, path, deps, assembly_info_dir): + def __init__(self, name, dll_name, path, deps, assembly_info_dir, default_key_file): Component.__init__(self, name, path, deps) if dll_name is None: dll_name = name @@ -1499,6 +1510,7 @@ class DotNetDLLComponent(Component): assembly_info_dir = "." self.dll_name = dll_name self.assembly_info_dir = assembly_info_dir + self.key_file = default_key_file def mk_pkg_config_file(self): """ @@ -1524,6 +1536,8 @@ class DotNetDLLComponent(Component): configure_file(pkg_config_template, pkg_config_output, substitutions) def mk_makefile(self, out): + global DOTNET_KEY_FILE + if not is_dotnet_enabled(): return cs_fp_files = [] @@ -1554,17 +1568,24 @@ class DotNetDLLComponent(Component): '/linkresource:{}.dll'.format(get_component(Z3_DLL_COMPONENT).dll_name), ] ) - pathToSnk = os.path.join(self.to_src_dir, 'z3.snk') - snkFile = os.path.join(self.src_dir, 'z3.snk') - 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') - snkFile = os.path.join(self.src_dir, 'Microsoft.Z3.mono.snk') - if os.path.isfile(snkFile): - cscCmdLine.append('/keyfile:{}'.format(pathToSnk)) - else: - print("Keyfile is not configured: %s" % snkFile) + + # We need to give the assembly a strong name so that it + # can be installed into the GAC with ``make install`` + if not DOTNET_KEY_FILE is None: + self.key_file = DOTNET_KEY_FILE + + if not self.key_file is None: + if os.path.isfile(self.key_file): + self.key_file = os.path.abspath(self.key_file) + elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): + self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) + else: + print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.dll_name, self.key_file)) + self.key_file = None + + if not self.key_file is None: + print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file)) + cscCmdLine.append('/keyfile:{}'.format(self.key_file)) cscCmdLine.extend( ['/unsafe+', '/nowarn:1701,1702', @@ -1588,6 +1609,7 @@ class DotNetDLLComponent(Component): ) else: cscCmdLine.extend(['/optimize+']) + if IS_WINDOWS: if VS_X64: cscCmdLine.extend(['/platform:x64']) @@ -2172,8 +2194,8 @@ def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports= reg_component(name, c) return c -def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None): - c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir) +def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None, default_key_file=None): + c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir, default_key_file) reg_component(name, c) def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, manifest_file=None): @@ -2593,6 +2615,16 @@ def update_version(): mk_all_assembly_infos(major, minor, build, revision) mk_def_files() +def get_full_version_string(major, minor, build, revision): + global GIT_HASH, GIT_DESCRIBE + res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision) + if GIT_HASH: + res += " " + GIT_HASH + if GIT_DESCRIBE: + branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long']) + res += " master " + check_output(['git', 'describe']) + return '"' + res + '"' + # Update files with the version number def mk_version_dot_h(major, minor, build, revision): c = get_component(UTIL_COMPONENT) @@ -2606,6 +2638,7 @@ def mk_version_dot_h(major, minor, build, revision): 'Z3_VERSION_MINOR': str(minor), 'Z3_VERSION_PATCH': str(build), 'Z3_VERSION_TWEAK': str(revision), + 'Z3_FULL_VERSION': get_full_version_string(major, minor, build, revision) } ) if VERBOSE: diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index a5804bd45..418ccc58c 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -430,6 +430,11 @@ extern "C" { *revision_number = Z3_REVISION_NUMBER; } + Z3_string Z3_API Z3_get_full_version(void) { + LOG_Z3_get_full_version(); + return Z3_FULL_VERSION; + } + void Z3_API Z3_enable_trace(Z3_string tag) { memory::initialize(UINT_MAX); LOG_Z3_enable_trace(tag); diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 17e92a40e..3f2feb5a6 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -30,7 +30,7 @@ namespace Microsoft.Z3 /// /// Constructor. /// - /// + /// public InterpolationContext(Dictionary settings) : base(settings) { } #region Terms diff --git a/src/api/dotnet/Microsoft.Z3.mono.snk b/src/api/dotnet/Microsoft.Z3.snk similarity index 100% rename from src/api/dotnet/Microsoft.Z3.mono.snk rename to src/api/dotnet/Microsoft.Z3.snk diff --git a/src/api/dotnet/Version.cs b/src/api/dotnet/Version.cs index 6c22ce7fe..364ada781 100644 --- a/src/api/dotnet/Version.cs +++ b/src/api/dotnet/Version.cs @@ -83,6 +83,17 @@ namespace Microsoft.Z3 } } + /// + /// A full version string + /// + public static string FullVersion + { + get + { + return Native.Z3_get_full_version(); + } + } + /// /// A string representation of the version information. /// diff --git a/src/api/java/Version.java b/src/api/java/Version.java index 939a3ca5c..0579e2b05 100644 --- a/src/api/java/Version.java +++ b/src/api/java/Version.java @@ -63,6 +63,14 @@ public class Version return revision.value; } + /** + * A full version string + **/ + public static String getFullVersion() + { + return Native.getFullVersion(); + } + /** * A string representation of the version information. **/ diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index bbbb9e74b..b7016c4c8 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -25,6 +25,8 @@ module Version = struct let (major, minor, build, revision) = Z3native.get_version () + let full_version : string = Z3native.get_full_version() + let to_string = string_of_int major ^ "." ^ string_of_int minor ^ "." ^ diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 9104b3080..1c91b28aa 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -80,6 +80,9 @@ sig (** The revision. *) val revision : int + (** A full version string. *) + val full_version : string + (** A string representation of the version information. *) val to_string : string end diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 7dfb95318..345b33d94 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -79,6 +79,9 @@ def get_version(): Z3_get_version(major, minor, build, rev) return (major.value, minor.value, build.value, rev.value) +def get_full_version(): + return Z3_get_full_version() + # We use _z3_assert instead of the assert command because we want to # produce nice error messages in Z3Py at rise4fun.com def _z3_assert(cond, msg): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 3334d1617..666485a7f 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5139,6 +5139,13 @@ extern "C" { */ void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number); + /** + \brief Return a string that fully describes the version of Z3 in use. + + def_API('Z3_get_full_version', STRING, ()) + */ + Z3_string Z3_API Z3_get_full_version(void); + /** \brief Enable tracing messages tagged as \c tag when Z3 is compiled in debug mode. It is a NOOP otherwise diff --git a/src/util/version.h.in b/src/util/version.h.in index 05b619f2d..daf568a29 100644 --- a/src/util/version.h.in +++ b/src/util/version.h.in @@ -3,3 +3,5 @@ #define Z3_MINOR_VERSION @Z3_VERSION_MINOR@ #define Z3_BUILD_NUMBER @Z3_VERSION_PATCH@ #define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@ + +#define Z3_FULL_VERSION @Z3_FULL_VERSION@