Understand output of JBSE on provided example

[danglotb]

Hi,

I tried to run JBSE on the example provided, but my output is a little bit different from the README.

Also, I do not understand the output that I obtain:

This is the Java Bytecode Symbolic Executor's Run Tool (JBSE v.0.8.0-SNAPSHOT).
Connecting to Z3 at ../z3/bin/z3.
Starting symbolic execution of method smalldemos/ifx/IfExample:(I)V:m at Fri Jan 05 12:39:02 CET 2018.
.1[50591] 
Leaf state, raised exception: Object[2556]
Path condition: 
    {R0} == Object[0] (fresh) &&
    pre_init(smalldemos/ifx/IfExample) &&
    pre_init(java/lang/IllegalArgumentException) &&
    pre_init(java/lang/IllegalMonitorStateException) &&
    pre_init(java/lang/StackOverflowError) &&
    pre_init(java/lang/ArithmeticException) &&
    pre_init(java/lang/ArrayStoreException) &&
    pre_init(java/lang/ClassCastException) &&
    pre_init(java/lang/NullPointerException) &&
    pre_init(java/lang/OutOfMemoryError) &&
    pre_init(java/lang/VirtualMachineError) &&
    pre_init(java/lang/Error) &&
    pre_init(java/lang/ref/FinalReference) &&
    pre_init(java/lang/ref/Finalizer$FinalizerThread) &&
    pre_init(java/lang/ref/SoftReference) &&
    pre_init(java/lang/Terminator$1) &&
    pre_init(sun/misc/NativeSignalHandler) &&
    pre_init(sun/misc/OSEnvironment) &&
    pre_init(java/lang/System$2) &&
    pre_init(sun/misc/Launcher$ExtClassLoader) &&
    pre_init(java/net/URLClassLoader) &&
    pre_init(java/security/SecureClassLoader) &&
    pre_init(sun/misc/Launcher$ExtClassLoader$1) &&
    pre_init(java/security/ProtectionDomain) &&
    pre_init(java/security/CodeSource) &&
    pre_init(java/security/ProtectionDomain$Key) &&
    pre_init(java/util/WeakHashMap) &&
    pre_init(java/util/Collections$SetFromMap) &&
    pre_init(java/util/WeakHashMap$KeySet) &&
    pre_init(java/util/WeakHashMap$Entry) &&
    pre_init(java/lang/ref/WeakReference) &&
    pre_init(sun/net/www/protocol/jar/Handler) &&
    pre_init(java/net/URLStreamHandler)
    where:
    {R0} == {ROOT}:this

I got a lot of stuff here, while in the output example, there are few lines. But what it is most disturbing for me it is this line:

.1[50591] 
Leaf state, raised exception: Object[2556]

What does it mean that raised an exception? Did I something wrong?

In addition to this, I have only one leaf with an impressive number of objects: 2k+.

Now, I'm giving my set up, even if I followed closely the README:

I have a maven project, with in sources:

package smalldemos.ifx;

import static jbse.meta.Analysis.ass3rt;

public class IfExample {
    boolean a, b;
    public void m(int x) {
        if (x > 0) {
            a = true;
        } else {
            a = false;
        }
        if (x > 0) {
            b = true;
        } else {
            b = false;
        }
        ass3rt(a == b);
    }
}

I use a Java Test Class to run JBSE:

package smalldemos.ifx;

import jbse.apps.run.RunParameters;
import jbse.apps.run.Run;
import org.junit.Test;

public class TestIf {

    @Test
    public void test() throws Exception {
        final RunParameters p = new RunParameters();
        p.setJREPath("lib/jre1.8.0/");
        p.addClasspath("./target/classes", "lib/jbse-0.8.0-SNAPSHOT.jar"); // build from sources, after cloning the repos
        p.setMethodSignature("smalldemos/ifx/IfExample", "(I)V", "m");
        p.setDecisionProcedureType(RunParameters.DecisionProcedureType.Z3);
        p.setExternalDecisionProcedurePath("lib/z3/bin/z3"); // build from sources, after cloning the repos
        p.setOutputFileName("out/runIf_z3.txt");
        p.setStepShowMode(RunParameters.StepShowMode.LEAVES);
        final Run r = new Run(p);
        r.run();
    }
}

In my pom.xml, I have:

 <dependencies>
    <dependency>
      <groupId>jbse</groupId>
      <artifactId>jbse</artifactId>
      <version>0.8.0-SNAPSHOT</version>
    </dependency>
    <dependency>
      <groupId>junit</groupId>
      <artifactId>junit</artifactId>
      <version>4.11</version>
    </dependency>
  </dependencies>

