From 91402f2060d8c88ccbc724881a996fc0a72c659e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Feb 2013 18:54:44 +0000 Subject: [PATCH] C API: fixed mk_context/mk_context_rc exception behaviour Adjusted .NET/Java APIs accordingly. Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 4 ++-- scripts/update_api.py | 35 +++++++++++++++++++++------------- src/api/api_context.cpp | 4 ++++ src/api/api_util.h | 1 + src/api/java/Context.java | 8 ++++---- 5 files changed, 33 insertions(+), 19 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index a26c21d65..c2743ece8 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2155,7 +2155,7 @@ class JavaExample // But you cannot mix numerals of different sorts // even if the size of their domains are the same: // System.out.println(ctx.mkEq(s1, t1)); - } + } public static void main(String[] args) { @@ -2226,7 +2226,7 @@ class JavaExample Context ctx = new Context(cfg); p.quantifierExample3(ctx); p.quantifierExample4(ctx); - } + } Log.close(); if (Log.isOpen()) diff --git a/scripts/update_api.py b/scripts/update_api.py index 08dd012e3..fa6111482 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -395,8 +395,7 @@ def mk_dotnet(): dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public unsafe class LIB\n') dotnet.write(' {\n') - dotnet.write(' ' - ' const string Z3_DLL_NAME = \"libz3.dll\";\n' + dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' ' \n'); dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') @@ -420,7 +419,8 @@ def mk_dotnet(): dotnet.write(' }\n') -DotnetUnwrapped = [ 'Z3_del_context' ] +NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] +Unwrapped = [ 'Z3_del_context' ] def mk_dotnet_wrappers(): global Type2Str @@ -469,11 +469,15 @@ def mk_dotnet_wrappers(): dotnet.write('a%d' % i) i = i + 1 dotnet.write(');\n'); - if name not in DotnetUnwrapped: - if len(params) > 0 and param_type(params[0]) == CONTEXT: - dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") - dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") - dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") + if name not in Unwrapped: + if name in NULLWrapped: + dotnet.write(" if (r == IntPtr.Zero)\n") + dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n") + else: + if len(params) > 0 and param_type(params[0]) == CONTEXT: + dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") + dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") + dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") if result == STRING: dotnet.write(" return Marshal.PtrToStringAnsi(r);\n") elif result != VOID: @@ -550,7 +554,7 @@ def mk_java(): java_native.write('%s a%d' % (param2java(param), i)) i = i + 1 java_native.write(')') - if len(params) > 0 and param_type(params[0]) == CONTEXT: + if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped: java_native.write(' throws Z3Exception') java_native.write('\n') java_native.write(' {\n') @@ -568,10 +572,15 @@ def mk_java(): java_native.write('a%d' % i) i = i + 1 java_native.write(');\n') - if len(params) > 0 and param_type(params[0]) == CONTEXT: - java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') - java_native.write(' if (err != Z3_error_code.Z3_OK)\n') - java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + if name not in Unwrapped: + if name in NULLWrapped: + java_native.write(" if (res == 0)\n") + java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n") + else: + if len(params) > 0 and param_type(params[0]) == CONTEXT: + java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') + java_native.write(' if (err != Z3_error_code.Z3_OK)\n') + java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') if result != VOID: java_native.write(' return res;\n') java_native.write(' }\n\n') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6106cb6c7..cf179332a 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -419,17 +419,21 @@ namespace api { extern "C" { Z3_context Z3_API Z3_mk_context(Z3_config c) { + Z3_TRY; LOG_Z3_mk_context(c); memory::initialize(UINT_MAX); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); RETURN_Z3(r); + Z3_CATCH_RETURN_NO_HANDLE(0); } Z3_context Z3_API Z3_mk_context_rc(Z3_config c) { + Z3_TRY; LOG_Z3_mk_context_rc(c); memory::initialize(UINT_MAX); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); + Z3_CATCH_RETURN_NO_HANDLE(0); } void Z3_API Z3_del_context(Z3_context c) { diff --git a/src/api/api_util.h b/src/api/api_util.h index c81384f2f..58abf97bf 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -26,6 +26,7 @@ Revision History: #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE } #define Z3_CATCH Z3_CATCH_CORE(return;) #define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;) +#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; } #define CHECK_REF_COUNT(a) (reinterpret_cast(a)->get_ref_count() > 0) #define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a)) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 7a1a404af..3ad136f12 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3053,10 +3053,10 @@ public class Context extends IDisposable // OK. } m_ctx = 0; - } else - /* re-queue the finalizer */ - /* BUG: DRQ's need to be taken over too! */ - new Context(m_ctx, m_refCount); + } + /* + else + CMW: re-queue the finalizer? */ } /**