|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object avrora.stack.AbstractArithmetic
The AbstractArithmetic
arithmetic class implements operations that are useful for working on
abstract integers which are represented as characters.
AbstractState
are canonical for efficiency and
clarity.
Field Summary | |
static char |
FALSE
The FALSE field represents the abstract bit that is known to be false. |
static char |
TRUE
The TRUE field represents the abstract bit that is known to be true. |
static char |
UNKNOWN
The UNKNOWN field represents the abstract value where none of the bits are known. |
static char |
ZERO
The ZERO field represents the abstract value where all bits are known to be zero. |
Constructor Summary | |
AbstractArithmetic()
|
Method Summary | |
static char |
add(char av1,
char av2)
The add() method performs addition of two abstract values. |
static char |
and(char av1,
char av2)
The and() method computes the logical bitwise AND of two abstract values. |
static char |
and(char av1,
char av2,
char av3)
The and() method computes the logical bitwise AND of three abstract values. |
static boolean |
areEqual(char val1,
char val2)
The areEqual() method tests whether two abstract values are equivalent in the "abstract
value" sense. |
static boolean |
areKnown(char av1,
char av2)
The areKnown() method tests whether two abstract values each represent a single, fully
known value. |
static char |
bitsOf(char av1)
The bitsOf() method returns the lower 8 bits (the value bits) of the abstract value,
ignoring the known bit mask. |
static char |
bitToChar(char av1)
The toString() method converts an 1-bit abstract value to a string representation. |
static char |
canon(char av1)
The canon() method canonicalizes an abstract value. |
static char |
canon(char mask,
char av1)
The canon() method canonicalizes an abstract value. |
static int |
ceiling(char av1)
The ceiling() function computes the concrete value with all unknown bits set to one. |
static int |
ceiling(char av1,
char av2)
The ceiling() function computes the concrete value with all unknown bits set to one. |
static char |
commonMask(char av1,
char av2)
The commonMask() method computes the intersection of the known bit masks of two abstract
values. |
static char |
commonMask(char av1,
char av2,
char av3)
The commonMask() method computes the intersection of the known bit masks of three abstract
values. |
static char |
couldBeEqual(char av1,
char av2)
The couldBeEqual() method performs a "fuzzy" equality test between two abstract values. |
static char |
couldBeZero(char av1)
The couldBeZero method performs a "fuzzy" equality test against zero for an abstract
value. |
static char |
couldBeZero(char av1,
char av2)
The couldBeZero() method performs a "fuzzy" equality test against zero for two abstract
values. |
static char |
decrement(char av1)
The decrement() method simply subtracts 1 to the abstract value. |
static int |
floor(char av1)
The floor() function computes the concrete value with all unknown bits set to zero. |
static int |
floor(char av1,
char av2)
The floor() function computes the concrete value with all unknown bits set to zero. |
static char |
getBit(char av1,
int bit)
The getBit() method extracts the specified abstract bit from the specified abstract
value. |
static char |
increment(char av1)
The increment() method simply adds 1 to the abstract value. |
static boolean |
isUnknown(char av1)
The isKnown() method tests whether an abstract value represents a single, fully known
value. |
static byte |
knownBitsOf(char val)
The knownBitsOf() method returns computes the concrete value from the given abstract value
where all unknown bits of the abstract value are set to zero. |
static char |
knownVal(byte cv1)
The knownVal() method creates a canonical abstract value from the given concrete value. |
static char |
logicalAnd(char av1,
char av2)
The logicalAnd method computes the logical bitwise AND of two abstract values. |
static char |
maskOf(char av1)
The maskOf() method returns the upper 8 bits of the abstract (the mask bits) of the
abstract value. |
static char |
merge(byte cv1,
byte cv2)
The merge() method merges abstract values. |
static char |
merge(byte cv1,
byte cv2,
byte cv3)
The merge() method merges abstract values. |
static char |
merge(byte cv1,
byte cv2,
byte cv3,
byte cv4)
The merge() method merges abstract values. |
static char |
merge(char av1,
byte cv2)
The merge() method merges abstract values. |
static char |
merge(char av1,
char av2)
The merge() method merges abstract values. |
static char |
mergeMask(char mask,
char av1)
The mergeMask() merges the given abstract value with the known bit mask passed. |
static char |
not(char av1)
The not() method computes the bitwise negation (one's complement) of the specified
abstract value |
static char |
or(char av1,
char av2)
The or() method computes the logical bitwise or of two abstract values. |
static char |
or(char av1,
char av2,
char av3)
The or() method computes the logical bitwise or of three abstract values. |
static char |
setBit(char av1,
int bit,
char on)
The setBit() method updates the specified abstract bit within the specified abstract
value. |
static char |
shiftLeftOne(char av1)
The shiftLeftOne() method shifts the abstract value left by one bit. |
static char |
shiftLeftOne(char av1,
char lowbit)
The shiftLeftOne() method shifts the abstract value left by one bit and sets the lowest
bit to the given value. |
static char |
subtract(char av1,
char av2)
The add() method performs subtraction of two abstract values. |
static java.lang.String |
toShortString(char av1)
The toShortString() method converts an 8-bit abstract value to a string representation.
|
static java.lang.String |
toString(char av1)
The toString() method converts an 8-bit abstract value to a string representation. |
static void |
toString(char av1,
java.lang.StringBuffer buf)
The toString() method converts an 8-bit abstract value to a string representation and
appends it to the end of the given string buffer. |
static char |
xor(char av1,
char av2)
The xor() method computes the bitwise exclusive or operation on the two given abstract
values. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static final char ZERO
ZERO
field represents the abstract value where all bits are known to be zero.
public static final char TRUE
TRUE
field represents the abstract bit that is known to be true.
public static final char FALSE
FALSE
field represents the abstract bit that is known to be false.
public static final char UNKNOWN
UNKNOWN
field represents the abstract value where none of the bits are known.
Constructor Detail |
public AbstractArithmetic()
Method Detail |
public static char merge(byte cv1, byte cv2)
merge()
method merges abstract values. The merge of two abstract values is defined
intuitively as the intersection of the known bits of the two values that agree, and all other bits are
unknown. This variant of the method accepts two concrete values to merge.
cv1
- the first (concrete) value to mergecv2
- the second (concrete) value to merge
public static char merge(char av1, byte cv2)
merge()
method merges abstract values. The merge of two abstract values is defined
intuitively as the intersection of the known bits of the two values that agree, and all other bits are
unknown. This variant of the method accepts one abstract value and one concrete value to merge
together.
av1
- the first (abstract) value to mergecv2
- the second (concrete) value to merge
public static char merge(byte cv1, byte cv2, byte cv3)
merge()
method merges abstract values. The merge of two abstract values is defined
intuitively as the intersection of the known bits of the two values that agree, and all other bits are
unknown. This variant of the method accepts three concrete values to merge.
cv1
- the first (concrete) value to mergecv2
- the second (concrete) value to mergecv3
- the third (concrete) value to merge
public static char merge(byte cv1, byte cv2, byte cv3, byte cv4)
merge()
method merges abstract values. The merge of two abstract values is defined
intuitively as the intersection of the known bits of the two values that agree, and all other bits are
unknown. This variant of the method accepts four concrete values to merge.
cv1
- the first (concrete) value to mergecv2
- the second (concrete) value to mergecv3
- the third (concrete) value to mergecv4
- the fourth (concrete) value to merge
public static char merge(char av1, char av2)
merge()
method merges abstract values. The merge of two abstract values is defined
intuitively as the intersection of the known bits of the two values that agree, and all other bits are
unknown. This variant of the method accepts two abstract values to merge.
av1
- the first (abstract) value to mergeav2
- the second (abstract) value to merge
public static boolean isUnknown(char av1)
isKnown()
method tests whether an abstract value represents a single, fully known
value.
av1
- the abstract value to test
public static boolean areKnown(char av1, char av2)
areKnown()
method tests whether two abstract values each represent a single, fully
known value.
av1
- the first abstract value to testav2
- the second abstract value to test
public static boolean areEqual(char val1, char val2)
areEqual()
method tests whether two abstract values are equivalent in the "abstract
value" sense. Two abstract values are equivalent if their known bits are equal and their known masks
are equal
val1
- the first abstract valueval2
- the second abstract value
public static char canon(char av1)
canon()
method canonicalizes an abstract value. An abstract value is canonical if all
of its unknown bits are set to zero. This variant takes a single abstract value and ensures that it is
canonical.
av1
- the abstract value to canonicalize
public static char canon(char mask, char av1)
canon()
method canonicalizes an abstract value. An abstract value is canonical if all
of its unknown bits are set to zero. This variant takes a mask and an abstract value and returns an
abstract value that is canonical with the specified known bit mask.
mask
- the known bit mask to canonicalize with respect toav1
- the abstract value to canonicalize
public static char knownVal(byte cv1)
knownVal()
method creates a canonical abstract value from the given concrete value.
cv1
- the concrete value to create an abstract value for
public static byte knownBitsOf(char val)
knownBitsOf()
method returns computes the concrete value from the given abstract value
where all unknown bits of the abstract value are set to zero.
val
- the abstract value to get the known bits of
public static char bitsOf(char av1)
bitsOf()
method returns the lower 8 bits (the value bits) of the abstract value,
ignoring the known bit mask. For a canonical abstract value, this method will return the same result as
knownBitsOf
, because, by definition, the unknown bits of a canonical abstract value are
set to zero.
av1
- the abstract value
public static char maskOf(char av1)
maskOf()
method returns the upper 8 bits of the abstract (the mask bits) of the
abstract value. This mask represents those bits that are known.
av1
- the abstract value
public static char getBit(char av1, int bit)
getBit()
method extracts the specified abstract bit from the specified abstract
value.
av1
- the abstract valuebit
- the bit number
AbstractArithmetic.TRUE
if the bit is known to be on;
AbstractArithmetic.FALSE
if the bit is known to be off;
AbstractArithmetic.UNKNOWN
otherwisepublic static char setBit(char av1, int bit, char on)
setBit()
method updates the specified abstract bit within the specified abstract
value.
av1
- the abstract valuebit
- the bit numberon
- the new abstract value of the bit
public static char couldBeZero(char av1)
couldBeZero
method performs a "fuzzy" equality test against zero for an abstract
value. It will return one of three values, depending on whether the specified abstract value is
definately zero, definately not zero, or unknown.
av1
- the abstract value
AbstractArithmetic.TRUE
if the specified abstract value is definately zero;
AbstractArithmetic.FALSE
if the specified abstract value cannot possibly be zero
(it has one bit that is known to be on); AbstractArithmetic.UNKNOWN
otherwisepublic static char couldBeZero(char av1, char av2)
couldBeZero()
method performs a "fuzzy" equality test against zero for two abstract
values. It will return one of three values, depending on whether the specified abstract values are
definately zero, definately not zero, or unknown.
av1
- the first abstract valueav2
- the second abstract value
AbstractArithmetic.TRUE
if both abstract values are definately zero;
AbstractArithmetic.FALSE
if either of the specified abstract values cannot
possibly be zero (it has one bit that is known to be on); AbstractArithmetic.UNKNOWN
otherwisepublic static char couldBeEqual(char av1, char av2)
couldBeEqual()
method performs a "fuzzy" equality test between two abstract values. It
will return one of three values, depending on whether the abstract values are definately equal,
definately not equal, or unknown.
av1
- the first abstract valueav2
- the second abstract value
AbstractArithmetic.TRUE
if the abstract values are definately equal;
AbstractArithmetic.FALSE
if the abstract values are definately not equal;
AbstractArithmetic.UNKNOWN
otherwisepublic static char commonMask(char av1, char av2)
commonMask()
method computes the intersection of the known bit masks of two abstract
values.
av1
- the first abstract valueav2
- the second abstract value
public static char commonMask(char av1, char av2, char av3)
commonMask()
method computes the intersection of the known bit masks of three abstract
values.
av1
- the first abstract valueav2
- the second abstract valueav3
- the third abstract value
public static char logicalAnd(char av1, char av2)
logicalAnd
method computes the logical bitwise AND of two abstract values.
av1
- the first abstract valueav2
- the second abstract value
public static char add(char av1, char av2)
add()
method performs addition of two abstract values. It relies on the
ceiling()
and floor()
functions that allow abstract addition to be expressed
in terms of two concrete additions, resulting in a straightforward and clean implementation.
av1
- the first abstract valueav2
- the second abstract value
public static char subtract(char av1, char av2)
add()
method performs subtraction of two abstract values. It relies on the
ceiling()
and floor()
functions that allow abstract subtraction to be
expressed in terms of two concrete subtractions, resulting in a straightforward and clean
implementation.
av1
- the first abstract valueav2
- the second abstract value
public static char increment(char av1)
increment()
method simply adds 1 to the abstract value. It is a special case of the
add()
that is common enough to warrant its own method.
av1
- the abstract value
public static char decrement(char av1)
decrement()
method simply subtracts 1 to the abstract value. It is a special case of
the subtract()
that is common enough to warrant its own method.
av1
- the abstract value
public static char mergeMask(char mask, char av1)
mergeMask()
merges the given abstract value with the known bit mask passed. This means
that the known bits will be the intersection of the known bits of the mask and the known bits of the
abstract value.
mask
- the known bit maskav1
- the abstract value
public static char xor(char av1, char av2)
xor()
method computes the bitwise exclusive or operation on the two given abstract
values.
av1
- the first abstract valueav2
- the second abstract value
public static char and(char av1, char av2)
and()
method computes the logical bitwise AND of two abstract values.
av1
- the first abstract valueav2
- the second abstract value
public static char or(char av1, char av2)
or()
method computes the logical bitwise or of two abstract values.
av1
- the first abstract valueav2
- the second abstract value
public static char and(char av1, char av2, char av3)
and()
method computes the logical bitwise AND of three abstract values.
av1
- the first abstract valueav2
- the second abstract valueav3
- the third abstract value
public static char or(char av1, char av2, char av3)
or()
method computes the logical bitwise or of three abstract values.
av1
- the first abstract valueav2
- the second abstract valueav3
- the third abstract value
public static char not(char av1)
not()
method computes the bitwise negation (one's complement) of the specified
abstract value
av1
- the abstract value
public static int ceiling(char av1)
ceiling()
function computes the concrete value with all unknown bits set to one. This
is useful for implementation of some arithmetic operations.
av1
- the abstract value to compute the ceiling of
public static int ceiling(char av1, char av2)
ceiling()
function computes the concrete value with all unknown bits set to one. This
is useful for implementation of some arithmetic operations. This variant takes two abstract values
representing the lower and upper bytes of a word and returns a concrete unsigned 16-bit word
representing the ceiling function.
av1
- the abstract value representing the lower byteav2
- the abstract value representing the high byte
public static int floor(char av1)
floor()
function computes the concrete value with all unknown bits set to zero. This
is useful for implementation of some arithmetic operations.
av1
- the abstract value to compute the ceiling of
public static int floor(char av1, char av2)
floor()
function computes the concrete value with all unknown bits set to zero. This
is useful for implementation of some arithmetic operations. This variant takes two abstract values
representing the lower and upper bytes of a word and returns a concrete unsigned 16-bit word
representing the floor function.
av1
- the abstract value representing the lower byteav2
- the abstract value representing the high byte
public static char shiftLeftOne(char av1)
shiftLeftOne()
method shifts the abstract value left by one bit.
av1
- the abstract value
public static char shiftLeftOne(char av1, char lowbit)
shiftLeftOne()
method shifts the abstract value left by one bit and sets the lowest
bit to the given value.
av1
- the abstract valuelowbit
- the value of the lowest bit
public static java.lang.String toString(char av1)
toString()
method converts an 8-bit abstract value to a string representation. Each
bit's value is represented as either '0', '1', or '.' and listed with the most significant first.
av1
- the abstract value to convert to a string
public static java.lang.String toShortString(char av1)
toShortString()
method converts an 8-bit abstract value to a string representation.
Each bit's value is represented as either '0', '1', or '.' and listed with the most significant first.
av1
- the abstract value to convert to a string
public static char bitToChar(char av1)
toString()
method converts an 1-bit abstract value to a string representation. The
bit's value is represented as either '0', '1', or '.'.
av1
- the abstract bit to convert to a string
public static void toString(char av1, java.lang.StringBuffer buf)
toString()
method converts an 8-bit abstract value to a string representation and
appends it to the end of the given string buffer. Each bit's value is represented as either '0', '1',
or '.' and listed with the most significant first.
av1
- the abstract value to convert to a stringbuf
- the string buffer to append the result to
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |