package daikon.tools.runtimechecker;

import daikon.PptMap;
import daikon.PptTopLevel;
import daikon.inv.Invariant;
import daikon.inv.OutputFormat;
import daikon.inv.ternary.threeScalar.FunctionBinary;
import daikon.tools.jtb.Ast;
import daikon.tools.jtb.PptNameMatcher;
import java.io.StringWriter;
import java.lang.reflect.Constructor;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.StringJoiner;
import java.util.Vector;
import jtb.syntaxtree.*;
import jtb.visitor.DepthFirstVisitor;
import jtb.visitor.TreeDumper;
import jtb.visitor.TreeFormatter;
import org.checkerframework.checker.nullness.qual.KeyFor;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.signature.qual.Identifier;
import org.plumelib.util.StringsPlume;

/**
 * Visitor that instruments a Java source file (i.e. adds code at certain places) to check invariant
 * violations at run time.
 */
@SuppressWarnings("rawtypes")
public class InstrumentVisitor extends DepthFirstVisitor {

  // If false, all invariants will be output. If true, only
  // invariants with high confidence will be output.
  public static boolean outputOnlyHighConfInvariants = false;

  // Properties under this threshold will be considered minor; at or
  // above threshold will be considered major.
  // See daikon.tools.runtimechecker.Property.calculateConfidence()
  public static double confidenceThreshold = 0.5;

  // If true, the instrumenter will make all fields of the class
  // visible. The reason for doing this is so that invariants over
  // potentially inaccessible object fields can be evaluated.
  public static boolean makeAllFieldsPublic = false;

  // The map containing the invariants.
  private final PptMap pptmap;

  // The AST of the class FooPropertyChecks, where Foo is the class
  // that we're instrumenting.
  public CheckerClasses checkerClasses;

  // The methods and constructors that were visited (in other words,
  // those explicitly declared in the source).
  public List<Method> visitedMethods = new ArrayList<>();
  public List<Constructor<?>> visitedConstructors = new ArrayList<>();

  // [[ TODO: I'm using xmlString() because it will definitely give
  // different values for different Properties. But if Properties
  // are in fact unique and immutable, and if I ensure that hashcode
  // returns unique values for unique Properties, then I should be
  // able to use hashcode. So: make sure that the statements above
  // are all correct, and then use hashcode. ]]
  private final Map<String, String> xmlStringToIndex = new HashMap<>();

  private int varNumCounter = 0;

  private final PptNameMatcher pptMatcher;

  /** Create a visitor that will insert code to check the invariants contained in pptmap. */
  public InstrumentVisitor(PptMap pptmap, TypeDeclaration root) {

    this.checkerClasses = new CheckerClasses();

    this.pptmap = pptmap;
    this.pptMatcher = new PptNameMatcher(root);

    for (PptTopLevel ppt : pptmap.pptIterable()) {

      if (ppt.ppt_name.isExitPoint() && !ppt.ppt_name.isCombinedExitPoint()) {
        continue;
      }

      List<Invariant> invList = filterInvariants(daikon.tools.jtb.Ast.getInvariants(ppt, pptmap));
      for (Invariant inv : invList) {
        xmlStringToIndex.put(toProperty(inv).xmlString(), Integer.toString(varNumCounter));
        varNumCounter++;
      }
    }
  }

  /** If makeAllFieldsPublic == true, then it makes this field declaration public. */
  @SuppressWarnings("JdkObsolete") // JTB uses Vector
  @Override
  public void visit(FieldDeclaration fd) {

    // Fix any line/col inconsistencies first
    fd.accept(new TreeFormatter());

    super.visit(fd);
    // Grammar production for ClassOrInterfaceBodyDeclaration:
    // f0 -> Initializer()
    //       | Modifiers() ( ClassOrInterfaceDeclaration(modifiers) | EnumDeclaration(modifiers)
    //                       | ConstructorDeclaration() | FieldDeclaration(modifiers)
    //                       | MethodDeclaration(modifiers) )
    //       | ";"

    if (makeAllFieldsPublic) {
      NodeSequence seq = (NodeSequence) fd.getParent().getParent();
      Modifiers modifiers = (Modifiers) seq.elementAt(0);
      List<Node> modifierList = modifiers.f0.nodes;

      List<Node> newModifiers = new ArrayList<>();
      for (Node modifier : modifierList) {
        NodeChoice nc = (NodeChoice) modifier;
        NodeToken token = (NodeToken) nc.choice;
        if (!token.tokenImage.equals("public")
            && !token.tokenImage.equals("protected")
            && !token.tokenImage.equals("private")) {
          newModifiers.add(token);
        }
      }

      newModifiers.add(new NodeToken("public"));
      modifiers.f0.nodes = new Vector<Node>(newModifiers);
    }
  }

