Symbolic Execution

This page is used to explain symbolic execution tools have limited support for inputs involving complex objects and data structures.

Simple Example

Objects of Interface Types

​x
interface MyInterface {
    void print();
}

class MyClass implements MyInterface {
    public void print() {
        System.out.println("!!MyClass!!");;
    }
}

public class MyTest {
    public static void main(String[] args) {
        MyInterface mi = (MyInterface) Debug.makeSymbolicRef("my_interface", new MyClass()); 
        mi.print();
    }
}

Objects with Array Type Fields.

xxxxxxxxxx
public class MyTest {
    
    public static int[] length(String str) {
        return new int[str.length()];
    }
    
    public static void main(String[] args) {
        String str = Debug.makeSymbolicString("my_str");
        
        length(str);
    }
}

Collection Data Structure

xxxxxxxxxx
class MyNode {
    int index;
    MyNode next;
    
    public static int getLastIndex(MyNode node) {
        while (node.next != null)
            node = node.next;
        return node.index;
    }
}

public class MyTest {
    public static void main(String[] args) {
        MyNode mc = (MyNode) Debug.makeSymbolicRef("my_node", new MyNode());
        MyNode.getLastIndex(mc);
    }
}

Root Causes Sample

R1. SPF crashed when invoking a method through a symbolic object of interface type

SPF Driver

xxxxxxxxxx
public class StrBuilder3Test {

  public static void main(String[] args) throws IOException {

    StrBuilder strbuilder = (StrBuilder) Debug.makeSymbolicRef("my_strbuilder", new StrBuilder());
    Appendable appendable = (Appendable) Debug.makeSymbolicRef("my_appendable", new StringBuffer());

    strbuilder.appendTo(appendable);
  }
  
}

Output Log

xxxxxxxxxx
java.lang.NullPointerException
  at gov.nasa.jpf.symbc.bytecode.INVOKEINTERFACE.execute(INVOKEINTERFACE.java:46)
  at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
  at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
  at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
  at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
  at gov.nasa.jpf.search.Search.forward(Search.java:579)
  at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
  at gov.nasa.jpf.JPF.run(JPF.java:617)
  at gov.nasa.jpf.JPF.start(JPF.java:189)
  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 gov.nasa.jpf.tool.Run.call(Run.java:80)
  at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

R2. SPF was stuck when forking a large number of states for heap objects

SPF Driver

xxxxxxxxxx
public class ExceptionUtils2Test {
  public static void main(String[] args) {
    Throwable throwable = (Throwable) Debug.makeSymbolicRef("my_throwable", new Throwable());

    ExceptionUtils.getThrowableList(throwable);
  }
}

R3. SPF crashed when accessing the length of an array field within a symbolic object

SPF Driver

xxxxxxxxxx
public class StringUtils2Test {

  public static void main(String[] args) {
    CharSequence cs = (CharSequence) Debug.makeSymbolicRef("my_arr", "test1");
    CharSequence[] arr = (CharSequence[]) Debug.makeSymbolicRef("my_arr", new CharSequence[]{"p1", "p2"});
    
    StringUtils.endsWithAny(cs, arr);
  }

}

Output Log

xxxxxxxxxx
java.lang.NullPointerException
  at gov.nasa.jpf.symbc.heap.Helper.addNewHeapNode(Helper.java:169)
  at gov.nasa.jpf.symbc.bytecode.GETFIELD.execute(GETFIELD.java:194)
  at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
  at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
  at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
  at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
  at gov.nasa.jpf.search.Search.forward(Search.java:579)
  at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
  at gov.nasa.jpf.JPF.run(JPF.java:617)
  at gov.nasa.jpf.JPF.start(JPF.java:189)
  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 gov.nasa.jpf.tool.Run.call(Run.java:80)
  at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

R4. SPF has limited support for String

SPF Driver

xxxxxxxxxx
public class DatasetUtils2Test {

  public static void main(String[] args) {
    String rowKeyPrefix = Debug.makeSymbolicString("my_rowKeyPrefix");
    String columnKeyPrefix = Debug.makeSymbolicString("my_columnKeyPrefix");
    Number[][] data = (Number[][]) Debug.makeSymbolicRef("my_data", new Number[][] {{new Double(1.2), new Integer(5)}, {new Long(6L), new Float(2.5f)}});

    DatasetUtils.createCategoryDataset(rowKeyPrefix, columnKeyPrefix, data);

  }

}

