src/bindings/compat/java/include/cvc3/JniUtils.h

   1 #ifndef _java__cvc3__jni_utils_h_
   2 #define _java__cvc3__jni_utils_h_
   3
   4 #include <cassert>
   5 #include <string>
   6 #include <jni.h>
   7 #include <typeinfo>
   8 #include "vcl.h"
   9 #include "hash_map.h"
  10 #include "exception.h"
  11
  12 namespace Java_cvc3_JniUtils {
  13
  14   /// Embedding of c++ objects in java objects
  15
  16   // generic delete function for any type T
  17   template <class T> class DeleteEmbedded {
  18   public:
  19     static void deleteEmbedded(void* cobj) {
  20       delete (T*) cobj;
  21     }
  22   };
  23
  24   typedef void (*TDeleteEmbedded)(void*);
  25
  26
  27   // Encapsulates a c++ object so that:
  28   // - (un)embedding casting is type safe
  29   // - deallocation is automatic (if needed)
  30   // This has probably quit a bit of overhead, because now for each
  31   // wrapper object (even if only a temporary reference) an instance
  32   // of Embedded is created.
  33   // But considering the above two benefits it should be worth it
  34   // because it should simplify maintenance quite a bit,
  35   // as changes in the cvc API should lead to assertion failures
  36   // instead of strange bugs.
  37   class Embedded {
  38   private:
  39     // the actual embedded c++ object,
  40     // as void* to make Embedded independent of its type
  41     void* d_cobj;
  42
  43     // the type info of d_cobj,
  44     // to make sure that later unembeddings are type safe
  45     // actually only needed in debugging, so might be guarded with IF_DEBUG
  46     const std::type_info& d_typeInfo;
  47
  48     // the type correct delete function for d_cobj,
  49     // or NULL if this embedding is merely a reference
  50     // and not responsible for its deallocation
  51     TDeleteEmbedded d_delete;
  52
  53   public:
  54     Embedded(void* cobj, const std::type_info& ti, TDeleteEmbedded del) :
  55       d_cobj(cobj), d_typeInfo(ti), d_delete(del) {
  56         assert(d_cobj != NULL);
  57     }
  58
  59     ~Embedded() {
  60       assert(d_cobj != NULL);
  61       if (d_delete != NULL) d_delete(d_cobj);
  62     }
  63
  64     const void* getCObj() const {
  65       return d_cobj;
  66     }
  67
  68     const std::type_info& getType() const {
  69       return d_typeInfo;
  70     }
  71   };
  72
  73
  74
  75   // embed functions
  76
  77   // embeds a c++ object of type T into a jobject
  78   // by first wrapping it into an Embedded object.
  79   template <class T> jobject embed(JNIEnv* env, T* cobj, const std::type_info& ti,
  80                                    TDeleteEmbedded del) {
  81     DebugAssert(cobj != NULL, "JniUtils::embed: null object given");
  82     Embedded* embedded = new Embedded((void*)cobj, ti, del);
  83     return (jobject)env->NewDirectByteBuffer(embedded, sizeof(Embedded));
  84   }
  85
  86   // embeds a constant reference to a c++ object into a jobject
  87   template <class T> jobject embed_const_ref(JNIEnv* env, const T* cobj) {
  88     DebugAssert(cobj != NULL, "JniUtils::embed_const: null object given");
  89     return embed<T>(env, (T*) cobj, typeid(cobj), NULL);
  90   }
  91
  92   // embeds a mutable reference to a c++ object into a jobject
  93   template <class T> jobject embed_mut_ref(JNIEnv* env, T* cobj) {
  94     DebugAssert(cobj != NULL, "JniUtils::embed_mut_ref: null object given");
  95     return embed<T>(env, (T*) cobj, typeid(cobj), NULL);
  96   }
  97
  98   // embeds a fresh copy of a (probably temporary) c++ object into a jobject
  99   template <class T> jobject embed_copy(JNIEnv* env, const T& cobj) {
 100     DebugAssert(&cobj != NULL, "JniUtils::embed_copy: null object given");
 101     T* copy = new T(cobj);
 102     assert(copy != NULL);
 103     return embed<T>(env, copy, typeid(copy), &DeleteEmbedded<T>::deleteEmbedded);
 104   }
 105
 106   // embeds a c++ object into a jobject,
 107   // and takes over the responsibility to deallocate it
 108   template <class T> jobject embed_own(JNIEnv* env, T* cobj) {
 109     DebugAssert(&cobj != NULL, "JniUtils::embed_own: null object given");
 110     return embed<T>(env, cobj, typeid(cobj), &DeleteEmbedded<T>::deleteEmbedded);
 111   }
 112
 113
 114   // unembed functions
 115
 116   // extract Embedded* from a jobject
 117   Embedded* unembed(JNIEnv* env, jobject jobj);
 118
 119   // extract a constant c++ object of type T from a jobject
 120   template <class T> const T* unembed_const(JNIEnv* env, jobject jobj) {
 121     Embedded* embedded = unembed(env, jobj);
 122     return (const T*) embedded->getCObj();
 123   }
 124
 125   // extract a mutable c++ object of type T from a jobject
 126   template <class T> T* unembed_mut(JNIEnv* env, jobject jobj) {
 127     Embedded* embedded = unembed(env, jobj);
 128     // check that the wrapped object is not const
 129     DebugAssert(embedded->getType() == typeid(T*),
 130                 "JniUtils::unembed_mut: type mismatch");
 131     return (T*) embedded->getCObj();
 132   }
 133
 134
 135   // delete embedded
 136
 137   // delete the Embedded object contained in a jobject,
 138   // and also destruct the wrapped c++ object if necessary.
 139   void deleteEmbedded(JNIEnv* env, jobject jobj);
 140
 141
 142
 143
 144   /// Conversions between c++ and java
 145
 146   // bool
 147   bool toCpp(jboolean j);
 148
 149   // string
 150   jstring toJava(JNIEnv* env, const std::string& cstring);
 151   jstring toJava(JNIEnv* env, const char* cstring);
 152   std::string toCpp(JNIEnv* env, const jstring& string);
 153
 154   // enums
 155   jstring toJava(JNIEnv* env, CVC3::QueryResult result);
 156   jstring toJava(JNIEnv* env, CVC3::FormulaValue result);
 157   jstring toJava(JNIEnv* env, CVC3::InputLanguage result);
 158   CVC3::InputLanguage toCppInputLanguage(JNIEnv* env, const std::string& lang);
 159
 160   // exceptions
 161   void toJava(JNIEnv* env, const CVC3::Exception& e);
 162
 163   // vectors
 164   template <class T> jobjectArray toJavaVCopy(JNIEnv* env, const std::vector<T>& v) {
 165     jobjectArray jarray = (jobjectArray)
 166       env->NewObjectArray(
 167         v.size(),
 168         env->FindClass("java/lang/Object"),
 169         NULL);
 170
 171     for (int i = 0; i < v.size(); ++i) {
 172       env->SetObjectArrayElement(jarray, i, embed_copy<T>(env, v[i]));
 173     }
 174
 175     return jarray;
 176   }
 177
 178   template <class T> jobjectArray toJavaVConstRef(JNIEnv* env, const std::vector<T>& v) {
 179     jobjectArray jarray = (jobjectArray)
 180       env->NewObjectArray(
 181         v.size(),
 182         env->FindClass("java/lang/Object"),
 183         NULL);
 184
 185     for (int i = 0; i < v.size(); ++i) {
 186       env->SetObjectArrayElement(jarray, i, embed_const_ref<T>(env, &v[i]));
 187     }
 188
 189     return jarray;
 190   }
 191
 192   template<class T>
 193     jobjectArray
 194     toJavaVVConstRef(JNIEnv* env, const std::vector<std::vector<T> >& v)
 195     {
 196       jobjectArray jarray = (jobjectArray) env->NewObjectArray(v.size(),
 197           env->FindClass("[Ljava/lang/Object;"), NULL);
 198       for (int i = 0; i < v.size(); ++i)
 199         {
 200           env->SetObjectArrayElement(jarray, i, toJavaVConstRef(env, v[i]));
 201         }
 202       return jarray;
 203     }
 204
 205   template <class T> std::vector<T> toCppV(JNIEnv* env, const jobjectArray& jarray) {
 206     std::vector<T> v;
 207     int length = env->GetArrayLength(jarray);
 208     for (int i = 0; i < length; ++i) {
 209       v.push_back(*unembed_const<T>(env, env->GetObjectArrayElement(jarray, i)));
 210     }
 211     return v;
 212   }
 213
 214   template <class T> std::vector<std::vector<T> > toCppVV(JNIEnv* env, const jobjectArray& jarray) {
 215     std::vector<std::vector<T> > v;
 216     int length = env->GetArrayLength(jarray);
 217     for (int i = 0; i < length; ++i) {
 218       jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i));
 219       v.push_back(toCppV<T>(env, jsub));
 220     }
 221     return v;
 222   }
 223
 224   template <class T> std::vector<std::vector<std::vector<T> > >
 225     toCppVVV(JNIEnv* env, const jobjectArray& jarray) {
 226     std::vector<std::vector<std::vector<T> > > v;
 227     int length = env->GetArrayLength(jarray);
 228     for (int i = 0; i < length; ++i) {
 229       jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i));
 230       v.push_back(toCppVV<T>(env, jsub));
 231     }
 232     return v;
 233   }
 234
 235   // string vectors
 236   std::vector<std::string> toCppV(JNIEnv* env, const jobjectArray& jarray);
 237   std::vector<std::vector<std::string> > toCppVV(JNIEnv* env, const jobjectArray& jarray);
 238   std::vector<std::vector<std::vector<std::string> > > toCppVVV(JNIEnv* env, const jobjectArray& jarray);
 239   jobjectArray toJavaV(JNIEnv* env, const std::vector<std::string>& v);
 240
 241   // primitive vectors
 242   std::vector<bool> toCppV(JNIEnv* env, const jbooleanArray& jarray);
 243
 244
 245   // hash map
 246   template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) {
 247     jobjectArray jarray = (jobjectArray)
 248       env->NewObjectArray(
 249         hm.size() * 2,
 250         env->FindClass("java/lang/Object"),
 251         NULL);
 252
 253     int i = 0;
 254     typename Hash::hash_map<K, V>::const_iterator it;
 255     for (it = hm.begin(); it != hm.end(); ++it) {
 256       assert(i < env->GetArrayLength(jarray));
 257       env->SetObjectArrayElement(jarray, i, embed_copy<K>(env, it->first));
 258       ++i;
 259       assert(i < env->GetArrayLength(jarray));
 260       env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second));
 261       ++i;
 262     }
 263     return jarray;
 264   }
 265
 266   template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) {
 267     jobjectArray jarray = (jobjectArray)
 268       env->NewObjectArray(
 269         hm.size() * 2,
 270         env->FindClass("java/lang/Object"),
 271         NULL);
 272
 273     int i = 0;
 274     typename CVC3::ExprMap<V>::const_iterator it;
 275     for (it = hm.begin(); it != hm.end(); ++it) {
 276       assert(i < env->GetArrayLength(jarray));
 277       env->SetObjectArrayElement(jarray, i, embed_copy<CVC3::Expr>(env, it->first));
 278       ++i;
 279       assert(i < env->GetArrayLength(jarray));
 280       env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second));
 281       ++i;
 282     }
 283     return jarray;
 284   }
 285
 286 }
 287
 288
 289 #endif