Dsc is a dynamic symbolic execution engine and test case generator for Java (bytecode) programs.
Implementation
Dsc is implemented in Java 6.
Dsc uses Asm to instrument Java classes at load-time.
Dsc uses the instrumentation code to build and maintain a symbolic shadow representation of the dynamic program state (call stack, operand stacks, and heap).
To reason about the program and generate test cases for the program, Dsc uses the Z3 theorem prover from Microsoft Research.
To communicate with Z3, Dsc uses a SWIG-generated Z3-wrapper.
License
Dsc is built on top of several third-party software components. For example, in the current release, Dsc uses the Z3 theorem prover from Microsoft Research. For your convenience, we distribute Dsc together with all third-party software components that are currently required to run Dsc. However, it is your responsibility to satisfy the license terms of each third-party software component. The following list is just for informational purposes and may be wrong. You are responsible for ensuring that you have the proper licenses.
Dsc is an academic prototype. Dsc has many known and unknown bugs. It is not integrated with any IDE. If you are looking for a related tool that is actually usable, we highly recommend Microsoft Pex.
Known limitations include the following. If the analyzed program uses one or more of these features, Dsc is in trouble.
Arrays: buggy.
Floating-point numbers (float, double): not supported.
Multi-threading: not supported (Dsc assumes the analyzed application is single-threaded).
Strings: only basic support (Dsc does not reason about String contents).
Use of standard Jdk classes: only basic support (Dsc currently does not instrument Jdk classes).
Extensions
Mock class generation
Some code under test refers to abstract types such as interfaces. If the abstract types are not implemented by any concrete classes (yet), the code cannot be executed. To address this problem, Dsc has a mock class generation extension, which reasons about type constraints and generates such required concrete classes. This even works for complex type constraints involving several abstract types and code under test that uses reflection to check type constraints.
The mock class generator also handles code under test that uses reflection to check for annotations.
To support such uses of Dsc, Dsc has a "dumper mode", which just dumps collected constraints to disk. In this mode, Dsc can be invoked without the Z3 binaries being present. This should allow Dsc to be used on any platform. To invoke Dsc in dumper mode, use the following configuration option:
Dsc+Mock is a dynamic symbolic test case generator that can reason about type constraints and can generate mock classes that satisfy such constraints. Our prototype implementation achieved higher code coverage than related test case generators that do not generate mock classes, such as Pex.
This paper discusses the implementation of our dynamic symbolic data structure repair tool, DSDSR. We provide initial empirical results of applying DSDSR on different formulations of the same correctness condition and compare DSDSR with a state-of-the-art tool, Juzi.
Dynamic symbolic data structure repair (Proc. 32nd ACM/IEEE International Conference on Software Engineering (ICSE), Volume 2, Emerging Results Track, 2010)
We motivate how dynamic symbolic techniques enable generic repair to support a wider range of correctness conditions and present DSDSR, a novel repair algorithm based on dynamic symbolic execution. We implement the algorithm for Java and report initial empirical results to demonstrate the promise of our approach for generic repair.
For a given branching statement encountered during program execution, CarFast estimates the number of statements that are yet uncovered but reachable from the respective branch outcomes. With the symbolic path condition collected during execution, CarFast selects input values such that a future execution will trigger a branch (path) that contains a high number of those yet uncovered statements.
We formalize a MapReduce-specific correctness condition that all MapReduce applications have to satisfy, in order to be free of a certain class of bugs. To detect such bugs, we then design a technique that encodes the correctness condition as symbolic program constraints, checks them via dynamic symbolic execution, and generates corresponding test cases.
Software testing interacts with data anonymization in surprising ways. I.e., increasing data anonymity to protect data during testing can drastically decrease test coverage. One problem is that current anonymization techniques do not take into account how the application under test actually uses the data. We therefore propose to guide data anonymization techniques with program analysis. Received the Best Paper Award.
We use dynamic symbolic execution to obtain a program path-condition. We then use this path-condition as a database query.
Sponsors
This material is based upon work supported by the National Science Foundation under Grants No. 1017305 and 1117369. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.