Some examples report errors which are like "IndexOutOfBoundsException: Index: 2, Size: 1".

[ghost-cai]

windows 11 jdk1.8_382 gradle7.1.1

my defs.java is:

public class Defs {
    //Customize them
    public static final Path CVC4_PATH     = Paths.get("/opt", "local", "bin", "cvc4");
    public static final Path Z3_PATH       = Paths.get("D:","cProject","SymbolicExecution","z3-4.12.2-x64-win","bin","z3.exe");
    public static final Path JBSE_HOME     = Paths.get("D:","cProject","SymbolicExecution","jbse_new","jbse");
    public static final Path EXAMPLES_HOME = Paths.get("D:","companyProject","SymbolicExecution","jbse-examples");

    //Leave them alone
    public static final Path JBSE_CLASSPATH        = JBSE_HOME.resolve("build/classes/java/main");
    public static final Path JBSE_SOURCEPATH       = JBSE_HOME.resolve("src/main/java");
    public static final Path TARGET_CLASSPATH      = EXAMPLES_HOME.resolve("classes/production/jbse-examples");
    public static final Path TARGET_GOLO_CLASSPATH = EXAMPLES_HOME.resolve("golo-bin");
    public static final Path JAR_ASM_CLASSPATH     = EXAMPLES_HOME.resolve("lib/asm-5.1.jar");
    public static final Path JAR_GOLO_CLASSPATH    = EXAMPLES_HOME.resolve("lib/golo-3.3.0.jar");
    public static final Path TARGET_SOURCEPATH     = EXAMPLES_HOME.resolve("src");
    public static final Path JRE_SOURCEPATH        = Paths.get(System.getProperty("java.home", "") + "src.zip");

    //Leave them alone, or add more stuff
    public static final Path[] CLASSPATH  = { TARGET_CLASSPATH, TARGET_GOLO_CLASSPATH, JAR_ASM_CLASSPATH, JAR_GOLO_CLASSPATH };
    public static final Path[] SOURCEPATH = { JBSE_SOURCEPATH, TARGET_SOURCEPATH, JRE_SOURCEPATH };
}

In these examples, such as golo->fibonacci, smalldemos->invokedynamic, tcas and lambda_1. I get the same error like which in the picture.

But in other examples, everthing is ok. I am looking forward to your help.

[pietrobraione]

This is a kind of error that I never encountered. My best guess is that there might be some deviations from one version of the Java 8 platform to another one that caused the breakage. However, while it might be expected that the most complex examples may break (lambda, golo and invokedynamic), tcas is mostly vanilla so it is strange that it is also breaking. Can you please send me the output of running tcas?

[ghost-cai]

Thank you for your answer, this is the output of running tcas(the red colored sentences).The white sentence in the picture is my manual output for debug.

Exception in thread "main" java.lang.IndexOutOfBoundsException: Index: 1, Size: 1
    at java.util.ArrayList.rangeCheck(ArrayList.java:659)
    at java.util.ArrayList.get(ArrayList.java:435)
    at jbse.mem.ObjectDictionary.getClassLoader(ObjectDictionary.java:170)
    at jbse.mem.State.createInstance_JAVA_CLASS(State.java:1601)
    at jbse.mem.State.ensureInstance_JAVA_CLASS(State.java:2091)
    at jbse.algo.Algo_LDCX_Y.lambda$bytecodeCooker$2(Algo_LDCX_Y.java:107)
    at jbse.algo.Algorithm.doExec(Algorithm.java:236)
    at jbse.algo.Algorithm.exec(Algorithm.java:218)
    at jbse.jvm.Engine.step(Engine.java:303)
    at jbse.jvm.Runner.doRun(Runner.java:550)
    at jbse.jvm.Runner.run(Runner.java:520)
    at jbse.apps.run.Run.run(Run.java:622)
    at tcas.RunTcas.main(RunTcas.java:18)

[ghost-cai]

I solved the problem，I chang the version of jdk1.8 to jdk1.8.0_311.And then I get the right result. (All examples which I refered to) This was my previous version of jdk1.8.

But I still have some questions. Can the jbse be used to analyze or test a jar package of a complete Java software? Or, is it only for .class files? Which version of jdk1.8 do you recommend? Hope your answer.