  /**
   * Adds the following new methods:
   *
   * <p>checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time time) Checks the
   * class invariants.
   *
   * <p>checkObjectInvariants_instrument(daikon.tools.runtimechecker.Violation.Time time) Check the
   * object invariants
   *
   * <p>isDaikonInstrumented() returns true (you can imagine calling this method to see if the class
   * has been instrumented).
   *
   * <p>getDaikonInvariants() Returns th array of properties being checked.
   *
   * <p>Adds the following field:
   *
   * <p>daikon.tools.runtimechecker.Property[] daikonProperties The properties being checked.
   *
   * <p>Adds code that initializes the properties array.
   */
  @Override
  public void visit(ClassOrInterfaceBody clazz) {

    checkerClasses.addCheckerClass(clazz);

    // Fix any line/col inconsistencies first
    clazz.accept(new TreeFormatter());

    super.visit(clazz);

    if (Ast.isInterface(clazz)) {
      return;
    }

    // add method to check object and class invariants.

    // just skip anonymous classes for now, hard to get a name for them without a decl node...
    if ((clazz.getParent() instanceof ClassOrInterfaceDeclaration)) {
      ClassOrInterfaceDeclaration ucd = (ClassOrInterfaceDeclaration) clazz.getParent();
      String classname = Ast.getClassName(ucd);
      ClassOrInterfaceBodyDeclaration objInvDecl =
          checkObjectInvariants_instrumentDeclaration(classname);
      Ast.addDeclaration(clazz, objInvDecl);

      checkerClasses.addDeclaration(
          clazz,
          checkObjectInvariants_instrumentDeclaration_checker(
              classname, false /* check minor properties */));
      checkerClasses.addDeclaration(
          clazz,
          checkObjectInvariants_instrumentDeclaration_checker(
              classname, true /* check major properties */));

      if (!Ast.isInner(ucd) || Ast.isStatic(ucd)) {
        ClassOrInterfaceBodyDeclaration classInvDecl =
            checkClassInvariantsInstrumentDeclaration(classname);
        checkerClasses.addDeclaration(
            clazz,
            checkClassInvariantsInstrumentDeclaration_checker(
                classname, false /* check minor properties */));
        checkerClasses.addDeclaration(
            clazz,
            checkClassInvariantsInstrumentDeclaration_checker(
                classname, true /* check minor properties */));
        Ast.addDeclaration(clazz, classInvDecl);
        Ast.addDeclaration(clazz, getInvariantsDecl());
        Ast.addDeclaration(clazz, isInstrumentedDecl());
        Ast.addDeclaration(clazz, staticPropertyDecl());
        Ast.addDeclaration(clazz, staticPropertyInit());
      }
    }
  }

  /**
   * Adds code to check class invariants and preconditions on entry (but not object invariants,
   * because there's no object yet!).
   *
   * <p>Adds code to check postcontiions, class and object invariants on exit.
   */
  // ConstructorDeclaration:
  // f0 -> [ TypeParameters() ]
  // f1 -> <IDENTIFIER>
  // f2 -> FormalParameters()
  // f3 -> [ "throws" NameList() ]
  // f4 -> "{"
  // f5 -> [ ExplicitConstructorInvocation() ]
  // f6 -> ( BlockStatement() )*
  @Override
  public void visit(ConstructorDeclaration ctor) {

    // Fix any line/col inconsistencies first
    ctor.accept(new TreeFormatter());

    visitedConstructors.add(Ast.getConstructor(ctor));

    super.visit(ctor);

    // Find declared throwables.
    // List<String> declaredThrowables = getDeclaredThrowables(ctor.f3);

    // System.out.println(Ast.formatEntireTree(ctor));

    List<PptTopLevel> matching_ppts = pptMatcher.getMatches(pptmap, ctor);

    StringBuilder code = new StringBuilder();

    NodeListOptional ctorBody = ctor.f6;

    // Create the code for a new BlockStatement that will be the new
    // body of the constructor.
    code.append("{");

    // Count this program point entry.
    code.append("daikon.tools.runtimechecker.Runtime.numPptEntries++;");

    // Check class invariants.
    code.append(
        "checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time.onEntry);");

    String name = Ast.getName(ctor);
    List<String> typesAndParameters = new ArrayList<>();
    for (FormalParameter param : Ast.getParametersNoImplicit(ctor)) {
      typesAndParameters.add(Ast.format(param));
    }

    checkerClasses.addDeclaration(
        ctor,
        checkPreconditions_checker_constructor(
            matching_ppts, pptmap, name, typesAndParameters, false /* check minor properties*/));
    checkerClasses.addDeclaration(
        ctor,
        checkPreconditions_checker_constructor(
            matching_ppts, pptmap, name, typesAndParameters, true /* check major properties*/));

    checkerClasses.addDeclaration(
        ctor,
        checkPostconditions_checker_constructor(
            matching_ppts, pptmap, name, typesAndParameters, false /* check minor properties*/));

    checkerClasses.addDeclaration(
        ctor,
        checkPostconditions_checker_constructor(
            matching_ppts, pptmap, name, typesAndParameters, true /* check major properties*/));

    // Check preconditions.
    checkPreconditions(code, matching_ppts, pptmap);

    // Call original constructor code, wrapped in a try clause so that
    // we can evaluate object/class invariants before exiting, even
    // if an exception is thrown.
    code.append("boolean methodThrewSomething_instrument = false;");

    // code.append("try {");

    // Insert original constructor code.
    // [[ TODO: should I use the daikon dumper that Mike found? ]]
    StringWriter stringWriter = new StringWriter();
    TreeDumper dumper = new TreeDumper(stringWriter);
    dumper.visit(ctorBody);
    code.append(stringWriter.toString());

    // Handle any exceptions, check postconditions, object and class
    // invariants.
    exitChecks(
        code,
        matching_ppts,
        pptmap,
        // declaredThrowables,
        false);

    code.append("}");

    // Replace constructor body with instrumented code.
    BlockStatement newCtorBody = (BlockStatement) Ast.create("BlockStatement", code.toString());
    // newCtorBody.accept(new TreeFormatter(2, 0));
    ctor.f6 = new NodeListOptional(newCtorBody);
  }

