de.uka.ilkd.key.symbolic_execution.strategy

Class SymbolicExecutionBreakpointStopCondition

java.lang.Object

de.uka.ilkd.key.symbolic_execution.strategy.ExecutedSymbolicExecutionTreeNodesStopCondition

de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionBreakpointStopCondition

All Implemented Interfaces:

StopCondition, IBreakpointStopCondition

public class SymbolicExecutionBreakpointStopCondition
extends ExecutedSymbolicExecutionTreeNodesStopCondition
implements IBreakpointStopCondition

An IBreakpointStopCondition which can be used during symbolic execution.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Set<IBreakpoint>	breakpoints The used IBreakpoints.

Fields inherited from class de.uka.ilkd.key.symbolic_execution.strategy.ExecutedSymbolicExecutionTreeNodesStopCondition

MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_FOR_ONE_STEP, MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_IN_COMPLETE_RUN

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionBreakpointStopCondition(IBreakpoint... breakpoints) Creates a new SymbolicExecutionBreakpointStopCondition.

Method Summary

Modifier and Type	Method and Description
void	addBreakpoint(IBreakpoint breakpoint) Adds a new IBreakpoint.
java.util.Set<IBreakpoint>	getBreakpoints() Returns all available IBreakpoints.
int	getMaximalWork(int maxApplications, long timeout, Proof proof) Returns the maximal amount of work needed to complete the task, used to display a progress bar.
protected void	handleNodeLimitNotExceeded(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal, Node node, RuleApp ruleApp, java.lang.Integer executedNumberOfSetNodes) Handles the state that the node limit is not exceeded.
protected boolean	isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node) Checks if a breakpoint is hit.
boolean	isGoalAllowed(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal) Checks if it is allowed to apply the next rule on the selected Goal chosen by the GoalChooser before it is applied.
void	removeBreakpoint(IBreakpoint breakpoint) Removes an IBreakpoint.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.strategy.ExecutedSymbolicExecutionTreeNodesStopCondition

getExectuedSetNodesPerGoal, getGoalNotAllowedMessage, getMaximalNumberOfSetNodesToExecutePerGoal, getStopMessage, handleNodeLimitExceeded, setMaximalNumberOfSetNodesToExecutePerGoal, shouldStop, wasSetNodeExecuted

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.prover.StopCondition

getGoalNotAllowedMessage, getStopMessage, shouldStop

Field Detail

breakpoints

private final java.util.Set<IBreakpoint> breakpoints

The used IBreakpoints.

Constructor Detail

SymbolicExecutionBreakpointStopCondition

public SymbolicExecutionBreakpointStopCondition(IBreakpoint... breakpoints)

Creates a new SymbolicExecutionBreakpointStopCondition.

Parameters:

breakpoints - The IBreakpoint to use.

Method Detail

getMaximalWork

public int getMaximalWork(int maxApplications,
                          long timeout,
                          Proof proof)

Returns the maximal amount of work needed to complete the task, used to display a progress bar. Pass 0 to indicate unknown size.

Specified by:

getMaximalWork in interface StopCondition

Overrides:

getMaximalWork in class ExecutedSymbolicExecutionTreeNodesStopCondition

Parameters:

maxApplications - The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps() in side proofs.

timeout - The defined timeout in ms or -1 if disabled. Can be different to StrategySettings.getTimeout() in side proofs.

proof - The current Proof.

Returns:

The maximal amount of work or 0 if it is unknown.

isGoalAllowed

public boolean isGoalAllowed(int maxApplications,
                             long timeout,
                             Proof proof,
                             long startTime,
                             int countApplied,
                             Goal goal)

Checks if it is allowed to apply the next rule on the selected Goal chosen by the GoalChooser before it is applied. If it is not allowed the apply strategy will stop.

Specified by:

isGoalAllowed in interface StopCondition

Overrides:

isGoalAllowed in class ExecutedSymbolicExecutionTreeNodesStopCondition

Parameters:

maxApplications - The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps() in side proofs.

timeout - The defined timeout in ms or -1 if disabled. Can be different to StrategySettings.getTimeout() in side proofs.

proof - The current Proof.

startTime - The timestamp when the apply strategy has started, computed via System.currentTimeMillis()

countApplied - The number of already applied rules.

goal - The current Goal on which the next rule will be applied.

Returns:

true rule application is allowed, false rule application is not allowed so stop apply strategy

handleNodeLimitNotExceeded

protected void handleNodeLimitNotExceeded(int maxApplications,
                                          long timeout,
                                          Proof proof,
                                          long startTime,
                                          int countApplied,
                                          Goal goal,
                                          Node node,
                                          RuleApp ruleApp,
                                          java.lang.Integer executedNumberOfSetNodes)

Handles the state that the node limit is not exceeded.

Overrides:

handleNodeLimitNotExceeded in class ExecutedSymbolicExecutionTreeNodesStopCondition

Parameters:

maxApplications - The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps() in side proofs.

timeout - The defined timeout in ms or -1 if disabled. Can be different to StrategySettings.getTimeout() in side proofs.

proof - The current Proof.

startTime - The timestamp when the apply strategy has started, computed via System.nanoTime()

countApplied - The number of already applied rules.

goal - The current Goal on which the next rule will be applied.

node - The Node of the current Goal.

ruleApp - The current RuleApp.

executedNumberOfSetNodes - The executed number of SET nodes.

isBreakpointHit

protected boolean isBreakpointHit(SourceElement activeStatement,
                                  RuleApp ruleApp,
                                  Proof proof,
                                  Node node)

Checks if a breakpoint is hit.

Parameters:

activeStatement - the activeStatement of the node

ruleApp - the applied RuleApp

proof - the current proof

node - the current node

Returns:

true at least one breakpoint is hit, false all breakpoints are not hit.

addBreakpoint

public void addBreakpoint(IBreakpoint breakpoint)

Adds a new IBreakpoint.

Specified by:

addBreakpoint in interface IBreakpointStopCondition

Parameters:

breakpoint - The IBreakpoint to add.

removeBreakpoint

public void removeBreakpoint(IBreakpoint breakpoint)

Removes an IBreakpoint.

Specified by:

removeBreakpoint in interface IBreakpointStopCondition

Parameters:

breakpoint - The IBreakpoint to remove.

getBreakpoints

public java.util.Set<IBreakpoint> getBreakpoints()

Returns all available IBreakpoints.

Specified by:

getBreakpoints in interface IBreakpointStopCondition

Returns:

The available IBreakpoints.