de.uka.ilkd.key.rule.merge

Class MergeRule

java.lang.Object

de.uka.ilkd.key.rule.merge.MergeRule

All Implemented Interfaces:

BuiltInRule, Rule

public class MergeRule
extends java.lang.Object
implements BuiltInRule

Base for implementing merge rules. Extend this class, implement method mergeValuesInStates(...) and register in class JavaProfile.

The rule is applicable if the chosen subterm has the form { x := v || ... } PHI and there are potential merge candidates.

Any rule application returned will be incomplete; completion is handled by de.uka.ilkd.key.gui.mergerule.MergeRuleCompletion.

Author:

Dominic Scheurer

See Also:

MergeRuleUtils, MergeTotalWeakening, MergeByIfThenElse, MergeIfThenElseAntecedent, MergeWithLatticeAbstraction, MergeWithPredicateAbstraction, MergeRuleCompletion, MergePartnerSelectionDialog

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static interface	MergeRule.MergeRuleProgressListener

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	DISPLAY_NAME
static MergeRule	INSTANCE
private static int	MAX_UPDATE_TERM_DEPTH_FOR_CHECKING Thresholds the maximum depth of right sides in updates for which an equivalence proof is started.
protected static boolean	RIGHT_SIDE_EQUIVALENCE_ONLY_SYNTACTICAL If set to true, merge rules are expected to check the equivalence for right sides (for preserving idempotency) only on a pure syntactical basis.
private static Name	RULE_NAME
private static int	SIMPLIFICATION_TIMEOUT_MS Time threshold in milliseconds for the automatic simplification of formulae (side proofs are stopped after that amount of time).

Constructor Summary

Constructors

Constructor and Description
MergeRule() MergeRule is a Singleton class, therefore constructor only package-wide visible.

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp ruleApp) the rule is applied on the given goal using the information of rule application.
IBuiltInRuleApp	createApp(PosInOccurrence pio, TermServices services)
java.lang.String	displayName() returns the display name of the rule
static ImmutableList<MergePartner>	findPotentialMergePartners(Goal goal, PosInOccurrence pio) Finds all suitable merge partners
boolean	isApplicable(Goal goal, PosInOccurrence pio) We admit top level formulas of the form \<{ ... }\> phi and U \<{ ... }\> phi, where U must be an update in normal form, i.e. a parallel update of elementary updates.
boolean	isApplicableOnSubTerms()
static boolean	isOfAdmissibleForm(Goal goal, PosInOccurrence pio, boolean doMergePartnerCheck) We admit top level formulas of the form \<{ ... }\> phi and U \<{ ... }\> phi, where U must be an update in normal form, i.e. a parallel update of elementary updates.
protected MergeProcedure.ValuesMergeResult	mergeHeaps(MergeProcedure mergeRule, LocationVariable heapVar, Term heap1, Term heap2, SymbolicExecutionState state1, SymbolicExecutionState state2, Term distinguishingFormula, Services services) Merges two heaps in a zip-like procedure.
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>>	mergeStates(MergeProcedure mergeRule, SymbolicExecutionState state1, SymbolicExecutionState state2, Term programCounter, Term distinguishingFormula, Services services) Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services) . p must be the same in both states, so it is supplied separately.
Name	name() the name of the rule
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final MergeRule INSTANCE

DISPLAY_NAME

private static final java.lang.String DISPLAY_NAME

See Also:

Constant Field Values

RULE_NAME

private static final Name RULE_NAME

RIGHT_SIDE_EQUIVALENCE_ONLY_SYNTACTICAL

protected static final boolean RIGHT_SIDE_EQUIVALENCE_ONLY_SYNTACTICAL

If set to true, merge rules are expected to check the equivalence for right sides (for preserving idempotency) only on a pure syntactical basis. If set to false, they are allowed to do a proof to check the equivalence in the respective contexts.

See Also:

Constant Field Values

MAX_UPDATE_TERM_DEPTH_FOR_CHECKING

private static final int MAX_UPDATE_TERM_DEPTH_FOR_CHECKING

Thresholds the maximum depth of right sides in updates for which an equivalence proof is started. We skip the check for equal valuation of this variable if the depth threshold is exceeded by one of the right sides. Experiments show a very big time overhead from a depth of about 8-10 on, or sometimes even earlier.

See Also:

