avrora.stack
Class AbstractArithmetic

java.lang.Object
  avrora.stack.AbstractArithmetic

Direct Known Subclasses:

AbstractInterpreter

public class AbstractArithmetic

extends java.lang.Object

The AbstractArithmetic arithmetic class implements operations that are useful for working on abstract integers which are represented as characters.

The abstract values (e.g. register values) are represented as characters. Thus, an 8 bit register is modelled using a 16-bit character. The upper 8 bits represent the "mask", those bits which are known. The lower 8 bits represent the known bits of the value. Thus, if bit(regs[R], i+8) is set, then bit(R, i) is known and its value is bit(regs[R], i). If bit(regs[R], i+8) is clear, then the value of bit(regs[R], i) is unknown in this abstract value.

Since there are 3 possible values (on, off, unknown) for each bit in the abstract state and there are two bits reserved for representing each of these states, there are 4 bit states to represent 3 values. We canonicalize the values when the bit value is unknown, i.e. when the known mask bit is clear, then the value bit is clear as well. This makes comparison of canonical abstract values the same as character equality. All abstract values stored within 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	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

ZERO

public static final char ZERO

The ZERO field represents the abstract value where all bits are known to be zero.

See Also:

Constant Field Values

TRUE

public static final char TRUE

The TRUE field represents the abstract bit that is known to be true.

See Also:

Constant Field Values

FALSE

public static final char FALSE

The FALSE field represents the abstract bit that is known to be false.

See Also:

Constant Field Values

UNKNOWN

public static final char UNKNOWN

The UNKNOWN field represents the abstract value where none of the bits are known.

See Also:

Constant Field Values

Constructor Detail

AbstractArithmetic

public AbstractArithmetic()

Method Detail

merge

public static char merge(byte cv1,
                         byte cv2)

The 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.

Parameters:

cv1 - the first (concrete) value to merge

cv2 - the second (concrete) value to merge

Returns:

the abstract value representing the results of merging the two values

merge

public static char merge(char av1,
                         byte cv2)

The 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.

Parameters:

av1 - the first (abstract) value to merge

cv2 - the second (concrete) value to merge

Returns:

the abstract value representing the results of merging the two values

merge

public static char merge(byte cv1,
                         byte cv2,
                         byte cv3)

The 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.

Parameters:

cv1 - the first (concrete) value to merge

cv2 - the second (concrete) value to merge

cv3 - the third (concrete) value to merge

Returns:

the abstract value representing the results of merging the two values

merge

public static char merge(byte cv1,
                         byte cv2,
                         byte cv3,
                         byte cv4)

The 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.

Parameters:

cv1 - the first (concrete) value to merge

cv2 - the second (concrete) value to merge

cv3 - the third (concrete) value to merge

cv4 - the fourth (concrete) value to merge

Returns:

the abstract value representing the results of merging the two values

merge

public static char merge(char av1,
                         char av2)

The 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.

Parameters:

av1 - the first (abstract) value to merge

av2 - the second (abstract) value to merge

Returns:

the abstract value representing the results of merging the two values

isUnknown

public static boolean isUnknown(char av1)

The isKnown() method tests whether an abstract value represents a single, fully known value.

Parameters:

av1 - the abstract value to test

Returns:

true if all of the bits of the abstract value are known; false if any bits are unknown

areKnown

public static boolean areKnown(char av1,
                               char av2)

The areKnown() method tests whether two abstract values each represent a single, fully known value.

Parameters:

av1 - the first abstract value to test

av2 - the second abstract value to test

Returns:

true if all of the bits of the both abstract values are known; false if any bits are unknown

areEqual

public static boolean areEqual(char val1,
                               char val2)

The 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

Parameters:

val1 - the first abstract value

val2 - the second abstract value

Returns:

true if the abstract values are equal; false otherwise

canon

public static char canon(char av1)

The 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.

Parameters:

av1 - the abstract value to canonicalize

Returns:

the canonicalized representation of this abstract value

canon

public static char canon(char mask,
                         char av1)

The 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.

Parameters:

mask - the known bit mask to canonicalize with respect to

av1 - the abstract value to canonicalize

Returns:

the canonicalized representation of this abstract value

knownVal

public static char knownVal(byte cv1)

The knownVal() method creates a canonical abstract value from the given concrete value.

Parameters:

cv1 - the concrete value to create an abstract value for

Returns:

a canonical abstract value representing the concrete value.

knownBitsOf

public 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.

Parameters:

val - the abstract value to get the known bits of

Returns:

a concrete value such that all unknown bits are set to zero

bitsOf

public 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. 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.

Parameters:

av1 - the abstract value

Returns:

the lower bits of the abstract value as a concrete value

maskOf

public static char maskOf(char av1)

The 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.

Parameters:

av1 - the abstract value

Returns:

the mask of known bits of the abstract value

getBit

public static char getBit(char av1,
                          int bit)

The getBit() method extracts the specified abstract bit from the specified abstract value.

Parameters:

av1 - the abstract value

bit - the bit number

Returns:

AbstractArithmetic.TRUE if the bit is known to be on; AbstractArithmetic.FALSE if the bit is known to be off; AbstractArithmetic.UNKNOWN otherwise

setBit

public static char setBit(char av1,
                          int bit,
                          char on)

The setBit() method updates the specified abstract bit within the specified abstract value.

Parameters:

av1 - the abstract value

bit - the bit number

