src/peers/gov/nasa/jpf/vm/JPF_java_text_DecimalFormat.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
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.annotation.MJI;
  22 import gov.nasa.jpf.vm.MJIEnv;
  23 import gov.nasa.jpf.vm.NativePeer;
  24
  25 import java.text.DecimalFormat;
  26 import java.text.Format;
  27 import java.text.NumberFormat;
  28 import java.text.ParsePosition;
  29
  30 // NOTE - this only works because DecimalFormat is a Format subclass, i.e.
  31 // the java.text.Format native peer will be initialized first
  32 // (otherwise we shouldn't depend on static data of other native peers)
  33
  34 public class JPF_java_text_DecimalFormat extends NativePeer {
  35
  36   static final int INTEGER_STYLE=0;
  37   static final int NUMBER_STYLE=1;
  38
  39   NumberFormat getInstance (MJIEnv env, int objref) {
  40     Format fmt = JPF_java_text_Format.getInstance(env,objref);
  41     assert fmt instanceof NumberFormat;
  42
  43     return (NumberFormat)fmt;
  44   }
  45
  46   /*
  47    * NOTE: if we would directly intercept the ctors, we would have to
  48    * explicitly call the superclass ctors here (the 'id' handle gets
  49    * initialized in the java.text.Format ctor)
  50    */
  51   @MJI
  52   public void init0____V (MJIEnv env, int objref) {
  53     DecimalFormat fmt = new DecimalFormat();
  54     JPF_java_text_Format.putInstance(env,objref,fmt);
  55   }
  56
  57   @MJI
  58   public void init0__Ljava_lang_String_2__V (MJIEnv env, int objref, int patternref) {
  59     String pattern = env.getStringObject(patternref);
  60
  61     DecimalFormat fmt = new DecimalFormat(pattern);
  62     JPF_java_text_Format.putInstance(env,objref,fmt);
  63   }
  64
  65   @MJI
  66   public void init0__I__V (MJIEnv env, int objref, int style) {
  67     NumberFormat fmt = null;
  68     if (style == INTEGER_STYLE) {
  69       fmt = NumberFormat.getIntegerInstance();
  70     } else if (style == NUMBER_STYLE) {
  71       fmt = NumberFormat.getNumberInstance();
  72     } else {
  73       // unknown style
  74       fmt = new DecimalFormat();
  75     }
  76
  77     JPF_java_text_Format.putInstance(env,objref,fmt);
  78   }
  79
  80   @MJI
  81   public void setMaximumFractionDigits__I__V (MJIEnv env, int objref, int newValue){
  82     NumberFormat fmt = getInstance(env,objref);
  83     if (fmt != null) {
  84       fmt.setMaximumFractionDigits(newValue);
  85     }
  86   }
  87
  88   @MJI
  89   public void setMaximumIntegerDigits__I__V (MJIEnv env, int objref, int newValue){
  90     NumberFormat fmt = getInstance(env,objref);
  91     if (fmt != null) {
  92       fmt.setMaximumIntegerDigits(newValue);
  93     }
  94   }
  95
  96   @MJI
  97   public void setMinimumFractionDigits__I__V (MJIEnv env, int objref, int newValue){
  98     NumberFormat fmt = getInstance(env,objref);
  99     if (fmt != null) {
 100       fmt.setMinimumFractionDigits(newValue);
 101     }
 102   }
 103
 104   @MJI
 105   public void setMinimumIntegerDigits__I__V (MJIEnv env, int objref, int newValue){
 106     NumberFormat fmt = getInstance(env,objref);
 107     if (fmt != null) {
 108       fmt.setMinimumIntegerDigits(newValue);
 109     }
 110   }
 111
 112   @MJI
 113   public int format__J__Ljava_lang_String_2 (MJIEnv env, int objref, long number) {
 114     NumberFormat fmt = getInstance(env,objref);
 115     if (fmt != null) {
 116       String s = fmt.format(number);
 117       int sref = env.newString(s);
 118       return sref;
 119     }
 120
 121     return MJIEnv.NULL;
 122   }
 123
 124   @MJI
 125   public int format__D__Ljava_lang_String_2 (MJIEnv env, int objref, double number) {
 126     NumberFormat fmt = getInstance(env,objref);
 127     if (fmt != null) {
 128       String s = fmt.format(number);
 129       int sref = env.newString(s);
 130       return sref;
 131     }
 132
 133     return MJIEnv.NULL;
 134   }
 135
 136   @MJI
 137   public void setParseIntegerOnly__Z__V(MJIEnv env, int objref, boolean value) {
 138     NumberFormat fmt = getInstance(env,objref);
 139     if (fmt != null) {
 140       fmt.setParseIntegerOnly(value);
 141     }
 142   }
 143
 144   @MJI
 145   public boolean isParseIntegerOnly____Z(MJIEnv env, int objref) {
 146     NumberFormat fmt = getInstance(env,objref);
 147     if (fmt != null) {
 148       return fmt.isParseIntegerOnly();
 149     }
 150     return false;
 151   }
 152
 153   @MJI
 154   public void setGroupingUsed__Z__V(MJIEnv env, int objref, boolean newValue) {
 155     NumberFormat fmt = getInstance(env,objref);
 156     if (fmt != null) {
 157       fmt.setGroupingUsed(newValue);
 158     }
 159   }
 160
 161   @MJI
 162   public boolean isGroupingUsed____Z(MJIEnv env, int objref) {
 163     NumberFormat fmt = getInstance(env,objref);
 164     if (fmt != null) {
 165       return fmt.isGroupingUsed();
 166     }
 167     return false;
 168   }
 169
 170   @MJI
 171   public int parse__Ljava_lang_String_2Ljava_text_ParsePosition_2__Ljava_lang_Number_2(MJIEnv env, int objref,int sourceRef,int parsePositionRef) {
 172     String source = env.getStringObject(sourceRef);
 173     ParsePosition parsePosition = createParsePositionFromRef(env,parsePositionRef);
 174     NumberFormat fmt = getInstance(env,objref);
 175     Number number = null;
 176     if (fmt != null) {
 177       number = fmt.parse(source,parsePosition);
 178     }
 179     updateParsePositionRef(env,parsePositionRef, parsePosition);
 180     return createNumberRefFromNumber(env,number);
 181   }
 182
 183   private static ParsePosition createParsePositionFromRef(MJIEnv env,int parsePositionRef) {
 184     int index = env.getIntField(parsePositionRef, "index");
 185     int errorIndex = env.getIntField(parsePositionRef, "errorIndex");
 186     ParsePosition ps = new ParsePosition(index);
 187     ps.setErrorIndex(errorIndex);
 188     return ps;
 189   }
 190
 191   private static void updateParsePositionRef(MJIEnv env,int parsePositionRef, ParsePosition parsePosition) {
 192     env.setIntField(parsePositionRef, "index", parsePosition.getIndex());
 193     env.setIntField(parsePositionRef, "errorIndex", parsePosition.getErrorIndex());
 194   }
 195
 196   private static int createNumberRefFromNumber(MJIEnv env,Number number) {
 197     int numberRef = MJIEnv.NULL;
 198     if(number instanceof Double) {
 199       numberRef = env.newObject("java.lang.Double");
 200       env.setDoubleField(numberRef, "value", number.doubleValue());
 201     } else if(number instanceof Long) {
 202       numberRef = env.newObject("java.lang.Long");
 203       env.setLongField(numberRef, "value", number.longValue());
 204     }
 205     return numberRef;
 206   }
 207
 208 }