Symbolic Execution using java.lang.String

[danglotb]

Hi,

I am using JBSE, I ran on the provided example, and on my own.

My example is a basic implementation of the standard charAt method of String: char charAt(String s, int i), i.e. it returns the char at the i th position in the given String s.

I setted up JBSE to perform the symbolic execution. But when I actually run it, It takes a while.

I assumed that came from the fact that there are a lot of possibilities. Also, I added an assumption at the begin of my method: assume(s.length < 4).

At the end, I obtain something like:

.1.1.1[3] 
Leaf state, raised exception: Object[2]
Path condition: 
	{R0} == Object[0] (fresh) &&
	pre_init(smalldemos/ifx/TestSuiteExample) &&
	{R1} == Object[1] (fresh) &&
	{V4} < 16
	where:
	{R0} == {ROOT}:this &&
	{R1} == {ROOT}:s &&
	{V4} == {ROOT}:s.count
Static store: {
	
}
Heap: {
	Object[0]: {
		Origin: {ROOT}:this
		Class: smalldemos/ifx/TestSuiteExample
	}
	Object[1]: {
		Origin: {ROOT}:s
		Class: java/lang/String
		Field[0]: Name: hash, Type: I, Value: {V5} (type: I)
		Field[1]: Name: value, Type: [C, Value: {R2} (type: L)
		Field[2]: Name: offset, Type: I, Value: {V3} (type: I)
		Field[3]: Name: count, Type: I, Value: {V4} (type: I)
	}
	Object[2]: {
		Class: java/lang/NoClassDefFoundError
		Field[0]: Name: detailMessage, Type: Ljava/lang/String;, Value: null (type: 0)
		Field[1]: Name: cause, Type: Ljava/lang/Throwable;, Value: null (type: 0)
		Field[2]: Name: backtrace, Type: Ljava/lang/Object;, Value: Object[3] (type: L)
		Field[3]: Name: stackTrace, Type: [Ljava/lang/StackTraceElement;, Value: null (type: 0)
	}
...

According to Leaf state, raised exception: Object[2] and to Object[2]: { Class: java/lang/NoClassDefFoundError, It seems that JBSE does not find java.lang.String, which is strange since I gave the rt.jar in the classpath.

Here, found more information about my setup:

@Test
    public void testExample() throws Exception {
        final RunParameters p = new RunParameters();
        p.addClasspath(
                "pathTo/jbse/data/jre/rt.jar",
                "./target/classes",
                "./target/test-classes",
                "lib/jbse-0.8.0-SNAPSHOT.jar"
        );
        p.setMethodSignature("smalldemos/ifx/Example", "(Ljava/lang/String;I)C", "charAt");
        p.setDecisionProcedureType(RunParameters.DecisionProcedureType.Z3);
        p.setExternalDecisionProcedurePath("lib/z3/bin/z3");
        p.setOutputFileName("out/runIf_z3.txt");
        p.setStepShowMode(RunParameters.StepShowMode.LEAVES);
        p.setStateFormatMode(RunParameters.StateFormatMode.FULLTEXT);
        final Run r = new Run(p);
        r.run();
    }

public char charAt(String s, int index) {
        assume(s.length() < 4);
        if (index <= 0)
            return s.charAt(0);
        else if (index < s.length())
            return s.charAt(index);
        else
            return s.charAt(s.length() - 1);
    }

Could you please tell me what I am doing wrong? Or point me some extra information?

Thank you very much.

-- Benjamin.

[pietrobraione]

Apparently it is not a rt.jar issue, if it hadn't found java.lang.String it wouldn't have created Object[1] that precisely is an instance of that class. Could you please send the full runIf_z3.txt file so I can detect what's missing?

[danglotb]

Hi, thank you!

Please find here, the txt report obtained: runIf_z3_leaves.txt

Here, I give you the same report but using RunParameters.StepShowMode.ALL: runIf_z3_all.txt you might need him.

Thank a lot!

-- Benjamin.

[pietrobraione]

From what I see the problem is that in the classpath you are missing the jbse.meta.Analysis class. Possibly your classpath entry "lib/jbse-0.8.0-SNAPSHOT.jar" is wrong (note that Maven puts the jar in target/ not in lib/).

[danglotb]

Hi,

Okay, I just changes the relative path to point to the jar generated by maven (inside target).

But I am facing another issue.

The Symbolic execution takes a lot of time, and end up with java.lang.OutOfMemoryError: Java heap space.

See here, an excerpt of the output runIf_z3.txt

How can I can prevent such behavior and limit the execution using string (for instance limit the size of the String)?

-- Benjamin.

[pietrobraione]

That's expected: If you loop liberally over a symbolic string without putting an iteration bound, symbolic execution will diverge. Assuming that the length of the string is less than a value (4, in your case) may be insufficient, because by default JBSE is unaware of the invariant that the length of the string is also the size of the array of chars stored in it. I will work on the issue, but since I am super busy I am afraid I will not be able to distill a fix before the end of next week. However I am definitely very interested in improving the support to strings in JBSE, so I will keep the issue high in my priority list.

[danglotb]

Hi,

If you loop liberally over a symbolic string without putting an iteration bound, symbolic execution will diverge.

Okay thank you very much!

However I am definitely very interested in improving the support to strings in JBSE, so I will keep the issue high in my priority list.

That is a good news! Let's keep this issue open to track the evolution about it.

Thank you!

-- Benjamin.

[danglotb]

Hi @pietrobraione

I saw that you made a lot of changes recently on JBSE.

Could you please keep me update if I can switch on the master branch rather than pre-java8.

Thank you very much.

[pietrobraione]

Not yet; the changes were not about strings, but about dynamic classloading. I am still thinking about the kind of changes that are best for strings (it turns out that the possible solutions are all quite complex). Also, the master branch has a severe regression on speed (currently it is >6 times slower than the pre-java8 branch). When I am ready to roll on changes on strings I will do it against the pre-java8 branch, and port them to the master branch later, so you will not have to switch branches.

[pietrobraione]

Now the master branch has no longer the regression on speed, so it is safe to use it (I will close the pre-java8 branch soon, because now it is lagging a lot behind the master branch, which has no more relevant regressions). There is no meaningful progress on string support, but there is much progress on using function symbols instead of invoking pure methods. A better string support will build upon this foundation.