Output Log

xxxxxxxxxx
java.lang.RuntimeException: ERROR: symbolic method not handled: hashCode
  at gov.nasa.jpf.symbc.bytecode.SymbolicStringHandler.handleSymbolicStrings(SymbolicStringHandler.java:311)
  at gov.nasa.jpf.symbc.bytecode.BytecodeUtils.execute(BytecodeUtils.java:219)
  at gov.nasa.jpf.symbc.bytecode.INVOKEVIRTUAL.execute(INVOKEVIRTUAL.java:52)
  at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
  at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
  at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
  at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
  at gov.nasa.jpf.search.Search.forward(Search.java:579)
  at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
  at gov.nasa.jpf.JPF.run(JPF.java:617)
  at gov.nasa.jpf.JPF.start(JPF.java:189)
  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 gov.nasa.jpf.tool.Run.call(Run.java:80)
  at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

R5. SPF is unable to handle native methods

SPF Driver

xxxxxxxxxx
public class ApcomplexMathTest {
  
  public static void main(String[] args) {
    Apcomplex ac = (Apcomplex) Debug.makeSymbolicRef("my_ac", new Apcomplex(new Apfloat(0.5)));
      ApcomplexMath.exp(ac);
    }

}

Output Log

xxxxxxxxxx
java.lang.UnsatisfiedLinkError: cannot find native sun.management.VMManagementImpl.getVersion0
  at sun.management.VMManagementImpl.getVersion0(no peer)
  at sun.management.VMManagementImpl.<clinit>(VMManagementImpl.java:64)
  at sun.management.ManagementFactoryHelper.<clinit>(ManagementFactoryHelper.java:455)
  at java.lang.management.ManagementFactory.getMemoryMXBean(ManagementFactory.java:329)
  at org.apfloat.ApfloatContext.<clinit>(ApfloatContext.java:1361)
  at org.apfloat.ApfloatHelper.getDefaultRadix(ApfloatHelper.java:783)
  at org.apfloat.ApfloatHelper.createApfloat(ApfloatHelper.java:88)
  at org.apfloat.Apint.<init>(Apint.java:111)
  at org.apfloat.Apcomplex.<clinit>(Apcomplex.java:60)
  at selab.ApcomplexMathTest.main(ApcomplexMathTest.java:13)

R6. SPF failed to solve path constraints

SPF Driver

xxxxxxxxxx
public class FractionTest {

  public static void main(String[] args) {
    Fraction fraction1 = (Fraction) Debug.makeSymbolicRef("my_fraction", Fraction.getFraction(2.3));
    Fraction fraction2 = (Fraction) Debug.makeSymbolicRef("my_fraction", Fraction.ONE_QUARTER);

    fraction1.divideBy(fraction2);
  }

}

Output Log

xxxxxxxxxx
java.lang.RuntimeException: ## Error Z3 

  at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3.and(ProblemZ3.java:971)
  at gov.nasa.jpf.symbc.numeric.PCParser.getExpression(PCParser.java:179)
  at gov.nasa.jpf.symbc.numeric.PCParser.createDPLinearIntegerConstraint(PCParser.java:730)
  at gov.nasa.jpf.symbc.numeric.PCParser.addConstraint(PCParser.java:1107)
  at gov.nasa.jpf.symbc.numeric.PCParser.parse(PCParser.java:1091)
  at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:128)
  at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:393)
  at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:340)
  at gov.nasa.jpf.symbc.bytecode.optimization.util.IFInstrSymbHelper.getNextInstructionAndSetPCChoice(IFInstrSymbHelper.java:490)
  at gov.nasa.jpf.symbc.bytecode.optimization.IFNE.execute(IFNE.java:67)
  at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
  at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
  at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
  at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
  at gov.nasa.jpf.search.Search.forward(Search.java:579)
  at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
  at gov.nasa.jpf.JPF.run(JPF.java:617)
  at gov.nasa.jpf.JPF.start(JPF.java:189)
  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 gov.nasa.jpf.tool.Run.call(Run.java:80)
  at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)