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.

diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
index 0047cc0ecb6257b865db8ae9476a7488eb902c72..76535762d2a58438410fd4087c5d05702828a018 100644 (file)
--- 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 893ea5c95dcd2dc88843d17390793e8b914196c9..6168a8e227b481da665208b1af6f19161b1ba96c 100644 (file)
--- 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 5550974c94ad8ef1e3813a6d22b4f5bc8e236eb6..50c52868bc2830258dd942c29dd3f36043899689 100755 (executable)
--- 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 108ae3cd37bdf0c7dc511783ce7f2bfec73d1492..31f62db5684f84981a32229d4222e258ad82c06d 100644 (file)
--- 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 (file)
index 0000000..d3ddb85
--- /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 (file)
index 0000000..6e255c5
--- /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 (file)
index 0000000..780f75b
--- /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 429d13a63d551aa62da98235537aa4ec962cb397..5098dbc6e46bc1d6a10f00c75f7a9262e16cfd52 100644 (file)
--- 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 6b3598a2fa1b9a42a529f4de03576bfe5319a852..32bdd08873894a39ca1d7d4a0b337ab1d8fa3343 100644 (file)
--- 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