Dynamic Symbolic Execution for Object-Oriented Libraries

Lian Li and Andrew Santosa
Oracle Labs Australia

Symbolic execution is a program analysis technique that   provides auxiliary execution semantics to execute programs with symbolic rather than concrete values. There has been much   recent interest in symbolic execution for automatic test case generation, and various symbolic execution tools have been successfully deployed for testing and security vulnerability  detection. Nevertheless, polymorphism of object-oriented programs has been neglected by existing symbolic execution techniques. We address the problem how this polymorphism can be expressed in a symbolic execution framework. We propose the notion of symbolic types, which make object types symbolic. Using symbolic types, various targets of method invocation can be explored by mutating the object type in test case generation. Symbolic types are critical for effectively testing object-oriented programs, especially libraries.  Our experimental results show that symbolic types achieve higher testing coverage for the Open Java\texttrademark Development Kit library (OpenJDK) than symbolic execution techniques without  symbolic types, and that symbolic types are essential in finding bugs and security vulnerabilities in OpenJDK.