  // Methods that we have created
  private final Set<MethodDeclaration> generated_methods = new HashSet<>();

  /** */
  // MethodDeclaration:
  // f0 -> [ TypeParameters() ]
  // f1 -> ResultType()
  // f2 -> MethodDeclarator()
  // f3 -> [ "throws" NameList() ]
  // f4 -> ( Block() | ";" )
  @Override
  public void visit(MethodDeclaration method) {

    // Fix any line/col inconsistencies first
    method.accept(new TreeFormatter());

    visitedMethods.add(Ast.getMethod(method));

    super.visit(method);

    @SuppressWarnings(
        "nullness") // application invariant: method node is always in a class or interface
    @NonNull ClassOrInterfaceDeclaration clsdecl =
        (ClassOrInterfaceDeclaration) Ast.getParent(ClassOrInterfaceDeclaration.class, method);

    // skip anonymous nested classes for now, hard to refer to the right this object there...
    if (Ast.isInterface(clsdecl) || Ast.isInAnonymousClass(method)) {
      return;
    }

    // skip abstract methods
    if (Ast.modifierPresent(Ast.getModifiers(method), "abstract")) {
      return;
    }

    method.accept(new TreeFormatter());

    //         System.out.println("@@@0");
    //         method.accept(new TreeDumper());
    //         System.out.println("@@@1");

    if (generated_methods.contains(method)) {
      return;
    }

    // Determine if method is static.
    boolean isStatic = Ast.isStatic(method);

    // Find declared throwables.
    // List<String> declaredThrowables = getDeclaredThrowables(method.f3);

    List<PptTopLevel> matching_ppts = pptMatcher.getMatches(pptmap, method);

    String name = Ast.getName(method);
    String returnType = Ast.getReturnType(method);
    List<String> typesAndParameters = new ArrayList<>();
    List<String> parameters = new ArrayList<>();
    for (FormalParameter param : Ast.getParameters(method)) {
      parameters.add(Ast.getName(param));
      typesAndParameters.add(Ast.format(param));
    }

    InstrumentHandler.debug.fine("Method: " + name);

    StringBuilder code = new StringBuilder();

    code.append("{");

    // Count this program point entry.
    code.append("daikon.tools.runtimechecker.Runtime.numPptEntries++;");

    // Check object invariants.
    if (!isStatic) {
      code.append(
          "checkObjectInvariants_instrument(daikon.tools.runtimechecker.Violation.Time.onEntry);");
    }

    // Check class invariants.
    code.append(
        "checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time.onEntry);");

    checkerClasses.addDeclaration(
        method,
        checkPreconditions_checker_method(
            matching_ppts, pptmap, name, typesAndParameters, false /* check minor properties */));
    checkerClasses.addDeclaration(
        method,
        checkPreconditions_checker_method(
            matching_ppts, pptmap, name, typesAndParameters, true /* check major properties */));

    checkerClasses.addDeclaration(
        method,
        checkPostconditions_checker_method(
            matching_ppts,
            pptmap,
            name,
            returnType,
            typesAndParameters,
            false /* check minor properties */));

    checkerClasses.addDeclaration(
        method,
        checkPostconditions_checker_method(
            matching_ppts,
            pptmap,
            name,
            returnType,
            typesAndParameters,
            true /* check major properties */));

    checkPreconditions(code, matching_ppts, pptmap);

    // Call original method, wrapped in a try clause so that we
    // can evaluate object/class invariants before exiting.
    code.append("boolean methodThrewSomething_instrument = false;");
    if (!returnType.equals("void")) {
      code.append(returnType + " retval_instrument = ");

      // Assign some initial value to retval_instrument, otherwise
      // compiler issues a "might not have been initialized" error.
      if (returnType.equals("boolean")) {
        code.append("false");
      } else if (returnType.equals("char")) {
        code.append("'a'");
      } else if (returnType.equals("byte")
          || returnType.equals("double")
          || returnType.equals("float")
          || returnType.equals("int")
          || returnType.equals("long")
          || returnType.equals("short")) {
        code.append("0");
      } else {
        code.append("null");
      }

      code.append(";");
    }

    // code.append("try {");

    if (!returnType.equals("void")) {
      code.append("retval_instrument = ");
    }

    code.append("internal$" + name + "(" + String.join(", ", parameters) + ");");

    exitChecks(
        code,
        matching_ppts,
        pptmap,
        // declaredThrowables,
        isStatic);

    // Return value.
    if (!returnType.equals("void")) {
      code.append("return retval_instrument;");
    }

    code.append("}");

    // Add method to AST.
    String new_method = code.toString();

    MethodDeclaration wrapper =
        (MethodDeclaration)
            Ast.create(
                "MethodDeclaration",
                new Class[] {Integer.TYPE},
                new Object[] {0}, // modifiers = 0
                Ast.format(method));

    Block block = (Block) Ast.create("Block", new_method);

    wrapper.f4.choice = block;
    wrapper.accept(new TreeFormatter());

    Modifiers modifiersOrig = Ast.getModifiers(method);
    Modifiers modifiers = (Modifiers) Ast.create("Modifiers", Ast.format(modifiersOrig));
    modifiers.accept(new TreeFormatter());

    @SuppressWarnings(
        "nullness") // application invariant: method node is always in a class or interface
    @NonNull ClassOrInterfaceBody c =
        (ClassOrInterfaceBody) Ast.getParent(ClassOrInterfaceBody.class, method);

    StringBuilder modifiers_declaration_stringbuffer = new StringBuilder();
    modifiers_declaration_stringbuffer.append(Ast.format(modifiers));
    modifiers_declaration_stringbuffer.append(" ");
    modifiers_declaration_stringbuffer.append(Ast.format(wrapper));

    ClassOrInterfaceBodyDeclaration d =
        (ClassOrInterfaceBodyDeclaration)
            Ast.create(
                "ClassOrInterfaceBodyDeclaration",
                new Class[] {Boolean.TYPE},
                new Object[] {false}, // isInterface == false
                modifiers_declaration_stringbuffer.toString());
    Ast.addDeclaration(c, d);
    NodeSequence ns = (NodeSequence) d.f0.choice;
    NodeChoice nc = (NodeChoice) ns.elementAt(1);
    MethodDeclaration generated_method = (MethodDeclaration) nc.choice;
    generated_methods.add(generated_method);

    // Rename the original method, and make it private.
    Ast.setName(method, "internal$" + name);
    Ast.setAccess(method, "private");
    Ast.removeMethodDeclAnnotations(method);
  }

