a4880c748dac81ac6a2a5313847140888bd16eae
[jpf-core.git] / src / main / gov / nasa / jpf / vm / MethodInfo.java
1 /*
2  * Copyright (C) 2014, United States Government, as represented by the
3  * Administrator of the National Aeronautics and Space Administration.
4  * All rights reserved.
5  *
6  * The Java Pathfinder core (jpf-core) platform is licensed under the
7  * Apache License, Version 2.0 (the "License"); you may not use this file except
8  * in compliance with the License. You may obtain a copy of the License at
9  * 
10  *        http://www.apache.org/licenses/LICENSE-2.0. 
11  *
12  * Unless required by applicable law or agreed to in writing, software
13  * distributed under the License is distributed on an "AS IS" BASIS,
14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15  * See the License for the specific language governing permissions and 
16  * limitations under the License.
17  */
18 package gov.nasa.jpf.vm;
19
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.JPFException;
23 import gov.nasa.jpf.util.JPFLogger;
24 import gov.nasa.jpf.util.LocationSpec;
25 import gov.nasa.jpf.vm.bytecode.ReturnInstruction;
26 import java.lang.reflect.Modifier;
27 import java.util.ArrayList;
28 import java.util.Collections;
29 import java.util.List;
30
31
32 /**
33  * information associated with a method. Each method in JPF
34  * is represented by a MethodInfo object
35  */
36 public class MethodInfo extends InfoObject implements GenericSignatureHolder  {
37
38   static JPFLogger logger = JPF.getLogger("gov.nasa.jpf.vm.MethodInfo");
39   
40   static final int INIT_MTH_SIZE = 4096;
41   protected static final ArrayList<MethodInfo> mthTable = new ArrayList<MethodInfo>(INIT_MTH_SIZE);
42   
43   // special globalIds
44   static final int DIRECT_CALL = -1;
45
46   static final LocalVarInfo[] EMPTY = new LocalVarInfo[0];
47   
48   static final int[] EMPTY_INT = new int[0];
49   
50   /**
51    * Used to warn about local variable information.
52    */
53   protected static boolean warnedLocalInfo = false;
54   
55   //--- various JPF method attributes
56   static final int  EXEC_ATOMIC = 0x10000; // method executed atomically
57   static final int  EXEC_HIDDEN = 0x20000; // method hidden from path
58   static final int  FIREWALL    = 0x40000; // firewall any unhandled exceptionHandlers
59                                            // (turn into UnhandledException throws)
60   static final int  IS_CLINIT   = 0x80000;
61   static final int  IS_INIT     = 0x100000;
62   
63   static final int  IS_REFLECTION = 0x200000; // this is a reflection direct call
64   static final int  IS_DIRECT_CALL = 0x400000;
65   
66   /** a unique int assigned to this method */
67   protected int globalId = -1;
68
69   /**
70    * this is a lazy evaluated mangled name consisting of the name and
71    * arg type signature
72    */
73   protected String uniqueName;
74
75   /** Name of the method */
76   protected String name;
77
78   /** Signature of the method */
79   protected String signature;
80
81   /** Generic signature of the method */
82   protected String genericSignature;
83
84   /** Class the method belongs to */
85   protected ClassInfo ci;
86
87   /** Instructions associated with the method */
88   protected Instruction[] code;
89
90   /** JPFConfigException handlers */
91   protected ExceptionHandler[] exceptionHandlers;
92
93   /** classnames of checked exception thrown by the method */
94   protected String[] thrownExceptionClassNames;
95
96   /** Table used for line numbers 
97    * this assigns a line number to every instruction index, instead of 
98    * using an array of ranges. Assuming we have 2-3 insns per line on average,
99    * this should still require less memory than a reference array with associated
100    * range objects, and allows faster access of instruction line numbers, which
101    * we might need for location specs
102    */
103   protected int[] lineNumbers;
104   
105   /** Local variable information */
106   protected LocalVarInfo localVars[] = null;
107
108   /** Maximum number of local variables */
109   protected int maxLocals;
110
111   /** Maximum number of elements on the stack */
112   protected int maxStack;
113
114   /** null if we don't have any */
115   AnnotationInfo[][] parameterAnnotations;
116
117   //--- a batch of attributes
118   
119   /** the standard Java modifier attributes */
120   protected int modifiers;
121    
122   /** a batch of execution related JPF attributes */
123   protected int attributes;
124       
125
126   //--- all the stuff we need for native methods
127   // <2do> pcm - turn this into a derived class
128
129   /**  the number of stack slots for the arguments (incl. 'this'), lazy eval */
130   protected int argSize = -1;
131
132   /** number of arguments (excl. 'this'), lazy eval */
133   protected int nArgs = -1;
134
135   /** what return type do we have (again, lazy evaluated) */
136   protected byte returnType = -1;
137
138   /** number of stack slots for return value */
139   protected int retSize = -1;
140
141   /** used for native method parameter conversion (lazy evaluated) */
142   protected byte[] argTypes = null;
143   
144   static boolean init (Config config) {
145     mthTable.clear();    
146     return true;
147   }
148
149   public static MethodInfo getMethodInfo (int globalId){
150     if (globalId >=0 && globalId <mthTable.size()){
151       return mthTable.get(globalId);
152     } else {
153       return null;
154     }
155   }
156   
157   public static MethodInfo create (String name, String signature, int modifiers){
158     return new MethodInfo( name, signature, modifiers);
159   }
160   
161   public static MethodInfo create (ClassInfo ci, String name, String signature, int modifiers){
162     return new MethodInfo( ci, name, signature, modifiers);
163   }
164   
165   static MethodInfo create (ClassInfo ci, String name, String signature, int modifiers, int maxLocals, int maxStack){
166     return new MethodInfo( ci, name, signature, modifiers, maxLocals, maxStack);
167   }
168
169   /**
170    * for direct call construction
171    * Note: this is only a partial initialization, the code still has to be created/installed by the caller
172    */
173   public MethodInfo (MethodInfo callee, int nLocals, int nOperands) {
174     globalId = DIRECT_CALL;
175     // we don't want direct call methods in the mthTable (would be a memory leak) so don't register
176     
177     ci = callee.ci;
178     name = "[" + callee.name + ']'; // it doesn't allocate anything, so we don't have to be unique
179     signature = "()V";
180     genericSignature = "";
181     maxLocals = nLocals;
182     maxStack = nOperands;  // <2do> cache for optimization
183     localVars = EMPTY;
184     lineNumbers = null;
185     exceptionHandlers = null;
186     thrownExceptionClassNames = null;
187     uniqueName = name;
188     
189     // we need to preserve the ClassInfo so that class resolution for static method calls works
190     ci = callee.ci;
191     
192     attributes |= IS_DIRECT_CALL;
193     modifiers = Modifier.STATIC;   // always treated as static
194     
195     // code still has to be installed by caller
196   }
197   
198   /**
199    * This is used to create synthetic methods of function object types
200    */
201   public MethodInfo(String name, String signature, int modifiers, int nLocals, int nOperands) {
202     this( name, signature, modifiers);
203     maxLocals = nLocals;
204     maxStack = nOperands;
205     localVars = EMPTY;
206   }
207   
208   /**
209    * for NativeMethodInfo creation 
210    */
211   public MethodInfo (MethodInfo mi) {
212     globalId = mi.globalId;
213     uniqueName = mi.uniqueName;
214     name = mi.name;
215     signature = mi.signature;
216     genericSignature = mi.genericSignature;
217     ci = mi.ci;
218     modifiers = mi.modifiers;
219     attributes = mi.attributes;
220     thrownExceptionClassNames = mi.thrownExceptionClassNames;
221     parameterAnnotations = mi.parameterAnnotations;
222
223     annotations = mi.annotations;
224     
225     localVars = null; // there are no StackFrame localVarInfos, this is native
226     // code still has to be installed by caller
227   }
228   
229   // <2do> this is going away
230   public MethodInfo (ClassInfo ci, String name, String signature, int modifiers, int maxLocals, int maxStack){
231     this.ci = ci;
232     this.name = name;
233     this.signature = signature;
234     this.uniqueName = getUniqueName(name, signature);
235     this.genericSignature = "";
236     this.maxLocals = maxLocals;
237     this.maxStack = maxStack;
238     this.modifiers = modifiers;
239
240     this.lineNumbers = null;
241     this.exceptionHandlers = null;
242     this.thrownExceptionClassNames = null;
243
244     // set attributes we can deduce from the name and the ClassInfo
245     if (ci != null){
246       if (name.equals("<init>")) {
247         attributes |= IS_INIT;
248       } else if (name.equals("<clinit>")) {
249         this.modifiers |= Modifier.SYNCHRONIZED;
250         attributes |= IS_CLINIT | FIREWALL;
251       }
252       if (ci.isInterface()) { // all interface methods are public
253         this.modifiers |= Modifier.PUBLIC;
254       }
255     }
256
257     this.globalId = mthTable.size();
258     mthTable.add(this);
259   }
260
261   
262   public MethodInfo (String name, String signature, int modifiers){
263     this.name = name;
264     this.signature = signature;
265     this.modifiers = modifiers;
266     this.uniqueName = getUniqueName(name, signature);
267     this.genericSignature = "";
268
269     if (name.equals("<init>")) {
270       attributes |= IS_INIT;
271     } else if (name.equals("<clinit>")) {
272       // for some reason clinits don't have the synchronized modifier, but they are synchronized
273       // we keep it consistent so that we don't have to implement special lock acquisition/release for clinits
274       this.modifiers |= Modifier.SYNCHRONIZED;
275       attributes |= IS_CLINIT | FIREWALL;
276     }
277     
278     this.globalId = mthTable.size();
279     mthTable.add(this);    
280   }
281
282   public MethodInfo (ClassInfo ci, String name, String signature, int modifiers){
283     this(name, signature, modifiers);
284     
285     this.ci = ci;
286   }
287   
288   //--- setters used during construction
289   
290   public void linkToClass (ClassInfo ci){
291     this.ci = ci;
292     
293     if (ci.isInterface()) { // all interface methods are public
294       this.modifiers |= Modifier.PUBLIC;
295     }
296   }
297   
298   public void setMaxLocals(int maxLocals){
299     this.maxLocals = maxLocals;
300   }
301
302   public void setMaxStack(int maxStack){
303     this.maxStack = maxStack;
304   }
305   
306   public void setCode (Instruction[] code){
307     for (int i=0; i<code.length; i++){
308       code[i].setMethodInfo(this);
309     }
310     this.code = code;
311   }
312   
313   
314   public boolean hasParameterAnnotations() {
315     return (parameterAnnotations != null);
316   }
317
318   // since some listeners might call this on every method invocation, we should do a little optimization
319   static AnnotationInfo[][] NO_PARAMETER_ANNOTATIONS_0 = new AnnotationInfo[0][];
320   static AnnotationInfo[][] NO_PARAMETER_ANNOTATIONS_1 = { new AnnotationInfo[0] };
321   static AnnotationInfo[][] NO_PARAMETER_ANNOTATIONS_2 = { new AnnotationInfo[0], new AnnotationInfo[0] };
322   static AnnotationInfo[][] NO_PARAMETER_ANNOTATIONS_3 = { new AnnotationInfo[0], new AnnotationInfo[0], new AnnotationInfo[0] };  
323   
324   public AnnotationInfo[][] getParameterAnnotations() {
325     if (parameterAnnotations == null){ // keep this similar to getAnnotations()
326       int n = getNumberOfArguments();
327       switch (n){
328       case 0: return NO_PARAMETER_ANNOTATIONS_0;
329       case 1: return NO_PARAMETER_ANNOTATIONS_1;
330       case 2: return NO_PARAMETER_ANNOTATIONS_2;
331       case 3: return NO_PARAMETER_ANNOTATIONS_3;
332       default:
333         AnnotationInfo[][] pai = new AnnotationInfo[n][];
334         for (int i=0; i<n; i++){
335           pai[i] = new AnnotationInfo[0];
336         }
337         return pai;
338       }
339       
340     } else {
341       return parameterAnnotations;
342     }
343   }
344
345   /**
346    * return annotations for parameterIndex
347    */
348   public AnnotationInfo[] getParameterAnnotations(int parameterIndex){
349     if (parameterAnnotations == null){
350       return null;
351     } else {
352       if (parameterIndex >= getNumberOfArguments()){
353         return null;
354       } else {
355         return parameterAnnotations[parameterIndex];
356       }
357     }
358   }
359
360
361   
362   public static int getNumberOfLoadedMethods () {
363     return mthTable.size();
364   }
365
366   void setAtomic (boolean isAtomic) {
367     if (isAtomic) {
368       attributes |= EXEC_ATOMIC;
369     } else {
370       attributes &= ~EXEC_ATOMIC;
371     }
372   }
373   public boolean isAtomic () {
374     return ((attributes & EXEC_ATOMIC) != 0);
375   }
376   
377   void setHidden (boolean isHidden) {
378     if (isHidden) {
379       attributes |= EXEC_HIDDEN;
380     } else {
381       attributes &= ~EXEC_HIDDEN;
382     }
383   }
384   public boolean isHidden () {
385     return ((attributes & EXEC_HIDDEN) != 0);    
386   }
387   
388   /**
389    * turn unhandled exceptionHandlers at the JPF execution level
390    * into UnhandledException throws at the host VM level
391    * this is useful to implement firewalls for direct calls
392    * which should not let exceptionHandlers permeate into bytecode/
393    * application code
394    */
395   public void setFirewall (boolean isFirewalled) {
396     if (isFirewalled) {
397       attributes |= FIREWALL;
398     } else {
399       attributes &= ~FIREWALL;
400     }
401   }
402   public boolean isFirewall () {
403     return ((attributes & FIREWALL) != 0);    
404   }
405   
406   
407   
408   @Override
409   public Object clone() {
410     try {
411       return super.clone();
412     } catch (CloneNotSupportedException cnx) {
413       return null;
414     }
415   }
416   
417   public int getGlobalId() {
418     return globalId;
419   }
420
421   public DirectCallStackFrame createRunStartStackFrame (ThreadInfo ti){
422     return ci.createRunStartStackFrame( ti, this);
423   }
424
425   public DirectCallStackFrame createDirectCallStackFrame (ThreadInfo ti, int nLocals){
426     return ci.createDirectCallStackFrame(ti, this, nLocals);
427   }
428
429   public boolean isSyncRelevant () {
430     return (name.charAt(0) != '<');
431   }
432   
433   public boolean isInitOrClinit (){
434     return ((attributes & (IS_CLINIT | IS_INIT)) != 0);
435   }
436   
437   public boolean isClinit () {
438     return ((attributes & IS_CLINIT) != 0);
439   }
440
441   public boolean isClinit (ClassInfo ci) {
442     return (((attributes & IS_CLINIT) != 0) && (this.ci == ci));
443   }
444
445   public boolean isInit() {
446     return ((attributes & IS_INIT) != 0);
447   }
448   
449   public boolean isDirectCallStub(){
450     return ((attributes & IS_DIRECT_CALL) != 0);    
451   }
452   
453   /**
454    * yet another name - this time with a non-mangled, but abbreviated signature
455    * and without return type (e.g. like "main(String[])"
456    */
457   public String getLongName () {
458     StringBuilder sb = new StringBuilder();
459     sb.append(name);
460     
461     sb.append('(');
462     String[] argTypeNames = getArgumentTypeNames();
463     for (int i=0; i<argTypeNames.length; i++) {
464       String a = argTypeNames[i];
465       int idx = a.lastIndexOf('.');
466       if (idx > 0) {
467         a = a.substring(idx+1);
468       }
469       if (i>0) {
470         sb.append(',');
471       }
472       sb.append(a);
473     }
474     sb.append(')');
475     
476     return sb.toString();
477   }
478   
479   /**
480    * return the minimal name that has to be unique for overloading
481    * used as a lookup key
482    * NOTE: with the silent introduction of covariant return types
483    * in Java 5.0, we have to use the full signature to be unique
484    */
485   public static String getUniqueName (String mname, String signature) {
486     return (mname + signature);
487   }
488
489   public String getStackTraceSource() {
490     return getSourceFileName();
491   }
492
493   public byte[] getArgumentTypes () {
494     if (argTypes == null) {
495       argTypes = Types.getArgumentTypes(signature);
496       nArgs = argTypes.length;
497     }
498
499     return argTypes;
500   }
501
502   public String[] getArgumentTypeNames () {
503     return Types.getArgumentTypeNames(signature);
504   }
505   
506   public int getArgumentsSize () {
507     if (argSize < 0) {
508       argSize = Types.getArgumentsSize(signature);
509
510       if (!isStatic()) {
511         argSize++;
512       }
513     }
514
515     return argSize;
516   }
517   
518   /**
519    * return only the LocalVarInfos for arguments, in order of definition
520    * or null if there are no localVarInfos.
521    * throw a JPFException if there are more immediately in scope vars than args
522    * 
523    * NOTE - it is perfectly legal for a method to have arguments but no LocalVarInfos,
524    * which are code attributes, clients have to check for a non-null return value
525    * even if the method has arguments.
526    * Note also that abstract / interface methods don't have code and hence no
527    * LocalVarInfos
528    */
529   public LocalVarInfo[] getArgumentLocalVars(){
530     if (localVars == null){ // shortcut in case we don't have args or localVars;
531       return null;
532     }
533     
534     int nArgs = getNumberOfStackArguments(); // we want 'this'
535     if (nArgs == 0){
536       return new LocalVarInfo[0]; // rare enough so that we don't use a static
537     }
538
539     LocalVarInfo[] argLvis = new LocalVarInfo[nArgs];
540     int n = 0; // how many args we've got so far
541     
542     for (LocalVarInfo lvi : localVars){
543       // arguments are the only ones that are immediately in scope
544       if (lvi.getStartPC() == 0){
545         if (n == nArgs){ // ARGH - more in-scope vars than args
546           throw new JPFException("inconsistent localVar table for method " + getFullName());
547         }
548         
549         // order with respect to slot index - since this might get called
550         // frequently, we don't use java.util.Arrays.sort() but sort in
551         // on-the-fly. Note that we can have several localVar entries for the
552         // same name, but only one can be immediately in scope
553         int slotIdx = lvi.getSlotIndex();
554
555         int i;
556         for (i = 0; i < n; i++) {
557           if (slotIdx < argLvis[i].getSlotIndex()) {
558             for (int j=n; j>i; j--){
559               argLvis[j] = argLvis[j-1];
560             }
561             argLvis[i] = lvi;
562             n++;
563             break;
564           }
565         }
566         if (i == n) { // append
567           argLvis[n++] = lvi;
568         }
569       }
570     }
571     
572     return argLvis;
573   }
574   
575   public String getReturnType () {
576     return Types.getReturnTypeSignature(signature);
577   }
578
579   public String getReturnTypeName () {
580     return Types.getReturnTypeName(signature);
581   }
582   
583   public String getSourceFileName () {
584     if (ci != null) {
585       return ci.getSourceFileName();
586     } else {
587       return "[VM]";
588     }
589   }
590
591   public String getClassName () {
592     if (ci != null) {
593       return ci.getName();
594     } else {
595       return "[VM]";
596     }
597   }
598   
599   /**
600    * Returns the class the method belongs to.
601    */
602   public ClassInfo getClassInfo () {
603     return ci;
604   }
605
606   /**
607    * @deprecated - use getFullName
608    */
609   @Deprecated
610 public String getCompleteName () {
611     return getFullName();
612   }
613
614   /**
615    * return classname.name (but w/o signature)
616    */
617   public String getBaseName() {
618     return getClassName() + '.' + name;
619   }
620     
621   public boolean isCtor () {
622     return (name.equals("<init>"));
623   }
624   
625   public boolean isInternalMethod () {
626     // <2do> pcm - should turn this into an attribute for efficiency reasons
627     return (name.equals("<clinit>") || uniqueName.equals("finalize()V"));
628   }
629   
630   public boolean isThreadEntry (ThreadInfo ti) {
631     return (uniqueName.equals("run()V") && (ti.countStackFrames() == 1));
632   }
633   
634   /**
635    * Returns the full classname (if any) + name + signature.
636    */
637   public String getFullName () {
638     if (ci != null) {
639       return ci.getName() + '.' + getUniqueName();
640     } else {
641       return getUniqueName();
642     }
643   }
644
645   /**
646    * returns stack trace name: classname (if any) + name
647    */
648   public String getStackTraceName(){
649     if (ci != null) {
650       return ci.getName() + '.' + name;
651     } else {
652       return name;
653     }
654   }
655   
656   /**
657    * return number of instructions
658    */
659   public int getNumberOfInstructions() {
660     if (code == null){
661       return 0;
662     }
663     
664     return code.length;
665   }
666   
667   /**
668    * Returns a specific instruction.
669    */
670   public Instruction getInstruction (int i) {
671     if (code == null) {
672       return null;
673     }
674
675     if ((i < 0) || (i >= code.length)) {
676       return null;
677     }
678
679     return code[i];
680   }
681
682   /**
683    * Returns the instruction at a certain position.
684    */
685   public Instruction getInstructionAt (int position) {
686     if (code == null) {
687       return null;
688     }
689
690     for (int i = 0, l = code.length; i < l; i++) {
691       if ((code[i] != null) && (code[i].getPosition() == position)) {
692         return code[i];
693       }
694     }
695
696     throw new JPFException("instruction not found");
697   }
698
699   /**
700    * Returns the instructions of the method.
701    */
702   public Instruction[] getInstructions () {
703     return code;
704   }
705   
706   public boolean includesLine (int line){
707     int len = code.length;
708     return (code[0].getLineNumber() <= line) && (code[len].getLineNumber() >= line);
709   }
710
711   public Instruction[] getInstructionsForLine (int line){
712     return getInstructionsForLineInterval(line,line);
713   }
714
715   public Instruction[] getInstructionsForLineInterval (int l1, int l2){
716     Instruction[] c = code;
717        
718     // instruction line numbers don't have to be monotonic (they can decrease for loops)
719     // hence we cannot easily check for overlapping ranges
720     
721     if (c != null){
722        ArrayList<Instruction> matchingInsns = null;
723        
724        for (int i = 0; i < c.length; i++) {
725         Instruction insn = c[i];
726         int line = insn.getLineNumber();
727         if (line == l1 || line == l2 || (line > l1 && line < l2)) {
728           if (matchingInsns == null) {
729             matchingInsns = new ArrayList<Instruction>();
730           }
731           matchingInsns.add(insn);
732         }
733       }
734       
735       if (matchingInsns == null) {
736         return null;
737       } else {
738         return matchingInsns.toArray(new Instruction[matchingInsns.size()]);
739       }
740             
741     } else {
742       return null;
743     }
744   }
745
746   public Instruction[] getMatchingInstructions (LocationSpec lspec){
747     return getInstructionsForLineInterval(lspec.getFromLine(), lspec.getToLine());
748   }
749
750
751   /**
752    * Returns the line number for a given position.
753    */
754   public int getLineNumber (Instruction pc) {
755     if (lineNumbers == null) {
756       if (pc == null)
757         return -1;
758       else
759         return pc.getPosition();
760     }
761
762     if (pc != null) {
763       int idx = pc.getInstructionIndex();
764       if (idx < 0) idx = 0;
765       return lineNumbers[idx];
766     } else {
767       return -1;
768     }
769   }
770
771   /**
772    * Returns a table to translate positions into line numbers.
773    */
774   public int[] getLineNumbers () {
775     return lineNumbers;
776   }
777
778   public boolean containsLineNumber (int n){
779     if (lineNumbers != null){
780       return (lineNumbers[0] <= n) && (lineNumbers[lineNumbers.length-1] <= n);
781     }
782     
783     return false;
784   }
785   
786   public boolean intersectsLineNumbers( int first, int last){
787     if (lineNumbers != null){
788       if ((last < lineNumbers[0]) || (first > lineNumbers[lineNumbers.length-1])){
789         return false;
790       }
791       return true;
792     }
793     
794     return false;
795   }
796   
797   public ExceptionHandler getHandlerFor (ClassInfo ciException, Instruction insn){
798     if (exceptionHandlers != null){
799       int position = insn.getPosition();
800       for (int i=0; i<exceptionHandlers.length; i++){
801         ExceptionHandler handler = exceptionHandlers[i];
802         if ((position >= handler.getBegin()) && (position < handler.getEnd())) {
803           // checks if this type of exception is caught here (null means 'any')
804           String handledType = handler.getName();
805           if ((handledType == null)   // a catch-all handler
806                   || ciException.isInstanceOf(handledType)) {
807             return handler;
808           }
809         }          
810       }      
811     }
812     
813     return null;
814   }
815   
816   public boolean isMJI () {
817     return false;
818   }
819
820   public int getMaxLocals () {
821     return maxLocals;
822   }
823
824   public int getMaxStack () {
825     return maxStack;
826   }
827
828   public ExceptionHandler[] getExceptions () {
829     return exceptionHandlers;
830   }
831
832   public String[] getThrownExceptionClassNames () {
833     return thrownExceptionClassNames;
834   }
835
836
837   public LocalVarInfo getLocalVar(String name, int pc){
838     LocalVarInfo[] vars = localVars;
839     if (vars != null){
840       for (int i = 0; i < vars.length; i++) {
841         LocalVarInfo lv = vars[i];
842         if (lv.matches(name, pc)) {
843           return lv;
844         }
845       }
846     }
847
848     return null;
849
850   }
851
852   public LocalVarInfo getLocalVar (int slotIdx, int pc){
853     LocalVarInfo[] vars = localVars;
854
855     if (vars != null){
856       for (int i = 0; i < vars.length; i++) {
857         LocalVarInfo lv = vars[i];
858         if (lv.matches(slotIdx, pc)) {
859           return lv;
860         }
861       }
862     }
863
864     return null;
865   }
866
867   public LocalVarInfo[] getLocalVars() {
868     return localVars; 
869   }
870
871
872   /**
873    * note that this might contain duplicates for variables with multiple
874    * scope entries
875    */
876   public String[] getLocalVariableNames() {
877     String[] names = new String[localVars.length];
878
879     for (int i=0; i<localVars.length; i++){
880       names[i] = localVars[i].getName();
881     }
882
883     return names;
884   }
885
886
887   public MethodInfo getOverriddenMethodInfo(){
888     MethodInfo smi = null;
889     
890     if (ci != null) {
891       ClassInfo sci = ci.getSuperClass();
892       if (sci != null){
893         smi = sci.getMethod(getUniqueName(), true);
894       }
895     }
896     
897     return smi;
898   }
899   
900   /**
901    * Returns the name of the method.
902    */
903   public String getName () {
904     return name;
905   }
906
907   public String getJNIName () {
908     return Types.getJNIMangledMethodName(null, name, signature);
909   }
910   
911   public int getModifiers () {
912     return modifiers;
913   }
914   
915   /**
916    * Returns true if the method is native
917    */
918   public boolean isNative () {
919     return ((modifiers & Modifier.NATIVE) != 0);
920   }
921
922   public boolean isAbstract () {
923     return ((modifiers & Modifier.ABSTRACT) != 0);
924   }
925   
926   // overridden by NativeMethodInfo
927   public boolean isUnresolvedNativeMethod(){
928     return ((modifiers & Modifier.NATIVE) != 0);
929   }
930
931   // overridden by NativeMethodInfo
932   public boolean isJPFExecutable (){
933     return !hasAttr(NoJPFExec.class);
934   }
935
936   public int getNumberOfArguments () {
937     if (nArgs < 0) {
938       nArgs = Types.getNumberOfArguments(signature);
939     }
940
941     return nArgs;
942   }
943
944   /**
945    * Returns the size of the arguments.
946    * This returns the number of parameters passed on the stack, incl. 'this'
947    */
948   public int getNumberOfStackArguments () {
949     int n = getNumberOfArguments();
950
951     return isStatic() ? n : n + 1;
952   }
953
954   public int getNumberOfCallerStackSlots () {
955     return Types.getNumberOfStackSlots(signature, isStatic()); // includes return type
956   }
957
958   public Instruction getFirstInsn(){
959     if (code != null){
960       return code[0];
961     }
962     return null;    
963   }
964   
965   public Instruction getLastInsn() {
966     if (code != null){
967       return code[code.length-1];
968     }
969     return null;
970   }
971
972   /**
973    * do we return Object references?
974    */
975   public boolean isReferenceReturnType () {
976     int r = getReturnTypeCode();
977
978     return ((r == Types.T_REFERENCE) || (r == Types.T_ARRAY));
979   }
980
981   public byte getReturnTypeCode () {
982     if (returnType < 0) {
983       returnType = Types.getReturnBuiltinType(signature);
984     }
985
986     return returnType;
987   }
988
989   /**
990    * what is the slot size of the return value
991    */
992   public int getReturnSize() {
993     if (retSize == -1){
994       switch (getReturnTypeCode()) {
995         case Types.T_VOID:
996           retSize = 0;
997           break;
998
999         case Types.T_LONG:
1000         case Types.T_DOUBLE:
1001           retSize = 2;
1002           break;
1003
1004         default:
1005           retSize = 1;
1006           break;
1007       }
1008     }
1009
1010     return retSize;
1011   }
1012
1013   public Class<? extends ChoiceGenerator<?>> getReturnChoiceGeneratorType (){
1014     switch (getReturnTypeCode()){
1015       case Types.T_BOOLEAN:
1016         return BooleanChoiceGenerator.class;
1017
1018       case Types.T_BYTE:
1019       case Types.T_CHAR:
1020       case Types.T_SHORT:
1021       case Types.T_INT:
1022         return IntChoiceGenerator.class;
1023
1024       case Types.T_LONG:
1025         return LongChoiceGenerator.class;
1026
1027       case Types.T_FLOAT:
1028         return FloatChoiceGenerator.class;
1029
1030       case Types.T_DOUBLE:
1031         return DoubleChoiceGenerator.class;
1032
1033       case Types.T_ARRAY:
1034       case Types.T_REFERENCE:
1035       case Types.T_VOID:
1036         return ReferenceChoiceGenerator.class;
1037     }
1038
1039     return null;
1040   }
1041
1042   /**
1043    * Returns the signature of the method.
1044    */
1045   public String getSignature () {
1046     return signature;
1047   }
1048
1049   @Override
1050   public String getGenericSignature() {
1051     return genericSignature;
1052   }
1053
1054   @Override
1055   public void setGenericSignature(String sig){
1056     genericSignature = sig;
1057   }
1058
1059   /**
1060    * Returns true if the method is static.
1061    */
1062   public boolean isStatic () {
1063     return ((modifiers & Modifier.STATIC) != 0);
1064   }
1065
1066   /**
1067    * is this a public method
1068    */
1069   public boolean isPublic() {
1070     return ((modifiers & Modifier.PUBLIC) != 0);
1071   }
1072   
1073   public boolean isPrivate() {
1074     return ((modifiers & Modifier.PRIVATE) != 0);
1075   }
1076   
1077   public boolean isProtected() {
1078     return ((modifiers & Modifier.PROTECTED) != 0);
1079   }
1080
1081   /**
1082    * Returns true if the method is synchronized.
1083    */
1084   public boolean isSynchronized () {
1085     return ((modifiers & Modifier.SYNCHRONIZED) != 0);
1086   }
1087
1088   // <2do> these modifiers are still java.lang.reflect internal and not
1089   // supported by public Modifier methods, but since we want to keep this 
1090   // similar to the Method reflection and we get the modifiers from the
1091   // classfile we implement this with explicit values
1092   
1093   public boolean isSynthetic(){
1094     return ((modifiers & 0x00001000) != 0);    
1095   } 
1096   public boolean isVarargs(){
1097     return ((modifiers & 0x00000080) != 0);        
1098   }
1099   
1100   /*
1101    * is this from a classfile or was it created by JPF (and hence should not
1102    * be visible in stacktraces etc)
1103    */
1104   public boolean isJPFInternal(){
1105     // note this has a different meaning than Method.isSynthetic(), which
1106     // is defined in VM spec 4.7.8. What we mean here is that this MethodInfo
1107     // is not associated with any class (such as direct call MethodInfos), but
1108     // there might be more in the future
1109     return (ci == null);
1110   }
1111   
1112   public String getUniqueName () {
1113     return uniqueName;
1114   }
1115   
1116   public boolean hasCode(){
1117     return (code != null);
1118   }
1119   
1120   public boolean hasEmptyBody (){
1121     // only instruction is a return
1122     return (code.length == 1 && (code[0] instanceof ReturnInstruction));
1123   }
1124
1125
1126   //--- parameter annotations
1127   //<2do> these are going away
1128   protected void startParameterAnnotations(int annotationCount){
1129     parameterAnnotations = new AnnotationInfo[annotationCount][];
1130   }
1131   protected void setParameterAnnotations(int index, AnnotationInfo[] ai){
1132     parameterAnnotations[index] = ai;
1133   }
1134   protected void finishParameterAnnotations(){
1135     // nothing
1136   }
1137
1138   public void setParameterAnnotations (AnnotationInfo[][] parameterAnnotations){
1139     this.parameterAnnotations = parameterAnnotations;
1140   }
1141   
1142   //--- thrown exceptions
1143   //<2do> these are going away
1144   protected void startTrownExceptions (int exceptionCount){
1145     thrownExceptionClassNames = new String[exceptionCount];
1146   }
1147   protected void setException (int index, String exceptionType){
1148     thrownExceptionClassNames[index] = Types.getClassNameFromTypeName(exceptionType);
1149   }
1150   protected void finishThrownExceptions(){
1151     // nothing
1152   }
1153
1154   public void setThrownExceptions (String[] exceptions){
1155     thrownExceptionClassNames = exceptions;
1156   }
1157   
1158
1159   //--- exception handler table initialization
1160   //<2do> these are going away
1161   protected void startExceptionHandlerTable (int handlerCount){
1162     exceptionHandlers = new ExceptionHandler[handlerCount];
1163   }
1164   protected void setExceptionHandler (int index, int startPc, int endPc, int handlerPc, String catchType){
1165     exceptionHandlers[index] = new ExceptionHandler(catchType, startPc, endPc, handlerPc);
1166   }
1167   protected void finishExceptionHandlerTable(){
1168     // nothing
1169   }
1170
1171   public void setExceptionHandlers (ExceptionHandler[] handlers){
1172     exceptionHandlers = handlers;
1173   }
1174   
1175   //--- local var table initialization
1176   // <2do> these are going away
1177   protected void startLocalVarTable (int localVarCount){
1178     localVars = new LocalVarInfo[localVarCount];
1179   }
1180   protected void setLocalVar(int index, String varName, String descriptor, int scopeStartPc, int scopeEndPc, int slotIndex){
1181     localVars[index] = new LocalVarInfo(varName, descriptor, "", scopeStartPc, scopeEndPc, slotIndex);
1182   }
1183   protected void finishLocalVarTable(){
1184     // nothing to do
1185   }
1186
1187   public void setLocalVarTable (LocalVarInfo[] locals){
1188     localVars = locals;
1189   }
1190   
1191   public void setLocalVarAnnotations (){
1192     if (localVars != null){
1193       for (VariableAnnotationInfo ai : getTargetTypeAnnotations(VariableAnnotationInfo.class)){
1194         for (int i = 0; i < ai.getNumberOfScopeEntries(); i++) {
1195           for (LocalVarInfo lv : localVars) {
1196             if (lv.getStartPC() == ai.getStartPC(i) && lv.getSlotIndex() == ai.getSlotIndex(i)) {
1197               lv.addTypeAnnotation(ai);
1198             }
1199           }
1200         }
1201       }
1202     }
1203   }
1204   
1205   public boolean hasTypeAnnotatedLocalVars (){
1206     if (localVars != null){
1207       for (LocalVarInfo lv : localVars){
1208         if (lv.hasTypeAnnotations()){
1209           return true;
1210         }
1211       }
1212     }
1213     
1214     return false;
1215   }
1216   
1217   public List<LocalVarInfo> getTypeAnnotatedLocalVars (){
1218     List<LocalVarInfo> list = null;
1219     
1220     if (localVars != null){
1221       for (LocalVarInfo lv : localVars){
1222         if (lv.hasTypeAnnotations()){
1223           if (list == null){
1224             list = new ArrayList<LocalVarInfo>();
1225           }
1226           list.add(lv);
1227         }
1228       }
1229     }
1230     
1231     if (list == null){
1232       list = Collections.emptyList();
1233     }
1234     
1235     return list;
1236   }
1237   
1238   public List<LocalVarInfo> getTypeAnnotatedLocalVars (String annotationClsName){
1239     List<LocalVarInfo> list = null;
1240     
1241     if (localVars != null){
1242       for (LocalVarInfo lv : localVars){
1243         AbstractTypeAnnotationInfo tai = lv.getTypeAnnotation(annotationClsName);
1244         if (tai != null){
1245           if (list == null){
1246             list = new ArrayList<LocalVarInfo>();
1247           }
1248           list.add(lv);
1249         }
1250       }
1251     }
1252     
1253     if (list == null){
1254       list = Collections.emptyList();
1255     }
1256     
1257     return list;
1258   }
1259   
1260   
1261   //--- line number table initialization
1262   // <2do> these are going away
1263   protected void startLineNumberTable(int lineNumberCount){
1264     int len = code.length;
1265     int[] ln = new int[len];
1266
1267     lineNumbers = ln;
1268   }
1269   protected void setLineNumber(int index, int lineNumber, int startPc){
1270     int len = code.length;
1271     int[] ln = lineNumbers;
1272
1273     for (int i=0; i<len; i++){
1274       Instruction insn = code[i];
1275       int pc = insn.getPosition();
1276
1277       if (pc == startPc){ // this is the first insn with this line number
1278         ln[i] = lineNumber;
1279         return;
1280       }
1281     }
1282   }
1283   protected void finishLineNumberTable (){
1284     int len = code.length;
1285     int[] ln = lineNumbers;
1286     int lastLine = ln[0];
1287
1288     for (int i=1; i<len; i++){
1289       if (ln[i] == 0){
1290         ln[i] = lastLine;
1291       } else {
1292         lastLine = ln[i];
1293       }
1294     }
1295   }
1296
1297   /**
1298    * note - this depends on that we already have a code array
1299    * and that the lines/startPcs are sorted (monotonic increasing)
1300    */
1301   public void setLineNumbers (int[] lines, int[] startPcs){
1302     int j=0;
1303     int lastLine = -1;
1304     
1305     int len = code.length;
1306     int[] ln = new int[len];
1307
1308     for (int i=0; i<len; i++){
1309       Instruction insn = code[i];
1310       int pc = insn.getPosition();
1311       
1312       if ((j < startPcs.length) && pc == startPcs[j]){
1313         lastLine = lines[j];
1314         j++;
1315       }
1316       
1317       ln[i] = lastLine;
1318     }
1319     
1320     lineNumbers = ln;
1321   }
1322
1323   /**
1324    * this version takes an already expanded line number array which has to be of
1325    * the same size as the code array
1326    */
1327   public void setLineNumbers (int[] lines){
1328     if (lines.length != code.length){
1329       throw new JPFException("inconsitent code/line number size");
1330     }
1331     lineNumbers = lines;
1332   }
1333   
1334   @Override
1335   public String toString() {
1336     return "MethodInfo[" + getFullName() + ']';
1337   }
1338   
1339   // for debugging purposes
1340   public void dump(){
1341     System.out.println("--- " + this);
1342     for (int i = 0; i < code.length; i++) {
1343       System.out.printf("%2d [%d]: %s\n", i, code[i].getPosition(), code[i].toString());
1344     }
1345   }
1346
1347   /**
1348    * Creates a method for a given class, by cloning this MethodInfo
1349    * and all the instructions belong to the method
1350    */
1351   public MethodInfo getInstanceFor(ClassInfo ci) {
1352     MethodInfo clone;
1353
1354     try {
1355       clone = (MethodInfo)super.clone();
1356       clone.ci = ci;
1357
1358       clone.globalId = mthTable.size();
1359       mthTable.add(this);
1360
1361       if(code == null) {
1362         clone.code = null;
1363       } else {
1364         clone.code = new Instruction[code.length];
1365
1366         for(int i=0; i<code.length; i++) {
1367           clone.code[i] = code[i].typeSafeClone(clone);
1368         }
1369       }
1370
1371     } catch (CloneNotSupportedException cnsx){
1372       cnsx.printStackTrace();
1373       return null;
1374     }
1375
1376     return clone;
1377   }
1378 }