InstConstraintVisitor.java

  1. /*
  2.  * Licensed to the Apache Software Foundation (ASF) under one or more
  3.  * contributor license agreements.  See the NOTICE file distributed with
  4.  * this work for additional information regarding copyright ownership.
  5.  * The ASF licenses this file to You under the Apache License, Version 2.0
  6.  * (the "License"); you may not use this file except in compliance with
  7.  * the License.  You may obtain a copy of the License at
  8.  *
  9.  *      http://www.apache.org/licenses/LICENSE-2.0
  10.  *
  11.  *  Unless required by applicable law or agreed to in writing, software
  12.  *  distributed under the License is distributed on an "AS IS" BASIS,
  13.  *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  14.  *  See the License for the specific language governing permissions and
  15.  *  limitations under the License.
  16.  */
  17. package org.apache.bcel.verifier.structurals;

  19. import org.apache.bcel.Const;
  20. import org.apache.bcel.Repository;
  21. import org.apache.bcel.classfile.Constant;
  22. import org.apache.bcel.classfile.ConstantClass;
  23. import org.apache.bcel.classfile.ConstantDouble;
  24. import org.apache.bcel.classfile.ConstantDynamic;
  25. import org.apache.bcel.classfile.ConstantFieldref;
  26. import org.apache.bcel.classfile.ConstantFloat;
  27. import org.apache.bcel.classfile.ConstantInteger;
  28. import org.apache.bcel.classfile.ConstantLong;
  29. import org.apache.bcel.classfile.ConstantString;
  30. import org.apache.bcel.classfile.Field;
  31. import org.apache.bcel.classfile.JavaClass;
  32. //CHECKSTYLE:OFF (there are lots of references!)
  33. import org.apache.bcel.generic.*;
  34. //CHECKSTYLE:ON
  35. import org.apache.bcel.verifier.VerificationResult;
  36. import org.apache.bcel.verifier.Verifier;
  37. import org.apache.bcel.verifier.VerifierFactory;
  38. import org.apache.bcel.verifier.exc.AssertionViolatedException;
  39. import org.apache.bcel.verifier.exc.StructuralCodeConstraintException;

  41. /**
  42.  * A Visitor class testing for valid preconditions of JVM instructions. The instance of this class will throw a
  43.  * StructuralCodeConstraintException instance if an instruction is visitXXX()ed which has preconditions that are not
  44.  * satisfied. TODO: Currently, the JVM's behavior concerning monitors (MONITORENTER, MONITOREXIT) is not modeled in
  45.  * JustIce.
  46.  *
  47.  * @see StructuralCodeConstraintException
  48.  */
  49. public class InstConstraintVisitor extends EmptyVisitor {

  51.     private static final ObjectType GENERIC_ARRAY = ObjectType.getInstance(GenericArray.class.getName());

  53.     /**
  54.      * The Execution Frame we're working on.
  55.      *
  56.      * @see #setFrame(Frame f)
  57.      * @see #locals()
  58.      * @see #stack()
  59.      */
  60.     private Frame frame;

  62.     /**
  63.      * The ConstantPoolGen we're working on.
  64.      *
  65.      * @see #setConstantPoolGen(ConstantPoolGen cpg)
  66.      */
  67.     private ConstantPoolGen cpg;

  69.     /**
  70.      * The MethodGen we're working on.
  71.      *
  72.      * @see #setMethodGen(MethodGen mg)
  73.      */
  74.     private MethodGen mg;

  76.     /**
  77.      * The constructor. Constructs a new instance of this class.
  78.      */
  79.     public InstConstraintVisitor() {
  80.     }

  82.     /**
  83.      * Assures arrayref is of ArrayType or NULL; returns true if and only if arrayref is non-NULL.
  84.      *
  85.      * @throws StructuralCodeConstraintException if the above constraint is violated.
  86.      */
  87.     private boolean arrayrefOfArrayType(final Instruction o, final Type arrayref) {
  88.         if (!(arrayref instanceof ArrayType || arrayref.equals(Type.NULL))) {
  89.             constraintViolated(o, "The 'arrayref' does not refer to an array but is of type " + arrayref + ".");
  90.         }
  91.         return arrayref instanceof ArrayType;
  92.     }

  94.     /**
  95.      * This method is called by the visitXXX() to notify the acceptor of this InstConstraintVisitor that a constraint
  96.      * violation has occurred. This is done by throwing an instance of a StructuralCodeConstraintException.
  97.      *
  98.      * @throws StructuralCodeConstraintException always.
  99.      */
  100.     private void constraintViolated(final Instruction violator, final String description) {
  101.         final String fqClassName = violator.getClass().getName();
  102.         throw new StructuralCodeConstraintException(
  103.             "Instruction " + fqClassName.substring(fqClassName.lastIndexOf('.') + 1) + " constraint violated: " + description);
  104.     }

  106.     private ObjectType getObjectType(final FieldInstruction o) {
  107.         final ReferenceType rt = o.getReferenceType(cpg);
  108.         if (rt instanceof ObjectType) {
  109.             return (ObjectType) rt;
  110.         }
  111.         constraintViolated(o, "expecting ObjectType but got " + rt);
  112.         return null;
  113.     }

  115.     /**
  116.      * Assures index is of type INT.
  117.      *
  118.      * @throws StructuralCodeConstraintException if the above constraint is not satisfied.
  119.      */
  120.     private void indexOfInt(final Instruction o, final Type index) {
  121.         if (!index.equals(Type.INT)) {
  122.             constraintViolated(o, "The 'index' is not of type int but of type " + index + ".");
  123.         }
  124.     }

  126.     /**
  127.      * The LocalVariables we're working on.
  128.      *
  129.      * @see #setFrame(Frame f)
  130.      */
  131.     private LocalVariables locals() {
  132.         return frame.getLocals();
  133.     }

  135.     /**
  136.      * Assures the ReferenceType r is initialized (or Type.NULL). Formally, this means (!(r instanceof
  137.      * UninitializedObjectType)), because there are no uninitialized array types.
  138.      *
  139.      * @throws StructuralCodeConstraintException if the above constraint is not satisfied.
  140.      */
  141.     private void referenceTypeIsInitialized(final Instruction o, final ReferenceType r) {
  142.         if (r instanceof UninitializedObjectType) {
  143.             constraintViolated(o, "Working on an uninitialized object '" + r + "'.");
  144.         }
  145.     }

  147.     /**
  148.      * Sets the ConstantPoolGen instance needed for constraint checking prior to execution.
  149.      */
  150.     public void setConstantPoolGen(final ConstantPoolGen cpg) { // TODO could be package-protected?
  151.         this.cpg = cpg;
  152.     }

  154.     /**
  155.      * This returns the single instance of the InstConstraintVisitor class. To operate correctly, other values must have
  156.      * been set before actually using the instance. Use this method for performance reasons.
  157.      *
  158.      * @see #setConstantPoolGen(ConstantPoolGen cpg)
  159.      * @see #setMethodGen(MethodGen mg)
  160.      */
  161.     public void setFrame(final Frame f) { // TODO could be package-protected?
  162.         this.frame = f;
  163.         // if (singleInstance.mg == null || singleInstance.cpg == null)
  164.         // throw new AssertionViolatedException("Forgot to set important values first.");
  165.     }

  167.     /**
  168.      * Sets the MethodGen instance needed for constraint checking prior to execution.
  169.      */
  170.     public void setMethodGen(final MethodGen mg) {
  171.         this.mg = mg;
  172.     }

  174.     /**
  175.      * The OperandStack we're working on.
  176.      *
  177.      * @see #setFrame(Frame f)
  178.      */
  179.     private OperandStack stack() {
  180.         return frame.getStack();
  181.     }

  183.     /** Assures value is of type INT. */
  184.     private void valueOfInt(final Instruction o, final Type value) {
  185.         if (!value.equals(Type.INT)) {
  186.             constraintViolated(o, "The 'value' is not of type int but of type " + value + ".");
  187.         }
  188.     }

  190.     /***************************************************************/
  191.     /* "generic"visitXXXX methods where XXXX is an interface */
  192.     /* therefore, we don't know the order of visiting; but we know */
  193.     /* these methods are called before the visitYYYY methods below */
  194.     /***************************************************************/

  196.     /**
  197.      * Ensures the specific preconditions of the said instruction.
  198.      */
  199.     @Override
  200.     public void visitAALOAD(final AALOAD o) {
  201.         final Type arrayref = stack().peek(1);
  202.         final Type index = stack().peek(0);

  204.         indexOfInt(o, index);
  205.         if (arrayrefOfArrayType(o, arrayref) && !(((ArrayType) arrayref).getElementType() instanceof ReferenceType)) {
  206.             constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "
  207.                 + ((ArrayType) arrayref).getElementType() + ".");
  208.         }
  209.         // referenceTypeIsInitialized(o, (ReferenceType) (((ArrayType) arrayref).getElementType()));
  210.     }

  212.     /**
  213.      * Ensures the specific preconditions of the said instruction.
  214.      */
  215.     @Override
  216.     public void visitAASTORE(final AASTORE o) {
  217.         final Type arrayref = stack().peek(2);
  218.         final Type index = stack().peek(1);
  219.         final Type value = stack().peek(0);

  221.         indexOfInt(o, index);
  222.         if (!(value instanceof ReferenceType)) {
  223.             constraintViolated(o, "The 'value' is not of a ReferenceType but of type " + value + ".");
  224.         }
  225.         // } else {
  226.             // referenceTypeIsInitialized(o, (ReferenceType) value);
  227.         // }
  228.         //
  229.         // Don't bother further with "referenceTypeIsInitialized()", there are no arrays
  230.         // of an uninitialized object type.
  231.         if (arrayrefOfArrayType(o, arrayref) && !(((ArrayType) arrayref).getElementType() instanceof ReferenceType)) {
  232.             constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a ReferenceType but to an array of "
  233.                 + ((ArrayType) arrayref).getElementType() + ".");
  234.         }
  235.         // No check for array element assignment compatibility. This is done at runtime.
  236.     }

  238.     /**
  239.      * Ensures the specific preconditions of the said instruction.
  240.      */
  241.     @Override
  242.     public void visitACONST_NULL(final ACONST_NULL o) {
  243.         // Nothing needs to be done here.
  244.     }

  246.     /**
  247.      * Ensures the specific preconditions of the said instruction.
  248.      */
  249.     @Override
  250.     public void visitALOAD(final ALOAD o) {
  251.         // visitLoadInstruction(LoadInstruction) is called before.

  253.         // Nothing else needs to be done here.
  254.     }

  256.     /**
  257.      * Ensures the specific preconditions of the said instruction.
  258.      */
  259.     @Override
  260.     public void visitANEWARRAY(final ANEWARRAY o) {
  261.         if (!stack().peek().equals(Type.INT)) {
  262.             constraintViolated(o, "The 'count' at the stack top is not of type '" + Type.INT + "' but of type '" + stack().peek() + "'.");
  263.             // The runtime constant pool item at that index must be a symbolic reference to a class,
  264.             // array, or interface type. See Pass 3a.
  265.         }
  266.     }

  268.     /**
  269.      * Ensures the specific preconditions of the said instruction.
  270.      */
  271.     @Override
  272.     public void visitARETURN(final ARETURN o) {
  273.         if (!(stack().peek() instanceof ReferenceType)) {
  274.             constraintViolated(o, "The 'objectref' at the stack top is not of a ReferenceType but of type '" + stack().peek() + "'.");
  275.         }
  276.         final ReferenceType objectref = (ReferenceType) stack().peek();
  277.         referenceTypeIsInitialized(o, objectref);

  279.         // The check below should already done via visitReturnInstruction(ReturnInstruction), see there.
  280.         // It cannot be done using Staerk-et-al's "set of object types" instead of a
  281.         // "wider cast object type", anyway.
  282.         // if (! objectref.isAssignmentCompatibleWith(mg.getReturnType() )) {
  283.         // constraintViolated(o, "The 'objectref' type "+objectref+
  284.         // " at the stack top is not assignment compatible with the return type '"+mg.getReturnType()+"' of the method.");
  285.         // }
  286.     }

  288.     /**
  289.      * Ensures the specific preconditions of the said instruction.
  290.      */
  291.     @Override
  292.     public void visitARRAYLENGTH(final ARRAYLENGTH o) {
  293.         final Type arrayref = stack().peek(0);
  294.         arrayrefOfArrayType(o, arrayref);
  295.     }

  297.     /**
  298.      * Ensures the specific preconditions of the said instruction.
  299.      */
  300.     @Override
  301.     public void visitASTORE(final ASTORE o) {
  302.         if (!(stack().peek() instanceof ReferenceType || stack().peek() instanceof ReturnaddressType)) {
  303.             constraintViolated(o, "The 'objectref' is not of a ReferenceType or of ReturnaddressType but of " + stack().peek() + ".");
  304.         }
  305.         // if (stack().peek() instanceof ReferenceType) {
  306.         // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
  307.         // }
  308.     }

  310.     /**
  311.      * Ensures the specific preconditions of the said instruction.
  312.      */
  313.     @Override
  314.     public void visitATHROW(final ATHROW o) {
  315.         try {
  316.             // It's stated that 'objectref' must be of a ReferenceType --- but since Throwable is
  317.             // not derived from an ArrayType, it follows that 'objectref' must be of an ObjectType or Type.NULL.
  318.             if (!(stack().peek() instanceof ObjectType || stack().peek().equals(Type.NULL))) {
  319.                 constraintViolated(o, "The 'objectref' is not of an (initialized) ObjectType but of type " + stack().peek() + ".");
  320.             }

  322.             // NULL is a subclass of every class, so to speak.
  323.             if (stack().peek().equals(Type.NULL)) {
  324.                 return;
  325.             }

  327.             final ObjectType exc = (ObjectType) stack().peek();
  328.             final ObjectType throwable = (ObjectType) Type.getType("Ljava/lang/Throwable;");
  329.             if (!exc.subclassOf(throwable) && !exc.equals(throwable)) {
  330.                 constraintViolated(o, "The 'objectref' is not of class Throwable or of a subclass of Throwable, but of '" + stack().peek() + "'.");
  331.             }
  332.         } catch (final ClassNotFoundException e) {
  333.             // FIXME: maybe not the best way to handle this
  334.             throw new AssertionViolatedException("Missing class: " + e, e);
  335.         }
  336.     }

  338.     /**
  339.      * Ensures the specific preconditions of the said instruction.
  340.      */
  341.     @Override
  342.     public void visitBALOAD(final BALOAD o) {
  343.         final Type arrayref = stack().peek(1);
  344.         final Type index = stack().peek(0);
  345.         indexOfInt(o, index);
  346.         if (arrayrefOfArrayType(o, arrayref)
  347.             && !(((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN) || ((ArrayType) arrayref).getElementType().equals(Type.BYTE))) {
  348.             constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"
  349.                 + ((ArrayType) arrayref).getElementType() + "'.");
  350.         }
  351.     }

  353.     /**
  354.      * Ensures the specific preconditions of the said instruction.
  355.      */
  356.     @Override
  357.     public void visitBASTORE(final BASTORE o) {
  358.         final Type arrayref = stack().peek(2);
  359.         final Type index = stack().peek(1);
  360.         final Type value = stack().peek(0);

  362.         indexOfInt(o, index);
  363.         valueOfInt(o, value);
  364.         if (arrayrefOfArrayType(o, arrayref)
  365.             && !(((ArrayType) arrayref).getElementType().equals(Type.BOOLEAN) || ((ArrayType) arrayref).getElementType().equals(Type.BYTE))) {
  366.             constraintViolated(o, "The 'arrayref' does not refer to an array with elements of a Type.BYTE or Type.BOOLEAN but to an array of '"
  367.                 + ((ArrayType) arrayref).getElementType() + "'.");
  368.         }
  369.     }

  371.     /***************************************************************/
  372.     /* "special"visitXXXX methods for one type of instruction each */
  373.     /***************************************************************/

  375.     /**
  376.      * Ensures the specific preconditions of the said instruction.
  377.      */
  378.     @Override
  379.     public void visitBIPUSH(final BIPUSH o) {
  380.         // Nothing to do...
  381.     }

  383.     /**
  384.      * Ensures the specific preconditions of the said instruction.
  385.      */
  386.     @Override
  387.     public void visitBREAKPOINT(final BREAKPOINT o) {
  388.         throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as BREAKPOINT.");
  389.     }

  391.     /**
  392.      * Ensures the specific preconditions of the said instruction.
  393.      */
  394.     @Override
  395.     public void visitCALOAD(final CALOAD o) {
  396.         final Type arrayref = stack().peek(1);
  397.         final Type index = stack().peek(0);

  399.         indexOfInt(o, index);
  400.         arrayrefOfArrayType(o, arrayref);
  401.     }

  403.     /**
  404.      * Ensures the specific preconditions of the said instruction.
  405.      */
  406.     @Override
  407.     public void visitCASTORE(final CASTORE o) {
  408.         final Type arrayref = stack().peek(2);
  409.         final Type index = stack().peek(1);
  410.         final Type value = stack().peek(0);

  412.         indexOfInt(o, index);
  413.         valueOfInt(o, value);
  414.         if (arrayrefOfArrayType(o, arrayref) && !((ArrayType) arrayref).getElementType().equals(Type.CHAR)) {
  415.             constraintViolated(o, "The 'arrayref' does not refer to an array with elements of type char but to an array of type "
  416.                 + ((ArrayType) arrayref).getElementType() + ".");
  417.         }
  418.     }

  420.     /**
  421.      * Ensures the specific preconditions of the said instruction.
  422.      */
  423.     @Override
  424.     public void visitCHECKCAST(final CHECKCAST o) {
  425.         // The objectref must be of type reference.
  426.         final Type objectref = stack().peek(0);
  427.         if (!(objectref instanceof ReferenceType)) {
  428.             constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type " + objectref + ".");
  429.         }
  430.         // else{
  431.         // referenceTypeIsInitialized(o, (ReferenceType) objectref);
  432.         // }
  433.         // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
  434.         // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
  435.         // pool item at the index must be a symbolic reference to a class, array, or interface type.
  436.         final Constant c = cpg.getConstant(o.getIndex());
  437.         if (!(c instanceof ConstantClass)) {
  438.             constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '" + c + "'.");
  439.         }
  440.     }

  442.     /***************************************************************/
  443.     /* "generic" visitYYYY methods where YYYY is a superclass. */
  444.     /* therefore, we know the order of visiting; we know */
  445.     /* these methods are called after the visitXXXX methods above. */
  446.     /***************************************************************/
  447.     /**
  448.      * Ensures the general preconditions of a CPInstruction instance.
  449.      */
  450.     @Override
  451.     public void visitCPInstruction(final CPInstruction o) {
  452.         final int idx = o.getIndex();
  453.         if (idx < 0 || idx >= cpg.getSize()) {
  454.             throw new AssertionViolatedException("Huh?! Constant pool index of instruction '" + o + "' illegal? Pass 3a should have checked this!");
  455.         }
  456.     }

  458.     /**
  459.      * Ensures the specific preconditions of the said instruction.
  460.      */
  461.     @Override
  462.     public void visitD2F(final D2F o) {
  463.         if (stack().peek() != Type.DOUBLE) {
  464.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  465.         }
  466.     }

  468.     /**
  469.      * Ensures the specific preconditions of the said instruction.
  470.      */
  471.     @Override
  472.     public void visitD2I(final D2I o) {
  473.         if (stack().peek() != Type.DOUBLE) {
  474.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  475.         }
  476.     }

  478.     /**
  479.      * Ensures the specific preconditions of the said instruction.
  480.      */
  481.     @Override
  482.     public void visitD2L(final D2L o) {
  483.         if (stack().peek() != Type.DOUBLE) {
  484.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  485.         }
  486.     }

  488.     /**
  489.      * Ensures the specific preconditions of the said instruction.
  490.      */
  491.     @Override
  492.     public void visitDADD(final DADD o) {
  493.         if (stack().peek() != Type.DOUBLE) {
  494.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  495.         }
  496.         if (stack().peek(1) != Type.DOUBLE) {
  497.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  498.         }
  499.     }

  501.     /**
  502.      * Ensures the specific preconditions of the said instruction.
  503.      */
  504.     @Override
  505.     public void visitDALOAD(final DALOAD o) {
  506.         indexOfInt(o, stack().peek());
  507.         if (stack().peek(1) == Type.NULL) {
  508.             return;
  509.         }
  510.         if (!(stack().peek(1) instanceof ArrayType)) {
  511.             constraintViolated(o, "Stack next-to-top must be of type double[] but is '" + stack().peek(1) + "'.");
  512.         }
  513.         final Type t = ((ArrayType) stack().peek(1)).getBasicType();
  514.         if (t != Type.DOUBLE) {
  515.             constraintViolated(o, "Stack next-to-top must be of type double[] but is '" + stack().peek(1) + "'.");
  516.         }
  517.     }

  519.     /**
  520.      * Ensures the specific preconditions of the said instruction.
  521.      */
  522.     @Override
  523.     public void visitDASTORE(final DASTORE o) {
  524.         if (stack().peek() != Type.DOUBLE) {
  525.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  526.         }
  527.         indexOfInt(o, stack().peek(1));
  528.         if (stack().peek(2) == Type.NULL) {
  529.             return;
  530.         }
  531.         if (!(stack().peek(2) instanceof ArrayType)) {
  532.             constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '" + stack().peek(2) + "'.");
  533.         }
  534.         final Type t = ((ArrayType) stack().peek(2)).getBasicType();
  535.         if (t != Type.DOUBLE) {
  536.             constraintViolated(o, "Stack next-to-next-to-top must be of type double[] but is '" + stack().peek(2) + "'.");
  537.         }
  538.     }

  540.     /**
  541.      * Ensures the specific preconditions of the said instruction.
  542.      */
  543.     @Override
  544.     public void visitDCMPG(final DCMPG o) {
  545.         if (stack().peek() != Type.DOUBLE) {
  546.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  547.         }
  548.         if (stack().peek(1) != Type.DOUBLE) {
  549.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  550.         }
  551.     }

  553.     /**
  554.      * Ensures the specific preconditions of the said instruction.
  555.      */
  556.     @Override
  557.     public void visitDCMPL(final DCMPL o) {
  558.         if (stack().peek() != Type.DOUBLE) {
  559.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  560.         }
  561.         if (stack().peek(1) != Type.DOUBLE) {
  562.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  563.         }
  564.     }

  566.     /**
  567.      * Ensures the specific preconditions of the said instruction.
  568.      */
  569.     @Override
  570.     public void visitDCONST(final DCONST o) {
  571.         // There's nothing to be done here.
  572.     }

  574.     /**
  575.      * Ensures the specific preconditions of the said instruction.
  576.      */
  577.     @Override
  578.     public void visitDDIV(final DDIV o) {
  579.         if (stack().peek() != Type.DOUBLE) {
  580.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  581.         }
  582.         if (stack().peek(1) != Type.DOUBLE) {
  583.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  584.         }
  585.     }

  587.     /**
  588.      * Ensures the specific preconditions of the said instruction.
  589.      */
  590.     @Override
  591.     public void visitDLOAD(final DLOAD o) {
  592.         // visitLoadInstruction(LoadInstruction) is called before.

  594.         // Nothing else needs to be done here.
  595.     }

  597.     /**
  598.      * Ensures the specific preconditions of the said instruction.
  599.      */
  600.     @Override
  601.     public void visitDMUL(final DMUL o) {
  602.         if (stack().peek() != Type.DOUBLE) {
  603.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  604.         }
  605.         if (stack().peek(1) != Type.DOUBLE) {
  606.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  607.         }
  608.     }

  610.     /**
  611.      * Ensures the specific preconditions of the said instruction.
  612.      */
  613.     @Override
  614.     public void visitDNEG(final DNEG o) {
  615.         if (stack().peek() != Type.DOUBLE) {
  616.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  617.         }
  618.     }

  620.     /**
  621.      * Ensures the specific preconditions of the said instruction.
  622.      */
  623.     @Override
  624.     public void visitDREM(final DREM o) {
  625.         if (stack().peek() != Type.DOUBLE) {
  626.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  627.         }
  628.         if (stack().peek(1) != Type.DOUBLE) {
  629.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  630.         }
  631.     }

  633.     /**
  634.      * Ensures the specific preconditions of the said instruction.
  635.      */
  636.     @Override
  637.     public void visitDRETURN(final DRETURN o) {
  638.         if (stack().peek() != Type.DOUBLE) {
  639.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  640.         }
  641.     }

  643.     /**
  644.      * Ensures the specific preconditions of the said instruction.
  645.      */
  646.     @Override
  647.     public void visitDSTORE(final DSTORE o) {
  648.         // visitStoreInstruction(StoreInstruction) is called before.

  650.         // Nothing else needs to be done here.
  651.     }

  653.     /**
  654.      * Ensures the specific preconditions of the said instruction.
  655.      */
  656.     @Override
  657.     public void visitDSUB(final DSUB o) {
  658.         if (stack().peek() != Type.DOUBLE) {
  659.             constraintViolated(o, "The value at the stack top is not of type 'double', but of type '" + stack().peek() + "'.");
  660.         }
  661.         if (stack().peek(1) != Type.DOUBLE) {
  662.             constraintViolated(o, "The value at the stack next-to-top is not of type 'double', but of type '" + stack().peek(1) + "'.");
  663.         }
  664.     }

  666.     /**
  667.      * Ensures the specific preconditions of the said instruction.
  668.      */
  669.     @Override
  670.     public void visitDUP(final DUP o) {
  671.         if (stack().peek().getSize() != 1) {
  672.             constraintViolated(o,
  673.                 "Won't DUP type on stack top '" + stack().peek() + "' because it must occupy exactly one slot, not '" + stack().peek().getSize() + "'.");
  674.         }
  675.     }

  677.     /**
  678.      * Ensures the specific preconditions of the said instruction.
  679.      */
  680.     @Override
  681.     public void visitDUP_X1(final DUP_X1 o) {
  682.         if (stack().peek().getSize() != 1) {
  683.             constraintViolated(o, "Type on stack top '" + stack().peek() + "' should occupy exactly one slot, not '" + stack().peek().getSize() + "'.");
  684.         }
  685.         if (stack().peek(1).getSize() != 1) {
  686.             constraintViolated(o,
  687.                 "Type on stack next-to-top '" + stack().peek(1) + "' should occupy exactly one slot, not '" + stack().peek(1).getSize() + "'.");
  688.         }
  689.     }

  691.     /**
  692.      * Ensures the specific preconditions of the said instruction.
  693.      */
  694.     @Override
  695.     public void visitDUP_X2(final DUP_X2 o) {
  696.         if (stack().peek().getSize() != 1) {
  697.             constraintViolated(o, "Stack top type must be of size 1, but is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
  698.         }
  699.         if (stack().peek(1).getSize() == 2) {
  700.             return; // Form 2, okay.
  701.         }
  702.         // stack().peek(1).getSize == 1.
  703.         if (stack().peek(2).getSize() != 1) {
  704.             constraintViolated(o, "If stack top's size is 1 and stack next-to-top's size is 1," + " stack next-to-next-to-top's size must also be 1, but is: '"
  705.                 + stack().peek(2) + "' of size '" + stack().peek(2).getSize() + "'.");
  706.         }
  707.     }

  709.     /**
  710.      * Ensures the specific preconditions of the said instruction.
  711.      */
  712.     @Override
  713.     public void visitDUP2(final DUP2 o) {
  714.         if (stack().peek().getSize() == 2) {
  715.             return; // Form 2, okay.
  716.         }
  717.         // stack().peek().getSize() == 1.
  718.         if (stack().peek(1).getSize() != 1) {
  719.             constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '" + stack().peek(1) + "' of size '"
  720.                 + stack().peek(1).getSize() + "'.");
  721.         }
  722.     }

  724.     /**
  725.      * Ensures the specific preconditions of the said instruction.
  726.      */
  727.     @Override
  728.     public void visitDUP2_X1(final DUP2_X1 o) {
  729.         if (stack().peek().getSize() == 2) {
  730.             if (stack().peek(1).getSize() != 1) {
  731.                 constraintViolated(o, "If stack top's size is 2, then stack next-to-top's size must be 1. But it is '" + stack().peek(1) + "' of size '"
  732.                     + stack().peek(1).getSize() + "'.");
  733.             }
  734.         } else { // stack top is of size 1
  735.             if (stack().peek(1).getSize() != 1) {
  736.                 constraintViolated(o, "If stack top's size is 1, then stack next-to-top's size must also be 1. But it is '" + stack().peek(1) + "' of size '"
  737.                     + stack().peek(1).getSize() + "'.");
  738.             }
  739.             if (stack().peek(2).getSize() != 1) {
  740.                 constraintViolated(o, "If stack top's size is 1, then stack next-to-next-to-top's size must also be 1. But it is '" + stack().peek(2)
  741.                     + "' of size '" + stack().peek(2).getSize() + "'.");
  742.             }
  743.         }
  744.     }

  746.     /**
  747.      * Ensures the specific preconditions of the said instruction.
  748.      */
  749.     @Override
  750.     public void visitDUP2_X2(final DUP2_X2 o) {

  752.         if (stack().peek(0).getSize() == 2) {
  753.             // stack top size is 2, next-to-top's size is 1
  754.             if (stack().peek(1).getSize() == 2 || stack().peek(2).getSize() == 1) {
  755.                 return; // Form 2
  756.             }
  757.             constraintViolated(o, "If stack top's size is 2 and stack-next-to-top's size is 1,"
  758.                 + " then stack next-to-next-to-top's size must also be 1. But it is '" + stack().peek(2) + "' of size '" + stack().peek(2).getSize() + "'.");
  759.         } else if (stack().peek(1).getSize() == 1 && (stack().peek(2).getSize() == 2 || stack().peek(3).getSize() == 1)) {
  760.             return; // Form 1
  761.         }
  762.         constraintViolated(o, "The operand sizes on the stack do not match any of the four forms of usage of this instruction.");
  763.     }

  765.     /**
  766.      * Ensures the specific preconditions of the said instruction.
  767.      */
  768.     @Override
  769.     public void visitF2D(final F2D o) {
  770.         if (stack().peek() != Type.FLOAT) {
  771.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  772.         }
  773.     }

  775.     /**
  776.      * Ensures the specific preconditions of the said instruction.
  777.      */
  778.     @Override
  779.     public void visitF2I(final F2I o) {
  780.         if (stack().peek() != Type.FLOAT) {
  781.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  782.         }
  783.     }

  785.     /**
  786.      * Ensures the specific preconditions of the said instruction.
  787.      */
  788.     @Override
  789.     public void visitF2L(final F2L o) {
  790.         if (stack().peek() != Type.FLOAT) {
  791.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  792.         }
  793.     }

  795.     /**
  796.      * Ensures the specific preconditions of the said instruction.
  797.      */
  798.     @Override
  799.     public void visitFADD(final FADD o) {
  800.         if (stack().peek() != Type.FLOAT) {
  801.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  802.         }
  803.         if (stack().peek(1) != Type.FLOAT) {
  804.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  805.         }
  806.     }

  808.     /**
  809.      * Ensures the specific preconditions of the said instruction.
  810.      */
  811.     @Override
  812.     public void visitFALOAD(final FALOAD o) {
  813.         indexOfInt(o, stack().peek());
  814.         if (stack().peek(1) == Type.NULL) {
  815.             return;
  816.         }
  817.         if (!(stack().peek(1) instanceof ArrayType)) {
  818.             constraintViolated(o, "Stack next-to-top must be of type float[] but is '" + stack().peek(1) + "'.");
  819.         }
  820.         final Type t = ((ArrayType) stack().peek(1)).getBasicType();
  821.         if (t != Type.FLOAT) {
  822.             constraintViolated(o, "Stack next-to-top must be of type float[] but is '" + stack().peek(1) + "'.");
  823.         }
  824.     }

  826.     /**
  827.      * Ensures the specific preconditions of the said instruction.
  828.      */
  829.     @Override
  830.     public void visitFASTORE(final FASTORE o) {
  831.         if (stack().peek() != Type.FLOAT) {
  832.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  833.         }
  834.         indexOfInt(o, stack().peek(1));
  835.         if (stack().peek(2) == Type.NULL) {
  836.             return;
  837.         }
  838.         if (!(stack().peek(2) instanceof ArrayType)) {
  839.             constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '" + stack().peek(2) + "'.");
  840.         }
  841.         final Type t = ((ArrayType) stack().peek(2)).getBasicType();
  842.         if (t != Type.FLOAT) {
  843.             constraintViolated(o, "Stack next-to-next-to-top must be of type float[] but is '" + stack().peek(2) + "'.");
  844.         }
  845.     }

  847.     /**
  848.      * Ensures the specific preconditions of the said instruction.
  849.      */
  850.     @Override
  851.     public void visitFCMPG(final FCMPG o) {
  852.         if (stack().peek() != Type.FLOAT) {
  853.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  854.         }
  855.         if (stack().peek(1) != Type.FLOAT) {
  856.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  857.         }
  858.     }

  860.     /**
  861.      * Ensures the specific preconditions of the said instruction.
  862.      */
  863.     @Override
  864.     public void visitFCMPL(final FCMPL o) {
  865.         if (stack().peek() != Type.FLOAT) {
  866.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  867.         }
  868.         if (stack().peek(1) != Type.FLOAT) {
  869.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  870.         }
  871.     }

  873.     /**
  874.      * Ensures the specific preconditions of the said instruction.
  875.      */
  876.     @Override
  877.     public void visitFCONST(final FCONST o) {
  878.         // nothing to do here.
  879.     }

  881.     /**
  882.      * Ensures the specific preconditions of the said instruction.
  883.      */
  884.     @Override
  885.     public void visitFDIV(final FDIV o) {
  886.         if (stack().peek() != Type.FLOAT) {
  887.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  888.         }
  889.         if (stack().peek(1) != Type.FLOAT) {
  890.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  891.         }
  892.     }

  894.     /**
  895.      * Ensures the general preconditions of a FieldInstruction instance.
  896.      */
  897.     @Override
  898.     public void visitFieldInstruction(final FieldInstruction o) {
  899.         // visitLoadClass(o) has been called before: Every FieldOrMethod
  900.         // implements LoadClass.
  901.         // visitCPInstruction(o) has been called before.
  902.         // A FieldInstruction may be: GETFIELD, GETSTATIC, PUTFIELD, PUTSTATIC
  903.         final Constant c = cpg.getConstant(o.getIndex());
  904.         if (!(c instanceof ConstantFieldref)) {
  905.             constraintViolated(o, "Index '" + o.getIndex() + "' should refer to a CONSTANT_Fieldref_info structure, but refers to '" + c + "'.");
  906.         }
  907.         // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).
  908.         final Type t = o.getType(cpg);
  909.         if (t instanceof ObjectType) {
  910.             final String name = ((ObjectType) t).getClassName();
  911.             final Verifier v = VerifierFactory.getVerifier(name);
  912.             final VerificationResult vr = v.doPass2();
  913.             if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
  914.                 constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
  915.             }
  916.         }
  917.     }

  919.     private Field visitFieldInstructionInternals(final FieldInstruction o) throws ClassNotFoundException {
  920.         final String fieldName = o.getFieldName(cpg);
  921.         final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
  922.         final Field f = jc.findField(fieldName, o.getType(cpg));
  923.         if (f == null) {
  924.             throw new AssertionViolatedException("Field '" + fieldName + "' not found in " + jc.getClassName());
  925.         }
  926.         final Type value = stack().peek();
  927.         final Type t = Type.getType(f.getSignature());
  928.         Type shouldBe = t;
  929.         if (shouldBe == Type.BOOLEAN || shouldBe == Type.BYTE || shouldBe == Type.CHAR || shouldBe == Type.SHORT) {
  930.             shouldBe = Type.INT;
  931.         }
  932.         if (t instanceof ReferenceType) {
  933.             if (value instanceof ReferenceType) {
  934.                 final ReferenceType rValue = (ReferenceType) value;
  935.                 referenceTypeIsInitialized(o, rValue);
  936.                 // TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
  937.                 // using "wider cast object types" created during verification.
  938.                 // Comment it out if you encounter problems. See also the analogon at visitPUTFIELD|visitPUTSTATIC.
  939.                 if (!rValue.isAssignmentCompatibleWith(shouldBe)) {
  940.                     constraintViolated(o, "The stack top type '" + value + "' is not assignment compatible with '" + shouldBe + "'.");
  941.                 }
  942.             } else {
  943.                 constraintViolated(o, "The stack top type '" + value + "' is not of a reference type as expected.");
  944.             }
  945.         } else if (shouldBe != value) {
  946.             constraintViolated(o, "The stack top type '" + value + "' is not of type '" + shouldBe + "' as expected.");
  947.         }
  948.         return f;
  949.     }

  951.     /**
  952.      * Ensures the specific preconditions of the said instruction.
  953.      */
  954.     @Override
  955.     public void visitFLOAD(final FLOAD o) {
  956.         // visitLoadInstruction(LoadInstruction) is called before.

  958.         // Nothing else needs to be done here.
  959.     }

  961.     /**
  962.      * Ensures the specific preconditions of the said instruction.
  963.      */
  964.     @Override
  965.     public void visitFMUL(final FMUL o) {
  966.         if (stack().peek() != Type.FLOAT) {
  967.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  968.         }
  969.         if (stack().peek(1) != Type.FLOAT) {
  970.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  971.         }
  972.     }

  974.     /**
  975.      * Ensures the specific preconditions of the said instruction.
  976.      */
  977.     @Override
  978.     public void visitFNEG(final FNEG o) {
  979.         if (stack().peek() != Type.FLOAT) {
  980.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  981.         }
  982.     }

  984.     /**
  985.      * Ensures the specific preconditions of the said instruction.
  986.      */
  987.     @Override
  988.     public void visitFREM(final FREM o) {
  989.         if (stack().peek() != Type.FLOAT) {
  990.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  991.         }
  992.         if (stack().peek(1) != Type.FLOAT) {
  993.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  994.         }
  995.     }

  997.     /**
  998.      * Ensures the specific preconditions of the said instruction.
  999.      */
  1000.     @Override
  1001.     public void visitFRETURN(final FRETURN o) {
  1002.         if (stack().peek() != Type.FLOAT) {
  1003.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  1004.         }
  1005.     }

  1007.     /**
  1008.      * Ensures the specific preconditions of the said instruction.
  1009.      */
  1010.     @Override
  1011.     public void visitFSTORE(final FSTORE o) {
  1012.         // visitStoreInstruction(StoreInstruction) is called before.

  1014.         // Nothing else needs to be done here.
  1015.     }

  1017.     /**
  1018.      * Ensures the specific preconditions of the said instruction.
  1019.      */
  1020.     @Override
  1021.     public void visitFSUB(final FSUB o) {
  1022.         if (stack().peek() != Type.FLOAT) {
  1023.             constraintViolated(o, "The value at the stack top is not of type 'float', but of type '" + stack().peek() + "'.");
  1024.         }
  1025.         if (stack().peek(1) != Type.FLOAT) {
  1026.             constraintViolated(o, "The value at the stack next-to-top is not of type 'float', but of type '" + stack().peek(1) + "'.");
  1027.         }
  1028.     }

  1030.     /**
  1031.      * Ensures the specific preconditions of the said instruction.
  1032.      */
  1033.     @Override
  1034.     public void visitGETFIELD(final GETFIELD o) {
  1035.         try {
  1036.             final Type objectref = stack().peek();
  1037.             if (!(objectref instanceof ObjectType || objectref == Type.NULL)) {
  1038.                 constraintViolated(o, "Stack top should be an object reference that's not an array reference, but is '" + objectref + "'.");
  1039.             }

  1041.             final String fieldName = o.getFieldName(cpg);

  1043.             final JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
  1044.             final Field f = jc.findField(fieldName, o.getType(cpg));
  1045.             if (f == null) {
  1046.                 throw new AssertionViolatedException("Field '" + fieldName + "' not found in " + jc.getClassName());
  1047.             }

  1049.             if (f.isProtected()) {
  1050.                 final ObjectType classtype = getObjectType(o);
  1051.                 final ObjectType curr = ObjectType.getInstance(mg.getClassName());

  1053.                 if (classtype.equals(curr) || curr.subclassOf(classtype)) {
  1054.                     final Type t = stack().peek();
  1055.                     if (t == Type.NULL) {
  1056.                         return;
  1057.                     }
  1058.                     if (!(t instanceof ObjectType)) {
  1059.                         constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '" + t + "'.");
  1060.                     }
  1061.                     // final ObjectType objreftype = (ObjectType) t;
  1062.                     // if (!(objreftype.equals(curr) || objreftype.subclassOf(curr))) {
  1063.                         // TODO: One day move to Staerk-et-al's "Set of object types" instead of "wider" object types
  1064.                         // created during the verification.
  1065.                         // "Wider" object types don't allow us to check for things like that below.
  1066.                         // constraintViolated(o, "The referenced field has the ACC_PROTECTED modifier, "+
  1067.                         // "and it's a member of the current class or a superclass of the current class."+
  1068.                         // " However, the referenced object type '"+stack().peek()+
  1069.                         // "' is not the current class or a subclass of the current class.");
  1070.                     //}
  1071.                 }
  1072.             }

  1074.             // TODO: Could go into Pass 3a.
  1075.             if (f.isStatic()) {
  1076.                 constraintViolated(o, "Referenced field '" + f + "' is static which it shouldn't be.");
  1077.             }

  1079.         } catch (final ClassNotFoundException e) {
  1080.             // FIXME: maybe not the best way to handle this
  1081.             throw new AssertionViolatedException("Missing class: " + e, e);
  1082.         }
  1083.     }

  1085.     /**
  1086.      * Ensures the specific preconditions of the said instruction.
  1087.      */
  1088.     @Override
  1089.     public void visitGETSTATIC(final GETSTATIC o) {
  1090.         // Field must be static: see Pass 3a.
  1091.     }

  1093.     /**
  1094.      * Ensures the specific preconditions of the said instruction.
  1095.      */
  1096.     @Override
  1097.     public void visitGOTO(final GOTO o) {
  1098.         // nothing to do here.
  1099.     }

  1101.     /**
  1102.      * Ensures the specific preconditions of the said instruction.
  1103.      */
  1104.     @Override
  1105.     public void visitGOTO_W(final GOTO_W o) {
  1106.         // nothing to do here.
  1107.     }

  1109.     /**
  1110.      * Ensures the specific preconditions of the said instruction.
  1111.      */
  1112.     @Override
  1113.     public void visitI2B(final I2B o) {
  1114.         if (stack().peek() != Type.INT) {
  1115.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1116.         }
  1117.     }

  1119.     /**
  1120.      * Ensures the specific preconditions of the said instruction.
  1121.      */
  1122.     @Override
  1123.     public void visitI2C(final I2C o) {
  1124.         if (stack().peek() != Type.INT) {
  1125.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1126.         }
  1127.     }

  1129.     /**
  1130.      * Ensures the specific preconditions of the said instruction.
  1131.      */
  1132.     @Override
  1133.     public void visitI2D(final I2D o) {
  1134.         if (stack().peek() != Type.INT) {
  1135.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1136.         }
  1137.     }

  1139.     /**
  1140.      * Ensures the specific preconditions of the said instruction.
  1141.      */
  1142.     @Override
  1143.     public void visitI2F(final I2F o) {
  1144.         if (stack().peek() != Type.INT) {
  1145.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1146.         }
  1147.     }

  1149.     /**
  1150.      * Ensures the specific preconditions of the said instruction.
  1151.      */
  1152.     @Override
  1153.     public void visitI2L(final I2L o) {
  1154.         if (stack().peek() != Type.INT) {
  1155.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1156.         }
  1157.     }

  1159.     /**
  1160.      * Ensures the specific preconditions of the said instruction.
  1161.      */
  1162.     @Override
  1163.     public void visitI2S(final I2S o) {
  1164.         if (stack().peek() != Type.INT) {
  1165.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1166.         }
  1167.     }

  1169.     /**
  1170.      * Ensures the specific preconditions of the said instruction.
  1171.      */
  1172.     @Override
  1173.     public void visitIADD(final IADD o) {
  1174.         if (stack().peek() != Type.INT) {
  1175.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1176.         }
  1177.         if (stack().peek(1) != Type.INT) {
  1178.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1179.         }
  1180.     }

  1182.     /**
  1183.      * Ensures the specific preconditions of the said instruction.
  1184.      */
  1185.     @Override
  1186.     public void visitIALOAD(final IALOAD o) {
  1187.         indexOfInt(o, stack().peek());
  1188.         if (stack().peek(1) == Type.NULL) {
  1189.             return;
  1190.         }
  1191.         if (!(stack().peek(1) instanceof ArrayType)) {
  1192.             constraintViolated(o, "Stack next-to-top must be of type int[] but is '" + stack().peek(1) + "'.");
  1193.         }
  1194.         final Type t = ((ArrayType) stack().peek(1)).getBasicType();
  1195.         if (t != Type.INT) {
  1196.             constraintViolated(o, "Stack next-to-top must be of type int[] but is '" + stack().peek(1) + "'.");
  1197.         }
  1198.     }

  1200.     /**
  1201.      * Ensures the specific preconditions of the said instruction.
  1202.      */
  1203.     @Override
  1204.     public void visitIAND(final IAND o) {
  1205.         if (stack().peek() != Type.INT) {
  1206.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1207.         }
  1208.         if (stack().peek(1) != Type.INT) {
  1209.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1210.         }
  1211.     }

  1213.     /**
  1214.      * Ensures the specific preconditions of the said instruction.
  1215.      */
  1216.     @Override
  1217.     public void visitIASTORE(final IASTORE o) {
  1218.         if (stack().peek() != Type.INT) {
  1219.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1220.         }
  1221.         indexOfInt(o, stack().peek(1));
  1222.         if (stack().peek(2) == Type.NULL) {
  1223.             return;
  1224.         }
  1225.         if (!(stack().peek(2) instanceof ArrayType)) {
  1226.             constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '" + stack().peek(2) + "'.");
  1227.         }
  1228.         final Type t = ((ArrayType) stack().peek(2)).getBasicType();
  1229.         if (t != Type.INT) {
  1230.             constraintViolated(o, "Stack next-to-next-to-top must be of type int[] but is '" + stack().peek(2) + "'.");
  1231.         }
  1232.     }

  1234.     /**
  1235.      * Ensures the specific preconditions of the said instruction.
  1236.      */
  1237.     @Override
  1238.     public void visitICONST(final ICONST o) {
  1239.         // nothing to do here.
  1240.     }

  1242.     /**
  1243.      * Ensures the specific preconditions of the said instruction.
  1244.      */
  1245.     @Override
  1246.     public void visitIDIV(final IDIV o) {
  1247.         if (stack().peek() != Type.INT) {
  1248.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1249.         }
  1250.         if (stack().peek(1) != Type.INT) {
  1251.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1252.         }
  1253.     }

  1255.     /**
  1256.      * Ensures the specific preconditions of the said instruction.
  1257.      */
  1258.     @Override
  1259.     public void visitIF_ACMPEQ(final IF_ACMPEQ o) {
  1260.         if (!(stack().peek() instanceof ReferenceType)) {
  1261.             constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
  1262.         }
  1263.         // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );

  1265.         if (!(stack().peek(1) instanceof ReferenceType)) {
  1266.             constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '" + stack().peek(1) + "'.");
  1267.         }
  1268.         // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );

  1270.     }

  1272.     /**
  1273.      * Ensures the specific preconditions of the said instruction.
  1274.      */
  1275.     @Override
  1276.     public void visitIF_ACMPNE(final IF_ACMPNE o) {
  1277.         if (!(stack().peek() instanceof ReferenceType)) {
  1278.             constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
  1279.             // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
  1280.         }
  1281.         if (!(stack().peek(1) instanceof ReferenceType)) {
  1282.             constraintViolated(o, "The value at the stack next-to-top is not of a ReferenceType, but of type '" + stack().peek(1) + "'.");
  1283.             // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek(1)) );
  1284.         }
  1285.     }

  1287.     /**
  1288.      * Ensures the specific preconditions of the said instruction.
  1289.      */
  1290.     @Override
  1291.     public void visitIF_ICMPEQ(final IF_ICMPEQ o) {
  1292.         if (stack().peek() != Type.INT) {
  1293.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1294.         }
  1295.         if (stack().peek(1) != Type.INT) {
  1296.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1297.         }
  1298.     }

  1300.     /**
  1301.      * Ensures the specific preconditions of the said instruction.
  1302.      */
  1303.     @Override
  1304.     public void visitIF_ICMPGE(final IF_ICMPGE o) {
  1305.         if (stack().peek() != Type.INT) {
  1306.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1307.         }
  1308.         if (stack().peek(1) != Type.INT) {
  1309.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1310.         }
  1311.     }

  1313.     /**
  1314.      * Ensures the specific preconditions of the said instruction.
  1315.      */
  1316.     @Override
  1317.     public void visitIF_ICMPGT(final IF_ICMPGT o) {
  1318.         if (stack().peek() != Type.INT) {
  1319.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1320.         }
  1321.         if (stack().peek(1) != Type.INT) {
  1322.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1323.         }
  1324.     }

  1326.     /**
  1327.      * Ensures the specific preconditions of the said instruction.
  1328.      */
  1329.     @Override
  1330.     public void visitIF_ICMPLE(final IF_ICMPLE o) {
  1331.         if (stack().peek() != Type.INT) {
  1332.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1333.         }
  1334.         if (stack().peek(1) != Type.INT) {
  1335.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1336.         }
  1337.     }

  1339.     /**
  1340.      * Ensures the specific preconditions of the said instruction.
  1341.      */
  1342.     @Override
  1343.     public void visitIF_ICMPLT(final IF_ICMPLT o) {
  1344.         if (stack().peek() != Type.INT) {
  1345.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1346.         }
  1347.         if (stack().peek(1) != Type.INT) {
  1348.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1349.         }
  1350.     }

  1352.     /**
  1353.      * Ensures the specific preconditions of the said instruction.
  1354.      */
  1355.     @Override
  1356.     public void visitIF_ICMPNE(final IF_ICMPNE o) {
  1357.         if (stack().peek() != Type.INT) {
  1358.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1359.         }
  1360.         if (stack().peek(1) != Type.INT) {
  1361.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1362.         }
  1363.     }

  1365.     /**
  1366.      * Ensures the specific preconditions of the said instruction.
  1367.      */
  1368.     @Override
  1369.     public void visitIFEQ(final IFEQ o) {
  1370.         if (stack().peek() != Type.INT) {
  1371.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1372.         }
  1373.     }

  1375.     /**
  1376.      * Ensures the specific preconditions of the said instruction.
  1377.      */
  1378.     @Override
  1379.     public void visitIFGE(final IFGE o) {
  1380.         if (stack().peek() != Type.INT) {
  1381.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1382.         }
  1383.     }

  1385.     /**
  1386.      * Ensures the specific preconditions of the said instruction.
  1387.      */
  1388.     @Override
  1389.     public void visitIFGT(final IFGT o) {
  1390.         if (stack().peek() != Type.INT) {
  1391.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1392.         }
  1393.     }

  1395.     /**
  1396.      * Ensures the specific preconditions of the said instruction.
  1397.      */
  1398.     @Override
  1399.     public void visitIFLE(final IFLE o) {
  1400.         if (stack().peek() != Type.INT) {
  1401.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1402.         }
  1403.     }

  1405.     /**
  1406.      * Ensures the specific preconditions of the said instruction.
  1407.      */
  1408.     @Override
  1409.     public void visitIFLT(final IFLT o) {
  1410.         if (stack().peek() != Type.INT) {
  1411.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1412.         }
  1413.     }

  1415.     /**
  1416.      * Ensures the specific preconditions of the said instruction.
  1417.      */
  1418.     @Override
  1419.     public void visitIFNE(final IFNE o) {
  1420.         if (stack().peek() != Type.INT) {
  1421.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1422.         }
  1423.     }

  1425.     /**
  1426.      * Ensures the specific preconditions of the said instruction.
  1427.      */
  1428.     @Override
  1429.     public void visitIFNONNULL(final IFNONNULL o) {
  1430.         if (!(stack().peek() instanceof ReferenceType)) {
  1431.             constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
  1432.         }
  1433.         referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
  1434.     }

  1436.     /**
  1437.      * Ensures the specific preconditions of the said instruction.
  1438.      */
  1439.     @Override
  1440.     public void visitIFNULL(final IFNULL o) {
  1441.         if (!(stack().peek() instanceof ReferenceType)) {
  1442.             constraintViolated(o, "The value at the stack top is not of a ReferenceType, but of type '" + stack().peek() + "'.");
  1443.         }
  1444.         referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
  1445.     }

  1447.     /**
  1448.      * Ensures the specific preconditions of the said instruction.
  1449.      */
  1450.     @Override
  1451.     public void visitIINC(final IINC o) {
  1452.         // Mhhh. In BCEL, at this time "IINC" is not a LocalVariableInstruction.
  1453.         if (locals().maxLocals() <= (o.getType(cpg).getSize() == 1 ? o.getIndex() : o.getIndex() + 1)) {
  1454.             constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
  1455.         }

  1457.         indexOfInt(o, locals().get(o.getIndex()));
  1458.     }

  1460.     /**
  1461.      * Ensures the specific preconditions of the said instruction.
  1462.      */
  1463.     @Override
  1464.     public void visitILOAD(final ILOAD o) {
  1465.         // All done by visitLocalVariableInstruction(), visitLoadInstruction()
  1466.     }

  1468.     /**
  1469.      * Ensures the specific preconditions of the said instruction.
  1470.      */
  1471.     @Override
  1472.     public void visitIMPDEP1(final IMPDEP1 o) {
  1473.         throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP1.");
  1474.     }

  1476.     /**
  1477.      * Ensures the specific preconditions of the said instruction.
  1478.      */
  1479.     @Override
  1480.     public void visitIMPDEP2(final IMPDEP2 o) {
  1481.         throw new AssertionViolatedException("In this JustIce verification pass there should not occur an illegal instruction such as IMPDEP2.");
  1482.     }

  1484.     /**
  1485.      * Ensures the specific preconditions of the said instruction.
  1486.      */
  1487.     @Override
  1488.     public void visitIMUL(final IMUL o) {
  1489.         if (stack().peek() != Type.INT) {
  1490.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1491.         }
  1492.         if (stack().peek(1) != Type.INT) {
  1493.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1494.         }
  1495.     }

  1497.     /**
  1498.      * Ensures the specific preconditions of the said instruction.
  1499.      */
  1500.     @Override
  1501.     public void visitINEG(final INEG o) {
  1502.         if (stack().peek() != Type.INT) {
  1503.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1504.         }
  1505.     }

  1507.     /**
  1508.      * Ensures the specific preconditions of the said instruction.
  1509.      */
  1510.     @Override
  1511.     public void visitINSTANCEOF(final INSTANCEOF o) {
  1512.         // The objectref must be of type reference.
  1513.         final Type objectref = stack().peek(0);
  1514.         if (!(objectref instanceof ReferenceType)) {
  1515.             constraintViolated(o, "The 'objectref' is not of a ReferenceType but of type " + objectref + ".");
  1516.         }
  1517.         // else{
  1518.         // referenceTypeIsInitialized(o, (ReferenceType) objectref);
  1519.         // }
  1520.         // The unsigned indexbyte1 and indexbyte2 are used to construct an index into the runtime constant pool of the
  1521.         // current class (�3.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The runtime constant
  1522.         // pool item at the index must be a symbolic reference to a class, array, or interface type.
  1523.         final Constant c = cpg.getConstant(o.getIndex());
  1524.         if (!(c instanceof ConstantClass)) {
  1525.             constraintViolated(o, "The Constant at 'index' is not a ConstantClass, but '" + c + "'.");
  1526.         }
  1527.     }

  1529.     /**
  1530.      * Ensures the specific preconditions of the said instruction.
  1531.      *
  1532.      * @since 6.0
  1533.      */
  1534.     @Override
  1535.     public void visitINVOKEDYNAMIC(final INVOKEDYNAMIC o) {
  1536.         throw new UnsupportedOperationException("INVOKEDYNAMIC instruction is not supported at this time");
  1537.     }

  1539.     /**
  1540.      * Ensures the general preconditions of an InvokeInstruction instance.
  1541.      */
  1542.     @Override
  1543.     public void visitInvokeInstruction(final InvokeInstruction o) {
  1544.         // visitLoadClass(o) has been called before: Every FieldOrMethod
  1545.         // implements LoadClass.
  1546.         // visitCPInstruction(o) has been called before.
  1547.         // TODO
  1548.     }

  1550.     /**
  1551.      * Ensures the specific preconditions of the said instruction.
  1552.      */
  1553.     @Override
  1554.     public void visitINVOKEINTERFACE(final INVOKEINTERFACE o) {
  1555.         // Method is not native, otherwise pass 3 would not happen.

  1557.         final int count = o.getCount();
  1558.         if (count == 0) {
  1559.             constraintViolated(o, "The 'count' argument must not be 0.");
  1560.         }
  1561.         // It is a ConstantInterfaceMethodref, Pass 3a made it sure.
  1562.         // TODO: Do we want to do anything with it?
  1563.         // ConstantInterfaceMethodref cimr = (ConstantInterfaceMethodref) (cpg.getConstant(o.getIndex()));

  1565.         // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).

  1567.         final Type t = o.getType(cpg);
  1568.         if (t instanceof ObjectType) {
  1569.             final String name = ((ObjectType) t).getClassName();
  1570.             final Verifier v = VerifierFactory.getVerifier(name);
  1571.             final VerificationResult vr = v.doPass2();
  1572.             if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
  1573.                 constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
  1574.             }
  1575.         }

  1577.         final Type[] argTypes = o.getArgumentTypes(cpg);
  1578.         final int argCount = argTypes.length;

  1580.         for (int i = argCount - 1; i >= 0; i--) {
  1581.             final Type fromStack = stack().peek(argCount - 1 - i); // 0 to argCount - 1
  1582.             Type fromDesc = argTypes[i];
  1583.             if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
  1584.                 fromDesc = Type.INT;
  1585.             }
  1586.             if (!fromStack.equals(fromDesc)) {
  1587.                 if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
  1588.                     final ReferenceType rFromStack = (ReferenceType) fromStack;
  1589.                     // ReferenceType rFromDesc = (ReferenceType) fromDesc;
  1590.                     // TODO: This can only be checked when using Staerk-et-al's "set of object types"
  1591.                     // instead of a "wider cast object type" created during verification.
  1592.                     // if ( ! rFromStack.isAssignmentCompatibleWith(rFromDesc) ) {
  1593.                     // constraintViolated(o, "Expecting a '"+fromDesc+"' but found a '"+fromStack+
  1594.                     // "' on the stack (which is not assignment compatible).");
  1595.                     // }
  1596.                     referenceTypeIsInitialized(o, rFromStack);
  1597.                 } else {
  1598.                     constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
  1599.                 }
  1600.             }
  1601.         }

  1603.         Type objRef = stack().peek(argCount);
  1604.         if (objRef == Type.NULL) {
  1605.             return;
  1606.         }
  1607.         if (!(objRef instanceof ReferenceType)) {
  1608.             constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objRef + "'.");
  1609.         }
  1610.         referenceTypeIsInitialized(o, (ReferenceType) objRef);
  1611.         if (!(objRef instanceof ObjectType)) {
  1612.             if (!(objRef instanceof ArrayType)) { // could be a ReturnaddressType
  1613.                 constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objRef + "'.");
  1614.             } else {
  1615.                 objRef = GENERIC_ARRAY;
  1616.             }
  1617.         }

  1619.         // String objRefClassName = ((ObjectType) objRef).getClassName();
  1620.         // String theInterface = o.getClassName(cpg);
  1621.         // TODO: This can only be checked if we're using Staerk-et-al's "set of object types"
  1622.         // instead of "wider cast object types" generated during verification.
  1623.         // if ( ! Repository.implementationOf(objRefClassName, theInterface) ) {
  1624.         // constraintViolated(o, "The 'objRef' item '" + objRef + "' does not implement '" + theInterface + "' as expected.");
  1625.         // }

  1627.         int countedCount = 1; // 1 for the objectref
  1628.         for (int i = 0; i < argCount; i++) {
  1629.             countedCount += argTypes[i].getSize();
  1630.         }
  1631.         if (count != countedCount) {
  1632.             constraintViolated(o, "The 'count' argument should probably read '" + countedCount + "' but is '" + count + "'.");
  1633.         }
  1634.     }

  1636.     private int visitInvokeInternals(final InvokeInstruction o) throws ClassNotFoundException {
  1637.         final Type t = o.getType(cpg);
  1638.         if (t instanceof ObjectType) {
  1639.             final String name = ((ObjectType) t).getClassName();
  1640.             final Verifier v = VerifierFactory.getVerifier(name);
  1641.             final VerificationResult vr = v.doPass2();
  1642.             if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
  1643.                 constraintViolated(o, "Class '" + name + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
  1644.             }
  1645.         }

  1647.         final Type[] argtypes = o.getArgumentTypes(cpg);
  1648.         final int nargs = argtypes.length;

  1650.         for (int i = nargs - 1; i >= 0; i--) {
  1651.             final Type fromStack = stack().peek(nargs - 1 - i); // 0 to nargs-1
  1652.             Type fromDesc = argtypes[i];
  1653.             if (fromDesc == Type.BOOLEAN || fromDesc == Type.BYTE || fromDesc == Type.CHAR || fromDesc == Type.SHORT) {
  1654.                 fromDesc = Type.INT;
  1655.             }
  1656.             if (!fromStack.equals(fromDesc)) {
  1657.                 if (fromStack instanceof ReferenceType && fromDesc instanceof ReferenceType) {
  1658.                     final ReferenceType rFromStack = (ReferenceType) fromStack;
  1659.                     final ReferenceType rFromDesc = (ReferenceType) fromDesc;
  1660.                     // TODO: This can possibly only be checked when using Staerk-et-al's "set of object types" instead
  1661.                     // of a single "wider cast object type" created during verification.
  1662.                     if (!rFromStack.isAssignmentCompatibleWith(rFromDesc)) {
  1663.                         constraintViolated(o,
  1664.                             "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack (which is not assignment compatible).");
  1665.                     }
  1666.                     referenceTypeIsInitialized(o, rFromStack);
  1667.                 } else {
  1668.                     constraintViolated(o, "Expecting a '" + fromDesc + "' but found a '" + fromStack + "' on the stack.");
  1669.                 }
  1670.             }
  1671.         }
  1672.         return nargs;
  1673.     }

  1675.     /**
  1676.      * Ensures the specific preconditions of the said instruction.
  1677.      */
  1678.     @Override
  1679.     public void visitINVOKESPECIAL(final INVOKESPECIAL o) {
  1680.         try {
  1681.             // Don't init an object twice.
  1682.             if (o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME) && !(stack().peek(o.getArgumentTypes(cpg).length) instanceof UninitializedObjectType)) {
  1683.                 constraintViolated(o,
  1684.                     "Possibly initializing object twice."
  1685.                         + " A valid instruction sequence must not have an uninitialized object on the operand stack or in a local variable"
  1686.                         + " during a backwards branch, or in a local variable in code protected by an exception handler."
  1687.                         + " Please see The Java Virtual Machine Specification, Second Edition, 4.9.4 (pages 147 and 148) for details.");
  1688.             }

  1690.             // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).

  1692.             final int nargs = visitInvokeInternals(o);
  1693.             Type objref = stack().peek(nargs);
  1694.             if (objref == Type.NULL) {
  1695.                 return;
  1696.             }
  1697.             if (!(objref instanceof ReferenceType)) {
  1698.                 constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
  1699.             }
  1700.             String objRefClassName = null;
  1701.             if (!o.getMethodName(cpg).equals(Const.CONSTRUCTOR_NAME)) {
  1702.                 referenceTypeIsInitialized(o, (ReferenceType) objref);
  1703.                 if (!(objref instanceof ObjectType)) {
  1704.                     if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
  1705.                         constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
  1706.                     } else {
  1707.                         objref = GENERIC_ARRAY;
  1708.                     }
  1709.                 }

  1711.                 objRefClassName = ((ObjectType) objref).getClassName();
  1712.             } else {
  1713.                 if (!(objref instanceof UninitializedObjectType)) {
  1714.                     constraintViolated(o, "Expecting an UninitializedObjectType as 'objectref' on the stack, not a '" + objref
  1715.                         + "'. Otherwise, you couldn't invoke a method since an array has no methods (not to speak of a return address).");
  1716.                 }
  1717.                 objRefClassName = ((UninitializedObjectType) objref).getInitialized().getClassName();
  1718.             }

  1720.             final String theClass = o.getClassName(cpg);
  1721.             if (!Repository.instanceOf(objRefClassName, theClass)) {
  1722.                 constraintViolated(o, "The 'objref' item '" + objref + "' does not implement '" + theClass + "' as expected.");
  1723.             }

  1725.         } catch (final ClassNotFoundException e) {
  1726.             // FIXME: maybe not the best way to handle this
  1727.             throw new AssertionViolatedException("Missing class: " + e, e);
  1728.         }
  1729.     }

  1731.     /**
  1732.      * Ensures the specific preconditions of the said instruction.
  1733.      */
  1734.     @Override
  1735.     public void visitINVOKESTATIC(final INVOKESTATIC o) {
  1736.         try {
  1737.             // Method is not native, otherwise pass 3 would not happen.
  1738.             visitInvokeInternals(o);
  1739.         } catch (final ClassNotFoundException e) {
  1740.             // FIXME: maybe not the best way to handle this
  1741.             throw new AssertionViolatedException("Missing class: " + e, e);
  1742.         }
  1743.     }

  1745.     /**
  1746.      * Ensures the specific preconditions of the said instruction.
  1747.      */
  1748.     @Override
  1749.     public void visitINVOKEVIRTUAL(final INVOKEVIRTUAL o) {
  1750.         try {
  1751.             // the o.getClassType(cpg) type has passed pass 2; see visitLoadClass(o).

  1753.             final int nargs = visitInvokeInternals(o);
  1754.             Type objref = stack().peek(nargs);
  1755.             if (objref == Type.NULL) {
  1756.                 return;
  1757.             }
  1758.             if (!(objref instanceof ReferenceType)) {
  1759.                 constraintViolated(o, "Expecting a reference type as 'objectref' on the stack, not a '" + objref + "'.");
  1760.             }
  1761.             referenceTypeIsInitialized(o, (ReferenceType) objref);
  1762.             if (!(objref instanceof ObjectType)) {
  1763.                 if (!(objref instanceof ArrayType)) { // could be a ReturnaddressType
  1764.                     constraintViolated(o, "Expecting an ObjectType as 'objectref' on the stack, not a '" + objref + "'.");
  1765.                 } else {
  1766.                     objref = GENERIC_ARRAY;
  1767.                 }
  1768.             }

  1770.             final String objRefClassName = ((ObjectType) objref).getClassName();

  1772.             final String theClass = o.getClassName(cpg);

  1774.             if (objref != GENERIC_ARRAY && !Repository.instanceOf(objRefClassName, theClass)) {
  1775.                 constraintViolated(o, "The 'objref' item '" + objref + "' does not implement '" + theClass + "' as expected.");
  1776.             }
  1777.         } catch (final ClassNotFoundException e) {
  1778.             // FIXME: maybe not the best way to handle this
  1779.             throw new AssertionViolatedException("Missing class: " + e, e);
  1780.         }
  1781.     }

  1783.     /**
  1784.      * Ensures the specific preconditions of the said instruction.
  1785.      */
  1786.     @Override
  1787.     public void visitIOR(final IOR o) {
  1788.         if (stack().peek() != Type.INT) {
  1789.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1790.         }
  1791.         if (stack().peek(1) != Type.INT) {
  1792.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1793.         }
  1794.     }

  1796.     /**
  1797.      * Ensures the specific preconditions of the said instruction.
  1798.      */
  1799.     @Override
  1800.     public void visitIREM(final IREM o) {
  1801.         if (stack().peek() != Type.INT) {
  1802.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1803.         }
  1804.         if (stack().peek(1) != Type.INT) {
  1805.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1806.         }
  1807.     }

  1809.     /**
  1810.      * Ensures the specific preconditions of the said instruction.
  1811.      */
  1812.     @Override
  1813.     public void visitIRETURN(final IRETURN o) {
  1814.         if (stack().peek() != Type.INT) {
  1815.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1816.         }
  1817.     }

  1819.     /**
  1820.      * Ensures the specific preconditions of the said instruction.
  1821.      */
  1822.     @Override
  1823.     public void visitISHL(final ISHL o) {
  1824.         if (stack().peek() != Type.INT) {
  1825.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1826.         }
  1827.         if (stack().peek(1) != Type.INT) {
  1828.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1829.         }
  1830.     }

  1832.     /**
  1833.      * Ensures the specific preconditions of the said instruction.
  1834.      */
  1835.     @Override
  1836.     public void visitISHR(final ISHR o) {
  1837.         if (stack().peek() != Type.INT) {
  1838.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1839.         }
  1840.         if (stack().peek(1) != Type.INT) {
  1841.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1842.         }
  1843.     }

  1845.     /**
  1846.      * Ensures the specific preconditions of the said instruction.
  1847.      */
  1848.     @Override
  1849.     public void visitISTORE(final ISTORE o) {
  1850.         // visitStoreInstruction(StoreInstruction) is called before.

  1852.         // Nothing else needs to be done here.
  1853.     }

  1855.     /**
  1856.      * Ensures the specific preconditions of the said instruction.
  1857.      */
  1858.     @Override
  1859.     public void visitISUB(final ISUB o) {
  1860.         if (stack().peek() != Type.INT) {
  1861.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1862.         }
  1863.         if (stack().peek(1) != Type.INT) {
  1864.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1865.         }
  1866.     }

  1868.     /**
  1869.      * Ensures the specific preconditions of the said instruction.
  1870.      */
  1871.     @Override
  1872.     public void visitIUSHR(final IUSHR o) {
  1873.         if (stack().peek() != Type.INT) {
  1874.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1875.         }
  1876.         if (stack().peek(1) != Type.INT) {
  1877.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1878.         }
  1879.     }

  1881.     /**
  1882.      * Ensures the specific preconditions of the said instruction.
  1883.      */
  1884.     @Override
  1885.     public void visitIXOR(final IXOR o) {
  1886.         if (stack().peek() != Type.INT) {
  1887.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  1888.         }
  1889.         if (stack().peek(1) != Type.INT) {
  1890.             constraintViolated(o, "The value at the stack next-to-top is not of type 'int', but of type '" + stack().peek(1) + "'.");
  1891.         }
  1892.     }

  1894.     /**
  1895.      * Ensures the specific preconditions of the said instruction.
  1896.      */
  1897.     @Override
  1898.     public void visitJSR(final JSR o) {
  1899.         // nothing to do here.
  1900.     }

  1902.     /**
  1903.      * Ensures the specific preconditions of the said instruction.
  1904.      */
  1905.     @Override
  1906.     public void visitJSR_W(final JSR_W o) {
  1907.         // nothing to do here.
  1908.     }

  1910.     /**
  1911.      * Ensures the specific preconditions of the said instruction.
  1912.      */
  1913.     @Override
  1914.     public void visitL2D(final L2D o) {
  1915.         if (stack().peek() != Type.LONG) {
  1916.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  1917.         }
  1918.     }

  1920.     /**
  1921.      * Ensures the specific preconditions of the said instruction.
  1922.      */
  1923.     @Override
  1924.     public void visitL2F(final L2F o) {
  1925.         if (stack().peek() != Type.LONG) {
  1926.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  1927.         }
  1928.     }

  1930.     /**
  1931.      * Ensures the specific preconditions of the said instruction.
  1932.      */
  1933.     @Override
  1934.     public void visitL2I(final L2I o) {
  1935.         if (stack().peek() != Type.LONG) {
  1936.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  1937.         }
  1938.     }

  1940.     /**
  1941.      * Ensures the specific preconditions of the said instruction.
  1942.      */
  1943.     @Override
  1944.     public void visitLADD(final LADD o) {
  1945.         if (stack().peek() != Type.LONG) {
  1946.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  1947.         }
  1948.         if (stack().peek(1) != Type.LONG) {
  1949.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  1950.         }
  1951.     }

  1953.     /**
  1954.      * Ensures the specific preconditions of the said instruction.
  1955.      */
  1956.     @Override
  1957.     public void visitLALOAD(final LALOAD o) {
  1958.         indexOfInt(o, stack().peek());
  1959.         if (stack().peek(1) == Type.NULL) {
  1960.             return;
  1961.         }
  1962.         if (!(stack().peek(1) instanceof ArrayType)) {
  1963.             constraintViolated(o, "Stack next-to-top must be of type long[] but is '" + stack().peek(1) + "'.");
  1964.         }
  1965.         final Type t = ((ArrayType) stack().peek(1)).getBasicType();
  1966.         if (t != Type.LONG) {
  1967.             constraintViolated(o, "Stack next-to-top must be of type long[] but is '" + stack().peek(1) + "'.");
  1968.         }
  1969.     }

  1971.     /**
  1972.      * Ensures the specific preconditions of the said instruction.
  1973.      */
  1974.     @Override
  1975.     public void visitLAND(final LAND o) {
  1976.         if (stack().peek() != Type.LONG) {
  1977.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  1978.         }
  1979.         if (stack().peek(1) != Type.LONG) {
  1980.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  1981.         }
  1982.     }

  1984.     /**
  1985.      * Ensures the specific preconditions of the said instruction.
  1986.      */
  1987.     @Override
  1988.     public void visitLASTORE(final LASTORE o) {
  1989.         if (stack().peek() != Type.LONG) {
  1990.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  1991.         }
  1992.         indexOfInt(o, stack().peek(1));
  1993.         if (stack().peek(2) == Type.NULL) {
  1994.             return;
  1995.         }
  1996.         if (!(stack().peek(2) instanceof ArrayType)) {
  1997.             constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '" + stack().peek(2) + "'.");
  1998.         }
  1999.         final Type t = ((ArrayType) stack().peek(2)).getBasicType();
  2000.         if (t != Type.LONG) {
  2001.             constraintViolated(o, "Stack next-to-next-to-top must be of type long[] but is '" + stack().peek(2) + "'.");
  2002.         }
  2003.     }

  2005.     /**
  2006.      * Ensures the specific preconditions of the said instruction.
  2007.      */
  2008.     @Override
  2009.     public void visitLCMP(final LCMP o) {
  2010.         if (stack().peek() != Type.LONG) {
  2011.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2012.         }
  2013.         if (stack().peek(1) != Type.LONG) {
  2014.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2015.         }
  2016.     }

  2018.     /**
  2019.      * Ensures the specific preconditions of the said instruction.
  2020.      */
  2021.     @Override
  2022.     public void visitLCONST(final LCONST o) {
  2023.         // Nothing to do here.
  2024.     }

  2026.     /**
  2027.      * Ensures the specific preconditions of the said instruction.
  2028.      */
  2029.     @Override
  2030.     public void visitLDC(final LDC o) {
  2031.         // visitCPInstruction is called first.

  2033.         final Constant c = cpg.getConstant(o.getIndex());
  2034.         if (!(c instanceof ConstantInteger
  2035.                 || c instanceof ConstantFloat
  2036.                 || c instanceof ConstantString
  2037.                 || c instanceof ConstantClass
  2038.                 || c instanceof ConstantDynamic)) {
  2039.             constraintViolated(o,
  2040.                 "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float, a CONSTANT_String, a CONSTANT_Class, or a CONSTANT_Dynamic but is '"
  2041.                         + c + "'.");
  2042.         }
  2043.     }

  2045.     /**
  2046.      * Ensures the specific preconditions of the said instruction.
  2047.      */
  2048.     public void visitLDC_W(final LDC_W o) {
  2049.         // visitCPInstruction is called first.

  2051.         final Constant c = cpg.getConstant(o.getIndex());
  2052.         if (!(c instanceof ConstantInteger || c instanceof ConstantFloat || c instanceof ConstantString || c instanceof ConstantClass)) {
  2053.             constraintViolated(o,
  2054.                 "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float, a CONSTANT_String or a CONSTANT_Class, but is '" + c + "'.");
  2055.         }
  2056.     }

  2058.     /**
  2059.      * Ensures the specific preconditions of the said instruction.
  2060.      */
  2061.     @Override
  2062.     public void visitLDC2_W(final LDC2_W o) {
  2063.         // visitCPInstruction is called first.

  2065.         final Constant c = cpg.getConstant(o.getIndex());
  2066.         if (!(c instanceof ConstantLong || c instanceof ConstantDouble)) {
  2067.             constraintViolated(o, "Referenced constant should be a CONSTANT_Integer, a CONSTANT_Float or a CONSTANT_String, but is '" + c + "'.");
  2068.         }
  2069.     }

  2071.     /**
  2072.      * Ensures the specific preconditions of the said instruction.
  2073.      */
  2074.     @Override
  2075.     public void visitLDIV(final LDIV o) {
  2076.         if (stack().peek() != Type.LONG) {
  2077.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2078.         }
  2079.         if (stack().peek(1) != Type.LONG) {
  2080.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2081.         }
  2082.     }

  2084.     /**
  2085.      * Ensures the specific preconditions of the said instruction.
  2086.      */
  2087.     @Override
  2088.     public void visitLLOAD(final LLOAD o) {
  2089.         // visitLoadInstruction(LoadInstruction) is called before.

  2091.         // Nothing else needs to be done here.
  2092.     }

  2094.     /**
  2095.      * Ensures the specific preconditions of the said instruction.
  2096.      */
  2097.     @Override
  2098.     public void visitLMUL(final LMUL o) {
  2099.         if (stack().peek() != Type.LONG) {
  2100.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2101.         }
  2102.         if (stack().peek(1) != Type.LONG) {
  2103.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2104.         }
  2105.     }

  2107.     /**
  2108.      * Ensures the specific preconditions of the said instruction.
  2109.      */
  2110.     @Override
  2111.     public void visitLNEG(final LNEG o) {
  2112.         if (stack().peek() != Type.LONG) {
  2113.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2114.         }
  2115.     }

  2117.     /**
  2118.      * Assures the generic preconditions of a LoadClass instance. The referenced class is loaded and pass2-verified.
  2119.      */
  2120.     @Override
  2121.     public void visitLoadClass(final LoadClass o) {
  2122.         final ObjectType t = o.getLoadClassType(cpg);
  2123.         if (t != null) { // null means "no class is loaded"
  2124.             final Verifier v = VerifierFactory.getVerifier(t.getClassName());
  2125.             final VerificationResult vr = v.doPass2();
  2126.             if (vr.getStatus() != VerificationResult.VERIFIED_OK) {
  2127.                 constraintViolated((Instruction) o,
  2128.                     "Class '" + o.getLoadClassType(cpg).getClassName() + "' is referenced, but cannot be loaded and resolved: '" + vr + "'.");
  2129.             }
  2130.         }
  2131.     }

  2133.     /**
  2134.      * Assures the generic preconditions of a LoadInstruction instance.
  2135.      */
  2136.     @Override
  2137.     public void visitLoadInstruction(final LoadInstruction o) {
  2138.         // visitLocalVariableInstruction(o) is called before, because it is more generic.

  2140.         // LOAD instructions must not read Type.UNKNOWN
  2141.         if (locals().get(o.getIndex()) == Type.UNKNOWN) {
  2142.             constraintViolated(o, "Read-Access on local variable " + o.getIndex() + " with unknown content.");
  2143.         }

  2145.         // LOAD instructions, two-slot-values at index N must have Type.UNKNOWN
  2146.         // as a symbol for the higher halve at index N+1
  2147.         // [suppose some instruction put an int at N+1--- our double at N is defective]
  2148.         if (o.getType(cpg).getSize() == 2 && locals().get(o.getIndex() + 1) != Type.UNKNOWN) {
  2149.             constraintViolated(o,
  2150.                 "Reading a two-locals value from local variables " + o.getIndex() + " and " + (o.getIndex() + 1) + " where the latter one is destroyed.");
  2151.         }

  2153.         // LOAD instructions must read the correct type.
  2154.         if (!(o instanceof ALOAD)) {
  2155.             if (locals().get(o.getIndex()) != o.getType(cpg)) {
  2156.                 constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '" + locals().get(o.getIndex())
  2157.                     + "'; Instruction type: '" + o.getType(cpg) + "'.");
  2158.             }
  2159.         } else if (!(locals().get(o.getIndex()) instanceof ReferenceType)) {
  2160.             constraintViolated(o, "Local Variable type and LOADing Instruction type mismatch: Local Variable: '" + locals().get(o.getIndex())
  2161.                 + "'; Instruction expects a ReferenceType.");
  2162.         }
  2163.         // ALOAD __IS ALLOWED__ to put uninitialized objects onto the stack!
  2164.         // referenceTypeIsInitialized(o, (ReferenceType) (locals().get(o.getIndex())));

  2166.         // LOAD instructions must have enough free stack slots.
  2167.         if (stack().maxStack() - stack().slotsUsed() < o.getType(cpg).getSize()) {
  2168.             constraintViolated(o, "Not enough free stack slots to load a '" + o.getType(cpg) + "' onto the OperandStack.");
  2169.         }
  2170.     }

  2172.     /**
  2173.      * Assures the generic preconditions of a LocalVariableInstruction instance. That is, the index of the local variable
  2174.      * must be valid.
  2175.      */
  2176.     @Override
  2177.     public void visitLocalVariableInstruction(final LocalVariableInstruction o) {
  2178.         if (locals().maxLocals() <= (o.getType(cpg).getSize() == 1 ? o.getIndex() : o.getIndex() + 1)) {
  2179.             constraintViolated(o, "The 'index' is not a valid index into the local variable array.");
  2180.         }
  2181.     }

  2183.     /**
  2184.      * Ensures the specific preconditions of the said instruction.
  2185.      */
  2186.     @Override
  2187.     public void visitLOOKUPSWITCH(final LOOKUPSWITCH o) {
  2188.         if (stack().peek() != Type.INT) {
  2189.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  2190.         }
  2191.         // See also pass 3a.
  2192.     }

  2194.     /**
  2195.      * Ensures the specific preconditions of the said instruction.
  2196.      */
  2197.     @Override
  2198.     public void visitLOR(final LOR o) {
  2199.         if (stack().peek() != Type.LONG) {
  2200.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2201.         }
  2202.         if (stack().peek(1) != Type.LONG) {
  2203.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2204.         }
  2205.     }

  2207.     /**
  2208.      * Ensures the specific preconditions of the said instruction.
  2209.      */
  2210.     @Override
  2211.     public void visitLREM(final LREM o) {
  2212.         if (stack().peek() != Type.LONG) {
  2213.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2214.         }
  2215.         if (stack().peek(1) != Type.LONG) {
  2216.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2217.         }
  2218.     }

  2220.     /**
  2221.      * Ensures the specific preconditions of the said instruction.
  2222.      */
  2223.     @Override
  2224.     public void visitLRETURN(final LRETURN o) {
  2225.         if (stack().peek() != Type.LONG) {
  2226.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2227.         }
  2228.     }

  2230.     /**
  2231.      * Ensures the specific preconditions of the said instruction.
  2232.      */
  2233.     @Override
  2234.     public void visitLSHL(final LSHL o) {
  2235.         if (stack().peek() != Type.INT) {
  2236.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  2237.         }
  2238.         if (stack().peek(1) != Type.LONG) {
  2239.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2240.         }
  2241.     }

  2243.     /**
  2244.      * Ensures the specific preconditions of the said instruction.
  2245.      */
  2246.     @Override
  2247.     public void visitLSHR(final LSHR o) {
  2248.         if (stack().peek() != Type.INT) {
  2249.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  2250.         }
  2251.         if (stack().peek(1) != Type.LONG) {
  2252.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2253.         }
  2254.     }

  2256.     /**
  2257.      * Ensures the specific preconditions of the said instruction.
  2258.      */
  2259.     @Override
  2260.     public void visitLSTORE(final LSTORE o) {
  2261.         // visitStoreInstruction(StoreInstruction) is called before.

  2263.         // Nothing else needs to be done here.
  2264.     }

  2266.     /**
  2267.      * Ensures the specific preconditions of the said instruction.
  2268.      */
  2269.     @Override
  2270.     public void visitLSUB(final LSUB o) {
  2271.         if (stack().peek() != Type.LONG) {
  2272.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2273.         }
  2274.         if (stack().peek(1) != Type.LONG) {
  2275.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2276.         }
  2277.     }

  2279.     /**
  2280.      * Ensures the specific preconditions of the said instruction.
  2281.      */
  2282.     @Override
  2283.     public void visitLUSHR(final LUSHR o) {
  2284.         if (stack().peek() != Type.INT) {
  2285.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  2286.         }
  2287.         if (stack().peek(1) != Type.LONG) {
  2288.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2289.         }
  2290.     }

  2292.     /**
  2293.      * Ensures the specific preconditions of the said instruction.
  2294.      */
  2295.     @Override
  2296.     public void visitLXOR(final LXOR o) {
  2297.         if (stack().peek() != Type.LONG) {
  2298.             constraintViolated(o, "The value at the stack top is not of type 'long', but of type '" + stack().peek() + "'.");
  2299.         }
  2300.         if (stack().peek(1) != Type.LONG) {
  2301.             constraintViolated(o, "The value at the stack next-to-top is not of type 'long', but of type '" + stack().peek(1) + "'.");
  2302.         }
  2303.     }

  2305.     /**
  2306.      * Ensures the specific preconditions of the said instruction.
  2307.      */
  2308.     @Override
  2309.     public void visitMONITORENTER(final MONITORENTER o) {
  2310.         if (!(stack().peek() instanceof ReferenceType)) {
  2311.             constraintViolated(o, "The stack top should be of a ReferenceType, but is '" + stack().peek() + "'.");
  2312.         }
  2313.         // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
  2314.     }

  2316.     /**
  2317.      * Ensures the specific preconditions of the said instruction.
  2318.      */
  2319.     @Override
  2320.     public void visitMONITOREXIT(final MONITOREXIT o) {
  2321.         if (!(stack().peek() instanceof ReferenceType)) {
  2322.             constraintViolated(o, "The stack top should be of a ReferenceType, but is '" + stack().peek() + "'.");
  2323.         }
  2324.         // referenceTypeIsInitialized(o, (ReferenceType) (stack().peek()) );
  2325.     }

  2327.     /**
  2328.      * Ensures the specific preconditions of the said instruction.
  2329.      */
  2330.     @Override
  2331.     public void visitMULTIANEWARRAY(final MULTIANEWARRAY o) {
  2332.         final int dimensions = o.getDimensions();
  2333.         // Dimensions argument is okay: see Pass 3a.
  2334.         for (int i = 0; i < dimensions; i++) {
  2335.             if (stack().peek(i) != Type.INT) {
  2336.                 constraintViolated(o, "The '" + dimensions + "' upper stack types should be 'int' but aren't.");
  2337.             }
  2338.         }
  2339.         // The runtime constant pool item at that index must be a symbolic reference to a class,
  2340.         // array, or interface type. See Pass 3a.
  2341.     }

  2343.     /**
  2344.      * Ensures the specific preconditions of the said instruction.
  2345.      */
  2346.     @Override
  2347.     public void visitNEW(final NEW o) {
  2348.         // visitCPInstruction(CPInstruction) has been called before.
  2349.         // visitLoadClass(LoadClass) has been called before.

  2351.         final Type t = o.getType(cpg);
  2352.         if (!(t instanceof ReferenceType)) {
  2353.             throw new AssertionViolatedException("NEW.getType() returning a non-reference type?!");
  2354.         }
  2355.         if (!(t instanceof ObjectType)) {
  2356.             constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + t + "'.");
  2357.         }
  2358.         final ObjectType obj = (ObjectType) t;

  2360.         // e.g.: Don't instantiate interfaces
  2361.         try {
  2362.             if (!obj.referencesClassExact()) {
  2363.                 constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + obj + "'.");
  2364.             }
  2365.         } catch (final ClassNotFoundException e) {
  2366.             constraintViolated(o, "Expecting a class type (ObjectType) to work on. Found: '" + obj + "'." + " which threw " + e);
  2367.         }
  2368.     }

  2370.     /**
  2371.      * Ensures the specific preconditions of the said instruction.
  2372.      */
  2373.     @Override
  2374.     public void visitNEWARRAY(final NEWARRAY o) {
  2375.         if (stack().peek() != Type.INT) {
  2376.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  2377.         }
  2378.     }

  2380.     /**
  2381.      * Ensures the specific preconditions of the said instruction.
  2382.      */
  2383.     @Override
  2384.     public void visitNOP(final NOP o) {
  2385.         // nothing is to be done here.
  2386.     }

  2388.     /**
  2389.      * Ensures the specific preconditions of the said instruction.
  2390.      */
  2391.     @Override
  2392.     public void visitPOP(final POP o) {
  2393.         if (stack().peek().getSize() != 1) {
  2394.             constraintViolated(o, "Stack top size should be 1 but stack top is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
  2395.         }
  2396.     }

  2398.     /**
  2399.      * Ensures the specific preconditions of the said instruction.
  2400.      */
  2401.     @Override
  2402.     public void visitPOP2(final POP2 o) {
  2403.         if (stack().peek().getSize() != 2) {
  2404.             constraintViolated(o, "Stack top size should be 2 but stack top is '" + stack().peek() + "' of size '" + stack().peek().getSize() + "'.");
  2405.         }
  2406.     }

  2408.     /**
  2409.      * Ensures the specific preconditions of the said instruction.
  2410.      */
  2411.     @Override
  2412.     public void visitPUTFIELD(final PUTFIELD o) {
  2413.         try {

  2415.             final Type objectref = stack().peek(1);
  2416.             if (!(objectref instanceof ObjectType || objectref == Type.NULL)) {
  2417.                 constraintViolated(o, "Stack next-to-top should be an object reference that's not an array reference, but is '" + objectref + "'.");
  2418.             }

  2420.             final Field f = visitFieldInstructionInternals(o);

  2422.             if (f.isProtected()) {
  2423.                 final ObjectType classtype = getObjectType(o);
  2424.                 final ObjectType curr = ObjectType.getInstance(mg.getClassName());

  2426.                 if (classtype.equals(curr) || curr.subclassOf(classtype)) {
  2427.                     final Type tp = stack().peek(1);
  2428.                     if (tp == Type.NULL) {
  2429.                         return;
  2430.                     }
  2431.                     if (!(tp instanceof ObjectType)) {
  2432.                         constraintViolated(o, "The 'objectref' must refer to an object that's not an array. Found instead: '" + tp + "'.");
  2433.                     }
  2434.                     final ObjectType objreftype = (ObjectType) tp;
  2435.                     if (!(objreftype.equals(curr) || objreftype.subclassOf(curr))) {
  2436.                         constraintViolated(o,
  2437.                             "The referenced field has the ACC_PROTECTED modifier, and it's a member of the current class or"
  2438.                                 + " a superclass of the current class. However, the referenced object type '" + stack().peek()
  2439.                                 + "' is not the current class or a subclass of the current class.");
  2440.                     }
  2441.                 }
  2442.             }

  2444.             // TODO: Could go into Pass 3a.
  2445.             if (f.isStatic()) {
  2446.                 constraintViolated(o, "Referenced field '" + f + "' is static which it shouldn't be.");
  2447.             }

  2449.         } catch (final ClassNotFoundException e) {
  2450.             // FIXME: maybe not the best way to handle this
  2451.             throw new AssertionViolatedException("Missing class: " + e, e);
  2452.         }
  2453.     }

  2455.     /**
  2456.      * Ensures the specific preconditions of the said instruction.
  2457.      */
  2458.     @Override
  2459.     public void visitPUTSTATIC(final PUTSTATIC o) {
  2460.         try {
  2461.             visitFieldInstructionInternals(o);
  2462.         } catch (final ClassNotFoundException e) {
  2463.             // FIXME: maybe not the best way to handle this
  2464.             throw new AssertionViolatedException("Missing class: " + e, e);
  2465.         }
  2466.     }

  2468.     /**
  2469.      * Ensures the specific preconditions of the said instruction.
  2470.      */
  2471.     @Override
  2472.     public void visitRET(final RET o) {
  2473.         if (!(locals().get(o.getIndex()) instanceof ReturnaddressType)) {
  2474.             constraintViolated(o, "Expecting a ReturnaddressType in local variable " + o.getIndex() + ".");
  2475.         }
  2476.         if (locals().get(o.getIndex()) == ReturnaddressType.NO_TARGET) {
  2477.             throw new AssertionViolatedException("RET expecting a target!");
  2478.         }
  2479.         // Other constraints such as non-allowed overlapping subroutines are enforced
  2480.         // while building the Subroutines data structure.
  2481.     }

  2483.     /**
  2484.      * Ensures the specific preconditions of the said instruction.
  2485.      */
  2486.     @Override
  2487.     public void visitRETURN(final RETURN o) {
  2488.         if (mg.getName().equals(Const.CONSTRUCTOR_NAME) && Frame.getThis() != null && !mg.getClassName().equals(Type.OBJECT.getClassName())) {
  2489.             constraintViolated(o, "Leaving a constructor that itself did not call a constructor.");
  2490.         }
  2491.     }

  2493.     /**
  2494.      * Assures the generic preconditions of a ReturnInstruction instance.
  2495.      */
  2496.     @Override
  2497.     public void visitReturnInstruction(final ReturnInstruction o) {
  2498.         Type methodType = mg.getType();
  2499.         if (methodType == Type.BOOLEAN || methodType == Type.BYTE || methodType == Type.SHORT || methodType == Type.CHAR) {
  2500.             methodType = Type.INT;
  2501.         }

  2503.         if (o instanceof RETURN) {
  2504.             if (methodType == Type.VOID) {
  2505.                 return;
  2506.             }
  2507.             constraintViolated(o, "RETURN instruction in non-void method.");
  2508.         }
  2509.         if (o instanceof ARETURN) {
  2510.             if (methodType == Type.VOID) {
  2511.                 constraintViolated(o, "ARETURN instruction in void method.");
  2512.             }
  2513.             if (stack().peek() == Type.NULL) {
  2514.                 return;
  2515.             }
  2516.             if (!(stack().peek() instanceof ReferenceType)) {
  2517.                 constraintViolated(o, "Reference type expected on top of stack, but is: '" + stack().peek() + "'.");
  2518.             }
  2519.             referenceTypeIsInitialized(o, (ReferenceType) stack().peek());
  2520.             // ReferenceType objectref = (ReferenceType) (stack().peek());
  2521.             // TODO: This can only be checked if using Staerk-et-al's "set of object types" instead of a
  2522.             // "wider cast object type" created during verification.
  2523.             // if (! (objectref.isAssignmentCompatibleWith(mg.getType())) ) {
  2524.             // constraintViolated(o, "Type on stack top which should be returned is a '"+stack().peek()+
  2525.             // "' which is not assignment compatible with the return type of this method, '"+mg.getType()+"'.");
  2526.             // }
  2527.         } else if (!methodType.equals(stack().peek())) {
  2528.             constraintViolated(o, "Current method has return type of '" + mg.getType() + "' expecting a '" + methodType
  2529.                 + "' on top of the stack. But stack top is a '" + stack().peek() + "'.");
  2530.         }
  2531.     }

  2533.     /**
  2534.      * Ensures the specific preconditions of the said instruction.
  2535.      */
  2536.     @Override
  2537.     public void visitSALOAD(final SALOAD o) {
  2538.         indexOfInt(o, stack().peek());
  2539.         if (stack().peek(1) == Type.NULL) {
  2540.             return;
  2541.         }
  2542.         if (!(stack().peek(1) instanceof ArrayType)) {
  2543.             constraintViolated(o, "Stack next-to-top must be of type short[] but is '" + stack().peek(1) + "'.");
  2544.         }
  2545.         final Type t = ((ArrayType) stack().peek(1)).getBasicType();
  2546.         if (t != Type.SHORT) {
  2547.             constraintViolated(o, "Stack next-to-top must be of type short[] but is '" + stack().peek(1) + "'.");
  2548.         }
  2549.     }

  2551.     /**
  2552.      * Ensures the specific preconditions of the said instruction.
  2553.      */
  2554.     @Override
  2555.     public void visitSASTORE(final SASTORE o) {
  2556.         if (stack().peek() != Type.INT) {
  2557.             constraintViolated(o, "The value at the stack top is not of type 'int', but of type '" + stack().peek() + "'.");
  2558.         }
  2559.         indexOfInt(o, stack().peek(1));
  2560.         if (stack().peek(2) == Type.NULL) {
  2561.             return;
  2562.         }
  2563.         if (!(stack().peek(2) instanceof ArrayType)) {
  2564.             constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '" + stack().peek(2) + "'.");
  2565.         }
  2566.         final Type t = ((ArrayType) stack().peek(2)).getBasicType();
  2567.         if (t != Type.SHORT) {
  2568.             constraintViolated(o, "Stack next-to-next-to-top must be of type short[] but is '" + stack().peek(2) + "'.");
  2569.         }
  2570.     }

  2572.     /**
  2573.      * Ensures the specific preconditions of the said instruction.
  2574.      */
  2575.     @Override
  2576.     public void visitSIPUSH(final SIPUSH o) {
  2577.         // nothing to do here. Generic visitXXX() methods did the trick before.
  2578.     }

  2580.     /***************************************************************/
  2581.     /* MISC */
  2582.     /***************************************************************/
  2583.     /**
  2584.      * Ensures the general preconditions of an instruction that accesses the stack. This method is here because BCEL has no
  2585.      * such superinterface for the stack accessing instructions; and there are funny unexpected exceptions in the semantices
  2586.      * of the superinterfaces and superclasses provided. E.g. SWAP is a StackConsumer, but DUP_X1 is not a StackProducer.
  2587.      * Therefore, this method is called by all StackProducer, StackConsumer, and StackInstruction instances via their
  2588.      * visitXXX() method. Unfortunately, as the superclasses and superinterfaces overlap, some instructions cause this
  2589.      * method to be called two or three times. [TODO: Fix this.]
  2590.      *
  2591.      * @see #visitStackConsumer(StackConsumer o)
  2592.      * @see #visitStackProducer(StackProducer o)
  2593.      * @see #visitStackInstruction(StackInstruction o)
  2594.      */
  2595.     private void visitStackAccessor(final Instruction o) {
  2596.         final int consume = o.consumeStack(cpg); // Stack values are always consumed first; then produced.
  2597.         if (consume > stack().slotsUsed()) {
  2598.             constraintViolated(o, "Cannot consume " + consume + " stack slots: only " + stack().slotsUsed() + " slot(s) left on stack!\nStack:\n" + stack());
  2599.         }

  2601.         final int produce = o.produceStack(cpg) - o.consumeStack(cpg); // Stack values are always consumed first; then produced.
  2602.         if (produce + stack().slotsUsed() > stack().maxStack()) {
  2603.             constraintViolated(o, "Cannot produce " + produce + " stack slots: only " + (stack().maxStack() - stack().slotsUsed())
  2604.                 + " free stack slot(s) left.\nStack:\n" + stack());
  2605.         }
  2606.     }

  2608.     /**
  2609.      * Ensures the general preconditions of a StackConsumer instance.
  2610.      */
  2611.     @Override
  2612.     public void visitStackConsumer(final StackConsumer o) {
  2613.         visitStackAccessor((Instruction) o);
  2614.     }

  2616.     /**
  2617.      * Ensures the general preconditions of a StackInstruction instance.
  2618.      */
  2619.     @Override
  2620.     public void visitStackInstruction(final StackInstruction o) {
  2621.         visitStackAccessor(o);
  2622.     }

  2624.     /**
  2625.      * Ensures the general preconditions of a StackProducer instance.
  2626.      */
  2627.     @Override
  2628.     public void visitStackProducer(final StackProducer o) {
  2629.         visitStackAccessor((Instruction) o);
  2630.     }

  2632.     /**
  2633.      * Assures the generic preconditions of a StoreInstruction instance.
  2634.      */
  2635.     @Override
  2636.     public void visitStoreInstruction(final StoreInstruction o) {
  2637.         // visitLocalVariableInstruction(o) is called before, because it is more generic.

  2639.         if (stack().isEmpty()) { // Don't bother about 1 or 2 stack slots used. This check is implicitly done below while type checking.
  2640.             constraintViolated(o, "Cannot STORE: Stack to read from is empty.");
  2641.         }

  2643.         if (!(o instanceof ASTORE)) {
  2644.             if (!(stack().peek() == o.getType(cpg))) { // the other xSTORE types are singletons in BCEL.
  2645.                 constraintViolated(o,
  2646.                     "Stack top type and STOREing Instruction type mismatch: Stack top: '" + stack().peek() + "'; Instruction type: '" + o.getType(cpg) + "'.");
  2647.             }
  2648.         } else { // we deal with ASTORE
  2649.             final Type stacktop = stack().peek();
  2650.             if (!(stacktop instanceof ReferenceType) && !(stacktop instanceof ReturnaddressType)) {
  2651.                 constraintViolated(o, "Stack top type and STOREing Instruction type mismatch: Stack top: '" + stack().peek()
  2652.                     + "'; Instruction expects a ReferenceType or a ReturnadressType.");
  2653.             }
  2654.             // if (stacktop instanceof ReferenceType) {
  2655.             // referenceTypeIsInitialized(o, (ReferenceType) stacktop);
  2656.             // }
  2657.         }
  2658.     }

  2660.     /**
  2661.      * Ensures the specific preconditions of the said instruction.
  2662.      */
  2663.     @Override
  2664.     public void visitSWAP(final SWAP o) {
  2665.         if (stack().peek().getSize() != 1) {
  2666.             constraintViolated(o, "The value at the stack top is not of size '1', but of size '" + stack().peek().getSize() + "'.");
  2667.         }
  2668.         if (stack().peek(1).getSize() != 1) {
  2669.             constraintViolated(o, "The value at the stack next-to-top is not of size '1', but of size '" + stack().peek(1).getSize() + "'.");
  2670.         }
  2671.     }

  2673.     /**
  2674.      * Ensures the specific preconditions of the said instruction.
  2675.      */
  2676.     @Override
  2677.     public void visitTABLESWITCH(final TABLESWITCH o) {
  2678.         indexOfInt(o, stack().peek());
  2679.         // See Pass 3a.
  2680.     }

  2682. }
Created with JaCoCo 0.8.12.202403310830