  // vioTime can be the name of a variable (which should be in scope)
  // or a string, but if it's a string, then you should write it as
  // something like: \"<ENTER>\"
  private void appendInvariantChecks(List<Invariant> invs, StringBuilder code, String vioTime) {
    for (Invariant inv : invs) {

      InstrumentHandler.debug.fine("inv type: " + inv.getClass().getName());

      String javarep = inv.format_using(OutputFormat.JAVA);

      InstrumentHandler.debug.fine("javarep: " + javarep);

      Property property = toProperty(inv);

      String xmlString = property.xmlString();

      InstrumentHandler.debug.fine("xmlString: " + xmlString);

      // [[ TODO : explain this. ]]
      // [[ TODO : move this to filterInvariants method. ]]
      if (xmlString.indexOf("orig(") != -1) {
        continue;
      }

      if (javarep.indexOf("unimplemented") != -1) {
        // [[ TODO: print a warning that some invariants were
        // unimplemented. ]]
        continue;
      }

      if (javarep.indexOf("\\result") != -1) {
        javarep = javarep.replaceAll("\\\\result", "retval_instrument");
      }

      InstrumentHandler.debug.fine("xmlStringToIndex: " + xmlStringToIndex.get(xmlString));

      String addViolationToListCode =
          "daikon.tools.runtimechecker.Runtime.violationsAdd"
              + "(daikon.tools.runtimechecker.Violation.get(daikonProperties["
              + xmlStringToIndex.get(xmlString)
              + "], "
              + vioTime
              + "));";

      code.append("try {" + daikon.Global.lineSep + "");
      code.append("daikon.tools.runtimechecker.Runtime.numEvaluations++;");
      code.append("if (!(" + daikon.Global.lineSep + "");
      code.append(javarep);
      code.append(")) {");
      code.append(addViolationToListCode);
      code.append("}");
      code.append("} catch (ThreadDeath t_instrument) {" + daikon.Global.lineSep + "");
      code.append("throw t_instrument;");
      code.append("} catch (Throwable t_instrument) {" + daikon.Global.lineSep + "");
      // don't catch anything. The assumption is that invariant-checking code
      // never leads to an exception.
      code.append("}");
      //             code.append(addViolationToListCode);
      //             code.append("} catch (Error t_instrument) {" + daikon.Global.lineSep + "");
      //             code.append(addViolationToListCode);
      //             code.append("}" + daikon.Global.lineSep + "");
    }
  }

  private void appendInvariantChecks_checker(List<InvProp> ips, StringBuilder code) {

    for (InvProp ip : ips) {

      Invariant inv = ip.invariant;
      Property property = ip.property;

      assert property.xmlString().equals(toProperty(inv).xmlString());

      String javarep = inv.format_using(OutputFormat.JAVA);

      String daikonrep = inv.format_using(OutputFormat.DAIKON);

      String xmlString = property.xmlString();

      // [[ TODO : explain this. ]]
      // [[ TODO : move this to filterInvariants method. ]]
      if (xmlString.indexOf("orig(") != -1) {
        continue;
      }

      if (javarep.indexOf("unimplemented") != -1) {
        // [[ TODO: print a warning that some invariants were
        // unimplemented. ]]
        continue;
      }

      if (javarep.indexOf("\\result") != -1) {
        javarep = javarep.replaceAll("\\\\result", "checker_returnval");
      }

      code.append("// Check: " + daikonrep + daikon.Global.lineSep);
      code.append("assert ");
      code.append(fixForExternalUse(javarep));
      code.append(";");
    }
  }

  private static String fixForExternalUse(String inv) {
    inv = inv.replace("this", "thiz");
    return inv;
  }

  private ClassOrInterfaceBodyDeclaration isInstrumentedDecl() {
    return (ClassOrInterfaceBodyDeclaration)
        Ast.create(
            "ClassOrInterfaceBodyDeclaration",
            new Class[] {Boolean.TYPE},
            new Object[] {false}, // isInterface == false
            "public static boolean isDaikonInstrumented() { return true; }");
  }

  private ClassOrInterfaceBodyDeclaration getInvariantsDecl() {
    StringBuilder code = new StringBuilder();
    code.append("public static java.util.Set getDaikonInvariants() {");
    code.append("  return new java.util.HashSet(java.util.Arrays.asList(daikonProperties));");
    code.append("}");
    return (ClassOrInterfaceBodyDeclaration)
        Ast.create(
            "ClassOrInterfaceBodyDeclaration",
            new Class[] {Boolean.TYPE},
            new Object[] {false}, // isInterface == false
            code.toString());
  }

