de.uka.ilkd.key.symbolic_execution.po

Class ProgramMethodSubsetPO

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractPO

de.uka.ilkd.key.proof.init.AbstractOperationPO

de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO

de.uka.ilkd.key.symbolic_execution.po.ProgramMethodSubsetPO

All Implemented Interfaces:

IPersistablePO, ProofOblInput

public class ProgramMethodSubsetPO
extends ProgramMethodPO

This proof obligation executes selected statements of the body of a given IProgramMethod. The statements are selected by its source location. All statements which ends in the given source range ]startPosition, endPosition] are executed.

To select statements by its end position is required, because KeY's recorder includes also leading space and leading comments into a statements position. Another drawback is that the end position of the previous statement is exactly the start position of the following statement.

Imagine the following snippet:

 int x = 1; // from 3/59 to 4/16
 int y = 2; // from 4/16 to 5/16
 int z = 3; // from 5/16 to 6/16
 

To execute only the last two statements a user would select intuitively the source range 5/0 to 6/16 (the text without leading white space) which matches exactly the used selection definition.

The generated Sequent has the following form:

 
 ==>
 <generalAssumptions> &
 <preconditions>
 ->
 <updatesToStoreInitialValues>
 <modalityStart>
 exc=null;try {<methodFrame><selectedStatements>}catch(java.lang.Exception e) {exc = e}
 <modalityEnd>
 (exc = null & <postconditions > & <optionalUninterpretedPredicate>)
 
 

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.proof.init.IPersistablePO

IPersistablePO.LoadedPOContainer

Field Summary

Fields

Modifier and Type	Field and Description
private Position	endPosition The end position.
private Position	startPosition The start position.
private UndeclaredProgramVariableCollector	undeclaredVariableCollector Contains all undeclared variables used in the method part to execute.

Fields inherited from class de.uka.ilkd.key.proof.init.AbstractOperationPO

proofConfig

Fields inherited from class de.uka.ilkd.key.proof.init.AbstractPO

environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb

Fields inherited from interface de.uka.ilkd.key.proof.init.IPersistablePO

PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME

Constructor Summary

Constructors

Constructor and Description
ProgramMethodSubsetPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition, Position startPosition, Position endPosition) Constructor.
ProgramMethodSubsetPO(InitConfig initConfig, java.lang.String name, IProgramMethod pm, java.lang.String precondition, Position startPosition, Position endPosition, boolean addUninterpretedPredicate, boolean addSymbolicExecutionLabel) Constructor.

Method Summary

Modifier and Type	Method and Description
protected Term	buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, ImmutableList<ProgramVariable> paramVars, java.util.List<LocationVariable> heaps, Services proofServices) Builds the "general assumption".
protected ImmutableList<StatementBlock>	buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services) Builds the code to execute in different statement blocks. 1. code to execute before the try block 2. code to execute in the try block 3. code to execute in the catch block 4. code to execute in the finally block
protected void	collectStatementsToExecute(java.util.List<Statement> toFill, StatementContainer container) Collects recursive the Statements which are in the given source range defined by startPosition and endPosition.
protected static ImmutableList<ProgramVariable>	convert(java.util.Collection<LocationVariable> c) Converts the given Collection into an ImmutableList.
protected boolean	endsWithReturn(Statement[] statements) Checks if the last statement is a Return statement.
protected Term	ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, ProgramVariable exceptionVar, java.lang.String name, Services proofServices) Creates AbstractOperationPO.uninterpretedPredicate.
boolean	equals(java.lang.Object obj)
void	fillSaveProperties(java.util.Properties properties) This method is called by a ProofSaver to store the proof specific settings in the given Properties.
Position	getEndPosition() Returns the end position.
protected static Position	getEndPosition(java.util.Properties properties) Extracts the end position from the given Properties.
protected Term	getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services) Creates the precondition.
Position	getStartPosition() Returns the start position.
protected static Position	getStartPosition(java.util.Properties properties) Extracts the start position from the given Properties.
int	hashCode()
static IPersistablePO.LoadedPOContainer	loadFrom(InitConfig initConfig, java.util.Properties properties) Instantiates a new proof obligation with the given settings.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO

buildFrameClause, buildPOName, generateMbyAtPreDef, getCalleeKeYJavaType, getContainerType, getGlobalDefs, getPost, getPrecondition, getPrecondition, getProgramMethod, getProgramMethod, getProgramMethodSignature, getTerminationMarker, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, isTransactionApplicable

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractOperationPO

addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit, readProblem

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractPO

assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getName, getPO, implies, name, register, register, register, selectClassAxioms

Methods inherited from class java.lang.Object

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

Field Detail

undeclaredVariableCollector

private UndeclaredProgramVariableCollector undeclaredVariableCollector

Contains all undeclared variables used in the method part to execute.

startPosition

private Position startPosition

The start position.

endPosition

private Position endPosition

The end position.

Constructor Detail

ProgramMethodSubsetPO

public ProgramMethodSubsetPO(InitConfig initConfig,
                             java.lang.String name,
                             IProgramMethod pm,
                             java.lang.String precondition,
                             Position startPosition,
                             Position endPosition)

Constructor.

Parameters:

initConfig - The InitConfig to use.

name - The name to use.

pm - The IProgramMethod to execute code parts from.

precondition - An optional precondition to use.

startPosition - The start position.

endPosition - The end position.

ProgramMethodSubsetPO

public ProgramMethodSubsetPO(InitConfig initConfig,
                             java.lang.String name,
                             IProgramMethod pm,
                             java.lang.String precondition,
                             Position startPosition,
                             Position endPosition,
                             boolean addUninterpretedPredicate,
                             boolean addSymbolicExecutionLabel)

