From 10d01a8379b1db9db5815d37854246b39345055b Mon Sep 17 00:00:00 2001
From: unknown <leonardo@Z3-1.redmond.corp.microsoft.com>
Date: Wed, 21 Nov 2012 22:52:52 -0800
Subject: [PATCH] Compiling java bindings on Windows
---
scripts/mk_project.py | 2 +-
scripts/mk_util.py | 66 +++++++++++++++++++++++++++----------------
scripts/update_api.py | 27 ++++++++++--------
3 files changed, 57 insertions(+), 38 deletions(-)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 2f2f4a721..6d2b7c70e 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -71,7 +71,7 @@ def init_project_def():
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_java_dll('java', 'api/java', dll_name='libz3j')
+ add_java_dll('java', 'api/java', dll_name='libz3java')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
set_z3py_dir('api/python')
# Examples
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 34ec94626..35ef7166d 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -26,7 +26,7 @@ import string
def getenv(name, default):
try:
- return os.environ[name]
+ return os.environ[name].strip(' "\'')
except:
return default
@@ -37,6 +37,7 @@ CXXFLAGS=getenv("CXXFLAGS", "")
LDFLAGS=getenv("LDFLAGS", "")
JAVA=getenv("JAVA", "java")
JAVAC=getenv("JAVAC", "javac")
+JAVA_HOME=getenv("JAVA_HOME", None)
CXX_COMPILERS=['g++', 'clang++']
C_COMPILERS=['gcc', 'clang']
@@ -71,7 +72,9 @@ VER_BUILD=None
VER_REVISION=None
PREFIX='/usr'
GMP=False
-JAVA_HOME=None
+
+def is_windows():
+ return IS_WINDOWS
def unix_path2dos(path):
return string.join(path.split('/'), '\\')
@@ -110,20 +113,25 @@ class TempFile:
try:
os.remove(self.name)
except:
- raise MKException("Failed to eliminate temporary file '%s'" % self.name)
+ pass
def exec_cmd(cmd):
if isinstance(cmd, str):
cmd = cmd.split(' ')
new_cmd = []
+ first = True
for e in cmd:
- e = e.strip(' ')
- if e != "":
- se = e.split(' ')
- if len(se) > 1:
- new_cmd.extend(se)
- else:
- new_cmd.append(e)
+ if first:
+ # Allow spaces in the executable name
+ first = False
+ new_cmd.append(e)
+ else:
+ if e != "":
+ se = e.split(' ')
+ if len(se) > 1:
+ new_cmd.extend(se)
+ else:
+ new_cmd.append(e)
cmd = new_cmd
null = open(os.devnull, 'wb')
try:
@@ -181,18 +189,15 @@ def check_java():
rmf('Hello.class')
if r != 0:
raise MKException('Failed testing Java program. Set environment variable JAVA with the path to the Java virtual machine')
- t2 = TempFile('Z3Native.java')
- t2.add('public final class Z3Native { public static native long mkConfig(); }\n')
- t2.commit()
- if is_verbose():
- print "Testing %s (for JNI)..." % JAVAC
- r = exec_cmd([JAVAC, 'Z3Native.java'])
- if r != 0:
- raise MKException('Failed testing Java compiler (for source containing JNI bindings). Set environment variable JAVAC with the path to the Java compiler')
find_java_home()
def find_java_home():
global JAVA_HOME
+ if JAVA_HOME != None:
+ if is_verbose():
+ print "Checking jni.h..."
+ if os.path.exists('%s%sinclude%sjni.h' % (JAVA_HOME, os.sep, os.sep)):
+ return
if is_verbose():
print "Finding JAVA_HOME..."
t = TempFile('output')
@@ -208,12 +213,13 @@ def find_java_home():
m = open_pat.match(line)
if m:
# Remove last 3 directives from m.group(1)
+ print m.group(1)
tmp = m.group(1).split(os.sep)
path = string.join(tmp[:len(tmp) - 3], os.sep)
if is_verbose():
print "Checking jni.h..."
- if not os.path.exists('%s/include/jni.h' % path):
- raise MKException("Failed to detect jni.h at '%s/include'" % path)
+ if not os.path.exists('%s%sinclude%sjni.h' % (path, os.sep, os.sep)):
+ raise MKException("Failed to detect jni.h at '%s%sinclude'" % (path, os.sep))
JAVA_HOME = path
return
raise MKException('Failed to find JAVA_HOME')
@@ -344,6 +350,7 @@ def display_help(exit_code):
print " CXXFLAGS C++ compiler flags"
print " JAVA Java virtual machine (only relevant if -j or --java option is provided)"
print " JAVAC Java compiler (only relevant if -j or --java option is provided)"
+ print " JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)"
exit(exit_code)
# Parse configuration option for mk_make script
@@ -716,9 +723,9 @@ class ExeComponent(Component):
def require_mem_initializer(self):
return True
- # All executables are included in the all: rule
+ # All executables (to be installed) are included in the all: rule
def main_component(self):
- return True
+ return self.install
def mk_install(self, out):
if self.install:
@@ -924,13 +931,16 @@ class JavaDLLComponent(Component):
if is_java_enabled():
dllfile = '%s$(SO_EXT)' % self.dll_name
out.write('%s: %s/Z3Native.java %s$(SO_EXT)\n' % (dllfile, self.to_src_dir, get_component('api_dll').dll_name))
- out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC))
if IS_WINDOWS:
+ out.write('\tcd %s && %s Z3Native.java\n' % (unix_path2dos(self.to_src_dir), JAVAC))
out.write('\tmove %s\\*.class .\n' % unix_path2dos(self.to_src_dir))
+ out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I"%s/include/win32" -I%s %s/Z3Native.c\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
+ out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) Z3Native$(OBJ_EXT) libz3.lib\n' % dllfile)
else:
+ out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC))
out.write('\tmv %s/*.class .\n' % self.to_src_dir)
- out.write('\t$(CC) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
- out.write('\t$(CC) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile)
+ out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
+ out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile)
out.write('%s: %s\n\n' % (self.name, dllfile))
def main_component(self):
@@ -1146,6 +1156,12 @@ def mk_config():
'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')
# End of Windows VS config.mk
+ if is_verbose():
+ print '64-bit: %s' % is64()
+ if is_java_enabled():
+ print 'Java Home: %s' % JAVA_HOME
+ print 'Java Compiler: %s' % JAVAC
+ print 'Java VM: %s' % JAVA
else:
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS
ARITH = "internal"
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 568737eee..a82ac205a 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -504,7 +504,10 @@ def mk_java():
java_native.write(' public static class IntPtr { public int value; }\n')
java_native.write(' public static class LongPtr { public long value; }\n')
java_native.write(' public static class StringPtr { public String value; }\n')
- java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
+ if is_windows():
+ java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java'))
+ else:
+ java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
for name, result, params in _dotnet_decls:
java_native.write(' public static native %s %s(' % (type2java(result), java_method_name(name)))
first = True
@@ -543,7 +546,7 @@ def mk_java():
if k == OUT or k == INOUT:
java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
- java_wrapper.write(' %s * _a%s = (%s *) (*jenv)->%s(jenv, a%s, NULL);\n' % (type2str(param_type(param)),
+ java_wrapper.write(' %s * _a%s = (%s *) jenv->%s(a%s, NULL);\n' % (type2str(param_type(param)),
i,
type2str(param_type(param)),
java_get_array_elements(param),
@@ -555,7 +558,7 @@ def mk_java():
param_array_capacity_pos(param),
type2str(param_type(param))))
elif k == IN and param_type(param) == STRING:
- java_wrapper.write(' Z3_string _a%s = (Z3_string) (*jenv)->GetStringUTFChars(jenv, a%s, NULL);\n' % (i, i))
+ java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
i = i + 1
# invoke procedure
java_wrapper.write(' ')
@@ -585,34 +588,34 @@ def mk_java():
for param in params:
k = param_kind(param)
if k == OUT_ARRAY:
- java_wrapper.write(' (*jenv)->%s(jenv, a%s, 0, (jsize)a%s, (%s *) _a%s);\n' % (java_set_array_region(param),
+ java_wrapper.write(' jenv->%s(a%s, 0, (jsize)a%s, (%s *) _a%s);\n' % (java_set_array_region(param),
i,
param_array_capacity_pos(param),
java_array_element_type(param),
i))
java_wrapper.write(' free(_a%s);\n' % i)
elif k == IN_ARRAY or k == OUT_ARRAY:
- java_wrapper.write(' (*jenv)->%s(jenv, a%s, (%s *) _a%s, JNI_ABORT);\n' % (java_release_array_elements(param),
+ java_wrapper.write(' jenv->%s(a%s, (%s *) _a%s, JNI_ABORT);\n' % (java_release_array_elements(param),
i,
java_array_element_type(param),
i))
elif k == OUT or k == INOUT:
if param_type(param) == INT or param_type(param) == UINT:
java_wrapper.write(' {\n')
- java_wrapper.write(' jclass mc = (*jenv)->GetObjectClass(jenv, a%s);\n' % i)
- java_wrapper.write(' jfieldID fid = (*jenv)->GetFieldID(jenv, mc, "value", "I");\n')
- java_wrapper.write(' (*jenv)->SetIntField(jenv, a%s, fid, (jint) _a%s);\n' % (i, i))
+ java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
+ java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
+ java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
java_wrapper.write(' }\n')
else:
java_wrapper.write(' {\n')
- java_wrapper.write(' jclass mc = (*jenv)->GetObjectClass(jenv, a%s);\n' % i)
- java_wrapper.write(' jfieldID fid = (*jenv)->GetFieldID(jenv, mc, "value", "J");\n')
- java_wrapper.write(' (*jenv)->SetLongField(jenv, a%s, fid, (jlong) _a%s);\n' % (i, i))
+ java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
+ java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
+ java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
java_wrapper.write(' }\n')
i = i + 1
# return
if result == STRING:
- java_wrapper.write(' return (*jenv)->NewStringUTF(jenv, result);\n')
+ java_wrapper.write(' return jenv->NewStringUTF(result);\n')
elif result != VOID:
java_wrapper.write(' return (%s) result;\n' % type2javaw(result))
java_wrapper.write('}\n')