  private ClassOrInterfaceBodyDeclaration staticPropertyDecl() {
    StringBuilder code = new StringBuilder();

    code.append("private static daikon.tools.runtimechecker.Property[] daikonProperties;");
    return (ClassOrInterfaceBodyDeclaration)
        Ast.create(
            "ClassOrInterfaceBodyDeclaration",
            new Class[] {Boolean.TYPE},
            new Object[] {false}, // isInterface == false
            code.toString());
  }

  /**
   * Returns an AST for initializng the {@code daikonProperties} variable.
   *
   * @return an AST for initializng the {@code daikonProperties} variable
   */
  private ClassOrInterfaceBodyDeclaration staticPropertyInit() {
    StringJoiner code = new StringJoiner(System.lineSeparator());

    code.add("static {");
    code.add("try {");
    code.add("daikonProperties = new daikon.tools.runtimechecker.Property[" + varNumCounter + "];");

    for (Map.Entry<@KeyFor("xmlStringToIndex") String, String> e : xmlStringToIndex.entrySet()) {
      code.add("daikonProperties[" + e.getValue() + "] = ");
      code.add("    daikon.tools.runtimechecker.Property.get(\"" + e.getKey() + "\");");
    }

    code.add("} catch (Exception e) {");
    code.add(
        " System.err.println(\"malformed invariant. This is probably a bug in the"
            + " daikon.tools.runtimechecker tool; please submit a bug report.\");");
    code.add(" e.printStackTrace();");
    code.add(" System.exit(1);");
    code.add("}");

    code.add("} // end static");

    return (ClassOrInterfaceBodyDeclaration)
        Ast.create(
            "ClassOrInterfaceBodyDeclaration",
            new Class[] {Boolean.TYPE},
            new Object[] {false}, // isInterface == false
            code.toString());
  }

  private ClassOrInterfaceBodyDeclaration checkObjectInvariants_instrumentDeclaration(
      String classname) {

    StringBuilder code = new StringBuilder();
    code.append(
        "private void checkObjectInvariants_instrument"
            + "(daikon.tools.runtimechecker.Violation.Time time) {");
    String objectPptname = classname + ":::OBJECT";
    PptTopLevel objectPpt = pptmap.get(objectPptname);
    if (objectPpt != null) {
      List<Invariant> objectInvariants = filterInvariants(Ast.getInvariants(objectPpt, pptmap));
      appendInvariantChecks(objectInvariants, code, "time");
    }
    code.append("}" + daikon.Global.lineSep + "");
    return (ClassOrInterfaceBodyDeclaration)
        Ast.create(
            "ClassOrInterfaceBodyDeclaration",
            new Class[] {Boolean.TYPE},
            new Object[] {false}, // isInterface == false
            code.toString());
  }

  private ClassOrInterfaceBodyDeclaration checkClassInvariantsInstrumentDeclaration(
      String classname) {
    StringBuilder code = new StringBuilder();
    code.append(
        "private static void checkClassInvariantsInstrument"
            + "(daikon.tools.runtimechecker.Violation.Time time) {");
    String classPptname = classname + ":::CLASS";
    PptTopLevel classPpt = pptmap.get(classPptname);
    if (classPpt != null) {
      List<Invariant> classInvariants = filterInvariants(Ast.getInvariants(classPpt, pptmap));
      appendInvariantChecks(classInvariants, code, "time");
    }
    code.append("}" + daikon.Global.lineSep + "");
    return (ClassOrInterfaceBodyDeclaration)
        Ast.create(
            "ClassOrInterfaceBodyDeclaration",
            new Class[] {Boolean.TYPE},
            new Object[] {false}, // isInterface == false
            code.toString());
  }

  private StringBuilder checkObjectInvariants_instrumentDeclaration_checker(
      String classname, boolean majorProperties) {
    StringBuilder code = new StringBuilder();
    code.append(
        "public static void check"
            + (majorProperties ? "Major" : "Minor")
            + "ObjectInvariants(Object thiz) {");
    String objectPptname = classname + ":::OBJECT";
    PptTopLevel objectPpt = pptmap.get(objectPptname);
    if (objectPpt != null) {
      List<Invariant> objectInvariants = filterInvariants(Ast.getInvariants(objectPpt, pptmap));
      List<InvProp> finalList;
      if (majorProperties) {
        finalList = getMajor(objectInvariants);
      } else {
        finalList = getMinor(objectInvariants);
      }
      appendInvariantChecks_checker(finalList, code);
    }
    code.append("}" + daikon.Global.lineSep);
    return code;
  }

  private StringBuilder checkClassInvariantsInstrumentDeclaration_checker(
      String classname, boolean majorProperties) {
    StringBuilder code = new StringBuilder();
    code.append(
        "public static void check" + (majorProperties ? "Major" : "Minor") + "ClassInvariants() {");
    String classPptname = classname + ":::CLASS";
    PptTopLevel classPpt = pptmap.get(classPptname);
    if (classPpt != null) {
      List<Invariant> classInvariants = filterInvariants(Ast.getInvariants(classPpt, pptmap));
      List<InvProp> finalList;
      if (majorProperties) {
        finalList = getMajor(classInvariants);
      } else {
        finalList = getMinor(classInvariants);
      }
      appendInvariantChecks_checker(finalList, code);
    }
    code.append("}" + daikon.Global.lineSep + "");
    return code;
  }

