de.uka.ilkd.key.symbolic_execution.strategy

Class SymbolicExecutionStrategy

java.lang.Object

de.uka.ilkd.key.strategy.StaticFeatureCollection

de.uka.ilkd.key.strategy.AbstractFeatureStrategy

de.uka.ilkd.key.strategy.JavaCardDLStrategy

de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionStrategy

All Implemented Interfaces:

Named, Feature, Strategy

public class SymbolicExecutionStrategy
extends JavaCardDLStrategy

Strategy to use for symbolic execution.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	SymbolicExecutionStrategy.Factory The StrategyFactory to create instances of SymbolicExecutionStrategy.

Field Summary

Fields

Modifier and Type	Field and Description
static IDefaultStrategyPropertiesFactory	DEFAULT_FACTORY The default factory.
static Name	name The Name of the symbolic execution Strategy.

Fields inherited from class de.uka.ilkd.key.strategy.JavaCardDLStrategy

JAVA_CARD_DL_STRATEGY, strategyProperties

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SymbolicExecutionStrategy(Proof proof, StrategyProperties sp) Constructor.

Method Summary

Modifier and Type	Method and Description
static StrategyProperties	getSymbolicExecutionStrategyProperties(boolean quantifierInstantiationWithSplitting, boolean methodTreatmentContract, boolean loopTreatmentInvariant, boolean blockTreatmentContract, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecks) Returns the default StrategyProperties of symbolic execution.
protected Feature	modalitySideProofFeature() Computes the cost Feature for the ModalitySideProofRule.
Name	name() returns the name of this element
protected Feature	querySideProofFeature() Computes the cost Feature for the QuerySideProofRule.
protected Feature	setupApprovalF()
protected Feature	setupGlobalF(Feature dispatcher)

Methods inherited from class de.uka.ilkd.key.strategy.JavaCardDLStrategy

arithDefOps, computeCost, getCostComputationDispatcher, getInstantiationDispatcher, getServices, instantiateApp, isApprovedApp, isStopAtFirstNonCloseableGoal

Methods inherited from class de.uka.ilkd.key.strategy.AbstractFeatureStrategy

bindRuleSet, bindRuleSet, bindRuleSet, bindRuleSet, clearRuleSetBindings, clearRuleSetBindings, disableInstantiate, enableInstantiate, forEach, getFilterFor, getHeuristic, getProof, ifHeuristics, ifHeuristics, ifHeuristics, instantiate, instantiate, instantiateApp, instantiateTriggeredVariable, oneOf, oneOf

Methods inherited from class de.uka.ilkd.key.strategy.StaticFeatureCollection

add, add, add, add, add, any, applyTF, applyTF, applyTFNonStrict, applyTFNonStrict, atomSmallerThan, blockContractExternalFeature, blockContractInternalFeature, c, contains, countOccurrences, eq, eq, eq, extendsTrans, ifZero, ifZero, ifZero, ifZero, implicitCastNecessary, inftyConst, inftyTermConst, instOf, instOfNonStrict, instOfTriggerVariable, isInstantiated, isSubSortFeature, isTriggerVariableInstantiated, leq, less, let, literalsSmallerThan, longConst, longTermConst, loopContractApplyHead, loopContractExternalFeature, loopContractInternalFeature, loopInvFeature, mergeRuleFeature, methodSpecFeature, monSmallerThan, not, not, op, opSub, opSub, opTerm, opTerm, opTerm, or, or, or, or, or, println, querySpecFeature, rec, sequentContainsNoPrograms, sub, sub, sub, subAt, sum, termSmallerThan

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.strategy.Strategy

updateStrategySettings

Field Detail

name

public static final Name name

The Name of the symbolic execution Strategy.

DEFAULT_FACTORY

public static IDefaultStrategyPropertiesFactory DEFAULT_FACTORY

The default factory.

Constructor Detail

SymbolicExecutionStrategy

private SymbolicExecutionStrategy(Proof proof,
                                  StrategyProperties sp)

Constructor.

Parameters:

proof - The proof.

sp - The StrategyProperties to use.

Method Detail

setupApprovalF

protected Feature setupApprovalF()

Overrides:

setupApprovalF in class JavaCardDLStrategy

setupGlobalF

protected Feature setupGlobalF(Feature dispatcher)

Overrides:

setupGlobalF in class JavaCardDLStrategy

modalitySideProofFeature

protected Feature modalitySideProofFeature()

Computes the cost Feature for the ModalitySideProofRule.

Returns:

The cost Feature for the ModalitySideProofRule.

querySideProofFeature

protected Feature querySideProofFeature()

Computes the cost Feature for the QuerySideProofRule.

Returns:

The cost Feature for the QuerySideProofRule.

name

public Name name()

returns the name of this element

Specified by:

name in interface Named

Overrides:

name in class JavaCardDLStrategy

Returns:

the name of the element

getSymbolicExecutionStrategyProperties

public static StrategyProperties getSymbolicExecutionStrategyProperties(boolean quantifierInstantiationWithSplitting,
                                                                        boolean methodTreatmentContract,
                                                                        boolean loopTreatmentInvariant,
                                                                        boolean blockTreatmentContract,
                                                                        boolean nonExecutionBranchHidingSideProofs,
                                                                        boolean aliasChecks)

Returns the default StrategyProperties of symbolic execution.

Parameters:

quantifierInstantiationWithSplitting - Instantiate quantifiers?

methodTreatmentContract - Use method contracts or inline method bodies otherwise?

loopTreatmentInvariant - Use loop invariants or unrole loops otherwise?

blockTreatmentContract - Block contracts or expand otherwise?

nonExecutionBranchHidingSideProofs - true hide non execution branch labels by side proofs, false do not hide execution branch labels.

aliasChecks - Do alias checks?

Returns:

The default StrategyProperties for symbolic execution.