From 692593baaa391ab747a08f3781224c22d26aa575 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 Nov 2012 22:31:07 +0000 Subject: [PATCH] Java API: 32-bit issues and bugfixes. Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 50 +++++++++++++++++++--------- scripts/update_api.py | 60 ++++++++++++++++++++++------------ src/api/java/AST.java | 39 +++++++++++++--------- src/api/java/Context.java | 2 +- src/api/java/EnumSort.java | 9 ++--- src/api/java/Quantifier.java | 15 +++++---- src/api/java/Sort.java | 13 +++++--- src/api/java/Z3Object.java | 2 +- 8 files changed, 119 insertions(+), 71 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 5d56a474b..d06f72217 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -907,11 +907,10 @@ class JavaExample // Error handling test. try { - IntExpr i = ctx.MkInt("0.5"); + IntExpr i = ctx.MkInt("1/2"); throw new TestFailedException(); // unreachable } catch (Z3Exception e) - { - System.out.println("GOT: " + e.getMessage()); + { } } @@ -1001,19 +1000,38 @@ class JavaExample } AST a = ctx.MkInt(42); - Expr ae = (a.getClass() == Expr.class) ? ((Expr) a) : null; - if (ae == null) + + try + { + Expr.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); - ArithExpr aae = (a.getClass() == ArithExpr.class) ? ((ArithExpr) a) - : null; - if (aae == null) + } + + try + { + ArithExpr.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); - IntExpr aie = (a.getClass() == IntExpr.class) ? ((IntExpr) a) : null; - if (aie == null) + } + + try + { + IntExpr.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); - IntNum ain = (a.getClass() == IntNum.class) ? ((IntNum) a) : null; - if (ain == null) + } + + try + { + IntNum.class.cast(a); + } catch (ClassCastException e) + { throw new TestFailedException(); + } Expr[][] earr = new Expr[2][]; earr[0] = new Expr[2]; @@ -1585,7 +1603,7 @@ class JavaExample Symbol name = ctx.MkSymbol("fruit"); - EnumSort fruit = ctx.MkEnumSort(ctx.MkSymbol("fruit"), + EnumSort fruit = ctx.MkEnumSort(name, new Symbol[] { ctx.MkSymbol("apple"), ctx.MkSymbol("banana"), ctx.MkSymbol("orange") }); @@ -1974,7 +1992,7 @@ class JavaExample { int num_Exprs = to_minimize.length; int[] upper = new int[num_Exprs]; - int[] lower = new int[num_Exprs]; + int[] lower = new int[num_Exprs]; for (int i = 0; i < upper.length; ++i) { upper[i] = Integer.MAX_VALUE; @@ -2207,12 +2225,12 @@ class JavaExample { System.out.println("Z3 Managed Exception: " + ex.getMessage()); System.out.println("Stack trace: "); - ex.printStackTrace(System.out); + ex.printStackTrace(System.out); } catch (TestFailedException ex) { System.out.println("TEST CASE FAILED: " + ex.getMessage()); System.out.println("Stack trace: "); - ex.printStackTrace(System.out); + ex.printStackTrace(System.out); } catch (Exception ex) { System.out.println("Unknown Exception: " + ex.getMessage()); diff --git a/scripts/update_api.py b/scripts/update_api.py index f89764299..d7dbb7bcf 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -474,11 +474,6 @@ def java_array_element_type(p): return 'jint' else: return 'jlong' -def java_set_array_region(p): - if param_type(p) == INT or param_type(p) == UINT: - return 'SetIntArrayRegion' - else: - return 'SetLongArrayRegion' def mk_java(): if not is_java_enabled(): @@ -563,21 +558,43 @@ def mk_java(): java_wrapper.write('#endif\n\n') java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') - java_wrapper.write(' T * NEW = (T*) jenv->GetLongArrayElements(OLD, NULL); \n') + java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') - java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') + java_wrapper.write(' if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') + java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW); \n') + java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW) \n\n') java_wrapper.write('#else\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write(' T * NEW = 0; { \\\n') - java_wrapper.write(' jlong * temp = jenv->GetLongArrayElements(OLD, NULL); \\\n') - java_wrapper.write(' unsigned int size = jenv->GetArrayLength(OLD); \\\n') - java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') - java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') - java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') - java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') - java_wrapper.write(' } \n\n') - java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') + java_wrapper.write(' jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \\\n') + java_wrapper.write(' unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \\\n') + java_wrapper.write(' if (OLD != 0) { \\\n') + java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') + java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') + java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') + java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') + java_wrapper.write(' } \\\n') + java_wrapper.write(' } \n\n') + java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write(' delete [] NEW; \n\n') + java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' { \\\n') + java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') + java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n') + java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n') + java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') + java_wrapper.write(' delete [] temp; \\\n') + java_wrapper.write(' }\n\n') + java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n') + java_wrapper.write(' { \\\n') + java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') + java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n') + java_wrapper.write(' temp[i] = reinterpret_cast(NEW[i]); \\\n') + java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \\\n') + java_wrapper.write(' delete [] temp; \\\n') + java_wrapper.write(' }\n\n') java_wrapper.write('#endif\n\n') java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n') java_wrapper.write('{\n') @@ -615,6 +632,10 @@ def mk_java(): type2str(param_type(param)), param_array_capacity_pos(param), type2str(param_type(param)))) + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + else: + java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) elif k == IN and param_type(param) == STRING: java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) i = i + 1 @@ -646,11 +667,10 @@ def mk_java(): for param in params: k = param_kind(param) if k == OUT_ARRAY: - 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)) + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + else: + java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i)) java_wrapper.write(' free(_a%s);\n' % i) elif k == IN_ARRAY or k == OUT_ARRAY: if param_type(param) == INT or param_type(param) == UINT: diff --git a/src/api/java/AST.java b/src/api/java/AST.java index fbefbf5e2..418c43e9f 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -37,10 +37,15 @@ public class AST extends Z3Object **/ public boolean equals(Object o) { - AST casted = (AST) o; - if (casted == null) - return false; - return this == casted; + AST casted = null; + + try { + casted = AST.class.cast(o); + } catch (ClassCastException e) { + return false; + } + + return this.NativeObject() == casted.NativeObject(); } /** @@ -53,18 +58,20 @@ public class AST extends Z3Object { if (other == null) return 1; - AST oAST = (AST) other; - if (oAST == null) - return 1; - else - { - if (Id() < oAST.Id()) - return -1; - else if (Id() > oAST.Id()) - return +1; - else - return 0; - } + + AST oAST = null; + try { + AST.class.cast(other); + } catch (ClassCastException e) { + return 1; + } + + if (Id() < oAST.Id()) + return -1; + else if (Id() > oAST.Id()) + return +1; + else + return 0; } /** diff --git a/src/api/java/Context.java b/src/api/java/Context.java index f375ab525..d6076b5ee 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -524,7 +524,7 @@ public class Context extends IDisposable public Expr MkConst(FuncDecl f) throws Z3Exception { - return MkApp(f, (Expr) null); + return MkApp(f, (Expr[]) null); } /** diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index f02301a5d..10f0f9764 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -16,7 +16,6 @@ public class EnumSort extends Sort **/ public FuncDecl[] ConstDecls() { - return _constdecls; } @@ -25,7 +24,6 @@ public class EnumSort extends Sort **/ public Expr[] Consts() { - return _consts; } @@ -34,7 +32,6 @@ public class EnumSort extends Sort **/ public FuncDecl[] TesterDecls() { - return _testerdecls; } @@ -53,12 +50,12 @@ public class EnumSort extends Sort n_constdecls, n_testers)); _constdecls = new FuncDecl[n]; for (int i = 0; i < n; i++) - _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); + _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]); _testerdecls = new FuncDecl[n]; for (int i = 0; i < n; i++) - _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); + _testerdecls[i] = new FuncDecl(ctx, n_testers[i]); _consts = new Expr[n]; for (int i = 0; i < n; i++) - _consts[i] = ctx.MkApp(_constdecls[i], (Expr)null); + _consts[i] = ctx.MkApp(_constdecls[i], (Expr[])null); } }; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 82e5a958b..6ee7e4412 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -159,13 +159,14 @@ public class Quantifier extends BoolExpr .NativeObject())); } else { - setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true - : false, weight, AST.GetNativeObject(quantifierID), AST - .GetNativeObject(skolemID), AST.ArrayLength(patterns), AST - .ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST - .ArrayToNative(noPatterns), AST.ArrayLength(sorts), AST - .ArrayToNative(sorts), Symbol.ArrayToNative(names), body - .NativeObject())); + setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), + (isForall) ? true : false, weight, AST.GetNativeObject(quantifierID), + AST.GetNativeObject(skolemID), + AST.ArrayLength(patterns), AST.ArrayToNative(patterns), + AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), + AST.ArrayLength(sorts), AST.ArrayToNative(sorts), + Symbol.ArrayToNative(names), + body.NativeObject())); } } diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 526329146..fcf6b117a 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -39,10 +39,15 @@ public class Sort extends AST **/ public boolean equals(Object o) { - Sort casted = (Sort) o; - if (casted == null) - return false; - return this == casted; + Sort casted = null; + + try { + casted = Sort.class.cast(o); + } catch (ClassCastException e) { + return false; + } + + return this.NativeObject() == casted.NativeObject(); } /** diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 877fead79..8aeb03ddf 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -104,7 +104,7 @@ public class Z3Object extends IDisposable return null; long[] an = new long[a.length]; for (int i = 0; i < a.length; i++) - an[i] = a[i].NativeObject(); + an[i] = (a[i] == null) ? 0 : a[i].NativeObject(); return an; }