de.uka.ilkd.key.symbolic_execution.strategy.breakpoint

Class AbstractConditionalBreakpoint

java.lang.Object

de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractBreakpoint

de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractHitCountBreakpoint

de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractConditionalBreakpoint

All Implemented Interfaces:

IBreakpoint

Direct Known Subclasses:

KeYWatchpoint, LineBreakpoint, MethodBreakpoint

public abstract class AbstractConditionalBreakpoint
extends AbstractHitCountBreakpoint

Adds the funtionality to breakpoints to evaluate conditions.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	condition The condition for this Breakpoint (set by user).
private boolean	conditionEnabled The flag if the the condition for the associated Breakpoint is enabled
private java.lang.String	conditionString The condition of the associated breakpoint saved as a String
private KeYJavaType	containerType The KeYJavaType of the container of the element associated with the breakpoint.
private java.util.Set<LocationVariable>	paramVars The list of parameter variables of the method that contains the associated breakpoint
private IProgramMethod	pm The IProgramMethod this Breakpoint lies within
private ProgramVariable	selfVar A ProgramVariable representing the instance the class KeY is working on
private java.util.Set<LocationVariable>	toKeep A list of variables KeY has to hold to evaluate the condition
private java.util.Map<SVSubstitute,SVSubstitute>	variableNamingMap A Map mapping from relevant variables for the condition to their runtime equivalent in KeY
private ImmutableList<ProgramVariable>	varsForCondition A list of ProgramVariables containing all variables that were parsed and have to be possibly replaced during runtime.

Constructor Summary

Constructors

Constructor and Description
AbstractConditionalBreakpoint(int hitCount, IProgramMethod pm, Proof proof, boolean enabled, boolean conditionEnabled, int methodStart, int methodEnd, KeYJavaType containerType) Creates a new AbstractConditionalBreakpoint.

Method Summary

Modifier and Type	Method and Description
private Term	computeTermForCondition(java.lang.String condition) Computes the Term that can be evaluated, from the user given condition
protected boolean	conditionMet(RuleApp ruleApp, Proof proof, Node node) Checks if the condition, that was given by the user, evaluates to true with the current of the proof
private void	freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScope) removes all stored parameters in to Keep when the ruleApp on the current node would induce a method return
Term	getCondition() Returns the condition of the associated Breakpoint.
java.lang.String	getConditionString() Returns the condition represented as a String.
private java.util.Map<SVSubstitute,SVSubstitute>	getOldMap() Returns a map containing the same entries as the variableNamingMap changes in one map do not effect the other map
IProgramMethod	getPm()
ProgramVariable	getSelfVar()
protected abstract StatementBlock	getStatementBlock(StatementContainer statementContainer) For a given StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself.
java.util.Set<LocationVariable>	getToKeep() Returns the variables KeY should keep to evaluate the condition.
java.util.Map<SVSubstitute,SVSubstitute>	getVariableNamingMap()
ImmutableList<ProgramVariable>	getVarsForCondition()
boolean	isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node) Determines if the breakpoint represented by this BreakpointStopConition is triggered.
boolean	isConditionEnabled() Checks if the condition for the associated Breakpoint is enabled.
protected abstract boolean	isInScope(Node node) Checks if the statement of a given Node is in the scope of this breakpoint.
protected abstract boolean	isInScopeForCondition(Node node) Checks if the statement of a given Node is in the scope of this breakpoint.
private void	putValuesFromGlobalVars(ProgramVariable varForCondition, Node node, boolean inScope) put values in toKeep and variableNamingMap that can be found in the global variables of the node
private void	putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope, java.util.Map<SVSubstitute,SVSubstitute> oldMap, RuleApp ruleApp) put relevant values from the current nodes renamings in toKeep and variableNamingMap
protected void	refreshVarMaps(RuleApp ruleApp, Node node) Modifies toKeep and variableNamingMap to hold the correct parameters after execution of the given ruleApp on the given node
private ImmutableList<ProgramVariable>	saveAddVariable(LocationVariable x, ImmutableList<ProgramVariable> varsForCondition)
void	setCondition(java.lang.String condition) Sets the condition to the Term that is parsed from the given String.
void	setConditionEnabled(boolean conditionEnabled) Sets the new conditionEnabled value.
void	setPm(IProgramMethod pm)
void	setSelfVar(ProgramVariable selfVar)
void	setVariableNamingMap(java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap)
void	setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition)
void	updateState(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal) This method is called from StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal) and can be used to update the state of the IBreakpoint.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractHitCountBreakpoint

