diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-21 13:55:13 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-21 13:55:23 -0400 |
commit | 2deb3a617f068af25457db23eae326dae2bf2ae2 (patch) | |
tree | de865815723d081aeb9a8ddcbc0a386074ed5c63 | |
parent | a0960d8b5bc0897191444b7bcffece8136630917 (diff) |
Safer swig-wrapping for unsigned long long in Java, which will throw an exception if the argument is out of bounds for unsigned long long. Thanks to Steve Siegel for the report.
-rw-r--r-- | src/cvc4.i | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/cvc4.i b/src/cvc4.i index fcd5a8470..cd5896ff3 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -244,6 +244,43 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; } %} +/* Copied (and modified) from java.swg; the standard swig version causes + * negative BigInteger to be interpreted unsigned. Here we throw an + * exception. */ +%typemap(in) unsigned long long { + jclass clazz; + jmethodID mid; + jbyteArray ba; + jbyte* bae; + jsize sz; + int i; + + if (!$input) { + SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "BigInteger null"); + return $null; + } + clazz = JCALL1(GetObjectClass, jenv, $input); + mid = JCALL3(GetMethodID, jenv, clazz, "toByteArray", "()[B"); + ba = (jbyteArray)JCALL2(CallObjectMethod, jenv, $input, mid); + bae = JCALL2(GetByteArrayElements, jenv, ba, 0); + sz = JCALL1(GetArrayLength, jenv, ba); + if((bae[0] & 0x80) != 0) { + SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument must be nonnegative."); + } + jsize test_sz = sz; + if(sz > 1 && bae[0] == 0) { + --test_sz; + } + if(test_sz > sizeof(unsigned long long)) { + SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument out of bounds."); + } + $1 = 0; + for(i=0; i<sz; i++) { + $1 = ($1 << 8) | ($1_type)(unsigned char)bae[i]; + } + JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0); +} + #endif /* SWIGJAVA */ %include "util/integer.i" |