Source code

001package daikon.simplify;
002
003import static java.nio.charset.StandardCharsets.UTF_8;
004import static java.util.logging.Level.FINE;
005import static java.util.logging.Level.INFO;
006
007import java.io.BufferedReader;
008import java.io.Closeable;
009import java.io.IOException;
010import java.io.InputStream;
011import java.io.InputStreamReader;
012import java.util.logging.Logger;
013import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
014import org.checkerframework.checker.lock.qual.GuardSatisfied;
015import org.checkerframework.checker.lock.qual.GuardedBy;
016import org.checkerframework.checker.mustcall.qual.MustCall;
017import org.checkerframework.checker.mustcall.qual.Owning;
018import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
019import org.checkerframework.checker.nullness.qual.Nullable;
020import org.checkerframework.checker.nullness.qual.RequiresNonNull;
021
022/** A SessionManager is a component which handles the threading interaction with the Session. */
023public class SessionManager implements Closeable {
024  /** The command to be performed (point of communication with worker thread). */
025  private @Nullable Cmd pending;
026
027  /** Our worker thread; hold onto it so that we can stop it. */
028  private @Owning Worker worker;
029
030  // The error message returned by the worked thread, or null
031  private @Nullable String error = null;
032
033  /** Debug tracer common to all Simplify classes. */
034  public static final Logger debug = Logger.getLogger("daikon.simplify");
035
036  // Deprecated method for setting the debug flag.
037  //    // Enable to dump input and output to the console
038  //    // Use "java -DDEBUG_SIMPLIFY=1 daikon.Daikon ..." or
039  //    //     "make USER_JAVA_FLAGS=-DDEBUG_SIMPLIFY=1 ..."
040
041  /** debugging flag */
042  private static final boolean debug_mgr = debug.isLoggable(FINE);
043
044  /**
045   * log debug message
046   *
047   * @param s message to log
048   */
049  public static void debugln(String s) {
050    if (!debug_mgr) {
051      return;
052    }
053    debug.fine(s);
054  }
055
056  public SessionManager() {
057    debugln("Creating SessionManager");
058    worker = new Worker();
059    worker.setDaemon(true);
060    debugln("Manager: starting worker");
061    synchronized (this) {
062      worker.start();
063      // We won't wake up from this until the worker thread is ready
064      // and wait()ing to accept requests.
065      try {
066        this.wait();
067      } catch (InterruptedException e) {
068        // It's OK for a wait() to be interrupted.
069      }
070    }
071    debugln("SessionManager created");
072  }
073
074  /** Performs the given command, or times out if too much time elapses. */
075  public void request(Cmd command) throws TimeoutException {
076    assert worker != null : "Cannot use closed SessionManager";
077    assert pending == null : "Cannot queue requests";
078    if (debug.isLoggable(FINE)) {
079      System.err.println("Running command " + command);
080      System.err.println(" called from");
081      Throwable t = new Throwable();
082      t.printStackTrace();
083      System.err.flush();
084    }
085    synchronized (this) {
086      // place the command in the slot
087      assert pending == null;
088      pending = command;
089      // tell the worker to wake up
090      this.notifyAll();
091      // wait for worker to finish
092      try {
093        this.wait();
094      } catch (InterruptedException e) {
095        // It's OK for a wait() to be interrupted.
096      }
097      // command finished iff the command was nulled out
098      if (pending != null) {
099        close();
100        throw new TimeoutException();
101      }
102      // check for error
103      if (error != null) {
104        throw new SimplifyError(error);
105      }
106    }
107  }
108
109  /** Shutdown this session. No further commands may be executed. */
110  @SuppressWarnings("nullness") // nulling worker for fast failure (& for GC)
111  @EnsuresCalledMethods(value = "worker", methods = "close")
112  @Override
113  public void close(@GuardSatisfied SessionManager this) {
114    worker.close();
115    worker = null;
116  }
117
118  private static @MonotonicNonNull String prover_background = null;
119
120  private static String proverBackground() {
121    if (prover_background == null) {
122      try {
123        StringBuilder result = new StringBuilder("");
124        String fileName;
125        if (daikon.inv.Invariant.dkconfig_simplify_define_predicates) {
126          fileName = "daikon-background-defined.txt";
127        } else {
128          fileName = "daikon-background.txt";
129        }
130        InputStream bg_stream = SessionManager.class.getResourceAsStream(fileName);
131        if (bg_stream == null) {
132          throw new RuntimeException(
133              "Could not find resource daikon/simplify/" + fileName + " on the classpath");
134        }
135        BufferedReader lines = new BufferedReader(new InputStreamReader(bg_stream, UTF_8));
136        String line;
137        while ((line = lines.readLine()) != null) {
138          line = line.trim();
139          if ((line.length() == 0) || line.startsWith(";")) {
140            continue;
141          }
142          result.append(" ");
143          result.append(line);
144          result.append(daikon.Global.lineSep);
145        }
146        lines.close();
147        prover_background = result.toString();
148      } catch (IOException e) {
149        throw new RuntimeException("Could not load prover background");
150      }
151    }
152    return prover_background;
153  }
154
155  public static int prover_instantiate_count = 0;
156
157  // Start up simplify, and send the universal backgound.
158  // Is successful exactly when return != null.
159  public static @Nullable SessionManager attemptProverStartup() {
160    SessionManager prover;
161
162    // Limit ourselves to a few tries
163    if (prover_instantiate_count > 5) {
164      return null;
165    }
166
167    // Start the prover
168    try {
169      prover_instantiate_count++;
170      prover = new SessionManager();
171    } catch (SimplifyError e) {
172      System.err.println("Could not utilize Simplify: " + e);
173      return null;
174    }
175
176    try {
177      prover.request(new CmdRaw(proverBackground()));
178    } catch (TimeoutException e) {
179      throw new RuntimeException("Timeout on universal background", e);
180    }
181    return prover;
182  }
183
184  /** Helper thread which interacts with a Session, according to the enclosing manager. */
185  @MustCall("close") private class Worker extends Thread implements Closeable {
186    /** The session mananger. */
187    private final SessionManager mgr = SessionManager.this; // just sugar
188
189    /** The associated session, or null if the thread should shutdown. */
190    private @Owning @Nullable @GuardedBy("<self>") Session session = new Session();
191
192    /** True if this has been closed. */
193    private boolean finished = false;
194
195    @Override
196    @SuppressWarnings("nullness") // tricky, but I think it's OK
197    public void run() {
198      debugln("Worker: run");
199      while (session != null) {
200        synchronized (mgr) {
201          mgr.pending = null;
202          mgr.notifyAll();
203          try {
204            mgr.wait(0);
205          } catch (InterruptedException e) {
206            // It's OK for a wait() to be interrupted.
207          }
208          assert mgr.pending != null
209              : "@AssumeAssertion(nullness): bug? might not be true if interrupted?";
210          // session != null && mgr.pending != null;
211        }
212        error = null;
213        try {
214          // session could also be null at this point, I presume.
215          // That's probably what the catch block is for.
216          mgr.pending.apply(session);
217        } catch (Throwable e) {
218          if (finished) {
219            return;
220          }
221          error = e.toString();
222          e.printStackTrace();
223        }
224      }
225    }
226
227    @SuppressWarnings({
228      "nullness:contracts.precondition.override",
229      "builder:required.method.not.called" // operation performed on alias
230    })
231    @EnsuresCalledMethods(value = "session", methods = "close")
232    @RequiresNonNull("session")
233    @Override
234    public void close(@GuardSatisfied Worker this) {
235      finished = true;
236      final @GuardedBy("<self>") Session tmp = session;
237      synchronized (tmp) {
238        tmp.close();
239      }
240      session = null;
241    }
242  }
243
244  /**
245   * Entry point for testing.
246   *
247   * @param args command-line arguments
248   * @throws TimeoutException if SessionManager times out
249   */
250  public static void main(String[] args) throws TimeoutException {
251    daikon.LogHelper.setupLogs(INFO);
252    SessionManager m = null; // dummy initialization to satisfy compiler's definite assignment check
253    try {
254      m = new SessionManager();
255      CmdCheck cc;
256
257      cc = new CmdCheck("(EQ 1 1)");
258      m.request(cc);
259      assert cc.valid;
260
261      cc = new CmdCheck("(EQ 1 2)");
262      m.request(cc);
263      assert !cc.valid;
264
265      cc = new CmdCheck("(EQ x z)");
266      m.request(cc);
267      assert !cc.valid;
268
269      CmdAssume a = new CmdAssume("(AND (EQ x y) (EQ y z))");
270      m.request(a);
271
272      m.request(cc);
273      assert cc.valid;
274
275      m.request(CmdUndoAssume.single);
276
277      m.request(cc);
278      assert !cc.valid;
279
280      StringBuilder buf = new StringBuilder();
281
282      for (int i = 0; i < 20000; i++) {
283        buf.append("(EQ (select a " + i + ") " + (int) (200000 * Math.random()) + ")");
284      }
285      m.request(new CmdAssume(buf.toString()));
286
287      for (int i = 0; i < 10; i++) {
288        try {
289          m.request(new CmdCheck("(NOT (EXISTS (x) (EQ (select a x) (+ x " + i + "))))"));
290        } catch (TimeoutException e) {
291          System.out.println("Timeout, retrying");
292          m.close();
293          m = new SessionManager();
294          m.request(new CmdAssume(buf.toString()));
295        }
296      }
297    } finally {
298      if (m != null) {
299        m.close();
300      }
301    }
302  }
303}