public static final class AuxiliaryContractBuilders.GoalsConfigurator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private AbstractAuxiliaryContractBuiltInRuleApp |
application
The rule application.
|
private AbstractAuxiliaryContractRule.Instantiation |
instantiation
The instantiation.
|
private java.util.List<Label> |
labels |
private PosInOccurrence |
occurrence
The position at which the rule is applied.
|
private AbstractAuxiliaryContractRule |
rule
The rule being applied.
|
private Services |
services
Services.
|
private TermLabelState |
termLabelState
The term label state.
|
private AuxiliaryContract.Variables |
variables |
Constructor and Description |
---|
GoalsConfigurator(AbstractAuxiliaryContractBuiltInRuleApp application,
TermLabelState termLabelState,
AbstractAuxiliaryContractRule.Instantiation instantiation,
java.util.List<Label> labels,
AuxiliaryContract.Variables variables,
PosInOccurrence occurrence,
Services services,
AbstractAuxiliaryContractRule rule) |
Modifier and Type | Method and Description |
---|---|
private static void |
addInfFlow(Goal goal)
Adds information flow properties to the specified goal.
|
private static Term |
buildFullPostBody(boolean bodyBreakFound,
JavaBlock tail,
Modality modality,
Term rememberNext,
Term decreasesCheck,
Term anonOut,
Term post,
Term postNext,
Term postAfterTail,
Term pre,
Term brokeLoop,
Term notBrokeLoop,
Term abrupt,
Term notAbrupt,
TermBuilder tb) |
private static Term |
buildLoopValiditySequent(Goal goal,
LoopContract contract,
JavaBlock unfold,
JavaBlock body,
JavaBlock tail,
Modality modality,
boolean bodyBreakFound,
Term context,
Term remember,
Term rememberNext,
Term decreasesCheck,
Term anonOut,
Term anonOut2,
Term post,
Term postNext,
Term postAfterTail,
Term pre,
Term brokeLoop,
Term notBrokeLoop,
Term exceptionEqNull,
Term exceptionNeqNull,
Term cond,
Term notCond,
Term abrupt,
Term notAbrupt,
TermBuilder tb) |
private static Term |
buildSimplifiedPostBody(boolean bodyBreakFound,
Term rememberNext,
Term decreasesCheck,
Term anonOut,
Term post,
Term postNext,
Term pre,
Term brokeLoop,
Term notBrokeLoop,
Term abrupt,
Term notAbrupt,
TermBuilder tb) |
private Term |
buildUsageFormula(Goal goal) |
private java.util.Map<Label,ProgramVariable> |
collectContinueFlags(LoopContract contract,
ProgramVariable continuedLoopVariable,
java.util.List<Continue> bodyContinues) |
private StatementBlock |
constructAbruptTerminationIfCascade() |
private static Term |
createAbruptTerms(AuxiliaryContract.Terms terms,
Term exceptionNeqNull,
TermBuilder tb) |
private JavaBlock[] |
createJavaBlocks(LoopContract contract,
ProgramVariable conditionVariable,
ProgramVariable exceptionParameter,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags) |
private static ProgramVariable[] |
createLoopVariables(Services services) |
private Term[] |
createPosts(Goal goal,
Term[] postconditions,
Term[] postconditionsNext,
AuxiliaryContract.Terms terms,
TermBuilder tb) |
private StatementBlock |
finishTransactionIfModalityIsTransactional(Statement statement) |
private JavaBlock |
getJavaBlock(ProgramVariable exceptionParameter) |
private JavaBlock |
replaceBlock(JavaBlock java,
JavaStatement oldBlock,
StatementBlock newBlock) |
Term |
setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
void |
setUpPreconditionGoal(Goal goal,
Term update,
Term[] preconditions)
Sets up the precondition goal.
|
void |
setUpUsageGoal(Goal goal,
Term[] updates,
Term[] assumptions)
Sets up the usage goal.
|
Term |
setUpValidityGoal(Goal goal,
Term[] updates,
Term[] assumptions,
Term[] postconditions,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms) |
Term |
setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
private Statement |
wrapInMethodFrameIfContextIsAvailable(StatementBlock block) |
private final AbstractAuxiliaryContractBuiltInRuleApp application
private final TermLabelState termLabelState
private final AbstractAuxiliaryContractRule.Instantiation instantiation
private final java.util.List<Label> labels
AuxiliaryContract.getLabels()
private final AuxiliaryContract.Variables variables
AuxiliaryContract.getVariables()
private final PosInOccurrence occurrence
private final Services services
private final AbstractAuxiliaryContractRule rule
public GoalsConfigurator(AbstractAuxiliaryContractBuiltInRuleApp application, TermLabelState termLabelState, AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.List<Label> labels, AuxiliaryContract.Variables variables, PosInOccurrence occurrence, Services services, AbstractAuxiliaryContractRule rule)
application
- the rule application.termLabelState
- the term label state.instantiation
- the instantiationlabels
- all labels belonging to the block.variables
- the contract's variables.occurrence
- the position at which the rule is applied.services
- services.rule
- the rule being applied.private static void addInfFlow(Goal goal)
goal
- a goal.private static ProgramVariable[] createLoopVariables(Services services)
services
- services.private static Term buildLoopValiditySequent(Goal goal, LoopContract contract, JavaBlock unfold, JavaBlock body, JavaBlock tail, Modality modality, boolean bodyBreakFound, Term context, Term remember, Term rememberNext, Term decreasesCheck, Term anonOut, Term anonOut2, Term post, Term postNext, Term postAfterTail, Term pre, Term brokeLoop, Term notBrokeLoop, Term exceptionEqNull, Term exceptionNeqNull, Term cond, Term notCond, Term abrupt, Term notAbrupt, TermBuilder tb)
goal
- the current goalcontract
- a loop contract.unfold
- the evaluation of the loop guard.body
- the loop body.tail
- all statements in the block after the loop.modality
- the contract's modality.bodyBreakFound
- whether or not the body contains a break statement.context
- the context update.remember
- the remembrance update.rememberNext
- the remembracne update for the next loop iteration.decreasesCheck
- the decreases check.anonOut
- the anonOut update.anonOut2
- a copy of the anonOut update.post
- the current loop iteration's postconditon.postNext
- the next loop iteration's postconditon.postAfterTail
- the formula [[tail]] -> post
where [[]]
the contract's
modality.pre
- the contract's precondition.brokeLoop
- the formula brokeLoop = true
notBrokeLoop
- the formula not brokeLoop = true
exceptionEqNull
- the formula exception = null
exceptionNeqNull
- the formula not exception = null
cond
- the formula cond = true
notCond
- the formula not cond = true
abrupt
- the formula for abrupt termination.notAbrupt
- the negation of the formula for abrupt termination.tb
- a term builder.private static Term buildSimplifiedPostBody(boolean bodyBreakFound, Term rememberNext, Term decreasesCheck, Term anonOut, Term post, Term postNext, Term pre, Term brokeLoop, Term notBrokeLoop, Term abrupt, Term notAbrupt, TermBuilder tb)
private static Term buildFullPostBody(boolean bodyBreakFound, JavaBlock tail, Modality modality, Term rememberNext, Term decreasesCheck, Term anonOut, Term post, Term postNext, Term postAfterTail, Term pre, Term brokeLoop, Term notBrokeLoop, Term abrupt, Term notAbrupt, TermBuilder tb)
private static Term createAbruptTerms(AuxiliaryContract.Terms terms, Term exceptionNeqNull, TermBuilder tb)
public Term setUpWdGoal(Goal goal, BlockContract contract, Term update, Term anonUpdate, LocationVariable heap, Function anonHeap, ImmutableSet<ProgramVariable> localIns)
goal
- If this is not null
, the returned formula is added to this goal.contract
- the contract being applied.update
- the update.anonUpdate
- the anonymization update.heap
- the heap.anonHeap
- the anonymization heap.localIns
- all free local variables in the block.public Term setUpValidityGoal(Goal goal, Term[] updates, Term[] assumptions, Term[] postconditions, ProgramVariable exceptionParameter, AuxiliaryContract.Terms terms)
goal
- If this is not null
, the returned term is added to this goal.updates
- the updates.assumptions
- the preconditions.postconditions
- the postconditions.exceptionParameter
- the exception variable.terms
- the termified variables.public Term setUpLoopValidityGoal(Goal goal, LoopContract contract, Term context, Term remember, Term rememberNext, java.util.Map<LocationVariable,Function> anonOutHeaps, java.util.Map<LocationVariable,Term> modifiesClauses, Term[] assumptions, Term decreasesCheck, Term[] postconditions, Term[] postconditionsNext, ProgramVariable exceptionParameter, AuxiliaryContract.Terms terms, AuxiliaryContract.Variables nextVars)
goal
- If this is not null
, the returned term is added to this goal.contract
- the contract being applied.context
- the context update.remember
- the remembrance update for the current loop iteration.rememberNext
- the remembrance update for the next loop iteration.anonOutHeaps
- the heaps used in the anonOut update.modifiesClauses
- the modified clauses.assumptions
- the assumptions.decreasesCheck
- the decreases check.postconditions
- the current loop iteration's postconditions.postconditionsNext
- the next loop iteration's postconditions.exceptionParameter
- the exception variable.terms
- the termified variables.nextVars
- the variables for the next loop iteration.public void setUpPreconditionGoal(Goal goal, Term update, Term[] preconditions)
goal
- the precondition goal.update
- the update.preconditions
- the preconditions.public void setUpUsageGoal(Goal goal, Term[] updates, Term[] assumptions)
goal
- the usage goal.updates
- the updates.assumptions
- the preconditions.private Statement wrapInMethodFrameIfContextIsAvailable(StatementBlock block)
block
- a block.private JavaBlock[] createJavaBlocks(LoopContract contract, ProgramVariable conditionVariable, ProgramVariable exceptionParameter, java.util.Map<Label,ProgramVariable> breakFlags, java.util.Map<Label,ProgramVariable> continueFlags)
contract
- the contract being applied.conditionVariable
- the variable used to store the loop guard's value.exceptionParameter
- the exception variable.breakFlags
- the break flags.continueFlags
- the continue flags.private StatementBlock finishTransactionIfModalityIsTransactional(Statement statement)
private JavaBlock replaceBlock(JavaBlock java, JavaStatement oldBlock, StatementBlock newBlock)
private StatementBlock constructAbruptTerminationIfCascade()
private JavaBlock getJavaBlock(ProgramVariable exceptionParameter)
private final java.util.Map<Label,ProgramVariable> collectContinueFlags(LoopContract contract, ProgramVariable continuedLoopVariable, java.util.List<Continue> bodyContinues)
private Term[] createPosts(Goal goal, Term[] postconditions, Term[] postconditionsNext, AuxiliaryContract.Terms terms, TermBuilder tb)