daikon
Class VarInfoName

Object
  VarInfoName

All Implemented Interfaces:

Serializable, Comparable<VarInfoName>

Direct Known Subclasses:

VarInfoName.Add, VarInfoName.Elements, VarInfoName.Field, VarInfoName.FunctionOf, VarInfoName.FunctionOfN, VarInfoName.Poststate, VarInfoName.Prestate, VarInfoName.Simple, VarInfoName.SizeOf, VarInfoName.Slice, VarInfoName.Subscript, VarInfoName.TypeOf

public abstract class VarInfoName
extends Object
implements Serializable, Comparable<VarInfoName>

VarInfoName represents the "name" of a variable. Calling it a "name", however, is somewhat misleading. It can be some expression that includes more than one variable, term, etc. We separate this from the VarInfo itself because clients wish to manipulate names into new expressions independent of the VarInfo that they might be associated with. VarInfoName's child classes are specific types of names, like applying a function to something. For example, "a" is a name, and "sin(a)" is a name that is the name "a" with the function "sin" applied to it.

See Also:

Serialized Form

Nested Class Summary

static class	VarInfoName.AbstractVisitor<T> Traverse the tree elements that have exactly one branch (so the traversal order doesn't matter).
static class	VarInfoName.Add An integer amount more or less than some other value, like "x+2".
static class	VarInfoName.BooleanAndVisitor
static class	VarInfoName.Elements The elements of a container, like "term[]".
static class	VarInfoName.ElementsFinder Use to traverse a tree, find the first (elements ...) node, and report whether it's in pre or post-state.
static class	VarInfoName.Field A 'getter' operation for some field, like a.foo.
static class	VarInfoName.Finder Finds if a given VarInfoName is contained in a set of nodes in the VarInfoName tree using == comparison.
static class	VarInfoName.FunctionOf A function over a term, like "sum(argument)".
static class	VarInfoName.FunctionOfN A function of multiple parameters.
static class	VarInfoName.InorderFlattener Use to collect all elements in a tree into an inorder-traversal list.
static class	VarInfoName.Intersection Intersection of two sequences.
static class	VarInfoName.IsAllNonPoststateVisitor
static class	VarInfoName.IsAllPrestateVisitor
static class	VarInfoName.LexicalComparator Compare VarInfoNames alphabetically.
static class	VarInfoName.NodeFinder Use to report whether a node is in a pre- or post-state context.
static class	VarInfoName.NoReturnValue
static class	VarInfoName.PostPreConverter Replace pre states by normal variables, and normal variables by post states.
static class	VarInfoName.Poststate The poststate value of a term, like "new(term)".
static class	VarInfoName.Prestate The prestate value of a term, like "orig(term)" or "\old(term)".
static class	VarInfoName.QuantHelper Helper for writing parts of quantification expressions.
static class	VarInfoName.QuantifierVisitor A quantifier visitor can be used to search a tree and return all unquantified sequences (e.g. a[] or a[i..j]).
static class	VarInfoName.Replacer A Replacer is a Visitor that makes a copy of a tree, but replaces some node (and its children) with another.
static class	VarInfoName.Simple A simple identifier like "a", etc.
static class	VarInfoName.SimpleNamesVisitor
static class	VarInfoName.SizeOf The size of a contained sequence; form is like "size(sequence)" or "sequence.length".
static class	VarInfoName.Slice A slice of elements from a sequence, like "sequence[i..j]".
static class	VarInfoName.Subscript An element from a sequence, like "sequence[index]".
static interface	VarInfoName.Transformer Specifies a function that performs a transformation on VarInfoNames.
static class	VarInfoName.TypeOf The type of the term, like "term.getClass()" or "\typeof(term)".
static class	VarInfoName.Union Union of two sequences.
static interface	VarInfoName.Visitor<T> Visitor framework for processing of VarInfoNames.

Field Summary

static Logger	debug Debugging Logger.
static VarInfoName.Transformer	IDENTITY_TRANSFORMER A pass-through transformer.
static VarInfoName	ORIG_THIS
static boolean	testCall
static VarInfoName	THIS
static VarInfoName	ZERO

Constructor Summary

VarInfoName()

Method Summary

abstract <T> T	accept(VarInfoName.Visitor<T> v) Accept the actions of a visitor.
VarInfoName	applyAdd(int amount) Returns a name for the this term plus a constant, like "this-1" or "this+1".
VarInfoName	applyDecrement() Returns a name for the decrement of this term, like "this-1".
VarInfoName	applyElements() Returns a name for the elements of a container (as opposed to the identity of the container) like "this[]" or "(elements this)".
VarInfoName	applyField(String field) Returns a 'getter' operation for some field of this name, like a.foo if this is a.
VarInfoName	applyFunction(String function) Returns a name for a unary function applied to this object.
static VarInfoName	applyFunctionOfN(String function, List<VarInfoName> vars) Returns a name for a function applied to more than one argument.
static VarInfoName	applyFunctionOfN(String function, VarInfoName[] vars) Returns a name for a function of more than one argument.
VarInfoName	applyIncrement() Returns a name for the increment of this term, like "this+1".
VarInfoName	applyIntersection(VarInfoName seq2) Returns a name for the intersection of with another sequence, like "intersect(a[], b[])".
VarInfoName	applyPoststate() Returns a name for a the poststate value of this object; form is like "new(this)" or "\new(this)".
VarInfoName	applyPrestate() Returns a name for a the prestate value of this object; form is like "orig(this)" or "\old(this)".
VarInfoName	applySize() Returns a name for the size of this (this object should be a sequence).
VarInfoName	applySlice(VarInfoName i, VarInfoName j) Returns a name for a slice of element selected from a sequence, like "this[i..j]".
VarInfoName	applySubscript(VarInfoName index) Returns a name for an element selected from a sequence, like "this[i]".
VarInfoName	applyTypeOf() Returns a name for the type of this object; form is like "this.getClass()" or "\typeof(this)".
VarInfoName	applyUnion(VarInfoName seq2) Returns a name for the union of this with another sequence, like "union(a[], b[])".
int	compareTo(VarInfoName other)
protected abstract String	dbc_name_impl(VarInfo v) Return the name in the DBC style output format.
String	dbc_name(VarInfo var) Return the String representation of this name in the dbc style output format.
boolean	equals(Object o)
boolean	equals(VarInfoName other)
protected abstract String	esc_name_impl() Returns the String representation of this name in the ESC style output format.
String	esc_name() Return the String representation of this name in the esc style output format.
VarInfoName[]	getSliceBounds() If this is a slice, (potentially in pre-state), return its lower and upper bounds, which can be subtracted to get one less than its size.
int	hashCode()
boolean	hasNode(VarInfoName node)
boolean	hasNodeOfType(Class<?> type)
boolean	hasTypeOf()
protected abstract String	identifier_name_impl() Returns the name using only letters, numbers, and underscores.
String	identifier_name() Return the String representation of this name using only letters, numbers, and underscores.
boolean	includesSimpleName(String name)
Collection<VarInfoName>	inOrderTraversal()
boolean	inPrestateContext(VarInfoName node)
VarInfoName	intern()
boolean	isAllPrestate()
boolean	isApplySizeSafe()
boolean	isLiteralConstant()
boolean	isThis() Returns whether or not this name refers to the 'this' variable of a class.
protected abstract String	java_name_impl(VarInfo v) Return the String representation of this name in java format.
String	java_name(VarInfo v) Return the String representation of this name in the java style output format.
protected abstract String	jml_name_impl(VarInfo v) Returns the name in JML style output format.
String	jml_name(VarInfo v) Return the String representation of this name in the JML style output format
VarInfoName	JMLElementCorrector()
protected abstract String	name_impl() Returns the String representation of this name in the default output format.
String	name_using(OutputFormat format, VarInfo vi)
String	name() Return the String representation of this name in the default output format.
static VarInfoName	parse(String name) Given the standard String representation of a variable name (like what appears in the normal output format), return the corresponding VarInfoName.
VarInfoName	replace(VarInfoName node, VarInfoName replacement) Replace the first instance of node by replacement, in the data structure rooted at this.
VarInfoName	replaceAll(VarInfoName node, VarInfoName replacement) Replace all instances of node by replacement, in the data structure rooted at this.
protected abstract String	repr_impl() return the name in a verbose debugging format.
String	repr()
protected abstract String	simplify_name_impl(boolean prestate) Returns the String representation of this name in the simplify output format in either prestate or poststate context
String	simplify_name()
protected String	simplify_name(boolean prestate)
String	toString()

Methods inherited from class Object

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

Field Detail

debug

public static Logger debug

Debugging Logger.

testCall

public static boolean testCall

ZERO

public static final VarInfoName ZERO

THIS

public static final VarInfoName THIS

ORIG_THIS

public static final VarInfoName ORIG_THIS

IDENTITY_TRANSFORMER

public static final VarInfoName.Transformer IDENTITY_TRANSFORMER

A pass-through transformer.

Constructor Detail

VarInfoName

public VarInfoName()

Method Detail

parse

public static VarInfoName parse(String name)

Given the standard String representation of a variable name (like what appears in the normal output format), return the corresponding VarInfoName. This method can't parse all the strings that the VarInfoName name() method might produce, but it should be able to handle anything that appears in a decls file. Specifically, it can only handle a subset of the grammar of derived variables. For some values of "name", "name.equals(parse(e.name()))" might throw an exception, but if it completes normally, the result should be true.

name

public String name()

Return the String representation of this name in the default output format.

Returns:

the string representation (interned) of this name, in the default output format

name_impl

protected abstract String name_impl()

Returns the String representation of this name in the default output format. Result is not interned; the client (name()) does so, then caches the interned value.

esc_name

public String esc_name()

Return the String representation of this name in the esc style output format.

Returns:

the string representation (interned) of this name, in the esc style output format

esc_name_impl

protected abstract String esc_name_impl()

Returns the String representation of this name in the ESC style output format. Cached by esc_name()

simplify_name

public String simplify_name()

Returns:

the string representation (interned) of this name, in the Simplify tool output format in the pre-state context.

simplify_name

protected String simplify_name(boolean prestate)

Returns:

the string representation (interned) of this name, in the Simplify tool output format, in the given pre/post-state context.

simplify_name_impl

protected abstract String simplify_name_impl(boolean prestate)

Returns the String representation of this name in the simplify output format in either prestate or poststate context

java_name

public String java_name(VarInfo v)

Return the String representation of this name in the java style output format.

Returns:

the string representation (interned) of this name, in the java style output format

java_name_impl

protected abstract String java_name_impl(VarInfo v)

Return the String representation of this name in java format. Cached and interned by java_name()

jml_name

public String jml_name(VarInfo v)

Return the String representation of this name in the JML style output format

jml_name_impl

protected abstract String jml_name_impl(VarInfo v)

Returns the name in JML style output format. Cached and interned by jml_name()

dbc_name

public String dbc_name(VarInfo var)

Return the String representation of this name in the dbc style output format.

Parameters:

var - the VarInfo which goes along with this VarInfoName. Used to determine the type of the variable. If var is null, the only repercussion is that if `this' is an "orig(x)" expression, it will be formatted in jml-style, something like "\old(x)". If var is not null and `this' is an "orig(x)" expressions, it will be formatted in Jtest's DBC style, as "$pre(, x)".

Returns:

the string representation (interned) of this name, in the dbc style output format.

dbc_name_impl

protected abstract String dbc_name_impl(VarInfo v)

Return the name in the DBC style output format. If v is null, uses JML style instead. Cached and interned by dbc_name()

identifier_name

public String identifier_name()

Return the String representation of this name using only letters, numbers, and underscores.

identifier_name_impl

protected abstract String identifier_name_impl()

Returns the name using only letters, numbers, and underscores. Cached and interned by identifier_name()

name_using

public String name_using(OutputFormat format,
                         VarInfo vi)

Returns:

name of this in the specified format

repr

public String repr()

Returns:

the name, in a debugging format

repr_impl

protected abstract String repr_impl()

return the name in a verbose debugging format. Cached by repr

intern

public VarInfoName intern()

isLiteralConstant

public boolean isLiteralConstant()

Returns:

true when this is "0", "-1", "1", etc.

inOrderTraversal

public Collection<VarInfoName> inOrderTraversal()

Returns:

the nodes of this, as given by an inorder traversal.

hasNode

public boolean hasNode(VarInfoName node)

Returns:

true iff the given node can be found in this. If the node has children, the whole subtree must match.

hasNodeOfType

public boolean hasNodeOfType(Class<?> type)

Returns:

true iff a node of the given type exists in this

hasTypeOf

public boolean hasTypeOf()

Returns:

true iff a TypeOf node exists in this

isThis

public boolean isThis()

Returns whether or not this name refers to the 'this' variable of a class. True for both normal and prestate versions of the variable

inPrestateContext

public boolean inPrestateContext(VarInfoName node)

Returns:

true if the given node is in a prestate context within this tree; the node must be a member of this tree.

isAllPrestate

public boolean isAllPrestate()

Returns:

true if every variable in the name is an orig(...) variable.

includesSimpleName

public boolean includesSimpleName(String name)

Returns:

true if this VarInfoName contains a simple variable whose name is NAME.

replace

public VarInfoName replace(VarInfoName node,
                           VarInfoName replacement)

Replace the first instance of node by replacement, in the data structure rooted at this.

replaceAll

public VarInfoName replaceAll(VarInfoName node,
                              VarInfoName replacement)

Replace all instances of node by replacement, in the data structure rooted at this.

equals

public boolean equals(Object o)

Overrides:

equals in class Object

equals

public boolean equals(VarInfoName other)

hashCode

public int hashCode()

Overrides:

hashCode in class Object

compareTo

public int compareTo(VarInfoName other)

Specified by:

compareTo in interface Comparable<VarInfoName>

toString

public String toString()

Overrides:

toString in class Object

isApplySizeSafe

public boolean isApplySizeSafe()

Returns:

true iff applySize will not throw an exception

See Also:

applySize()

applySize

public VarInfoName applySize()

Returns a name for the size of this (this object should be a sequence). Form is like "size(a[])" or "a.length".

getSliceBounds

public VarInfoName[] getSliceBounds()

If this is a slice, (potentially in pre-state), return its lower and upper bounds, which can be subtracted to get one less than its size.

applyFunction

public VarInfoName applyFunction(String function)

Returns a name for a unary function applied to this object. The result is like "sum(this)".

applyFunctionOfN

public static VarInfoName applyFunctionOfN(String function,
                                           List<VarInfoName> vars)

Returns a name for a function applied to more than one argument. The result is like "sum(var1, var2)".

Parameters:

function - the name of the function

vars - The arguments to the function, of type VarInfoName

applyFunctionOfN

public static VarInfoName applyFunctionOfN(String function,
                                           VarInfoName[] vars)

Returns a name for a function of more than one argument. The result is like "sum(var1, var2)".

Parameters:

function - the name of the function

vars - The arguments to the function

applyIntersection

public VarInfoName applyIntersection(VarInfoName seq2)

Returns a name for the intersection of with another sequence, like "intersect(a[], b[])".

applyUnion

public VarInfoName applyUnion(VarInfoName seq2)

Returns a name for the union of this with another sequence, like "union(a[], b[])".

applyField

public VarInfoName applyField(String field)

Returns a 'getter' operation for some field of this name, like a.foo if this is a.

applyTypeOf

public VarInfoName applyTypeOf()

Returns a name for the type of this object; form is like "this.getClass()" or "\typeof(this)".

applyPrestate

public VarInfoName applyPrestate()

Returns a name for a the prestate value of this object; form is like "orig(this)" or "\old(this)".

applyPoststate

public VarInfoName applyPoststate()

Returns a name for a the poststate value of this object; form is like "new(this)" or "\new(this)".

applyAdd

public VarInfoName applyAdd(int amount)

Returns a name for the this term plus a constant, like "this-1" or "this+1".

applyDecrement

public VarInfoName applyDecrement()

Returns a name for the decrement of this term, like "this-1".

applyIncrement

public VarInfoName applyIncrement()

Returns a name for the increment of this term, like "this+1".

applyElements

public VarInfoName applyElements()

Returns a name for the elements of a container (as opposed to the identity of the container) like "this[]" or "(elements this)".

applySubscript

public VarInfoName applySubscript(VarInfoName index)

Returns a name for an element selected from a sequence, like "this[i]".

applySlice

public VarInfoName applySlice(VarInfoName i,
                              VarInfoName j)

Returns a name for a slice of element selected from a sequence, like "this[i..j]". If an endpoint is null, it means "from the start" or "to the end".

accept

public abstract <T> T accept(VarInfoName.Visitor<T> v)

Accept the actions of a visitor.

JMLElementCorrector

public VarInfoName JMLElementCorrector()