Constant Field Values

SIMPLIFICATION_TIMEOUT_MS

private static final int SIMPLIFICATION_TIMEOUT_MS

Time threshold in milliseconds for the automatic simplification of formulae (side proofs are stopped after that amount of time).

See Also:

Constant Field Values

Constructor Detail

MergeRule

MergeRule()

MergeRule is a Singleton class, therefore constructor only package-wide visible.

Method Detail

name

public Name name()

Description copied from interface: Rule

the name of the rule

Specified by:

name in interface Rule

displayName

public java.lang.String displayName()

Description copied from interface: Rule

returns the display name of the rule

Specified by:

displayName in interface Rule

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

apply

public final ImmutableList<Goal> apply(Goal goal,
                                       Services services,
                                       RuleApp ruleApp)
                                throws RuleAbortException

Description copied from interface: Rule

the rule is applied on the given goal using the information of rule application.

Specified by:

apply in interface Rule

Parameters:

goal - the Goal on which to apply ruleApp

services - the Services with the necessary information about the java programs

ruleApp - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

Throws:

RuleAbortException

mergeStates

protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> mergeStates(MergeProcedure mergeRule,
                                                                                                                 SymbolicExecutionState state1,
                                                                                                                 SymbolicExecutionState state2,
                                                                                                                 Term programCounter,
                                                                                                                 Term distinguishingFormula,
                                                                                                                 Services services)

Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services) . p must be the same in both states, so it is supplied separately.

Override this method for special merge procedures.

Parameters:

mergeRule - The merge procedure to use for the merge.

state1 - First state to merge.

state2 - Second state to merge.

programCounter - The formula \<{ ... }\> phi consisting of the common program counter and the post condition.

distinguishingFormula - The user-specified distinguishing formula. May be null (for automatic generation).

services - The services object.

Returns:

A new merged SE state (U*,C*) which is a weakening of the original states.

mergeHeaps

protected MergeProcedure.ValuesMergeResult mergeHeaps(MergeProcedure mergeRule,
                                                      LocationVariable heapVar,
                                                      Term heap1,
                                                      Term heap2,
                                                      SymbolicExecutionState state1,
                                                      SymbolicExecutionState state2,
                                                      Term distinguishingFormula,
                                                      Services services)

Merges two heaps in a zip-like procedure. The fallback is an if-then-else construct that is tried to be shifted as far inwards as possible.

Override this method for specialized heap merge procedures.

Parameters:

heapVar - The heap variable for which the values should be merged.

heap1 - The first heap term.

heap2 - The second heap term.

state1 - SE state for the first heap term.

state2 - SE state for the second heap term

services - The services object.

distinguishingFormula - The user-specified distinguishing formula. May be null (for automatic generation).

Returns:

A merged heap term.

isApplicable

public boolean isApplicable(Goal goal,
                            PosInOccurrence pio)

We admit top level formulas of the form \<{ ... }\> phi and U \<{ ... }\> phi, where U must be an update in normal form, i.e. a parallel update of elementary updates.

Specified by:

isApplicable in interface BuiltInRule

Parameters:

goal - Current goal.

pio - Position of selected sequent formula.

Returns:

true iff a suitable top level formula for merging.

isOfAdmissibleForm

public static boolean isOfAdmissibleForm(Goal goal,
                                         PosInOccurrence pio,
                                         boolean doMergePartnerCheck)

We admit top level formulas of the form \<{ ... }\> phi and U \<{ ... }\> phi, where U must be an update in normal form, i.e. a parallel update of elementary updates. We require that phi does not contain a Java block.

Parameters:

goal - Current goal.

pio - Position of selected sequent formula.

doMergePartnerCheck - Checks for available merge partners iff this flag is set to true.

Returns:

true iff a suitable top level formula for merging.

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule

createApp

public IBuiltInRuleApp createApp(PosInOccurrence pio,
                                 TermServices services)

Specified by:

createApp in interface BuiltInRule

findPotentialMergePartners

public static ImmutableList<MergePartner> findPotentialMergePartners(Goal goal,
                                                                     PosInOccurrence pio)

Finds all suitable merge partners

Parameters:

goal - Current goal to merge.

pio - Position of update-program counter formula in goal.

start - Node to start the search with.

services - The services object.

Returns:

A list of suitable merge partners. May be empty if none exist.