001package daikon.simplify;
002
003import java.io.IOException;
004import java.util.logging.Logger;
005import org.checkerframework.checker.lock.qual.GuardSatisfied;
006import org.checkerframework.checker.lock.qual.GuardedBy;
007import org.checkerframework.dataflow.qual.SideEffectFree;
008
009/**
010 * A Check command takes a given proposition and asks the Session to prove it. The apply method
011 * returns when a result is available; the valid field contains the result.
012 */
013public class CmdCheck implements Cmd {
014  public static final Logger debug = Logger.getLogger("daikon.simplify.CmdCheck");
015
016  private static final String lineSep = System.lineSeparator();
017
018  public final String proposition;
019  public boolean valid = false;
020  public boolean unknown = false;
021  public String counterexample = "";
022
023  public CmdCheck(String proposition) {
024    this.proposition = proposition.trim();
025    SimpUtil.assert_well_formed(proposition);
026  }
027
028  /** For documentation, read the class overview. */
029  @Override
030  public void apply(final @GuardedBy("<self>") Session s) {
031    try {
032
033      String result;
034      synchronized (s) {
035        // send out the proposition
036        s.sendLine(proposition);
037        if (Session.dkconfig_verbose_progress > 0) {
038          System.out.print("-");
039          System.out.flush();
040        }
041
042        // read the answer
043        // first, the real result
044        result = s.readLine();
045        if (result == null) {
046          throw new SimplifyError("Probable core dump");
047        }
048        // The "Bad input:"  message generally comes from a syntax error in
049        // a previous formula given to Simplify; see the debugging code in
050        // simplify.LemmaStack.pushLemmas().
051        if (result.startsWith("Bad input:") || result.startsWith("Sx.ReadError in file.")) {
052          if (proposition.equals("(OR)") && !LemmaStack.dkconfig_synchronous_errors) {
053            System.err.println(
054                "For improved error reporting, try using"
055                    + " --config_option "
056                    + "daikon.simplify.LemmaStack."
057                    + "synchronous_errors=true");
058          }
059
060          throw new Error("Simplify error: " + result + " on " + proposition);
061        }
062        if (result.equals("Abort (core dumped)")) {
063          throw new SimplifyError(result);
064        }
065        if (result.equals("Counterexample:")) {
066          // Suck in the counterexample, if given
067          do {
068            counterexample += result + lineSep;
069            result = s.readLine();
070            if (result == null) {
071              throw new SimplifyError("Probable core dump");
072            }
073          } while (result.startsWith(" ") || result.startsWith("\t") || result.equals(""));
074        }
075        // then, a blank line
076        String blank = s.readLine();
077        assert "".equals(blank) : "Not a blank line '" + blank + "' after output '" + result + "'";
078      }
079
080      // expect "##: [Inv|V]alid."
081      int colon = result.indexOf(": ");
082      assert colon != -1;
083      try {
084        Integer.parseInt(result.substring(0, colon));
085      } catch (NumberFormatException e) {
086        throw new Error(
087            "Expected number to prefix result '" + result + "' while checking: " + proposition);
088      }
089      result = result.substring(colon + 2);
090      if ("Valid.".equals(result)) {
091        valid = true;
092        if (Session.dkconfig_verbose_progress > 0) {
093          System.out.print("\bT");
094          System.out.flush();
095        }
096      } else if (result.equals("Unknown.")) {
097        valid = false;
098        unknown = true;
099        if (Session.dkconfig_verbose_progress > 0) {
100          System.out.print("\b?");
101          System.out.flush();
102        }
103      } else {
104        assert "Invalid.".equals(result) : "unexpected reply " + result;
105        if (Session.dkconfig_verbose_progress > 0) {
106          System.out.print("\bF");
107          System.out.flush();
108        }
109        valid = false;
110      }
111
112      SessionManager.debugln("Result: " + valid);
113    } catch (IOException e) {
114      throw new SimplifyError(e.toString());
115    }
116  }
117
118  @SideEffectFree
119  @Override
120  public String toString(@GuardSatisfied CmdCheck this) {
121    return "CmdCheck: " + proposition;
122  }
123}