getHitCount, hitcountExceeded, setHitCount

Methods inherited from class de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractBreakpoint

getProof, isEnabled, setEnabled

Methods inherited from class java.lang.Object

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

Field Detail

condition

private Term condition

The condition for this Breakpoint (set by user).

conditionEnabled

private boolean conditionEnabled

The flag if the the condition for the associated Breakpoint is enabled

conditionString

private java.lang.String conditionString

The condition of the associated breakpoint saved as a String

varsForCondition

private ImmutableList<ProgramVariable> varsForCondition

A list of ProgramVariables containing all variables that were parsed and have to be possibly replaced during runtime.

containerType

private KeYJavaType containerType

The KeYJavaType of the container of the element associated with the breakpoint.

toKeep

private java.util.Set<LocationVariable> toKeep

A list of variables KeY has to hold to evaluate the condition

variableNamingMap

private java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap

A Map mapping from relevant variables for the condition to their runtime equivalent in KeY

paramVars

private java.util.Set<LocationVariable> paramVars

The list of parameter variables of the method that contains the associated breakpoint

selfVar

private ProgramVariable selfVar

A ProgramVariable representing the instance the class KeY is working on

pm

private IProgramMethod pm

The IProgramMethod this Breakpoint lies within

Constructor Detail

AbstractConditionalBreakpoint

public AbstractConditionalBreakpoint(int hitCount,
                                     IProgramMethod pm,
                                     Proof proof,
                                     boolean enabled,
                                     boolean conditionEnabled,
                                     int methodStart,
                                     int methodEnd,
                                     KeYJavaType containerType)

Creates a new AbstractConditionalBreakpoint. Call setCondition immediately after calling the constructor!

Parameters:

hitCount - the number of hits after which the execution should hold at this breakpoint

pm - the IProgramMethod representing the Method which the Breakpoint is located at

proof - the Proof that will be executed and should stop

enabled - flag if the Breakpoint is enabled

conditionEnabled - flag if the condition is enabled

methodStart - the line the containing method of this breakpoint starts at

methodEnd - the line the containing method of this breakpoint ends at

containerType - the type of the element containing the breakpoint

Method Detail

updateState

public void updateState(int maxApplications,
                        long timeout,
                        Proof proof,
                        long startTime,
                        int countApplied,
                        Goal goal)

This method is called from StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal) and can be used to update the state of the IBreakpoint.

Specified by:

updateState in interface IBreakpoint

Overrides:

updateState in class AbstractBreakpoint

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.

putValuesFromGlobalVars

private void putValuesFromGlobalVars(ProgramVariable varForCondition,
                                     Node node,
                                     boolean inScope)

put values in toKeep and variableNamingMap that can be found in the global variables of the node

Parameters:

varForCondition -

node -

inScope -

getOldMap

private java.util.Map<SVSubstitute,SVSubstitute> getOldMap()

Returns a map containing the same entries as the variableNamingMap changes in one map do not effect the other map

Returns:

the cloned map

freeVariablesAfterReturn

private void freeVariablesAfterReturn(Node node,
                                      RuleApp ruleApp,
                                      boolean inScope)

removes all stored parameters in to Keep when the ruleApp on the current node would induce a method return

Parameters:

node -

ruleApp -

inScope -

putValuesFromRenamings

private void putValuesFromRenamings(ProgramVariable varForCondition,
                                    Node node,
                                    boolean inScope,
                                    java.util.Map<SVSubstitute,SVSubstitute> oldMap,
                                    RuleApp ruleApp)

put relevant values from the current nodes renamings in toKeep and variableNamingMap

Parameters:

varForCondition - the variable that might be relevant for the condition

node - the current

inScope - the flag to determine if the current statement is in the scope of the breakpoint

oldMap - the oldMap variableNamings

