daikon.derive
Class Derivation

Object
  Derivation

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

BinaryDerivation, TernaryDerivation, UnaryDerivation

public abstract class Derivation
extends Object
implements Serializable, Cloneable

Structure that represents a derivation; can generate values and derived variables from base variables. A Derivation has a set of base VarInfo from which the Derivation is derived. Use getVarInfo() to get the VarInfo representation of this Derivation. When we want the actual value of this derivation, we pass in a ValueTuple; the Derivation picks out the values of its base variables and finds the value of the derived variable. Use computeValueandModified() to get value. Derivations are created by DerivationFactory.

See Also:

Serialized Form

Field Summary

static Logger	debug Debug tracer.
static boolean	dkconfig_disable_derived_variables Boolean.
boolean	missing_array_bounds

Constructor Summary

Derivation()

Method Summary

abstract boolean	canBeMissing()
int	complexity() Return the complexity of this derivation.
abstract ValueAndModified	computeValueAndModified(ValueTuple full_vt)
abstract int	derivedDepth() Returns how many levels of derivation this Derivation is based on.
String	esc_name(String index) Returns the name of this variable in ESC format.
VarInfo	get_array_var() Returns the array variable that underlies this slice.
Quantify.Term	get_lower_bound() Returns the lower bound of a slice.
Quantify.Term	get_upper_bound() Returns the lower bound of a slice.
abstract VarInfo[]	getBases()
VarInfo	getVarInfo() Get the VarInfo that this would represent.
protected String	inside_esc_name(VarInfo vi, boolean in_orig, int shift) Returns the esc name of a variable which is included inside an an expression (such as orig(a[vi])).
protected String	inside_jml_name(VarInfo vi, boolean in_orig, int shift) Returns the jml name of a variable which is included inside an an expression (such as orig(a[vi])).
boolean	is_prestate_version(Derivation d) Returns true if d is the prestate version of this.
abstract boolean	isDerivedFromNonCanonical()
protected abstract boolean	isParam()
abstract boolean	isSameFormula(Derivation other)
String	jml_name(String index) Returns the name of this variable in JML format.
protected void	makeVarInfo_common_setup(VarInfo vi)
protected abstract VarInfo	makeVarInfo() Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().
boolean	missingOutOfBounds() True if we have encountered to date any missing values in this derivation due to array indices being out of bounds.
protected String	shift_str(int shift) Returns a string that corresponds to the the specified shift
String	simplify_name() Returns the name of this variable in simplify format
abstract Derivation	switchVars(VarInfo[] old_vars, VarInfo[] new_vars)

Methods inherited from class Object

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

Field Detail

dkconfig_disable_derived_variables

public static boolean dkconfig_disable_derived_variables

Boolean. If true, Daikon will not create any derived variables. Derived variables, which are combinations of variables that appeared in the program, like array[index] if array and index appeared, can increase the number of properties Daikon finds, especially over sequences. However, derived variables increase Daikon's time and memory usage, sometimes dramatically. If false, individual kinds of derived variables can be enabled or disabled individually using configuration options under daikon.derive.

debug

public static final Logger debug

Debug tracer.

missing_array_bounds

public boolean missing_array_bounds

Constructor Detail

Derivation

public Derivation()

Method Detail

switchVars

public abstract Derivation switchVars(VarInfo[] old_vars,
                                      VarInfo[] new_vars)

getBases

public abstract VarInfo[] getBases()

Returns:

array of the VarInfos this was derived from

computeValueAndModified

public abstract ValueAndModified computeValueAndModified(ValueTuple full_vt)

Parameters:

full_vt - The set of values in a program point that will be used to derive the value.

Returns:

a pair of: the derived value and whether the variable counts as modified.

getVarInfo

public VarInfo getVarInfo()

Get the VarInfo that this would represent. However, the VarInfo can't be used to obtain values without further modification -- use computeValueAndModified() for this.

See Also:

computeValueAndModified(daikon.ValueTuple)

makeVarInfo

protected abstract VarInfo makeVarInfo()

Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().

makeVarInfo_common_setup

protected void makeVarInfo_common_setup(VarInfo vi)

isParam

protected abstract boolean isParam()

missingOutOfBounds

public boolean missingOutOfBounds()

True if we have encountered to date any missing values in this derivation due to array indices being out of bounds. This can happen with both simple subscripts and subsequences. Note that this becomes true as we are running, it cannot be set in advance (which would require a first pass).

isDerivedFromNonCanonical

public abstract boolean isDerivedFromNonCanonical()

derivedDepth

public abstract int derivedDepth()

Returns how many levels of derivation this Derivation is based on. The depth counts this as well as the depths of its bases.

isSameFormula

public abstract boolean isSameFormula(Derivation other)

Returns:

true iff other and this represent the same derivation (modulo the variable they are applied to). Default implentation will just checks runtime type, but subclasses with state (e.g. SequenceInitial index) should match that, too.

canBeMissing

public abstract boolean canBeMissing()

get_lower_bound

public Quantify.Term get_lower_bound()

Returns the lower bound of a slice. Throws an error if this is not a slice. Slices should override.

get_upper_bound

public Quantify.Term get_upper_bound()

Returns the lower bound of a slice. Throws an error if this is not a slice. Slices should override.

get_array_var

public VarInfo get_array_var()

Returns the array variable that underlies this slice. Throws an error if this is not a slice. Slices should override.

esc_name

public String esc_name(String index)

Returns the name of this variable in ESC format. If an index is specified, it is used as an array index. It is an error to specify an index on a non-array variable

jml_name

public String jml_name(String index)

Returns the name of this variable in JML format. If an index is specified, it is used as an array index. It is an error to specify an index on a non-array variable

simplify_name

public String simplify_name()

Returns the name of this variable in simplify format

is_prestate_version

public boolean is_prestate_version(Derivation d)

Returns true if d is the prestate version of this. Returns true if this and d are of the same derivation with the same formula and have the same bases.

complexity

public int complexity()

Return the complexity of this derivation. This is only for the derivation itself and not for the variables included in the derivation. The default implementation returns 1 (which is the added complexity of an derivation). Subclasses that add additional complexity (such as an offset) should override

shift_str

protected String shift_str(int shift)

Returns a string that corresponds to the the specified shift

inside_esc_name

protected String inside_esc_name(VarInfo vi,
                                 boolean in_orig,
                                 int shift)

Returns the esc name of a variable which is included inside an an expression (such as orig(a[vi])). If the expression is orig, the orig is implied for this variable.

inside_jml_name

protected String inside_jml_name(VarInfo vi,
                                 boolean in_orig,
                                 int shift)

Returns the jml name of a variable which is included inside an an expression (such as orig(a[vi])). If the expression is orig, the orig is implied for this variable.