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}