  /**
   * Returns a subset of the argument list, removing invariants that do not have a properly
   * implemented Java format.
   *
   * @param invariants a list of invariants
   * @return a new list that is a subset of the argument list
   */
  private static List<Invariant> filterInvariants(List<Invariant> invariants) {
    List<Invariant> survivors = new ArrayList<>();
    for (Invariant inv : invariants) {

      if (!inv.isValidExpression(OutputFormat.JAVA)) {
        continue;
      }
      // Left and right shifts are formatted properly by Daikon,
      // but as of 2/6/2005, a JTB bug prevents them from being
      // inserted into code.
      if (inv instanceof FunctionBinary) {
        FunctionBinary fb = (FunctionBinary) inv;
        if (fb.isLshift() || fb.isRshiftSigned() || fb.isRshiftUnsigned()) {
          // System.err.println("Warning: shift operation skipped: " +
          // inv.format_using(OutputFormat.JAVA));
          continue;
        }
      }

      if (outputOnlyHighConfInvariants) {
        if (toProperty(inv).calculateConfidence() < 0.5) {
          continue;
        }
      }

      survivors.add(inv);
    }
    return survivors;
  }

  // private static List<String> getDeclaredThrowables(NodeOptional nodeOpt) {
  //   List<String> declaredThrowables = new ArrayList<>();
  //   if (nodeOpt.present()) {
  //     NodeSequence seq = (NodeSequence) nodeOpt.node;
  //     // There should only be two elements: "throws" and NameList
  //     assert seq.size() == 2;
  //     NameList nameList = (NameList) seq.elementAt(1);
  //
  //     StringWriter stringWriter = new StringWriter();
  //     TreeDumper dumper = new TreeDumper(stringWriter);
  //     dumper.visit(nameList);
  //
  //     String[] declaredThrowablesArray = stringWriter.toString().trim().split(",");
  //     for (int i = 0; i < declaredThrowablesArray.length; i++) {
  //       declaredThrowables.add(declaredThrowablesArray[i].trim());
  //     }
  //     //       System.out.println("@@@");
  //     //       for (int i = 0 ; i < declaredThrowables.size() ; i++) {
  //     //         System.out.println("xxx" + declaredThrowables.get(i) + "xxx");
  //     //       }
  //   }
  //   return declaredThrowables;
  // }

  // [[ TODO: This method can return the wrong sequence of catch clauses,
  //    because it has no concept of throwable subclasses, and it just
  //    orders catch clauses in the order in which they appear in
  //    declaredThrowable. This can cause compilation to fail. ]]
  private void exitChecks(
      StringBuilder code,
      List<PptTopLevel> matching_ppts,
      PptMap pptmap,
      // List<String> declaredThrowables,
      boolean isStatic) {

    //      List<String> declaredThrowablesLocal = new ArrayList<>(declaredThrowables);
    //      declaredThrowablesLocal.remove("java.lang.RuntimeException");
    //      declaredThrowablesLocal.remove("RuntimeException");
    //      declaredThrowablesLocal.remove("java.lang.Error");
    //      declaredThrowablesLocal.remove("Error");

    // Count this program point exit.
    code.append("daikon.tools.runtimechecker.Runtime.numNormalPptExits++;");

    //         // [[ TODO: Figure out what could go wrong here (e.g. what if
    //         // method declaration says "throws Throwable") and prepare for
    //         // it. ]]
    //         for (String declaredThrowable : declaredThrowablesLocal) {
    //             code.append("} catch (" + declaredThrowable + " t_instrument) {");
    //             // Count this program point exit.
    //             code.append("daikon.tools.runtimechecker.Runtime.numExceptionalPptExits++;");
    //             code.append("  methodThrewSomething_instrument = true;");
    //             code.append("  throw t_instrument;");
    //         }

    //      code.append("} catch (java.lang.RuntimeException t_instrument) {");
    //      code.append("  methodThrewSomething_instrument = true;");
    //         // Count this program point exit.
    //         code.append("daikon.tools.runtimechecker.Runtime.numExceptionalPptExits++;");
    //      code.append("  throw t_instrument;");
    //      code.append("} catch (java.lang.Error t_instrument) {");
    //         // Count this program point exit.
    //         code.append("daikon.tools.runtimechecker.Runtime.numExceptionalPptExits++;");
    //      code.append("  methodThrewSomething_instrument = true;");
    //      code.append("  throw t_instrument;");

    //         code.append("} finally {");

    // If method didn't throw an exception, it completed
    // normally--check method postconditions (If the method didn't
    // complete normally, it makes no sense to check postconditions,
    // because Daikon only reports normal-exit postconditions.)

    //         code.append(" if (!methodThrewSomething_instrument) {");

    // Check postconditions.
    for (PptTopLevel ppt : matching_ppts) {
      if (ppt.ppt_name.isExitPoint() && ppt.ppt_name.isCombinedExitPoint()) {
        List<Invariant> postconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
        appendInvariantChecks(
            postconditions, code, "daikon.tools.runtimechecker.Violation.Time.onExit");
      }
    }
    //         code.append("}");

    // Check object invariants.
    if (!isStatic) {
      code.append(
          "checkObjectInvariants_instrument(daikon.tools.runtimechecker.Violation.Time.onExit);");
    }
    // Check class invariants.
    code.append(
        "checkClassInvariantsInstrument(daikon.tools.runtimechecker.Violation.Time.onExit);");

    //         code.append("}"); // this closes the finally clause
  }

