* Updated header: Added 2006. Changed address of FSF. Changed email
[cacao.git] / src / vm / jit / verify / typecheck.c
index 769017561f8c29e515046dd7fecf30eb7ec4fe4a..5d21065fb217f3bfebe1e580b310c638c8ad20d1 100644 (file)
@@ -1,9 +1,9 @@
 /* src/vm/jit/verify/typecheck.c - typechecking (part of bytecode verification)
 
-   Copyright (C) 1996-2005 R. Grafl, A. Krall, C. Kruegel, C. Oates,
-   R. Obermaisser, M. Platter, M. Probst, S. Ring, E. Steiner,
-   C. Thalinger, D. Thuernbeck, P. Tomsich, C. Ullrich, J. Wenninger,
-   Institut f. Computersprachen - TU Wien
+   Copyright (C) 1996-2005, 2006 R. Grafl, A. Krall, C. Kruegel,
+   C. Oates, R. Obermaisser, M. Platter, M. Probst, S. Ring,
+   E. Steiner, C. Thalinger, D. Thuernbeck, P. Tomsich, C. Ullrich,
+   J. Wenninger, Institut f. Computersprachen - TU Wien
 
    This file is part of CACAO.
 
 
    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
-   Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
-   02111-1307, USA.
+   Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
+   02110-1301, USA.
 
-   Contact: cacao@complang.tuwien.ac.at
+   Contact: cacao@cacaojvm.org
 
    Authors: Edwin Steiner
 
    Changes: Christian Thalinger
 
-   $Id: typecheck.c 2788 2005-06-22 16:08:51Z edwin $
+   $Id: typecheck.c 4357 2006-01-22 23:33:38Z twisti $
 
 */
 
+/*
+
+What's the purpose of the `typechecker`?
+----------------------------------------
+
+The typechecker analyses (the intermediate repr. of) the bytecode of
+each method and ensures that for each instruction the values on the
+stack and in local variables are of the correct type whenever the
+instruction is executed.
+
+type checking is a mandatory part of bytecode verification.
+
+
+How does the typechecker work?
+------------------------------
+
+The JVM stack and the local variables are not statically typed, so the
+typechecker has to *infer* the static types of stack slots and local
+variables at each point of the method. The JVM spec imposes a lot of
+restrictions on the bytecode in order to guarantee that this is always
+possible.
+
+Basically the typechecker solves the data flow equations of the method.
+This is done in the usual way for a forward data flow analysis: Starting
+from the entry point of the method the typechecker follows the CFG and
+records the type of each stack slot and local variable at each point[1].
+When two or more control flow paths merge at a point, the union of the
+types for each slot/variable is taken. The algorithm continues to follow
+all possible paths[2] until the recorded types do not change anymore (ie.
+the equations have been solved).
+
+If the solution has been reached and the resulting types are valid for
+all instructions, then type checking terminates with success, otherwise
+an exception is thrown.
+
+
+Why is this code so damn complicated?
+-------------------------------------
+
+Short answer: The devil's in the details.
+
+While the basic operation of the typechecker is no big deal, there are
+many properties of Java bytecode which make type checking hard. Some of
+them are not even addressed in the JVM spec. Some problems and their
+solutions:
+
+*) Finding a good representation of the union of two reference types is
+difficult because of multiple inheritance of interfaces. 
+
+       Solution: The typeinfo system can represent such "merged" types by a
+       list of proper subclasses of a class. Example:
+
+               typeclass=java.lang.Object merged={ InterfaceA, InterfaceB }
+       
+       represents the result of merging two interface types "InterfaceA"
+       and "InterfaceB".
+
+*) When the code of a method is verified, there may still be unresolved
+references to classes/methods/fields in the code, which we may not force
+to be resolved eagerly. (A similar problem arises because of the special
+checks for protected members.)
+
+       Solution: The typeinfo system knows how to deal with unresolved
+       class references. Whenever a check has to be performed for an
+       unresolved type, the type is annotated with constraints representing
+       the check. Later, when the type is resolved, the constraints are
+       checked. (See the constrain_unresolved_... and the resolve_...
+       methods.)[3]
+
+*) The boundaries of jsr subroutines are not well-defined. For a given
+instruction it may be impossible to tell whether it is part of a
+subroutine, or to which subroutine it belongs.
+
+       Solution: The typechecker implements a method developed by
+       Alessandro Coglio[4] which treats each returnAddress as a distinct
+       type that is not merged with other returnAddresses. This way, when a
+       RET instruction is reached, we know exactly which types to propagate
+       to which return target among the possible targets of the RET. The
+       downside of this method is, that for each slot/variable we must
+       store not just one type, but one type *for each possible use of the
+       returnAddresses* that currently are in a slot/variable.[5]
+
+*) Checks for uninitialized object instances are hard because after the
+invocation of <init> on an uninitialized object *all* slots/variables
+referring to this object (and exactly those slots/variables) must be
+marked as initialized.
+
+       Solution: The JVM spec describes a solution, which has been
+       implemented in this typechecker.
+
+
+--- Footnotes
+
+[1] Actually only the types of slots/variables at the start of each
+basic block are remembered. Within a basic block the algorithm only keeps
+the types of the slots/variables for the "current" instruction which is
+being analysed. 
+
+[2] Actually the algorithm iterates through the basic block list until
+there are no more changes. Theoretically it would be wise to sort the
+basic blocks topologically beforehand, but the number of average/max
+iterations observed is so low, that this was not deemed necessary.
+
+[3] This is similar to a method proposed by: Alessandro Coglio et al., A
+Formal Specification of Java Class Loading, Technical Report, Kestrel
+Institute April 2000, revised July 2000 
+http://www.kestrel.edu/home/people/coglio/loading.pdf
+An important difference is that Coglio's subtype constraints are checked
+after loading, while our constraints are checked when the field/method
+is accessed for the first time, so we can guarantee lexically correct
+error reporting.
+
+[4] Alessandro Coglio, Simple Verification Technique for Complex Java
+Bytecode Subroutines, 4th ECOOP Workshop on Formal Techniques for
+Java-like Programs, June 2002
+http://www.kestrel.edu/home/people/coglio/ftjp02.pdf
+
+[5] This is a major source of code complexity. The main data structures
+dealing with this are the "typevector set" and the typestack. The
+"typevector set" is a set of alternative typevectors, such that each
+typevector specifies the types of the local variables for a single
+combination of returnAddresses used. Thus we support full polymorphism
+of subroutines over the types of local variables. The typestack,
+however, does not support polymorphism, both for historical and JVM-spec
+reasons. A slot of the typestack may, however, contain multiple
+alternative returnAddresses, which is realized by a linked list hanging
+of the typeinfo of the stack slot.
+
+*/
 
 #include <assert.h>
 #include <string.h>
 
-#include "vm/global.h" /* must be here because of CACAO_TYPECHECK */
+#include "config.h"
+#include "vm/types.h"
+#include "vm/global.h"
 
-#ifdef CACAO_TYPECHECK
+#ifdef ENABLE_VERIFIER
 
-#include "types.h"
 #include "mm/memory.h"
 #include "toolbox/logging.h"
 #include "native/native.h"
 #include "vm/jit/patcher.h"
 #include "vm/loader.h"
 #include "vm/options.h"
-#include "vm/tables.h"
 #include "vm/jit/jit.h"
 #include "vm/jit/stack.h"
 #include "vm/access.h"
@@ -165,6 +294,8 @@ typestate_print(FILE *file,stackptr instack,typevector *localset,int size)
 
 static int stat_typechecked = 0;
 static int stat_typechecked_jsr = 0;
+static int stat_methods_with_handlers = 0;
+static int stat_methods_maythrow = 0;
 static int stat_iterations[STAT_ITERATIONS+1] = { 0 };
 static int stat_reached = 0;
 static int stat_copied = 0;
@@ -174,18 +305,29 @@ static int stat_backwards = 0;
 static int stat_blocks[STAT_BLOCKS+1] = { 0 };
 static int stat_locals[STAT_LOCALS+1] = { 0 };
 static int stat_ins = 0;
+static int stat_ins_maythrow = 0;
+static int stat_ins_stack = 0;
 static int stat_ins_field = 0;
+static int stat_ins_field_unresolved = 0;
+static int stat_ins_field_uninitialized = 0;
 static int stat_ins_invoke = 0;
+static int stat_ins_invoke_unresolved = 0;
 static int stat_ins_primload = 0;
 static int stat_ins_aload = 0;
 static int stat_ins_builtin = 0;
 static int stat_ins_builtin_gen = 0;
 static int stat_ins_branch = 0;
 static int stat_ins_switch = 0;
+static int stat_ins_primitive_return = 0;
+static int stat_ins_areturn = 0;
+static int stat_ins_areturn_unresolved = 0;
+static int stat_ins_athrow = 0;
+static int stat_ins_athrow_unresolved = 0;
 static int stat_ins_unchecked = 0;
 static int stat_handlers_reached = 0;
 static int stat_savedstack = 0;
 
+#define TYPECHECK_MARK(var)   ((var) = true)
 #define TYPECHECK_COUNT(cnt)  (cnt)++
 #define TYPECHECK_COUNTIF(cond,cnt)  do{if(cond) (cnt)++;} while(0)
 #define TYPECHECK_COUNT_FREQ(array,val,limit) \
@@ -199,12 +341,14 @@ static void print_freq(FILE *file,int *array,int limit)
        int i;
        for (i=0; i<limit; ++i)
                fprintf(file,"      %3d: %8d\n",i,array[i]);
