Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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` | `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

### 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

### toShortString

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

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

  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

Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD