Source code

001package daikon.tools.runtimechecker;
002
003import daikon.PptMap;
004import daikon.PptTopLevel;
005import daikon.inv.Invariant;
006import daikon.inv.OutputFormat;
007import daikon.inv.ternary.threeScalar.FunctionBinary;
008import daikon.tools.jtb.Ast;
009import daikon.tools.jtb.PptNameMatcher;
010import java.io.StringWriter;
011import java.lang.reflect.Constructor;
012import java.lang.reflect.Method;
013import java.util.ArrayList;
014import java.util.HashMap;
015import java.util.HashSet;
016import java.util.List;
017import java.util.Map;
018import java.util.Set;
019import java.util.StringJoiner;
020import java.util.Vector;
021import jtb.syntaxtree.*;
022import jtb.visitor.DepthFirstVisitor;
023import jtb.visitor.TreeDumper;
024import jtb.visitor.TreeFormatter;
025import org.checkerframework.checker.nullness.qual.KeyFor;
026import org.checkerframework.checker.nullness.qual.NonNull;
027import org.plumelib.util.StringsPlume;
028
029/**
030 * Visitor that instruments a Java source file (i.e. adds code at certain places) to check invariant
031 * violations at run time.
032 */
033@SuppressWarnings("rawtypes")
034public class InstrumentVisitor extends DepthFirstVisitor {
035
036  // If false, all invariants will be output. If true, only
037  // invariants with high confidence will be output.
038  public static boolean outputOnlyHighConfInvariants = false;
039
040  // Properties under this threshold will be considered minor; at or
041  // above threshold will be considered major.
042  // See daikon.tools.runtimechecker.Property.calculateConfidence()
043  public static double confidenceThreshold = 0.5;
044
045  // If true, the instrumenter will make all fields of the class
046  // visible. The reason for doing this is so that invariants over
047  // potentially inaccessible object fields can be evaluated.
048  public static boolean makeAllFieldsPublic = false;
049
050  // The map containing the invariants.
051  private final PptMap pptmap;
052
053  // The AST of the class FooPropertyChecks, where Foo is the class
054  // that we're instrumenting.
055  public CheckerClasses checkerClasses;
056
057  // The methods and constructors that were visited (in other words,
058  // those explicitly declared in the source).
059  public List<Method> visitedMethods = new ArrayList<>();
060  public List<Constructor<?>> visitedConstructors = new ArrayList<>();
061
062  // [[ TODO: I'm using xmlString() because it will definitely give
063  // different values for different Properties. But if Properties
064  // are in fact unique and immutable, and if I ensure that hashcode
065  // returns unique values for unique Properties, then I should be
066  // able to use hashcode. So: make sure that the statements above
067  // are all correct, and then use hashcode. ]]
068  private final Map<String, String> xmlStringToIndex = new HashMap<>();
069
070  private int varNumCounter = 0;
071
072  private final PptNameMatcher pptMatcher;
073
074  /** Create a visitor that will insert code to check the invariants contained in pptmap. */
075  public InstrumentVisitor(PptMap pptmap, TypeDeclaration root) {
076
077    this.checkerClasses = new CheckerClasses();
078
079    this.pptmap = pptmap;
080    this.pptMatcher = new PptNameMatcher(root);
081
082    for (PptTopLevel ppt : pptmap.pptIterable()) {
083
084      if (ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isCombinedExitPoint()) {
085        continue;
086      }
087
088      List<Invariant> invList = filterInvariants(daikon.tools.jtb.Ast.getInvariants(ppt, pptmap));
089      for (Invariant inv : invList) {
090        xmlStringToIndex.put(toProperty(inv).xmlString(), Integer.toString(varNumCounter));
091        varNumCounter++;
092      }
093    }
094  }
095
096  /** If makeAllFieldsPublic == true, then it makes this field declaration public. */
097  @SuppressWarnings("JdkObsolete") // JTB uses Vector
098  @Override
099  public void visit(FieldDeclaration fd) {
100
101    // Fix any line/col inconsistencies first
102    fd.accept(new TreeFormatter());
103
104    super.visit(fd);
105    // Grammar production for ClassOrInterfaceBodyDeclaration:
106    // f0 -> Initializer()
107    //       | Modifiers() ( ClassOrInterfaceDeclaration(modifiers) | EnumDeclaration(modifiers)
108    //                       | ConstructorDeclaration() | FieldDeclaration(modifiers)
109    //                       | MethodDeclaration(modifiers) )
110    //       | ";"
111
112    if (makeAllFieldsPublic) {
113      NodeSequence seq = (NodeSequence) fd.getParent().getParent();
114      Modifiers modifiers = (Modifiers) seq.elementAt(0);
115      List<Node> modifierList = modifiers.f0.nodes;
116
117      List<Node> newModifiers = new ArrayList<>();
118      for (Node modifier : modifierList) {
119        NodeChoice nc = (NodeChoice) modifier;
120        NodeToken token = (NodeToken) nc.choice;
121        if (!token.tokenImage.equals("public")
122            && !token.tokenImage.equals("protected")
123            && !token.tokenImage.equals("private")) {
124          newModifiers.add(token);
125        }
126      }
127
128      newModifiers.add(new NodeToken("public"));
129      modifiers.f0.nodes = new Vector<Node>(newModifiers);
130    }
131  }
132
133  /**
134   * Adds the following new methods:
135   *
136   * <p>checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time time) Checks the
137   * class invariants.
138   *
139   * <p>checkObjectInvariants_instrument(daikon.tools.runtimechecker.Violation.Time time) Check the
140   * object invariants
141   *
142   * <p>isDaikonInstrumented() returns true (you can imagine calling this method to see if the class
143   * has been instrumented).
144   *
145   * <p>getDaikonInvariants() Returns th array of properties being checked.
146   *
147   * <p>Adds the following field:
148   *
149   * <p>daikon.tools.runtimechecker.Property[] daikonProperties The properties being checked.
150   *
151   * <p>Adds code that initializes the properties array.
152   */
153  @Override
154  public void visit(ClassOrInterfaceBody clazz) {
155
156    checkerClasses.addCheckerClass(clazz);
157
158    // Fix any line/col inconsistencies first
159    clazz.accept(new TreeFormatter());
160
161    super.visit(clazz);
162
163    if (Ast.isInterface(clazz)) {
164      return;
165    }
166
167    // add method to check object and class invariants.
168
169    // just skip anonymous classes for now, hard to get a name for them without a decl node...
170    if ((clazz.getParent() instanceof ClassOrInterfaceDeclaration)) {
171      ClassOrInterfaceDeclaration ucd = (ClassOrInterfaceDeclaration) clazz.getParent();
172      String classname = Ast.getClassName(ucd);
173      ClassOrInterfaceBodyDeclaration objInvDecl =
174          checkObjectInvariants_instrumentDeclaration(classname);
175      Ast.addDeclaration(clazz, objInvDecl);
176
177      checkerClasses.addDeclaration(
178          clazz,
179          checkObjectInvariants_instrumentDeclaration_checker(
180              classname, false /* check minor properties */));
181      checkerClasses.addDeclaration(
182          clazz,
183          checkObjectInvariants_instrumentDeclaration_checker(
184              classname, true /* check major properties */));
185
186      if (!Ast.isInner(ucd) || Ast.isStatic(ucd)) {
187        ClassOrInterfaceBodyDeclaration classInvDecl =
188            checkClassInvariantsInstrumentDeclaration(classname);
189        checkerClasses.addDeclaration(
190            clazz,
191            checkClassInvariantsInstrumentDeclaration_checker(
192                classname, false /* check minor properties */));
193        checkerClasses.addDeclaration(
194            clazz,
195            checkClassInvariantsInstrumentDeclaration_checker(
196                classname, true /* check minor properties */));
197        Ast.addDeclaration(clazz, classInvDecl);
198        Ast.addDeclaration(clazz, getInvariantsDecl());
199        Ast.addDeclaration(clazz, isInstrumentedDecl());
200        Ast.addDeclaration(clazz, staticPropertyDecl());
201        Ast.addDeclaration(clazz, staticPropertyInit());
202      }
203    }
204  }
205
206  /**
207   * Adds code to check class invariants and preconditions on entry (but not object invariants,
208   * because there's no object yet!).
209   *
210   * <p>Adds code to check postcontiions, class and object invariants on exit.
211   */
212  // ConstructorDeclaration:
213  // f0 -> [ TypeParameters() ]
214  // f1 -> <IDENTIFIER>
215  // f2 -> FormalParameters()
216  // f3 -> [ "throws" NameList() ]
217  // f4 -> "{"
218  // f5 -> [ ExplicitConstructorInvocation() ]
219  // f6 -> ( BlockStatement() )*
220  @Override
221  public void visit(ConstructorDeclaration ctor) {
222
223    // Fix any line/col inconsistencies first
224    ctor.accept(new TreeFormatter());
225
226    visitedConstructors.add(Ast.getConstructor(ctor));
227
228    super.visit(ctor);
229
230    // Find declared throwables.
231    // List<String> declaredThrowables = getDeclaredThrowables(ctor.f3);
232
233    // System.out.println(Ast.formatEntireTree(ctor));
234
235    List<PptTopLevel> matching_ppts = pptMatcher.getMatches(pptmap, ctor);
236
237    StringBuilder code = new StringBuilder();
238
239    NodeListOptional ctorBody = ctor.f6;
240
241    // Create the code for a new BlockStatement that will be the new
242    // body of the constructor.
243    code.append("{");
244
245    // Count this program point entry.
246    code.append("daikon.tools.runtimechecker.Runtime.numPptEntries++;");
247
248    // Check class invariants.
249    code.append(
250        "checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time.onEntry);");
251
252    String name = Ast.getName(ctor);
253    List<String> typesAndParameters = new ArrayList<>();
254    for (FormalParameter param : Ast.getParametersNoImplicit(ctor)) {
255      typesAndParameters.add(Ast.format(param));
256    }
257
258    checkerClasses.addDeclaration(
259        ctor,
260        checkPreconditions_checker_constructor(
261            matching_ppts, pptmap, name, typesAndParameters, false /* check minor properties*/));
262    checkerClasses.addDeclaration(
263        ctor,
264        checkPreconditions_checker_constructor(
265            matching_ppts, pptmap, name, typesAndParameters, true /* check major properties*/));
266
267    checkerClasses.addDeclaration(
268        ctor,
269        checkPostconditions_checker_constructor(
270            matching_ppts, pptmap, name, typesAndParameters, false /* check minor properties*/));
271
272    checkerClasses.addDeclaration(
273        ctor,
274        checkPostconditions_checker_constructor(
275            matching_ppts, pptmap, name, typesAndParameters, true /* check major properties*/));
276
277    // Check preconditions.
278    checkPreconditions(code, matching_ppts, pptmap);
279
280    // Call original constructor code, wrapped in a try clause so that
281    // we can evaluate object/class invariants before exiting, even
282    // if an exception is thrown.
283    code.append("boolean methodThrewSomething_instrument = false;");
284
285    // code.append("try {");
286
287    // Insert original constructor code.
288    // [[ TODO: should I use the daikon dumper that Mike found? ]]
289    StringWriter stringWriter = new StringWriter();
290    TreeDumper dumper = new TreeDumper(stringWriter);
291    dumper.visit(ctorBody);
292    code.append(stringWriter.toString());
293
294    // Handle any exceptions, check postconditions, object and class
295    // invariants.
296    exitChecks(
297        code,
298        matching_ppts,
299        pptmap,
300        // declaredThrowables,
301        false);
302
303    code.append("}");
304
305    // Replace constructor body with instrumented code.
306    BlockStatement newCtorBody = (BlockStatement) Ast.create("BlockStatement", code.toString());
307    // newCtorBody.accept(new TreeFormatter(2, 0));
308    ctor.f6 = new NodeListOptional(newCtorBody);
309  }
310
311  // Methods that we have created
312  private final Set<MethodDeclaration> generated_methods = new HashSet<>();
313
314  /** */
315  // MethodDeclaration:
316  // f0 -> [ TypeParameters() ]
317  // f1 -> ResultType()
318  // f2 -> MethodDeclarator()
319  // f3 -> [ "throws" NameList() ]
320  // f4 -> ( Block() | ";" )
321  @Override
322  public void visit(MethodDeclaration method) {
323
324    // Fix any line/col inconsistencies first
325    method.accept(new TreeFormatter());
326
327    visitedMethods.add(Ast.getMethod(method));
328
329    super.visit(method);
330
331    @SuppressWarnings(
332        "nullness") // application invariant: method node is always in a class or interface
333    @NonNull ClassOrInterfaceDeclaration clsdecl =
334        (ClassOrInterfaceDeclaration) Ast.getParent(ClassOrInterfaceDeclaration.class, method);
335
336    // skip anonymous nested classes for now, hard to refer to the right this object there...
337    if (Ast.isInterface(clsdecl) || Ast.isInAnonymousClass(method)) {
338      return;
339    }
340
341    // skip abstract methods
342    if (Ast.modifierPresent(Ast.getModifiers(method), "abstract")) {
343      return;
344    }
345
346    method.accept(new TreeFormatter());
347
348    //         System.out.println("@@@0");
349    //         method.accept(new TreeDumper());
350    //         System.out.println("@@@1");
351
352    if (generated_methods.contains(method)) {
353      return;
354    }
355
356    // Determine if method is static.
357    boolean isStatic = Ast.isStatic(method);
358
359    // Find declared throwables.
360    // List<String> declaredThrowables = getDeclaredThrowables(method.f3);
361
362    List<PptTopLevel> matching_ppts = pptMatcher.getMatches(pptmap, method);
363
364    String name = Ast.getName(method);
365    String returnType = Ast.getReturnType(method);
366    List<String> typesAndParameters = new ArrayList<>();
367    List<String> parameters = new ArrayList<>();
368    for (FormalParameter param : Ast.getParameters(method)) {
369      parameters.add(Ast.getName(param));
370      typesAndParameters.add(Ast.format(param));
371    }
372
373    InstrumentHandler.debug.fine("Method: " + name);
374
375    StringBuilder code = new StringBuilder();
376
377    code.append("{");
378
379    // Count this program point entry.
380    code.append("daikon.tools.runtimechecker.Runtime.numPptEntries++;");
381
382    // Check object invariants.
383    if (!isStatic) {
384      code.append(
385          "checkObjectInvariants_instrument(daikon.tools.runtimechecker.Violation.Time.onEntry);");
386    }
387
388    // Check class invariants.
389    code.append(
390        "checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time.onEntry);");
391
392    checkerClasses.addDeclaration(
393        method,
394        checkPreconditions_checker_method(
395            matching_ppts, pptmap, name, typesAndParameters, false /* check minor properties */));
396    checkerClasses.addDeclaration(
397        method,
398        checkPreconditions_checker_method(
399            matching_ppts, pptmap, name, typesAndParameters, true /* check major properties */));
400
401    checkerClasses.addDeclaration(
402        method,
403        checkPostconditions_checker_method(
404            matching_ppts,
405            pptmap,
406            name,
407            returnType,
408            typesAndParameters,
409            false /* check minor properties */));
410
411    checkerClasses.addDeclaration(
412        method,
413        checkPostconditions_checker_method(
414            matching_ppts,
415            pptmap,
416            name,
417            returnType,
418            typesAndParameters,
419            true /* check major properties */));
420
421    checkPreconditions(code, matching_ppts, pptmap);
422
423    // Call original method, wrapped in a try clause so that we
424    // can evaluate object/class invariants before exiting.
425    code.append("boolean methodThrewSomething_instrument = false;");
426    if (!returnType.equals("void")) {
427      code.append(returnType + " retval_instrument = ");
428
429      // Assign some initial value to retval_instrument, otherwise
430      // compiler issues a "might not have been initialized" error.
431      if (returnType.equals("boolean")) {
432        code.append("false");
433      } else if (returnType.equals("char")) {
434        code.append("'a'");
435      } else if (returnType.equals("byte")
436          || returnType.equals("double")
437          || returnType.equals("float")
438          || returnType.equals("int")
439          || returnType.equals("long")
440          || returnType.equals("short")) {
441        code.append("0");
442      } else {
443        code.append("null");
444      }
445
446      code.append(";");
447    }
448
449    // code.append("try {");
450
451    if (!returnType.equals("void")) {
452      code.append("retval_instrument = ");
453    }
454
455    code.append("internal$" + name + "(" + String.join(", ", parameters) + ");");
456
457    exitChecks(
458        code,
459        matching_ppts,
460        pptmap,
461        // declaredThrowables,
462        isStatic);
463
464    // Return value.
465    if (!returnType.equals("void")) {
466      code.append("return retval_instrument;");
467    }
468
469    code.append("}");
470
471    // Add method to AST.
472    String new_method = code.toString();
473
474    MethodDeclaration wrapper =
475        (MethodDeclaration)
476            Ast.create(
477                "MethodDeclaration",
478                new Class[] {Integer.TYPE},
479                new Object[] {0}, // modifiers = 0
480                Ast.format(method));
481
482    Block block = (Block) Ast.create("Block", new_method);
483
484    wrapper.f4.choice = block;
485    wrapper.accept(new TreeFormatter());
486
487    Modifiers modifiersOrig = Ast.getModifiers(method);
488    Modifiers modifiers = (Modifiers) Ast.create("Modifiers", Ast.format(modifiersOrig));
489    modifiers.accept(new TreeFormatter());
490
491    @SuppressWarnings(
492        "nullness") // application invariant: method node is always in a class or interface
493    @NonNull ClassOrInterfaceBody c =
494        (ClassOrInterfaceBody) Ast.getParent(ClassOrInterfaceBody.class, method);
495
496    StringBuilder modifiers_declaration_stringbuffer = new StringBuilder();
497    modifiers_declaration_stringbuffer.append(Ast.format(modifiers));
498    modifiers_declaration_stringbuffer.append(" ");
499    modifiers_declaration_stringbuffer.append(Ast.format(wrapper));
500
501    ClassOrInterfaceBodyDeclaration d =
502        (ClassOrInterfaceBodyDeclaration)
503            Ast.create(
504                "ClassOrInterfaceBodyDeclaration",
505                new Class[] {Boolean.TYPE},
506                new Object[] {Boolean.FALSE}, // isInterface == false
507                modifiers_declaration_stringbuffer.toString());
508    Ast.addDeclaration(c, d);
509    NodeSequence ns = (NodeSequence) d.f0.choice;
510    NodeChoice nc = (NodeChoice) ns.elementAt(1);
511    MethodDeclaration generated_method = (MethodDeclaration) nc.choice;
512    generated_methods.add(generated_method);
513
514    // Rename the original method, and make it private.
515    Ast.setName(method, "internal$" + name);
516    Ast.setAccess(method, "private");
517    Ast.removeMethodDeclAnnotations(method);
518  }
519
520  // vioTime can be the name of a variable (which should be in scope)
521  // or a string, but if it's a string, then you should write it as
522  // something like: \"<ENTER>\"
523  private void appendInvariantChecks(List<Invariant> invs, StringBuilder code, String vioTime) {
524    for (Invariant inv : invs) {
525
526      InstrumentHandler.debug.fine("inv type: " + inv.getClass().getName());
527
528      String javarep = inv.format_using(OutputFormat.JAVA);
529
530      InstrumentHandler.debug.fine("javarep: " + javarep);
531
532      Property property = toProperty(inv);
533
534      String xmlString = property.xmlString();
535
536      InstrumentHandler.debug.fine("xmlString: " + xmlString);
537
538      // [[ TODO : explain this. ]]
539      // [[ TODO : move this to filterInvariants method. ]]
540      if (xmlString.indexOf("orig(") != -1) {
541        continue;
542      }
543
544      if (javarep.indexOf("unimplemented") != -1) {
545        // [[ TODO: print a warning that some invariants were
546        // unimplemented. ]]
547        continue;
548      }
549
550      if (javarep.indexOf("\\result") != -1) {
551        javarep = javarep.replaceAll("\\\\result", "retval_instrument");
552      }
553
554      InstrumentHandler.debug.fine("xmlStringToIndex: " + xmlStringToIndex.get(xmlString));
555
556      String addViolationToListCode =
557          "daikon.tools.runtimechecker.Runtime.violationsAdd"
558              + "(daikon.tools.runtimechecker.Violation.get(daikonProperties["
559              + xmlStringToIndex.get(xmlString)
560              + "], "
561              + vioTime
562              + "));";
563
564      code.append("try {" + daikon.Global.lineSep + "");
565      code.append("daikon.tools.runtimechecker.Runtime.numEvaluations++;");
566      code.append("if (!(" + daikon.Global.lineSep + "");
567      code.append(javarep);
568      code.append(")) {");
569      code.append(addViolationToListCode);
570      code.append("}");
571      code.append("} catch (ThreadDeath t_instrument) {" + daikon.Global.lineSep + "");
572      code.append("throw t_instrument;");
573      code.append("} catch (Throwable t_instrument) {" + daikon.Global.lineSep + "");
574      // don't catch anything. The assumption is that invariant-checking code
575      // never leads to an exception.
576      code.append("}");
577      //             code.append(addViolationToListCode);
578      //             code.append("} catch (Error t_instrument) {" + daikon.Global.lineSep + "");
579      //             code.append(addViolationToListCode);
580      //             code.append("}" + daikon.Global.lineSep + "");
581    }
582  }
583
584  private void appendInvariantChecks_checker(List<InvProp> ips, StringBuilder code) {
585
586    for (InvProp ip : ips) {
587
588      Invariant inv = ip.invariant;
589      Property property = ip.property;
590
591      assert property.xmlString().equals(toProperty(inv).xmlString());
592
593      String javarep = inv.format_using(OutputFormat.JAVA);
594
595      String daikonrep = inv.format_using(OutputFormat.DAIKON);
596
597      String xmlString = property.xmlString();
598
599      // [[ TODO : explain this. ]]
600      // [[ TODO : move this to filterInvariants method. ]]
601      if (xmlString.indexOf("orig(") != -1) {
602        continue;
603      }
604
605      if (javarep.indexOf("unimplemented") != -1) {
606        // [[ TODO: print a warning that some invariants were
607        // unimplemented. ]]
608        continue;
609      }
610
611      if (javarep.indexOf("\\result") != -1) {
612        javarep = javarep.replaceAll("\\\\result", "checker_returnval");
613      }
614
615      code.append("// Check: " + daikonrep + daikon.Global.lineSep);
616      code.append("assert ");
617      code.append(fixForExternalUse(javarep));
618      code.append(";");
619    }
620  }
621
622  private static String fixForExternalUse(String inv) {
623    inv = inv.replace("this", "thiz");
624    return inv;
625  }
626
627  private ClassOrInterfaceBodyDeclaration isInstrumentedDecl() {
628    return (ClassOrInterfaceBodyDeclaration)
629        Ast.create(
630            "ClassOrInterfaceBodyDeclaration",
631            new Class[] {Boolean.TYPE},
632            new Object[] {Boolean.FALSE}, // isInterface == false
633            "public static boolean isDaikonInstrumented() { return true; }");
634  }
635
636  private ClassOrInterfaceBodyDeclaration getInvariantsDecl() {
637    StringBuilder code = new StringBuilder();
638    code.append("public static java.util.Set getDaikonInvariants() {");
639    code.append("  return new java.util.HashSet(java.util.Arrays.asList(daikonProperties));");
640    code.append("}");
641    return (ClassOrInterfaceBodyDeclaration)
642        Ast.create(
643            "ClassOrInterfaceBodyDeclaration",
644            new Class[] {Boolean.TYPE},
645            new Object[] {Boolean.FALSE}, // isInterface == false
646            code.toString());
647  }
648
649  private ClassOrInterfaceBodyDeclaration staticPropertyDecl() {
650    StringBuilder code = new StringBuilder();
651
652    code.append("private static daikon.tools.runtimechecker.Property[] daikonProperties;");
653    return (ClassOrInterfaceBodyDeclaration)
654        Ast.create(
655            "ClassOrInterfaceBodyDeclaration",
656            new Class[] {Boolean.TYPE},
657            new Object[] {Boolean.FALSE}, // isInterface == false
658            code.toString());
659  }
660
661  /**
662   * Returns an AST for initializng the {@code daikonProperties} variable.
663   *
664   * @return an AST for initializng the {@code daikonProperties} variable
665   */
666  private ClassOrInterfaceBodyDeclaration staticPropertyInit() {
667    StringJoiner code = new StringJoiner(System.lineSeparator());
668
669    code.add("static {");
670    code.add("try {");
671    code.add("daikonProperties = new daikon.tools.runtimechecker.Property[" + varNumCounter + "];");
672
673    for (Map.Entry<@KeyFor("xmlStringToIndex") String, String> e : xmlStringToIndex.entrySet()) {
674      code.add("daikonProperties[" + e.getValue() + "] = ");
675      code.add("    daikon.tools.runtimechecker.Property.get(\"" + e.getKey() + "\");");
676    }
677
678    code.add("} catch (Exception e) {");
679    code.add(
680        " System.err.println(\"malformed invariant. This is probably a bug in the"
681            + " daikon.tools.runtimechecker tool; please submit a bug report.\");");
682    code.add(" e.printStackTrace();");
683    code.add(" System.exit(1);");
684    code.add("}");
685
686    code.add("} // end static");
687
688    return (ClassOrInterfaceBodyDeclaration)
689        Ast.create(
690            "ClassOrInterfaceBodyDeclaration",
691            new Class[] {Boolean.TYPE},
692            new Object[] {Boolean.FALSE}, // isInterface == false
693            code.toString());
694  }
695
696  private ClassOrInterfaceBodyDeclaration checkObjectInvariants_instrumentDeclaration(
697      String classname) {
698
699    StringBuilder code = new StringBuilder();
700    code.append(
701        "private void checkObjectInvariants_instrument"
702            + "(daikon.tools.runtimechecker.Violation.Time time) {");
703    String objectPptname = classname + ":::OBJECT";
704    PptTopLevel objectPpt = pptmap.get(objectPptname);
705    if (objectPpt != null) {
706      List<Invariant> objectInvariants = filterInvariants(Ast.getInvariants(objectPpt, pptmap));
707      appendInvariantChecks(objectInvariants, code, "time");
708    }
709    code.append("}" + daikon.Global.lineSep + "");
710    return (ClassOrInterfaceBodyDeclaration)
711        Ast.create(
712            "ClassOrInterfaceBodyDeclaration",
713            new Class[] {Boolean.TYPE},
714            new Object[] {Boolean.FALSE}, // isInterface == false
715            code.toString());
716  }
717
718  private ClassOrInterfaceBodyDeclaration checkClassInvariantsInstrumentDeclaration(
719      String classname) {
720    StringBuilder code = new StringBuilder();
721    code.append(
722        "private static void checkClassInvariantsInstrument"
723            + "(daikon.tools.runtimechecker.Violation.Time time) {");
724    String classPptname = classname + ":::CLASS";
725    PptTopLevel classPpt = pptmap.get(classPptname);
726    if (classPpt != null) {
727      List<Invariant> classInvariants = filterInvariants(Ast.getInvariants(classPpt, pptmap));
728      appendInvariantChecks(classInvariants, code, "time");
729    }
730    code.append("}" + daikon.Global.lineSep + "");
731    return (ClassOrInterfaceBodyDeclaration)
732        Ast.create(
733            "ClassOrInterfaceBodyDeclaration",
734            new Class[] {Boolean.TYPE},
735            new Object[] {Boolean.FALSE}, // isInterface == false
736            code.toString());
737  }
738
739  private StringBuilder checkObjectInvariants_instrumentDeclaration_checker(
740      String classname, boolean majorProperties) {
741    StringBuilder code = new StringBuilder();
742    code.append(
743        "public static void check"
744            + (majorProperties ? "Major" : "Minor")
745            + "ObjectInvariants(Object thiz) {");
746    String objectPptname = classname + ":::OBJECT";
747    PptTopLevel objectPpt = pptmap.get(objectPptname);
748    if (objectPpt != null) {
749      List<Invariant> objectInvariants = filterInvariants(Ast.getInvariants(objectPpt, pptmap));
750      List<InvProp> finalList;
751      if (majorProperties) {
752        finalList = getMajor(objectInvariants);
753      } else {
754        finalList = getMinor(objectInvariants);
755      }
756      appendInvariantChecks_checker(finalList, code);
757    }
758    code.append("}" + daikon.Global.lineSep);
759    return code;
760  }
761
762  private StringBuilder checkClassInvariantsInstrumentDeclaration_checker(
763      String classname, boolean majorProperties) {
764    StringBuilder code = new StringBuilder();
765    code.append(
766        "public static void check" + (majorProperties ? "Major" : "Minor") + "ClassInvariants() {");
767    String classPptname = classname + ":::CLASS";
768    PptTopLevel classPpt = pptmap.get(classPptname);
769    if (classPpt != null) {
770      List<Invariant> classInvariants = filterInvariants(Ast.getInvariants(classPpt, pptmap));
771      List<InvProp> finalList;
772      if (majorProperties) {
773        finalList = getMajor(classInvariants);
774      } else {
775        finalList = getMinor(classInvariants);
776      }
777      appendInvariantChecks_checker(finalList, code);
778    }
779    code.append("}" + daikon.Global.lineSep + "");
780    return code;
781  }
782
783  /**
784   * Return a subset of the argument list, removing invariants that do not have a properly
785   * implemented Java format.
786   */
787  private static List<Invariant> filterInvariants(List<Invariant> invariants) {
788    List<Invariant> survivors = new ArrayList<>();
789    for (Invariant inv : invariants) {
790
791      if (!inv.isValidExpression(OutputFormat.JAVA)) {
792        continue;
793      }
794      // Left and right shifts are formatted properly by Daikon,
795      // but as of 2/6/2005, a JTB bug prevents them from being
796      // inserted into code.
797      if (inv instanceof FunctionBinary) {
798        FunctionBinary fb = (FunctionBinary) inv;
799        if (fb.isLshift() || fb.isRshiftSigned() || fb.isRshiftUnsigned()) {
800          // System.err.println("Warning: shift operation skipped: " +
801          // inv.format_using(OutputFormat.JAVA));
802          continue;
803        }
804      }
805
806      if (outputOnlyHighConfInvariants) {
807        if (toProperty(inv).calculateConfidence() < 0.5) {
808          continue;
809        }
810      }
811
812      survivors.add(inv);
813    }
814    return survivors;
815  }
816
817  // private static List<String> getDeclaredThrowables(NodeOptional nodeOpt) {
818  //   List<String> declaredThrowables = new ArrayList<>();
819  //   if (nodeOpt.present()) {
820  //     NodeSequence seq = (NodeSequence) nodeOpt.node;
821  //     // There should only be two elements: "throws" and NameList
822  //     assert seq.size() == 2;
823  //     NameList nameList = (NameList) seq.elementAt(1);
824  //
825  //     StringWriter stringWriter = new StringWriter();
826  //     TreeDumper dumper = new TreeDumper(stringWriter);
827  //     dumper.visit(nameList);
828  //
829  //     String[] declaredThrowablesArray = stringWriter.toString().trim().split(",");
830  //     for (int i = 0; i < declaredThrowablesArray.length; i++) {
831  //       declaredThrowables.add(declaredThrowablesArray[i].trim());
832  //     }
833  //     //       System.out.println("@@@");
834  //     //       for (int i = 0 ; i < declaredThrowables.size() ; i++) {
835  //     //         System.out.println("xxx" + declaredThrowables.get(i) + "xxx");
836  //     //       }
837  //   }
838  //   return declaredThrowables;
839  // }
840
841  // [[ TODO: This method can return the wrong sequence of catch clauses,
842  //    because it has no concept of throwable subclasses, and it just
843  //    orders catch clauses in the order in which they appear in
844  //    declaredThrowable. This can cause compilation to fail. ]]
845  private void exitChecks(
846      StringBuilder code,
847      List<PptTopLevel> matching_ppts,
848      PptMap pptmap,
849      // List<String> declaredThrowables,
850      boolean isStatic) {
851
852    //      List<String> declaredThrowablesLocal = new ArrayList<>(declaredThrowables);
853    //      declaredThrowablesLocal.remove("java.lang.RuntimeException");
854    //      declaredThrowablesLocal.remove("RuntimeException");
855    //      declaredThrowablesLocal.remove("java.lang.Error");
856    //      declaredThrowablesLocal.remove("Error");
857
858    // Count this program point exit.
859    code.append("daikon.tools.runtimechecker.Runtime.numNormalPptExits++;");
860
861    //         // [[ TODO: Figure out what could go wrong here (e.g. what if
862    //         // method declaration says "throws Throwable") and prepare for
863    //         // it. ]]
864    //         for (String declaredThrowable : declaredThrowablesLocal) {
865    //             code.append("} catch (" + declaredThrowable + " t_instrument) {");
866    //             // Count this program point exit.
867    //             code.append("daikon.tools.runtimechecker.Runtime.numExceptionalPptExits++;");
868    //             code.append("  methodThrewSomething_instrument = true;");
869    //             code.append("  throw t_instrument;");
870    //         }
871
872    //      code.append("} catch (java.lang.RuntimeException t_instrument) {");
873    //      code.append("  methodThrewSomething_instrument = true;");
874    //         // Count this program point exit.
875    //         code.append("daikon.tools.runtimechecker.Runtime.numExceptionalPptExits++;");
876    //      code.append("  throw t_instrument;");
877    //      code.append("} catch (java.lang.Error t_instrument) {");
878    //         // Count this program point exit.
879    //         code.append("daikon.tools.runtimechecker.Runtime.numExceptionalPptExits++;");
880    //      code.append("  methodThrewSomething_instrument = true;");
881    //      code.append("  throw t_instrument;");
882
883    //         code.append("} finally {");
884
885    // If method didn't throw an exception, it completed
886    // normally--check method postconditions (If the method didn't
887    // complete normally, it makes no sense to check postconditions,
888    // because Daikon only reports normal-exit postconditions.)
889
890    //         code.append(" if (!methodThrewSomething_instrument) {");
891
892    // Check postconditions.
893    for (PptTopLevel ppt : matching_ppts) {
894      if (ppt.ppt_name.isExitPoint() && ppt.ppt_name.isCombinedExitPoint()) {
895        List<Invariant> postconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
896        appendInvariantChecks(
897            postconditions, code, "daikon.tools.runtimechecker.Violation.Time.onExit");
898      }
899    }
900    //         code.append("}");
901
902    // Check object invariants.
903    if (!isStatic) {
904      code.append(
905          "checkObjectInvariants_instrument(daikon.tools.runtimechecker.Violation.Time.onExit);");
906    }
907    // Check class invariants.
908    code.append(
909        "checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time.onExit);");
910
911    //         code.append("}"); // this closes the finally clause
912  }
913
914  private void checkPreconditions(
915      StringBuilder code, List<PptTopLevel> matching_ppts, PptMap pptmap) {
916    for (PptTopLevel ppt : matching_ppts) {
917      if (ppt.ppt_name.isEnterPoint()) {
918        List<Invariant> preconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
919        appendInvariantChecks(
920            preconditions, code, "daikon.tools.runtimechecker.Violation.Time.onEntry");
921      }
922    }
923  }
924
925  private StringBuilder checkPreconditions_checker_method(
926      List<PptTopLevel> matching_ppts,
927      PptMap pptmap,
928      String methodName,
929      List<String> parameters,
930      boolean majorProperties) {
931
932    StringBuilder code = new StringBuilder();
933    code.append(
934        "public static void check"
935            + (majorProperties ? "Major" : "Minor")
936            + "Preconditions_"
937            + methodName
938            + "("
939            + "Object thiz"
940            + (parameters.size() > 0 ? ", " : "")
941            + String.join(", ", parameters)
942            + ") {");
943
944    for (PptTopLevel ppt : matching_ppts) {
945      if (ppt.ppt_name.isEnterPoint()) {
946        List<Invariant> preconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
947        List<InvProp> finalList;
948        if (majorProperties) {
949          finalList = getMajor(preconditions);
950        } else {
951          finalList = getMinor(preconditions);
952        }
953        appendInvariantChecks_checker(finalList, code);
954      }
955    }
956
957    code.append("}");
958    return code;
959  }
960
961  private StringBuilder checkPostconditions_checker_method(
962      List<PptTopLevel> matching_ppts,
963      PptMap pptmap,
964      String methodName,
965      String returnType,
966      List<String> parameters,
967      boolean majorProperties) {
968
969    StringBuilder code = new StringBuilder();
970    code.append(
971        "public static void check"
972            + (majorProperties ? "Major" : "Minor")
973            + "Postconditions_"
974            + methodName
975            + "("
976            + "Object thiz "
977            + (returnType.equals("void") ? "" : ", " + returnType + " checker_returnval")
978            + (parameters.size() > 0 ? ", " : "")
979            + String.join(", ", parameters)
980            + ") {");
981
982    for (PptTopLevel ppt : matching_ppts) {
983      if (ppt.ppt_name.isExitPoint() && ppt.ppt_name.isCombinedExitPoint()) {
984        List<Invariant> postconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
985        List<InvProp> finalList;
986        if (majorProperties) {
987          finalList = getMajor(postconditions);
988        } else {
989          finalList = getMinor(postconditions);
990        }
991        appendInvariantChecks_checker(finalList, code);
992      }
993    }
994
995    code.append("}");
996    return code;
997  }
998
999  private StringBuilder checkPreconditions_checker_constructor(
1000      List<PptTopLevel> matching_ppts,
1001      PptMap pptmap,
1002      String methodName,
1003      List<String> parameters,
1004      boolean majorProperties) {
1005
1006    StringBuilder code = new StringBuilder();
1007    code.append(
1008        "public static void check"
1009            + (majorProperties ? "Major" : "Minor")
1010            + "Preconditions_"
1011            + methodName
1012            + "("
1013            + String.join(", ", parameters)
1014            + ") {");
1015
1016    for (PptTopLevel ppt : matching_ppts) {
1017      if (ppt.ppt_name.isEnterPoint()) {
1018        List<Invariant> preconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
1019        List<InvProp> finalList;
1020        if (majorProperties) {
1021          finalList = getMajor(preconditions);
1022        } else {
1023          finalList = getMinor(preconditions);
1024        }
1025        appendInvariantChecks_checker(finalList, code);
1026      }
1027    }
1028
1029    code.append("}");
1030    return code;
1031  }
1032
1033  private StringBuilder checkPostconditions_checker_constructor(
1034      List<PptTopLevel> matching_ppts,
1035      PptMap pptmap,
1036      String methodName,
1037      List<String> parameters,
1038      boolean majorProperties) {
1039
1040    StringBuilder code = new StringBuilder();
1041    code.append(
1042        "public static void check"
1043            + (majorProperties ? "Major" : "Minor")
1044            + "Postconditions_"
1045            + methodName
1046            + "("
1047            + "Object thiz "
1048            + (parameters.size() > 0 ? ", " : "")
1049            + String.join(", ", parameters)
1050            + ") {");
1051
1052    for (PptTopLevel ppt : matching_ppts) {
1053      if (ppt.ppt_name.isExitPoint() && ppt.ppt_name.isCombinedExitPoint()) {
1054        List<Invariant> postconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
1055        List<InvProp> finalList;
1056        if (majorProperties) {
1057          finalList = getMajor(postconditions);
1058        } else {
1059          finalList = getMinor(postconditions);
1060        }
1061        appendInvariantChecks_checker(finalList, code);
1062      }
1063    }
1064
1065    code.append("}");
1066    return code;
1067  }
1068
1069  private static Property toProperty(Invariant inv) {
1070    StringBuilder code = new StringBuilder();
1071
1072    String daikonrep = inv.format_using(OutputFormat.DAIKON);
1073
1074    String javarep = inv.format_using(OutputFormat.JAVA);
1075
1076    if (daikonrep.indexOf("\"") != -1 || daikonrep.indexOf("\\") != -1) {
1077      // Now comes some real ugliness: [[ ... ]] It's easier to do
1078      // this transformation on a character list than by pattern
1079      // matching against a String.
1080      char[] chars = daikonrep.toCharArray();
1081      List<Character> charList = new ArrayList<>();
1082      for (int j = 0; j < chars.length; j++) {
1083        char c = chars[j];
1084        if ((c == '\"') || (c == '\\')) {
1085          charList.add('\\');
1086        }
1087        charList.add(c);
1088      }
1089      char[] backslashedChars = new char[charList.size()];
1090      for (int j = 0; j < charList.size(); j++) {
1091        backslashedChars[j] = charList.get(j).charValue();
1092      }
1093      daikonrep = new String(backslashedChars);
1094    }
1095
1096    code.append("<INVINFO>");
1097    code.append("<" + inv.ppt.parent.ppt_name.getPoint() + ">");
1098    code.append("<DAIKON>" + daikonrep + "</DAIKON>");
1099    code.append("<INV>" + StringsPlume.escapeJava(javarep) + "</INV>");
1100    code.append("<DAIKONCLASS>" + inv.getClass().toString() + "</DAIKONCLASS>");
1101    code.append("<METHOD>" + inv.ppt.parent.ppt_name.getSignature() + "</METHOD>");
1102    code.append("</INVINFO>");
1103
1104    try {
1105      return Property.get(code.toString());
1106    } catch (MalformedPropertyException e) {
1107      throw new Error(e);
1108    }
1109  }
1110
1111  /** A pair consisting of an Invariant and its corresponding Property. */
1112  private static class InvProp {
1113    public InvProp(Invariant inv, Property p) {
1114      this.invariant = inv;
1115      this.property = p;
1116    }
1117
1118    public Invariant invariant;
1119    public Property property;
1120  }
1121
1122  /**
1123   * Returns the invariants (and their properties) that have confidence values at or above
1124   * confidenceThreshold.
1125   */
1126  List<InvProp> getMajor(List<Invariant> invs) {
1127
1128    List<InvProp> ret = new ArrayList<>();
1129    for (Invariant i : invs) {
1130      Property p = toProperty(i);
1131      if (p.confidence >= confidenceThreshold) {
1132        ret.add(new InvProp(i, p));
1133      }
1134    }
1135    return ret;
1136  }
1137
1138  /**
1139   * Returns the invariants (and their properties) that have confidence values below
1140   * confidenceThreshold.
1141   */
1142  List<InvProp> getMinor(List<Invariant> invs) {
1143
1144    List<InvProp> ret = new ArrayList<>();
1145    for (Invariant i : invs) {
1146      Property p = toProperty(i);
1147      if (p.confidence < confidenceThreshold) {
1148        ret.add(new InvProp(i, p));
1149      }
1150    }
1151    return ret;
1152  }
1153
1154  /**
1155   * Add checker methods with empty bodies for all public methods and constuctors not explicitly
1156   * declared.
1157   */
1158  public void add_checkers_for_nondeclared_members() {
1159
1160    for (CheckerClass cc : checkerClasses.classes) {
1161
1162      Class<?> c = Ast.getClass(cc.fclassbody);
1163
1164      // Check that all declared methods were in fact visited.
1165      for (Method m : c.getDeclaredMethods()) {
1166        if (!visitedMethods.contains(m)) {
1167          throw new Error("m=" + m + ", visitedMethods=" + visitedMethods);
1168        }
1169      }
1170
1171      // FIXME consider implicit constructors when doing check.
1172      // Check that all declared constructors were in fact visited.
1173      //             for (Constructor cons : c.getDeclaredConstructors()) {
1174      //                 if (!visitedConstructors.contains(cons)) {
1175      //                     assert cons.equals(getDefaultConstructor(c))
1176      //                        : "cons=" + cons + ", visitedConstructors=" + visitedConstructors);
1177      //                 }
1178      //             }
1179
1180      for (Method m : c.getMethods()) {
1181        if (!visitedMethods.contains(m)) {
1182          cc.addDeclaration(createEmptyDeclaration(m));
1183        }
1184      }
1185
1186      for (Constructor<?> cons : c.getConstructors()) {
1187        if (!visitedConstructors.contains(cons)) {
1188          cc.addDeclaration(createEmptyDeclaration(cons));
1189        }
1190      }
1191    }
1192  }
1193
1194  private StringBuilder createEmptyDeclaration(Method m) {
1195
1196    List<String> parameters = new ArrayList<>();
1197    int paramCounter = 0;
1198    for (Class<?> c : m.getParameterTypes()) {
1199      parameters.add(Ast.classnameForSourceOutput(c) + " param" + paramCounter++);
1200    }
1201
1202    StringBuilder code = new StringBuilder();
1203
1204    for (String s : new String[] {"Major", "Minor"}) {
1205      code.append(
1206          "public static void check"
1207              + s
1208              + "Preconditions_"
1209              + m.getName()
1210              + "("
1211              + "Object thiz"
1212              + (parameters.size() > 0 ? ", " : "")
1213              + String.join(", ", parameters)
1214              + ") { /* no properties for this member */ }");
1215
1216      code.append(
1217          "public static void check"
1218              + s
1219              + "Postconditions_"
1220              + m.getName()
1221              + "("
1222              + "Object thiz "
1223              + (m.getReturnType().equals(Void.TYPE)
1224                  ? ""
1225                  : (", " + Ast.classnameForSourceOutput(m.getReturnType()) + " checker_returnval"))
1226              + (parameters.size() > 0 ? ", " : "")
1227              + String.join(", ", parameters)
1228              + ") { /* no properties for this member */ }");
1229    }
1230
1231    return code;
1232  }
1233
1234  private StringBuilder createEmptyDeclaration(Constructor<?> c) {
1235
1236    List<String> parameters = new ArrayList<>();
1237    int paramCounter = 0;
1238    for (Class<?> cls : c.getParameterTypes()) {
1239      parameters.add(Ast.classnameForSourceOutput(cls) + " param" + paramCounter++);
1240    }
1241
1242    StringBuilder code = new StringBuilder();
1243
1244    Package pacg = c.getDeclaringClass().getPackage();
1245    String packageName = (pacg == null ? "" : pacg.getName());
1246    int packageNameLength =
1247        (packageName.equals("") ? 0 : packageName.length() + 1 /* account for ending dot */);
1248    String className = c.getDeclaringClass().getName();
1249    assert className.startsWith(packageName);
1250    String baseClassName = className.substring(packageNameLength);
1251
1252    for (String s : new String[] {"Major", "Minor"}) {
1253
1254      code.append(
1255          "public static void check"
1256              + s
1257              + "Preconditions_"
1258              + baseClassName
1259              + "("
1260              + String.join(", ", parameters)
1261              + ") { /* no properties for this member */ }");
1262
1263      code.append(
1264          "public static void check"
1265              + s
1266              + "Postconditions_"
1267              + baseClassName
1268              + "("
1269              + "Object thiz "
1270              + (parameters.size() > 0 ? ", " : "")
1271              + String.join(", ", parameters)
1272              + ") { /* no properties for this member */ }");
1273    }
1274
1275    return code;
1276  }
1277}