Package de.uzl.its.swat.symbolic

Class SymbolicInstructionVisitor

java.lang.Object
de.uzl.its.swat.symbolic.SymbolicInstructionVisitor
All Implemented Interfaces:
IVisitor
public class SymbolicInstructionVisitor extends Object implements IVisitor

  • Constructor Details

    • SymbolicInstructionVisitor

      public SymbolicInstructionVisitor(ClassNames classNames)

  • Method Details

    • checkArrayBounds

      public boolean checkArrayBounds(Value<?,?> ref, IntValue idx, int iid)

    • visitAALOAD

      public void visitAALOAD(AALOAD inst)
      Loads a reference from an array and stores the reference on the symbolic stack ToDo (Nils): Reference arrays are not symbolically tracked currently See: ...
      Specified by:
      visitAALOAD in interface IVisitor
      Parameters:
      inst - The AALOAD instruction

    • visitAASTORE

      public void visitAASTORE(AASTORE inst)
      Stores a reference value into an array
      Specified by:
      visitAASTORE in interface IVisitor
      Parameters:
      inst - The ASTORE instruction

    • visitACONST_NULL

      public void visitACONST_NULL(ACONST_NULL inst)
      Pushes NULL onto the symbolic stack
      Specified by:
      visitACONST_NULL in interface IVisitor
      Parameters:
      inst - The ACONST_NULL instruction

    • visitALOAD

      public void visitALOAD(ALOAD inst)
      Fetches a reference from the symbolic locals and puts it onto the symbolic stack
      Specified by:
      visitALOAD in interface IVisitor
      Parameters:
      inst - One on the ALOAD (ALOAD, ALOAD_0 - ALOAD_3) instructions

    • visitANEWARRAY

      public void visitANEWARRAY(ANEWARRAY inst)
      Creates a new array of references and puts the array onto the symbolic stack.
      Specified by:
      visitANEWARRAY in interface IVisitor
      Parameters:
      inst - The ANEWARRAY instruction.

    • visitARETURN

      public void visitARETURN(ARETURN inst)
      Takes the top value (has to be a reference) from the symbolic stack and sets it as the symbolic return value
      Specified by:
      visitARETURN in interface IVisitor
      Parameters:
      inst - The ARETURN instruction

    • visitARRAYLENGTH

      public void visitARRAYLENGTH(ARRAYLENGTH inst)
      Determines the size of an array and puts it onto the symbolic stack INFO: While the length is tracked symbolically it is currently unclear to what effect that is useful See: Issue
      Specified by:
      visitARRAYLENGTH in interface IVisitor
      Parameters:
      inst - The ARRAYLENGTH instruction

    • visitASTORE

      public void visitASTORE(ASTORE inst)
      Stores the top reference from the symbolic stack into the symbolic locals. The index of the locals position is indicated by the instruction and not taken from the stack
      Specified by:
      visitASTORE in interface IVisitor
      Parameters:
      inst - One of the ASTORE (ASTORE, ASTORE_0 - ASTORE_3) instructions. inst.var is the locals index

    • visitATHROW

      public void visitATHROW(ATHROW inst)
      Throws an error or exception in the symbolic frame. The symbolic stack is cleared and only a reference to the exception remains on the symbolic stack. ToDo (Nils): Could some information be saved here to record that an exception has occurred? See: ...
      Specified by:
      visitATHROW in interface IVisitor
      Parameters:
      inst - The ATHROW instruction

    • visitBALOAD

      public void visitBALOAD(BALOAD inst)
      Retrieves a boolean or byte from an array and puts it onto the symbolic stack
      Specified by:
      visitBALOAD in interface IVisitor
      Parameters:
      inst - The BALOAD instruction.

    • visitBASTORE

      public void visitBASTORE(BASTORE inst)
      Stores a boolean or byte into an array
      Specified by:
      visitBASTORE in interface IVisitor
      Parameters:
      inst - The BASTORE instruction.

    • visitBIPUSH

      public void visitBIPUSH(BIPUSH inst)
      Pushes a byte onto the symbolic stack as an integer
      Specified by:
      visitBIPUSH in interface IVisitor
      Parameters:
      inst - The BIPUSH instruction

    • visitCALOAD

      public void visitCALOAD(CALOAD inst)
      Retrieves a char from an array and puts it onto the symbolic stack
      Specified by:
      visitCALOAD in interface IVisitor
      Parameters:
      inst - The CALOAD instruction.

    • visitCASTORE

      public void visitCASTORE(CASTORE inst)
      Stores a char into an array
      Specified by:
      visitCASTORE in interface IVisitor
      Parameters:
      inst - The CASTORE instruction.

    • visitCHECKCAST

      public void visitCHECKCAST(CHECKCAST inst)
      No symbolic tracking needed here. Exceptions in case the object cannot be cast need to be caught.
      Specified by:
      visitCHECKCAST in interface IVisitor
      Parameters:
      inst - The CHECKCAST instruction

    • visitD2F

      public void visitD2F(D2F inst)
      Casts a double value to a float and puts the result onto the symbolic stack
      Specified by:
      visitD2F in interface IVisitor
      Parameters:
      inst - The D2F instruction

    • visitD2I

      public void visitD2I(D2I inst)
      Casts a double to an integer and puts the int onto the symbolic stack
      Specified by:
      visitD2I in interface IVisitor
      Parameters:
      inst - The D2I instruction

    • visitD2L

      public void visitD2L(D2L inst)
      Casts a double to a long and puts the long onto the symbolic stack
      Specified by:
      visitD2L in interface IVisitor
      Parameters:
      inst - The D2L instruction

    • visitDADD

      public void visitDADD(DADD inst)
      Adds two doubles and pushes the result onto the symbolic stack
      Specified by:
      visitDADD in interface IVisitor
      Parameters:
      inst - The DADD instruction

    • visitDALOAD

      public void visitDALOAD(DALOAD inst)
      Retrieves a double from an array and puts it onto the symbolic stack
      Specified by:
      visitDALOAD in interface IVisitor
      Parameters:
      inst - The DALOAD instruction.

    • visitDASTORE

      public void visitDASTORE(DASTORE inst)
      Stores a double into an array
      Specified by:
      visitDASTORE in interface IVisitor
      Parameters:
      inst - The DASTORE instruction.

    • visitDCMPG

      public void visitDCMPG(DCMPG inst)
      Compares two doubles and encodes the result as an integer that is put onto the symbolic stack
      Specified by:
      visitDCMPG in interface IVisitor
      Parameters:
      inst - The DCMPG instruction

    • visitDCMPL

      public void visitDCMPL(DCMPL inst)
      Compares two doubles and encodes the result as an integer that is put onto the symbolic stack
      Specified by:
      visitDCMPL in interface IVisitor
      Parameters:
      inst - The DCMPL instruction

    • visitDCONST_0

      public void visitDCONST_0(DCONST_0 inst)
      Loads the constant 0.0 onto the symbolic stack
      Specified by:
      visitDCONST_0 in interface IVisitor
      Parameters:
      inst - The DCONST_0 instruction

    • visitDCONST_1

      public void visitDCONST_1(DCONST_1 inst)
      Loads the constant 1.0 onto the symbolic stack
      Specified by:
      visitDCONST_1 in interface IVisitor
      Parameters:
      inst - The DCONST_1 instruction

    • visitDDIV

      public void visitDDIV(DDIV inst)
      Divides two doubles and pushes the result onto the symbolic stack
      Specified by:
      visitDDIV in interface IVisitor
      Parameters:
      inst - The DDIV instruction

    • visitDLOAD

      public void visitDLOAD(DLOAD inst)
      Loads a double from the symbolic locals onto the symbolic stack.
      Specified by:
      visitDLOAD in interface IVisitor
      Parameters:
      inst - One of the DLOAD instructions (DLOAD, DLOAD_0 - DLOAD_3)

    • visitDMUL

      public void visitDMUL(DMUL inst)
      Multiplies two doubles and pushes the result onto the symbolic stack
      Specified by:
      visitDMUL in interface IVisitor
      Parameters:
      inst - The DMUL instruction

    • visitDNEG

      public void visitDNEG(DNEG inst)
      Negates a double and pushes the result onto the symbolic stack
      Specified by:
      visitDNEG in interface IVisitor
      Parameters:
      inst - The DNEG instruction

    • visitDREM

      public void visitDREM(DREM inst)
      Specified by:
      visitDREM in interface IVisitor

    • visitDRETURN

      public void visitDRETURN(DRETURN inst)
      Sets the return value of the current symbolic frame to the double value on top of the symbolic stack
      Specified by:
      visitDRETURN in interface IVisitor
      Parameters:
      inst - The DRETURN instruction

    • visitDSTORE

      public void visitDSTORE(DSTORE inst)
      Stores the top value from the symbolic stack (double) into a slot in the symbolic locals
      Specified by:
      visitDSTORE in interface IVisitor
      Parameters:
      inst - One of the DSTORE instructions (DSTORE, DSTORE_0 - DSTORE_3)

    • visitDSUB

      public void visitDSUB(DSUB inst)
      Subtracts two doubles and pushes the result onto the symbolic stack
      Specified by:
      visitDSUB in interface IVisitor
      Parameters:
      inst - The DSUB instruction

    • visitDUP

      public void visitDUP(DUP inst)
      Duplicates the top value on the symbolic stack (only one word -> 8 bytes) | 1 | --> | 1 | | 1 |
      Specified by:
      visitDUP in interface IVisitor
      Parameters:
      inst - The DUP instruction

    • visitDUP2

      public void visitDUP2(DUP2 inst)
      Duplicates the top value on the symbolic stack (two words -> 16 bytes) | 1 | | 1 | | 2 | --> | 2 | | 1 | | 2 |
      Specified by:
      visitDUP2 in interface IVisitor
      Parameters:
      inst - The DUP2 instruction

    • visitDUP2_X1

      public void visitDUP2_X1(DUP2_X1 inst)
      Duplicate two words and insert them beneath a third word | 1 | | 1 | | 2 | --> | 2 | | 3 | | 3 | | 1 | | 2 |
      Specified by:
      visitDUP2_X1 in interface IVisitor
      Parameters:
      inst - The DUP2_X1 instruction

    • visitDUP2_X2

      public void visitDUP2_X2(DUP2_X2 inst)
      Duplicate two words and insert them beneath a fourth word | 1 | | 1 | | 2 | --> | 2 | | 3 | | 3 | | 4 | | 4 | | 1 | | 2 |
      Specified by:
      visitDUP2_X2 in interface IVisitor
      Parameters:
      inst - The DUP2_X2 instruction

    • visitDUP_X1

      public void visitDUP_X1(DUP_X1 inst)
      Duplicate the top word and insert it beneath a second word | 1 | | 1 | | 2 | --> | 2 | | 1 |
      Specified by:
      visitDUP_X1 in interface IVisitor
      Parameters:
      inst - The DUP2_X1 instruction

    • visitDUP_X2

      public void visitDUP_X2(DUP_X2 inst)
      Duplicate the top word and insert it beneath the third word | 1 | | 1 | | 2 | --> | 2 | | 3 | | 3 | | 1 |
      Specified by:
      visitDUP_X2 in interface IVisitor
      Parameters:
      inst - The DUP2_X1 instruction

    • visitF2D

      public void visitF2D(F2D inst)
      Casts a float to a double and puts the result onto the symbolic stack
      Specified by:
      visitF2D in interface IVisitor
      Parameters:
      inst - The F2D instruction

    • visitF2I

      public void visitF2I(F2I inst)
      Casts a float to an integer and puts the result onto the symbolic stack
      Specified by:
      visitF2I in interface IVisitor
      Parameters:
      inst - The F2I instruction

    • visitF2L

      public void visitF2L(F2L inst)
      Specified by:
      visitF2L in interface IVisitor

    • visitFADD

      public void visitFADD(FADD inst)
      Adds two floats and adds the result onto the symbolic stack
      Specified by:
      visitFADD in interface IVisitor
      Parameters:
      inst - The FADD instruction

    • visitFALOAD

      public void visitFALOAD(FALOAD inst)
      Loads a float from an array and puts it onto the symbolic stack
      Specified by:
      visitFALOAD in interface IVisitor
      Parameters:
      inst - The FALOAD instruction

    • visitFASTORE

      public void visitFASTORE(FASTORE inst)
      Stores a float into an array
      Specified by:
      visitFASTORE in interface IVisitor
      Parameters:
      inst - The FASTORE instruction

    • visitFCMPG

      public void visitFCMPG(FCMPG inst)
      Compares two floats and encodes the result as an integer that is put onto the symbolic stack
      Specified by:
      visitFCMPG in interface IVisitor
      Parameters:
      inst - The FCMPG instruction

    • visitFCMPL

      public void visitFCMPL(FCMPL inst)
      Compares two floats and encodes the result as an integer that is put onto the symbolic stack
      Specified by:
      visitFCMPL in interface IVisitor
      Parameters:
      inst - The FCMPL instruction

    • visitFCONST_0

      public void visitFCONST_0(FCONST_0 inst)
      Loads the constant 0.0f as a float onto the symbolic stack
      Specified by:
      visitFCONST_0 in interface IVisitor
      Parameters:
      inst - The FCONST_0 instruction

    • visitFCONST_1

      public void visitFCONST_1(FCONST_1 inst)
      Loads the constant 1.0f as a float onto the symbolic stack
      Specified by:
      visitFCONST_1 in interface IVisitor
      Parameters:
      inst - The FCONST_1 instruction

    • visitFCONST_2

      public void visitFCONST_2(FCONST_2 inst)
      Loads the constant 2.0f as a float onto the symbolic stack
      Specified by:
      visitFCONST_2 in interface IVisitor
      Parameters:
      inst - The FCONST_2 instruction

    • visitFDIV

      public void visitFDIV(FDIV inst)
      Divides two floats and puts the result onto the symbolic stack
      Specified by:
      visitFDIV in interface IVisitor
      Parameters:
      inst - The FDIV instruction

    • visitFLOAD

      public void visitFLOAD(FLOAD inst)
      Loads a float from the symbolic locals onto the symbolic stack
      Specified by:
      visitFLOAD in interface IVisitor
      Parameters:
      inst - One of the FLOAD instructions (FLOAD, FLOAD_0 - FLOAD_3)

    • visitFMUL

      public void visitFMUL(FMUL inst)
      Multiplies two floats and puts the result onto the symbolic stack
      Specified by:
      visitFMUL in interface IVisitor
      Parameters:
      inst - The FMUL instruction

    • visitFNEG

      public void visitFNEG(FNEG inst)
      Negates a float and puts the result onto the symbolic stack
      Specified by:
      visitFNEG in interface IVisitor
      Parameters:
      inst - The FNEG instruction

    • visitFREM

      public void visitFREM(FREM inst)
      Calculates the remaider of the divion of two flaots and puts the result onto the symbolic stack WARNING: This is currently only the concrete value
      Specified by:
      visitFREM in interface IVisitor
      Parameters:
      inst - The FREM instruction

    • visitFRETURN

      public void visitFRETURN(FRETURN inst)
      Sets the return value of the current symbolic frame to the float value on top of the symbolic stack
      Specified by:
      visitFRETURN in interface IVisitor
      Parameters:
      inst - The FRETURN instruction

    • visitFSTORE

      public void visitFSTORE(FSTORE inst)
      Puts the float on top of the symbolic stack into one of the symbolic locals of the current frame
      Specified by:
      visitFSTORE in interface IVisitor
      Parameters:
      inst - One of the FSTORE instructions (FSTORE, FSTORE_0 - FSTORE_3)

    • visitFSUB

      public void visitFSUB(FSUB inst)
      Subtracts two floats and puts the resulting FloatValuer onto the symbolic stack.
      Specified by:
      visitFSUB in interface IVisitor
      Parameters:
      inst - The FSUB instruction.

    • visitGETFIELD

      public void visitGETFIELD(GETFIELD inst)
      Fetches a field from an object instance and puts it onto the symbolic stack
      Specified by:
      visitGETFIELD in interface IVisitor
      Parameters:
      inst - The GETFIELD instruction

    • visitGETSTATIC

      public void visitGETSTATIC(GETSTATIC inst)
      Fetches a static field from an object and puts it onto the symbolic stack
      Specified by:
      visitGETSTATIC in interface IVisitor
      Parameters:
      inst - The GETSTATIC instruction

    • visitGETVALUE_Object

      public void visitGETVALUE_Object(GETVALUE_Object<?> inst)
      Specified by:
      visitGETVALUE_Object in interface IVisitor

    • visitGETVALUE_boolean

      public void visitGETVALUE_boolean(GETVALUE_boolean inst)
      Artificial instruction used to fetch concrete boolean values
      Specified by:
      visitGETVALUE_boolean in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_boolean instruction

    • visitGETVALUE_byte

      public void visitGETVALUE_byte(GETVALUE_byte inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_byte in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_byte instruction

    • visitGETVALUE_char

      public void visitGETVALUE_char(GETVALUE_char inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_char in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_char instruction

    • visitGETVALUE_double

      public void visitGETVALUE_double(GETVALUE_double inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_double in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_double instruction

    • visitGETVALUE_float

      public void visitGETVALUE_float(GETVALUE_float inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_float in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_float instruction

    • visitGETVALUE_int

      public void visitGETVALUE_int(GETVALUE_int inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_int in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_int instruction

    • visitGETVALUE_long

      public void visitGETVALUE_long(GETVALUE_long inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_long in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_long instruction

    • visitGETVALUE_short

      public void visitGETVALUE_short(GETVALUE_short inst)
      Artificial instruction used to fetch concrete values
      Specified by:
      visitGETVALUE_short in interface IVisitor
      Parameters:
      inst - The (artificial) GETVALUE_short instruction

    • visitGETVALUE_void

      public void visitGETVALUE_void(GETVALUE_void inst)
      Specified by:
      visitGETVALUE_void in interface IVisitor

    • visitGOTO

      public void visitGOTO(GOTO inst)
      No symbolic tracking needed for the uncoditional jump.
      Specified by:
      visitGOTO in interface IVisitor
      Parameters:
      inst - Either the GOTO or GOTO_w instruction

    • visitI2B

      public void visitI2B(I2B inst)
      Converts an integer to a byte and puts the result onto the symbolic stack
      Specified by:
      visitI2B in interface IVisitor
      Parameters:
      inst - The I2B instruction

    • visitI2C

      public void visitI2C(I2C inst)
      Converts an integer to a char and puts the result onto the symbolic stack ToDo (Nils): Symbolic information regarding the integer is currently lost here! See: Issue 60
      Specified by:
      visitI2C in interface IVisitor
      Parameters:
      inst - The I2C instruction

    • visitI2D

      public void visitI2D(I2D inst)
      Converts an integer to a double and puts the result onto the symbolic stack
      Specified by:
      visitI2D in interface IVisitor
      Parameters:
      inst - The I2D instruction

    • visitI2F

      public void visitI2F(I2F inst)
      Converts an integer to a float and puts the result onto the symbolic stack
      Specified by:
      visitI2F in interface IVisitor
      Parameters:
      inst - The I2F instruction

    • visitI2L

      public void visitI2L(I2L inst)
      Converts an integer to a long and puts the result onto the symbolic stack
      Specified by:
      visitI2L in interface IVisitor
      Parameters:
      inst - The I2L instruction

    • visitI2S

      public void visitI2S(I2S inst)
      Converts an integer to a short and puts the result onto the symbolic stack
      Specified by:
      visitI2S in interface IVisitor
      Parameters:
      inst - The I2S instruction

    • visitIADD

      public void visitIADD(IADD inst)
      Adds two integers and pushes the result onto the symbolic stack
      Specified by:
      visitIADD in interface IVisitor
      Parameters:
      inst - The IADD instruction

    • visitIALOAD

      public void visitIALOAD(IALOAD inst)
      Loads an integer from an array and puts it onto the symbolic stack
      Specified by:
      visitIALOAD in interface IVisitor
      Parameters:
      inst - The IALOAD instruction

    • visitIAND

      public void visitIAND(IAND inst)
      Calculates the bitwise and of two integers in binary representation and puts the result onto the symbolic stack
      Specified by:
      visitIAND in interface IVisitor
      Parameters:
      inst - The IAND instruction

    • visitIASTORE

      public void visitIASTORE(IASTORE inst)
      Stores an integer into an array
      Specified by:
      visitIASTORE in interface IVisitor
      Parameters:
      inst - The IASTORE instruction

    • visitICONST_0

      public void visitICONST_0(ICONST_0 inst)
      Load the int value 0 onto the symbolic stack
      Specified by:
      visitICONST_0 in interface IVisitor
      Parameters:
      inst - Current instruction

    • visitICONST_1

      public void visitICONST_1(ICONST_1 inst)
      Load the int value 1 onto the symbolic stack
      Specified by:
      visitICONST_1 in interface IVisitor
      Parameters:
      inst - Current instruction

    • visitICONST_2

      public void visitICONST_2(ICONST_2 inst)
      Load the int value 2 onto the symbolic stack
      Specified by:
      visitICONST_2 in interface IVisitor
      Parameters:
      inst - Current instruction

    • visitICONST_3

      public void visitICONST_3(ICONST_3 inst)
      Load the int value 3 onto the symbolic stack
      Specified by:
      visitICONST_3 in interface IVisitor
      Parameters:
      inst - Current instruction

    • visitICONST_4

      public void visitICONST_4(ICONST_4 inst)
      Load the int value 4 onto the symbolic stack
      Specified by:
      visitICONST_4 in interface IVisitor
      Parameters:
      inst - Current instruction

    • visitICONST_5

      public void visitICONST_5(ICONST_5 inst)
      Load the int value 5 onto the symbolic stack
      Specified by:
      visitICONST_5 in interface IVisitor
      Parameters:
      inst - Current instruction

    • visitICONST_M1

      public void visitICONST_M1(ICONST_M1 inst)
      Load the int value -1 onto the symbolic stack
      Specified by:
      visitICONST_M1 in interface IVisitor
      Parameters:
      inst - Current ICONST_M1 instruction

    • visitIDIV

      public void visitIDIV(IDIV inst)
      Divides two integers and puts the result onto the symbolic stack.
      Specified by:
      visitIDIV in interface IVisitor
      Parameters:
      inst - Current IDIV instruction

    • visitIFEQ

      public void visitIFEQ(IFEQ inst)
      Branches if the top value on the stack is equal to 0
      Specified by:
      visitIFEQ in interface IVisitor
      Parameters:
      inst - The IFEQ instruction

    • visitIFGE

      public void visitIFGE(IFGE inst)
      Branches if the top value on the stack is greater or equal to 0
      Specified by:
      visitIFGE in interface IVisitor
      Parameters:
      inst - The IFGE instruction

    • visitIFGT

      public void visitIFGT(IFGT inst)
      Branches if the top value on the stack is greater then 0
      Specified by:
      visitIFGT in interface IVisitor
      Parameters:
      inst - The IFGT instruction

    • visitIFLE

      public void visitIFLE(IFLE inst)
      Branches if the top value on the stack is less or equal to 0
      Specified by:
      visitIFLE in interface IVisitor
      Parameters:
      inst - The IFLE instruction

    • visitIFLT

      public void visitIFLT(IFLT inst)
      Branches if the top value on the stack is less then 0
      Specified by:
      visitIFLT in interface IVisitor
      Parameters:
      inst - The IFLT instruction

    • visitIFNE

      public void visitIFNE(IFNE inst)
      Checks if the current Value is not equal to 0
      Specified by:
      visitIFNE in interface IVisitor
      Parameters:
      inst - The IFNE instruction

    • visitIFNONNULL

      public void visitIFNONNULL(IFNONNULL inst)
      Checks if an object is not null and saves the resulting symbolic formula as a path constraint
      Specified by:
      visitIFNONNULL in interface IVisitor
      Parameters:
      inst - The IFNONNULL instruction.

    • visitIFNULL

      public void visitIFNULL(IFNULL inst)
      Checks if an object is null and saves the resulting symbolic formula as a path constraint
      Specified by:
      visitIFNULL in interface IVisitor
      Parameters:
      inst - The IFNULL instruction.

    • visitIF_ACMPEQ

      public void visitIF_ACMPEQ(IF_ACMPEQ inst)
      Checks if two object references are equal and saves the resulting symbolic formula as a path constraint
      Specified by:
      visitIF_ACMPEQ in interface IVisitor
      Parameters:
      inst - The IF_ACMPEQ instruction.

    • visitIF_ACMPNE

      public void visitIF_ACMPNE(IF_ACMPNE inst)
      Checks if two object references are not equal and saves the resulting symbolic formula as a path constraint
      Specified by:
      visitIF_ACMPNE in interface IVisitor
      Parameters:
      inst - The IF_ACMPNE instruction.

    • visitIF_ICMPEQ

      public void visitIF_ICMPEQ(IF_ICMPEQ inst)
      Checks if the two integers are equal
      Specified by:
      visitIF_ICMPEQ in interface IVisitor
      Parameters:
      inst - The IF_ICMPEQ instruction

    • determineIid

      public int determineIid(int iid)

    • visitIF_ICMPGE

      public void visitIF_ICMPGE(IF_ICMPGE inst)
      Checks if the integer is greater or equal to the second integer
      Specified by:
      visitIF_ICMPGE in interface IVisitor
      Parameters:
      inst - The IF_ICMPGE instruction

    • visitIF_ICMPGT

      public void visitIF_ICMPGT(IF_ICMPGT inst)
      Checks if the integer is greater than the second integer
      Specified by:
      visitIF_ICMPGT in interface IVisitor
      Parameters:
      inst - The IF_ICMPGT instruction

    • visitIF_ICMPLE

      public void visitIF_ICMPLE(IF_ICMPLE inst)
      Checks if the integer is less than or equal to the second integer
      Specified by:
      visitIF_ICMPLE in interface IVisitor
      Parameters:
      inst - The IF_ICMPLE instruction

    • visitIF_ICMPLT

      public void visitIF_ICMPLT(IF_ICMPLT inst)
      Checks if the integer is greater than the second integer
      Specified by:
      visitIF_ICMPLT in interface IVisitor
      Parameters:
      inst - The IF_ICMPLT instruction

    • visitIF_ICMPNE

      public void visitIF_ICMPNE(IF_ICMPNE inst)
      Checks if the wo integers are not equal
      Specified by:
      visitIF_ICMPNE in interface IVisitor
      Parameters:
      inst - The IF_ICMPNE instruction

    • visitIINC

      public void visitIINC(IINC inst)
      Increments an integer that is in the locals. No change to the symbolic stack
      Specified by:
      visitIINC in interface IVisitor
      Parameters:
      inst - The IINC instruction

    • visitILOAD

      public void visitILOAD(ILOAD inst)
      Loads an integer from the locals onto the stack After this instruction a GETVALUE_int instruction follows to fetch the concrete value if the sybolic locals did not contain the value
      Specified by:
      visitILOAD in interface IVisitor
      Parameters:
      inst - The ILOAD instruction (including ILOAD_0 - ILOAD_3)

    • visitIMUL

      public void visitIMUL(IMUL inst)
      Multiplies two integers and adds the result onto the symbolic stack
      Specified by:
      visitIMUL in interface IVisitor
      Parameters:
      inst - The IMUL instruction

    • visitINEG

      public void visitINEG(INEG inst)
      Negates an integer and puts the resulting value onto the symbolic stack
      Specified by:
      visitINEG in interface IVisitor
      Parameters:
      inst - The INEG instruction

    • visitINSTANCEOF

      public void visitINSTANCEOF(INSTANCEOF inst)
      Removes the object reference from the symbolic stack and pushes true onto the symbolic stack. ToDo (Nils): Find a way to push the correct value onto the stack here See: Issue 61
      Specified by:
      visitINSTANCEOF in interface IVisitor
      Parameters:
      inst - The INSTANCEOF instruction.

    • visitINVOKEINTERFACE

      public void visitINVOKEINTERFACE(INVOKEINTERFACE inst)
      Invokes an interface method on an object reference from the symbolic stack
      Specified by:
      visitINVOKEINTERFACE in interface IVisitor
      Parameters:
      inst - The INVOKEINTERFACE instruction

    • visitINVOKESPECIAL

      public void visitINVOKESPECIAL(INVOKESPECIAL inst)
      Invokes an instance method on an object reference from the symbolic stack
      Specified by:
      visitINVOKESPECIAL in interface IVisitor
      Parameters:
      inst - The INVOKESPECIAL instruction

    • visitINVOKESTATIC

      public void visitINVOKESTATIC(INVOKESTATIC inst)
      Invokes a static method
      Specified by:
      visitINVOKESTATIC in interface IVisitor
      Parameters:
      inst - The INVOKESTATIC instruction

    • visitINVOKEVIRTUAL

      public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst)
      Invokes a virtual method on an object reference from the symbolic stack
      Specified by:
      visitINVOKEVIRTUAL in interface IVisitor
      Parameters:
      inst - The INVOKEVIRTUAL instruction

    • visitINVOKEDYNAMIC

      public void visitINVOKEDYNAMIC(INVOKEDYNAMIC inst)
      Invokes a dynamic method
      Specified by:
      visitINVOKEDYNAMIC in interface IVisitor
      Parameters:
      inst - The INVOKEDYNAMIC instruction

    • visitIOR

      public void visitIOR(IOR inst)
      Calculates the bitwise OR of two integers and puts the result onto the symbolic stack
      Specified by:
      visitIOR in interface IVisitor
      Parameters:
      inst - The IOR instruction

    • visitIREM

      public void visitIREM(IREM inst)
      Calculates the modulo of two integers and puts the result onto the symbolic stack
      Specified by:
      visitIREM in interface IVisitor
      Parameters:
      inst - The IREM instruction

    • visitIRETURN

      public void visitIRETURN(IRETURN inst)
      Sets the return value of the current symbolic frame to the int value on top of the symbolic stack
      Specified by:
      visitIRETURN in interface IVisitor
      Parameters:
      inst - The IRETURN instruction

    • visitISHL

      public void visitISHL(ISHL inst)
      Shifts an integer bitwise to the left and puts the result onto the symbolic stack
      Specified by:
      visitISHL in interface IVisitor
      Parameters:
      inst - The ISHL instruction

    • visitISHR

      public void visitISHR(ISHR inst)
      Shifts an integer bitwise arithmetically to the right and puts the result onto the symbolic stack
      Specified by:
      visitISHR in interface IVisitor
      Parameters:
      inst - The ISHR instruction

    • visitISTORE

      public void visitISTORE(ISTORE inst)
      Puts an integer from the symbolic stack into the symbolic locals
      Specified by:
      visitISTORE in interface IVisitor
      Parameters:
      inst - The ISTORE instruction

    • visitISUB

      public void visitISUB(ISUB inst)
      Subtracts two ints and puts the result onto the symbolic stack
      Specified by:
      visitISUB in interface IVisitor
      Parameters:
      inst - The ISUB instruction

    • visitIUSHR

      public void visitIUSHR(IUSHR inst)
      Shifts an integer bitwise logically to the right and puts the result onto the symbolic stack
      Specified by:
      visitIUSHR in interface IVisitor
      Parameters:
      inst - The IUSHR instruction

    • visitIXOR

      public void visitIXOR(IXOR inst)
      Calculates the bitwise exclusive OR of two integers and puts the result onto the symbolic stack
      Specified by:
      visitIXOR in interface IVisitor
      Parameters:
      inst - The IXOR instruction

    • visitJSR

      public void visitJSR(JSR inst)
      Jump subroutine. No symbolic handling needed. ToDo (Nils): The instruction pushes the return address onto the symbolic stack Should a placeholder be put here? See: Issue 62
      Specified by:
      visitJSR in interface IVisitor
      Parameters:
      inst - Either the JSR or JSR_W instruction

    • visitL2D

      public void visitL2D(L2D inst)
      Specified by:
      visitL2D in interface IVisitor

    • visitL2F

      public void visitL2F(L2F inst)
      Specified by:
      visitL2F in interface IVisitor

    • visitL2I

      public void visitL2I(L2I inst)
      Specified by:
      visitL2I in interface IVisitor

    • visitLADD

      public void visitLADD(LADD inst)
      Adds two longs and adds the result onto the symbolic stack
      Specified by:
      visitLADD in interface IVisitor
      Parameters:
      inst - The LADD instruction

    • visitLALOAD

      public void visitLALOAD(LALOAD inst)
      Loads a long from an array and puts it onto the symbolic stack
      Specified by:
      visitLALOAD in interface IVisitor
      Parameters:
      inst - The LALOAD instruction

    • visitLAND

      public void visitLAND(LAND inst)
      Calculates the bitwise and of two longs in binary representation and puts the resulting long onto the stack
      Specified by:
      visitLAND in interface IVisitor
      Parameters:
      inst - The LAND instruction

    • visitLASTORE

      public void visitLASTORE(LASTORE inst)
      Stores a long into an array
      Specified by:
      visitLASTORE in interface IVisitor
      Parameters:
      inst - The LASTORE instruction

    • visitLCMP

      public void visitLCMP(LCMP inst)
      Compares two longs and adds the result encoded as an integer onto the symbolic stack
      Specified by:
      visitLCMP in interface IVisitor
      Parameters:
      inst - The LCMP instruction

    • visitLCONST_0

      public void visitLCONST_0(LCONST_0 inst)
      Puts the constant 0L as a long onto the symbolic stack
      Specified by:
      visitLCONST_0 in interface IVisitor
      Parameters:
      inst - The LCONST_0 instruction

    • visitLCONST_1

      public void visitLCONST_1(LCONST_1 inst)
      Puts the constant 1L as a long onto the symbolic stack
      Specified by:
      visitLCONST_1 in interface IVisitor
      Parameters:
      inst - The LCONST_1 instruction

    • visitLDC_String

      public void visitLDC_String(LDC_String inst)
      Puts a constant string onto the symbolic stack
      Specified by:
      visitLDC_String in interface IVisitor
      Parameters:
      inst - The (artificial) LDC_String instruction

    • visitLDC_Object

      public void visitLDC_Object(LDC_Object inst)
      Puts an object onto the symbolic stack
      Specified by:
      visitLDC_Object in interface IVisitor
      Parameters:
      inst - The (artificial) LDC_Object instruction

    • visitLDC_double

      public void visitLDC_double(LDC_double inst)
      Puts a constant double onto the symbolic stack
      Specified by:
      visitLDC_double in interface IVisitor
      Parameters:
      inst - The (artificial) LDC_double instruction

    • visitLDC_float

      public void visitLDC_float(LDC_float inst)
      Puts a constant float onto the symbolic stack
      Specified by:
      visitLDC_float in interface IVisitor
      Parameters:
      inst - The (artificial) LDC_float instruction

    • visitLDC_int

      public void visitLDC_int(LDC_int inst)
      Loads a constant int onto the symbolic stack
      Specified by:
      visitLDC_int in interface IVisitor
      Parameters:
      inst - The (artificial) LDC_int instruction

    • visitLDC_long

      public void visitLDC_long(LDC_long inst)
      Loads a constant long onto the symbolic stack
      Specified by:
      visitLDC_long in interface IVisitor
      Parameters:
      inst - The (artificial) LDC_long instruction

    • visitLDIV

      public void visitLDIV(LDIV inst)
      Divides two longs and puts the result onto the symbolic stack
      Specified by:
      visitLDIV in interface IVisitor
      Parameters:
      inst - The LDIV instruction

    • visitLLOAD

      public void visitLLOAD(LLOAD inst)
      Loads a long from the symbolic locals and adds it to the symbolic stack
      Specified by:
      visitLLOAD in interface IVisitor
      Parameters:
      inst - One of the LLOAD isntructions (LLOAD, LLOAD_0 - LLOAD_3)

    • visitLMUL

      public void visitLMUL(LMUL inst)
      Multiplies two longs and puts the result onto the symbolic stack
      Specified by:
      visitLMUL in interface IVisitor
      Parameters:
      inst - The LMUL instruction

    • visitLNEG

      public void visitLNEG(LNEG inst)
      Negates a long and puts the result onto the symbolic stack
      Specified by:
      visitLNEG in interface IVisitor
      Parameters:
      inst - The LNEG isntruction

    • visitLOR

      public void visitLOR(LOR inst)
      Calculates the bitwise or of two longs and puts the result onto the symbolic stack
      Specified by:
      visitLOR in interface IVisitor
      Parameters:
      inst - The LOR instruction

    • visitLREM

      public void visitLREM(LREM inst)
      Calculates the modulo of two longs and puts the result onto the symbolic stack
      Specified by:
      visitLREM in interface IVisitor
      Parameters:
      inst - The LREM instruction

    • visitLRETURN

      public void visitLRETURN(LRETURN inst)
      Sets the return value of the current symbolic frame to the long value on top of the symbolic stack
      Specified by:
      visitLRETURN in interface IVisitor
      Parameters:
      inst - The LRETURN instruction

    • visitLSHL

      public void visitLSHL(LSHL inst)
      Calculates the bitwise left shift of a long and puts the result onto the symbolic stack
      Specified by:
      visitLSHL in interface IVisitor
      Parameters:
      inst - The LSHL instruction

    • visitLSHR

      public void visitLSHR(LSHR inst)
      Calculates the bitwise right shift of a long and puts the result onto the symbolic stack
      Specified by:
      visitLSHR in interface IVisitor
      Parameters:
      inst - The LSHR instruction

    • visitLSTORE

      public void visitLSTORE(LSTORE inst)
      Stores the top value from the symbolic stack (long) into a slot in the symbolic locals
      Specified by:
      visitLSTORE in interface IVisitor
      Parameters:
      inst - One of the LSTORE instructions (LSTORE, LSTORE_0 - LSTORE_3)

    • visitLSUB

      public void visitLSUB(LSUB inst)
      Subtracts two longs and puts the result onto the symbolic stack
      Specified by:
      visitLSUB in interface IVisitor
      Parameters:
      inst - The LSUB instruction

    • visitLUSHR

      public void visitLUSHR(LUSHR inst)
      Calculates the bitwise logical right shift of a long and puts the result onto the symbolic stack
      Specified by:
      visitLUSHR in interface IVisitor
      Parameters:
      inst - The LUSHR instruction

    • visitLXOR

      public void visitLXOR(LXOR inst)
      Calculates the bitwise exclusive or of two longs and puts the result onto the symbolic stack
      Specified by:
      visitLXOR in interface IVisitor
      Parameters:
      inst - The LXOR instruction

    • visitMONITORENTER

      public void visitMONITORENTER(MONITORENTER inst)
      No symbolic behaviour defined.
      Specified by:
      visitMONITORENTER in interface IVisitor
      Parameters:
      inst - The MONITORENTER instruction.

    • visitMONITOREXIT

      public void visitMONITOREXIT(MONITOREXIT inst)
      No symbolic behaviour defined.
      Specified by:
      visitMONITOREXIT in interface IVisitor
      Parameters:
      inst - The MONITOREXIT instruction.

    • visitNEW

      public void visitNEW(NEW inst)
      Specified by:
      visitNEW in interface IVisitor

    • visitNEWARRAY

      public void visitNEWARRAY(NEWARRAY inst)
      Specified by:
      visitNEWARRAY in interface IVisitor

    • visitNOP

      public void visitNOP(NOP inst)
      Nothing to do here ;D
      Specified by:
      visitNOP in interface IVisitor
      Parameters:
      inst - The NOP instruction.

    • visitPOP

      public void visitPOP(POP inst)
      Pops the top value from the symbolic stack.
      Specified by:
      visitPOP in interface IVisitor
      Parameters:
      inst - The POP instruction

    • visitPOP2

      public void visitPOP2(POP2 inst)
      Pops the top two values from the symbolic stack.
      Specified by:
      visitPOP2 in interface IVisitor
      Parameters:
      inst - The POP2 instruction

    • visitPUTFIELD

      public void visitPUTFIELD(PUTFIELD inst)
      Puts a value into the field of an object reference The handling has changed in the JVM: - SE11 (new) - SE7 (Old)
      Specified by:
      visitPUTFIELD in interface IVisitor
      Parameters:
      inst - The PUTFIELD instruction

    • visitPUTSTATIC

      public void visitPUTSTATIC(PUTSTATIC inst)
      Puts a value into a static field of a class
      Specified by:
      visitPUTSTATIC in interface IVisitor
      Parameters:
      inst - The PUTSTATIC instruction

    • visitRET

      public void visitRET(RET inst)
      Unconditional jump no handling needed
      Specified by:
      visitRET in interface IVisitor
      Parameters:
      inst - The RET instruction

    • visitRETURN

      public void visitRETURN(RETURN inst)
      Returns void from method, no handling needed (here)
      Specified by:
      visitRETURN in interface IVisitor
      Parameters:
      inst - The RETURN instruction

    • visitSALOAD

      public void visitSALOAD(SALOAD inst)
      Retrieves a short from an array and puts it onto the symbolic stack
      Specified by:
      visitSALOAD in interface IVisitor
      Parameters:
      inst - The SALOAD instruction.

    • visitSASTORE

      public void visitSASTORE(SASTORE inst)
      Stores a short into an array
      Specified by:
      visitSASTORE in interface IVisitor
      Parameters:
      inst - The SASTORE instruction.

    • visitSIPUSH

      public void visitSIPUSH(SIPUSH inst)
      Pushes a short onto the symbolic stack as an integer
      Specified by:
      visitSIPUSH in interface IVisitor
      Parameters:
      inst - The SIPUSH instruction

    • visitSWAP

      public void visitSWAP(SWAP inst)
      Swaps the top two words on the symbolic stack
      Specified by:
      visitSWAP in interface IVisitor
      Parameters:
      inst - The SWAP instruction

    • visitINVOKEMETHOD_EXCEPTION

      public void visitINVOKEMETHOD_EXCEPTION(INVOKEMETHOD_EXCEPTION inst)
      Specified by:
      visitINVOKEMETHOD_EXCEPTION in interface IVisitor

    • visitINVOKEMETHOD_END

      public void visitINVOKEMETHOD_END(INVOKEMETHOD_END inst)
      Removes a frame from the stack frame and puts the removed frame's return value onto the old (current) frame's stack
      Specified by:
      visitINVOKEMETHOD_END in interface IVisitor
      Parameters:
      inst - INVOKEMETHOD_END

    • visitMAKE_SYMBOLIC

      public void visitMAKE_SYMBOLIC(MAKE_SYMBOLIC inst)
      Specified by:
      visitMAKE_SYMBOLIC in interface IVisitor

    • visitLOOP_BEGIN

      public void visitLOOP_BEGIN(LOOP_BEGIN inst)
      Specified by:
      visitLOOP_BEGIN in interface IVisitor

    • visitLOOP_END

      public void visitLOOP_END(LOOP_END inst)
      Specified by:
      visitLOOP_END in interface IVisitor

    • visitSPECIAL

      public void visitSPECIAL(SPECIAL inst)
      Specified by:
      visitSPECIAL in interface IVisitor

    • setNext

      public void setNext(Instruction next)
      Specified by:
      setNext in interface IVisitor

    • visitMULTIANEWARRAY

      public void visitMULTIANEWARRAY(MULTIANEWARRAY inst)
      Creates a multidimensional array of references. Currently, no symbolic handling here because arrays are not of primitive type? See: Issue 63
      Specified by:
      visitMULTIANEWARRAY in interface IVisitor
      Parameters:
      inst - The MULTIANEWARRAY instruction

    • visitLOOKUPSWITCH

      public void visitLOOKUPSWITCH(LOOKUPSWITCH inst)
      Builds a path-constraint based on where the execution continues. ToDo (Nils): Constraint correctness not verified!
      Specified by:
      visitLOOKUPSWITCH in interface IVisitor
      Parameters:
      inst - The LOOKUPSWITCH instruction.

    • visitTABLESWITCH

      public void visitTABLESWITCH(TABLESWITCH inst)
      Builds a path-constraint based on where the execution continues. ToDo (Nils): Constraint correctness not verified!
      Specified by:
      visitTABLESWITCH in interface IVisitor
      Parameters:
      inst - The TABLESWITCH instruction.

    • getStack

      public Stack<Frame> getStack()

    • getSymbolicStateHandler

      public SymbolicTraceHandler getSymbolicStateHandler()

    • getCurrentFrame

      public Frame getCurrentFrame()