Instantly share code, notes, and snippets.

@rindPHI /Main.java
Last active Feb 16, 2017

Embed
What would you like to do?
Example Usage of the Symbolic Execution API
package example;
import java.io.File;
import java.util.HashMap;
import java.util.List;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.java.StringUtil;
import de.uka.ilkd.key.control.*;
import de.uka.ilkd.key.java.abstraction.*;
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);
env.dispose();
}
// Set Taclet options
ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
HashMap<String, String> newSettings = new HashMap<String, String>(oldSettings);
newSettings.putAll(MiscTools.getDefaultTacletOptions());
choiceSettings.setDefaultChoices(newSettings);
// 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,
"equals",
ImmutableSLList.<Type>nil().append(classType),
classType);
// Instantiate proof for symbolic execution of the program method (Java semantics)
AbstractOperationPO po = new ProgramMethodPO(env.getInitConfig(),
"Symbolic Execution of: " + pm,
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
builder.analyse();
// 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
SymbolicExecutionUtil.initializeStrategy(builder);
SymbolicExecutionEnvironment.configureProofForSymbolicExecution(proof,
100,
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
proof.getSettings().getStrategySettings().setCustomApplyStrategyStopCondition(stopCondition);
// Perform strategy which will stop at breakpoint
symbolicEnv.getProofControl().startAndWaitForAutoMode(proof);
builder.analyse();
printSymbolicExecutionTree("Stopped at Breakpoint", builder);
// Perform strategy again to complete symbolic execution tree
symbolicEnv.getProofControl().startAndWaitForAutoMode(proof);
builder.analyse();
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 + "':");
e.printStackTrace();
}
}
/**
* 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(title);
System.out.println(StringUtil.createLine("=", title.length()));
ExecutionNodePreorderIterator iterator = new ExecutionNodePreorderIterator(builder.getStartNode());
while (iterator.hasNext()) {
IExecutionNode<?> next = iterator.next();
System.out.println(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.
}
System.out.println();
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment