diff options
Diffstat (limited to 'src/bindings/compat/java/include/cvc3/JniUtils.h')
-rw-r--r-- | src/bindings/compat/java/include/cvc3/JniUtils.h | 289 |
1 files changed, 289 insertions, 0 deletions
diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h new file mode 100644 index 000000000..3ce1e9224 --- /dev/null +++ b/src/bindings/compat/java/include/cvc3/JniUtils.h @@ -0,0 +1,289 @@ +#ifndef _java__cvc3__jni_utils_h_ +#define _java__cvc3__jni_utils_h_ + +#include <cassert> +#include <string> +#include <jni.h> +#include <typeinfo> +#include "vcl.h" +#include "hash_map.h" +#include "exception.h" + +namespace Java_cvc3_JniUtils { + + /// Embedding of c++ objects in java objects + + // generic delete function for any type T + template <class T> class DeleteEmbedded { + public: + static void deleteEmbedded(void* cobj) { + delete (T*) cobj; + } + }; + + typedef void (*TDeleteEmbedded)(void*); + + + // Encapsulates a c++ object so that: + // - (un)embedding casting is type safe + // - deallocation is automatic (if needed) + // This has probably quit a bit of overhead, because now for each + // wrapper object (even if only a temporary reference) an instance + // of Embedded is created. + // But considering the above two benefits it should be worth it + // because it should simplify maintenance quite a bit, + // as changes in the cvc API should lead to assertion failures + // instead of strange bugs. + class Embedded { + private: + // the actual embedded c++ object, + // as void* to make Embedded independent of its type + void* d_cobj; + + // the type info of d_cobj, + // to make sure that later unembeddings are type safe + // actually only needed in debugging, so might be guarded with IF_DEBUG + const std::type_info& d_typeInfo; + + // the type correct delete function for d_cobj, + // or NULL if this embedding is merely a reference + // and not responsible for its deallocation + TDeleteEmbedded d_delete; + + public: + Embedded(void* cobj, const std::type_info& ti, TDeleteEmbedded del) : + d_cobj(cobj), d_typeInfo(ti), d_delete(del) { + assert(d_cobj != NULL); + } + + ~Embedded() { + assert(d_cobj != NULL); + if (d_delete != NULL) d_delete(d_cobj); + } + + const void* getCObj() const { + return d_cobj; + } + + const std::type_info& getType() const { + return d_typeInfo; + } + }; + + + + // embed functions + + // embeds a c++ object of type T into a jobject + // by first wrapping it into an Embedded object. + template <class T> jobject embed(JNIEnv* env, T* cobj, const std::type_info& ti, + TDeleteEmbedded del) { + DebugAssert(cobj != NULL, "JniUtils::embed: null object given"); + Embedded* embedded = new Embedded((void*)cobj, ti, del); + return (jobject)env->NewDirectByteBuffer(embedded, sizeof(Embedded)); + } + + // embeds a constant reference to a c++ object into a jobject + template <class T> jobject embed_const_ref(JNIEnv* env, const T* cobj) { + DebugAssert(cobj != NULL, "JniUtils::embed_const: null object given"); + return embed<T>(env, (T*) cobj, typeid(cobj), NULL); + } + + // embeds a mutable reference to a c++ object into a jobject + template <class T> jobject embed_mut_ref(JNIEnv* env, T* cobj) { + DebugAssert(cobj != NULL, "JniUtils::embed_mut_ref: null object given"); + return embed<T>(env, (T*) cobj, typeid(cobj), NULL); + } + + // embeds a fresh copy of a (probably temporary) c++ object into a jobject + template <class T> jobject embed_copy(JNIEnv* env, const T& cobj) { + DebugAssert(&cobj != NULL, "JniUtils::embed_copy: null object given"); + T* copy = new T(cobj); + assert(copy != NULL); + return embed<T>(env, copy, typeid(copy), &DeleteEmbedded<T>::deleteEmbedded); + } + + // embeds a c++ object into a jobject, + // and takes over the responsibility to deallocate it + template <class T> jobject embed_own(JNIEnv* env, T* cobj) { + DebugAssert(&cobj != NULL, "JniUtils::embed_own: null object given"); + return embed<T>(env, cobj, typeid(cobj), &DeleteEmbedded<T>::deleteEmbedded); + } + + + // unembed functions + + // extract Embedded* from a jobject + Embedded* unembed(JNIEnv* env, jobject jobj); + + // extract a constant c++ object of type T from a jobject + template <class T> const T* unembed_const(JNIEnv* env, jobject jobj) { + Embedded* embedded = unembed(env, jobj); + return (const T*) embedded->getCObj(); + } + + // extract a mutable c++ object of type T from a jobject + template <class T> T* unembed_mut(JNIEnv* env, jobject jobj) { + Embedded* embedded = unembed(env, jobj); + // check that the wrapped object is not const + DebugAssert(embedded->getType() == typeid(T*), + "JniUtils::unembed_mut: type mismatch"); + return (T*) embedded->getCObj(); + } + + + // delete embedded + + // delete the Embedded object contained in a jobject, + // and also destruct the wrapped c++ object if necessary. + void deleteEmbedded(JNIEnv* env, jobject jobj); + + + + + /// Conversions between c++ and java + + // bool + bool toCpp(jboolean j); + + // string + jstring toJava(JNIEnv* env, const std::string& cstring); + jstring toJava(JNIEnv* env, const char* cstring); + std::string toCpp(JNIEnv* env, const jstring& string); + + // enums + jstring toJava(JNIEnv* env, CVC3::QueryResult result); + jstring toJava(JNIEnv* env, CVC3::FormulaValue result); + jstring toJava(JNIEnv* env, CVC3::InputLanguage result); + CVC3::InputLanguage toCppInputLanguage(JNIEnv* env, const std::string& lang); + + // exceptions + void toJava(JNIEnv* env, const CVC3::Exception& e); + + // vectors + template <class T> jobjectArray toJavaVCopy(JNIEnv* env, const std::vector<T>& v) { + jobjectArray jarray = (jobjectArray) + env->NewObjectArray( + v.size(), + env->FindClass("java/lang/Object"), + NULL); + + for (int i = 0; i < v.size(); ++i) { + env->SetObjectArrayElement(jarray, i, embed_copy<T>(env, v[i])); + } + + return jarray; + } + + template <class T> jobjectArray toJavaVConstRef(JNIEnv* env, const std::vector<T>& v) { + jobjectArray jarray = (jobjectArray) + env->NewObjectArray( + v.size(), + env->FindClass("java/lang/Object"), + NULL); + + for (int i = 0; i < v.size(); ++i) { + env->SetObjectArrayElement(jarray, i, embed_const_ref<T>(env, &v[i])); + } + + return jarray; + } + + template<class T> + jobjectArray + toJavaVVConstRef(JNIEnv* env, const std::vector<std::vector<T> >& v) + { + jobjectArray jarray = (jobjectArray) env->NewObjectArray(v.size(), + env->FindClass("[Ljava/lang/Object;"), NULL); + for (int i = 0; i < v.size(); ++i) + { + env->SetObjectArrayElement(jarray, i, toJavaVConstRef(env, v[i])); + } + return jarray; + } + + template <class T> std::vector<T> toCppV(JNIEnv* env, const jobjectArray& jarray) { + std::vector<T> v; + int length = env->GetArrayLength(jarray); + for (int i = 0; i < length; ++i) { + v.push_back(*unembed_const<T>(env, env->GetObjectArrayElement(jarray, i))); + } + return v; + } + + template <class T> std::vector<std::vector<T> > toCppVV(JNIEnv* env, const jobjectArray& jarray) { + std::vector<std::vector<T> > v; + int length = env->GetArrayLength(jarray); + for (int i = 0; i < length; ++i) { + jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i)); + v.push_back(toCppV<T>(env, jsub)); + } + return v; + } + + template <class T> std::vector<std::vector<std::vector<T> > > + toCppVVV(JNIEnv* env, const jobjectArray& jarray) { + std::vector<std::vector<std::vector<T> > > v; + int length = env->GetArrayLength(jarray); + for (int i = 0; i < length; ++i) { + jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i)); + v.push_back(toCppVV<T>(env, jsub)); + } + return v; + } + + // string vectors + std::vector<std::string> toCppV(JNIEnv* env, const jobjectArray& jarray); + std::vector<std::vector<std::string> > toCppVV(JNIEnv* env, const jobjectArray& jarray); + std::vector<std::vector<std::vector<std::string> > > toCppVVV(JNIEnv* env, const jobjectArray& jarray); + jobjectArray toJavaV(JNIEnv* env, const std::vector<std::string>& v); + + // primitive vectors + std::vector<bool> toCppV(JNIEnv* env, const jbooleanArray& jarray); + + + // hash map + template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) { + jobjectArray jarray = (jobjectArray) + env->NewObjectArray( + hm.size() * 2, + env->FindClass("java/lang/Object"), + NULL); + + int i = 0; + typename Hash::hash_map<K, V>::const_iterator it; + for (it = hm.begin(); it != hm.end(); ++it) { + assert(i < env->GetArrayLength(jarray)); + env->SetObjectArrayElement(jarray, i, embed_copy<K>(env, it->first)); + ++i; + assert(i < env->GetArrayLength(jarray)); + env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second)); + ++i; + } + return jarray; + } + + template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) { + jobjectArray jarray = (jobjectArray) + env->NewObjectArray( + hm.size() * 2, + env->FindClass("java/lang/Object"), + NULL); + + int i = 0; + typename CVC3::ExprMap<V>::const_iterator it; + for (it = hm.begin(); it != hm.end(); ++it) { + assert(i < env->GetArrayLength(jarray)); + env->SetObjectArrayElement(jarray, i, embed_copy<CVC3::Expr>(env, it->first)); + ++i; + assert(i < env->GetArrayLength(jarray)); + env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second)); + ++i; + } + return jarray; + } + +} + + +#endif |