de.uka.ilkd.key.symbolic_execution.model.impl

Class ExecutionVariable

java.lang.Object

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionVariable

de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionVariable

All Implemented Interfaces:

IExecutionElement, IExecutionVariable

Direct Known Subclasses:

ExecutionAllArrayIndicesVariable

public class ExecutionVariable
extends AbstractExecutionVariable

The default implementation of IExecutionVariable.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private ExecutionValue	lengthValue The ExecutionValue from which the array length was computed.
private IExecutionNode<?>	parentNode The parent IExecutionNode which provides this ExecutionVariable.
private ExecutionValue[]	values The possible values of this IExecutionValue.

Constructor Summary

Constructors

Constructor and Description
ExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, ExecutionValue parentValue, IProgramVariable programVariable, Term additionalCondition) Constructor for a "normal" child value.
ExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, ExecutionValue parentValue, Term arrayIndex, ExecutionValue lengthValue, Term additionalCondition) Constructor for an array cell value.
ExecutionVariable(IExecutionNode<?> parentNode, Node proofNode, PosInOccurrence modalityPIO, IProgramVariable programVariable, Term additionalCondition) Constructor for a "normal" value.

Method Summary

Modifier and Type	Method and Description
protected Term	computeValueCondition(TermBuilder tb, java.util.List<Goal> valueGoals, InitConfig initConfig) Computes the combined path condition of all Goals which is the or combination of each path condition per Goal.
Term	createSelectTerm() Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().
ExecutionValue	getLengthValue() Returns the ExecutionValue from which the array length was computed.
IExecutionNode<?>	getParentNode() Returns the parent IExecutionNode which provides this ExecutionVariable.
ExecutionValue	getParentValue() Returns the parent IExecutionValue if available.
ExecutionValue[]	getValues() Returns the possible values of this IExecutionVariable.
protected void	groupGoalsByValue(ImmutableList<Goal> goals, Operator operator, Term siteProofSelectTerm, Term siteProofCondition, java.util.Map<Term,java.util.List<Goal>> valueMap, java.util.List<Goal> unknownValues, Services services) Groups all Goals which provides the same value.
protected ExecutionValue[]	instantiateValuesFromSideProof(InitConfig initConfig, Services services, TermBuilder tb, ApplyStrategyInfo info, Operator resultOperator, Term siteProofSelectTerm, Term siteProofCondition) Analyzes the side proof defined by the ApplyStrategyInfo and creates ExecutionValues from it.
protected boolean	isValidValue(Term value) Checks if the given Term represents a valid value.
protected ExecutionValue[]	lazyComputeValues() Computes the value for getValues() lazily when the method is called the first time.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionVariable

getAdditionalCondition, getArrayIndex, getArrayIndexString, getElementType, getModalityPIO, getProgramVariable, isArrayIndex, lazyComputeName

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

parentNode

private final IExecutionNode<?> parentNode

The parent IExecutionNode which provides this ExecutionVariable.

lengthValue

private final ExecutionValue lengthValue

The ExecutionValue from which the array length was computed.

values

private ExecutionValue[] values

The possible values of this IExecutionValue.

Constructor Detail

ExecutionVariable

public ExecutionVariable(IExecutionNode<?> parentNode,
                         Node proofNode,
                         PosInOccurrence modalityPIO,
                         IProgramVariable programVariable,
                         Term additionalCondition)

Constructor for a "normal" value.

Parameters:

parentNode - The parent IExecutionNode which provides this ExecutionVariable.

programVariable - The represented IProgramVariable which value is shown.

additionalCondition - An optional additional condition to consider.

ExecutionVariable

public ExecutionVariable(IExecutionNode<?> parentNode,
                         Node proofNode,
                         PosInOccurrence modalityPIO,
                         ExecutionValue parentValue,
                         IProgramVariable programVariable,
                         Term additionalCondition)

Constructor for a "normal" child value.

Parameters:

settings - The ITreeSettings to use.

parentNode - The parent IExecutionNode which provides this ExecutionVariable.

parentValue - The parent ExecutionValue or null if not available.

programVariable - The represented IProgramVariable which value is shown.