by running mvn test, I obtain what I presented you.

If you want to have a look, I wrapped everything inside a repository.

Could please, tell me what I am doing wrong? Or if the result a perfectly correct, could please explain them a little bit or at least give me some tips to understand them?

Thank you very much.

-- Benjamin.

[pietrobraione]

Hi Benjamin, and thank you for trying JBSE. The master branch currently is in an "in progress" state, as I am trying to implement the JVM specification v8 (invokedynamic and lambdas). Please, shift to the pre-java8 branch, and try again.

[danglotb]

Hi @pietrobraione

Thank for your quick answer.

I switched on the pre-java8 branch as you suggest.

I rebuild the JBSE jar. But, It seems that this API has been added after the branch: p.setJREPath("lib/jre1.8.0/");.

I commented it, but obviously, it is not the right thing to do because I obtain the following stack trace:

Unexpected internal error.
jbse.common.exc.UnexpectedInternalException: jbse.bc.exc.ClassFileNotFoundException: java/lang/Object
    at jbse.mem.State.newInstanceSymbolic(State.java:661)
    at jbse.mem.State.createObjectSymbolic(State.java:643)
    at jbse.mem.State.assumeExpands(State.java:1428)
    at jbse.mem.State.makeArgsSymbolic(State.java:1051)
    at jbse.mem.State.pushFrameSymbolic(State.java:1098)
    at jbse.algo.Algo_INIT.createInitialState(Algo_INIT.java:49)
    at jbse.algo.Algo_INIT.exec(Algo_INIT.java:33)
    at jbse.jvm.Engine.init(Engine.java:153)
    at jbse.jvm.EngineBuilder.build(EngineBuilder.java:63)
    at jbse.jvm.RunnerBuilder.build(RunnerBuilder.java:48)
    at jbse.apps.run.Run.build(Run.java:662)
    at jbse.apps.run.Run.run(Run.java:538)
    at smalldemos.ifx.TestIf.test(TestIf.java:25)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
    at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
    at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
    at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
    at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:271)
    at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:70)
    at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
    at org.junit.runners.ParentRunner$3.run(ParentRunner.java:238)
    at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:63)
    at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:236)
    at org.junit.runners.ParentRunner.access$000(ParentRunner.java:53)
    at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:229)
    at org.junit.runners.ParentRunner.run(ParentRunner.java:309)
    at org.junit.runner.JUnitCore.run(JUnitCore.java:160)
    at com.intellij.junit4.JUnit4IdeaTestRunner.startRunnerWithArgs(JUnit4IdeaTestRunner.java:68)
    at com.intellij.rt.execution.junit.IdeaTestRunner$Repeater.startRunnerWithArgs(IdeaTestRunner.java:51)
    at com.intellij.rt.execution.junit.JUnitStarter.prepareStreamsAndStart(JUnitStarter.java:242)
    at com.intellij.rt.execution.junit.JUnitStarter.main(JUnitStarter.java:70)
Caused by: jbse.bc.exc.ClassFileNotFoundException: java/lang/Object
    at jbse.bc.ClassFileJavassist.<init>(ClassFileJavassist.java:39)
    at jbse.bc.ClassFileFactoryJavassist.newClassFileClass(ClassFileFactoryJavassist.java:26)
    at jbse.bc.ClassFileFactory.newClassFile(ClassFileFactory.java:60)
    at jbse.bc.ClassFileStore.getClassFile(ClassFileStore.java:65)
    at jbse.bc.ClassHierarchy$IterableSuperclasses$MyIterator.next(ClassHierarchy.java:283)
    at jbse.bc.ClassHierarchy$IterableSuperclasses$MyIterator.next(ClassHierarchy.java:257)
    at jbse.bc.ClassHierarchy.getAllFieldsInstance(ClassHierarchy.java:400)
    at jbse.mem.State.newInstanceSymbolic(State.java:659)
    ... 34 more

I tried first to add the JRE jars in the classpath of the RunParameters:

 p.addClasspath(
                "lib/jre1.8.0/charsets.jar",
                "lib/jre1.8.0/rt.jar",
                "./target/classes",
                "lib/jbse-0.8.0-SNAPSHOT.jar"
        ); // build from sources, after cloning the repos

But it is not working.

I looked in code and commits to find a equivalent to this new API you added, but I could not find it. Could please help me?

Thank you very much.

[danglotb]

Hi again,

Sorry, I was still following the README of master branch, and so, had some unmatched configuration.

I was able to run JBSE on the example, and I now obtain something more similar to the expected output.

Thank you, I'm gonna look deeper in it.

Benjamin.

[pietrobraione]

Great, feel free to contact me for any issue.