From c1f8d64f3bc73fe27527046c521c2327e8e310d8 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 9 Jun 2020 05:44:24 -0700 Subject: Language bindings: Enable catching of exceptions (#2813) Fixes #2810. SWIG relies on throw specifiers to determine which exceptions a method can throw. The wrappers generated by SWIG catch those C++ exceptions and turn them into exceptions for the target language. However, we have removed throw specifiers because they have been deprecated in C++11, so SWIG did not know about any of our exceptions. This commit fixes the issue using the %catches directive, declaring that all methods may throw a CVC4::Exception or a general exception. Note: This means that users of the language bindings will just receive a general CVC4::Exception instead of more specific exceptions like TypeExceptions. Given that we are planning to have a single exception type for the new CVC4 API, this seemed like a natural choice. Additionally, the commit (significantly) simplifies the mapping of C++ to Java exceptions and fixes an issue with Python exceptions not inheriting from BaseException. Finally, the commit adds API examples for Java and Python, which demonstrate catching exceptions, and adds Python examples as tests in our build system. --- src/base/exception.i | 4 +++ src/cvc4.i | 87 ++++++++++------------------------------------------ 2 files changed, 20 insertions(+), 71 deletions(-) (limited to 'src') diff --git a/src/base/exception.i b/src/base/exception.i index 429d13a63..5098dbc6e 100644 --- a/src/base/exception.i +++ b/src/base/exception.i @@ -6,6 +6,10 @@ %ignore CVC4::Exception::Exception(const char*); %typemap(javabase) CVC4::Exception "java.lang.RuntimeException"; +// Make sure that the CVC4.Exception class of the Python API inherits from +// BaseException and can be caught +%exceptionclass CVC4::Exception; + %rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; %include "base/exception.h" diff --git a/src/cvc4.i b/src/cvc4.i index 6b3598a2f..32bdd0887 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -1,3 +1,8 @@ +// Declare that all functions in the interface can throw exceptions of type +// CVC4::Exception and exceptions in general. SWIG catches those exceptions and +// turns them into target language exceptions via "throws" typemaps. +%catches(CVC4::Exception,...); + %import "bindings/swig.h" %include "stdint.i" @@ -75,77 +80,17 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; #include "bindings/java_iterator_adapter.h" #include "bindings/java_stream_adapters.h" -%exception %{ - try { - $action - } catch(CVC4::Exception& e) { - std::stringstream ss; - ss << e.what() << ": " << e.getMessage(); - std::string explanation = ss.str(); - SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str()); - } -%} - -// Create a mapping from C++ Exceptions to Java Exceptions. -// This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in. -%typemap(throws) Exception %{ - std::string name = "edu/stanford/CVC4/$1_type"; - /* - size_t i = name.find("::"); - if(i != std::string::npos) { - size_t j = name.rfind("::"); - assert(i <= j); - name.replace(i, j - i + 2, "/"); - } - */ - jclass clazz = jenv->FindClass(name.c_str()); - assert(clazz != NULL && jenv->ExceptionOccurred() == NULL); - jmethodID method = jenv->GetMethodID(clazz, "", "(JZ)V"); - assert(method != NULL && jenv->ExceptionOccurred() == NULL); - jthrowable t = static_cast(jenv->NewObject(clazz, method, reinterpret_cast(new $1_type($1)), true)); - assert(t != NULL && jenv->ExceptionOccurred() == NULL); - int status = jenv->Throw(t); - assert(status == 0); -%} -%typemap(throws) CVC4::Exception %{ - std::string name = "edu/stanford/$1_type"; - size_t i = name.find("::"); - if(i != std::string::npos) { - size_t j = name.rfind("::"); - assert(i <= j); - name.replace(i, j - i + 2, "/"); - } - jclass clazz = jenv->FindClass(name.c_str()); - assert(clazz != NULL && jenv->ExceptionOccurred() == NULL); - jmethodID method = jenv->GetMethodID(clazz, "", "(JZ)V"); - assert(method != NULL && jenv->ExceptionOccurred() == NULL); - jthrowable t = static_cast(jenv->NewObject(clazz, method, reinterpret_cast(new $1_type($1)), true)); - assert(t != NULL && jenv->ExceptionOccurred() == NULL); - int status = jenv->Throw(t); - assert(status == 0); -%} - -%typemap(throws) CVC4::ModalException = CVC4::Exception; -%typemap(throws) CVC4::LogicException = CVC4::Exception; -%typemap(throws) CVC4::OptionException = CVC4::Exception; -%typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception; -%typemap(throws) CVC4::AssertionException = CVC4::Exception; - -%typemap(throws) CVC4::TypeCheckingException = CVC4::Exception; -%typemap(throws) CVC4::ScopeException = CVC4::Exception; -%typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception; -%typemap(throws) IllegalArgumentException = Exception; -%typemap(throws) CVC4::AssertionException = CVC4::Exception; - -// TIM: Really unclear why both of these are required -%typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception; -%typemap(throws) UnsafeInterruptException = CVC4::Exception; -%typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception; - -// Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above -%typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{ -#error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it" -%} +// Map C++ exceptions of type CVC4::Exception to Java exceptions of type +// edu.stanford.CVC4.Exception +// +// As suggested in: +// http://www.swig.org/Doc3.0/SWIGDocumentation.html#Java_exception_typemap +%typemap(throws, throws="edu.stanford.CVC4.Exception") CVC4::Exception { + jclass excep = jenv->FindClass("edu/stanford/CVC4/Exception"); + if (excep) + jenv->ThrowNew(excep, $1.what()); + return $null; +} %include "java/typemaps.i" // primitive pointers and references %include "java/std_string.i" // map std::string to java.lang.String -- cgit v1.2.3