refreshVarMaps

protected void refreshVarMaps(RuleApp ruleApp,
                              Node node)

Modifies toKeep and variableNamingMap to hold the correct parameters after execution of the given ruleApp on the given node

Parameters:

ruleApp - the applied rule app

nodethe - current node

computeTermForCondition

private Term computeTermForCondition(java.lang.String condition)
                              throws SLTranslationException

Computes the Term that can be evaluated, from the user given condition

Parameters:

condition - the condition given by the user

Returns:

the Term that represents the condition

Throws:

SLTranslationException - if the Term could not be parsed

conditionMet

protected boolean conditionMet(RuleApp ruleApp,
                               Proof proof,
                               Node node)

Checks if the condition, that was given by the user, evaluates to true with the current of the proof

Parameters:

ruleApp - the RuleApp to be executed next

proof - the current Proof

node - the current Node

Returns:

true if the condition evaluates to true

isBreakpointHit

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

Determines if the breakpoint represented by this BreakpointStopConition is triggered. Override this method in order to suspend execution when a breakpoint is hit.

Specified by:

isBreakpointHit in interface IBreakpoint

Overrides:

isBreakpointHit in class AbstractHitCountBreakpoint

Parameters:

activeStatement - the activeStatement of the node

ruleApp - the applied RuleApp

proof - the current proof

node - the current node

Returns:

true if execution should hold

getStatementBlock

protected abstract StatementBlock getStatementBlock(StatementContainer statementContainer)

For a given StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself.

Parameters:

statementContainer - the StatementContainer to build the block from

Returns:

the StatementBlock representing the container without the line below the Breakpoint

isInScope

protected abstract boolean isInScope(Node node)

Checks if the statement of a given Node is in the scope of this breakpoint.

Parameters:

node - the Node to be checked

Returns:

true if the node represents a statement in the scope of this breakpoint.

isInScopeForCondition

protected abstract boolean isInScopeForCondition(Node node)

Checks if the statement of a given Node is in the scope of this breakpoint.

Parameters:

node - the Node to be checked

Returns:

true if the node represents a statement in the scope of this breakpoint.

saveAddVariable

private ImmutableList<ProgramVariable> saveAddVariable(LocationVariable x,
                                                       ImmutableList<ProgramVariable> varsForCondition)

setConditionEnabled

public void setConditionEnabled(boolean conditionEnabled)

Sets the new conditionEnabled value.

Parameters:

conditionEnabled - the new value

getCondition

public Term getCondition()

Returns the condition of the associated Breakpoint.

Returns:

the condition of the associated Breakpoint

isConditionEnabled

public boolean isConditionEnabled()

Checks if the condition for the associated Breakpoint is enabled.

Parameters:

conditionEnabled - true if the condition for the associated Breakpoint is enabled

setCondition

public void setCondition(java.lang.String condition)
                  throws SLTranslationException

Sets the condition to the Term that is parsed from the given String.

Parameters:

condition - the String to be parsed

Throws:

SLTranslationException - if the parsing failed

getConditionString

public java.lang.String getConditionString()

Returns the condition represented as a String.

Returns:

the condition represented as a String

getToKeep

public java.util.Set<LocationVariable> getToKeep()

Returns the variables KeY should keep to evaluate the condition.

Returns:

the variables KeY should keep to evaluate the condition

getVariableNamingMap

public java.util.Map<SVSubstitute,SVSubstitute> getVariableNamingMap()

Returns:

the variableNamingMap

setVariableNamingMap

public void setVariableNamingMap(java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap)

Parameters:

variableNamingMap - the variableNamingMap to set

getSelfVar

public ProgramVariable getSelfVar()

Returns:

the selfVar

setSelfVar

public void setSelfVar(ProgramVariable selfVar)

Parameters:

selfVar - the selfVar to set

getVarsForCondition

public ImmutableList<ProgramVariable> getVarsForCondition()

Returns:

the varsForCondition

setVarsForCondition

public void setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition)

Parameters:

varsForCondition - the varsForCondition to set

getPm

public IProgramMethod getPm()

Returns:

the pm

setPm

public void setPm(IProgramMethod pm)

Parameters:

pm - the pm to set