Commenting out a line that causes a lot of loops; let the exclusion trace continue...
[jpf-core.git] / src / main / gov / nasa / jpf / vm / choice / NumberChoiceFromList.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.choice;
19
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPFException;
22 import gov.nasa.jpf.vm.ChoiceGeneratorBase;
23 import gov.nasa.jpf.vm.StackFrame;
24 import gov.nasa.jpf.vm.ThreadInfo;
25
26 import java.util.Arrays;
27 import java.util.Comparator;
28
29 /** 
30  * common root for list based number choice generators
31  */
32 public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGeneratorBase<T> {
33
34   // int values to choose from stored as Strings or Integers
35   protected T[] values;
36   protected int count = -1;
37   
38   /**
39    *  super constructor for subclasses that want to configure themselves
40    * @param id name used in choice config
41    */
42   protected NumberChoiceFromList(String id){
43     super(id);
44   }
45
46   protected NumberChoiceFromList (String id, T[] vals){
47     super(id);
48     values = vals;
49     count = -1;
50   }
51   
52   protected abstract T[] createValueArray(int len);
53   protected abstract T getDefaultValue();
54   protected abstract T parseLiteral (String literal, int sign);
55   protected abstract T newValue (Number num, int sign);
56   
57   /**
58    * @param conf JPF configuration object
59    * @param id name used in choice config
60    */
61   public NumberChoiceFromList(Config conf, String id) {
62     super(id);
63
64     String[] vals = conf.getCompactStringArray(id + ".values");
65     if (vals == null || vals.length == 0) {
66       throw new JPFException("no value specs for IntChoiceFromList " + id);
67     }
68
69     // get the choice values here because otherwise successive getNextChoice()
70     // calls within the same transition could see different values when looking
71     // up fields and locals
72     values = createValueArray(vals.length);
73     StackFrame resolveFrame = ThreadInfo.getCurrentThread().getLastNonSyntheticStackFrame();
74     for (int i=0; i<vals.length; i++){
75       values[i] = parse(vals[i], resolveFrame);
76     }
77   }
78   
79   @Override
80   public T getChoice (int idx){
81     if (idx >=0 && idx < values.length){
82       return values[idx];
83     } else {
84       throw new IllegalArgumentException("choice index out of range: " + idx);
85     }
86   }
87
88   @Override
89   public void reset () {
90     count = -1;
91
92     isDone = false;
93   }
94       
95   /** 
96    * @see gov.nasa.jpf.vm.IntChoiceGenerator#getNextChoice()
97    **/
98   @Override
99   public T getNextChoice() {
100
101     if ((count >= 0) && (count < values.length)) {
102       return values[count];
103     }
104
105     return getDefaultValue();
106   }
107
108   /**
109    * @see gov.nasa.jpf.vm.ChoiceGenerator#hasMoreChoices()
110    **/
111   @Override
112   public boolean hasMoreChoices() {
113     // TODO: Fix for Groovy's model-checking
114     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
115     if (!isDone)
116       return true;
117     else
118       return false;
119
120     /* TODO: ORIGINAL CODE
121     if (!isDone && (count < values.length-1))
122       return true;
123     else
124       return false;*/
125   }
126
127   /**
128    * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
129    **/
130   @Override
131   public void advance() {
132     // TODO: Fix for Groovy's model-checking
133     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
134
135     // TODO: We make this circular
136     if (count < values.length-1) count++;
137     else count = 0;
138
139     /* TODO: ORIGINAL CODE
140     if (count < values.length-1) count++;*/
141   }
142
143   /**
144    * get String label of current value, as specified in config file
145    **/
146   public String getValueLabel(){
147     return values[count].toString();
148   }
149
150   @Override
151   public int getTotalNumberOfChoices () {
152     return values.length;
153   }
154
155   @Override
156   public int getProcessedNumberOfChoices () {
157     return count+1;
158   }
159   
160   @Override
161   public boolean supportsReordering(){
162     return true;
163   }
164   
165   
166   protected T parse (String varSpec, StackFrame resolveFrame){
167     int sign = 1;
168
169     char c = varSpec.charAt(0);
170     if (c == '+'){
171       varSpec = varSpec.substring(1);
172     } else if (c == '-'){
173       sign = -1;
174       varSpec = varSpec.substring(1);
175     }
176
177     if (varSpec.isEmpty()){
178       throw new JPFException("illegal value spec for IntChoiceFromList " + id);
179     }
180
181     c = varSpec.charAt(0);
182     if (Character.isDigit(c)){ // its an integer literal
183       return parseLiteral(varSpec, sign);
184
185     } else { // a variable or field name
186       Object o = resolveFrame.getLocalOrFieldValue(varSpec);
187       if (o == null){
188         throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
189       }
190       if (o instanceof Number){
191         return newValue( (Number)o, sign);
192       } else {
193         throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
194       }
195     }
196   }
197
198   
199   @Override
200   public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
201     
202     T[] newValues = values.clone();
203     Arrays.sort( newValues, comparator);
204     
205     // we can't instantiate directly
206     try {
207     NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
208     clone.values = newValues;
209     clone.count = -1;
210     return clone;
211     
212     } catch (CloneNotSupportedException cnsx){
213       // can't happen
214       throw new JPFException("can't clone NumberChoiceFromList " + this);
215     }
216   }
217   
218   @Override
219   public String toString() {
220     StringBuilder sb = new StringBuilder(getClass().getName());
221     sb.append("[id=\"");
222     sb.append(id);
223     sb.append('"');
224
225     sb.append(",isCascaded:");
226     sb.append(isCascaded);
227
228     sb.append(",");
229     for (int i=0; i<values.length; i++) {
230       if (i > 0) {
231         sb.append(',');
232       }
233       if (i == count) {
234         sb.append(MARKER);
235       }
236       sb.append(values[i]);
237     }
238     sb.append(']');
239     return sb.toString();
240   }
241   
242   
243   @Override
244   public NumberChoiceFromList<T> randomize () {
245     for (int i = values.length - 1; i > 0; i--) {
246       int j = random.nextInt(i + 1);
247       T tmp = values[i];
248       values[i] = values[j];
249       values[j] = tmp;
250     }
251     return this;
252   }
253
254   // TODO: Fix for Groovy's model-checking
255   // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
256   public void setNewValues(T[] vals) {
257     values = vals;
258   }
259
260   public int getNextChoiceIndex() {
261     return count;
262   }
263
264   public void setChoice(int idx, T value) {
265     if ((idx >= 0) && (idx < values.length)) {
266       values[idx] = value;
267     } else {
268       throw new JPFException("illegal value " + idx + " for array index");
269     }
270   }
271 }