Class Frame<V extends Value>

  • Type Parameters:
    V - type of the Value used for the analysis.

    public class Frame<V extends Value>
    extends Object
    A symbolic execution stack frame. A stack frame contains a set of local variable slots, and an operand stack. Warning: long and double values are represented by two slots in local variables, and by one slot in the operand stack.
    Author:
    Eric Bruneton
    • Constructor Summary

      Constructors 
      Constructor Description
      Frame​(int nLocals, int nStack)
      Constructs a new frame with the given size.
      Frame​(Frame<? extends V> src)
      Constructs a new frame that is identical to the given frame.
    • Constructor Detail

      • Frame

        public Frame​(int nLocals,
                     int nStack)
        Constructs a new frame with the given size.
        Parameters:
        nLocals - the maximum number of local variables of the frame.
        nStack - the maximum stack size of the frame.
      • Frame

        public Frame​(Frame<? extends V> src)
        Constructs a new frame that is identical to the given frame.
        Parameters:
        src - a frame.
    • Method Detail

      • init

        public Frame<V> init​(Frame<? extends V> src)
        Copies the state of the given frame into this frame.
        Parameters:
        src - a frame.
        Returns:
        this frame.
      • setReturn

        public void setReturn​(V v)
        Sets the expected return type of the analyzed method.
        Parameters:
        v - the expected return type of the analyzed method, or null if the method returns void.
      • getLocals

        public int getLocals()
        Returns the maximum number of local variables of this frame.
        Returns:
        the maximum number of local variables of this frame.
      • getMaxStackSize

        public int getMaxStackSize()
        Returns the maximum stack size of this frame.
        Returns:
        the maximum stack size of this frame.
      • getLocal

        public V getLocal​(int i)
                   throws IndexOutOfBoundsException
        Returns the value of the given local variable.
        Parameters:
        i - a local variable index.
        Returns:
        the value of the given local variable.
        Throws:
        IndexOutOfBoundsException - if the variable does not exist.
      • setLocal

        public void setLocal​(int i,
                             V value)
                      throws IndexOutOfBoundsException
        Sets the value of the given local variable.
        Parameters:
        i - a local variable index.
        value - the new value of this local variable.
        Throws:
        IndexOutOfBoundsException - if the variable does not exist.
      • getStackSize

        public int getStackSize()
        Returns the number of values in the operand stack of this frame. Long and double values are treated as single values.
        Returns:
        the number of values in the operand stack of this frame.
      • getStack

        public V getStack​(int i)
                   throws IndexOutOfBoundsException
        Returns the value of the given operand stack slot.
        Parameters:
        i - the index of an operand stack slot.
        Returns:
        the value of the given operand stack slot.
        Throws:
        IndexOutOfBoundsException - if the operand stack slot does not exist.
      • clearStack

        public void clearStack()
        Clears the operand stack of this frame.
      • push

        public void push​(V value)
                  throws IndexOutOfBoundsException
        Pushes a value into the operand stack of this frame.
        Parameters:
        value - the value that must be pushed into the stack.
        Throws:
        IndexOutOfBoundsException - if the operand stack is full.
      • merge

        public boolean merge​(Frame<? extends V> frame,
                             Interpreter<V> interpreter)
                      throws AnalyzerException
        Merges this frame with the given frame.
        Parameters:
        frame - a frame.
        interpreter - the interpreter used to merge values.
        Returns:
        true if this frame has been changed as a result of the merge operation, or false otherwise.
        Throws:
        AnalyzerException - if the frames have incompatible sizes.
      • merge

        public boolean merge​(Frame<? extends V> frame,
                             boolean[] access)
        Merges this frame with the given frame (case of a RET instruction).
        Parameters:
        frame - a frame
        access - the local variables that have been accessed by the subroutine to which the RET instruction corresponds.
        Returns:
        true if this frame has been changed as a result of the merge operation, or false otherwise.
      • toString

        public String toString()
        Returns a string representation of this frame.
        Overrides:
        toString in class Object
        Returns:
        a string representation of this frame.