JPF fails on a java.net.URL.openStream call

[Chris Lewis]

Hi all,
I've been trying to get Drools <http://jboss.org/drools> running
within JPF as a possible way of specifying properties.

However, it seems to fail when running a java.net.URL.openStream call,
which I believe is trying to read configuration files from the hard
disk:

====
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native
java.util.zip.ZipFile.initIDs
at java.util.zip.ZipFile.initIDs(no peer)
at java.util.zip.ZipFile.<clinit>(ZipFile.java:54)
at
sun.net.www.protocol.jar.JarFileFactory.get(JarFileFactory.java:55)
at
sun.net.www.protocol.jar.JarURLConnection.connect(JarURLConnection.java:
104)
at
sun.net.www.protocol.jar.JarURLConnection.getInputStream(JarURLConnection.java:
132)
at java.net.URL.openStream(URL.java:1010)
at
org.drools.util.ChainedProperties.loadProperties(ChainedProperties.java:
254)
at
org.drools.util.ChainedProperties.loadProperties(ChainedProperties.java:
225)
at
org.drools.util.ChainedProperties.<init>(ChainedProperties.java:112)
at
org.drools.compiler.PackageBuilderConfiguration.init(PackageBuilderConfiguration.java:
167)
at
org.drools.compiler.PackageBuilderConfiguration.<init>(PackageBuilderConfiguration.java:
159)
at
org.drools.compiler.PackageBuilder.<init>(PackageBuilder.java:210)
at
org.drools.compiler.PackageBuilder.<init>(PackageBuilder.java:143)
at
org.drools.builder.impl.KnowledgeBuilderFactoryServiceImpl.newKnowledgeBuilder(KnowledgeBuilderFactoryServiceImpl.java:
34)
at
org.drools.builder.KnowledgeBuilderFactory.newKnowledgeBuilder(KnowledgeBuilderFactory.java:
47)
at com.cflewis.jpfools.HelloWorld.run(HelloWorld.java:42)
at com.cflewis.jpfools.HelloWorld.main(HelloWorld.java:58)
====

IIRC, JPF requires a closed system, correct? Is there some means of
working around this?

Thank you!
Chris Lewis, UC Santa Cruz

[Chris Lewis]

Addendum: In case it matters, JPF is executing symbolically when it
runs this. I have no need for symbolic checking to be enabled, but
can't see how to turn it off.

Thanks!
Chris

[Chris Lewis]

Oh, I did more reading around the closed system stuff and this looks
like an MJI problem... I'll have a crack at it and let you know how it
goes :)

Chris

[Peter Mehlitz]

we neither have local peers nor model classes for the java.util.zip stuff, so from JPFs perspective this is an UnsatisfiedLinkError for a missing native method.

Reading zips can be forwarded to the host VM and should be straight forward to do, but access of the Zip*Streams would be a whole different story.

-- Peter

[Chris Lewis]

Hi Peter,
Thanks for the reply, hope you had a good Thanksgiving... no rest for
the wicked and/or researchers, huh? :)

Looking at the code for the JarFileFactory, it looks like the import
isn't even used: <http://grepcode.com/file/repository.grepcode.com/
java/root/jdk/openjdk/6-b14/sun/net/www/protocol/jar/
JarFileFactory.java>

I see no reason not to stub out the native peer with null ops. I did
this with the GenPeer tool, and got the source (attached at [1]).
However, I'm not having any success with it.

I added "peer_packages+=;com.cflewis.jpfools.peers" to my HelloWorld
JPF file, but I'm still getting the same error. It looks like JPF
isn't loading it. Is there a quick way to verify whether it is or
isn't being loaded? Is there a really quick+dirty way of trying to
force it to work?

I'm all about quick and dirty this weekend... proving it works is all
I (read: my advisor ;) ) cares about!

Thanks Peter,
Chris Lewis

[1] That source I promised/threatened:

====
package com.cflewis.jpfools.peers;

import gov.nasa.jpf.jvm.MJIEnv;

