Skip to content

Instantly share code, notes, and snippets.



Last active Feb 16, 2017
What would you like to do?
Example Usage of the Symbolic Execution API
package example;
import java.util.HashMap;
import java.util.List;
import org.key_project.util.collection.ImmutableSLList;
import de.uka.ilkd.key.control.*;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.proof.*;
import de.uka.ilkd.key.settings.*;
import de.uka.ilkd.key.symbolic_execution.*;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO;
import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile;
import de.uka.ilkd.key.symbolic_execution.strategy.*;
import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.*;
import de.uka.ilkd.key.symbolic_execution.util.*;
import de.uka.ilkd.key.util.MiscTools;
* Example application which symbolically executes
* {@code example/Number#equals(Number)}
* @author Martin Hentschel
public class Main {
* The program entry point.
* @param args The start parameters.
public static void main(String[] args) {
File location = new File("example"); // Path to the source code folder/file or to a *.proof file
List<File> classPaths = null; // Optionally: Additional specifications for API classes
File bootClassPath = null; // Optionally: Different default specifications for Java API
List<File> includes = null; // Optionally: Additional includes to consider
try {
// Ensure that Taclets are parsed
if (!ProofSettings.isChoiceSettingInitialised()) {
KeYEnvironment<?> env = KeYEnvironment.load(location, classPaths, bootClassPath, includes);
// Set Taclet options
ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
HashMap<String, String> newSettings = new HashMap<String, String>(oldSettings);
// Load source code
KeYEnvironment<DefaultUserInterfaceControl> env = KeYEnvironment.load(SymbolicExecutionJavaProfile.getDefaultInstance(), location, classPaths, bootClassPath, includes, true); // env.getLoadedProof() returns performed proof if a *.proof file is loaded
try {
// Find method to symbolically execute
KeYJavaType classType = env.getJavaInfo().getKeYJavaType("Number");
IProgramMethod pm = env.getJavaInfo().getProgramMethod(classType,
// Instantiate proof for symbolic execution of the program method (Java semantics)
AbstractOperationPO po = new ProgramMethodPO(env.getInitConfig(),
"Symbolic Execution of: " + pm,
null, // An optional precondition
true, // Needs to be true for symbolic execution!
true); // Needs to be true for symbolic execution!
// po = new ProgramMethodSubsetPO(...); // PO for symbolic execution of some statements within a method (Java semantics)
// po = new FunctionalOperationContractPO(...) // PO for verification (JML semantics)
Proof proof = env.createProof(po);
// Create symbolic execution tree builder
SymbolicExecutionTreeBuilder builder = new SymbolicExecutionTreeBuilder(proof,
false, // Merge branch conditions
false, // Use Unicode?
true, // Use Pretty Printing?
true, // Variables are collected from updates instead of the visible type structure
true); // Simplify conditions
// Optionally, create an SymbolicExecutionEnvironment which provides access to all relevant objects for symbolic execution
SymbolicExecutionEnvironment<DefaultUserInterfaceControl> symbolicEnv = new SymbolicExecutionEnvironment<DefaultUserInterfaceControl>(env, builder);
printSymbolicExecutionTree("Initial State", builder);
// Configure strategy for full exploration
false, // true to apply method contracts instead of inlining,
false, // true to apply loop invariants instead of unrolling,
false, // true to apply block contracts instead of expanding.
false, // true to hide branch conditions caused by symbolic execution within modalities not of interest,
false); // true to perform alias checks during symbolic execution
// Optionally, add a more advanced stop conditions like breakpoints
CompoundStopCondition stopCondition = new CompoundStopCondition();
stopCondition.addChildren(new ExecutedSymbolicExecutionTreeNodesStopCondition(100)); // Stop after 100 nodes have been explored on each branch.
// stopCondition.addChildren(new StepOverSymbolicExecutionTreeNodesStopCondition()); // Perform only a step over
// stopCondition.addChildren(new StepReturnSymbolicExecutionTreeNodesStopCondition()); // Perform only a step return
IBreakpoint breakpoint = new ExceptionBreakpoint(proof, "java.lang.NullPointerException", true, true, true, true, 1);
stopCondition.addChildren(new SymbolicExecutionBreakpointStopCondition(breakpoint)); // Stop at specified breakpoints
// Perform strategy which will stop at breakpoint
printSymbolicExecutionTree("Stopped at Breakpoint", builder);
// Perform strategy again to complete symbolic execution tree
printSymbolicExecutionTree("Stopped at Breakpoint", builder);
finally {
env.dispose(); // Ensure always that all instances of KeYEnvironment are disposed
catch (Exception e) {
System.out.println("Exception at '" + location + "':");
* Prints the symbolic execution tree as flat list into the console.
* @param title The title.
* @param builder The {@link SymbolicExecutionTreeBuilder} providing the root of the symbolic execution tree.
protected static void printSymbolicExecutionTree(String title, SymbolicExecutionTreeBuilder builder) {
System.out.println(StringUtil.createLine("=", title.length()));
ExecutionNodePreorderIterator iterator = new ExecutionNodePreorderIterator(builder.getStartNode());
while (iterator.hasNext()) {
IExecutionNode<?> next =;
// next.getVariables(); // Access the symbolic state.
// next.getCallStack(); // Access the call stack.
// next.getPathCondition(); // Access the path condition.
// next.getFormatedPathCondition(); // Access the formated path condition.
// next... // Additional methods provide access to additional information.
// Check also the specific sub types of IExecutionNode like IExecutionTermination.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.