From: Andres Noetzli Date: Mon, 26 Mar 2018 19:09:33 +0000 (-0700) Subject: Make Java bindings work with newer build envs (#1709) X-Git-Tag: cvc5-1.0.0~5207 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a4c2248a49506f60d555cbd7b99784b20ff02aef;p=cvc5.git Make Java bindings work with newer build envs (#1709) Our current build scripts did not work with Automake 1.16. At configure time, the .swig_deps target in src/bindings/Makefile.am was executed due to the `@mk_include@ .swig_deps` (which is not the case with older versions of Automake). This ultimately caused configure to fail because SWIG was complaining about missing files (generated source files, such as src/expr/expr.h). This commit fixes the issue by adding `-ignoremissing` to the call to SWIG. With that option, SWIG is not complaining about the missing files and the dependency generation completes successfully. Currently, the src/bindings/compat/java/create_impl.py script is not compatible with Python 3, which leads to errors when building on systems where `python` links to Python 3 (e.g. on Arch Linux). This commit makes the script compatible with both Python 2 and 3. Our build scripts were using old -source/-target versions when calling `javac`. Those are not supported by newer Java versions (e.g. Java 9). This commit updates the version to 1.6, which is still fairly old, so should be broadly supported. Finally, some systems (e.g. Arch Linux' AUR package for SWIG 2) refer to SWIG 2 as `swig-2`. This commit adds support for detecting this at configure time. --- diff --git a/config/bindings.m4 b/config/bindings.m4 index 3f75479bd..7174934c1 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -47,7 +47,7 @@ if test "$noswig" = yes; then SWIG= else if test -z "$SWIG"; then - AC_CHECK_PROGS(SWIG, [swig swig2.0], [], []) + AC_CHECK_PROGS(SWIG, [swig swig2.0 swig-2], [], []) else AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", []) fi diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index 994054882..fcfcb9409 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -181,7 +181,7 @@ CVC4.jar: java.cpp (cd java && \ rm -fr classes && \ mkdir -p classes && \ - $(JAVAC) -source 1.5 -target 1.5 -classpath . -d classes `find . -name '*.java'` && \ + $(JAVAC) -source 1.6 -target 1.6 -classpath . -d classes `find . -name '*.java'` && \ cd classes) && \ $(JAR) cf $@ -C java/classes . #java.cpp:; @@ -223,8 +223,11 @@ $(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdi $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) $(AM_V_GEN)$(SWIG) -Wall -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) $($(subst .,_,$@)_SWIGFLAGS) -o $@ $< +# Automake 1.16 is executing this target at configuration time. Because some +# generated source files do not exist at that time, we use the -ignoremissing +# option to not have SWIG complain about those missing files. $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i - $(AM_V_GEN)$(SWIG) -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -c++ -$(patsubst %.d,%,$@) -MM -o $(patsubst %.d,%.cpp,$@) $< + $(AM_V_GEN)$(SWIG) -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. -c++ -$(patsubst %.d,%,$@) -ignoremissing -MM -o $(patsubst %.d,%.cpp,$@) $< # .PHONY so they get rebuilt each time .PHONY: .swig_deps $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) .swig_deps: $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index eae498368..c3c256e8b 100644 --- a/src/bindings/compat/java/Makefile.am +++ b/src/bindings/compat/java/Makefile.am @@ -139,7 +139,7 @@ JniUtils.lo: src/cvc3/JniUtils.cpp .headers $(LIB_FILES:%=classes/cvc3/%.class) classes/cvc3/JniUtils.class: .classes .classes: - $(AM_V_GEN)mkdir -p classes && $(JAVAC) -source 1.4 -target 1.4 -sourcepath $(srcdir)/src -d classes $(LIB_FILES:%=$(srcdir)/src/cvc3/%.java) + $(AM_V_GEN)mkdir -p classes && $(JAVAC) -source 1.6 -target 1.6 -sourcepath $(srcdir)/src -d classes $(LIB_FILES:%=$(srcdir)/src/cvc3/%.java) @touch .classes .headers: $(LIB_FILES:%=cvc3/%.h) @touch .headers diff --git a/src/bindings/compat/java/create_impl.py b/src/bindings/compat/java/create_impl.py index 486f92080..875c8dd45 100644 --- a/src/bindings/compat/java/create_impl.py +++ b/src/bindings/compat/java/create_impl.py @@ -53,7 +53,8 @@ def is_vector3(arg_qual): # returns the jni type corresponding to the pseudo type signature -def arg_type_to_java((arg_qual, arg_type, arg_name)): +def arg_type_to_java(arg): + arg_qual, arg_type, arg_name = arg check_arg_qual(arg_qual); if arg_type == "jobject": if (not is_native(arg_qual)) or is_vector(arg_qual): @@ -90,7 +91,8 @@ def arg_type_to_java((arg_qual, arg_type, arg_name)): else: return "jobject" -def print_unembed_arg(cpp_file, (arg_qual, arg_type, arg_name)): +def print_unembed_arg(cpp_file, arg): + arg_qual, arg_type, arg_name = arg check_arg_qual(arg_qual); if arg_type == "jobject": () @@ -152,11 +154,13 @@ def print_unembed_args(cpp_file, args): print_unembed_arg(cpp_file, arg) -# check hat declaration and definition signatures match -def match_signatures((decl_result, decl_args), (def_result, def_args, _)): +# check that declaration and definition signatures match +def match_signatures(decl, defn): + decl_result, decl_args = decl + def_result, def_args, _ = defn if decl_result != def_result or len(decl_args) != len(def_args): return False - for i in xrange(0, len(decl_args)): + for i in range(0, len(decl_args)): java_type = arg_type_to_java(def_args[i]) #print java_type if decl_args[i] != java_type: @@ -179,14 +183,15 @@ def print_header(cpp_file, includes): def print_signature(cpp_file, name, result, args): arg_strings = ["JNIEnv* env", "jclass"] arg_strings.extend( \ - map(lambda (argQual, argType, argName): \ - arg_type_to_java((argQual, argType, argName)) \ - + " j" + argName, args)) + map(lambda arg: \ + arg_type_to_java(arg) \ + + " j" + arg[2], args)) cpp_file.writelines([ "JNIEXPORT " + result + " JNICALL " + name + "\n", "(" + ", ".join(arg_strings) + ")\n"]) -def print_definition(cpp_file, name, (result, args, body)): +def print_definition(cpp_file, name, defn): + result, args, body = defn cpp_file.writelines(["extern \"C\"\n"]) print_signature(cpp_file, name, result, args) cpp_file.writelines([ @@ -203,7 +208,7 @@ def print_definition(cpp_file, name, (result, args, body)): cpp_file.writelines([" return false;\n"]) elif result == "jint": cpp_file.writelines([" return -1;\n"]) - elif result <> "void": + elif result != "void": print("BUG: return type " + result + " is not handled in print_definition") sys.exit(1) cpp_file.writelines([" };\n", @@ -218,7 +223,7 @@ def print_cpp(cpp_name, declarations, definitions, includes): #names = declarations.keys() #names.sort() for name in declarations[0]: - if not definitions.has_key(name): + if name not in definitions: #continue print("Error: " + name + " is declared in header" \ + " but not defined in implementation.") @@ -230,7 +235,7 @@ def print_cpp(cpp_name, declarations, definitions, includes): if not match_signatures(declaration, definition): print("Error: signature for " + name \ + " in definition and implementation do not match:") - print declaration + print(declaration) print (definition[0], definition[1]) sys.exit(1) @@ -239,13 +244,14 @@ def print_cpp(cpp_name, declarations, definitions, includes): if not len(definitions) == 0: print("Error: found definitions in implementation" \ " without declaration in header file:") - print definitions + print(definitions) sys.exit(1) - except IOError, (error_nr, error_string): + except IOError as err: + error_nr, error_string = err print ("Couldn't open " + cpp_name + ": " + error_string) - sys.exit(0) + sys.exit(1) ### header file function declarations @@ -255,7 +261,7 @@ def print_cpp(cpp_name, declarations, definitions, includes): # - result: result type # - args: list of argument types, except for the first two (JNIEnv*, jclass) def register_declaration(declarations, name, result, args): - assert(not declarations[1].has_key(name)); + assert(name not in declarations[1]); declarations[0].append(name) declarations[1][name] = (result, args) @@ -303,9 +309,10 @@ def read_header(header_name): header_file.close() - except IOError, (error_nr, error_string): + except IOError as err: + error_nr, error_string = err print ("Couldn't open " + header_name + ": " + error_string) - sys.exit(0) + sys.exit(1) return declarations @@ -320,7 +327,7 @@ def read_header(header_name): # - args: list of pairs of argument types and argument names, # except for the first two (JNIEnv*, jclass) def register_definition(definitions, name, result, args, body): - if definitions.has_key(name): + if name in definitions: print("Error: redefinition of " + name + " in implementation.") sys.exit(1) @@ -391,9 +398,10 @@ def read_impl(impl_name): impl_file.close() - except IOError, (error_nr, error_string): + except IOError as err: + error_nr, error_string = err print ("Couldn't open " + impl_name + ": " + error_string) - sys.exit(0) + sys.exit(1) return definitions, includes