-       fprintf(file,"    =>%3d: %8d\n",limit,array[limit]);
+       fprintf(file,"    >=%3d: %8d\n",limit,array[limit]);
 }
 
 void typecheck_print_statistics(FILE *file) {
        fprintf(file,"typechecked methods: %8d\n",stat_typechecked);
-       fprintf(file,"methods with JSR   : %8d\n",stat_typechecked_jsr);
+       fprintf(file,"    with JSR       : %8d\n",stat_typechecked_jsr);
+       fprintf(file,"    with handler(s): %8d\n",stat_methods_with_handlers);
+       fprintf(file,"    with throw(s)  : %8d\n",stat_methods_maythrow);
        fprintf(file,"reached blocks     : %8d\n",stat_reached);
        fprintf(file,"copied states      : %8d\n",stat_copied);
        fprintf(file,"merged states      : %8d\n",stat_merged);
@@ -213,15 +357,25 @@ void typecheck_print_statistics(FILE *file) {
        fprintf(file,"handlers reached   : %8d\n",stat_handlers_reached);
        fprintf(file,"saved stack (times): %8d\n",stat_savedstack);
        fprintf(file,"instructions       : %8d\n",stat_ins);
+       fprintf(file,"    stack          : %8d\n",stat_ins_stack);
        fprintf(file,"    field access   : %8d\n",stat_ins_field);
+       fprintf(file,"      (unresolved) : %8d\n",stat_ins_field_unresolved);
+       fprintf(file,"      (uninit.)    : %8d\n",stat_ins_field_uninitialized);
        fprintf(file,"    invocations    : %8d\n",stat_ins_invoke);
-       fprintf(file,"    load primitive : %8d\n",stat_ins_primload);
+       fprintf(file,"      (unresolved) : %8d\n",stat_ins_invoke_unresolved);
+       fprintf(file,"    load primitive : (currently not counted) %8d\n",stat_ins_primload);
        fprintf(file,"    load address   : %8d\n",stat_ins_aload);
        fprintf(file,"    builtins       : %8d\n",stat_ins_builtin);
        fprintf(file,"        generic    : %8d\n",stat_ins_builtin_gen);
-       fprintf(file,"    unchecked      : %8d\n",stat_ins_unchecked);
        fprintf(file,"    branches       : %8d\n",stat_ins_branch);
        fprintf(file,"    switches       : %8d\n",stat_ins_switch);
+       fprintf(file,"    prim. return   : %8d\n",stat_ins_primitive_return);
+       fprintf(file,"    areturn        : %8d\n",stat_ins_areturn);
+       fprintf(file,"      (unresolved) : %8d\n",stat_ins_areturn_unresolved);
+       fprintf(file,"    athrow         : %8d\n",stat_ins_athrow);
+       fprintf(file,"      (unresolved) : %8d\n",stat_ins_athrow_unresolved);
+       fprintf(file,"    unchecked      : %8d\n",stat_ins_unchecked);
+       fprintf(file,"    maythrow       : %8d\n",stat_ins_maythrow);
        fprintf(file,"iterations used:\n");
        print_freq(file,stat_iterations,STAT_ITERATIONS);
        fprintf(file,"basic blocks per method / 10:\n");
@@ -233,13 +387,13 @@ void typecheck_print_statistics(FILE *file) {
 #else
                                                   
 #define TYPECHECK_COUNT(cnt)
+#define TYPECHECK_MARK(var)
 #define TYPECHECK_COUNTIF(cond,cnt)
 #define TYPECHECK_COUNT_FREQ(array,val,limit)
 #endif
 
-
 /****************************************************************************/
-/* MACROS FOR STACK TYPE CHECKING                                           */
+/* MACROS FOR THROWING EXCEPTIONS                                           */
 /****************************************************************************/
 
 #define TYPECHECK_VERIFYERROR_ret(m,msg,retval) \
@@ -251,6 +405,10 @@ void typecheck_print_statistics(FILE *file) {
 #define TYPECHECK_VERIFYERROR_main(msg)  TYPECHECK_VERIFYERROR_ret(state.m,(msg),NULL)
 #define TYPECHECK_VERIFYERROR_bool(msg)  TYPECHECK_VERIFYERROR_ret(state->m,(msg),false)
 
+/****************************************************************************/
+/* MACROS FOR STACK SLOT TYPE CHECKING                                      */
+/****************************************************************************/
+
 #define TYPECHECK_CHECK_TYPE(sp,tp,msg) \
     do { \
                if ((sp)->type != (tp)) { \
@@ -265,6 +423,43 @@ void typecheck_print_statistics(FILE *file) {
 #define TYPECHECK_DBL(sp)  TYPECHECK_CHECK_TYPE(sp,TYPE_DBL,"Expected to find double on stack")
 #define TYPECHECK_ADR(sp)  TYPECHECK_CHECK_TYPE(sp,TYPE_ADR,"Expected to find object on stack")
 
+/****************************************************************************/
+/* VERIFIER STATE STRUCT                                                    */
+/****************************************************************************/
+
+/* verifier_state - This structure keeps the current state of the      */
+/* bytecode verifier for passing it between verifier functions.        */
+
+typedef struct verifier_state {
+    stackptr curstack;      /* input stack top for current instruction */
+    instruction *iptr;               /* pointer to current instruction */
+    basicblock *bptr;                /* pointer to current basic block */
+
+       methodinfo *m;                               /* the current method */
+       codegendata *cd;                 /* codegendata for current method */
+       registerdata *rd;               /* registerdata for current method */
+       
+       s4 numlocals;                         /* number of local variables */
+       s4 validlocals;                /* number of Java-accessible locals */
+       void *localbuf;       /* local variable types for each block start */
+       typevector *localset;        /* typevector set for local variables */
+       typedescriptor returntype;    /* return type of the current method */
+       
+       stackptr savedstackbuf;             /* buffer for saving the stack */
+       stackptr savedstack;             /* saved instack of current block */
+       
+    exceptiontable **handlers;            /* active exception handlers */
+       stackelement excstack;           /* instack for exception handlers */
+       
+    bool repeat;            /* if true, blocks are iterated over again */
+    bool initmethod;             /* true if this is an "<init>" method */
+       bool jsrencountered;                 /* true if we there was a JSR */
+
+#ifdef TYPECHECK_STATISTICS
+       bool stat_maythrow;          /* at least one instruction may throw */
+#endif
+} verifier_state;
+
 /****************************************************************************/
 /* TYPESTACK MACROS AND FUNCTIONS                                           */
 /*                                                                          */
@@ -281,23 +476,36 @@ void typecheck_print_statistics(FILE *file) {
 #define TYPESTACK_IS_RETURNADDRESS(sptr) \
             TYPE_IS_RETURNADDRESS((sptr)->type,(sptr)->typeinfo)
 
-#define TYPESTACK_IS_REFERENCE(sptr) \
-            TYPE_IS_REFERENCE((sptr)->type,(sptr)->typeinfo)
-
 #define TYPESTACK_RETURNADDRESSSET(sptr) \
             ((typeinfo_retaddr_set*)TYPEINFO_RETURNADDRESS((sptr)->typeinfo))
 
 #define RETURNADDRESSSET_SEEK(set,pos) \
             do {int i; for (i=pos;i--;) set=set->alt;} while(0)
 
-#define TYPESTACK_COPY(sp,copy)                                                                        \
-               do {for(; sp; sp=sp->prev, copy=copy->prev) {           \
-                                       copy->type = sp->type;                                          \
-                                       TYPEINFO_COPY(sp->typeinfo,copy->typeinfo);     \
-                               }} while (0)                                                                    \
+/* typestack_copy **************************************************************
+   Copy the types on the given stack to the destination stack.
 
-static void
-typestack_copy(stackptr dst,stackptr y,typevector *selected)
+   This function does a straight forward copy except for returnAddress types.
+   For returnAddress slots only the return addresses corresponding to
+   typevectors in the SELECTED set are copied.
+   
+   IN:
+          state............current verifier state
+          y................stack with types to copy
+          selected.........set of selected typevectors
+
+   OUT:
+       *dst.............the destination stack
+
+   RETURN VALUE:
+       true.............success
+          false............an exception has been thrown
+
+*******************************************************************************/
+
+static bool
+typestack_copy(verifier_state *state,stackptr dst,stackptr y,typevector *selected)
 {
        typevector *sel;
        typeinfo_retaddr_set *sety;
@@ -306,15 +514,14 @@ typestack_copy(stackptr dst,stackptr y,typevector *selected)
        int k;
        
        for (;dst; dst=dst->prev, y=y->prev) {
+               /* XXX only check the following two in debug mode? */
                if (!y) {
-                       log_text("Stack depth mismatch 1");
-                                       /* XXX verify error */
-                       assert(0);
+                       *exceptionptr = new_verifyerror(state->m,"Stack depth mismatch");
+                       return false;
                }
                if (dst->type != y->type) {
-                       log_text("Stack type mismatch 1");
-                                       /* XXX verify error */
-                       assert(0);
+                       *exceptionptr = new_verifyerror(state->m,"Stack type mismatch");
+                       return false;
                }
                LOG3("copy %p -> %p (type %d)",y,dst,dst->type);
                if (dst->type == TYPE_ADDRESS) {
@@ -344,12 +551,28 @@ typestack_copy(stackptr dst,stackptr y,typevector *selected)
                }
        }
        if (y) {
-               log_text("Stack depth mismatch 2");
-                                       /* XXX verify error */
-               assert(0);
+               *exceptionptr = new_verifyerror(state->m,"Stack depth mismatch");
+               return false;
        }
+       return true;
 }
 
+/* typestack_put_retaddr *******************************************************
+   Put a returnAddress into a stack slot.
+
+   The stack slot receives a set of return addresses with as many members as
+   there are typevectors in the local variable set.
+
+   IN:
+          retaddr..........the returnAddress to set (a basicblock *)
+          loc..............the local variable typevector set
+
+   OUT:
+       *dst.............the destination stack slot
+
+*******************************************************************************/
+
 static void
 typestack_put_retaddr(stackptr dst,void *retaddr,typevector *loc)
 {
@@ -364,6 +587,16 @@ typestack_put_retaddr(stackptr dst,void *retaddr,typevector *loc)
        }
 }
 
+/* typestack_collapse **********************************************************
+   Collapse the given stack by shortening all return address sets to a single
+   member.
+
+   OUT:
+       *dst.............the destination stack to collapse
+
+*******************************************************************************/
+
 static void
 typestack_collapse(stackptr dst)
 {
@@ -373,49 +606,83 @@ typestack_collapse(stackptr dst)
        }
 }
 
-static bool
-typestack_merge(stackptr dst,stackptr y)
+/* typestack_merge *************************************************************
+   Merge the types on one stack into the destination stack.
+
+   IN:
+       state............current state of the verifier
+          dst..............the destination stack
+          y................the second stack
+
+   OUT:
+       *dst.............receives the result of the stack merge
+
+   RETURN VALUE:
+       typecheck_TRUE...*dst has been modified
+          typecheck_FALSE..*dst has not been modified
+          typecheck_FAIL...an exception has been thrown
+
+*******************************************************************************/
+
+static typecheck_result
+typestack_merge(verifier_state *state,stackptr dst,stackptr y)
 {
+       typecheck_result r;
        bool changed = false;
+       
        for (; dst; dst = dst->prev, y=y->prev) {
                if (!y) {
-                       log_text("Stack depth mismatch 3");
-                                       /* XXX verify error */
-                       assert(0);
+                       *exceptionptr = new_verifyerror(state->m,"Stack depth mismatch");
+                       return typecheck_FAIL;
                }
                if (dst->type != y->type) {
-                       log_text("Stack type mismatch 2");
-                                       /* XXX verify error */
-                       assert(0);
+                       *exceptionptr = new_verifyerror(state->m,"Stack type mismatch");
+                       return typecheck_FAIL;
                }
                if (dst->type == TYPE_ADDRESS) {
                        if (TYPEINFO_IS_PRIMITIVE(dst->typeinfo)) {
                                /* dst has returnAddress type */
                                if (!TYPEINFO_IS_PRIMITIVE(y->typeinfo)) {
-                                       log_text("Merging returnAddress with reference");
-                                       /* XXX verify error */
-                                       assert(0);
+                                       *exceptionptr = new_verifyerror(state->m,"Merging returnAddress with reference");
+                                       return typecheck_FAIL;
                                }
                        }
                        else {
                                /* dst has reference type */
                                if (TYPEINFO_IS_PRIMITIVE(y->typeinfo)) {
-                                       log_text("Merging reference with returnAddress");
-                                       /* XXX verify error */
-                                       assert(0);
+                                       *exceptionptr = new_verifyerror(state->m,"Merging reference with returnAddress");
+                                       return typecheck_FAIL;
                                }
-                               changed |= typeinfo_merge(&(dst->typeinfo),&(y->typeinfo));
+                               r = typeinfo_merge(state->m,&(dst->typeinfo),&(y->typeinfo));
+                               if (r == typecheck_FAIL)
+                                       return r;
+                               changed |= r;
                        }
                }
        }
        if (y) {
-               log_text("Stack depth mismatch 4");
-                                       /* XXX verify error */
-               assert(0);
+               *exceptionptr = new_verifyerror(state->m,"Stack depth mismatch");
+               return typecheck_FAIL;
        }
        return changed;
 }
 
+/* typestack_add ***************************************************************
+   Add the return addresses in the given stack at a given k-index to the
+   corresponding return address sets in the destination stack.
+
+   IN:
+          dst..............the destination stack
+          y................the second stack
+          ky...............the k-index which should be selected from the Y stack
+
+   OUT:
+       *dst.............receives the result of adding the addresses
+
+*******************************************************************************/
+
 static void
 typestack_add(stackptr dst,stackptr y,int ky)
 {
@@ -436,7 +703,30 @@ typestack_add(stackptr dst,stackptr y,int ky)
        }
 }
 
-/* 'a' and 'b' are assumed to have passed typestack_canmerge! */
+/* typestack_separable_with ****************************************************
+   This function answers the question: If variant 'kb' of typestack 'b' is
+   added to typestack 'a', will the result be separable?
+
+   A typestack is called 'separable' if it has at least one slot of type
+   returnAddress that contains at least two different return addresses.
+   (ie. a RET using the value in this slot could go to more than one target)
+   
+   IN:
+          a................the first typestack
+          b................the second typestack
+          kb...............the k-index of the variant that should be selected
+                           from typestack 'b'
+
+   OUT:
+       true.............the result would be separable
+          false............the result would not be separable
+
+   PRE-CONDITION:
+       'a' and 'b' are assumed to have passed typestack_canmerge!
+
+*******************************************************************************/
+
 static bool
 typestack_separable_with(stackptr a,stackptr b,int kb)
 {
@@ -459,7 +749,33 @@ typestack_separable_with(stackptr a,stackptr b,int kb)
        return false;
 }
 
-/* 'a' and 'b' are assumed to have passed typestack_canmerge! */
+/* typestack_separable_from ****************************************************
+   This function answers the question: Is variant 'ka' of typestack 'a'
+   separable from variant 'kb' of typestack 'b'?
+
+   Two variants of typestacks are called 'separable' from each other, if there
+   is at least one slot for which the variants contain different return addresses.
+   (ie. a RET using the value in this slot would go to one target in the first
+   variant and to another target in the second variant)
+   
+   IN:
+          a................the first typestack
+          ka...............the k-index of the variant that should be selected
+                           from typestack 'a'
+          b................the second typestack
+          kb...............the k-index of the variant that should be selected
+                           from typestack 'b'
+
+   OUT:
+       true.............the variants are separable
+          false............the variants are not separable
+
+   PRE-CONDITION:
+       'a' and 'b' are assumed to have passed typestack_canmerge!
+
+*******************************************************************************/
+
 static bool
 typestack_separable_from(stackptr a,int ka,stackptr b,int kb)
 {
@@ -490,29 +806,60 @@ typestack_separable_from(stackptr a,int ka,stackptr b,int kb)
 /*     - the set of type vectors describing the local variables             */
 /****************************************************************************/
 
-static bool
-typestate_merge(stackptr deststack,typevector *destloc,
-                               stackptr ystack,typevector *yloc,
-                               int locsize,bool jsrencountered)
+/* typestate_merge *************************************************************
+   Merge the types of one state into the destination state.
+
+   IN:
+       state............current state of the verifier
+          deststack........the destination stack
+          destloc..........the destination set of local variable typevectors
+          ystack...........the second stack
+          yloc.............the second set of local variable typevectors
+
+   OUT:
+       *deststack.......receives the result of the stack merge
+          *destloc.........receives the result of the local variable merge
+
+   RETURN VALUE:
+       typecheck_TRUE...destination state has been modified
+          typecheck_FALSE..destination state has not been modified
+          typecheck_FAIL...an exception has been thrown
+
+*******************************************************************************/
+
+static typecheck_result
+typestate_merge(verifier_state *state,
+                               stackptr deststack,typevector *destloc,
+                               stackptr ystack,typevector *yloc)
 {
        typevector *dvec,*yvec;
        int kd,ky;
        bool changed = false;
+       typecheck_result r;
        
        LOG("merge:");
        LOGSTR("dstack: "); DOLOG(typestack_print(get_logfile(),deststack)); LOGNL;
        LOGSTR("ystack: "); DOLOG(typestack_print(get_logfile(),ystack)); LOGNL;
-       LOGSTR("dloc  : "); DOLOG(typevectorset_print(get_logfile(),destloc,locsize)); LOGNL;
-       LOGSTR("yloc  : "); DOLOG(typevectorset_print(get_logfile(),yloc,locsize)); LOGNL;
+       LOGSTR("dloc  : "); DOLOG(typevectorset_print(get_logfile(),destloc,state->numlocals)); LOGNL;
+       LOGSTR("yloc  : "); DOLOG(typevectorset_print(get_logfile(),yloc,state->numlocals)); LOGNL;
        LOGFLUSH;
 
        /* The stack is always merged. If there are returnAddresses on
         * the stack they are ignored in this step. */
 
-       changed |= typestack_merge(deststack,ystack);
-
-       if (!jsrencountered)
-               return typevector_merge(destloc,yloc,locsize);
+       r = typestack_merge(state,deststack,ystack);
+       if (r == typecheck_FAIL)
+               return r;
+       changed |= r;
+
+       /* If there have not been any JSRs we just have a single typevector merge */
+       if (!state->jsrencountered) {
+               r = typevector_merge(state->m,destloc,yloc,state->numlocals);
+               if (r == typecheck_FAIL)
+                       return r;
+               return changed | r;
+       }
 
        for (yvec=yloc; yvec; yvec=yvec->alt) {
                ky = yvec->k;
@@ -521,15 +868,17 @@ typestate_merge(stackptr deststack,typevector *destloc,
                 * separable when (ystack,yvec) is added. */
 
                if (!typestack_separable_with(deststack,ystack,ky)
-                       && !typevectorset_separable_with(destloc,yvec,locsize))
+                       && !typevectorset_separable_with(destloc,yvec,state->numlocals))
                {
                        /* No, the resulting set won't be separable, thus we
                         * may merge all states in (deststack,destloc) and
                         * (ystack,yvec). */
 
                        typestack_collapse(deststack);
-                       typevectorset_collapse(destloc,locsize);
-                       typevector_merge(destloc,yvec,locsize);
+                       if (typevectorset_collapse(state->m,destloc,state->numlocals) == typecheck_FAIL)
+                               return typecheck_FAIL;
+                       if (typevector_merge(state->m,destloc,yvec,state->numlocals) == typecheck_FAIL)
+                               return typecheck_FAIL;
                }
                else {
                        /* Yes, the resulting set will be separable. Thus we check
@@ -538,13 +887,16 @@ typestate_merge(stackptr deststack,typevector *destloc,
                
                        for (dvec=destloc,kd=0; dvec; dvec=dvec->alt, kd++) {
                                if (!typestack_separable_from(ystack,ky,deststack,kd)
-                                       && !typevector_separable_from(yvec,dvec,locsize))
+                                       && !typevector_separable_from(yvec,dvec,state->numlocals))
                                {
                                        /* The typestate (ystack,yvec) is not separable from
                                         * (deststack,dvec) by any returnAddress. Thus we may
                                         * merge the states. */
                                        
-                                       changed |= typevector_merge(dvec,yvec,locsize);
+                                       r = typevector_merge(state->m,dvec,yvec,state->numlocals);
+                                       if (r == typecheck_FAIL)
+                                               return r;
+                                       changed |= r;
                                        
                                        goto merged;
                                }
@@ -555,7 +907,7 @@ typestate_merge(stackptr deststack,typevector *destloc,
                         * result set. */
 
                        typestack_add(deststack,ystack,ky);
-                       typevectorset_add(destloc,yvec,locsize);
+                       typevectorset_add(destloc,yvec,state->numlocals);
                        changed = true;
                }
                   
@@ -565,33 +917,51 @@ typestate_merge(stackptr deststack,typevector *destloc,
        
        LOG("result:");
        LOGSTR("dstack: "); DOLOG(typestack_print(get_logfile(),deststack)); LOGNL;
-       LOGSTR("dloc  : "); DOLOG(typevectorset_print(get_logfile(),destloc,locsize)); LOGNL;
+       LOGSTR("dloc  : "); DOLOG(typevectorset_print(get_logfile(),destloc,state->numlocals)); LOGNL;
        LOGFLUSH;
        
        return changed;
 }
 
+/* typestate_reach *************************************************************
+   Reach a destination block and propagate stack and local variable types
+
+   IN:
+       state............current state of the verifier
+          destblock........destination basic block
+          ystack...........stack to propagate
+          yloc.............set of local variable typevectors to propagate
+
+   OUT:
+       state->repeat....set to true if the verifier must iterate again
+                           over the basic blocks
+          
+   RETURN VALUE:
+       true.............success
+          false............an exception has been thrown
+
+*******************************************************************************/
 
 static bool
-typestate_reach(codegendata *cd, registerdata *rd,void *localbuf,
-                               basicblock *current,
+typestate_reach(verifier_state *state,
                                basicblock *destblock,
-                               stackptr ystack,typevector *yloc,
-                               int locsize,bool jsrencountered)
+                               stackptr ystack,typevector *yloc)
 {
        typevector *destloc;
        int destidx;
        bool changed = false;
+       typecheck_result r;
 
        LOG1("reaching block L%03d",destblock->debug_nr);
        TYPECHECK_COUNT(stat_reached);
        
-       destidx = destblock - cd->method->basicblocks;
-       destloc = MGET_TYPEVECTOR(localbuf,destidx,locsize);
+       destidx = destblock - state->cd->method->basicblocks;
+       destloc = MGET_TYPEVECTOR(state->localbuf,destidx,state->numlocals);
 
        /* When branching backwards we have to check for uninitialized objects */
        
-       if (destblock <= current) {
+       if (destblock <= state->bptr) {
                stackptr sp;
                int i;
 
@@ -603,19 +973,16 @@ typestate_reach(codegendata *cd, registerdata *rd,void *localbuf,
                        for (sp = ystack; sp; sp=sp->prev)
                                if (sp->type == TYPE_ADR &&
                                TYPEINFO_IS_NEWOBJECT(sp->typeinfo)) {
-                                       /*show_icmd_method(cd->method,cd,rd);*/
-                                       printf("current: %d, dest: %d\n", current->debug_nr, destblock->debug_nr);
-                                       log_text("Branching backwards with uninitialized object on stack");
-                                       /* XXX verify error */
-                                       assert(0);
-                       }
-
-                       for (i=0; i<locsize; ++i)
+                                       /*printf("current: %d, dest: %d\n", state->bptr->debug_nr, destblock->debug_nr);*/
+                                       *exceptionptr = new_verifyerror(state->m,"Branching backwards with uninitialized object on stack");
+                                       return false;
+                               }
+
+                       for (i=0; i<state->numlocals; ++i)
                                if (yloc->td[i].type == TYPE_ADR &&
                                        TYPEINFO_IS_NEWOBJECT(yloc->td[i].info)) {
-                                       log_text("Branching backwards with uninitialized object in local variable");
-                                       /* XXX verify error */
-                                       assert(0);
+                                       *exceptionptr = new_verifyerror(state->m,"Branching backwards with uninitialized object in local variable");
+                                       return false;
                                }
                }
        }
@@ -626,8 +993,9 @@ typestate_reach(codegendata *cd, registerdata *rd,void *localbuf,
                TYPECHECK_COUNT(stat_copied);
                LOG1("block (index %04d) reached first time",destidx);
                
-               typestack_copy(destblock->instack,ystack,yloc);
-               COPY_TYPEVECTORSET(yloc,destloc,locsize);
+               if (!typestack_copy(state,destblock->instack,ystack,yloc))
+                       return false;
+               typevectorset_copy_inplace(yloc,destloc,state->numlocals);
                changed = true;
        }
        else {
@@ -636,105 +1004,135 @@ typestate_reach(codegendata *cd, registerdata *rd,void *localbuf,
                TYPECHECK_COUNT(stat_merged);
                LOG1("block (index %04d) reached before",destidx);
                
-               changed = typestate_merge(destblock->instack,destloc,
-                                                                 ystack,yloc,locsize,
-                                                                 jsrencountered);
+               r = typestate_merge(state,destblock->instack,destloc,ystack,yloc);
+               if (r == typecheck_FAIL)
+                       return false;
+               changed = r;
                TYPECHECK_COUNTIF(changed,stat_merging_changed);
        }
 
        if (changed) {
                LOG("changed!");
                destblock->flags = BBTYPECHECK_REACHED;
-               if (destblock <= current) {LOG("REPEAT!"); return true;}
+               if (destblock <= state->bptr) {
+                       LOG("REPEAT!"); 
+                       state->repeat = true;
+               }
        }
-       return false;
+       return true;
 }
 
+/* typestate_ret ***************************************************************
+   Reach the destinations of a RET instruction.
+
+   IN:
+       state............current state of the verifier
+          retindex.........index of local variable containing the returnAddress
+
+   OUT:
+       state->repeat....set to true if the verifier must iterate again
+                           over the basic blocks
+          
+   RETURN VALUE:
+       true.............success
+          false............an exception has been thrown
+
+*******************************************************************************/
 
 static bool
-typestate_ret(codegendata *cd,registerdata *rd, void *localbuf,
-                         basicblock *current,
-                         stackptr ystack,typevector *yloc,
-                         int retindex,int locsize)
+typestate_ret(verifier_state *state,int retindex)
 {
        typevector *yvec;
        typevector *selected;
        basicblock *destblock;
-       bool repeat = false;
 
-       for (yvec=yloc; yvec; ) {
+       for (yvec=state->localset; yvec; ) {
                if (!TYPEDESC_IS_RETURNADDRESS(yvec->td[retindex])) {
-                       log_text("Illegal instruction: RET on non-returnAddress");
-                       /* XXX verify error */
-                       assert(0);
+                       *exceptionptr = new_verifyerror(state->m,"Illegal instruction: RET on non-returnAddress");
+                       return false;
                }
 
                destblock = (basicblock*) TYPEINFO_RETURNADDRESS(yvec->td[retindex].info);
 
                selected = typevectorset_select(&yvec,retindex,destblock);
                
-               repeat |= typestate_reach(cd, rd,  localbuf,current,destblock,
-                                                                 ystack,selected,locsize,true);
+               if (!typestate_reach(state,destblock,state->curstack,selected))
+                       return false;
        }
-       return repeat;
+       return true;
 }
 
-/****************************************************************************/
-/* MACROS FOR LOCAL VARIABLE CHECKING                                       */
-/****************************************************************************/
+/* typestate_save_instack ******************************************************
+   Save the input stack of the current basic block in the "savedstackbuf"
+   of the verifier state.
 
-#define INDEX_ONEWORD(num)                                                                             \
-       do { if((num)<0 || (num)>=state->validlocals)                           \
-                       TYPECHECK_VERIFYERROR_bool("Invalid local variable index"); } while (0)
-#define INDEX_TWOWORD(num)                                                                             \
-       do { if((num)<0 || ((num)+1)>=state->validlocals)                       \
-                       TYPECHECK_VERIFYERROR_bool("Invalid local variable index"); } while (0)
+   This function must be called before an instruction modifies a stack slot
+   that happens to be part of the instack of the current block. In such
+   cases the instack of the block must be saved, and restored at the end
+   of the analysis of this basic block, so that the instack again reflects
+   the *input* to this basic block (and does not randomly contain types
+   that appear within the block).
 
-#define STORE_ONEWORD(num,type)                                                                        \
-       do {typevectorset_store(state->localset,num,type,NULL);} while(0)
+   IN:
+       state............current state of the verifier
 
-#define STORE_TWOWORD(num,type)                                                                                \
-       do {typevectorset_store_twoword(state->localset,num,type);} while(0)
+*******************************************************************************/
 
+static void
+typestate_save_instack(verifier_state *state)
+{
+       stackptr sp;
+       stackptr dest;
+       s4 i;
+       
+       LOG("saving input stack types");
+       if (!state->savedstackbuf) {
+               LOG("allocating savedstack buffer");
+               state->savedstackbuf = DMNEW(stackelement, state->cd->maxstack);
+               state->savedstackbuf->prev = NULL;
+               for (i = 1; i < state->cd->maxstack; ++i)
+                       state->savedstackbuf[i].prev = state->savedstackbuf+(i-1);
+       }
+       sp = state->savedstack = state->bptr->instack;
+       dest = state->bptr->instack = state->savedstackbuf + (state->bptr->indepth-1);
+       
+       for(; sp; sp=sp->prev, dest=dest->prev) {
+               dest->type = sp->type;
+               TYPEINFO_COPY(sp->typeinfo,dest->typeinfo);
+       }
+}
 
-#ifdef TYPECHECK_VERBOSE
-#define WORDCHECKFAULT \
-       do { \
-               dolog("localset->td index: %ld\ninstruction belongs to:%s.%s, outermethod:%s.%s\n", \
-               state->iptr->op1,state->iptr->method->class->name->text, \
-                       state->iptr->method->name->text,state->m->class->name->text,state->m->name->text); \
-               show_icmd(state->iptr++, false); \
-               show_icmd(state->iptr, false); \
-       } while (0)
-#else
-#define WORDCHECKFAULT
-#endif
+/* typestate_restore_instack ***************************************************
+   Restore the input stack of the current basic block that has been previously
+   saved by `typestate_save_instack`.
+
+   IN:
+       state............current state of the verifier
 
+*******************************************************************************/
 
-#define CHECK_ONEWORD(num,tp)                                                                                  \
-       do {TYPECHECK_COUNT(stat_ins_primload);                                                         \
-               if (state->jsrencountered) {                                                                                    \
-                       if (!typevectorset_checktype(state->localset,num,tp)) {                         \
-                               WORDCHECKFAULT; \
-                               TYPECHECK_VERIFYERROR_bool("Variable type mismatch");                                           \
-                       }       \
-               }                                                                                                                               \
-               else {                                                                                                                  \
-                       if (state->localset->td[num].type != tp) {                                                      \
-                               TYPECHECK_VERIFYERROR_bool("Variable type mismatch");                                           \
-                               WORDCHECKFAULT; \
-                       } \
-               }                                                                                                                               \
-               } while(0)
-
-#define CHECK_TWOWORD(num,type)                                                                                        \
-       do {TYPECHECK_COUNT(stat_ins_primload);                                                         \
-               if (!typevectorset_checktype(state->localset,num,type)) {                \
-                       WORDCHECKFAULT; \
-                       TYPECHECK_VERIFYERROR_bool("Variable type mismatch");                           \
-               } \
-       } while(0)
+static void
+typestate_restore_instack(verifier_state *state)
+{
+       stackptr sp;
+       stackptr dest;
+       
+       TYPECHECK_COUNT(stat_savedstack);
+       LOG("restoring saved instack");
+
+       sp = state->bptr->instack;
+       dest = state->savedstack;
+       for(; sp; sp=sp->prev, dest=dest->prev) {
+               dest->type = sp->type;
+               TYPEINFO_COPY(sp->typeinfo,dest->typeinfo);
+       }
 
+       state->bptr->instack = state->savedstack;
+       state->savedstack = NULL;
+}
 
 /****************************************************************************/
 /* MISC MACROS                                                              */
@@ -746,72 +1144,6 @@ typestate_ret(codegendata *cd,registerdata *rd, void *localbuf,
 
 #define ISBUILTIN(v)   (bte->fp == (functionptr) (v))
 
-/* TYPECHECK_REACH: executed, when the target block (tbptr) can be reached
- *     from the current block (bptr). The types of local variables and
- *     stack slots are propagated to the target block.
- * Input:
- *     state......verifier state
- *     tbptr......target block
- *     dst........current output stack pointer
- * Output:
- *     state->repeat.....changed to true if a block before the current
- *                       block has changed
- */
-#define TYPECHECK_REACH                                                 \
-    do {                                                                \
-    state->repeat |= typestate_reach(state->cd,state->rd, state->localbuf,state->bptr,tbptr,dst,               \
-                                                         state->localset,state->numlocals,state->jsrencountered);       \
-    LOG("done.");                                                       \
-    } while (0)
-
-/* TYPECHECK_LEAVE: executed when the method is exited non-abruptly
- * Input:
- *     class........class of the current method
- *     state........verifier state
- */
-#define TYPECHECK_LEAVE                                                 \
-    do {                                                                \
-        if (state->initmethod && state->m->class != class_java_lang_Object) {         \
-            /* check the marker variable */                             \
-            LOG("Checking <init> marker");                              \
-            if (!typevectorset_checktype(state->localset,state->numlocals-1,TYPE_INT))\
-                TYPECHECK_VERIFYERROR_bool("<init> method does not initialize 'this'");      \
-        }                                                               \
-    } while (0)
-
-/****************************************************************************/
-/* VERIFIER STATE STRUCT                                                    */
-/****************************************************************************/
-
-/* verifier_state - This structure keeps the current state of the      */
-/* bytecode verifier for passing it between verifier functions.        */
-
-typedef struct verifier_state {
-    stackptr curstack;      /* input stack top for current instruction */
-    instruction *iptr;               /* pointer to current instruction */
-    basicblock *bptr;                /* pointer to current basic block */
-
-       methodinfo *m;                               /* the current method */
-       codegendata *cd;                 /* codegendata for current method */
-       registerdata *rd;               /* registerdata for current method */
-       
-       s4 numlocals;                         /* number of local variables */
-       s4 validlocals;                /* number of Java-accessible locals */
-       void *localbuf;       /* local variable types for each block start */
-       typevector *localset;        /* typevector set for local variables */
-       typedescriptor returntype;    /* return type of the current method */
-       
-       stackptr savedstackbuf;             /* buffer for saving the stack */
-       stackptr savedstack;             /* saved instack of current block */
-       
-    exceptiontable **handlers;            /* active exception handlers */
-       stackelement excstack;           /* instack for exception handlers */
-       
-    bool repeat;            /* if true, blocks are iterated over again */
-    bool initmethod;             /* true if this is an "<init>" method */
-       bool jsrencountered;                 /* true if we there was a JSR */
-} verifier_state;
-
 /* verify_invocation ***********************************************************
  
    Verify an ICMD_INVOKE* instruction.
@@ -841,7 +1173,6 @@ verify_invocation(verifier_state *state)
        stackelement *dst;               /* result stack of the invocation */
        int i;                                                  /* counter */
     u1 rtype;                          /* return type of called method */
-       static utf *name_init = NULL;     /* cache for "<init>" utf string */
 
        um = (unresolved_method *) state->iptr[0].target;
        mref = um->methodref;
@@ -850,38 +1181,16 @@ verify_invocation(verifier_state *state)
        opcode = state->iptr[0].opc;
        dst = state->iptr->dst;
 
-       if (!name_init)
-               name_init = utf_new_char("<init>");
-       
+       /* prevent compiler warnings */
+
+       ins = NULL;
+
        /* check whether we are calling <init> */
        
-       callinginit = (opcode == ICMD_INVOKESPECIAL && mref->name == name_init);
+       callinginit = (opcode == ICMD_INVOKESPECIAL && mref->name == utf_init);
        if (specialmethod && !callinginit)
                TYPECHECK_VERIFYERROR_bool("Invalid invocation of special method");
 
-       /* record subtype constraints for parameters */
-       
-       if (!constrain_unresolved_method(um,state->m->class,state->m,state->iptr,state->curstack))
-               return false; /* XXX maybe wrap exception */
-
-       /* try to resolve the method lazily */
-       
-       if (!resolve_method(um,resolveLazy,(methodinfo **) &(state->iptr[0].val.a)))
-               return false;
-
-#if 0
-       if (opcode == ICMD_INVOKESPECIAL) {
-               /* XXX for INVOKESPECIAL: check if the invokation is done at all */
-
-               /* (If callinginit the class is checked later.) */
-               if (!callinginit) { 
-                       /* XXX classrefs */
-                       if (!builtin_isanysubclass(myclass,mi->class)) 
-                               XXXTYPECHECK_VERIFYERROR_bool("Illegal instruction: INVOKESPECIAL calling non-superclass method"); 
-               } 
-       }
-#endif
-
        /* allocate parameters if necessary */
        
        if (!md->params)
@@ -910,12 +1219,19 @@ verify_invocation(verifier_state *state)
                                LOGINFO(&(stack->typeinfo));
                                ins = (instruction*)TYPEINFO_NEWOBJECT_INSTRUCTION(stack->typeinfo);
                                if (ins)
-                                       initclass = CLASSREF_OR_CLASSINFO(ins[-1].val.a);
+                                       initclass = CLASSREF_OR_CLASSINFO(ins[-1].target);
                                else
                                        initclass.cls = state->m->class;
                                LOGSTR("class: "); LOGNAME(initclass); LOGNL;
                        }
                }
+               else {
+                       /* non-adress argument. if this is the first argument and we are */
+                       /* invoking an instance method, this is an error.                */
+                       if (i==0 && opcode != ICMD_INVOKESTATIC) {
+                               TYPECHECK_VERIFYERROR_bool("Parameter type mismatch for 'this' argument");
+                       }
+               }
                LOG("ok");
 
                if (i)
@@ -947,21 +1263,7 @@ verify_invocation(verifier_state *state)
                                 * we are going to replace.
                                 */
                                if (stack <= state->bptr->instack && !state->savedstack)
-                               {
-                                       stackptr sp;
-                                       stackptr copy;
-                                       LOG("saving input stack types");
-                                       if (!state->savedstackbuf) {
-                                               LOG("allocating savedstack buffer");
-                                               state->savedstackbuf = DMNEW(stackelement, state->cd->maxstack);
-                                               state->savedstackbuf->prev = NULL;
-                                               for (i = 1; i < state->cd->maxstack; ++i)
-                                                       state->savedstackbuf[i].prev = state->savedstackbuf+(i-1);
-                                       }
-                                       sp = state->savedstack = state->bptr->instack;
-                                       copy = state->bptr->instack = state->savedstackbuf + (state->bptr->indepth-1);
-                                       TYPESTACK_COPY(sp,copy);
-                               }
+                                       typestate_save_instack(state);
 
                                if (!typeinfo_init_class(&(stack->typeinfo),initclass))
                                        return false;
@@ -974,34 +1276,112 @@ verify_invocation(verifier_state *state)
 
                /* initializing the 'this' reference? */
                if (!ins) {
+                       classinfo *cls;
                        TYPECHECK_ASSERT(state->initmethod);
-                       /* must be <init> of current class or direct superclass */
-                       /* XXX check with classrefs */
-#if 0
-                       if (mi->class != m->class && mi->class != m->class->super.cls)
+                       /* { we are initializing the 'this' reference }                           */
+                       /* must be <init> of current class or direct superclass                   */
+                       /* the current class is linked, so must be its superclass. thus we can be */
+                       /* sure that resolving will be trivial.                                   */
+                       if (!resolve_classref(state->m,mref->classref,resolveLazy,false,true,&cls))
+                               return false; /* exception */
+
+                       /* if lazy resolving did not succeed, it's not one of the allowed classes */
+                       /* otherwise we check it directly                                         */
+                       if (cls == NULL || (cls != state->m->class && cls != state->m->class->super.cls)) {
                                TYPECHECK_VERIFYERROR_bool("<init> calling <init> of the wrong class");
-#endif
+                       }
 
                        /* set our marker variable to type int */
                        LOG("setting <init> marker");
                        typevectorset_store(state->localset,state->numlocals-1,TYPE_INT,NULL);
                }
                else {
-                       /* initializing an instance created with NEW */
-                       /* XXX is this strictness ok? */
-                       /* XXX check with classrefs */
-#if 0
-                       if (mi->class != initclass.cls)
-                               TYPECHECK_VERIFYERROR_bool("Calling <init> method of the wrong class");
-#endif
+                       /* { we are initializing an instance created with NEW } */
+                       if ((IS_CLASSREF(initclass) ? initclass.ref->name : initclass.cls->name) != mref->classref->name) {
+                               TYPECHECK_VERIFYERROR_bool("wrong <init> called for uninitialized reference");
+                       }
+               }
+       }
+
+       /* record subtype constraints for parameters */
+       
+       if (!constrain_unresolved_method(um,state->m->class,state->m,state->iptr,state->curstack))
+               return false; /* XXX maybe wrap exception */
+
+       /* try to resolve the method lazily */
+       
+       if (!resolve_method(um,resolveLazy,(methodinfo **) &(state->iptr[0].val.a)))
+               return false;
+
+       return true;
+}
+
+/* verify_generic_builtin ******************************************************
+   Verify the call of a generic builtin method.
+  
+   IN:
+       state............the current state of the verifier
+
+   RETURN VALUE:
+       true.............successful verification,
+          false............an exception has been thrown.
+
+*******************************************************************************/
+
+static bool
+verify_generic_builtin(verifier_state *state)
+{
+       builtintable_entry *bte;
+       s4 i;
+       u1 rtype;
+       methoddesc *md;
+    stackptr sp;
+
+       TYPECHECK_COUNT(stat_ins_builtin_gen);
+
+       bte = (builtintable_entry *) state->iptr[0].val.a;
+       md = bte->md;
+       i = md->paramcount;
+       
+       /* check the types of the arguments on the stack */
+
+       sp = state->curstack;
+       for (i--; i >= 0; i--) {
+               if (sp->type != md->paramtypes[i].type) {
+                       TYPECHECK_VERIFYERROR_bool("parameter type mismatch for builtin method");
+               }
+               
+#ifdef TYPECHECK_DEBUG
+               /* generic builtins may only take primitive types and java.lang.Object references */
+               if (sp->type == TYPE_ADR && md->paramtypes[i].classref->name != utf_java_lang_Object) {
+                       *exceptionptr = new_internalerror("generic builtin method with non-generic reference parameter");
+                       return false;
                }
+#endif
+               
+               sp = sp->prev;
+       }
+
+       /* check the return type */
+
+       rtype = md->returntype.type;
+       if (rtype != TYPE_VOID) {
+               stackptr dst;
+
+               dst = state->iptr->dst;
+               if (rtype != dst->type)
+                       TYPECHECK_VERIFYERROR_bool("Return type mismatch in generic builtin invocation");
+               if (!typeinfo_init_from_typedesc(&(md->returntype),NULL,&(dst->typeinfo)))
+                       return false;
        }
+
        return true;
 }
 
 /* verify_builtin **************************************************************
  
-   Verify the call of a builtin function.
+   Verify the call of a builtin method.
   
    IN:
        state............the current state of the verifier
@@ -1016,22 +1396,19 @@ static bool
 verify_builtin(verifier_state *state)
 {
        builtintable_entry *bte;
-    classinfo *cls;
+    classref_or_classinfo cls;
     stackptr dst;               /* output stack of current instruction */
 
        bte = (builtintable_entry *) state->iptr[0].val.a;
        dst = state->iptr->dst;
 
-       if (ISBUILTIN(BUILTIN_new) || ISBUILTIN(PATCHER_builtin_new)) {
+       /* XXX this is an ugly if-chain but twisti did not want a function */
+       /* pointer in builtintable_entry for this, so here you go.. ;)     */
+
+       if (ISBUILTIN(BUILTIN_new)) {
                if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_new without classinfo");
-               cls = (classinfo *) state->iptr[-1].val.a;
-#ifdef XXX
-               TYPECHECK_ASSERT(!cls || cls->linked);
-               /* The following check also forbids array classes and interfaces: */
-               if ((cls->flags & ACC_ABSTRACT) != 0)
-                       TYPECHECK_VERIFYERROR_bool("Invalid instruction: NEW creating instance of abstract class");
-#endif
+                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_new without class");
+               cls.any = state->iptr[-1].target;
                TYPEINFO_INIT_NEWOBJECT(dst->typeinfo,state->iptr);
        }
        else if (ISBUILTIN(BUILTIN_newarray_boolean)) {
@@ -1067,91 +1444,97 @@ verify_builtin(verifier_state *state)
                TYPEINFO_INIT_PRIMITIVE_ARRAY(dst->typeinfo,ARRAYTYPE_LONG);
        }
        else if (ISBUILTIN(BUILTIN_newarray))
-       {
-               vftbl_t *vft;
-               TYPECHECK_INT(state->curstack->prev);
-               if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_newarray without classinfo");
-               vft = (vftbl_t *)state->iptr[-1].val.a;
-               if (!vft)
-                       TYPECHECK_VERIFYERROR_bool("ANEWARRAY with unlinked class");
-               if (!vft->arraydesc)
-                       TYPECHECK_VERIFYERROR_bool("ANEWARRAY with non-array class");
-               TYPEINFO_INIT_CLASSINFO(dst->typeinfo,vft->class);
-       }
-       else if (ISBUILTIN(PATCHER_builtin_newarray))
        {
                TYPECHECK_INT(state->curstack->prev);
-               if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_newarray without classinfo");
-               if (!typeinfo_init_class(&(dst->typeinfo),CLASSREF_OR_CLASSINFO(state->iptr[-1].val.a)))
-                       return false;
-       }
-       else if (ISBUILTIN(BUILTIN_newarray))
-       {
-               vftbl_t *vft;
-               TYPECHECK_INT(state->curstack->prev);
-               if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_newarray without classinfo");
-               vft = (vftbl_t *)state->iptr[-1].val.a;
-               if (!vft)
-                       TYPECHECK_VERIFYERROR_bool("ANEWARRAY with unlinked class");
-               if (!vft->arraydesc)
-                       TYPECHECK_VERIFYERROR_bool("ANEWARRAY with non-array class");
-               TYPEINFO_INIT_CLASSINFO(dst->typeinfo,vft->class);
+               if (state->iptr[-1].opc != ICMD_ACONST || !state->iptr[-1].target)
+                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_newarray without class");
+               /* XXX check that it is an array class(ref) */
+               typeinfo_init_class(&(dst->typeinfo),CLASSREF_OR_CLASSINFO(state->iptr[-1].target));
        }
        else if (ISBUILTIN(BUILTIN_arrayinstanceof))
        {
-               vftbl_t *vft;
                TYPECHECK_ADR(state->curstack->prev);
                if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_arrayinstanceof without classinfo");
-               vft = (vftbl_t *)state->iptr[-1].val.a;
-               if (!vft)
-                       TYPECHECK_VERIFYERROR_bool("INSTANCEOF with unlinked class");
-               if (!vft->arraydesc)
-                       TYPECHECK_VERIFYERROR_bool("internal error: builtin_arrayinstanceof with non-array class");
+                       TYPECHECK_VERIFYERROR_bool("illegal instruction: builtin_arrayinstanceof without class");
+               /* XXX check that it is an array class(ref) */
        }
-       else if (ISBUILTIN(BUILTIN_arraycheckcast)) {
-               vftbl_t *vft;
-               TYPECHECK_ADR(state->curstack->prev);
-               if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: BUILTIN_arraycheckcast without classinfo");
-               vft = (vftbl_t *)state->iptr[-1].val.a;
-               if (!vft)
-                       TYPECHECK_VERIFYERROR_bool("CHECKCAST with unlinked class");
-               if (!vft->arraydesc)
-                       TYPECHECK_VERIFYERROR_bool("internal error: builtin_arraycheckcast with non-array class");
-               TYPEINFO_INIT_CLASSINFO(dst->typeinfo,vft->class);
+       else {
+               return verify_generic_builtin(state);
        }
-       else if (ISBUILTIN(PATCHER_builtin_arraycheckcast)) {
-               TYPECHECK_ADR(state->curstack->prev);
-               if (state->iptr[-1].opc != ICMD_ACONST)
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: BUILTIN_arraycheckcast without classinfo");
-               if (!typeinfo_init_class(&(dst->typeinfo),CLASSREF_OR_CLASSINFO(state->iptr[-1].val.a)))
-                       return false;
+       return true;
+}
+
+/* verify_multianewarray *******************************************************
+   Verify a MULTIANEWARRAY instruction.
+  
+   IN:
+       state............the current state of the verifier
+
+   RETURN VALUE:
+       true.............successful verification,
+          false............an exception has been thrown.
+
+*******************************************************************************/
+
+static bool
+verify_multianewarray(verifier_state *state)
+{
+    stackptr sp;
+       classinfo *arrayclass;
+       arraydescriptor *desc;
+       s4 i;
+
+       /* check the array lengths on the stack */
+       i = state->iptr[0].op1;
+       if (i < 1)
+               TYPECHECK_VERIFYERROR_bool("Illegal dimension argument");
+
+       sp = state->curstack;
+       while (i--) {
+               if (!sp)
+                       TYPECHECK_VERIFYERROR_bool("Unable to pop operand off an empty stack");
+               TYPECHECK_INT(sp);
+               sp = sp->prev;
        }
-       else if (ISBUILTIN(BUILTIN_aastore)) {
-               TYPECHECK_ADR(state->curstack);
-               TYPECHECK_INT(state->curstack->prev);
-               TYPECHECK_ADR(state->curstack->prev->prev);
-               if (!TYPEINFO_MAYBE_ARRAY_OF_REFS(state->curstack->prev->prev->typeinfo))
-                       TYPECHECK_VERIFYERROR_bool("illegal instruction: AASTORE to non-reference array");
+
+       /* check array descriptor */
+       if (state->iptr[0].val.a != NULL) {
+               /* the array class reference has already been resolved */
+               arrayclass = (classinfo *) state->iptr[0].val.a;
+               if (!arrayclass)
+                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY with unlinked class");
+               if ((desc = arrayclass->vftbl->arraydesc) == NULL)
+                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY with non-array class");
+               if (desc->dimension < state->iptr[0].op1)
+                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY dimension to high");
+
+               /* set the array type of the result */
+               typeinfo_init_classinfo(&(state->iptr->dst->typeinfo), arrayclass);
        }
        else {
-#if 0
-               /* XXX put these checks in a function */
-               TYPECHECK_COUNT(stat_ins_builtin_gen);
-               builtindesc = builtin_desc;
-               while (builtindesc->opcode && builtindesc->builtin
-                               != state->iptr->val.fp) builtindesc++;
-               if (!builtindesc->opcode) {
-                       dolog("Builtin not in table: %s",icmd_builtin_name(state->iptr->val.fp));
-                       TYPECHECK_ASSERT(false);
-               }
-               TYPECHECK_ARGS3(builtindesc->type_s3,builtindesc->type_s2,builtindesc->type_s1);
-#endif
+               const char *p;
+               constant_classref *cr;
+               
+               /* the array class reference is still unresolved */
+               /* check that the reference indicates an array class of correct dimension */
+               cr = (constant_classref *) state->iptr[0].target;
+               i = 0;
+               p = cr->name->text;
+               while (p[i] == '[')
+                       i++;
+               /* { the dimension of the array class == i } */
+               if (i < 1)
+                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY with non-array class");
+               if (i < state->iptr[0].op1)
+                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY dimension to high");
+
+               /* set the array type of the result */
+               if (!typeinfo_init_class(&(state->iptr->dst->typeinfo),CLASSREF_OR_CLASSINFO(state->iptr[0].target)))
+                       return false;
        }
+
+       /* everything ok */
        return true;
 }
 
@@ -1171,7 +1554,6 @@ verify_builtin(verifier_state *state)
 static bool
 verify_basic_block(verifier_state *state)
 {
-    stackptr srcstack;         /* source stack for copying and merging */
     int opcode;                                      /* current opcode */
     int len;                        /* for counting instructions, etc. */
     bool superblockend;        /* true if no fallthrough to next block */
@@ -1185,6 +1567,7 @@ verify_basic_block(verifier_state *state)
        fieldinfo **fieldinfop;                      /* for field accesses */
        s4 i;
        s4 b_index;
+       typecheck_result r;
 
        LOGSTR1("\n---- BLOCK %04d ------------------------------------------------\n",state->bptr->debug_nr);
        LOGFLUSH;
@@ -1196,6 +1579,10 @@ verify_basic_block(verifier_state *state)
        /* init stack at the start of this block */
        state->curstack = state->bptr->instack;
 
+       /* prevent compiler warnings */
+
+       dst = NULL;
+
        /* determine the active exception handlers for this block */
        /* XXX could use a faster algorithm with sorted lists or  */
        /* something?                                             */
@@ -1209,11 +1596,11 @@ verify_basic_block(verifier_state *state)
        state->handlers[len] = NULL;
 
        /* init variable types at the start of this block */
-       COPY_TYPEVECTORSET(MGET_TYPEVECTOR(state->localbuf,b_index,state->numlocals),
+       typevectorset_copy_inplace(MGET_TYPEVECTOR(state->localbuf,b_index,state->numlocals),
                        state->localset,state->numlocals);
 
        /* XXX FIXME FOR INLINING */
-       if(!useinlining) {
+       if (!useinlining) {
                if (state->handlers[0])
                        for (i=0; i<state->numlocals; ++i)
                                if (state->localset->td[i].type == TYPE_ADR
@@ -1226,7 +1613,7 @@ verify_basic_block(verifier_state *state)
                                        /* of eclipse 3.0.2                                                  */
                                        if (TYPEINFO_NEWOBJECT_INSTRUCTION(state->localset->td[i].info) != NULL) {
                                                /*show_icmd_method(state->m, state->cd, state->rd);*/
-                                               printf("Uninitialized variale: %d, block: %d\n", i, state->bptr->debug_nr);
+                                               printf("Uninitialized variable: %d, block: %d\n", i, state->bptr->debug_nr);
                                                TYPECHECK_VERIFYERROR_bool("Uninitialized object in local variable inside try block");
                                        }
                                }
@@ -1265,16 +1652,19 @@ verify_basic_block(verifier_state *state)
                         */
 
                        case ICMD_DUP:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst);
                                break;
 
                        case ICMD_DUP_X1:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst);
                                COPYTYPE(state->curstack,dst-2);
                                COPYTYPE(state->curstack->prev,dst-1);
                                break;
 
                        case ICMD_DUP_X2:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst);
                                COPYTYPE(state->curstack,dst-3);
                                COPYTYPE(state->curstack->prev,dst-1);
@@ -1282,11 +1672,13 @@ verify_basic_block(verifier_state *state)
                                break;
 
                        case ICMD_DUP2:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst);
                                COPYTYPE(state->curstack->prev,dst-1);
                                break;
 
                        case ICMD_DUP2_X1:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst);
                                COPYTYPE(state->curstack->prev,dst-1);
                                COPYTYPE(state->curstack,dst-3);
@@ -1295,6 +1687,7 @@ verify_basic_block(verifier_state *state)
                                break;
 
                        case ICMD_DUP2_X2:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst);
                                COPYTYPE(state->curstack->prev,dst-1);
                                COPYTYPE(state->curstack,dst-4);
@@ -1304,6 +1697,7 @@ verify_basic_block(verifier_state *state)
                                break;
 
                        case ICMD_SWAP:
+                               TYPECHECK_COUNT(stat_ins_stack);
                                COPYTYPE(state->curstack,dst-1);
                                COPYTYPE(state->curstack->prev,dst);
                                break;
@@ -1311,16 +1705,26 @@ verify_basic_block(verifier_state *state)
                                /****************************************/
                                /* PRIMITIVE VARIABLE ACCESS            */
 
-                       case ICMD_ILOAD: CHECK_ONEWORD(state->iptr->op1,TYPE_INT); break;
-                       case ICMD_FLOAD: CHECK_ONEWORD(state->iptr->op1,TYPE_FLOAT); break;
-                       case ICMD_IINC:  CHECK_ONEWORD(state->iptr->op1,TYPE_INT); break;
-                       case ICMD_LLOAD: CHECK_TWOWORD(state->iptr->op1,TYPE_LONG); break;
-                       case ICMD_DLOAD: CHECK_TWOWORD(state->iptr->op1,TYPE_DOUBLE); break;
-
-                       case ICMD_FSTORE: STORE_ONEWORD(state->iptr->op1,TYPE_FLOAT); break;
-                       case ICMD_ISTORE: STORE_ONEWORD(state->iptr->op1,TYPE_INT); break;
-                       case ICMD_LSTORE: STORE_TWOWORD(state->iptr->op1,TYPE_LONG); break;
-                       case ICMD_DSTORE: STORE_TWOWORD(state->iptr->op1,TYPE_DOUBLE); break;
+                       case ICMD_ILOAD: if (!typevectorset_checktype(state->localset,state->iptr->op1,TYPE_INT)) 
+                                                                TYPECHECK_VERIFYERROR_bool("Local variable type mismatch");
+                                                        break;
+                       case ICMD_IINC:  if (!typevectorset_checktype(state->localset,state->iptr->op1,TYPE_INT))
+                                                                TYPECHECK_VERIFYERROR_bool("Local variable type mismatch");
+                                                        break;
+                       case ICMD_FLOAD: if (!typevectorset_checktype(state->localset,state->iptr->op1,TYPE_FLOAT))
+                                                                TYPECHECK_VERIFYERROR_bool("Local variable type mismatch");
+                                                        break;
+                       case ICMD_LLOAD: if (!typevectorset_checktype(state->localset,state->iptr->op1,TYPE_LONG))
+                                                                TYPECHECK_VERIFYERROR_bool("Local variable type mismatch");
+                                                        break;
+                       case ICMD_DLOAD: if (!typevectorset_checktype(state->localset,state->iptr->op1,TYPE_DOUBLE))
+                                                                TYPECHECK_VERIFYERROR_bool("Local variable type mismatch");
+                                                        break;
+
+                       case ICMD_ISTORE: typevectorset_store(state->localset,state->iptr->op1,TYPE_INT,NULL); break;
+                       case ICMD_FSTORE: typevectorset_store(state->localset,state->iptr->op1,TYPE_FLOAT,NULL); break;
+                       case ICMD_LSTORE: typevectorset_store_twoword(state->localset,state->iptr->op1,TYPE_LONG); break;
+                       case ICMD_DSTORE: typevectorset_store_twoword(state->localset,state->iptr->op1,TYPE_DOUBLE); break;
 
                                /****************************************/
                                /* LOADING ADDRESS FROM VARIABLE        */
@@ -1333,7 +1737,8 @@ verify_basic_block(verifier_state *state)
                                        if (!typevectorset_checkreference(state->localset,state->iptr->op1)) {
                                                TYPECHECK_VERIFYERROR_bool("illegal instruction: ALOAD loading non-reference");
                                        }
-                                       typevectorset_copymergedtype(state->localset,state->iptr->op1,&(dst->typeinfo));
+                                       if (typevectorset_copymergedtype(state->m,state->localset,state->iptr->op1,&(dst->typeinfo)) == -1)
+                                               return false;
                                }
                                else {
                                        if (!TYPEDESC_IS_REFERENCE(state->localset->td[state->iptr->op1])) {
@@ -1382,7 +1787,7 @@ verify_basic_block(verifier_state *state)
                                uf = INSTRUCTION_PUTCONST_FIELDREF(state->iptr);
                                fieldinfop = INSTRUCTION_PUTCONST_FIELDINFO_PTR(state->iptr);
 
-                               goto putfield_tail;
+                               goto fieldaccess_tail;
 
                        case ICMD_PUTFIELD:
                        case ICMD_PUTSTATIC:
@@ -1390,36 +1795,34 @@ verify_basic_block(verifier_state *state)
 
                                uf = (unresolved_field *) state->iptr[0].target;
                                fieldinfop = (fieldinfo **) &(state->iptr[0].val.a);
-putfield_tail:
-                               /* record the subtype constraints for this field access */
-                               if (!constrain_unresolved_field(uf,state->m->class,state->m,state->iptr,state->curstack))
-                                       return false; /* XXX maybe wrap exception? */
-
-                               /* try to resolve the field reference */
-                               if (!resolve_field(uf,resolveLazy,fieldinfop))
-                                       return false;
-                               maythrow = true;
-                               break;
+                               
+                               goto fieldaccess_tail;
 
                        case ICMD_GETFIELD:
                        case ICMD_GETSTATIC:
                                TYPECHECK_COUNT(stat_ins_field);
 
                                uf = (unresolved_field *) state->iptr[0].target;
+                               fieldinfop = (fieldinfo **) &(state->iptr[0].val.a);
+
+                               /* the result is pushed on the stack */
+                               if (dst->type == TYPE_ADR) {
+                                       if (!typeinfo_init_from_typedesc(uf->fieldref->parseddesc.fd,NULL,&(dst->typeinfo)))
+                                               return false;
+                               }
 
+fieldaccess_tail:
                                /* record the subtype constraints for this field access */
                                if (!constrain_unresolved_field(uf,state->m->class,state->m,state->iptr,state->curstack))
                                        return false; /* XXX maybe wrap exception? */
 
                                /* try to resolve the field reference */
-                               if (!resolve_field(uf,resolveLazy,(fieldinfo **) &(state->iptr[0].val.a)))
+                               if (!resolve_field(uf,resolveLazy,fieldinfop))
                                        return false;
 
-                               /* the result is pushed on the stack */
-                               if (dst->type == TYPE_ADR) {
-                                       if (!typeinfo_init_from_typedesc(uf->fieldref->parseddesc.fd,NULL,&(dst->typeinfo)))
-                                               return false;
-                               }
+                               TYPECHECK_COUNTIF(!*fieldinfop,stat_ins_field_unresolved);
+                               TYPECHECK_COUNTIF(*fieldinfop && !(*fieldinfop)->class->initialized,stat_ins_field_uninitialized);
+                                       
                                maythrow = true;
                                break;
 
@@ -1507,6 +1910,19 @@ putfield_tail:
                                maythrow = true;
                                break;
 
+                       case ICMD_AASTORE:
+                               /* we just check the basic input types and that the           */
+                               /* destination is an array of references. Assignability to    */
+                               /* the actual array must be checked at runtime, each time the */
+                               /* instruction is performed. (See builtin_canstore.)          */
+                               TYPECHECK_ADR(state->curstack);
+                               TYPECHECK_INT(state->curstack->prev);
+                               TYPECHECK_ADR(state->curstack->prev->prev);
+                               if (!TYPEINFO_MAYBE_ARRAY_OF_REFS(state->curstack->prev->prev->typeinfo))
+                                       TYPECHECK_VERIFYERROR_bool("illegal instruction: AASTORE to non-reference array");
+                               maythrow = true;
+                               break;
+
                        case ICMD_IASTORECONST:
                                if (!TYPEINFO_MAYBE_PRIMITIVE_ARRAY(state->curstack->prev->typeinfo, ARRAYTYPE_INT))
                                        TYPECHECK_VERIFYERROR_bool("Array type mismatch");
@@ -1542,11 +1958,18 @@ putfield_tail:
                                /* ADDRESS CONSTANTS                    */
 
                        case ICMD_ACONST:
-                               if (state->iptr->val.a == NULL)
-                                       TYPEINFO_INIT_NULLTYPE(dst->typeinfo);
-                               else
-                                       /* string constant (or constant for builtin function) */
-                                       TYPEINFO_INIT_CLASSINFO(dst->typeinfo,class_java_lang_String);
+                               if (state->iptr->target) {
+                                       /* a java.lang.Class reference */
+                                       TYPEINFO_INIT_JAVA_LANG_CLASS(dst->typeinfo,(constant_classref *)state->iptr->target);
+                               }
+                               else {
+                                       if (state->iptr->val.a == NULL)
+                                               TYPEINFO_INIT_NULLTYPE(dst->typeinfo);
+                                       else {
+                                               /* string constant (or constant for builtin function) */
+                                               typeinfo_init_classinfo(&(dst->typeinfo),class_java_lang_String);
+                                       }
+                               }
                                break;
 
                                /****************************************/
@@ -1560,7 +1983,7 @@ putfield_tail:
 
                                cls = (classinfo *) state->iptr[0].val.a;
                                if (cls)
-                                       TYPEINFO_INIT_CLASSINFO(dst->typeinfo,cls);
+                                       typeinfo_init_classinfo(&(dst->typeinfo),cls);
                                else
                                        if (!typeinfo_init_class(&(dst->typeinfo),CLASSREF_OR_CLASSINFO(state->iptr[0].target)))
                                                return false;
@@ -1612,7 +2035,8 @@ putfield_tail:
                                tbptr = (basicblock *) state->iptr->target;
 
                                /* propagate stack and variables to the target block */
-                               TYPECHECK_REACH;
+                               if (!typestate_reach(state,tbptr,dst,state->localset))
+                                       return false;
                                break;
 
                                /****************************************/
@@ -1641,7 +2065,8 @@ switch_instruction_tail:
                                while (--i >= 0) {
                                        tbptr = *tptr++;
                                        LOG2("target %d is block %04d",(tptr-(basicblock **)state->iptr->target)-1,tbptr->debug_nr);
-                                       TYPECHECK_REACH;
+                                       if (!typestate_reach(state,tbptr,dst,state->localset))
+                                               return false;
                                }
                                LOG("switch done");
                                superblockend = true;
@@ -1651,22 +2076,46 @@ switch_instruction_tail:
                                /* ADDRESS RETURNS AND THROW            */
 
                        case ICMD_ATHROW:
-                               /* XXX lazy loading */
-                               if (!typeinfo_is_assignable_to_class(
-                                                       &state->curstack->typeinfo,CLASSREF_OR_CLASSINFO(class_java_lang_Throwable)))
+                               TYPECHECK_COUNT(stat_ins_athrow);
+                               r = typeinfo_is_assignable_to_class(&state->curstack->typeinfo,
+                                               CLASSREF_OR_CLASSINFO(class_java_lang_Throwable));
+                               if (r == typecheck_FALSE)
                                        TYPECHECK_VERIFYERROR_bool("illegal instruction: ATHROW on non-Throwable");
+                               if (r == typecheck_FAIL)
+                                       return false;
+                               if (r == typecheck_MAYBE) {
+                                       /* the check has to be postponed. we need a patcher */
+                                       TYPECHECK_COUNT(stat_ins_athrow_unresolved);
+                                       state->iptr->val.a = create_unresolved_class(
+                                                       state->m, 
+                                                       /* XXX make this more efficient, use class_java_lang_Throwable
+                                                        * directly */
+                                                       class_get_classref(state->m->class,utf_java_lang_Throwable),
+                                                       &state->curstack->typeinfo);
+                               }
                                superblockend = true;
                                maythrow = true;
                                break;
 
                        case ICMD_ARETURN:
-                               /* XXX lazy loading */
+                               TYPECHECK_COUNT(stat_ins_areturn);
                                if (!TYPEINFO_IS_REFERENCE(state->curstack->typeinfo))
                                        TYPECHECK_VERIFYERROR_bool("illegal instruction: ARETURN on non-reference");
 
                                if (state->returntype.type != TYPE_ADDRESS
-                                               || !typeinfo_is_assignable(&state->curstack->typeinfo,&(state->returntype.info)))
+                                               || (r = typeinfo_is_assignable(&state->curstack->typeinfo,&(state->returntype.info))) 
+                                                               == typecheck_FALSE)
                                        TYPECHECK_VERIFYERROR_bool("Return type mismatch");
+                               if (r == typecheck_FAIL)
+                                       return false;
+                               if (r == typecheck_MAYBE) {
+                                       /* the check has to be postponed, we need a patcher */
+                                       TYPECHECK_COUNT(stat_ins_areturn_unresolved);
+                                       state->iptr->val.a = create_unresolved_class(
+                                                       state->m, 
+                                                       state->m->parseddesc->returntype.classref,
+                                                       &state->curstack->typeinfo);
+                               }
                                goto return_tail;
 
                                /****************************************/
@@ -1691,7 +2140,15 @@ switch_instruction_tail:
                        case ICMD_RETURN:
                                if (state->returntype.type != TYPE_VOID) TYPECHECK_VERIFYERROR_bool("Return type mismatch");
 return_tail:
-                               TYPECHECK_LEAVE;
+                               TYPECHECK_COUNT(stat_ins_primitive_return);
+
+                               if (state->initmethod && state->m->class != class_java_lang_Object) {
+                                       /* Check if the 'this' instance has been initialized. */
+                                       LOG("Checking <init> marker");
+                                       if (!typevectorset_checktype(state->localset,state->numlocals-1,TYPE_INT))
+                                               TYPECHECK_VERIFYERROR_bool("<init> method does not initialize 'this'");
+                               }
+
                                superblockend = true;
                                maythrow = true;
                                break;
@@ -1713,8 +2170,8 @@ return_tail:
                                if (state->bptr + 1 == (state->m->basicblocks + state->m->basicblockcount + 1))
                                        TYPECHECK_VERIFYERROR_bool("Illegal instruction: JSR at end of bytecode");
                                typestack_put_retaddr(dst,state->bptr+1,state->localset);
-                               state->repeat |= typestate_reach(state->cd, state->rd,state->localbuf,state->bptr,tbptr,dst,
-                                               state->localset,state->numlocals,true);
+                               if (!typestate_reach(state,tbptr,dst,state->localset))
+                                       return false;
 
                                superblockend = true;
                                break;
@@ -1724,8 +2181,8 @@ return_tail:
                                if (!typevectorset_checkretaddr(state->localset,state->iptr->op1))
                                        TYPECHECK_VERIFYERROR_bool("illegal instruction: RET using non-returnAddress variable");
 
-                               state->repeat |= typestate_ret(state->cd,state->rd, state->localbuf,state->bptr,state->curstack,
-                                               state->localset,state->iptr->op1,state->numlocals);
+                               if (!typestate_ret(state,state->iptr->op1))
+                                       return false;
 
                                superblockend = true;
                                break;
@@ -1740,6 +2197,7 @@ return_tail:
                                TYPECHECK_COUNT(stat_ins_invoke);
                                if (!verify_invocation(state))
                                        return false;
+                               TYPECHECK_COUNTIF(!state->iptr[0].val.a,stat_ins_invoke_unresolved);
                                maythrow = true;
                                break;
 
@@ -1747,41 +2205,8 @@ return_tail:
                                /* MULTIANEWARRAY                       */
 
                        case ICMD_MULTIANEWARRAY:
-                               {
-                                       vftbl_t *arrayvftbl;
-                                       arraydescriptor *desc;
-
-                                       /* check the array lengths on the stack */
-                                       i = state->iptr[0].op1;
-                                       if (i < 1)
-                                               TYPECHECK_VERIFYERROR_bool("Illegal dimension argument");
-                                       srcstack = state->curstack;
-                                       while (i--) {
-                                               if (!srcstack)
-                                                       TYPECHECK_VERIFYERROR_bool("Unable to pop operand off an empty stack");
-                                               TYPECHECK_INT(srcstack);
-                                               srcstack = srcstack->prev;
-                                       }
-
-                                       /* check array descriptor */
-                                       if (state->iptr[0].target == NULL) {
-                                               arrayvftbl = (vftbl_t*) state->iptr[0].val.a;
-                                               if (!arrayvftbl)
-                                                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY with unlinked class");
-                                               if ((desc = arrayvftbl->arraydesc) == NULL)
-                                                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY with non-array class");
-                                               if (desc->dimension < state->iptr[0].op1)
-                                                       TYPECHECK_VERIFYERROR_bool("MULTIANEWARRAY dimension to high");
-
-                                               /* set the array type of the result */
-                                               TYPEINFO_INIT_CLASSINFO(dst->typeinfo,arrayvftbl->class);
-                                       }
-                                       else {
-                                               /* XXX do checks in patcher */
-                                               if (!typeinfo_init_class(&(dst->typeinfo),CLASSREF_OR_CLASSINFO(state->iptr[0].val.a)))
-                                                       return false;
-                                       }
-                               }
+                               if (!verify_multianewarray(state))
+                                       return false;           
                                maythrow = true;
                                break;
 
@@ -1798,11 +2223,6 @@ return_tail:
                                /****************************************/
                                /* SIMPLE EXCEPTION THROWING TESTS      */
 
-                       case ICMD_CHECKASIZE:
-                               /* The argument to CHECKASIZE is typechecked by
-                                * typechecking the array creation instructions. */
-
-                               /* FALLTHROUGH! */
                        case ICMD_CHECKNULL:
                                /* CHECKNULL just requires that the stack top
                                 * is an address. This is checked in stack.c */
@@ -1819,7 +2239,6 @@ return_tail:
                        case ICMD_ANEWARRAY:
                        case ICMD_MONITORENTER:
                        case ICMD_MONITOREXIT:
-                       case ICMD_AASTORE:
                                LOG2("ICMD %d at %d\n", state->iptr->opc, (int)(state->iptr-state->bptr->iinstr));
                                LOG("Should have been converted to builtin function call.");
                                TYPECHECK_ASSERT(false);
@@ -1840,7 +2259,9 @@ return_tail:
                                 * Instructions below...
                                 *     *) don't operate on local variables,
                                 *     *) don't operate on references,
-                                *     *) don't operate on returnAddresses.
+                                *     *) don't operate on returnAddresses,
+                                *     *) don't affect control flow (except
+                                *        by throwing exceptions).
                                 *
                                 * (These instructions are typechecked in
                                 *  analyse_stack.)
@@ -1895,10 +2316,8 @@ return_tail:
                        case ICMD_LSHL:
                        case ICMD_LSHR:
                        case ICMD_LUSHR:
-#if 0
-                       case ICMD_IREM0X10001:
-                       case ICMD_LREM0X10001:
-#endif
+                       case ICMD_IMULPOW2:
+                       case ICMD_LMULPOW2:
                        case ICMD_IDIVPOW2:
                        case ICMD_LDIVPOW2:
                        case ICMD_IADDCONST:
@@ -1960,7 +2379,6 @@ return_tail:
 
 
                                /*XXX What shall we do with the following ?*/
-                       case ICMD_CHECKEXCEPTION:
                        case ICMD_AASTORECONST:
                                TYPECHECK_COUNT(stat_ins_unchecked);
                                break;
@@ -1978,6 +2396,8 @@ return_tail:
 
                /* reach exception handlers for this instruction */
                if (maythrow) {
+                       TYPECHECK_COUNT(stat_ins_maythrow);
+                       TYPECHECK_MARK(state->stat_maythrow);
                        LOG("reaching exception handlers");
                        i = 0;
                        while (state->handlers[i]) {
@@ -1986,11 +2406,10 @@ return_tail:
                                        state->excstack.typeinfo.typeclass = state->handlers[i]->catchtype;
                                else
                                        state->excstack.typeinfo.typeclass.cls = class_java_lang_Throwable;
-                               state->repeat |= typestate_reach(state->cd,state->rd, state->localbuf,state->bptr,
+                               if (!typestate_reach(state,
                                                state->handlers[i]->handler,
-                                               &(state->excstack),state->localset,
-                                               state->numlocals,
-                                               state->jsrencountered);
+                                               &(state->excstack),state->localset))
+                                       return false;
                                i++;
                        }
                }
@@ -2011,26 +2430,22 @@ return_tail:
                while (tbptr->flags == BBDELETED) {
                        tbptr++;
 #ifdef TYPECHECK_DEBUG
+                       /* this must be checked in parse.c */
                        if ((tbptr->debug_nr) >= state->m->basicblockcount)
                                TYPECHECK_VERIFYERROR_bool("Control flow falls off the last block");
 #endif
                }
-               TYPECHECK_REACH;
+               if (!typestate_reach(state,tbptr,dst,state->localset))
+                       return false;
        }
 
        /* We may have to restore the types of the instack slots. They
         * have been saved if an <init> call inside the block has
         * modified the instack types. (see INVOKESPECIAL) */
 
-       if (state->savedstack) {
-               stackptr sp = state->bptr->instack;
-               stackptr copy = state->savedstack;
-               TYPECHECK_COUNT(stat_savedstack);
-               LOG("restoring saved instack");
-               TYPESTACK_COPY(sp,copy);
-               state->bptr->instack = state->savedstack;
-               state->savedstack = NULL;
-       }
+       if (state->savedstack)
+               typestate_restore_instack(state);
+
        return true;
 }
 
@@ -2078,7 +2493,7 @@ verify_init_locals(verifier_state *state)
         if (state->initmethod)
             TYPEINFO_INIT_NEWOBJECT(td->info,NULL);
         else
-            TYPEINFO_INIT_CLASSINFO(td->info, state->m->class);
+            typeinfo_init_classinfo(&(td->info), state->m->class);
         td++;
                i--;
     }
@@ -2108,6 +2523,90 @@ verify_init_locals(verifier_state *state)
        return true;
 }
 
+/* typecheck_init_flags ********************************************************
+   Initialize the basic block flags for the following CFG traversal.
+  
+   IN:
+       state............the current state of the verifier
+
+*******************************************************************************/
+
+static void
+typecheck_init_flags(verifier_state *state)
+{
+       s4 i;
+       basicblock *block;
+
+    /* set all BBFINISHED blocks to BBTYPECHECK_UNDEF. */
+       
+    i = state->m->basicblockcount;
+    block = state->m->basicblocks;
+
+    while (--i >= 0) {
+               
+#ifdef TYPECHECK_DEBUG
+               /* check for invalid flags */
+        if (block->flags != BBFINISHED && block->flags != BBDELETED && block->flags != BBUNDEF)
+        {
+            /*show_icmd_method(state->cd->method,state->cd,state->rd);*/
+            LOGSTR1("block flags: %d\n",block->flags); LOGFLUSH;
+                       TYPECHECK_ASSERT(false);
+        }
+#endif
+
+        if (block->flags >= BBFINISHED) {
+            block->flags = BBTYPECHECK_UNDEF;
+        }
+        block++;
+    }
+
+    /* the first block is always reached */
+       
+    if (state->m->basicblockcount && state->m->basicblocks[0].flags == BBTYPECHECK_UNDEF)
+        state->m->basicblocks[0].flags = BBTYPECHECK_REACHED;
+}
+
+/* typecheck_reset_flags *******************************************************
+   Reset the flags of basic blocks we have not reached.
+  
+   IN:
+       state............the current state of the verifier
+
+*******************************************************************************/
+
+static void
+typecheck_reset_flags(verifier_state *state)
+{
+       s4 i;
+
+       /* check for invalid flags at exit */
+       
+#ifdef TYPECHECK_DEBUG
+       for (i=0; i<state->m->basicblockcount; ++i) {
+               if (state->m->basicblocks[i].flags != BBDELETED
+                       && state->m->basicblocks[i].flags != BBUNDEF
+                       && state->m->basicblocks[i].flags != BBFINISHED
+                       && state->m->basicblocks[i].flags != BBTYPECHECK_UNDEF) /* typecheck may never reach
+                                                                                                        * some exception handlers,
+                                                                                                        * that's ok. */
+               {
+                       LOG2("block L%03d has invalid flags after typecheck: %d",
+                                state->m->basicblocks[i].debug_nr,state->m->basicblocks[i].flags);
+                       TYPECHECK_ASSERT(false);
+               }
+       }
+#endif
+       
+       /* Reset blocks we never reached */
+       
+       for (i=0; i<state->m->basicblockcount; ++i) {
+               if (state->m->basicblocks[i].flags == BBTYPECHECK_UNDEF)
+                       state->m->basicblocks[i].flags = BBFINISHED;
+       }
+}
+               
 /****************************************************************************/
 /* typecheck()                                                              */
 /* This is the main function of the bytecode verifier. It is called         */
