Package org.checkerframework.dataflow.reachingdef

Class ReachingDefinitionStore

java.lang.Object

org.checkerframework.dataflow.reachingdef.ReachingDefinitionStore

All Implemented Interfaces:

Store<ReachingDefinitionStore>

public class ReachingDefinitionStore
extends java.lang.Object
implements Store<ReachingDefinitionStore>

A reaching definition store contains a set of reaching definitions represented by ReachingDefinitionNode

Nested Class Summary

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Store

Store.FlowRule, Store.Kind

Constructor Summary

Constructors

Constructor	Description
ReachingDefinitionStore()	Create a new ReachDefinitionStore.
ReachingDefinitionStore(java.util.Set<ReachingDefinitionNode> reachingDefSet)	Create a new ReachDefinitionStore.

Method Summary

Modifier and Type	Method	Description
boolean	canAlias(JavaExpression a, JavaExpression b)	Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).
ReachingDefinitionStore	copy()	Returns an exact copy of this store.
boolean	equals(@Nullable java.lang.Object obj)	Returns true if this is equal to the given argument.
int	hashCode()
void	killDef(Node defTarget)	Remove the information of a reaching definition from the reaching definition set.
ReachingDefinitionStore	leastUpperBound(ReachingDefinitionStore other)	Compute the least upper bound of two stores.
void	putDef(ReachingDefinitionNode def)	Add a reaching definition to the reaching definition set.
java.lang.String	toString()
java.lang.String	visualize(CFGVisualizer<?,ReachingDefinitionStore,?> viz)	Delegate visualization responsibility to a visualizer.
ReachingDefinitionStore	widenedUpperBound(ReachingDefinitionStore previous)	Compute an upper bound of two stores that is wider than the least upper bound of the two stores.

Methods inherited from class java.lang.Object

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

Constructor Detail

ReachingDefinitionStore

public ReachingDefinitionStore()

Create a new ReachDefinitionStore.

ReachingDefinitionStore

public ReachingDefinitionStore(java.util.Set<ReachingDefinitionNode> reachingDefSet)

Create a new ReachDefinitionStore.

Parameters:

reachingDefSet - a set of reaching definition nodes. The parameter is captured and the caller should not retain an alias.

Method Detail

killDef

public void killDef(Node defTarget)

Remove the information of a reaching definition from the reaching definition set.

Parameters:

defTarget - target of a reaching definition

putDef

public void putDef(ReachingDefinitionNode def)

Add a reaching definition to the reaching definition set.

Parameters:

def - a reaching definition

equals

public boolean equals(@Nullable java.lang.Object obj)

Description copied from interface: Store

Returns true if this is equal to the given argument.

Specified by:

equals in interface Store<ReachingDefinitionStore>

Overrides:

equals in class java.lang.Object

Parameters:

obj - the object to compare against this

Returns:

true if this is equal to the given argument

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

copy

public ReachingDefinitionStore copy()

Description copied from interface: Store

Returns an exact copy of this store.

Specified by:

copy in interface Store<ReachingDefinitionStore>

Returns:

an exact copy of this store

leastUpperBound

public ReachingDefinitionStore leastUpperBound(ReachingDefinitionStore other)

Description copied from interface: Store

Compute the least upper bound of two stores.

Important: This method must fulfill the following contract:

• Does not change this.
• Does not change other.
• Returns a fresh object which is not aliased yet.
• Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
• Is commutative.

Specified by:

leastUpperBound in interface Store<ReachingDefinitionStore>

widenedUpperBound

public ReachingDefinitionStore widenedUpperBound(ReachingDefinitionStore previous)

Description copied from interface: Store

Compute an upper bound of two stores that is wider than the least upper bound of the two stores. Used to jump to a higher abstraction to allow faster termination of the fixed point computations in Analysis. previous must be the previous store.

A particular analysis might not require widening and should implement this method by calling leastUpperBound.

Important: This method must fulfill the following contract:

• Does not change this.
• Does not change previous.
• Returns a fresh object which is not aliased yet.
• Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
• Is commutative.

Specified by:

widenedUpperBound in interface Store<ReachingDefinitionStore>

Parameters:

previous - must be the previous store

canAlias

public boolean canAlias(JavaExpression a,
                        JavaExpression b)

Description copied from interface: Store

Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).

Specified by:

canAlias in interface Store<ReachingDefinitionStore>

visualize

public java.lang.String visualize(CFGVisualizer<?,ReachingDefinitionStore,?> viz)

Description copied from interface: Store

Delegate visualization responsibility to a visualizer.

Specified by:

visualize in interface Store<ReachingDefinitionStore>

Parameters:

viz - the visualizer to visualize this store

Returns:

the String representation of this store

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object