src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.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.annotation.MJI;
  24 import gov.nasa.jpf.util.IntTable;
  25 import gov.nasa.jpf.util.JPFLogger;
  26 import gov.nasa.jpf.util.ObjectConverter;
  27 import gov.nasa.jpf.util.ObjectList;
  28 import gov.nasa.jpf.util.RunListener;
  29 import gov.nasa.jpf.util.RunRegistry;
  30 import gov.nasa.jpf.util.json.CGCall;
  31 import gov.nasa.jpf.util.json.JSONLexer;
  32 import gov.nasa.jpf.util.json.JSONObject;
  33 import gov.nasa.jpf.util.json.JSONParser;
  34 import gov.nasa.jpf.vm.choice.DoubleChoiceFromList;
  35 import gov.nasa.jpf.vm.choice.FloatChoiceFromList;
  36 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  37 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  38 import gov.nasa.jpf.vm.choice.LongChoiceFromList;
  39
  40 import java.io.FileInputStream;
  41 import java.io.FileNotFoundException;
  42 import java.io.IOException;
  43 import java.io.ObjectInputStream;
  44 import java.io.PrintStream;
  45 import java.util.BitSet;
  46 import java.util.List;
  47
  48 /**
  49  * native peer class for programmatic JPF interface (that can be used inside
  50  * of apps to verify - if you are aware of the danger that comes with it)
  51  *
  52  * this peer is a bit different in that it only uses static fields and methods because
  53  * its use is supposed to be JPF global (without classloader namespaces)
  54  */
  55 public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer {
  56   static final int MAX_COUNTERS = 127;
  57
  58   static boolean isInitialized;
  59
  60   // those are used to store search global int values (e.g. from TestJPF derived classes)
  61   static int[] counter;
  62   static IntTable<String> map;
  63
  64   public static int heuristicSearchValue;
  65
  66   static boolean supportIgnorePath;
  67   static boolean breakSingleChoice;
  68   static boolean enableAtomic;
  69
  70   static Config config;  // we need to keep this around for CG creation
  71
  72   // our const ChoiceGenerator ctor argtypes
  73   static Class[] cgArgTypes = { Config.class, String.class };
  74   // this is our cache for ChoiceGenerator ctor parameters
  75   static Object[] cgArgs = { null, null };
  76
  77   static BitSet[] bitSets;
  78   static int nextBitSet;
  79
  80   static PrintStream out;
  81
  82   public static boolean init (Config conf) {
  83
  84     if (!isInitialized){
  85       supportIgnorePath = conf.getBoolean("vm.verify.ignore_path");
  86       breakSingleChoice = conf.getBoolean("cg.break_single_choice");
  87       enableAtomic = conf.getBoolean("cg.enable_atomic", true);
  88
  89       heuristicSearchValue = conf.getInt("search.heuristic.default_value");
  90
  91       counter = null;
  92       map = null;
  93
  94       config = conf;
  95
  96       String outFile = conf.getString("vm.verify.output_file");
  97       if (outFile != null){
  98         try {
  99           out = new PrintStream(outFile);
 100         } catch (FileNotFoundException fnx){
 101           System.err.println("error: could not open verify output file " + outFile + ", using System.out");
 102           out = System.out;
 103         }
 104       } else {
 105         out = System.out;
 106       }
 107
 108       Verify.setPeerClass( JPF_gov_nasa_jpf_vm_Verify.class);
 109
 110       RunRegistry.getDefaultRegistry().addListener( new RunListener() {
 111         @Override
 112                     public void reset (RunRegistry reg){
 113           isInitialized = false;
 114         }
 115       });
 116     }
 117     return true;
 118   }
 119
 120
 121   public static final int NO_VALUE = -1;
 122
 123   @MJI
 124   public static int getValue__Ljava_lang_String_2__I (MJIEnv env, int clsObjRef, int keyRef) {
 125     if (map == null) {
 126       return NO_VALUE;
 127     } else {
 128       String key = env.getStringObject(keyRef);
 129       IntTable.Entry<String> e = map.get(key);
 130       if (e != null) {
 131         return e.val;
 132       } else {
 133         return NO_VALUE;
 134       }
 135     }
 136   }
 137
 138   @MJI
 139   public static void putValue__Ljava_lang_String_2I__V (MJIEnv env, int clsObjRef, int keyRef, int val) {
 140     if (map == null) {
 141       map = new IntTable<String>();
 142     }
 143
 144     String key = env.getStringObject(keyRef);
 145     map.put(key, val);
 146   }
 147
 148   @MJI
 149   public static int getCounter__I__I (MJIEnv env, int clsObjRef, int counterId) {
 150     if ((counter == null) || (counterId < 0) || (counterId >= counter.length)) {
 151       return 0;
 152     }
 153
 154     return counter[counterId];
 155   }
 156
 157   private static void ensureCounterCapacity (int counterId){
 158     if (counter == null) {
 159       counter = new int[(counterId >= MAX_COUNTERS) ? counterId+1 : MAX_COUNTERS];
 160     } else if (counterId >= counter.length) {
 161       int[] newCounter = new int[counterId+1];
 162       System.arraycopy(counter, 0, newCounter, 0, counter.length);
 163       counter = newCounter;
 164     }
 165   }
 166
 167   @MJI
 168   public static void resetCounter__I__V (MJIEnv env, int clsObjRef, int counterId) {
 169     if ((counter == null) || (counterId < 0) || (counterId >= counter.length)) {
 170       return;
 171     }
 172     counter[counterId] = 0;
 173   }
 174
 175   @MJI
 176   public static void setCounter__II__V (MJIEnv env, int clsObjRef, int counterId, int val) {
 177     if (counterId < 0){
 178       return;
 179     }
 180
 181     ensureCounterCapacity(counterId);
 182     counter[counterId] = val;
 183   }
 184
 185   @MJI
 186   public static int incrementCounter__I__I (MJIEnv env, int clsObjRef, int counterId) {
 187     if (counterId < 0) {
 188       return 0;
 189     }
 190
 191     ensureCounterCapacity(counterId);
 192     return ++counter[counterId];
 193   }
 194
 195   private static void checkBitSetId(int id) {
 196     if (bitSets == null) {
 197       bitSets = new BitSet[id + 1];
 198     } else if (id >= bitSets.length) {
 199       BitSet[] newBitSets = new BitSet[id + 1];
 200       System.arraycopy(bitSets, 0, newBitSets, 0, bitSets.length);
 201       bitSets = newBitSets;
 202     }
 203
 204     if (bitSets[id] == null) {
 205       bitSets[id] = new BitSet();
 206     }
 207   }
 208
 209   @MJI
 210   public static void setBitInBitSet__IIZ__V(MJIEnv env, int clsObjRef, int id, int bitNum, boolean value) {
 211     checkBitSetId(id);
 212     bitSets[id].set(bitNum, value);
 213   }
 214
 215   @MJI
 216   public static boolean getBitInBitSet__II__Z(MJIEnv env, int clsObjRef, int id, int bitNum) {
 217     checkBitSetId(id);
 218     return bitSets[id].get(bitNum);
 219   }
 220
 221   @MJI
 222   public static long currentTimeMillis____J (MJIEnv env, int clsObjRef) {
 223     return System.currentTimeMillis();
 224   }
 225
 226   @MJI
 227   public static String getType (int objRef, MJIEnv env) {
 228     return Types.getTypeName(env.getElementInfo(objRef).getType());
 229   }
 230
 231   @MJI
 232   public static void addComment__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int stringRef) {
 233     SystemState ss = env.getSystemState();
 234     String      cmt = env.getStringObject(stringRef);
 235     ss.getTrail().setAnnotation(cmt);
 236   }
 237
 238   @MJI
 239   public static void assertTrue__Z__V (MJIEnv env, int clsObjRef, boolean b) {
 240     if (!b) {
 241       env.throwException("java.lang.AssertionError", "assertTrue failed");
 242     }
 243   }
 244
 245   // those are evil - use with extreme care. If something blocks inside of
 246   // an atomic section we have to raise an exception
 247
 248   @MJI
 249   public static void beginAtomic____V (MJIEnv env, int clsObjRef) {
 250     if (enableAtomic){
 251       ThreadInfo tiAtomic = env.getThreadInfo();
 252
 253       if (tiAtomic.getScheduler().setsBeginAtomicCG(tiAtomic)){
 254         env.repeatInvocation();
 255         return;
 256       }
 257
 258       env.getSystemState().incAtomic();
 259     }
 260   }
 261
 262   @MJI
 263   public static void endAtomic____V (MJIEnv env, int clsObjRef) {
 264     if (enableAtomic){
 265       ThreadInfo tiAtomic = env.getThreadInfo();
 266
 267       if (!tiAtomic.isFirstStepInsn()){
 268         env.getSystemState().decAtomic();
 269       }
 270
 271       if (tiAtomic.getScheduler().setsEndAtomicCG(tiAtomic)){
 272         env.repeatInvocation();
 273         return;
 274       }
 275     }
 276   }
 277
 278   @MJI
 279   public static void busyWait__J__V (MJIEnv env, int clsObjRef, long duration) {
 280     // nothing required here (we systematically explore scheduling
 281     // sequences anyway), but we need to intercept the call
 282   }
 283
 284   @MJI
 285   public static void ignoreIf__Z__V (MJIEnv env, int clsObjRef, boolean cond) {
 286     if (supportIgnorePath) {
 287       env.getSystemState().setIgnored(cond);
 288     }
 289   }
 290
 291   @MJI
 292   public static void interesting__Z__V (MJIEnv env, int clsObjRef, boolean cond) {
 293     env.getSystemState().setInteresting(cond);
 294   }
 295
 296   @MJI
 297   public static void breakTransition__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int reasonRef){
 298     ThreadInfo ti = env.getThreadInfo();
 299     String reason = env.getStringObject(reasonRef);
 300     ti.breakTransition(reason);
 301   }
 302
 303   /**
 304    * mostly for debugging purposes - this does not optimize away single choice CGs
 305    */
 306   @MJI
 307   public int breakTransition__Ljava_lang_String_2II__I (MJIEnv env, int clsObjRef, int reasonRef, int min, int max) {
 308     ThreadInfo ti = env.getThreadInfo();
 309     SystemState ss = env.getSystemState();
 310     String reason = env.getStringObject(reasonRef);
 311
 312     if (!ti.isFirstStepInsn()) { // first time around
 313       IntChoiceGenerator cg = new IntIntervalGenerator( reason, min,max);
 314       if (ss.setNextChoiceGenerator(cg)){
 315         env.repeatInvocation();
 316       }
 317       return -1;
 318
 319     } else {
 320       return getNextChoice(ss, reason, IntChoiceGenerator.class, Integer.class);
 321     }
 322   }
 323
 324   @MJI
 325   public static boolean isCalledFromClass__Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
 326                                            int clsNameRef) {
 327     String refClassName = env.getStringObject(clsNameRef);
 328     ThreadInfo ti = env.getThreadInfo();
 329
 330     StackFrame caller = ti.getLastInvokedStackFrame();
 331     if (caller != null){
 332       ClassInfo ci = caller.getClassInfo();
 333       return ci.isInstanceOf(refClassName);
 334     }
 335
 336     return false;
 337   }
 338
 339
 340   static <T extends ChoiceGenerator<?>> T createChoiceGenerator (Class<T> cgClass, SystemState ss, String id) {
 341     T gen = null;
 342
 343     cgArgs[0] = config;
 344     cgArgs[1] = id; // good thing we are not multithreaded (other fields are const)
 345
 346     String key = id + ".class";
 347     gen = config.getEssentialInstance(key, cgClass, cgArgTypes, cgArgs);
 348     return gen;
 349   }
 350
 351   static <T> T registerChoiceGenerator (MJIEnv env, SystemState ss, ThreadInfo ti, ChoiceGenerator<T> cg, T dummyVal){
 352
 353     int n = cg.getTotalNumberOfChoices();
 354     if (n == 0) {
 355       // nothing, just return the default value
 356
 357     } else if (n == 1 && !breakSingleChoice) {
 358       // no choice -> no CG optimization
 359       cg.advance();
 360       return cg.getNextChoice();
 361
 362     } else {
 363       if (ss.setNextChoiceGenerator(cg)){
 364         env.repeatInvocation();
 365       }
 366     }
 367
 368     return dummyVal;
 369   }
 370
 371   static <T,C extends ChoiceGenerator<T>> T getNextChoice (SystemState ss, String id, Class<C> cgClass, Class<T> choiceClass){
 372     ChoiceGenerator<?> cg = ss.getCurrentChoiceGenerator(id, cgClass);
 373
 374     assert (cg != null) : "no ChoiceGenerator of type " + cgClass.getName();
 375     return ((ChoiceGenerator<T>)cg).getNextChoice();
 376   }
 377
 378   @MJI
 379   public static boolean getBoolean____Z (MJIEnv env, int clsObjRef) {
 380     ThreadInfo ti = env.getThreadInfo();
 381     SystemState ss = env.getSystemState();
 382     ChoiceGenerator<?> cg;
 383
 384     if (!ti.isFirstStepInsn()) { // first time around
 385       cg = new BooleanChoiceGenerator(config, "verifyGetBoolean");
 386       if (ss.setNextChoiceGenerator(cg)){
 387         env.repeatInvocation();
 388       }
 389       return true;  // not used if we repeat
 390
 391     } else {  // this is what really returns results
 392       return getNextChoice(ss,"verifyGetBoolean", BooleanChoiceGenerator.class,Boolean.class);
 393     }
 394   }
 395
 396   @MJI
 397   public static boolean getBoolean__Z__Z (MJIEnv env, int clsObjRef, boolean falseFirst) {
 398     ThreadInfo ti = env.getThreadInfo();
 399     SystemState ss = env.getSystemState();
 400     ChoiceGenerator<?> cg;
 401
 402     if (!ti.isFirstStepInsn()) { // first time around
 403       cg = new BooleanChoiceGenerator( "verifyGetBoolean(Z)", falseFirst );
 404       if (ss.setNextChoiceGenerator(cg)){
 405         env.repeatInvocation();
 406       }
 407       return true;  // not used if we repeat
 408
 409     } else {  // this is what really returns results
 410       return getNextChoice(ss,"verifyGetBoolean(Z)", BooleanChoiceGenerator.class, Boolean.class);
 411     }
 412   }
 413
 414   @MJI
 415   public static int getInt__II__I (MJIEnv env, int clsObjRef, int min, int max) {
 416     ThreadInfo ti = env.getThreadInfo();
 417     SystemState ss = env.getSystemState();
 418
 419     if (!ti.isFirstStepInsn()) { // first time around
 420
 421       if (min > max){
 422         int t = max;
 423         max = min;
 424         min = t;
 425       }
 426
 427       IntChoiceGenerator cg = new IntIntervalGenerator( "verifyGetInt(II)", min,max);
 428       return registerChoiceGenerator(env,ss,ti,cg,0);
 429
 430     } else {
 431       return getNextChoice(ss, "verifyGetInt(II)", IntChoiceGenerator.class, Integer.class);
 432     }
 433   }
 434
 435   static int getIntFromList (MJIEnv env, int[] values){
 436     ThreadInfo ti = env.getThreadInfo();
 437     SystemState ss = env.getSystemState();
 438
 439     if (!ti.isFirstStepInsn()) { // first time around
 440       ChoiceGenerator<Integer> cg = new IntChoiceFromSet( "verifyGetIntSet([I)", values);
 441       return registerChoiceGenerator(env,ss,ti,cg,0);
 442
 443     } else {
 444       return getNextChoice(ss, "verifyGetIntSet([I)", IntChoiceGenerator.class, Integer.class);
 445     }
 446   }
 447
 448   @MJI
 449   public static int getIntFromList___3I__I (MJIEnv env, int clsObjRef, int valArrayRef){
 450     int[] values = env.getIntArrayObject(valArrayRef);
 451     return getIntFromList( env, values);
 452   }
 453
 454   @MJI
 455   public static int getInt__Ljava_lang_String_2__I (MJIEnv env, int clsObjRef, int idRef) {
 456     ThreadInfo ti = env.getThreadInfo();
 457     SystemState ss = env.getSystemState();
 458
 459
 460     if (!ti.isFirstStepInsn()) { // first time around
 461       String id = env.getStringObject(idRef);
 462       IntChoiceGenerator cg = createChoiceGenerator( IntChoiceGenerator.class, ss, id);
 463       return registerChoiceGenerator(env,ss,ti,cg, 0);
 464
 465     } else {
 466       String id = env.getStringObject(idRef);
 467       return getNextChoice(ss, id, IntChoiceGenerator.class,Integer.class);
 468     }
 469   }
 470
 471   static long getLongFromList (MJIEnv env, long[] values){
 472     ThreadInfo ti = env.getThreadInfo();
 473     SystemState ss = env.getSystemState();
 474
 475     if (!ti.isFirstStepInsn()) { // first time around
 476       ChoiceGenerator<Long> cg = new LongChoiceFromList( "verifyLongList([J)", values);
 477       return registerChoiceGenerator(env,ss,ti,cg,0L);
 478
 479     } else {
 480       return getNextChoice(ss, "verifyLongList([J)", LongChoiceGenerator.class, Long.class);
 481     }
 482   }
 483
 484   @MJI
 485   public static long getLongFromList___3J__J (MJIEnv env, int clsObjRef, int valArrayRef){
 486     long[] values = env.getLongArrayObject(valArrayRef);
 487     return getLongFromList( env, values);
 488   }
 489
 490   @MJI
 491   public static int getObject__Ljava_lang_String_2__Ljava_lang_Object_2 (MJIEnv env, int clsObjRef, int idRef) {
 492     ThreadInfo ti = env.getThreadInfo();
 493     SystemState ss = env.getSystemState();
 494
 495     if (!ti.isFirstStepInsn()) { // first time around
 496       String id = env.getStringObject(idRef);
 497       ReferenceChoiceGenerator cg = createChoiceGenerator( ReferenceChoiceGenerator.class, ss, id);
 498       return registerChoiceGenerator(env,ss,ti,cg, MJIEnv.NULL);
 499
 500     } else {
 501       String id = env.getStringObject(idRef);
 502       return getNextChoice(ss, id, ReferenceChoiceGenerator.class,Integer.class);
 503     }
 504   }
 505
 506   @MJI
 507   public static double getDouble__Ljava_lang_String_2__D (MJIEnv env, int clsObjRef, int idRef) {
 508     ThreadInfo ti = env.getThreadInfo();
 509     SystemState ss = env.getSystemState();
 510
 511     if (!ti.isFirstStepInsn()) { // first time around
 512       String id = env.getStringObject(idRef);
 513       DoubleChoiceGenerator cg = createChoiceGenerator( DoubleChoiceGenerator.class, ss, id);
 514       return registerChoiceGenerator(env,ss,ti,cg, 0.0);
 515
 516     } else {
 517       String id = env.getStringObject(idRef);
 518       return getNextChoice(ss, id, DoubleChoiceGenerator.class,Double.class);
 519     }
 520   }
 521
 522   @MJI
 523   public static double getDoubleFromList (MJIEnv env, double[] values){
 524     ThreadInfo ti = env.getThreadInfo();
 525     SystemState ss = env.getSystemState();
 526
 527     if (!ti.isFirstStepInsn()) { // first time around
 528       ChoiceGenerator<Double> cg = new DoubleChoiceFromList("verifyDoubleList([D)", values);
 529       return registerChoiceGenerator(env,ss,ti,cg, 0.0);
 530
 531     } else {
 532       return getNextChoice(ss, "verifyDoubleList([D)", DoubleChoiceFromList.class,Double.class);
 533     }
 534   }
 535
 536   @MJI
 537   public static double getDoubleFromList___3D__D (MJIEnv env, int clsObjRef, int valArrayRef){
 538     double[] values = env.getDoubleArrayObject(valArrayRef);
 539     return getDoubleFromList( env, values);
 540   }
 541
 542   @MJI
 543   public static float getFloatFromList (MJIEnv env, float[] values){
 544     ThreadInfo ti = env.getThreadInfo();
 545     SystemState ss = env.getSystemState();
 546
 547     if (!ti.isFirstStepInsn()) { // first time around
 548       ChoiceGenerator<Float> cg = new FloatChoiceFromList("verifyFloatList([F)", values);
 549       return registerChoiceGenerator(env,ss,ti,cg, 0.0f);
 550
 551     } else {
 552       return getNextChoice(ss, "verifyFloatList([F)", FloatChoiceFromList.class, Float.class);
 553     }
 554   }
 555
 556   @MJI
 557   public static float getFloatFromList___3F__F (MJIEnv env, int clsObjRef, int valArrayRef){
 558     float[] values = env.getFloatArrayObject(valArrayRef);
 559     return getFloatFromList( env, values);
 560   }
 561
 562   @MJI
 563   public static void threadPrint__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
 564     String s = env.getStringObject(sRef);
 565     ThreadInfo ti = env.getThreadInfo();
 566     System.out.print(ti.getName());
 567     System.out.print(s);
 568   }
 569
 570   @MJI
 571   public static void print__Ljava_lang_String_2I__V (MJIEnv env, int clsRef, int sRef, int val){
 572     String s = env.getStringObject(sRef);
 573     System.out.print(s + " : " + val);
 574   }
 575
 576   @MJI
 577   public static void print__Ljava_lang_String_2Z__V (MJIEnv env, int clsRef, int sRef, boolean val){
 578     String s = env.getStringObject(sRef);
 579     System.out.print(s + " : " + val);
 580   }
 581
 582   @MJI
 583   public static void print___3Ljava_lang_String_2__V (MJIEnv env, int clsRef, int argsRef){
 584     int n = env.getArrayLength(argsRef);
 585     for (int i=0; i<n; i++){
 586       int aref = env.getReferenceArrayElement(argsRef, i);
 587       String s = env.getStringObject(aref);
 588       System.out.print(s);
 589     }
 590   }
 591
 592   @MJI
 593   public static void print__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
 594     String s = env.getStringObject(sRef);
 595     System.out.print(s);
 596   }
 597
 598   @MJI
 599   public static void println__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
 600     String s = env.getStringObject(sRef);
 601     System.out.println(s);
 602   }
 603
 604   @MJI
 605   public static void threadPrintln__Ljava_lang_String_2__V (MJIEnv env, int clsRef, int sRef){
 606     threadPrint__Ljava_lang_String_2__V(env, clsRef, sRef);
 607     System.out.println();
 608   }
 609
 610
 611   @MJI
 612   public static void println____V (MJIEnv env, int clsRef){
 613     System.out.println();
 614   }
 615
 616   //--- various attribute test methods
 617
 618   private static int getAttribute (MJIEnv env, Object a){
 619     if (a != null) {
 620       if (a instanceof Integer) {
 621         return ((Integer) a).intValue();
 622       } else {
 623         env.throwException("java.lang.RuntimeException", "element attribute not an Integer: " + a);
 624       }
 625     }
 626
 627     return 0;
 628   }
 629
 630   private static int getAttributeList (MJIEnv env, Object a){
 631     if (a != null) {
 632       int l = ObjectList.size(a);
 633       int[] attrs = new int[l];
 634       int i = 0;
 635       for (Integer v : ObjectList.typedIterator(a, Integer.class)) {
 636         attrs[i++] = v;
 637       }
 638       if (i != l) {
 639         env.throwException("java.lang.RuntimeException", "found non-Integer attributes");
 640         return 0;
 641       }
 642
 643       return env.newIntArray(attrs);
 644
 645     } else {
 646       return MJIEnv.NULL;
 647     }
 648   }
 649
 650   @MJI
 651   public static void setObjectAttribute__Ljava_lang_Object_2I__V (MJIEnv env, int clsRef, int oRef, int attr){
 652     if (oRef != MJIEnv.NULL){
 653       ElementInfo ei = env.getElementInfo(oRef);
 654       ei.setObjectAttr(Integer.valueOf(attr));
 655     }
 656   }
 657
 658   @MJI
 659   public static int getObjectAttribute__Ljava_lang_Object_2__I (MJIEnv env, int clsRef, int oRef){
 660     if (oRef != MJIEnv.NULL){
 661       ElementInfo ei = env.getElementInfo(oRef);
 662       return getAttribute( env, ei.getObjectAttr());
 663     }
 664
 665     return 0;
 666   }
 667
 668   @MJI
 669   public static void addObjectAttribute__Ljava_lang_Object_2I__V (MJIEnv env, int clsRef, int oRef, int attr){
 670     if (oRef != MJIEnv.NULL){
 671       ElementInfo ei = env.getElementInfo(oRef);
 672       ei.addObjectAttr(Integer.valueOf(attr));
 673     }
 674   }
 675
 676   @MJI
 677   public static int getObjectAttributes__Ljava_lang_Object_2___3I (MJIEnv env, int clsRef, int oRef){
 678     if (oRef != MJIEnv.NULL){
 679       ElementInfo ei = env.getElementInfo(oRef);
 680       return getAttributeList( env, ei.getObjectAttr());
 681     }
 682
 683     return MJIEnv.NULL;
 684   }
 685
 686   @MJI
 687   public static void setFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V (MJIEnv env, int clsRef,
 688                                                                                     int oRef, int fnRef, int attr){
 689     if (oRef != MJIEnv.NULL){
 690       ElementInfo ei = env.getElementInfo(oRef);
 691       if (ei != null){
 692         String fname = env.getStringObject(fnRef);
 693         FieldInfo fi = ei.getFieldInfo(fname);
 694
 695         if (fi != null) {
 696           ei.setFieldAttr(fi, Integer.valueOf(attr));
 697         } else {
 698           env.throwException("java.lang.NoSuchFieldException",
 699                   ei.getClassInfo().getName() + '.' + fname);
 700         }
 701       } else {
 702         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 703       }
 704     }
 705   }
 706
 707   @MJI
 708   public static int getFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2__I (MJIEnv env, int clsRef,
 709                                                                                     int oRef, int fnRef){
 710     if (oRef != MJIEnv.NULL){
 711       ElementInfo ei = env.getElementInfo(oRef);
 712       if (ei != null){
 713         String fname = env.getStringObject(fnRef);
 714         FieldInfo fi = ei.getFieldInfo(fname);
 715
 716         if (fi != null) {
 717           return getAttribute( env, ei.getFieldAttr(fi));
 718         } else {
 719           env.throwException("java.lang.NoSuchFieldException",
 720                   ei.toString() + '.' + fname);
 721         }
 722       } else {
 723         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 724       }
 725     }
 726
 727     return 0;
 728   }
 729
 730   @MJI
 731   public static void addFieldAttribute__Ljava_lang_Object_2Ljava_lang_String_2I__V (MJIEnv env, int clsRef,
 732                                                                                     int oRef, int fnRef, int attr){
 733     if (oRef != MJIEnv.NULL){
 734       ElementInfo ei = env.getElementInfo(oRef);
 735       if (ei != null){
 736         String fname = env.getStringObject(fnRef);
 737         FieldInfo fi = ei.getFieldInfo(fname);
 738
 739         if (fi != null) {
 740           ei.addFieldAttr(fi, Integer.valueOf(attr));
 741         } else {
 742           env.throwException("java.lang.NoSuchFieldException",
 743                   ei.getClassInfo().getName() + '.' + fname);
 744         }
 745       } else {
 746         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 747       }
 748     }
 749   }
 750
 751   @MJI
 752   public static int getFieldAttributes__Ljava_lang_Object_2Ljava_lang_String_2___3I (MJIEnv env, int clsRef,
 753                                                                                     int oRef, int fnRef){
 754     if (oRef != MJIEnv.NULL){
 755       ElementInfo ei = env.getElementInfo(oRef);
 756       if (ei != null){
 757         String fname = env.getStringObject(fnRef);
 758         FieldInfo fi = ei.getFieldInfo(fname);
 759
 760         if (fi != null) {
 761           return getAttributeList( env, ei.getFieldAttr(fi));
 762         } else {
 763           env.throwException("java.lang.NoSuchFieldException",
 764                   ei.toString() + '.' + fname);
 765         }
 766       } else {
 767         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 768       }
 769     }
 770
 771     return MJIEnv.NULL;
 772   }
 773
 774   @MJI
 775   public static void setLocalAttribute__Ljava_lang_String_2I__V (MJIEnv env, int clsRef, int varRef, int attr) {
 776     String slotName = env.getStringObject(varRef);
 777     StackFrame frame = env.getModifiableCallerStackFrame(); // we are executing in a NativeStackFrame
 778
 779     if (!frame.getMethodInfo().isStatic() &&  slotName.equals("this")) {
 780       frame.setLocalAttr(0, Integer.valueOf(attr)); // only for instance methods of course
 781
 782     } else {
 783       int slotIdx = frame.getLocalVariableSlotIndex(slotName);
 784       if (slotIdx >= 0) {
 785         frame.setLocalAttr(slotIdx, Integer.valueOf(attr));
 786       } else {
 787         env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
 788       }
 789     }
 790   }
 791
 792   @MJI
 793   public static int getLocalAttribute__Ljava_lang_String_2__I (MJIEnv env, int clsRef, int varRef) {
 794     String slotName = env.getStringObject(varRef);
 795     ThreadInfo ti = env.getThreadInfo();
 796     StackFrame frame = env.getCallerStackFrame();
 797
 798     int slotIdx = frame.getLocalVariableSlotIndex(slotName);
 799     if (slotIdx >= 0) {
 800       return getAttribute( env, frame.getLocalAttr(slotIdx));
 801     } else {
 802       env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
 803       return 0;
 804     }
 805   }
 806
 807   @MJI
 808   public static void addLocalAttribute__Ljava_lang_String_2I__V (MJIEnv env, int clsRef, int varRef, int attr) {
 809     String slotName = env.getStringObject(varRef);
 810     StackFrame frame = env.getModifiableCallerStackFrame(); // we are executing in a NativeStackFrame
 811
 812     if (!frame.getMethodInfo().isStatic() &&  slotName.equals("this")) {
 813       frame.addLocalAttr(0, Integer.valueOf(attr)); // only for instance methods of course
 814
 815     } else {
 816       int slotIdx = frame.getLocalVariableSlotIndex(slotName);
 817       if (slotIdx >= 0) {
 818         frame.addLocalAttr(slotIdx, Integer.valueOf(attr));
 819       } else {
 820         env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
 821       }
 822     }
 823   }
 824
 825   @MJI
 826   public static int getLocalAttributes__Ljava_lang_String_2___3I (MJIEnv env, int clsRef, int varRef) {
 827     String slotName = env.getStringObject(varRef);
 828     ThreadInfo ti = env.getThreadInfo();
 829     StackFrame frame = env.getCallerStackFrame();
 830
 831     int slotIdx = frame.getLocalVariableSlotIndex(slotName);
 832     if (slotIdx >= 0) {
 833       return getAttributeList( env, frame.getLocalAttr(slotIdx));
 834     } else {
 835       env.throwException("java.lang.RuntimeException", "local variable not found: " + slotName);
 836     }
 837
 838     return MJIEnv.NULL;
 839   }
 840
 841   @MJI
 842   public static void setElementAttribute__Ljava_lang_Object_2II__V (MJIEnv env, int clsRef,
 843                                                                     int oRef, int idx, int attr){
 844     if (oRef != MJIEnv.NULL){
 845       ElementInfo ei = env.getElementInfo(oRef);
 846
 847       if (ei != null){
 848         if (ei.isArray()) {
 849           if (idx < ei.arrayLength()) {
 850             ei.setElementAttr(idx, Integer.valueOf(attr));
 851           } else {
 852             env.throwException("java.lang.ArrayIndexOutOfBoundsException",
 853                     Integer.toString(idx));
 854           }
 855         } else {
 856           env.throwException("java.lang.RuntimeException",
 857                   "not an array: " + ei);
 858         }
 859       } else {
 860         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 861       }
 862     }
 863   }
 864
 865   @MJI
 866   public static int getElementAttribute__Ljava_lang_Object_2I__I (MJIEnv env, int clsRef,
 867                                                                   int oRef, int idx){
 868     if (oRef != MJIEnv.NULL){
 869       ElementInfo ei = env.getElementInfo(oRef);
 870
 871       if (ei != null) {
 872         if (ei.isArray()) {
 873           if (idx < ei.arrayLength()) {
 874             return getAttribute( env, ei.getElementAttr( idx));
 875           } else {
 876             env.throwException("java.lang.ArrayIndexOutOfBoundsException",
 877                     Integer.toString(idx));
 878           }
 879         } else {
 880           env.throwException("java.lang.RuntimeException",
 881                   "not an array: " + ei);
 882         }
 883       } else {
 884         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 885       }
 886     }
 887
 888     return 0;
 889   }
 890
 891   @MJI
 892   public static void addElementAttribute__Ljava_lang_Object_2II__V (MJIEnv env, int clsRef,
 893                                                                     int oRef, int idx, int attr){
 894     if (oRef != MJIEnv.NULL){
 895       ElementInfo ei = env.getElementInfo(oRef);
 896
 897       if (ei != null){
 898         if (ei.isArray()) {
 899           if (idx < ei.arrayLength()) {
 900             ei.addElementAttr(idx, Integer.valueOf(attr));
 901           } else {
 902             env.throwException("java.lang.ArrayIndexOutOfBoundsException",
 903                     Integer.toString(idx));
 904           }
 905         } else {
 906           env.throwException("java.lang.RuntimeException",
 907                   "not an array: " + ei);
 908         }
 909       } else {
 910         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 911       }
 912     }
 913   }
 914
 915   @MJI
 916   public static int getElementAttributes__Ljava_lang_Object_2I___3I (MJIEnv env, int clsRef,
 917                                                                         int oRef, int idx){
 918     if (oRef != MJIEnv.NULL){
 919       ElementInfo ei = env.getElementInfo(oRef);
 920       if (ei != null) {
 921         if (ei.isArray()) {
 922           if (idx < ei.arrayLength()) {
 923             return getAttributeList( env, ei.getElementAttr( idx));
 924           } else {
 925             env.throwException("java.lang.ArrayIndexOutOfBoundsException",
 926                     Integer.toString(idx));
 927           }
 928         } else {
 929           env.throwException("java.lang.RuntimeException",
 930                   "not an array: " + ei);
 931         }
 932       } else {
 933         env.throwException("java.lang.RuntimeException", "illegal reference value: " + oRef);
 934       }
 935     }
 936
 937     return MJIEnv.NULL;
 938   }
 939
 940
 941   /**
 942    *  deprecated, use getBoolean()
 943    */
 944   @MJI
 945   public static boolean randomBool (MJIEnv env, int clsObjRef) {
 946     //SystemState ss = env.getSystemState();
 947     //return (ss.random(2) != 0);
 948
 949     return getBoolean____Z(env, clsObjRef);
 950   }
 951
 952
 953
 954   /**
 955    * deprecated, use getInt
 956    */
 957   @MJI
 958   public static int random__I__I (MJIEnv env, int clsObjRef, int x) {
 959    return getInt__II__I(env, clsObjRef, 0, x);
 960   }
 961
 962   static void boring__Z__V (MJIEnv env, int clsObjRef, boolean b) {
 963     env.getSystemState().setBoring(b);
 964   }
 965
 966   @MJI
 967   public static boolean isRunningInJPF____Z(MJIEnv env, int clsObjRef) {
 968     return true;
 969   }
 970
 971   @MJI
 972   public static boolean vmIsMatchingStates____Z(MJIEnv env, int clsObjRef) {
 973     return env.getVM().getStateSet() != null;
 974   }
 975
 976   @MJI
 977   public static void storeTrace__Ljava_lang_String_2Ljava_lang_String_2__V (MJIEnv env, int clsObjRef,
 978                                       int filenameRef, int commentRef) {
 979     String fileName = env.getStringObject(filenameRef);
 980     String comment = env.getStringObject(commentRef);
 981     env.getVM().storeTrace(fileName, comment, config.getBoolean("trace.verbose", false));
 982   }
 983
 984   @MJI
 985   public static void terminateSearch____V (MJIEnv env, int clsObjRef) {
 986     JPF jpf = env.getVM().getJPF();
 987     jpf.getSearch().terminate();
 988   }
 989
 990   @MJI public static void setHeuristicSearchValue__I__V (MJIEnv env, int clsObjRef, int val){
 991     heuristicSearchValue =  val;
 992   }
 993
 994   @MJI public static int getHeuristicSearchValue____I (MJIEnv env, int clsObjRef){
 995     return heuristicSearchValue;
 996   }
 997
 998   @MJI public static void resetHeuristicSearchValue____V (MJIEnv env, int clsObjRef){
 999     heuristicSearchValue = config.getInt("search.heuristic.default_value");
1000   }
1001
1002
1003
1004   @MJI
1005   public static boolean isTraceReplay____Z (MJIEnv env, int clsObjRef) {
1006     return env.getVM().isTraceReplay();
1007   }
1008
1009   @MJI
1010   public static boolean isShared__Ljava_lang_Object_2__Z (MJIEnv env, int clsObjRef, int objRef){
1011     if (objRef != MJIEnv.NULL){
1012       ElementInfo ei = env.getElementInfo(objRef);
1013       if (ei != null){
1014         return ei.isShared();
1015       }
1016     }
1017
1018     return false;
1019   }
1020
1021   @MJI
1022   public static void setShared__Ljava_lang_Object_2Z__V (MJIEnv env, int clsObjRef, int objRef, boolean isShared) {
1023     if (objRef != MJIEnv.NULL){
1024       ElementInfo ei = env.getElementInfo(objRef);
1025       if (ei != null){
1026         if (ei.getClassInfo() == ClassLoaderInfo.getCurrentSystemClassLoader().getClassClassInfo()) {
1027           // it's a class object, set static fields shared
1028           ei = env.getStaticElementInfo(objRef);
1029         }
1030
1031         if (ei.isShared() != isShared) {
1032           ei = ei.getModifiableInstance();
1033           ei.setShared( env.getThreadInfo(), isShared);
1034         }
1035       }
1036     }
1037   }
1038
1039   @MJI
1040   public static void freezeSharedness__Ljava_lang_Object_2Z__V (MJIEnv env, int clsObjRef, int objRef, boolean freeze) {
1041     if (objRef != MJIEnv.NULL){
1042       ElementInfo ei = env.getElementInfo(objRef);
1043       if (ei != null) {
1044         if (ei.getClassInfo() == ClassLoaderInfo.getCurrentSystemClassLoader().getClassClassInfo()) {
1045           // it's a class object, freeze sharedness of static fields
1046           ei = env.getStaticElementInfo(objRef);
1047         }
1048
1049         if (ei.isSharednessFrozen() != freeze) {
1050           ei = ei.getModifiableInstance();
1051           ei.freezeSharedness(freeze);
1052         }
1053       }
1054     }
1055   }
1056
1057   @MJI
1058   public static void setProperties___3Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int argRef) {
1059     if (argRef != MJIEnv.NULL) {
1060       Config conf = env.getConfig();
1061
1062       int n = env.getArrayLength(argRef);
1063       for (int i=0; i<n; i++) {
1064         int pRef = env.getReferenceArrayElement(argRef, i);
1065         if (pRef != MJIEnv.NULL) {
1066           String p = env.getStringObject(pRef);
1067           config.parse(p);
1068         }
1069       }
1070     }
1071   }
1072
1073   @MJI
1074   public static int getProperty__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int keyRef) {
1075     if (keyRef != MJIEnv.NULL){
1076       Config conf = env.getConfig();
1077
1078       String key = env.getStringObject(keyRef);
1079       String val = config.getString(key);
1080
1081       if (val != null){
1082         return env.newString(val);
1083       } else {
1084         return MJIEnv.NULL;
1085       }
1086
1087     } else {
1088       return MJIEnv.NULL;
1089     }
1090   }
1091
1092   @MJI
1093   public static void printPathOutput__ZLjava_lang_String_2__V (MJIEnv env, int clsObjRef, boolean cond, int msgRef){
1094     if (cond){
1095       printPathOutput__Ljava_lang_String_2__V(env,clsObjRef,msgRef);
1096     }
1097   }
1098
1099   @MJI
1100   public static void printPathOutput__Ljava_lang_String_2__V (MJIEnv env, int clsObjRef, int msgRef){
1101     VM vm = env.getVM();
1102
1103     System.out.println();
1104     if (msgRef != MJIEnv.NULL){
1105       String msg = env.getStringObject(msgRef);
1106       System.out.println("~~~~~~~~~~~~~~~~~~~~~~~ begin program output at: " + msg);
1107     } else {
1108       System.out.println("~~~~~~~~~~~~~~~~~~~~~~~ begin path output");
1109     }
1110
1111     for (Transition t : vm.getPath()) {
1112       String s = t.getOutput();
1113       if (s != null) {
1114         System.out.print(s);
1115       }
1116     }
1117
1118     // we might be in the middle of a transition that isn't stored yet in the path
1119     String s = vm.getPendingOutput();
1120     if (s != null) {
1121       System.out.print(s);
1122     }
1123
1124     System.out.println("~~~~~~~~~~~~~~~~~~~~~~~ end path output");
1125   }
1126
1127
1128   // the JSON object initialization
1129   @MJI
1130   public static int createFromJSON__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(
1131           MJIEnv env, int clsObjRef, int newObjClsRef, int jsonStringRef) {
1132     ThreadInfo ti = env.getThreadInfo();
1133     SystemState ss = env.getSystemState();
1134
1135     String jsonString = env.getStringObject(jsonStringRef);
1136     JSONLexer lexer = new JSONLexer(jsonString);
1137     JSONParser parser = new JSONParser(lexer);
1138     JSONObject jsonObject = parser.parse();
1139
1140     if (jsonObject != null) {
1141       ClassInfo ci = env.getReferredClassInfo( newObjClsRef);
1142
1143       // check if we need any class init (and hence reexecution) before creating any CGs
1144       if (jsonObject.requiresClinitExecution(ci,ti)){
1145         env.repeatInvocation();
1146         return MJIEnv.NULL;
1147       }
1148
1149       if (!ti.isFirstStepInsn()) {
1150         // Top half - get and register CGs we need to set to fill object from JSON
1151         List<ChoiceGenerator<?>> cgList = CGCall.createCGList(jsonObject);
1152         if (cgList.isEmpty()){
1153           return jsonObject.fillObject(env, ci, null, "");
1154
1155         } else {
1156           for (ChoiceGenerator<?> cg : cgList) {
1157             ss.setNextChoiceGenerator(cg);
1158           }
1159
1160           env.repeatInvocation();
1161           return MJIEnv.NULL;
1162         }
1163
1164       } else {
1165         // Bottom half - fill object with JSON and current values of CGs
1166         ChoiceGenerator<?>[] cgs = ss.getChoiceGenerators();
1167
1168         return jsonObject.fillObject(env, ci, cgs, "");
1169       }
1170
1171     } else {
1172       return MJIEnv.NULL;
1173     }
1174   }
1175
1176   @MJI
1177   public static int readObjectFromFile__Ljava_lang_Class_2Ljava_lang_String_2__Ljava_lang_Object_2(
1178           MJIEnv env, int clsObjRef, int newObjClsRef, int fileNameRef) {
1179     int typeNameRef = env.getReferenceField(newObjClsRef, "name");
1180     String typeName = env.getStringObject(typeNameRef);
1181     String fileName = env.getStringObject(fileNameRef);
1182
1183     try {
1184
1185       FileInputStream fis = new FileInputStream(fileName);
1186       ObjectInputStream ois = new ObjectInputStream(fis);
1187       Object javaObject = ois.readObject();
1188       String readObjectTypeName = javaObject.getClass().getCanonicalName();
1189
1190       int readObjRef = ObjectConverter.JPFObjectFromJavaObject(env, javaObject);
1191
1192       return readObjRef;
1193
1194     } catch (ClinitRequired clix){
1195       env.repeatInvocation();
1196       return MJIEnv.NULL;
1197
1198     } catch (IOException iox){
1199       throw new JPFException("failure reading object from file: " + fileName, iox);
1200     } catch (ClassNotFoundException cnfx){
1201       throw new JPFException("failure reading object from file: " + fileName, cnfx);
1202     }
1203   }
1204
1205   //--- those need to be kept in sync with the model side
1206   public static final int SEVERE = 1;
1207   public static final int WARNING = 2;
1208   public static final int INFO = 3;
1209   public static final int FINE = 4;
1210   public static final int FINER = 5;
1211   public static final int FINEST = 6;
1212
1213
1214   private static void log (JPFLogger logger, int logLevel, String msg){
1215     switch (logLevel){
1216     case SEVERE:
1217       logger.severe( msg);
1218       break;
1219     case WARNING:
1220       logger.warning( msg);
1221       break;
1222     case INFO:
1223       logger.info( msg);
1224       break;
1225     case FINE:
1226       logger.fine( msg);
1227       break;
1228     case FINER:
1229       logger.finer( msg);
1230       break;
1231     case FINEST:
1232       logger.finest( msg);
1233       break;
1234     default:
1235       throw new JPFException("unknown log level " + logLevel + " for logger " + logger.getName());
1236     }
1237   }
1238
1239   @MJI
1240   public static void log__Ljava_lang_String_2ILjava_lang_String_2__V (MJIEnv env, int clsObjRef,
1241       int loggerIdRef, int logLevel, int msgRef){
1242     String loggerId = env.getStringObject(loggerIdRef);
1243     String msg = env.getStringObject(msgRef);
1244     JPFLogger logger = JPF.getLogger(loggerId);
1245
1246     log( logger, logLevel, msg);
1247   }
1248
1249   @MJI
1250   public static void log__Ljava_lang_String_2ILjava_lang_String_2Ljava_lang_String_2__V (MJIEnv env, int clsObjRef,
1251       int loggerIdRef, int logLevel, int arg1Ref, int arg2Ref){
1252     String loggerId = env.getStringObject(loggerIdRef);
1253     String msg = env.getStringObject(arg1Ref) + env.getStringObject(arg2Ref);
1254     JPFLogger logger = JPF.getLogger(loggerId);
1255
1256     log( logger, logLevel, msg);
1257   }
1258
1259   @MJI
1260   public static void log__Ljava_lang_String_2ILjava_lang_String_2_3Ljava_lang_Object_2__V (MJIEnv env, int clsObjRef,
1261       int loggerIdRef, int logLevel, int fmtRef, int argsRef){
1262     String loggerId = env.getStringObject(loggerIdRef);
1263     String fmt = env.getStringObject(fmtRef);
1264     JPFLogger logger = JPF.getLogger(loggerId);
1265
1266     int[] argRefs = env.getReferenceArrayObject( argsRef);
1267     Object[] args = new Object[argRefs.length];
1268     for (int i=0; i<args.length; i++){
1269       ElementInfo eiArg = env.getElementInfo(argRefs[i]);
1270       if (eiArg.isStringObject()){
1271         args[i] = env.getStringObject(argRefs[i]);
1272       } else if (eiArg.isBoxObject()){
1273         args[i] = eiArg.asBoxObject();
1274       } else {
1275         args[i] = eiArg.toString();
1276       }
1277     }
1278
1279     String msg = String.format(fmt, args);
1280
1281     log( logger, logLevel, msg);
1282   }
1283 }