[pietrobraione]

Yes, JBSE can work with jars; actually, it uses the rt.jar of the jdk 8 on which it is installed. For the version, I can report that JBSE works correctly with Temurin 1.8.0_312 (I cannot see any reason why it should not work with a previous version). As soon as I find some free time I will upgrade JBSE so it can work correctly with the last 1.8.0. Until then please bear patience and keep using the old version of the JDK.

[ghost-cai]

I am glad to you can answer quickly. But I mean "test the jar package", not "work with jar package". The example, fibonacci, is working with jar. However, it still need "Fibonacci.class" These are details of the fibonacci:

// From RunGoloFibonacci.java 
private static void set(RunParameters p) {
  ...
  p.addUserClasspath(CLASSPATH);
  ...
}

public class Defs {
    //Customize them
    public static final Path CVC4_PATH     = Paths.get("/opt", "local", "bin", "cvc4");
    public static final Path Z3_PATH       = Paths.get("D:","cProject","SymbolicExecution","z3-4.12.2-x64-win","bin","z3.exe");
    public static final Path JBSE_HOME     = Paths.get("D:","cProject","SymbolicExecution","jbse_new","jbse");
    public static final Path EXAMPLES_HOME = Paths.get("D:","cProject","SymbolicExecution","jbse-examples");

    //Leave them alone
    public static final Path JBSE_CLASSPATH        = JBSE_HOME.resolve("build/classes/java/main");
    public static final Path JBSE_SOURCEPATH       = JBSE_HOME.resolve("src/main/java");
    public static final Path TARGET_CLASSPATH      = EXAMPLES_HOME.resolve("classes/production/jbse-examples");

//Look Here
//CLASSPATH with addUserClasspath still needs TARGET_GOLO_CLASSPATH which is the path of .class file.
    public static final Path TARGET_GOLO_CLASSPATH = EXAMPLES_HOME.resolve("golo-bin");

    public static final Path JAR_ASM_CLASSPATH     = EXAMPLES_HOME.resolve("lib/asm-5.1.jar");
    public static final Path JAR_GOLO_CLASSPATH    = EXAMPLES_HOME.resolve("lib/golo-3.3.0.jar");
    public static final Path TARGET_SOURCEPATH     = EXAMPLES_HOME.resolve("src");
    public static final Path JRE_SOURCEPATH        = Paths.get(System.getProperty("java.home", "") + "src.zip");

    //Leave them alone, or add more stuff
    public static final Path[] CLASSPATH  = { TARGET_CLASSPATH, TARGET_GOLO_CLASSPATH, JAR_ASM_CLASSPATH, JAR_GOLO_CLASSPATH };
    public static final Path[] SOURCEPATH = { JBSE_SOURCEPATH, TARGET_SOURCEPATH, JRE_SOURCEPATH };
}

If I want to test a java project named "A", I package the project to a A.jar package. How do I use jbse to test the A.jar package? Do I have to extract the main.class from the A.jar with the decompiler tool and put it in the runAproject (you know, using jbse need to write somthing, runAproject is the project wrote by me for using the jbes to test the A.jar ) ? Is there a simpler way? I wrote a example which like this to test a java project ,but it had a error.

public class RunTestWebGoat {

    public static void main(String[] args)  {
        final RunParameters p = new RunParameters();
        set(p);
        final Run r = new Run(p);
        r.run();
    }
    //"BOOT-INF/classes/org/owasp/webgoat/StartWebGoat"

    public static final Path Z3_PATH = Paths.get("D:","companyProject","SymbolicExecution","z3-4.12.2-x64-win","bin","z3.exe");
    public static final Path JBSE_HOME = Paths.get("D:","companyProject","SymbolicExecution","jbse_new","jbse");

    public static final Path JBSE_CLASSPATH = JBSE_HOME.resolve("build/libs/jbse-0.11.0-SNAPSHOT-shaded.jar");
//
    public static final Path USER_ClASSPATH = Paths.get("../../webgoat-server-8.0.0-cifuzz-nologin.jar");

// I know the "METHOD_CLASS" from jar package by using the decompiler tool. I show the picture at the end of message.
        private static final String METHOD_CLASS = "BOOT-INF/classes/org/owasp/webgoat/StartWebGoat";
        private static final String METHOD_DESCRIPTOR = "([Ljava/lang/String;)V";
        private static final String METHOD_NAME = "main";