additionalCondition - An optional additional condition to consider.

ExecutionVariable

public ExecutionVariable(IExecutionNode<?> parentNode,
                         Node proofNode,
                         PosInOccurrence modalityPIO,
                         ExecutionValue parentValue,
                         Term arrayIndex,
                         ExecutionValue lengthValue,
                         Term additionalCondition)

Constructor for an array cell value.

Parameters:

parentNode - The parent IExecutionNode which provides this ExecutionVariable.

parentValue - The parent ExecutionValue or null if not available.

arrayIndex - The index in the parent array.

lengthValue - The ExecutionValue from which the array length was computed.

additionalCondition - An optional additional condition to consider.

Method Detail

getValues

public ExecutionValue[] getValues()
                           throws ProofInputException

Returns the possible values of this IExecutionVariable.

Returns:

The possible values of this IExecutionVariable.

Throws:

ProofInputException

lazyComputeValues

protected ExecutionValue[] lazyComputeValues()
                                      throws ProofInputException

Computes the value for getValues() lazily when the method is called the first time.

Throws:

ProofInputException - Occurred Exception.

instantiateValuesFromSideProof

protected ExecutionValue[] instantiateValuesFromSideProof(InitConfig initConfig,
                                                          Services services,
                                                          TermBuilder tb,
                                                          ApplyStrategyInfo info,
                                                          Operator resultOperator,
                                                          Term siteProofSelectTerm,
                                                          Term siteProofCondition)
                                                   throws ProofInputException

Analyzes the side proof defined by the ApplyStrategyInfo and creates ExecutionValues from it.

Parameters:

initConfig - The InitConfig of the side proof.

services - The Services of the side proof.

tb - The TermBuilder of the side proof.

info - The side proof.

resultOperator - The Operator of the result predicate.

siteProofSelectTerm - The queried value.

siteProofCondition - The condition under which the value is queried.

Returns:

The created ExecutionValue instances.

Throws:

ProofInputException - Occurred Exception.

isValidValue

protected boolean isValidValue(Term value)

Checks if the given Term represents a valid value.

Parameters:

value - The value to check.

Returns:

true valid value, false invalid value to be ignored.

groupGoalsByValue

protected void groupGoalsByValue(ImmutableList<Goal> goals,
                                 Operator operator,
                                 Term siteProofSelectTerm,
                                 Term siteProofCondition,
                                 java.util.Map<Term,java.util.List<Goal>> valueMap,
                                 java.util.List<Goal> unknownValues,
                                 Services services)
                          throws ProofInputException

Groups all Goals which provides the same value.

Parameters:

goals - All available Goals to group.

operator - The Operator of the Term which provides the value.

services - The Services to use.

Throws:

ProofInputException

computeValueCondition

protected Term computeValueCondition(TermBuilder tb,
                                     java.util.List<Goal> valueGoals,
                                     InitConfig initConfig)
                              throws ProofInputException

Computes the combined path condition of all Goals which is the or combination of each path condition per Goal.

Parameters:

tb - The TermBuilder to use passed to ensure that it is still available even if the Proof is disposed in between.

valueGoals - The Goals to compute combined path condition for.

initConfig - The InitConfig to use.

Returns:

The combined path condition.

Throws:

ProofInputException - Occurred Exception.

createSelectTerm

public Term createSelectTerm()

Creates recursive a term which can be used to determine the value of IExecutionVariable.getProgramVariable().

Returns:

The created term.

getParentValue

public ExecutionValue getParentValue()

Returns the parent IExecutionValue if available.

Specified by:

getParentValue in interface IExecutionVariable

Overrides:

getParentValue in class AbstractExecutionVariable

Returns:

The parent IExecutionValue if available and null otherwise.

getParentNode

public IExecutionNode<?> getParentNode()

Returns the parent IExecutionNode which provides this ExecutionVariable.

Returns:

The parent IExecutionNode which provides this ExecutionVariable.

getLengthValue

public ExecutionValue getLengthValue()

Returns the ExecutionValue from which the array length was computed.

Returns:

The ExecutionValue from which the array length was computed.