@@ -2133,7 +2632,6 @@ methodinfo *typecheck(methodinfo *meth, codegendata *cdata, registerdata *rdata)
 {
        verifier_state state;             /* current state of the verifier */
     int i;                                        /* temporary counter */
-    static utf *name_init;            /* cache for utf string "<init>" */
 
        /* collect statistics */
 
@@ -2141,11 +2639,13 @@ methodinfo *typecheck(methodinfo *meth, codegendata *cdata, registerdata *rdata)
        int count_iterations = 0;
        TYPECHECK_COUNT(stat_typechecked);
        TYPECHECK_COUNT_FREQ(stat_locals,cdata->maxlocals,STAT_LOCALS);
-       TYPECHECK_COUNT_FREQ(stat_blocks,meth->basicblockcount/10,STAT_BLOCKS);
+       TYPECHECK_COUNT_FREQ(stat_blocks,cdata->method->basicblockcount/10,STAT_BLOCKS);
+       TYPECHECK_COUNTIF(cdata->method->exceptiontablelength != 0,stat_methods_with_handlers);
+       state.stat_maythrow = false;
 #endif
 
        /* some logging on entry */
-       
+
     LOGSTR("\n==============================================================================\n");
     /*DOLOG( show_icmd_method(cdata->method,cdata,rdata));*/
     LOGSTR("\n==============================================================================\n");
@@ -2169,36 +2669,11 @@ methodinfo *typecheck(methodinfo *meth, codegendata *cdata, registerdata *rdata)
 
        /* check if this method is an instance initializer method */
 
-       if (!name_init)
-               name_init = utf_new_char("<init>");
-    state.initmethod = (state.m->name == name_init);
+    state.initmethod = (state.m->name == utf_init);
 
-    /* reset all BBFINISHED blocks to BBTYPECHECK_UNDEF. */
-       
-    i = state.m->basicblockcount;
-    state.bptr = state.m->basicblocks;
-    while (--i >= 0) {
-#ifdef TYPECHECK_DEBUG
-        if (state.bptr->flags != BBFINISHED && state.bptr->flags != BBDELETED
-            && state.bptr->flags != BBUNDEF)
-        {
-            /*show_icmd_method(state.cd->method,state.cd,state.rd);*/
-            LOGSTR1("block flags: %d\n",state.bptr->flags); LOGFLUSH;
-                       TYPECHECK_ASSERT(false);
-        }
-#endif
-        if (state.bptr->flags >= BBFINISHED) {
-            state.bptr->flags = BBTYPECHECK_UNDEF;
-        }
-        state.bptr++;
-    }
-
-    /* the first block is always reached */
-       
-    if (state.m->basicblockcount && state.m->basicblocks[0].flags == BBTYPECHECK_UNDEF)
-        state.m->basicblocks[0].flags = BBTYPECHECK_REACHED;
+       /* initialize the basic block flags for the following CFG traversal */
 
-    LOG("Blocks reset.\n");
+       typecheck_init_flags(&state);
 
     /* number of local variables */
     
@@ -2230,7 +2705,7 @@ methodinfo *typecheck(methodinfo *meth, codegendata *cdata, registerdata *rdata)
        
        state.excstack.prev = NULL;
        state.excstack.type = TYPE_ADR;
-       TYPEINFO_INIT_CLASSINFO(state.excstack.typeinfo,
+       typeinfo_init_classinfo(&(state.excstack.typeinfo),
                                                        class_java_lang_Throwable); /* changed later */
 
     LOG("Exception handler stacks set.\n");
@@ -2257,7 +2732,7 @@ methodinfo *typecheck(methodinfo *meth, codegendata *cdata, registerdata *rdata)
             state.bptr++;
         } /* while blocks */
 
-        LOGIF(state.repeat,"state.repeat=true");
+        LOGIF(state.repeat,"state.repeat == true");
     } while (state.repeat);
 
        /* statistics */