on - the new abstract value of the bit

Returns:

a new abstract value where the specified bit has been replaced with the specified abstract value

couldBeZero

public static char couldBeZero(char av1)

The 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.

Parameters:

av1 - the abstract value

Returns:

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 otherwise

couldBeZero

public static char couldBeZero(char av1,
                               char av2)

The 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.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

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 otherwise

couldBeEqual

public static char couldBeEqual(char av1,
                                char av2)

The 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.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

AbstractArithmetic.TRUE if the abstract values are definately equal; AbstractArithmetic.FALSE if the abstract values are definately not equal; AbstractArithmetic.UNKNOWN otherwise

commonMask

public static char commonMask(char av1,
                              char av2)

The commonMask() method computes the intersection of the known bit masks of two abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

the intersection of the known bit masks of each abstract value

commonMask

public static char commonMask(char av1,
                              char av2,
                              char av3)

The commonMask() method computes the intersection of the known bit masks of three abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

av3 - the third abstract value

Returns:

the intersection of the known bit masks of each abstract value

logicalAnd

public static char logicalAnd(char av1,
                              char av2)

The logicalAnd method computes the logical bitwise AND of two abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

an abstract value representing the bitwise AND of the two abstract value operands

add

public static char add(char av1,
                       char av2)

The 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.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

an abstract value that represents the sum of the two abstract values.

subtract

public static char subtract(char av1,
                            char av2)

The 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.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

an abstract value that represents the difference of the two abstract values.

increment

public static char increment(char av1)

The 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.

Parameters:

av1 - the abstract value

Returns:

an abstract value that represents the sum of the specified abstract value and the known value 1

decrement

public static char decrement(char av1)

The 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.

Parameters:

av1 - the abstract value

Returns:

an abstract value that represents the difference of the specified abstract value and the known value 1

mergeMask

public static char mergeMask(char mask,
                             char av1)

The 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.

Parameters:

mask - the known bit mask

av1 - the abstract value

Returns:

an abstract value in which the known bit mask is the intersection of the given bit mask and the bit mask of the given abstract value

xor

public static char xor(char av1,
                       char av2)

The xor() method computes the bitwise exclusive or operation on the two given abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

the bitwise exclusive or of the two abstract values

and

public static char and(char av1,
                       char av2)

The and() method computes the logical bitwise AND of two abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

an abstract value representing the bitwise AND of the two abstract value operands

or

public static char or(char av1,
                      char av2)

The or() method computes the logical bitwise or of two abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

Returns:

an abstract value representing the bitwise inclusive or of the two abstract value operands

and

public static char and(char av1,
                       char av2,
                       char av3)

The and() method computes the logical bitwise AND of three abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

av3 - the third abstract value

Returns:

an abstract value representing the bitwise AND of the three abstract value operands

or

public static char or(char av1,
                      char av2,
                      char av3)

The or() method computes the logical bitwise or of three abstract values.

Parameters:

av1 - the first abstract value

av2 - the second abstract value

av3 - the third abstract value

Returns:

an abstract value representing the bitwise inclusive or of the two abstract value operands

not

public static char not(char av1)

The not() method computes the bitwise negation (one's complement) of the specified abstract value

Parameters:

av1 - the abstract value

Returns:

the abstract value representing the bitwise negation of the operand

ceiling

public static int ceiling(char av1)

The ceiling() function computes the concrete value with all unknown bits set to one. This is useful for implementation of some arithmetic operations.

Parameters:

av1 - the abstract value to compute the ceiling of

Returns:

a concrete value where each of the unknown bits of the abstract value are set to one

ceiling

public static int ceiling(char av1,
                          char av2)

The 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.

Parameters:

av1 - the abstract value representing the lower byte

av2 - the abstract value representing the high byte

Returns:

a concrete word value where each of the unknown bits of the abstract value are set to one

floor

public static int floor(char av1)

The floor() function computes the concrete value with all unknown bits set to zero. This is useful for implementation of some arithmetic operations.

Parameters:

av1 - the abstract value to compute the ceiling of

Returns:

a concrete value where each of the unknown bits of the abstract value are set to zero

floor

public static int floor(char av1,
                        char av2)

The 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.

Parameters:

av1 - the abstract value representing the lower byte

av2 - the abstract value representing the high byte

Returns:

a concrete word value where each of the unknown bits of the abstract value are set to zero

shiftLeftOne

public static char shiftLeftOne(char av1)

The shiftLeftOne() method shifts the abstract value left by one bit.

Parameters:

av1 - the abstract value

Returns:

an abstract value representing the operand shifted left by one and the lower bit is set to known zero

shiftLeftOne

public 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.

Parameters:

av1 - the abstract value

lowbit - the value of the lowest bit

Returns:

an abstract value representing the operand shifted left by one and the lower bit is set to the given value

toString

public static java.lang.String toString(char av1)

The 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.

Parameters:

av1 - the abstract value to convert to a string

Returns:

a string representation of the abstract value

bitToChar

public static char bitToChar(char av1)

The toString() method converts an 1-bit abstract value to a string representation. The bit's value is represented as either '0', '1', or '.'.

Parameters:

av1 - the abstract bit to convert to a string

Returns:

a character representation of the abstract bit

toString

public 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. Each bit's value is represented as either '0', '1', or '.' and listed with the most significant first.

Parameters:

av1 - the abstract value to convert to a string

buf - the string buffer to append the result to