class JPF_java_util_zip_ZipFile {

public static void $clinit____V (MJIEnv env, int clsObjRef) {

}

public static int getMethod (MJIEnv env, int rcls, long v0) {
int v = (int)0;
return v;
}

public static void close (MJIEnv env, int rcls, long v0) {
}

public static long getSize (MJIEnv env, int rcls, long v0) {
long v = (long)0;
return v;
}

public static long getEntry (MJIEnv env, int rcls, long v0, int
rString1, boolean v2) {
long v = (long)0;
return v;
}

public static void initIDs (MJIEnv env, int rcls) {
}

public static int read (MJIEnv env, int rcls, long v0, long v1, long
v2, int rB3, int v4, int v5) {
int v = (int)0;
return v;
}

public static long open (MJIEnv env, int rcls, int rString0, int v1,
long v2) {
long v = (long)0;
return v;
}

public static int getTotal (MJIEnv env, int rcls, long v0) {
int v = (int)0;
return v;
}

public static void freeEntry (MJIEnv env, int rcls, long v0, long
v1) {
}

public static long getNextEntry (MJIEnv env, int rcls, long v0, int
v1) {
long v = (long)0;
return v;
}

public static long getCSize (MJIEnv env, int rcls, long v0) {
long v = (long)0;
return v;
}

public static int getZipMessage (MJIEnv env, int rcls, long v0) {
int rString = MJIEnv.NULL;
return rString;
}
}
====

[Peter Mehlitz]

+log.info=gov.nasa.jpf.jvm.NativePeer

Make sure your peers are in the vm.classpath. Best way to do that is to have a proper jpf.properties in your project.

While not strictly required if there is no ambiguity, your peer methods should have the signature mangled into the method name (see the existing peers in jpf-core/**/peers)

-- Peter

[Chris Lewis]

OK, it definitely looks like the file isn't being loaded, but I'm
still unsure why. vm.classpath is deprecated, no? I'm using just the
classpath setting.

Here's my JPF file:

====

target=com.cflewis.jpfools.HelloWorld
classpath+=;/Users/cflewis/Documents/Computing/Projects/JPF/jpfools/
target/classes:...[lots of dependencies from Maven here]
peer_packages+=;com.cflewis.jpfools.peers

+log.info=gov.nasa.jpf.jvm.NativePeer

====

My structure of my build folder is:

====

cflewis@coral-reef ~/D/C/P/J/j/t/classes> ls -R
com gov print.drl

./com:
cflewis

./com/cflewis:
jpfools

./com/cflewis/jpfools:
HelloWorld.class Text.class peers

./com/cflewis/jpfools/peers:
JPF_java_util_zip_ZipFile.class

====

I can't see why JPF is still unhappy :(

Thanks Peter for all your help, I owe you a beer next time I'm in
Mountain View :)

Chris

PS. In the interests of completeness, here's the output from JPF right
now.

====

Executing command: java -jar /Users/cflewis/Library/JPF/jpf-core/build/
RunJPF.jar +shell.port=4242 /Users/cflewis/Documents/Computing/
Projects/JPF/jpfools/src/main/java/com/cflewis/jpfools/HelloWorld.jpf
Running Symbolic PathFinder ...
symbolic.dp=choco
symbolic.string_dp_timeout_ms=0
symbolic.string_dp=none
symbolic.choco_time_bound=30000
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Object
[INFO] load MJI method: getClass()Ljava/lang/Class;
[INFO] load MJI method: clone()Ljava/lang/Object;
[INFO] load MJI method: hashCode()I
[INFO] load MJI method: registerNatives()V
[INFO] load MJI method: wait()V
[INFO] load MJI method: wait(J)V
[INFO] load MJI method: notify()V
[INFO] load MJI method: notifyAll()V
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Class
[INFO] load MJI method: getEnumConstants
[INFO] load MJI method: isArray()Z
[INFO] load MJI method: getComponentType()Ljava/lang/Class;
[INFO] load MJI method: isInstance(Ljava/lang/Object;)Z
[INFO] load MJI method: isInterface()Z
[INFO] load MJI method: isAssignableFrom(Ljava/lang/Class;)Z
[INFO] load MJI method: getAnnotations()[Ljava/lang/annotation/
Annotation;
[INFO] load MJI method: getAnnotation(Ljava/lang/Class;)Ljava/lang/
annotation/Annotation;
[INFO] load MJI method: getPrimitiveClass(Ljava/lang/String;)Ljava/
lang/Class;
[INFO] load MJI method: desiredAssertionStatus()Z
[INFO] load MJI method: forName(Ljava/lang/String;)Ljava/lang/Class;
[INFO] load MJI method: newInstance()Ljava/lang/Object;
[INFO] load MJI method: getSuperclass()Ljava/lang/Class;
[INFO] load MJI method: getClassLoader()Ljava/lang/ClassLoader;
[INFO] load MJI method: getDeclaredMethod(Ljava/lang/String;[Ljava/
lang/Class;)Ljava/lang/reflect/Method;
[INFO] load MJI method: getDeclaredConstructor([Ljava/lang/
Class;)Ljava/lang/reflect/Constructor;
[INFO] load MJI method: getMethod(Ljava/lang/String;[Ljava/lang/
Class;)Ljava/lang/reflect/Method;
[INFO] load MJI method: getMethods()[Ljava/lang/reflect/Method;
[INFO] load MJI method: getDeclaredMethods()[Ljava/lang/reflect/
Method;
[INFO] load MJI method: getConstructors()[Ljava/lang/reflect/
Constructor;
[INFO] load MJI method: getDeclaredConstructors()[Ljava/lang/reflect/
Constructor;
[INFO] load MJI method: getConstructor([Ljava/lang/Class;)Ljava/lang/
reflect/Constructor;
[INFO] load MJI method: getDeclaredFields()[Ljava/lang/reflect/Field;
[INFO] load MJI method: getDeclaredField(Ljava/lang/String;)Ljava/lang/
reflect/Field;
[INFO] load MJI method: getField(Ljava/lang/String;)Ljava/lang/reflect/
Field;
[INFO] load MJI method: getModifiers()I
[INFO] load MJI method: getInterfaces()[Ljava/lang/Class;
[INFO] load MJI method: getByteArrayFromResourceStream
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_ClassLoader
[INFO] load MJI method: init0()V
[INFO] load MJI method: getResourcePath(Ljava/lang/String;)Ljava/lang/
String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Character
[INFO] load MJI method: isDefined(C)Z
[INFO] load MJI method: isDigit(C)Z
[INFO] load MJI method: isISOControl(C)Z
[INFO] load MJI method: isIdentifierIgnorable(C)Z
[INFO] load MJI method: isJavaIdentifierPart(C)Z
[INFO] load MJI method: isJavaIdentifierStart(C)Z
[INFO] load MJI method: isJavaLetterOrDigit(C)Z
[INFO] load MJI method: isJavaLetter(C)Z
[INFO] load MJI method: isLetterOrDigit(C)Z
[INFO] load MJI method: isLetter(C)Z
[INFO] load MJI method: isLowerCase(C)Z
[INFO] load MJI method: getNumericValue(C)I
[INFO] load MJI method: isSpaceChar(C)Z
[INFO] load MJI method: isSpace(C)Z
[INFO] load MJI method: isTitleCase(C)Z
[INFO] load MJI method: getType(C)I
[INFO] load MJI method: isUnicodeIdentifierPart(C)Z
[INFO] load MJI method: isUnicodeIdentifierStart(C)Z
[INFO] load MJI method: isUpperCase(C)Z
[INFO] load MJI method: isWhitespace(C)Z
[INFO] load MJI method: <clinit>
[INFO] load MJI method: digit(CI)I
[INFO] load MJI method: forDigit(II)C
[INFO] load MJI method: toLowerCase(C)C
[INFO] load MJI method: toTitleCase(C)C
[INFO] load MJI method: toUpperCase(C)C
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Short
[INFO] load MJI method: parseShort(Ljava/lang/String;)S
[INFO] load MJI method: parseShort(Ljava/lang/String;I)S
[INFO] load MJI method: toString(S)Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Integer
[INFO] load MJI method: parseInt(Ljava/lang/String;)I
[INFO] load MJI method: parseInt(Ljava/lang/String;I)I
[INFO] load MJI method: toBinaryString(I)Ljava/lang/String;
[INFO] load MJI method: toHexString(I)Ljava/lang/String;
[INFO] load MJI method: toOctalString(I)Ljava/lang/String;
[INFO] load MJI method: toString(I)Ljava/lang/String;
[INFO] load MJI method: toString(II)Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Long
[INFO] load MJI method: parseLong(Ljava/lang/String;I)J
[INFO] load MJI method: parseLong(Ljava/lang/String;)J
[INFO] load MJI method: toBinaryString(J)Ljava/lang/String;
[INFO] load MJI method: toHexString(J)Ljava/lang/String;
[INFO] load MJI method: toOctalString(J)Ljava/lang/String;
[INFO] load MJI method: toString(J)Ljava/lang/String;
[INFO] load MJI method: toString(JI)Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Float
[INFO] load MJI method: floatToIntBits(F)I
[INFO] load MJI method: floatToRawIntBits(F)I
[INFO] load MJI method: intBitsToFloat(I)F
[INFO] load MJI method: isInfinite(F)Z
[INFO] load MJI method: isNaN(F)Z
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Double
[INFO] load MJI method: doubleToLongBits(D)J
[INFO] load MJI method: doubleToRawLongBits(D)J
[INFO] load MJI method: longBitsToDouble(J)D
[INFO] load MJI method: toString(D)Ljava/lang/String;
[INFO] load MJI method: isInfinite(D)Z
[INFO] load MJI method: isNaN(D)Z
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_String
[INFO] load MJI method: hashCode()I
[INFO] load MJI method: intern()Ljava/lang/String;
[INFO] load MJI method: equals(Ljava/lang/Object;)Z
[INFO] load MJI method: toCharArray()[C
[INFO] load MJI method: indexOf(I)I
[INFO] load MJI method: matches(Ljava/lang/String;)Z
[INFO] load MJI method: format(Ljava/lang/String;[Ljava/lang/
Object;)Ljava/lang/String;
[INFO] load MJI method: getBytes(Ljava/lang/String;)[B
[INFO] load MJI method: split(Ljava/lang/String;)[Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Thread
[INFO] load MJI method: isAlive()Z
[INFO] load MJI method: setDaemon0(Z)V
[INFO] load MJI method: setName0(Ljava/lang/String;)V
[INFO] load MJI method: setPriority0(I)V
[INFO] load MJI method: countStackFrames()I
[INFO] load MJI method: currentThread()Ljava/lang/Thread;
[INFO] load MJI method: holdsLock(Ljava/lang/Object;)Z
[INFO] load MJI method: init0(Ljava/lang/ThreadGroup;Ljava/lang/
Runnable;Ljava/lang/String;J)V
[INFO] load MJI method: interrupt()V
[INFO] load MJI method: isInterrupted()Z
[INFO] load MJI method: interrupted()Z
[INFO] load MJI method: start()V
[INFO] load MJI method: yield()V
[INFO] load MJI method: sleep(JI)V
[INFO] load MJI method: suspend()V
[INFO] load MJI method: resume()V
[INFO] load MJI method: join()V
[INFO] load MJI method: join(J)V
[INFO] load MJI method: join(JI)V
[INFO] load MJI method: getId()J
[INFO] load MJI method: getState0()I
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_System
[INFO] load MJI method: arraycopy(Ljava/lang/Object;ILjava/lang/
Object;II)V
[INFO] load MJI method: getenv(Ljava/lang/String;)Ljava/lang/String;
[INFO] load MJI method: createSystemOut()Ljava/io/PrintStream;
[INFO] load MJI method: createSystemErr()Ljava/io/PrintStream;
[INFO] load MJI method: getKeyValuePairs()[Ljava/lang/String;
[INFO] load MJI method: currentTimeMillis()J
[INFO] load MJI method: nanoTime()J
[INFO] load MJI method: exit(I)V
[INFO] load MJI method: gc()V
[INFO] load MJI method: identityHashCode(Ljava/lang/Object;)I
JavaPathfinder v5.x - (C) RIACS/NASA Ames Research Center


====================================================== system under
test
application: com/cflewis/jpfools/HelloWorld.java

====================================================== search started:
11/27/10 2:15 PM
[INFO] load peer:
gov.nasa.jpf.jvm.JPF_gov_nasa_jpf_ConsoleOutputStream
[INFO] load MJI method: <init>()V
[INFO] load MJI method: print(C)V
[INFO] load MJI method: print(D)V
[INFO] load MJI method: print(F)V
[INFO] load MJI method: print(I)V
[INFO] load MJI method: print(J)V
[INFO] load MJI method: print(Ljava/lang/String;)V
[INFO] load MJI method: print(Z)V
[INFO] load MJI method: println()V
[INFO] load MJI method: println(C)V
[INFO] load MJI method: println(D)V
[INFO] load MJI method: println(F)V
[INFO] load MJI method: println(I)V
[INFO] load MJI method: println(J)V
[INFO] load MJI method: println(Ljava/lang/String;)V
[INFO] load MJI method: write(I)V
[INFO] load MJI method: write([BII)V
[INFO] load MJI method: println(Z)V
[INFO] load MJI method: printf(Ljava/lang/String;[Ljava/lang/
Object;)Ljava/io/PrintStream;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_sun_misc_Unsafe
[INFO] load MJI method: objectFieldOffset(Ljava/lang/reflect/Field;)J
[INFO] load MJI method: fieldOffset(Ljava/lang/reflect/Field;)I
[INFO] load MJI method: compareAndSwapObject(Ljava/lang/Object;JLjava/
lang/Object;Ljava/lang/Object;)Z
[INFO] load MJI method: compareAndSwapInt(Ljava/lang/Object;JII)Z
[INFO] load MJI method: compareAndSwapLong(Ljava/lang/Object;JJJ)Z
[INFO] load MJI method: park(ZJ)V
[INFO] load MJI method: unpark(Ljava/lang/Object;)V
[INFO] load MJI method: ensureClassInitialized(Ljava/lang/Class;)V
[INFO] load MJI method: getObject(Ljava/lang/Object;J)Ljava/lang/
Object;
[INFO] load MJI method: putObject(Ljava/lang/Object;JLjava/lang/
Object;)V
[INFO] load MJI method: putOrderedObject(Ljava/lang/Object;JLjava/lang/
Object;)V
[INFO] load MJI method: getBoolean(Ljava/lang/Object;J)Z
[INFO] load MJI method: putBoolean(Ljava/lang/Object;JZ)V
[INFO] load MJI method: getByte(Ljava/lang/Object;J)B
[INFO] load MJI method: putByte(Ljava/lang/Object;JB)V
[INFO] load MJI method: getChar(Ljava/lang/Object;J)C
[INFO] load MJI method: putChar(Ljava/lang/Object;JC)V
[INFO] load MJI method: getShort(Ljava/lang/Object;J)S
[INFO] load MJI method: putShort(Ljava/lang/Object;JS)V
[INFO] load MJI method: getInt(Ljava/lang/Object;J)I
[INFO] load MJI method: putInt(Ljava/lang/Object;JI)V
[INFO] load MJI method: putOrderedInt(Ljava/lang/Object;JI)V
[INFO] load MJI method: getFloat(Ljava/lang/Object;J)F
[INFO] load MJI method: putFloat(Ljava/lang/Object;JF)V
[INFO] load MJI method: getLong(Ljava/lang/Object;J)J
[INFO] load MJI method: putLong(Ljava/lang/Object;JJ)V
[INFO] load MJI method: putOrderedLong(Ljava/lang/Object;JJ)V
[INFO] load MJI method: getDouble(Ljava/lang/Object;J)D
[INFO] load MJI method: putDouble(Ljava/lang/Object;JD)V
[INFO] load MJI method: arrayBaseOffset(Ljava/lang/Class;)I
[INFO] load MJI method: arrayIndexScale(Ljava/lang/Class;)I
Hello
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_reflect_Field
[INFO] load MJI method: getAnnotations()[Ljava/lang/annotation/
Annotation;
[INFO] load MJI method: getAnnotation(Ljava/lang/Class;)Ljava/lang/
annotation/Annotation;
[INFO] load MJI method: getModifiers()I
[INFO] load MJI method: getName()Ljava/lang/String;
[INFO] load MJI method: getDeclaringClass()Ljava/lang/Class;
[INFO] load MJI method: getType()Ljava/lang/Class;
[INFO] load MJI method: getBoolean(Ljava/lang/Object;)Z
[INFO] load MJI method: getByte(Ljava/lang/Object;)B
[INFO] load MJI method: getChar(Ljava/lang/Object;)C
[INFO] load MJI method: getShort(Ljava/lang/Object;)S
[INFO] load MJI method: getInt(Ljava/lang/Object;)I
[INFO] load MJI method: getLong(Ljava/lang/Object;)J
[INFO] load MJI method: getFloat(Ljava/lang/Object;)F
[INFO] load MJI method: getDouble(Ljava/lang/Object;)D
[INFO] load MJI method: setBoolean(Ljava/lang/Object;Z)V
[INFO] load MJI method: setByte(Ljava/lang/Object;B)V
[INFO] load MJI method: setChar(Ljava/lang/Object;C)V
[INFO] load MJI method: setShort(Ljava/lang/Object;S)V
[INFO] load MJI method: setInt(Ljava/lang/Object;I)V
[INFO] load MJI method: setLong(Ljava/lang/Object;J)V
[INFO] load MJI method: setFloat(Ljava/lang/Object;F)V
[INFO] load MJI method: setDouble(Ljava/lang/Object;D)V
[INFO] load MJI method: get(Ljava/lang/Object;)Ljava/lang/Object;
[INFO] load MJI method: isSynthetic()Z
[INFO] load MJI method: set(Ljava/lang/Object;Ljava/lang/Object;)V
[INFO] load peer: gov.nasa.jpf.symbc.JPF_java_lang_Math
[INFO] load MJI method: sqrt(D)D
[INFO] load MJI method: random()D
[INFO] load MJI method: round(D)J
[INFO] load MJI method: exp(D)D
[INFO] load MJI method: asin(D)D
[INFO] load MJI method: acos(D)D
[INFO] load MJI method: atan(D)D
[INFO] load MJI method: atan2(DD)D
[INFO] load MJI method: log(D)D
[INFO] load MJI method: log10(D)D
[INFO] load MJI method: tan(D)D
[INFO] load MJI method: sin(D)D
[INFO] load MJI method: cos(D)D
[INFO] load MJI method: pow(DD)D
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_StringBuilder
[INFO] load MJI method: toString()Ljava/lang/String;
[INFO] load MJI method: append(Ljava/lang/String;)Ljava/lang/
StringBuilder;
[INFO] load MJI method: append(I)Ljava/lang/StringBuilder;
[INFO] load MJI method: append(F)Ljava/lang/StringBuilder;
[INFO] load MJI method: append(D)Ljava/lang/StringBuilder;
[INFO] load MJI method: append(J)Ljava/lang/StringBuilder;
[INFO] load MJI method: append(Z)Ljava/lang/StringBuilder;
[INFO] load MJI method: append(C)Ljava/lang/StringBuilder;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_io_File
[INFO] load MJI method: getAbsolutePath()Ljava/lang/String;
[INFO] load MJI method: getCanonicalPath()Ljava/lang/String;
[INFO] load MJI method: getURLSpec()Ljava/lang/String;
[INFO] load MJI method: getURISpec()Ljava/lang/String;
[INFO] load MJI method: exists()Z
[INFO] load MJI method: isDirectory()Z
[INFO] load MJI method: isFile()Z
[INFO] load MJI method: delete()Z
[INFO] load MJI method: length()J
[INFO] load MJI method: canRead()Z
[INFO] load MJI method: list()[Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_lang_Throwable
[INFO] load MJI method: toString()Ljava/lang/String;
[INFO] load MJI method: createStackTrace()[Ljava/lang/
StackTraceElement;
[INFO] load MJI method: fillInStackTrace()Ljava/lang/Throwable;
[INFO] load MJI method: printStackTrace()V
[INFO] load MJI method: getStackTraceAsString()Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_util_Locale
[INFO] load MJI method: getDisplayName(Ljava/util/Locale;)Ljava/lang/
String;
[INFO] load MJI method: getDisplayVariant(Ljava/util/Locale;)Ljava/
lang/String;
[INFO] load MJI method: getDisplayCountry(Ljava/util/Locale;)Ljava/
lang/String;
[INFO] load MJI method: getDisplayLanguage(Ljava/util/Locale;)Ljava/
lang/String;
[INFO] load MJI method: getISO3Country()Ljava/lang/String;
[INFO] load MJI method: getISO3Language()Ljava/lang/String;
[INFO] load MJI method: getISOCountries()[Ljava/lang/String;
[INFO] load MJI method: getISOLanguages()[Ljava/lang/String;
[INFO] load peer: gov.nasa.jpf.jvm.JPF_java_io_ObjectStreamClass
[INFO] load MJI method: initNative()V
[INFO] load MJI method: hasStaticInitializer(Ljava/lang/Class;)Z
[INFO] load peer: gov.nasa.jpf.jvm.JPF_sun_reflect_ReflectionFactory
[INFO] load MJI method: newConstructorForSerialization(Ljava/lang/
Class;Ljava/lang/reflect/Constructor;)Ljava/lang/reflect/Constructor;

====================================================== error #1

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native
java.util.zip.ZipFile.initIDs
at java.util.zip.ZipFile.initIDs(no peer)
at java.util.zip.ZipFile.<clinit>(ZipFile.java:54)
at
sun.net.www.protocol.jar.JarFileFactory.get(JarFileFactory.java:55)
at
sun.net.www.protocol.jar.JarURLConnection.connect(JarURLConnection.java:
104)
at
sun.net.www.protocol.jar.JarURLConnection.getInputStream(JarURLConnection.java:
132)
at java.net.URL.openStream(URL.java:1010)
at
org.drools.util.ChainedProperties.loadProperties(ChainedProperties.java:
254)
at
org.drools.util.ChainedProperties.loadProperties(ChainedProperties.java:
225)
at
org.drools.util.ChainedProperties.<init>(ChainedProperties.java:112)
at

org.drools.compiler.PackageBuilderConfiguration.init(PackageBuilderConfiguration.java:
167)
at
org.drools.compiler.PackageBuilderConfiguration.<init>(PackageBuilderConfiguration.java:

159)
at
org.drools.compiler.PackageBuilder.<init>(PackageBuilder.java:210)
at
org.drools.compiler.PackageBuilder.<init>(PackageBuilder.java:143)
at

org.drools.builder.impl.KnowledgeBuilderFactoryServiceImpl.newKnowledgeBuilder(KnowledgeBuilderFactoryServiceImpl.java:
34)
at
org.drools.builder.KnowledgeBuilderFactory.newKnowledgeBuilder(KnowledgeBuilderFactory.java:
47)

at com.cflewis.jpfools.HelloWorld.run(HelloWorld.java:40)
at com.cflewis.jpfools.HelloWorld.main(HelloWorld.java:56)


====================================================== snapshot #1
thread
index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0,suspendCount=0
owned locks:java.lang.Class@1175
call stack:

at java.util.zip.ZipFile.<clinit>(ZipFile.java:54)
at
sun.net.www.protocol.jar.JarFileFactory.get(JarFileFactory.java:55)
at
sun.net.www.protocol.jar.JarURLConnection.connect(JarURLConnection.java:
104)
at
sun.net.www.protocol.jar.JarURLConnection.getInputStream(JarURLConnection.java:
132)
at java.net.URL.openStream(URL.java:1010)
at
org.drools.util.ChainedProperties.loadProperties(ChainedProperties.java:
254)
at
org.drools.util.ChainedProperties.loadProperties(ChainedProperties.java:
225)
at
org.drools.util.ChainedProperties.<init>(ChainedProperties.java:112)
at

org.drools.compiler.PackageBuilderConfiguration.init(PackageBuilderConfiguration.java:
167)
at
org.drools.compiler.PackageBuilderConfiguration.<init>(PackageBuilderConfiguration.java:

159)
at
org.drools.compiler.PackageBuilder.<init>(PackageBuilder.java:210)
at
org.drools.compiler.PackageBuilder.<init>(PackageBuilder.java:143)
at

org.drools.builder.impl.KnowledgeBuilderFactoryServiceImpl.newKnowledgeBuilder(KnowledgeBuilderFactoryServiceImpl.java:
34)
at
org.drools.builder.KnowledgeBuilderFactory.newKnowledgeBuilder(KnowledgeBuilderFactory.java:
47)

at com.cflewis.jpfools.HelloWorld.run(HelloWorld.java:40)
at com.cflewis.jpfools.HelloWorld.main(HelloWorld.java:56)


====================================================== results
error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
"java.lang.UnsatisfiedLinkError: cannot find native..."

====================================================== statistics
elapsed time: 0:00:03
states: new=0, visited=1, backtracked=0, end=0
search: maxDepth=0, constraints=0
choice generators: thread=1, data=0
heap: gc=0, new=1174, free=0
instructions: 40921
max memory: 81MB
loaded code: classes=189, methods=2727

====================================================== search
finished: 11/27/10 2:16 PM

[Peter Mehlitz]

sorry, I meant native_classpath of course. Peers have to be located by the host VM

Please don't post large logs to the mailing list

-- Peter

[Chris Lewis]

My apologies.

This was exactly what was required to get it working, but
unfortunately stubbing out the zip class with nulls didn't work...
it's actually trying to call methods on it, then dying with NPEs :
( Goodness knows why it needs to use that class at all, all it's doing
is opening a Java URL, why does it need to have that functionality?

Earlier you mentioned: "Reading zips can be forwarded to the host VM

and should be straight forward to do, but access of the Zip*Streams
would be a whole different story."

How would one forward reading zips to the host VM?

Thanks
Chris

[Peter Mehlitz]

like the File & FileDescriptor models/peers. If you have library calls that just return objects, you can create those on the native side by using the host VM to get the host VM object and then translate it into JPF space.

-- Peter