4a7b4425d57cee80ad131ed7f63f6507401a9d17
[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     if (!isDone && (count < values.length-1))  
114       return true;
115     else
116       return false;
117   }
118
119   /**
120    * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
121    **/
122   @Override
123   public void advance() {
124     if (count < values.length-1) count++;
125   }
126
127   /**
128    * get String label of current value, as specified in config file
129    **/
130   public String getValueLabel(){
131     return values[count].toString();
132   }
133
134   @Override
135   public int getTotalNumberOfChoices () {
136     return values.length;
137   }
138
139   @Override
140   public int getProcessedNumberOfChoices () {
141     return count+1;
142   }
143   
144   @Override
145   public boolean supportsReordering(){
146     return true;
147   }
148   
149   
150   protected T parse (String varSpec, StackFrame resolveFrame){
151     int sign = 1;
152
153     char c = varSpec.charAt(0);
154     if (c == '+'){
155       varSpec = varSpec.substring(1);
156     } else if (c == '-'){
157       sign = -1;
158       varSpec = varSpec.substring(1);
159     }
160
161     if (varSpec.isEmpty()){
162       throw new JPFException("illegal value spec for IntChoiceFromList " + id);
163     }
164
165     c = varSpec.charAt(0);
166     if (Character.isDigit(c)){ // its an integer literal
167       return parseLiteral(varSpec, sign);
168
169     } else { // a variable or field name
170       Object o = resolveFrame.getLocalOrFieldValue(varSpec);
171       if (o == null){
172         throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
173       }
174       if (o instanceof Number){
175         return newValue( (Number)o, sign);
176       } else {
177         throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
178       }
179     }
180   }
181
182   
183   @Override
184   public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
185     
186     T[] newValues = values.clone();
187     Arrays.sort( newValues, comparator);
188     
189     // we can't instantiate directly
190     try {
191     NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
192     clone.values = newValues;
193     clone.count = -1;
194     return clone;
195     
196     } catch (CloneNotSupportedException cnsx){
197       // can't happen
198       throw new JPFException("can't clone NumberChoiceFromList " + this);
199     }
200   }
201   
202   @Override
203   public String toString() {
204     StringBuilder sb = new StringBuilder(getClass().getName());
205     sb.append("[id=\"");
206     sb.append(id);
207     sb.append('"');
208
209     sb.append(",isCascaded:");
210     sb.append(isCascaded);
211
212     sb.append(",");
213     for (int i=0; i<values.length; i++) {
214       if (i > 0) {
215         sb.append(',');
216       }
217       if (i == count) {
218         sb.append(MARKER);
219       }
220       sb.append(values[i]);
221     }
222     sb.append(']');
223     return sb.toString();
224   }
225   
226   
227   @Override
228   public NumberChoiceFromList<T> randomize () {
229     for (int i = values.length - 1; i > 0; i--) {
230       int j = random.nextInt(i + 1);
231       T tmp = values[i];
232       values[i] = values[j];
233       values[j] = tmp;
234     }
235     return this;
236   }
237
238   // TODO: Fix for Groovy's model-checking
239   // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
240   public void setNewValues(T[] vals) {
241     values = vals;
242   }
243
244   public int getNextChoiceIndex() {
245     return count;
246   }
247
248   public void setChoice(int idx, T value) {
249     if ((idx >= 0) && (idx < values.length)) {
250       values[idx] = value;
251     } else {
252       throw new JPFException("illegal value " + idx + " for array index");
253     }
254   }
255 }