map C++ exceptions to Java exceptions correctly when they are thrown, and give a...

diff --git a/src/cvc4.i b/src/cvc4.i
index b13a555e6a5ddb1ce073ca32ad8a69a038f14452..cb8a7ba067161195c8655fe3b9dc835715a94aa3 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -45,6 +45,8 @@ using namespace CVC4;
 #include <set>
 #include <string>
 #include <ext/hash_map>
+#include <typeinfo>
+#include <cassert>
 
 #include "util/sexpr.h"
 #include "util/exception.h"
@@ -74,12 +76,57 @@ using namespace CVC4;
   try {
     $action
   } catch(CVC4::Exception& e) {
-    ::std::cerr << e << ::std::endl;
-    jclass clazz = jenv->FindClass("java/lang/RuntimeException");
-    jenv->ThrowNew(clazz, e.toString().c_str());
+    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 %{
+  jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/$1_type");
+  assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
+  jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
+  assert(method != NULL && jenv->ExceptionOccurred() == NULL);
+  jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(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/nyu/acsys/$1_type";
+  for(size_t i = name.find("::"); i != std::string::npos; i = name.find("::")) {
+    name.replace(i, 2, "/");
+  }
+  jclass clazz = jenv->FindClass(name.c_str());
+  assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
+  jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
+  assert(method != NULL && jenv->ExceptionOccurred() == NULL);
+  jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(new $1_type($1)), true));
+  assert(t != NULL && jenv->ExceptionOccurred() == NULL);
+  int status = jenv->Throw(t);
+  assert(status == 0);
+%}
+
+%typemap(throws) ModalException = Exception;
+%typemap(throws) OptionException = Exception;
+%typemap(throws) IllegalArgumentException = Exception;
+%typemap(throws) AssertionException = Exception;
+
+%typemap(throws) CVC4::TypeCheckingException = CVC4::Exception;
+%typemap(throws) CVC4::ScopeException = CVC4::Exception;
+%typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
+%typemap(throws) CVC4::AssertionException = CVC4::Exception;
+%typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
+%typemap(throws) CVC4::parser::ParserException = 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"
+%}
+
 %include "java/typemaps.i" // primitive pointers and references
 %include "java/std_string.i" // map std::string to java.lang.String
 %include "java/arrays_java.i" // C arrays to Java arrays