@@ -2266,43 +2741,19 @@ methodinfo *typecheck(methodinfo *meth, codegendata *cdata, registerdata *rdata)
        LOG1("Typechecker did %4d iterations",count_iterations);
        TYPECHECK_COUNT_FREQ(stat_iterations,count_iterations,STAT_ITERATIONS);
        TYPECHECK_COUNTIF(state.jsrencountered,stat_typechecked_jsr);
+       TYPECHECK_COUNTIF(state.stat_maythrow,stat_methods_maythrow);
 #endif
 
-       /* check for invalid flags at exit */
-       
-#ifdef TYPECHECK_DEBUG
-       for (i=0; i<state.m->basicblockcount; ++i) {
-               if (state.m->basicblocks[i].flags != BBDELETED
-                       && state.m->basicblocks[i].flags != BBUNDEF
-                       && state.m->basicblocks[i].flags != BBFINISHED
-                       && state.m->basicblocks[i].flags != BBTYPECHECK_UNDEF) /* typecheck may never reach
-                                                                                                        * some exception handlers,
-                                                                                                        * that's ok. */
-               {
-                       LOG2("block L%03d has invalid flags after typecheck: %d",
-                                state.m->basicblocks[i].debug_nr,state.m->basicblocks[i].flags);
-                       TYPECHECK_ASSERT(false);
-               }
-       }
-#endif
-       
-       /* Reset blocks we never reached */
-       
-       for (i=0; i<state.m->basicblockcount; ++i) {
-               if (state.m->basicblocks[i].flags == BBTYPECHECK_UNDEF)
-                       state.m->basicblocks[i].flags = BBFINISHED;
-       }
-               
-    LOGimp("exiting typecheck");
+       /* reset the flags of blocks we haven't reached */
 
-       /* just return methodinfo* to indicate everything was ok */
+       typecheck_reset_flags(&state);
 
+       /* just return methodinfo* to indicate everything was ok */
+    LOGimp("exiting typecheck");
        return state.m;
 }
 
-#undef COPYTYPE
-
-#endif /* CACAO_TYPECHECK */
+#endif /* ENABLE_VERIFIER */
 
 /*
  * These are local overrides for various environment variables in Emacs.