Constructor.

Parameters:

initConfig - The InitConfig to use.

name - The name to use.

pm - The IProgramMethod to execute code parts from.

precondition - An optional precondition to use.

startPosition - The start position.

endPosition - The end position.

addUninterpretedPredicate - true postcondition contains uninterpreted predicate, false uninterpreted predicate is not contained in postcondition.

addSymbolicExecutionLabel - true to add the SymbolicExecutionTermLabel to the modality, false to not label the modality.

Method Detail

buildOperationBlocks

protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
                                                             ProgramVariable selfVar,
                                                             ProgramVariable resultVar,
                                                             Services services)

Builds the code to execute in different statement blocks. 1. code to execute before the try block 2. code to execute in the try block 3. code to execute in the catch block 4. code to execute in the finally block

Overrides:

buildOperationBlocks in class ProgramMethodPO

Parameters:

formalParVars - Arguments from formal parameters for method call.

selfVar - The self variable.

resultVar - The result variable.

services - services instance

Returns:

operation blocks as statement blocks

collectStatementsToExecute

protected void collectStatementsToExecute(java.util.List<Statement> toFill,
                                          StatementContainer container)

Collects recursive the Statements which are in the given source range defined by startPosition and endPosition.

Parameters:

toFill - The result List to fill.

container - The StatementContainer to seach in.

endsWithReturn

protected boolean endsWithReturn(Statement[] statements)

Checks if the last statement is a Return statement.

Parameters:

statements - The statements to check.

Returns:

true last statement is Return, false statements are empty or last statement is something else.

getPre

protected Term getPre(java.util.List<LocationVariable> modHeaps,
                      ProgramVariable selfVar,
                      ImmutableList<ProgramVariable> paramVars,
                      java.util.Map<LocationVariable,LocationVariable> atPreVars,
                      Services services)

Creates the precondition.

Overrides:

getPre in class ProgramMethodPO

Parameters:

modHeaps - The heaps.

selfVar - The self variable.

paramVars - The parameters ProgramVariables.

atPreVars - Mapping of LocationVariable to the LocationVariable which contains the initial value.

services - The Services to use.

Returns:

The Term representing the precondition.

buildFreePre

protected Term buildFreePre(ProgramVariable selfVar,
                            KeYJavaType selfKJT,
                            ImmutableList<ProgramVariable> paramVars,
                            java.util.List<LocationVariable> heaps,
                            Services proofServices)

Builds the "general assumption".

Overrides:

buildFreePre in class AbstractOperationPO

Parameters:

selfVar - The self variable.

selfKJT - The KeYJavaType of the self variable.

paramVars - The parameters ProgramVariables.

heaps - The heaps.

proofServices - The services instance.

Returns:

The Term containing the general assumptions.

ensureUninterpretedPredicateExists

protected Term ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
                                                  ImmutableList<LocationVariable> formalParamVars,
                                                  ProgramVariable exceptionVar,
                                                  java.lang.String name,
                                                  Services proofServices)

Creates AbstractOperationPO.uninterpretedPredicate.

Overrides:

ensureUninterpretedPredicateExists in class AbstractOperationPO

Parameters:

paramVars - The parameters ProgramVariables.

formalParamVars - The formal parameters LocationVariables.

exceptionVar - The exception variable.

name - The name of the uninterpreted predicate.

proofServices - services instance.

Returns:

The created uninterpreted predicate.

convert

protected static ImmutableList<ProgramVariable> convert(java.util.Collection<LocationVariable> c)

Converts the given Collection into an ImmutableList.

Parameters:

c - The Collection to convert.

Returns:

The created ImmutableList.

hashCode

public int hashCode()

Overrides:

hashCode in class ProgramMethodPO

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class ProgramMethodPO

getStartPosition

public Position getStartPosition()

Returns the start position.

Returns:

The start position.

getEndPosition

public Position getEndPosition()

Returns the end position.

Returns:

The end position.

fillSaveProperties

public void fillSaveProperties(java.util.Properties properties)
                        throws java.io.IOException

This method is called by a ProofSaver to store the proof specific settings in the given Properties. The stored settings have to contain all information required to instantiate the proof obligation again and this instance should create the same Sequent (if code and specifications are unchanged).

Specified by:

fillSaveProperties in interface IPersistablePO

Overrides:

fillSaveProperties in class ProgramMethodPO

Parameters:

properties - The Properties to fill with the proof obligation specific settings.

Throws:

java.io.IOException - Occurred Exception.

loadFrom

public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig,
                                                        java.util.Properties properties)
                                                 throws java.io.IOException

Instantiates a new proof obligation with the given settings.

Parameters:

initConfig - The already load InitConfig.

properties - The settings of the proof obligation to instantiate.

Returns:

The instantiated proof obligation.

Throws:

java.io.IOException - Occurred Exception.

getStartPosition

protected static Position getStartPosition(java.util.Properties properties)
                                    throws java.io.IOException

Extracts the start position from the given Properties.

Parameters:

properties - The proof obligation settings to read from.

Returns:

The defined start Position.

Throws:

java.io.IOException - Occurred Exception if it was not possible to read the start position.

getEndPosition

protected static Position getEndPosition(java.util.Properties properties)
                                  throws java.io.IOException

Extracts the end position from the given Properties.

Parameters:

properties - The proof obligation settings to read from.

Returns:

The defined end Position.

Throws:

java.io.IOException - Occurred Exception if it was not possible to read the end position.