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.

9 files changed, 170 insertions, 76 deletions

diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
index 0047cc0ec..76535762d 100644
--- a/cmake/CVC4Config.cmake.in
+++ b/cmake/CVC4Config.cmake.in
@@ -1,6 +1,7 @@
 @PACKAGE_INIT@
 
 set(CVC4_BINDINGS_JAVA @BUILD_SWIG_BINDINGS_JAVA@)
+set(CVC4_BINDINGS_PYTHON @BUILD_SWIG_BINDINGS_PYTHON@)
 
 if(NOT TARGET CVC4::cvc4)
   include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 893ea5c95..6168a8e22 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -86,3 +86,8 @@ if(TARGET CVC4::cvc4jar)
 
   add_subdirectory(api/java)
 endif()
+
+if(CVC4_BINDINGS_PYTHON)
+  # If legacy Python API has been built
+  add_subdirectory(api/python)
+endif()
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index 5550974c9..50c52868b 100755
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -16,11 +16,9 @@
 ### A simple demonstration of the Python interface.  Compare to the
 ### C++ interface in simple_vc_cxx.cpp; they are quite similar.
 ###
-### To run, use something like:
+### To run from a build directory, use something like:
 ###
-###   ln -s ../builds/src/bindings/python/CVC4.py CVC4.py
-###   ln -s ../builds/src/bindings/python/.libs/CVC4.so _CVC4.so
-###   ./SimpleVC.py
+###   PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py
 ####
 
 import CVC4
@@ -61,4 +59,3 @@ def main():
 
 if __name__ == '__main__':
   sys.exit(main())
-
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 108ae3cd3..31f62db56 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -5,6 +5,7 @@ set(EXAMPLES_API_JAVA
   #CVC4Streams
   Combination
   Datatypes
+  Exceptions
   FloatingPointArith
   HelloWorld
   LinearArith
diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java
new file mode 100644
index 000000000..d3ddb85cc
--- /dev/null
+++ b/examples/api/java/Exceptions.java
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file Exceptions.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Catching CVC4 exceptions via the Java API.
+ **
+ ** A simple demonstration of catching CVC4 execptions via the Java API.
+ **/
+
+import edu.stanford.CVC4.*;
+
+public class Exceptions {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    smt.setOption("produce-models", new SExpr(true));
+
+    // Setting an invalid option
+    try {
+      smt.setOption("non-existing", new SExpr(true));
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+
+    // Creating a term with an invalid type
+    try {
+      Type integer = em.integerType();
+      Expr x = em.mkVar("x", integer);
+      Expr invalidExpr = em.mkExpr(Kind.AND, x, x);
+      smt.checkSat(invalidExpr);
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+
+    // Asking for a model after unsat result
+    try {
+      smt.checkSat(em.mkConst(false));
+      smt.getModel();
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+  }
+}
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
new file mode 100644
index 000000000..6e255c5b1
--- /dev/null
+++ b/examples/api/python/CMakeLists.txt
@@ -0,0 +1,27 @@
+set(EXAMPLES_API_PYTHON
+  exceptions
+)
+
+find_package(PythonInterp REQUIRED)
+
+# Find Python bindings in the corresponding python-*/site-packages directory.
+# Lookup Python module directory and store path in PYTHON_MODULE_PATH.
+execute_process(COMMAND
+                  ${PYTHON_EXECUTABLE} -c
+                    "from distutils.sysconfig import get_python_lib;\
+                     print(get_python_lib(plat_specific=True,\
+                             prefix='${CMAKE_PREFIX_PATH}/../..'))"
+                OUTPUT_VARIABLE PYTHON_MODULE_PATH
+                OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+foreach(example ${EXAMPLES_API_PYTHON})
+  set(example_test example/api/python/${example})
+  add_test(
+    NAME ${example_test}
+    COMMAND
+      "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/api/python/${example}.py"
+  )
+  set_tests_properties(${example_test} PROPERTIES
+    LABELS "example"
+    ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH})
+endforeach()
diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
new file mode 100644
index 000000000..780f75bf7
--- /dev/null
+++ b/examples/api/python/exceptions.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python
+
+#####################
+## \file exceptions.py
+## \verbatim
+## Top contributors (to current version):
+##   Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief Catching CVC4 exceptions with the legacy Python API.
+##
+## A simple demonstration of catching CVC4 execptions with the legacy Python
+## API.
+
+import CVC4
+import sys
+
+
+def main():
+    em = CVC4.ExprManager()
+    smt = CVC4.SmtEngine(em)
+
+    smt.setOption("produce-models", CVC4.SExpr("true"))
+
+    # Setting an invalid option
+    try:
+        smt.setOption("non-existing", CVC4.SExpr("true"))
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    # Creating a term with an invalid type
+    try:
+        integer = em.integerType()
+        x = em.mkVar("x", integer)
+        invalidExpr = em.mkExpr(CVC4.AND, x, x)
+        smt.checkSat(invalidExpr)
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    # Asking for a model after unsat result
+    try:
+        smt.checkSat(em.mkBoolConst(False))
+        smt.getModel()
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    return 0
+
+
+if __name__ == '__main__':
+    sys.exit(main())
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<JavaInputStreamAdapter*> 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, "<init>", "(JZ)V");
-  assert(method != NULL && jenv->ExceptionOccurred() == NULL);
-  jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<uintptr_t>(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, "<init>", "(JZ)V");
-  assert(method != NULL && jenv->ExceptionOccurred() == NULL);
-  jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<uintptr_t>(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