    public static final Path OUT_FILE = Paths.get("../../out/runTestWebGoat.txt");

    private static void set(RunParameters p) {

        p.addUserClasspath(USER_ClASSPATH);
        p.setJBSELibPath(JBSE_CLASSPATH);
        p.setMethodSignature(METHOD_CLASS, METHOD_DESCRIPTOR, METHOD_NAME);
        p.setDecisionProcedureType(DecisionProcedureType.Z3);
        p.setExternalDecisionProcedurePath(Z3_PATH);
        p.setOutputFilePath(OUT_FILE);
        p.setStateFormatMode(StateFormatMode.TEXT);
        p.setStepShowMode(StepShowMode.LEAVES);
    }
}

This is hte error picture:

Can you give some suggestions? Thank you for your help.

The picture of decompiler tool:

[pietrobraione]

There is no need to extract any class file from the jars. JBSE can work with all the class files, including the entry point of symbolic execution, inside a jar file. From what I see it is possible that JBSE cannot find the jar file. I can suggest to use an absolute path, instead of a relative path, as USER_CLASSPATH and try again.

[ghost-cai]

Thank you for your help. I used an absolute path, and the jbse can find the classpath. Unfortunately, I get a new error. I guess the reason is that the jdk which the webgoat (tested project) used is over the jkd8. Can the jbse work with the project which uses the jdk9/10/11/17/21? This is the url of webgoat's jar. WebGoat-v8.0.0(I used this one) WebGoat_releases

[pietrobraione]

Unfortunately no: JBSE supports only JDK 8.

[ghost-cai]

Thank you a lot for your answer. Based on your answer, I hava tried a new project (java-sec-code). java-sec-code.This project used the jdk1.8. However I got a new error.

This is the Java Bytecode Symbolic Executor's Run Tool (null v.null).
Connecting to Z3 at D:\companyProject\SymbolicExecution\z3-4.12.2-x64-win\bin\z3.exe.
Cannot find item in the classpath.
jbse.common.exc.ClasspathException: jbse.bc.exc.ClassFileNotFoundException: Did not find any class org/springframework/boot/web/support/SpringBootServletInitializer in the classpath.
    at jbse.algo.Action_START.loadCreateEssentialClasses(Action_START.java:331)
    at jbse.algo.Action_START.createStateStart(Action_START.java:158)
    at jbse.algo.Action_START.exec(Action_START.java:138)
    at jbse.jvm.Engine.init(Engine.java:158)
    at jbse.jvm.EngineBuilder.build(EngineBuilder.java:71)
    at jbse.jvm.RunnerBuilder.build(RunnerBuilder.java:56)
    at jbse.apps.run.Run.build(Run.java:730)
    at jbse.apps.run.Run.run(Run.java:610)
    at webgoat.RunTestWebGoat.main(RunTestWebGoat.java:17)
Caused by: jbse.bc.exc.ClassFileNotFoundException: Did not find any class org/springframework/boot/web/support/SpringBootServletInitializer in the classpath.
    at jbse.bc.ClassHierarchy.loadCreateClass(ClassHierarchy.java:666)
    at jbse.bc.ClassHierarchy.resolveClass(ClassHierarchy.java:974)
    at jbse.bc.ClassHierarchy.resolveSuperclass(ClassHierarchy.java:835)
    at jbse.bc.ClassHierarchy.defineClass(ClassHierarchy.java:797)
    at jbse.bc.ClassHierarchy.loadCreateClass(ClassHierarchy.java:677)
    at jbse.algo.Action_START.loadCreateEssentialClasses(Action_START.java:327)
    ... 8 more

But the 'org/springframework/boot/web/support/SpringBootServletInitializer' is not the start class. I haven't coded about it. The picture is the start class of java-sec-code.The jbse not find the blue sentence.

It is strange tht I started the jar of java-sec-code with jdk1.8 successfully.

java -jar java-sec-code-1.0.0.jar --server.port=9091

And I can find the SpringBootServletInitializer.class in path "org/springframework/boot/web/support/' like this picture.

Can you give me some suggestions about the ClassFileNotFoundException?

[ghost-cai]

hello?