  private void checkPreconditions(
      StringBuilder code, List<PptTopLevel> matching_ppts, PptMap pptmap) {
    for (PptTopLevel ppt : matching_ppts) {
      if (ppt.ppt_name.isEnterPoint()) {
        List<Invariant> preconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
        appendInvariantChecks(
            preconditions, code, "daikon.tools.runtimechecker.Violation.Time.onEntry");
      }
    }
  }

  private StringBuilder checkPreconditions_checker_method(
      List<PptTopLevel> matching_ppts,
      PptMap pptmap,
      @Identifier String methodName,
      List<String> parameters,
      boolean majorProperties) {

    StringBuilder code = new StringBuilder();
    code.append(
        "public static void check"
            + (majorProperties ? "Major" : "Minor")
            + "Preconditions_"
            + methodName
            + "("
            + "Object thiz"
            + (!parameters.isEmpty() ? ", " : "")
            + String.join(", ", parameters)
            + ") {");

    for (PptTopLevel ppt : matching_ppts) {
      if (ppt.ppt_name.isEnterPoint()) {
        List<Invariant> preconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
        List<InvProp> finalList;
        if (majorProperties) {
          finalList = getMajor(preconditions);
        } else {
          finalList = getMinor(preconditions);
        }
        appendInvariantChecks_checker(finalList, code);
      }
    }

    code.append("}");
    return code;
  }

  private StringBuilder checkPostconditions_checker_method(
      List<PptTopLevel> matching_ppts,
      PptMap pptmap,
      @Identifier String methodName,
      String returnType,
      List<String> parameters,
      boolean majorProperties) {

    StringBuilder code = new StringBuilder();
    code.append(
        "public static void check"
            + (majorProperties ? "Major" : "Minor")
            + "Postconditions_"
            + methodName
            + "("
            + "Object thiz "
            + (returnType.equals("void") ? "" : ", " + returnType + " checker_returnval")
            + (!parameters.isEmpty() ? ", " : "")
            + String.join(", ", parameters)
            + ") {");

    for (PptTopLevel ppt : matching_ppts) {
      if (ppt.ppt_name.isExitPoint() && ppt.ppt_name.isCombinedExitPoint()) {
        List<Invariant> postconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
        List<InvProp> finalList;
        if (majorProperties) {
          finalList = getMajor(postconditions);
        } else {
          finalList = getMinor(postconditions);
        }
        appendInvariantChecks_checker(finalList, code);
      }
    }

    code.append("}");
    return code;
  }

  private StringBuilder checkPreconditions_checker_constructor(
      List<PptTopLevel> matching_ppts,
      PptMap pptmap,
      @Identifier String methodName,
      List<String> parameters,
      boolean majorProperties) {

    StringBuilder code = new StringBuilder();
    code.append(
        "public static void check"
            + (majorProperties ? "Major" : "Minor")
            + "Preconditions_"
            + methodName
            + "("
            + String.join(", ", parameters)
            + ") {");

    for (PptTopLevel ppt : matching_ppts) {
      if (ppt.ppt_name.isEnterPoint()) {
        List<Invariant> preconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
        List<InvProp> finalList;
        if (majorProperties) {
          finalList = getMajor(preconditions);
        } else {
          finalList = getMinor(preconditions);
        }
        appendInvariantChecks_checker(finalList, code);
      }
    }

    code.append("}");
    return code;
  }

  private StringBuilder checkPostconditions_checker_constructor(
      List<PptTopLevel> matching_ppts,
      PptMap pptmap,
      @Identifier String methodName,
      List<String> parameters,
      boolean majorProperties) {

    StringBuilder code = new StringBuilder();
    code.append(
        "public static void check"
            + (majorProperties ? "Major" : "Minor")
            + "Postconditions_"
            + methodName
            + "("
            + "Object thiz "
            + (!parameters.isEmpty() ? ", " : "")
            + String.join(", ", parameters)
            + ") {");

    for (PptTopLevel ppt : matching_ppts) {
      if (ppt.ppt_name.isExitPoint() && ppt.ppt_name.isCombinedExitPoint()) {
        List<Invariant> postconditions = filterInvariants(Ast.getInvariants(ppt, pptmap));
        List<InvProp> finalList;
        if (majorProperties) {
          finalList = getMajor(postconditions);
        } else {
          finalList = getMinor(postconditions);
        }
        appendInvariantChecks_checker(finalList, code);
      }
    }

    code.append("}");
    return code;
  }

  private static Property toProperty(Invariant inv) {
    StringBuilder code = new StringBuilder();

    String daikonrep = inv.format_using(OutputFormat.DAIKON);

    String javarep = inv.format_using(OutputFormat.JAVA);

    if (daikonrep.indexOf('\"') != -1 || daikonrep.indexOf('\\') != -1) {
      // Now comes some real ugliness: [[ ... ]] It's easier to do
      // this transformation on a character list than by pattern
      // matching against a String.
      char[] chars = daikonrep.toCharArray();
      List<Character> charList = new ArrayList<>();
      for (int j = 0; j < chars.length; j++) {
        char c = chars[j];
        if ((c == '\"') || (c == '\\')) {
          charList.add('\\');
        }
        charList.add(c);
      }
      char[] backslashedChars = new char[charList.size()];
      for (int j = 0; j < charList.size(); j++) {
        backslashedChars[j] = charList.get(j).charValue();
      }
      daikonrep = new String(backslashedChars);
    }

    code.append("<INVINFO>");
    code.append("<" + inv.ppt.parent.ppt_name.getPoint() + ">");
    code.append("<DAIKON>" + daikonrep + "</DAIKON>");
    code.append("<INV>" + StringsPlume.escapeJava(javarep) + "</INV>");
    code.append("<DAIKONCLASS>" + inv.getClass().toString() + "</DAIKONCLASS>");
    code.append("<METHOD>" + inv.ppt.parent.ppt_name.getSignature() + "</METHOD>");
    code.append("</INVINFO>");

    try {
      return Property.get(code.toString());
    } catch (MalformedPropertyException e) {
      throw new Error(e);
    }
  }

