001package daikon.test;
002
003import static java.nio.charset.StandardCharsets.UTF_8;
004import static java.util.logging.Level.INFO;
005import static org.junit.Assert.assertEquals;
006import static org.junit.Assert.assertTrue;
007
008import daikon.*;
009import java.io.BufferedReader;
010import java.io.IOException;
011import java.io.InputStream;
012import java.io.InputStreamReader;
013import java.io.PrintStream;
014import java.util.ArrayDeque;
015import java.util.ArrayList;
016import java.util.Deque;
017import java.util.HashMap;
018import java.util.List;
019import java.util.Map;
020import java.util.StringTokenizer;
021
022/**
023 * This is called by VarInfoName to parse varInfoNameTest<em>foo</em> files and then apply various
024 * transformation tests on them. To add your own test, follow directions in VarInfoNameTest.
025 */
026@SuppressWarnings("nullness") // testing code
027public class VarInfoNameDriver {
028
029  /**
030   * Convenience entry point for TraceSelect
031   *
032   * @param args command-line arguments
033   */
034  public static void main(String[] args) {
035    daikon.LogHelper.setupLogs(INFO);
036    run(System.in, System.out);
037  }
038
039  private static final Map<String, Handler> handlers = new HashMap<>();
040
041  public static void run(InputStream commands, PrintStream output) {
042    try {
043      run_helper(commands, output);
044    } catch (IOException e) {
045      throw new RuntimeException(e.toString());
046    }
047  }
048
049  private static void run_helper(InputStream _commands, PrintStream output) throws IOException {
050    BufferedReader commands = new BufferedReader(new InputStreamReader(_commands, UTF_8));
051    Map<String, VarInfoName> variables = new HashMap<>();
052
053    String command;
054    while ((command = commands.readLine()) != null) {
055      if (command.startsWith(";")) {
056        output.println(command);
057        continue;
058      }
059
060      // tokenize arguments
061      StringTokenizer tok = new StringTokenizer(command);
062      Deque<String> list = new ArrayDeque<String>();
063      while (tok.hasMoreTokens()) {
064        list.add(tok.nextToken());
065      }
066
067      // ignore blank lines
068      if (list.size() == 0) {
069        continue;
070      }
071
072      output.println("; " + command);
073
074      // call the handler
075      String method = list.removeFirst();
076      String[] args = list.toArray(new String[0]);
077      Handler handler = handlers.get(method);
078      if (handler == null) {
079        throw new UnsupportedOperationException("Unknown method: " + method);
080      }
081      handler.handle(variables, args, output);
082    }
083  }
084
085  public static interface Handler {
086    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out);
087  }
088
089  // VarInfoName parse(String);
090  private static class Parse implements Handler {
091    @Override
092    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
093      assertEquals(2, args.length);
094      String var = args[0];
095      String expr = args[1];
096      VarInfoName parse = VarInfoName.parse(expr);
097      vars.put(var, parse);
098      out.println(var + " = " + parse.name());
099    }
100  }
101
102  static {
103    handlers.put("parse", new Parse());
104  }
105
106  // String name();
107  private static class Name implements Handler {
108    @Override
109    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
110      assertEquals(1, args.length);
111      VarInfoName var = vars.get(args[0]);
112      out.println(var.name());
113    }
114  }
115
116  static {
117    handlers.put("name", new Name());
118  }
119
120  // String esc_name();
121  private static class EscName implements Handler {
122    @Override
123    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
124      assertEquals(1, args.length);
125      VarInfoName var = vars.get(args[0]);
126      out.println(var.esc_name());
127    }
128  }
129
130  static {
131    handlers.put("esc_name", new EscName());
132  }
133
134  // String simplify_name();
135  private static class SimplifyName implements Handler {
136    @Override
137    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
138      assertEquals(1, args.length);
139      VarInfoName var = vars.get(args[0]);
140      out.println(var.simplify_name());
141    }
142  }
143
144  static {
145    handlers.put("simplify_name", new SimplifyName());
146  }
147
148  // String[] QuantHelper.format_esc(VarInfoName[] roots)
149  private static class QuantifyEscName implements Handler {
150    @Override
151    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
152      VarInfoName[] roots = new VarInfoName[args.length];
153      for (int i = 0; i < args.length; i++) {
154        roots[i] = vars.get(args[i]);
155      }
156      String[] result = VarInfoName.QuantHelper.format_esc(roots);
157      String result2 = VarInfoName.QuantHelper.format_esc(roots, true)[0];
158      for (int i = 0; i < result.length; i++) {
159        if (i != 0 && i != result.length - 1) {
160          out.print('\t');
161        }
162        out.println(result[i]);
163        if (i == 0 && roots.length > 1) {
164          out.println(result2);
165        }
166      }
167    }
168  }
169
170  static {
171    handlers.put("quantify_esc_name", new QuantifyEscName());
172  }
173
174  // String[] QuantHelper.format_simplify(VarInfoName[] roots)
175  private static class QuantifySimplifyName implements Handler {
176    @Override
177    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
178      VarInfoName[] roots = new VarInfoName[args.length];
179      for (int i = 0; i < args.length; i++) {
180        roots[i] = vars.get(args[i]);
181      }
182      String[] result = VarInfoName.QuantHelper.format_simplify(roots);
183      for (int i = 0; i < result.length; i++) {
184        if (i != 0 && i != result.length - 1) {
185          out.print('\t');
186        }
187        out.println(result[i]);
188      }
189    }
190  }
191
192  static {
193    handlers.put("quantify_simplify_name", new QuantifySimplifyName());
194  }
195
196  // VarInfoName intern();
197  // TODO
198
199  // boolean isLiteralConstant();
200  // TODO
201
202  // boolean equals(Object);
203  // boolean equals(VarInfoName);
204  private static class Equals implements Handler {
205    @Override
206    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
207      assertEquals(2, args.length);
208      VarInfoName a = vars.get(args[0]);
209      VarInfoName b = vars.get(args[1]);
210      out.println(args[0] + " " + (a.equals(b) ? "=" : "!") + "= " + args[1]);
211    }
212  }
213
214  static {
215    handlers.put("equals", new Equals());
216  }
217
218  // int hashCode(@GuardSatisfied VarInfoNameDriver this);
219  private static class HashCode implements Handler {
220    @Override
221    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
222      assertEquals(2, args.length);
223      VarInfoName a = vars.get(args[0]);
224      VarInfoName b = vars.get(args[1]);
225      out.println(
226          args[0]
227              + ".hash "
228              + ((a.hashCode() == b.hashCode()) ? "=" : "!")
229              + "= "
230              + args[1]
231              + ".hash");
232    }
233  }
234
235  static {
236    handlers.put("hash", new HashCode());
237  }
238
239  // String toString(@GuardSatisfied VarInfoNameDriver this);
240
241  // VarInfoName applySize();
242  private static class Size implements Handler {
243    @Override
244    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
245      assertEquals(2, args.length);
246      VarInfoName var = vars.get(args[1]);
247      VarInfoName result = var.applySize();
248      vars.put(args[0], result);
249      out.println(args[0] + " = " + result.name());
250    }
251  }
252
253  static {
254    handlers.put("size", new Size());
255  }
256
257  // VarInfoName applyFunction(String);
258  private static class Function implements Handler {
259    @Override
260    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
261      assertEquals(3, args.length);
262      String func = args[1];
263      VarInfoName var = vars.get(args[2]);
264      VarInfoName result = var.applyFunction(func);
265      vars.put(args[0], result);
266      out.println(args[0] + " = " + result.name());
267    }
268  }
269
270  static {
271    handlers.put("function", new Function());
272  }
273
274  // VarInfoName applyTypeOf();
275  private static class TypeOf implements Handler {
276    @Override
277    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
278      assertEquals(2, args.length);
279      VarInfoName var = vars.get(args[1]);
280      VarInfoName result = var.applyTypeOf();
281      vars.put(args[0], result);
282      out.println(args[0] + " = " + result.name());
283    }
284  }
285
286  static {
287    handlers.put("typeof", new TypeOf());
288  }
289
290  // VarInfoName applyPrestate();
291  private static class Prestate implements Handler {
292    @Override
293    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
294      assertEquals(2, args.length);
295      VarInfoName var = vars.get(args[1]);
296      VarInfoName result = var.applyPrestate();
297      vars.put(args[0], result);
298      out.println(args[0] + " = " + result.name());
299    }
300  }
301
302  static {
303    handlers.put("prestate", new Prestate());
304  }
305
306  // VarInfoName applyPoststate();
307  private static class Poststate implements Handler {
308    @Override
309    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
310      assertEquals(2, args.length);
311      VarInfoName var = vars.get(args[1]);
312      VarInfoName result = var.applyPoststate();
313      vars.put(args[0], result);
314      out.println(args[0] + " = " + result.name());
315    }
316  }
317
318  static {
319    handlers.put("poststate", new Poststate());
320  }
321
322  // VarInfoName.PostPreConverter visitor test
323  private static class PostPreConverter implements Handler {
324    private static VarInfoName.PostPreConverter converter = new VarInfoName.PostPreConverter();
325
326    @Override
327    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
328      VarInfoName var = vars.get(args[0]);
329      VarInfoName result = converter.replace(var);
330      vars.put(args[0], result);
331      out.println(args[0] + " = " + result.name());
332    }
333  }
334
335  static {
336    handlers.put("postPreConverter", new PostPreConverter());
337  }
338
339  // VarInfoName applyAdd(int);
340  private static class Add implements Handler {
341    @Override
342    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
343      assertEquals(3, args.length);
344      VarInfoName var = vars.get(args[1]);
345      int amt = Integer.parseInt(args[2]);
346      VarInfoName result = var.applyAdd(amt);
347      vars.put(args[0], result);
348      out.println(args[0] + " = " + result.name());
349    }
350  }
351
352  static {
353    handlers.put("add", new Add());
354  }
355
356  // VarInfoName applyElements();
357  private static class Elements implements Handler {
358    @Override
359    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
360      assertEquals(2, args.length);
361      VarInfoName var = vars.get(args[1]);
362      VarInfoName result = var.applyElements();
363      vars.put(args[0], result);
364      out.println(args[0] + " = " + result.name());
365    }
366  }
367
368  static {
369    handlers.put("elements", new Elements());
370  }
371
372  // VarInfoName applySubscript(VarInfoName);
373  private static class Subscript implements Handler {
374    @Override
375    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
376      assertEquals(3, args.length);
377      VarInfoName var = vars.get(args[1]);
378      VarInfoName sub = vars.get(args[2]);
379      VarInfoName result = var.applySubscript(sub);
380      vars.put(args[0], result);
381      out.println(args[0] + " = " + result.name());
382    }
383  }
384
385  static {
386    handlers.put("subscript", new Subscript());
387  }
388
389  // VarInfoName applySlice(VarInfoName, VarInfoName);
390  private static class Slice implements Handler {
391    @Override
392    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
393      assertEquals(4, args.length);
394      VarInfoName var = vars.get(args[1]);
395      VarInfoName i = vars.get(args[2]);
396      VarInfoName j = vars.get(args[3]);
397      VarInfoName result = var.applySlice(i, j);
398      vars.put(args[0], result);
399      out.println(args[0] + " = " + result.name());
400    }
401  }
402
403  static {
404    handlers.put("slice", new Slice());
405  }
406
407  // String jml_name()
408  private static class JMLName implements Handler {
409    @Override
410    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
411      assertEquals(1, args.length);
412      VarInfoName var = vars.get(args[0]);
413      VarInfoName.testCall = true;
414      out.println(args[0] + ".jml_name() = " + var.jml_name(null));
415      VarInfoName.testCall = false;
416    }
417  }
418
419  static {
420    handlers.put("jml_name", new JMLName());
421  }
422
423  // VarInfoName applyFunctionOfN(String function, List vars)
424  private static class FunctionOfN implements Handler {
425    @Override
426    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
427      assertTrue(args.length >= 4);
428      String func = args[1];
429      List<VarInfoName> function_vars = new ArrayList<>();
430      for (int x = 2; x < args.length; x++) {
431        function_vars.add(vars.get(args[x]));
432      }
433      VarInfoName result = VarInfoName.applyFunctionOfN(func, function_vars);
434      vars.put(args[0], result);
435      out.println(args[0] + " = " + result.name());
436    }
437  }
438
439  static {
440    handlers.put("function_of_N", new FunctionOfN());
441  }
442
443  // public VarInfoName applyField(String field)
444  private static class Field implements Handler {
445    @Override
446    public void handle(Map<String, VarInfoName> vars, String[] args, PrintStream out) {
447      assertEquals(3, args.length);
448      VarInfoName var = vars.get(args[1]);
449      String fieldname = args[2];
450      VarInfoName result = var.applyField(fieldname);
451      vars.put(args[0], result);
452      out.println(args[0] + " = " + result.name());
453    }
454  }
455
456  static {
457    handlers.put("field", new Field());
458  }
459
460  // public String[] QuantHelper.format_jml(VarInfoName[] roots)
461  //   private static class QuantifyFormatJML implements Handler {
462  //     public void handle(Map<String,VarInfoName> vars, String[] args, PrintStream out) {
463  //       assertTrue (args.length >= 1);
464  //       VarInfoName roots[] = new VarInfoName [args.length];
465  //       for (int x = 0; x<args.length; x++)
466  //         roots[x] = vars.get(args[x]);
467  //       String result[] = VarInfoName.QuantHelper.format_jml(roots);
468  //       for (int x = 0; x<result.length; x++)
469  //         out.println(result[x]);
470  //     }
471  //   }
472  //   static { handlers.put("quantify_format_jml", new QuantifyFormatJML()); }
473
474  //   // public String[] QuantHelper.format_jml(VarInfoName[] roots, boolean elementwise)
475  //   private static class QuantifyFormatJMLElementwise implements Handler {
476  //     public void handle(Map<String,VarInfoName> vars, String[] args, PrintStream out) {
477  //       assertTrue (args.length >= 1);
478  //       VarInfoName roots[] = new VarInfoName [args.length];
479  //       for (int x = 0; x<args.length; x++)
480  //         roots[x] = vars.get(args[x]);
481  //       String result[] = VarInfoName.QuantHelper.format_jml(roots, true);
482  //       for (int x = 0; x<result.length; x++)
483  //         out.println(result[x]);
484  //     }
485  //   }
486  //   static { handlers.put("quantify_format_jml_elem", new QuantifyFormatJMLElementwise()); }
487
488  //   // public String[] QuantHelper.format_jml(VarInfoName[] roots, boolean elementwise,boolean
489  // forall)
490  //   private static class QuantifyFormatJMLExists implements Handler {
491  //     public void handle(Map<String,VarInfoName> vars, String[] args, PrintStream out) {
492  //       assertTrue(args.length >= 1);
493  //       VarInfoName roots[] = new VarInfoName [args.length];
494  //       for (int x = 0; x<args.length; x++)
495  //         roots[x] = vars.get(args[x]);
496  //       String result[] = VarInfoName.QuantHelper.format_jml(roots, false, false);
497  //       for (int x = 0; x<result.length; x++)
498  //         out.println(result[x]);
499  //     }
500  //   }
501  //   static { handlers.put("quantify_format_jml_exists", new QuantifyFormatJMLExists()); }
502}