public final class SymbolicExecutionUtil
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult
The result of
searchContractPostOrExcPostExceptionVariable(Node, Services) . |
private static class |
SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId
Utility class used to find the maximal modality Term
used by
findModalityWithMaxSymbolicExecutionLabelId(Term) . |
static class |
SymbolicExecutionUtil.SiteProofVariableValueInput
Helper class which represents the return value of
ExecutionMethodReturn#createExtractReturnVariableValueSequent(TypeReference, ReferencePrefix, Node, IProgramVariable) and
ExecutionMethodReturn#createExtractVariableValueSequent(IExecutionContext, Node, IProgramVariable) . |
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
CHOICE_SETTING_RUNTIME_EXCEPTIONS
Key for the choice option "runtimeExceptions".
|
static java.lang.String |
CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW
Value in choice option "runtimeExceptions" to allow exceptions.
|
static java.lang.String |
CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN
Value in choice option "runtimeExceptions" to ban exceptions.
|
static TermLabel |
LOOP_BODY_LABEL
Label attached to the modality which executes a loop body in branch
"Body Preserves Invariant" of applied "Loop Invariant" rules.
|
static Name |
LOOP_BODY_LABEL_NAME
Name of
LOOP_BODY_LABEL . |
static TermLabel |
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
Label attached to the implication when a loop body execution terminated
normally without any exceptions, returns or breaks in branch
"Body Preserves Invariant" of applied "Loop Invariant" rules to show the
loop invariant.
|
static Name |
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
Name of
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL . |
static TermLabel |
RESULT_LABEL
Label attached to a
Term to evaluate in a side proof. |
static Name |
RESULT_LABEL_NAME
Name of
RESULT_LABEL . |
Modifier | Constructor and Description |
---|---|
private |
SymbolicExecutionUtil()
Forbid instances.
|
Modifier and Type | Method and Description |
---|---|
private static Term |
addLabelRecursiveToNonSkolem(TermFactory tf,
Term term,
TermLabel label)
|
static boolean |
canComputeVariables(IExecutionNode<?> node,
Services services)
Checks if it is right now possible to compute the variables of the given
IExecutionNode
via IExecutionNode.getVariables() . |
private static boolean |
checkNull(Node node,
Term additionalAntecedent,
Term newSuccedent,
boolean nullExpected)
|
private static boolean |
checkReplaceTerm(Term toCheck,
PosInOccurrence posInOccurrence,
Term replaceTerm)
|
static int |
checkSkolemEquality(SequentFormula sf)
Checks if the given
SequentFormula is a skolem equality. |
static int |
checkSkolemEquality(Term term)
Checks if the given
Term is a skolem equality. |
static java.util.List<IProgramVariable> |
collectAllElementaryUpdateTerms(Node node)
Collects all
IProgramVariable used in ElementaryUpdate s. |
private static void |
collectContractPreconditions(Services services,
SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult search,
java.util.List<Term> normalConditions,
java.util.List<Term> exceptinalConditions)
Collects the preconditions of an applied operation contract.
|
static ImmutableList<Term> |
collectElementaryUpdates(Term term)
Collects the
ElementaryUpdate s in the given Term . |
static ImmutableList<Goal> |
collectGoalsInSubtree(IExecutionElement executionElement)
Collects all
Goal s in the subtree of the given IExecutionElement . |
static ImmutableList<Goal> |
collectGoalsInSubtree(Node node)
|
private static java.util.Set<Term> |
collectSkolemConstants(Sequent sequent,
Term term)
Collects all contained skolem
Term s which fulfill
isSkolemConstant(Term) as well as the skolem constants
used in the find once recursive. |
private static java.util.Set<Term> |
collectSkolemConstantsNonRecursive(Term term)
Collects all contained skolem
Term s which fulfill
isSkolemConstant(Term) . |
private static void |
collectSpecifcationCasesPreconditions(Term normalExcDefinition,
Term exceptionalExcDefinition,
Term term,
java.util.List<Term> normalConditions,
java.util.List<Term> exceptinalConditions)
Collects recursively the preconditions of specification cases.
|
private static Term |
computeBlockContractBuiltInRuleAppBranchCondition(Node parent,
Node node,
boolean simplify,
boolean improveReadability)
Computes the branch condition of the given
Node which was constructed by an
AbstractBlockContractBuiltInRuleApp . |
static Term |
computeBranchCondition(Node node,
boolean simplify,
boolean improveReadability)
Computes the branch condition of the given
Node . |
private static Term |
computeContractRuleAppBranchCondition(Node parent,
Node node,
boolean simplify,
boolean improveReadability)
Computes the branch condition of the given
Node which was constructed by a ContractRuleApp . |
private static Term |
computeLoopInvariantBuiltInRuleAppBranchCondition(Node parent,
Node node,
boolean simplify,
boolean improveReadability)
Computes the branch condition of the given
Node which was constructed by a LoopInvariantBuiltInRuleApp . |
static Term |
computePathCondition(Node node,
boolean simplify,
boolean improveReadability)
Computes the path condition of the given
Node . |
static Term |
computePathCondition(Node parentNode,
Node childNode,
boolean simplify,
boolean improveReadability)
Computes the path condition between the given
Node s. |
static ImmutableList<Term> |
computeRootElementaryUpdates(Node root)
Computes the initial
ElementaryUpdate s on the given root Node . |
static Pair<java.lang.Integer,SourceElement> |
computeSecondStatement(RuleApp ruleApp)
Computes the call stack size and the second statement
similar to
NodeInfo.computeActiveStatement(SourceElement) . |
static int |
computeStackSize(RuleApp ruleApp)
|
private static Term |
computeTacletAppBranchCondition(Node parent,
Node node,
boolean simplify,
boolean improveReadability)
|
static boolean |
containsStatement(ProgramElement toSearchIn,
SourceElement toSearch,
Services services)
Checks if the given
ProgramElement contains the given SourceElement . |
static boolean |
containsSymbolicExecutionLabel(Term term)
Checks if the
Term or one of its sub terms contains
a symbolic execution label. |
static IExecutionVariable[] |
createAllExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionConstraint[] |
createExecutionConstraints(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
IExecutionConstraint s. |
static IExecutionVariable[] |
createExecutionVariables(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
createExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
createExecutionVariables(IExecutionNode<?> node,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
createExtractReturnVariableValueSequent(Services services,
IExecutionContext context,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
createExtractTermSequent(Services sideProofServices,
Node node,
PosInOccurrence pio,
Term additionalConditions,
Term term,
boolean keepUpdates)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
createExtractVariableValueSequent(Services services,
Node node,
PosInOccurrence pio,
Term additionalConditions,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static NotationInfo |
createNotationInfo(IExecutionElement element)
Creates the
NotationInfo for the given IExecutionElement . |
static NotationInfo |
createNotationInfo(Node node)
Creates the
NotationInfo for the given Node . |
static NotationInfo |
createNotationInfo(Proof proof)
Creates the
NotationInfo for the given Proof . |
static Term |
createSelectTerm(IExecutionVariable variable)
Creates recursive a term which can be used to determine the value
of
#getProgramVariable() . |
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term newSuccedent)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static boolean |
equalsWithPosition(SourceElement first,
SourceElement second)
Compares the given
SourceElement s including their PositionInfo s. |
private static Term |
evaluateInSideProof(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String splittingOption)
|
static IProgramVariable |
extractExceptionVariable(Proof proof)
Extracts the exception variable which is used to check if the executed program in proof terminates normally.
|
protected static ImmutableArray<Term> |
extractValueFromUpdate(Term term,
IProgramVariable variable)
Utility method to extract the value of the
IProgramVariable
from the given update term. |
private static Term |
findInnerMostSelect(Term term,
Services services) |
static Node |
findMethodCallNode(Node node,
PosInOccurrence pio)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static PosInOccurrence |
findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent,
boolean inAntec)
Searches the modality
Term with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Semisequent . |
static PosInOccurrence |
findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)
Searches the modality
PosInOccurrence with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Sequent . |
static PosInTerm |
findModalityWithMaxSymbolicExecutionLabelId(Term term)
Searches the modality
PosInTerm with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Term . |
static PosInOccurrence |
findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent,
boolean inAntec)
Searches the modality
PosInOccurrence with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Semisequent . |
static PosInOccurrence |
findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)
Searches the modality
PosInOccurrence with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Sequent . |
static PosInTerm |
findModalityWithMinSymbolicExecutionLabelId(Term term)
Searches the modality
PosInTerm with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Term . |
static Node |
findParentSetNode(Node node)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp) ). |
private static Term |
findReplacement(Semisequent semisequent,
PosInOccurrence posInOccurrence,
Term replaceTerm)
|
static IProgramVariable |
findSelfTerm(Node node,
PosInOccurrence pio)
|
private static java.util.List<Term> |
findSkolemReplacements(Sequent sequent,
Term skolemConstant,
Term skolemEquality)
Utility method of
replaceSkolemConstants(Sequent, Term, Services) to
find all equality parts of the given skolem constant. |
static Term |
followPosInOccurrence(PosInOccurrence posInOccurrence,
Term term)
Returns the sub
Term at the given PosInOccurrence
but on the given Term instead of the one contained in the PosInOccurrence . |
static java.lang.String |
formatTerm(Term term,
Services services,
boolean useUnicode,
boolean usePrettyPrinting)
|
static Term |
getArrayIndex(Services services,
HeapLDT heapLDT,
Term arrayIndexTerm)
Returns the array index defined by the given
Term . |
static java.lang.String |
getChoiceSetting(java.lang.String key)
Returns the default choice value.
|
static java.util.HashMap<java.lang.String,java.lang.String> |
getDefaultTacletOptions()
Returns the default taclet options for symbolic execution.
|
static java.lang.String |
getDisplayString(IProgramVariable pv)
Returns the human readable name of the given
IProgramVariable . |
static ProgramVariable |
getProgramVariable(Services services,
HeapLDT heapLDT,
Term locationTerm)
Returns the
ProgramVariable defined by the given Term . |
static java.util.Set<IProgramVariable> |
getProgramVariables(FieldDeclaration fd)
Collects all
IProgramVariable s of the given FieldDeclaration . |
static IExecutionNode<?> |
getRoot(IExecutionNode<?> executionNode)
Returns the root of the given
IExecutionNode . |
static java.lang.String |
getSourcePath(PositionInfo posInfo)
Returns the path to the source file defined by the given
PositionInfo . |
static SymbolicExecutionTermLabel |
getSymbolicExecutionLabel(RuleApp ruleApp)
Returns the contained
SymbolicExecutionTermLabel if available. |
static SymbolicExecutionTermLabel |
getSymbolicExecutionLabel(Term term)
Returns the contained
SymbolicExecutionTermLabel if available. |
static boolean |
hasApplicableRules(Goal goal)
Checks if the
Goal has applicable rules. |
static boolean |
hasLoopBodyLabel(RuleApp ruleApp)
|
static boolean |
hasLoopBodyTerminationLabel(RuleApp ruleApp)
|
static boolean |
hasLoopCondition(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given
Node has a loop condition. |
static boolean |
hasReferenceSort(Services services,
IProgramVariable var)
Checks if the
Sort of the given IProgramVariable is a reference type. |
static boolean |
hasReferenceSort(Services services,
Sort sort)
Checks if the
Sort is a reference type. |
static boolean |
hasReferenceSort(Services services,
Term term)
|
static boolean |
hasSymbolicExecutionLabel(RuleApp ruleApp)
|
static boolean |
hasSymbolicExecutionLabel(Term term)
Checks if the given
Term contains a SymbolicExecutionTermLabel . |
static Term |
improveReadability(Term term,
Services services)
Improves the
Term to increase its readability. |
private static Term |
improveReadabilityRecursive(Term term,
Services services,
IntegerLDT integerLDT)
Helper method of
improveReadability(Term, Services) . |
static void |
initializeStrategy(SymbolicExecutionTreeBuilder builder)
Initializes the
Proof of the given SymbolicExecutionTreeBuilder
so that the correct Strategy is used. |
static Term |
instantiateTerm(Node node,
Term term,
TacletApp tacletApp,
Services services)
|
private static void |
internalCollectAllElementaryUpdateTerms(Services services,
java.util.List<IProgramVariable> result,
Term term)
Utility method of
collectAllElementaryUpdateTerms(Node) which
collects all IProgramVariable s of ElementaryUpdate s
and static field manipulations. |
private static void |
internalCollectStaticProgramVariablesOnHeap(Services services,
java.util.Set<IProgramVariable> result,
Term term)
Utility method of
internalCollectAllElementaryUpdateTerms(Services, List, Term)
which collects static field manipulations on the given heap update. |
static boolean |
isBaseHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is the base heap. |
static boolean |
isBlockContractValidityBranch(PosInOccurrence pio)
Checks if the modality at the given
PosInOccurrence represents the validity branch of an applied block contract. |
static boolean |
isBlockContractValidityBranch(RuleApp appliedRuleApp)
Checks if the modality at the applied rule represents the validity branch of an applied block contract.
|
static boolean |
isBlockSpecificationElement(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as block/loop contract.
|
static boolean |
isBoolean(Services services,
Operator op)
Checks if the given
Operator is a boolean. |
static boolean |
isBranchStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as branch statement.
|
static boolean |
isChoiceSettingInitialised()
Checks if the choice settings are initialized.
|
static boolean |
isCloseAfterJoin(RuleApp ruleApp)
Checks if the
CloseAfterMergeRuleBuiltInRuleApp is applied. |
static boolean |
isDoWhileLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a do while loop. |
static boolean |
isExceptionalMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as exceptional method return.
|
static boolean |
isForLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a for loop. |
static boolean |
isHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is a heap. |
static boolean |
isHeapUpdate(Services services,
Term term)
Checks if the given
Term represents a heap update,
in particular a store or create operation on a heap. |
static boolean |
isInImplicitMethod(Node node,
RuleApp ruleApp)
Checks if the currently executed code is in an implicit method
(
IProgramMethod.isImplicit() is true ). |
static boolean |
isJoin(RuleApp ruleApp)
Checks if the
MergeRuleBuiltInRuleApp is applied. |
static boolean |
isLoopBodyTermination(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop body termination.
|
static boolean |
isLoopInvariant(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop invariant.
|
static boolean |
isLoopStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as loop statement.
|
static boolean |
isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given node should be represented as method call.
|
static boolean |
isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement,
boolean allowImpliciteMethods)
Checks if the given node should be represented as method call.
|
static boolean |
isMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as method return.
|
private static boolean |
isMinusOne(Term term,
IntegerLDT integerLDT)
Checks if the given
Term represents the integer constant -1 . |
static boolean |
isNotImplicit(Services services,
IProgramMethod pm)
Checks if the given
IProgramMethod is not implicit. |
static boolean |
isNotNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
isNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
isNullSort(Sort sort,
Services services)
|
static boolean |
isNumber(Operator op)
Checks if the given
Operator is a number. |
private static boolean |
isOne(Term subOne,
IntegerLDT integerLDT)
Checks if the given term represent the number one
|
static boolean |
isOperationContract(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as operation contract.
|
static boolean |
isRuleAppToIgnore(RuleApp ruleApp)
Checks if the given
RuleApp should be ignored or
checked for possible symbolic execution tree node representation. |
static boolean |
isSelect(Services services,
Term term)
Checks if the given
Term is a select on a heap. |
static boolean |
isSkolemConstant(Term term)
|
static boolean |
isStatementNode(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as statement.
|
static boolean |
isStaticVariable(IProgramVariable programVariable)
Checks if the given
IProgramVariable is static or not. |
static boolean |
isSymbolicExecutionTreeNode(Node node,
RuleApp ruleApp)
|
static boolean |
isTerminationNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as termination.
|
static boolean |
isUsePrettyPrinting()
Checks if pretty printing is enabled or not.
|
static boolean |
isWeakeningGoalEnabled(Proof proof)
Checks if the weakening goal is enabled or not.
|
protected static Sequent |
labelSkolemConstants(Sequent sequent,
java.util.Set<Term> constantsToLabel,
TermFactory factory)
Labels all specified skolem equalities with the
RESULT_LABEL . |
static Sort |
lazyComputeExceptionSort(Node node,
IProgramVariable exceptionVariable)
Computes the exception
Sort lazily when #getExceptionSort()
is called the first time. |
static boolean |
lazyComputeIsAdditionalBranchVerified(Node node)
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
static boolean |
lazyComputeIsExceptionalTermination(Node node,
IProgramVariable exceptionVariable)
Checks if is an exceptional termination.
|
static boolean |
lazyComputeIsMainBranchVerified(Node node)
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
private static ImmutableList<Term> |
listNewSemisequentTerms(Semisequent parent,
Semisequent child)
|
static ImmutableList<Term> |
listSemisequentTerms(Semisequent semisequent)
Lists the
Term s contained in the given Semisequent . |
static Term |
posInOccurrenceInOtherNode(Node original,
PosInOccurrence pio,
Node toApplyOn)
Returns the
Term described by the given PosInOccurrence of the original Node
in the Node to apply on. |
static Term |
posInOccurrenceInOtherNode(Sequent original,
PosInOccurrence pio,
Sequent toApplyOn)
Returns the
Term described by the given PosInOccurrence of the original Sequent
in the Sequent to apply on. |
static PosInOccurrence |
posInOccurrenceToOtherSequent(Node original,
PosInOccurrence pio,
Node toApplyTo)
Returns the
PosInOccurrence described by the given PosInOccurrence of the original Node
in the Node to apply too. |
static PosInOccurrence |
posInOccurrenceToOtherSequent(Sequent original,
PosInOccurrence pio,
Sequent toApplyTo)
Returns the
PosInOccurrence described by the given PosInOccurrence of the original Sequent
in the Sequent to apply too. |
private static Sequent |
removeAllUnusedSkolemEqualities(Sequent sequent,
java.util.Collection<Term> skolemConstants)
Removes all
SequentFormula s with a skolem equality from the given Sequent
if the skolem Term is not contained in the given Collection . |
private static Sequent |
removeAllUnusedSkolemEqualities(Sequent sequent,
SequentFormula sf,
boolean antecedent,
java.util.Collection<Term> skolemConstants)
Helper method of
removeAllUnusedSkolemEqualities(Sequent, Collection)
which removes the given SequentFormula if required. |
static Term |
removeLabelRecursive(TermFactory tf,
Term term,
TermLabel label)
|
static Term |
replaceSkolemConstants(Sequent sequent,
Term term,
Services services)
Replaces all skolem constants in the given
Term . |
static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult |
searchContractPostOrExcPostExceptionVariable(Node node,
Services services)
Searches the used exception variable in the post or exceptional post branch of an applied
ContractRuleApp on the parent of the given Node . |
private static Term |
searchExceptionDefinition(Term term,
Services services)
Searches the exception definition.
|
static Term |
sequentToImplication(Sequent sequent,
Services services)
Converts the given
Sequent into an implication. |
static void |
setChoiceSetting(java.lang.String key,
java.lang.String value)
Sets the default choice value.
|
static void |
setUsePrettyPrinting(boolean usePrettyPrinting)
Defines if pretty printing is enabled or not.
|
static Term |
simplify(InitConfig initConfig,
Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
simplify(InitConfig initConfig,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
simplify(Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static void |
updateStrategySettings(Proof proof,
boolean useOperationContracts,
boolean useLoopInvariants,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecksImmediately)
Configures the proof to use the given settings.
|
static void |
updateStrategySettings(Proof proof,
StrategyProperties sp)
Configures the proof to use the given
StrategyProperties . |
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW
public static final Name RESULT_LABEL_NAME
RESULT_LABEL
.public static final TermLabel RESULT_LABEL
Term
to evaluate in a side proof.public static final Name LOOP_BODY_LABEL_NAME
LOOP_BODY_LABEL
.public static final TermLabel LOOP_BODY_LABEL
public static final Name LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
.public static final TermLabel LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
public static Term simplify(InitConfig initConfig, Term term) throws ProofInputException
Term
in a side proof.initConfig
- The InitConfig
to use.term
- The Term
to simplify.Term
.ProofInputException
- Occurred Exception.public static Term simplify(Proof parentProof, Term term) throws ProofInputException
Term
in a side proof.parentProof
- The parent Proof
.term
- The Term
to simplify.Term
.ProofInputException
- Occurred Exception.public static Term simplify(InitConfig initConfig, Proof parentProof, Term term) throws ProofInputException
Term
in a side proof.initConfig
- The InitConfig
to use.parentProof
- The parent Proof
which provides the StrategySettings
.term
- The Term
to simplify.Term
.ProofInputException
- Occurred Exception.public static Term sequentToImplication(Sequent sequent, Services services)
Sequent
into an implication.public static ImmutableList<Term> listSemisequentTerms(Semisequent semisequent)
Term
s contained in the given Semisequent
.semisequent
- The Semisequent
to list terms of.Term
s.public static Term improveReadability(Term term, Services services)
Term
to increase its readability.
The following changes will be performed:
a < 1 + b
=> a <= b
a < b + 1
=> a <= b
a >= 1 + b
=> a > b
a >= b + 1
=> a > b
a <= -1 + b
=> a < b
a <= b + -1
=> a < b
a <= b - 1
=> a < b
a > -1 + b
=> a >= b
a > b + -1
=> a >= b
a > b - 1
=> a >= b
a >= 1 + b
=> a > b
a >= b + 1
=> a > b
!a >= b
=> a < b
!a > b
=> a <= b
!a <= b
=> a > b
!a < b
=> a >= b
private static Term improveReadabilityRecursive(Term term, Services services, IntegerLDT integerLDT)
improveReadability(Term, Services)
.term
- The Term
to improve.services
- The Services
to use.integerLDT
- The IntegerLDT
to use.Term
or the Term
itself if no improvements are possible.private static boolean isOne(Term subOne, IntegerLDT integerLDT)
subOne
- the term to be checkedintegerLDT
- the LDT for integersprivate static boolean isMinusOne(Term term, IntegerLDT integerLDT)
Term
represents the integer constant -1
.term
- The Term
to check.integerLDT
- The IntegerLDT
to use.true
Term
represents -1
, false
Term
is something else.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractReturnVariableValueSequent(Services services, TypeReference contextObjectType, IProgramMethod contextMethod, ReferencePrefix contextObject, Node methodReturnNode, Node methodCallEmptyNode, IProgramVariable variable)
Sequent
which can be used in site proofs to
extract the return value of the given IProgramVariable
from the
sequent of the given Node
.services
- The Services
to use.contextObjectType
- The type of the current object (this reference).contextMethod
- The current method.contextObject
- The current object (this reference).methodReturnNode
- The method return Node
which provides the sequent to extract updates and return expression from.methodCallEmptyNode
- The method call empty Node
which provides the sequent to start site proof in.variable
- The IProgramVariable
of the value which is interested.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractReturnVariableValueSequent(Services services, IExecutionContext context, Node methodReturnNode, Node methodCallEmptyNode, IProgramVariable variable)
Sequent
which can be used in site proofs to
extract the return value of the given IProgramVariable
from the
sequent of the given Node
.services
- The Services
to use.context
- The IExecutionContext
that defines the current object (this reference).methodReturnNode
- The method return Node
which provides the sequent to extract updates and return expression from.methodCallEmptyNode
- The method call empty Node
which provides the sequent to start site proof in.variable
- The IProgramVariable
of the value which is interested.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractVariableValueSequent(Services services, Node node, PosInOccurrence pio, Term additionalConditions, IProgramVariable variable)
Sequent
which can be used in site proofs to
extract the value of the given IProgramVariable
from the
sequent of the given Node
.services
- The Services
to use.node
- The original Node
which provides the sequent to extract from.pio
- The PosInOccurrence
of the SE modality.additionalConditions
- Optional additional conditions.variable
- The IProgramVariable
of the value which is interested.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractTermSequent(Services sideProofServices, Node node, PosInOccurrence pio, Term additionalConditions, Term term, boolean keepUpdates)
Sequent
which can be used in site proofs to
extract the value of the given IProgramVariable
from the
sequent of the given Node
.sideProofServices
- The Services
of the side proof to use.node
- The original Node
which provides the sequent to extract from.pio
- The PosInOccurrence
of the modality or its updates.additionalConditions
- Additional conditions to add to the antecedent.term
- The new succedent term.keepUpdates
- true
keep updates, false
throw updates away.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static boolean isHeapUpdate(Services services, Term term)
Term
represents a heap update,
in particular a store or create operation on a heap.public static boolean canComputeVariables(IExecutionNode<?> node, Services services) throws ProofInputException
IExecutionNode
via IExecutionNode.getVariables()
.node
- The IExecutionNode
to check.services
- The Services
to use.true
right now it is possible to compute variables, false
it is not possible to compute variables.ProofInputException
- Occurred Exception.public static IExecutionConstraint[] createExecutionConstraints(IExecutionNode<?> node)
IExecutionNode
the contained
IExecutionConstraint
s.node
- The IExecutionNode
to create constraints for.IExecutionConstraint
s.public static boolean containsSymbolicExecutionLabel(Term term)
Term
or one of its sub terms contains
a symbolic execution label.term
- The Term
to check.true
SE label is somewhere contained, false
SE label is not contained at all.public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node) throws ProofInputException
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.IExecutionVariable
s.ProofInputException
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node, Term condition) throws ProofInputException
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s.ProofInputException
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node, Node proofNode, PosInOccurrence modalityPIO, Term condition) throws ProofInputException
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.proofNode
- The proof Node
to work with.modalityPIO
- The PosInOccurrence
of the modality of interest.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s.ProofInputException
public static IExecutionVariable[] createAllExecutionVariables(IExecutionNode<?> node, Node proofNode, PosInOccurrence modalityPIO, Term condition)
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.proofNode
- The proof Node
to work with.modalityPIO
- The PosInOccurrence
of the modality of interest.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s.public static java.util.List<IProgramVariable> collectAllElementaryUpdateTerms(Node node)
IProgramVariable
used in ElementaryUpdate
s.node
- The Node
to search in.IProgramVariable
which are used in ElementaryUpdate
s.private static void internalCollectAllElementaryUpdateTerms(Services services, java.util.List<IProgramVariable> result, Term term)
collectAllElementaryUpdateTerms(Node)
which
collects all IProgramVariable
s of ElementaryUpdate
s
and static field manipulations.services
- The Services
to use.result
- The result List
to fill.term
- The current term to analyze.private static void internalCollectStaticProgramVariablesOnHeap(Services services, java.util.Set<IProgramVariable> result, Term term)
internalCollectAllElementaryUpdateTerms(Services, List, Term)
which collects static field manipulations on the given heap update.services
- The Services
to use.result
- The result List
to fill.term
- The current term to analyze.public static ProgramVariable getProgramVariable(Services services, HeapLDT heapLDT, Term locationTerm)
ProgramVariable
defined by the given Term
.services
- The Services
to use.heapLDT
- The HeapLDT
to use.locationTerm
- The Term
to extract ProgramVariable
from.Term
s ProgramVariable
or null
if not available.public static Term getArrayIndex(Services services, HeapLDT heapLDT, Term arrayIndexTerm)
Term
.public static IProgramVariable findSelfTerm(Node node, PosInOccurrence pio)
node
- The Node
to search in.pio
- The PosInOccurrence
describing the location of the modality of interest.IProgramVariable
with the current this
/self
reference or null
if no one is available.public static boolean isMethodCallNode(Node node, RuleApp ruleApp, SourceElement statement)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).true
represent node as method call, false
represent node as something else.public static boolean isMethodCallNode(Node node, RuleApp ruleApp, SourceElement statement, boolean allowImpliciteMethods)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).allowImpliciteMethods
- true
implicit methods are included, false
implicit methods are outfiltered.true
represent node as method call, false
represent node as something else.public static boolean isNotImplicit(Services services, IProgramMethod pm)
IProgramMethod
is not implicit.services
- The Services
to use.pm
- The IProgramMethod
to check.true
is not implicit, false
is implicitpublic static boolean isBranchStatement(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).posInfo
- The PositionInfo
.true
represent node as branch statement, false
represent node as something else.public static boolean isLoopStatement(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).posInfo
- The PositionInfo
.true
represent node as loop statement, false
represent node as something else.public static boolean isStatementNode(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).posInfo
- The PositionInfo
.true
represent node as statement, false
represent node as something else.public static boolean isTerminationNode(Node node, RuleApp ruleApp)
public static boolean isOperationContract(Node node, RuleApp ruleApp)
public static boolean isBlockSpecificationElement(Node node, RuleApp ruleApp)
public static boolean isLoopInvariant(Node node, RuleApp ruleApp)
public static boolean isMethodReturnNode(Node node, RuleApp ruleApp)
public static boolean isExceptionalMethodReturnNode(Node node, RuleApp ruleApp)
public static boolean hasLoopCondition(Node node, RuleApp ruleApp, SourceElement statement)
Node
has a loop condition.node
- The Node
to check.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The actual statement (SourceElement
).true
has loop condition, false
has no loop condition.public static boolean hasLoopBodyLabel(RuleApp ruleApp)
ruleApp
- The RuleApp
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given RuleApp
is null
.public static boolean hasLoopBodyTerminationLabel(RuleApp ruleApp)
ruleApp
- The RuleApp
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given RuleApp
is null
.public static boolean hasSymbolicExecutionLabel(RuleApp ruleApp)
ruleApp
- The RuleApp
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given RuleApp
is null
.public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(RuleApp ruleApp)
SymbolicExecutionTermLabel
if available.ruleApp
- The RuleApp
may used or not used in the rule.SymbolicExecutionTermLabel
or null
if no SymbolicExecutionTermLabel
is provided.public static boolean hasSymbolicExecutionLabel(Term term)
Term
contains a SymbolicExecutionTermLabel
.term
- The Term
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given Term
is null
.public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(Term term)
SymbolicExecutionTermLabel
if available.term
- The Term
to search in.SymbolicExecutionTermLabel
or null
if no SymbolicExecutionTermLabel
is provided.public static PosInOccurrence findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)
PosInOccurrence
with the maximal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Sequent
.sequent
- The Sequent
to search in.PosInOccurrence
with the maximal ID if available or null
otherwise.public static PosInOccurrence findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent, boolean inAntec)
Term
with the maximal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Semisequent
.semisequent
- The Semisequent
to search in.inAntec
- true
antecedent, false
succedent.Term
with the maximal ID if available or null
otherwise.public static PosInTerm findModalityWithMaxSymbolicExecutionLabelId(Term term)
PosInTerm
with the maximal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Term
.public static PosInOccurrence findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)
PosInOccurrence
with the minimal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Sequent
.sequent
- The Sequent
to search in.PosInOccurrence
with the maximal ID if available or null
otherwise.public static PosInOccurrence findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent, boolean inAntec)
PosInOccurrence
with the minimal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Semisequent
.semisequent
- The Semisequent
to search in.inAntec
- true
antecedent, false
succedent.PosInOccurrence
with the minimal ID if available or null
otherwise.public static PosInTerm findModalityWithMinSymbolicExecutionLabelId(Term term)
PosInTerm
with the minimal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Term
.public static boolean isSymbolicExecutionTreeNode(Node node, RuleApp ruleApp)
public static boolean isRuleAppToIgnore(RuleApp ruleApp)
RuleApp
should be ignored or
checked for possible symbolic execution tree node representation.public static boolean isInImplicitMethod(Node node, RuleApp ruleApp)
IProgramMethod.isImplicit()
is true
).public static int computeStackSize(RuleApp ruleApp)
public static boolean isDoWhileLoopCondition(Node node, SourceElement statement)
SourceElement
is a do while loop.node
- The Node
to check.statement
- The actual statement (SourceElement
).true
is do while loop, false
is something else.public static boolean isForLoopCondition(Node node, SourceElement statement)
SourceElement
is a for loop.node
- The Node
to check.statement
- The actual statement (SourceElement
).true
is for loop, false
is something else.public static ImmutableList<Goal> collectGoalsInSubtree(IExecutionElement executionElement)
Goal
s in the subtree of the given IExecutionElement
.executionElement
- The IExecutionElement
to collect Goal
s in.Goal
s.public static ImmutableList<Goal> collectGoalsInSubtree(Node node)
public static Node findMethodCallNode(Node node, PosInOccurrence pio)
Node
the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp)
).node
- The Node
to start search in.pio
- The PosInOccurrence
of the modality.Node
of the given Node
which is also a set node or null
if no parent node was found.public static Node findParentSetNode(Node node)
Node
the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp)
).public static Term computeBranchCondition(Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Node
.node
- The Node
to compute its branch condition.simplify
- true
simplify condition in a side proof, false
do not simplify condition.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.private static Term computeContractRuleAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Computes the branch condition of the given Node
which was constructed by a ContractRuleApp
.
The branch conditions are:
Idea:
exc_0 = null
and pre -> post
/excPre -> !exc_0 = null & signals
termsexc_0 = null
Termexc_0 = null
parent
- The parent Node
of the given one.node
- The Node
to compute its branch condition.simplify
- true
simplify condition in a side proof, false
do not simplify condition.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.private static void collectContractPreconditions(Services services, SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult search, java.util.List<Term> normalConditions, java.util.List<Term> exceptinalConditions) throws ProofInputException
services
- The Services
to use.search
- The SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult
.normalConditions
- The List
with the normal case conditions to fill.exceptinalConditions
- The List
with the exceptional case conditions to fill.ProofInputException
- Occurred Exception.private static void collectSpecifcationCasesPreconditions(Term normalExcDefinition, Term exceptionalExcDefinition, Term term, java.util.List<Term> normalConditions, java.util.List<Term> exceptinalConditions) throws ProofInputException
normalExcDefinition
- The normal exception equality.exceptionalExcDefinition
- The exceptional equality.term
- The current Term
.normalConditions
- The List
with the normal case conditions to fill.exceptinalConditions
- The List
with the exceptional case conditions to fill.ProofInputException
- Occurred Exception.public static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult searchContractPostOrExcPostExceptionVariable(Node node, Services services) throws ProofInputException
ContractRuleApp
on the parent of the given Node
.node
- The Node
which is the post or exceptional post branch of an applied ContractRuleApp
.services
- The Services
to use.ProofInputException
- Occurred exception if something is not as expected.private static Term searchExceptionDefinition(Term term, Services services)
private static Term computeLoopInvariantBuiltInRuleAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Computes the branch condition of the given Node
which was constructed by a LoopInvariantBuiltInRuleApp
.
The branch conditions are:
parent
- The parent Node
of the given one.node
- The Node
to compute its branch condition.simplify
- true
simplify condition in a side proof, false
do not simplify condition.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.private static Term computeBlockContractBuiltInRuleAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Computes the branch condition of the given Node
which was constructed by an
AbstractBlockContractBuiltInRuleApp
.
The branch conditions are:
parent
- The parent Node
of the given one.node
- The Node
to compute its branch condition.simplify
- true
simplify condition in a side proof, false
do not simplify condition.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.public static Term posInOccurrenceInOtherNode(Node original, PosInOccurrence pio, Node toApplyOn)
Term
described by the given PosInOccurrence
of the original Node
in the Node
to apply on.original
- The original Node
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyOn
- The new Node
to apply the PosInOccurrence
on.Term
in the other Node
described by the PosInOccurrence
or null
if not available.public static Term posInOccurrenceInOtherNode(Sequent original, PosInOccurrence pio, Sequent toApplyOn)
Term
described by the given PosInOccurrence
of the original Sequent
in the Sequent
to apply on.original
- The original Sequent
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyOn
- The new Sequent
to apply the PosInOccurrence
on.Term
in the other Sequent
described by the PosInOccurrence
or null
if not available.public static PosInOccurrence posInOccurrenceToOtherSequent(Node original, PosInOccurrence pio, Node toApplyTo)
PosInOccurrence
described by the given PosInOccurrence
of the original Node
in the Node
to apply too.original
- The original Node
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyTo
- The new Node
to apply the PosInOccurrence
to.PosInOccurrence
in the other Node
described by the PosInOccurrence
or null
if not available.public static PosInOccurrence posInOccurrenceToOtherSequent(Sequent original, PosInOccurrence pio, Sequent toApplyTo)
PosInOccurrence
described by the given PosInOccurrence
of the original Sequent
in the Sequent
to apply too.original
- The original Sequent
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyTo
- The new Sequent
to apply the PosInOccurrence
to.PosInOccurrence
in the other Sequent
described by the PosInOccurrence
or null
if not available.private static Term computeTacletAppBranchCondition(Node parent, Node node, boolean simplify, boolean improveReadability) throws ProofInputException
parent
- The parent Node
of the given one.node
- The Node
to compute its branch condition.simplify
- true
simplify condition in a side proof, false
do not simplify condition.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.private static ImmutableList<Term> listNewSemisequentTerms(Semisequent parent, Semisequent child)
parent
- The parent Semisequent
.child
- The child Semisequent
.ImmutableList
with all new Term
s.private static Term findReplacement(Semisequent semisequent, PosInOccurrence posInOccurrence, Term replaceTerm)
Rule
application instantiated replace Term
which is equal modulo labels to the given replace Term
.terms
- The available candidates created by Rule
application.posInOccurrence
- The PosInOccurrence
on which the rule was applied.replaceTerm
- The Term
to find.Term
or null
if not available.private static boolean checkReplaceTerm(Term toCheck, PosInOccurrence posInOccurrence, Term replaceTerm)
toCheck
- The Term
to check.posInOccurrence
- The PosInOccurrence
of the Rule
application.replaceTerm
- The Term
to compare with.true
equal modulo labels, false
not equal at all.public static Term followPosInOccurrence(PosInOccurrence posInOccurrence, Term term)
Term
at the given PosInOccurrence
but on the given Term
instead of the one contained in the PosInOccurrence
.posInOccurrence
- The PosInOccurrence
which defines the sub term position.term
- The Term
to work with.Term
or null
if the PosInOccurrence
is not compatible.public static Term instantiateTerm(Node node, Term term, TacletApp tacletApp, Services services)
private static Term evaluateInSideProof(Services services, Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, java.lang.String description, java.lang.String splittingOption) throws ProofInputException
services
- The Services
to use.proof
- The Proof
from on which the side proof si performed.sequentToProve
- The Sequent
to prove in a side proof.label
- The TermLabel
which is used to compute the result.description
- The side proof description.splittingOption
- The splitting options to use.Term
.ProofInputException
- Occurred Exception.public static java.lang.String getChoiceSetting(java.lang.String key)
null
if it is called before
a proof is instantiated the first time. It can be checked via
isChoiceSettingInitialised()
.key
- The choice key.public static void setChoiceSetting(java.lang.String key, java.lang.String value)
isChoiceSettingInitialised()
.key
- The choice key to modify.value
- The new choice value to set.public static boolean isNull(Node node, Term additionalAntecedent, Term newSuccedent) throws ProofInputException
public static boolean isNotNull(Node node, Term additionalAntecedent, Term newSuccedent) throws ProofInputException
private static boolean checkNull(Node node, Term additionalAntecedent, Term newSuccedent, boolean nullExpected) throws ProofInputException
node
- The Node
which provides the original Sequent
additionalAntecedent
- An additional antecedent.newSuccedent
- The Term
to check.nullExpected
- true
expect that Term
is null, false
expect that term is not null.true
term is null value matches the expected nullExpected value, false
otherwise.ProofInputException
- Occurred Exceptionpublic static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term newSuccedent)
public static Sequent createSequentToProveWithNewSuccedent(Node node, Term additionalAntecedent, Term newSuccedent, boolean addResultLabel)
public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term additionalAntecedent, Term newSuccedent, boolean addResultLabel)
public static ImmutableList<Term> computeRootElementaryUpdates(Node root)
ElementaryUpdate
s on the given root Node
.root
- The root Node
of the Proof
.ElementaryUpdate
s.public static ImmutableList<Term> collectElementaryUpdates(Term term)
ElementaryUpdate
s in the given Term
.term
- The Term
to collect its updates.ElementaryUpdate
s.public static Sequent createSequentToProveWithNewSuccedent(Node node, Term additionalAntecedent, Term newSuccedent, ImmutableList<Term> updates, boolean addResultLabel)
public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term additionalAntecedent, Term newSuccedent, ImmutableList<Term> updates, boolean addResultLabel)
protected static Sequent labelSkolemConstants(Sequent sequent, java.util.Set<Term> constantsToLabel, TermFactory factory)
RESULT_LABEL
.sequent
- The Sequent
to modify.constantsToLabel
- The skolem constants to label.factory
- The TermFactory
to use.Sequent
.private static Term addLabelRecursiveToNonSkolem(TermFactory tf, Term term, TermLabel label)
tf
- The TermFactory
to use.term
- The Term
to add label to.label
- The TermLabel
to add.Term
with the given TermLabel
.public static Term removeLabelRecursive(TermFactory tf, Term term, TermLabel label)
tf
- The TermFactory
to use.term
- The Term
to remove label from.label
- The TermLabel
to remove.Term
without the given TermLabel
.private static java.util.Set<Term> collectSkolemConstants(Sequent sequent, Term term)
Term
s which fulfill
isSkolemConstant(Term)
as well as the skolem constants
used in the find once recursive.private static java.util.Set<Term> collectSkolemConstantsNonRecursive(Term term)
Term
s which fulfill
isSkolemConstant(Term)
.public static boolean isSkolemConstant(Term term)
private static Sequent removeAllUnusedSkolemEqualities(Sequent sequent, java.util.Collection<Term> skolemConstants)
SequentFormula
s with a skolem equality from the given Sequent
if the skolem Term
is not contained in the given Collection
.private static Sequent removeAllUnusedSkolemEqualities(Sequent sequent, SequentFormula sf, boolean antecedent, java.util.Collection<Term> skolemConstants)
removeAllUnusedSkolemEqualities(Sequent, Collection)
which removes the given SequentFormula
if required.sequent
- The Sequent
to modify.sf
- The SequentFormula
to remove if its skolem Term
is not listed.antecedent
- true
antecedent, false
succedent.skolemConstants
- The allowed skolem Term
s.Sequent
in which the SequentFormula
might be removed.public static int checkSkolemEquality(SequentFormula sf)
SequentFormula
is a skolem equality.sf
- The SequentFormula
to check.-1
left side of skolem equality, 0
no skolem equality, 1
right side of skolem equality.public static int checkSkolemEquality(Term term)
Term
is a skolem equality.sf
- The Term
to check.-1
left side of skolem equality, 0
no skolem equality, 1
right side of skolem equality.public static Term replaceSkolemConstants(Sequent sequent, Term term, Services services)
Term
.private static java.util.List<Term> findSkolemReplacements(Sequent sequent, Term skolemConstant, Term skolemEquality)
replaceSkolemConstants(Sequent, Term, Services)
to
find all equality parts of the given skolem constant.sequent
- The Sequent
which provides the skolem equalities.skolemConstant
- The skolem constant to solve.skolemEquality
- The optional skolem equality to ignore.public static boolean isStaticVariable(IProgramVariable programVariable)
IProgramVariable
is static or not.true
is static, false
is not static or is array cell.public static java.util.Set<IProgramVariable> getProgramVariables(FieldDeclaration fd)
IProgramVariable
s of the given FieldDeclaration
.fd
- The given FieldDeclaration
.IProgramVariable
s for the given FieldDeclaration
.public static Term computePathCondition(Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Node
.node
- The Node
to compute its path condition.simplify
- true
simplify each branch condition in a side proof, false
do not simplify branch conditions.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.public static Term computePathCondition(Node parentNode, Node childNode, boolean simplify, boolean improveReadability) throws ProofInputException
Node
s.parentNode
- The Node
to stop path condition computation at.childNode
- The Node
to compute its path condition back to the parent.simplify
- true
simplify each branch condition in a side proof, false
do not simplify branch conditions.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.public static boolean hasReferenceSort(Services services, IProgramVariable var)
Sort
of the given IProgramVariable
is a reference type.services
- The Services
to use.var
- The IProgramVariable
to check.true
is reference sort, false
is no reference sort.public static boolean hasReferenceSort(Services services, Sort sort)
Sort
is a reference type.public static java.lang.String getDisplayString(IProgramVariable pv)
IProgramVariable
.pv
- The IProgramVariable
to get its name.IProgramVariable
.public static IExecutionNode<?> getRoot(IExecutionNode<?> executionNode)
IExecutionNode
.executionNode
- The IExecutionNode
to get the root of its symbolic execution tree.IExecutionNode
.public static IProgramVariable extractExceptionVariable(Proof proof)
proof
- The Proof
to extract variable from.public static void updateStrategySettings(Proof proof, boolean useOperationContracts, boolean useLoopInvariants, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecksImmediately)
proof
- The Proof
to configure.useOperationContracts
- true
use operation contracts, false
expand methods.useLoopInvariants
- true
use loop invariants, false
expand loops.nonExecutionBranchHidingSideProofs
- true
hide non execution branch labels by side proofs, false
do not hide execution branch labels.useLoopInvariants
- true
immediately alias checks, false
alias checks never.public static void updateStrategySettings(Proof proof, StrategyProperties sp)
StrategyProperties
.proof
- The Proof
to configure.sb
- The StrategyProperties
to set.public static boolean isChoiceSettingInitialised()
true
settings are initialized, false
settings are not initialized.public static boolean isLoopBodyTermination(Node node, RuleApp ruleApp)
public static boolean isHeap(Operator op, HeapLDT heapLDT)
Operator
is a heap.public static boolean isBaseHeap(Operator op, HeapLDT heapLDT)
Operator
is the base heap.public static java.lang.String getSourcePath(PositionInfo posInfo)
PositionInfo
.posInfo
- The PositionInfo
to extract source file from.null
if not available.public static boolean isSelect(Services services, Term term)
Term
is a select on a heap.public static boolean isNumber(Operator op)
Operator
is a number.op
- The Operator
to check.true
is number, false
is something else.public static boolean isBoolean(Services services, Operator op)
Operator
is a boolean.op
- The Operator
to check.true
is boolean, false
is something else.public static java.util.HashMap<java.lang.String,java.lang.String> getDefaultTacletOptions()
public static java.lang.String formatTerm(Term term, Services services, boolean useUnicode, boolean usePrettyPrinting)
Converts the given Term
into a String
respecting #isUsePretty()
.
The functionality is similar to OutputStreamProofSaver.printTerm(Term, Services, boolean)
but allows to set custom settings.
public static boolean isUsePrettyPrinting()
true
pretty printing is enabled, false
pretty printing is disabled.public static void setUsePrettyPrinting(boolean usePrettyPrinting)
usePrettyPrinting
- true
pretty printing is enabled, false
pretty printing is disabled.public static boolean hasApplicableRules(Goal goal)
Goal
has applicable rules.goal
- The Goal
to check.true
has applicable rules, false
no rules are applicable.public static Pair<java.lang.Integer,SourceElement> computeSecondStatement(RuleApp ruleApp)
NodeInfo.computeActiveStatement(SourceElement)
.ruleApp
- The RuleApp
.public static boolean equalsWithPosition(SourceElement first, SourceElement second)
SourceElement
s including their PositionInfo
s.first
- The first SourceElement
.second
- The second SourceElement
.true
both are equal and at the same PositionInfo
, false
otherwise.public static boolean containsStatement(ProgramElement toSearchIn, SourceElement toSearch, Services services)
ProgramElement
contains the given SourceElement
.toSearchIn
- The ProgramElement
to search in.toSearch
- The SourceElement
to search.services
- The Services
to use.true
contained, false
not contained.public static Term createSelectTerm(IExecutionVariable variable)
#getProgramVariable()
.services
- The Services
to use.public static NotationInfo createNotationInfo(IExecutionElement element)
NotationInfo
for the given IExecutionElement
.element
- The IExecutionElement
to create its NotationInfo
.NotationInfo
.public static NotationInfo createNotationInfo(Node node)
NotationInfo
for the given Node
.node
- The Node
to create its NotationInfo
.NotationInfo
.public static NotationInfo createNotationInfo(Proof proof)
NotationInfo
for the given Proof
.proof
- The Proof
to create its NotationInfo
.NotationInfo
.public static boolean lazyComputeIsMainBranchVerified(Node node)
true
verified/closed, false
not verified/still openpublic static boolean lazyComputeIsAdditionalBranchVerified(Node node)
true
verified/closed, false
not verified/still openpublic static boolean lazyComputeIsExceptionalTermination(Node node, IProgramVariable exceptionVariable)
node
- the node which is used for computation.exceptionVariable
- the exception variable which is used to check if the executed program in proof terminates normally.true
exceptional termination, false
normal termination.public static Sort lazyComputeExceptionSort(Node node, IProgramVariable exceptionVariable)
Sort
lazily when #getExceptionSort()
is called the first time.node
- the node which is user for computation.exceptionVariable
- the exception variable which is used to check if the executed program in proof terminates normally.Sort
.protected static ImmutableArray<Term> extractValueFromUpdate(Term term, IProgramVariable variable)
IProgramVariable
from the given update term.term
- The given update term.variable
- The IProgramVariable
for that the value is needed.null
if it is not defined in the given update term.public static void initializeStrategy(SymbolicExecutionTreeBuilder builder)
Proof
of the given SymbolicExecutionTreeBuilder
so that the correct Strategy
is used.builder
- The SymbolicExecutionTreeBuilder
to initialize.public static boolean isBlockContractValidityBranch(RuleApp appliedRuleApp)
appliedRuleApp
- The RuleApp
to check.true
validitiy branch, false
otherwise.public static boolean isBlockContractValidityBranch(PosInOccurrence pio)
PosInOccurrence
represents the validity branch of an applied block contract.pio
- The PosInOccurrence
to check.false
otherwise.public static boolean isJoin(RuleApp ruleApp)
MergeRuleBuiltInRuleApp
is applied.ruleApp
- The RuleApp
to check.true
is MergeRuleBuiltInRuleApp
, false
otherwise.public static boolean isCloseAfterJoin(RuleApp ruleApp)
CloseAfterMergeRuleBuiltInRuleApp
is applied.ruleApp
- The RuleApp
to check.true
is CloseAfterMergeRuleBuiltInRuleApp
, false
otherwise.