  /** A pair consisting of an Invariant and its corresponding Property. */
  private static class InvProp {
    InvProp(Invariant inv, Property p) {
      this.invariant = inv;
      this.property = p;
    }

    Invariant invariant;
    Property property;
  }

  /**
   * Returns the invariants (and their properties) that have confidence values at or above
   * confidenceThreshold.
   */
  List<InvProp> getMajor(List<Invariant> invs) {

    List<InvProp> ret = new ArrayList<>();
    for (Invariant i : invs) {
      Property p = toProperty(i);
      if (p.confidence >= confidenceThreshold) {
        ret.add(new InvProp(i, p));
      }
    }
    return ret;
  }

  /**
   * Returns the invariants (and their properties) that have confidence values below
   * confidenceThreshold.
   */
  List<InvProp> getMinor(List<Invariant> invs) {

    List<InvProp> ret = new ArrayList<>();
    for (Invariant i : invs) {
      Property p = toProperty(i);
      if (p.confidence < confidenceThreshold) {
        ret.add(new InvProp(i, p));
      }
    }
    return ret;
  }

  /**
   * Add checker methods with empty bodies for all public methods and constructors not explicitly
   * declared.
   */
  public void add_checkers_for_nondeclared_members() {

    for (CheckerClass cc : checkerClasses.classes) {

      Class<?> c = Ast.getClass(cc.fclassbody);

      // Check that all declared methods were in fact visited.
      for (Method m : c.getDeclaredMethods()) {
        if (!visitedMethods.contains(m)) {
          throw new Error("m=" + m + ", visitedMethods=" + visitedMethods);
        }
      }

      // FIXME consider implicit constructors when doing check.
      // Check that all declared constructors were in fact visited.
      //             for (Constructor cons : c.getDeclaredConstructors()) {
      //                 if (!visitedConstructors.contains(cons)) {
      //                     assert cons.equals(getDefaultConstructor(c))
      //                        : "cons=" + cons + ", visitedConstructors=" + visitedConstructors);
      //                 }
      //             }

      for (Method m : c.getMethods()) {
        if (!visitedMethods.contains(m)) {
          cc.addDeclaration(createEmptyDeclaration(m));
        }
      }

      for (Constructor<?> cons : c.getConstructors()) {
        if (!visitedConstructors.contains(cons)) {
          cc.addDeclaration(createEmptyDeclaration(cons));
        }
      }
    }
  }

  private StringBuilder createEmptyDeclaration(Method m) {

    List<String> parameters = new ArrayList<>();
    int paramCounter = 0;
    for (Class<?> c : m.getParameterTypes()) {
      parameters.add(Ast.classnameForSourceOutput(c) + " param" + paramCounter++);
    }

    StringBuilder code = new StringBuilder();

    for (String s : new String[] {"Major", "Minor"}) {
      code.append(
          "public static void check"
              + s
              + "Preconditions_"
              + m.getName()
              + "("
              + "Object thiz"
              + (!parameters.isEmpty() ? ", " : "")
              + String.join(", ", parameters)
              + ") { /* no properties for this member */ }");

      code.append(
          "public static void check"
              + s
              + "Postconditions_"
              + m.getName()
              + "("
              + "Object thiz "
              + (m.getReturnType().equals(Void.TYPE)
                  ? ""
                  : (", " + Ast.classnameForSourceOutput(m.getReturnType()) + " checker_returnval"))
              + (!parameters.isEmpty() ? ", " : "")
              + String.join(", ", parameters)
              + ") { /* no properties for this member */ }");
    }

    return code;
  }

  private StringBuilder createEmptyDeclaration(Constructor<?> c) {

    List<String> parameters = new ArrayList<>();
    int paramCounter = 0;
    for (Class<?> cls : c.getParameterTypes()) {
      parameters.add(Ast.classnameForSourceOutput(cls) + " param" + paramCounter++);
    }

    StringBuilder code = new StringBuilder();

    Package pacg = c.getDeclaringClass().getPackage();
    String packageName = (pacg == null ? "" : pacg.getName());
    int packageNameLength =
        (packageName.equals("") ? 0 : packageName.length() + 1 /* account for ending dot */);
    String className = c.getDeclaringClass().getName();
    assert className.startsWith(packageName);
    String baseClassName = className.substring(packageNameLength);

    for (String s : new String[] {"Major", "Minor"}) {

      code.append(
          "public static void check"
              + s
              + "Preconditions_"
              + baseClassName
              + "("
              + String.join(", ", parameters)
              + ") { /* no properties for this member */ }");

      code.append(
          "public static void check"
              + s
              + "Postconditions_"
              + baseClassName
              + "("
              + "Object thiz "
              + (!parameters.isEmpty() ? ", " : "")
              + String.join(", ", parameters)
              + ") { /* no properties for this member */ }");
    }

    return code;
  }
}
