diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java index 2fbfc7b1ce4..85012ab93a4 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java @@ -35,6 +35,7 @@ import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.smt.*; +import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; @@ -392,7 +393,8 @@ public Collection filterSolverResultsAndShowSolverStatistics( final List output = new ArrayList<>(); for (final SMTSolver solver : problemSolvers) { try { - final SMTSolverResult.ThreeValuedTruth res = solver.getFinalResult().isValid(); + final SMTSolverResult.ThreeValuedTruth res = + solver.getFinalResult().isValid(); if (res == SMTSolverResult.ThreeValuedTruth.UNKNOWN) { unknown++; if (solver.getException() != null) { @@ -400,8 +402,9 @@ public Collection filterSolverResultsAndShowSolverStatistics( } } else if (res == SMTSolverResult.ThreeValuedTruth.FALSIFIABLE) { solvedPaths++; - if (solver.getSocket().getQuery() != null) { - final Model m = solver.getSocket().getQuery().getModel(); + if (solver.getSocket() instanceof AbstractCESolverSocket) { + final Model m = + ((AbstractCESolverSocket) solver.getSocket()).getQuery().getModel(); if (TestCaseGenerator.modelIsOK(m)) { output.add(solver); } else { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java index 0b66418b71b..62576116fd7 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java @@ -23,6 +23,7 @@ import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.smt.*; +import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket; import de.uka.ilkd.key.smt.lang.SMTSort; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.solvertypes.SolverType; @@ -99,7 +100,7 @@ public void launcherStopped(SolverLauncher launcher, Collection finis SMTSolverResult result = solver.getFinalResult(); if (result.isValid().equals(SMTSolverResult.ThreeValuedTruth.FALSIFIABLE) && models.size() < target) { - Model model = solver.getSocket().getQuery().getModel(); + Model model = ((AbstractCESolverSocket) solver.getSocket()).getQuery().getModel(); models.add(model); addModelToTerm(model); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index 3b0112a4f05..f3d738bc973 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java @@ -22,6 +22,7 @@ import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.smt.SMTSolver; +import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket; import de.uka.ilkd.key.smt.model.Heap; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.model.ObjectVal; @@ -521,8 +522,9 @@ public StringBuilder createTestCaseCotent(Collection problemSolvers) */ .proof().name().toString(); boolean success = false; - if (solver.getSocket().getQuery() != null) { - final Model m = solver.getSocket().getQuery().getModel(); + if (solver.getSocket() instanceof AbstractCESolverSocket) { + final Model m = + ((AbstractCESolverSocket) solver.getSocket()).getQuery().getModel(); if (TestCaseGenerator.modelIsOK(m)) { logger.writeln("Generate: " + originalNodeName); Map typeInfMap = diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTProblem.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTProblem.java index 79176217814..7b987bfccc3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTProblem.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTProblem.java @@ -101,7 +101,8 @@ public Sequent getSequent() { * thrown. */ public SMTSolverResult getFinalResult() { - SMTSolverResult unknown = SMTSolverResult.NO_IDEA; + SMTSolverResult unknown = SMTSolverResult + .getUnknownResult(solvers.stream().findFirst().orElseThrow(), this, -1L, null); SMTSolverResult valid = null; SMTSolverResult invalid = null; for (SMTSolver solver : solvers) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolver.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolver.java index a7324aecb57..b7147a2e7f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolver.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.smt; import java.util.Collection; +import java.util.concurrent.Callable; import de.uka.ilkd.key.smt.communication.AbstractSolverSocket; import de.uka.ilkd.key.smt.solvertypes.SolverType; @@ -21,7 +22,7 @@ * * @author ? */ -public interface SMTSolver { +public interface SMTSolver extends Runnable, Callable { /** * Possible reasons for why a solver process was interrupted/stopped. @@ -102,9 +103,6 @@ enum SolverState { */ long getTimeout(); - void setTimeout(long timeout); - - /** * Returns the current state of the solver. Possible values are
* Waiting: The solver process is waiting for the start signal
@@ -130,16 +128,6 @@ enum SolverState { */ boolean isRunning(); - /** - * Starts a solver process. This method should be accessed only by an instance of - * SolverLauncher. If you want to start a solver please have a look at - * SolverLauncher. - * - * @param timeout - * @param settings - */ - void start(SolverTimeout timeout, SMTSettings settings); - /** * @return the reason of the interruption: see ReasonOfInterruption. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index cf920273d82..6ed1b70507a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java @@ -6,6 +6,7 @@ import java.io.IOException; import java.util.Collection; import java.util.LinkedList; +import java.util.Timer; import java.util.concurrent.atomic.AtomicInteger; import de.uka.ilkd.key.java.Services; @@ -13,6 +14,7 @@ import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; +import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket; import de.uka.ilkd.key.smt.communication.AbstractSolverSocket; import de.uka.ilkd.key.smt.communication.ExternalProcessLauncher; import de.uka.ilkd.key.smt.communication.SolverCommunication; @@ -38,7 +40,7 @@ * @author ? * @author Wolfram Pfeifer (SMT communication overhaul) */ -public final class SMTSolverImplementation implements SMTSolver, Runnable { +public final class SMTSolverImplementation implements SMTSolver { private static final Logger LOGGER = LoggerFactory.getLogger(SMTSolverImplementation.class); /** @@ -73,7 +75,7 @@ public final class SMTSolverImplementation implements SMTSolver, Runnable { private final SolverListener listener; /** - * starts a external process and returns the result + * starts an external process and returns the result */ private final ExternalProcessLauncher processLauncher; @@ -88,16 +90,11 @@ public final class SMTSolverImplementation implements SMTSolver, Runnable { */ private final SolverCommunication solverCommunication = new SolverCommunication(); - /** - * The thread that is associated with this solver. - */ - private Thread thread; - /** * The timeout that is associated with this solver. Represents the timertask that is started * when the solver is started. */ - private SolverTimeout solverTimeout; + private final SolverTimeout solverTimeout; /** * stores the reason for interruption if present (e.g. User, Timeout, Exception) @@ -117,7 +114,7 @@ public final class SMTSolverImplementation implements SMTSolver, Runnable { /** * Stores the settings that are used for the execution. */ - private SMTSettings smtSettings; + private final SMTSettings smtSettings; /** * Stores the translation of the problem that is associated with this solver @@ -130,7 +127,7 @@ public final class SMTSolverImplementation implements SMTSolver, Runnable { private TacletSetTranslation tacletTranslation; /** - * If there was an exception while executing the solver it is stored in this attribute. + * If there was an exception while executing the solver, it is stored in this attribute. */ private Throwable exception; @@ -142,7 +139,9 @@ public final class SMTSolverImplementation implements SMTSolver, Runnable { /** * The timeout in seconds for this SMT solver run. */ - private long timeout = -1; + private final long timeout; + + private SMTSolverResult result; /** * Creates a new instance an SMT solver. @@ -151,32 +150,21 @@ public final class SMTSolverImplementation implements SMTSolver, Runnable { * @param listener the listener that has to be informed when the solver state changes * @param services the services needed to translate the problem to SMT format * @param myType the type of the solver to run (e.g., Z3, CVC3, Z3_CE) + * @param timeout the length of timeout */ public SMTSolverImplementation(SMTProblem problem, SolverListener listener, Services services, - SolverType myType) { + SMTSettings smtSettings, + SolverType myType, long timeout) { this.problem = problem; this.listener = listener; this.services = services; + this.smtSettings = smtSettings; this.type = myType; // Why not just call type.getSocket(query) here? this.socket = AbstractSolverSocket.createSocket(type, query); processLauncher = new ExternalProcessLauncher(solverCommunication, myType.getDelimiters()); - } - - /** - * Starts a solver process. This method should be accessed only by an instance of - * SolverLauncher. If you want to start a solver please have a look at - * SolverLauncher. - * - * @param timeout the timeout to use for the solver - * @param settings the SMTSettings to use for this solver - */ - @Override - public void start(SolverTimeout timeout, SMTSettings settings) { - thread = new Thread(this, "SMTProcessor"); - solverTimeout = timeout; - smtSettings = settings; - thread.start(); + this.timeout = timeout; + this.solverTimeout = new SolverTimeout(this); } @Override @@ -193,10 +181,17 @@ public SMTProblem getProblem() { } public void setReasonOfInterruption(ReasonOfInterruption reasonOfInterruption) { - this.reasonOfInterruption = reasonOfInterruption; + setReasonOfInterruption(reasonOfInterruption, null); } - private void setReasonOfInterruption(ReasonOfInterruption reasonOfInterruption, Throwable exc) { + private synchronized void setReasonOfInterruption(ReasonOfInterruption reasonOfInterruption, + Throwable exc) { + if (this.reasonOfInterruption != ReasonOfInterruption.NoInterruption + || solverState == SolverState.Stopped) { + // don't change the reason of interruption after the first interrupt + // also don't interrupt a stopped solver + return; + } this.reasonOfInterruption = reasonOfInterruption; this.exception = exc; } @@ -219,11 +214,6 @@ public long getTimeout() { return timeout; } - @Override - public void setTimeout(long timeout) { - this.timeout = timeout; - } - @Override public SolverState getState() { return solverState; @@ -246,10 +236,12 @@ public boolean isRunning() { @Override public void run() { + Timer timeoutWatcher = new Timer(true); + timeoutWatcher.schedule(solverTimeout, timeout); // Firstly: Set the state to running and inform the listener. setSolverState(SolverState.Running); - listener.processStarted(this, problem); + notifyProcessStarted(); // Secondly: Translate the given problem String[] commands; @@ -257,9 +249,9 @@ public void run() { commands = translateToCommand(problem.getSequent()); } catch (Throwable e) { interruptionOccurred(e); - listener.processInterrupted(this, problem, e); - setSolverState(SolverState.Stopped); solverTimeout.cancel(); + setSolverState(SolverState.Stopped); + notifyProcessInterrupted(e); return; } @@ -270,32 +262,46 @@ public void run() { // processLauncher.getPipe().sendEOF(); String msg = processLauncher.getPipe().readMessage(); - while (msg != null) { - socket.messageIncoming(processLauncher.getPipe(), msg); + SMTSolverResult.ThreeValuedTruth result = null; + while (msg != null && result == null) { + result = socket.messageIncoming(processLauncher.getPipe(), msg); msg = processLauncher.getPipe().readMessage(); } + switch (result) { + case VALID -> this.result = SMTSolverResult.getValidResult(this, problem, + System.currentTimeMillis() - getStartTime(), solverCommunication); + case FALSIFIABLE -> this.result = SMTSolverResult.getFalsifiableResult(this, problem, + System.currentTimeMillis() - getStartTime(), solverCommunication); + case UNKNOWN -> this.result = SMTSolverResult.getUnknownResult(this, problem, + System.currentTimeMillis() - getStartTime(), solverCommunication); + case null -> this.result = SMTSolverResult.getExceptionResult(this, problem, + System.currentTimeMillis() - getStartTime(), solverCommunication, + new IllegalStateException("Solver " + name() + " did not return any result!")); + } } catch (IllegalStateException | IOException | InterruptedException e) { interruptionOccurred(e); Thread.currentThread().interrupt(); } finally { // Close everything. solverTimeout.cancel(); - setSolverState(SolverState.Stopped); - listener.processStopped(this, problem); processLauncher.stop(); + setSolverState(SolverState.Stopped); + notifyProcessStopped(); } } private void interruptionOccurred(Throwable e) { + // TODO this does not make sense. If there was a reason for the interrupt it is overwritten + // here. Only listeners can tell what happened, but this class stores another reason ReasonOfInterruption reason = getReasonOfInterruption(); setReasonOfInterruption(ReasonOfInterruption.Exception, e); switch (reason) { case Exception, NoInterruption -> { setReasonOfInterruption(ReasonOfInterruption.Exception, e); - listener.processInterrupted(this, problem, e); + notifyProcessInterrupted(e); } - case Timeout -> listener.processTimeout(this, problem); - case User -> listener.processUser(this, problem); + case Timeout -> notifyProcessTimeout(); + case User -> notifyProcessUser(); } } @@ -334,9 +340,12 @@ private String[] translateToCommand(Sequent sequent) throws IllegalFormulaExcept new SMTObjTranslator(smtSettings, services, typeOfClassUnderTest); problemString = objTrans.translateProblem(sequent, services, smtSettings).toString(); ModelExtractor transQuery = objTrans.getQuery(); - getSocket().setQuery(transQuery); + AbstractSolverSocket socket = getSocket(); + if (!(socket instanceof AbstractCESolverSocket)) { + throw new IllegalStateException("Socket used does not support counterexamples."); + } + ((AbstractCESolverSocket) socket).setQuery(transQuery); tacletTranslation = null; - } else { SMTTranslator trans = getType().createTranslator(); problemString = @@ -365,15 +374,14 @@ public void interrupt(ReasonOfInterruption reason) { if (solverTimeout != null) { solverTimeout.cancel(); } - if (thread != null) { + if (processLauncher != null) { processLauncher.stop(); - thread.interrupt(); } } @Override public SMTSolverResult getFinalResult() { - return isRunning() ? null : solverCommunication.getFinalResult(); + return isRunning() ? null : result; } @Override @@ -429,4 +437,40 @@ public ModelExtractor getQuery() { public void setQuery(ModelExtractor query) { this.query = query; } + + @Override + public SMTSolverResult call() throws Exception { + run(); + return getFinalResult(); + } + + private void notifyProcessStarted() { + if (listener != null) { + listener.processStarted(this, getProblem()); + } + } + + private void notifyProcessInterrupted(Throwable e) { + if (listener != null) { + listener.processInterrupted(this, getProblem(), e); + } + } + + private void notifyProcessUser() { + if (listener != null) { + listener.processUser(this, getProblem()); + } + } + + private void notifyProcessTimeout() { + if (listener != null) { + listener.processTimeout(this, getProblem()); + } + } + + private void notifyProcessStopped() { + if (listener != null) { + listener.processStopped(this, getProblem()); + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java index cca321c766c..0f31fd9025e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java @@ -3,10 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.smt; +import de.uka.ilkd.key.smt.communication.SolverCommunication; + /** * Encapsulates the result of a single solver. */ -public class SMTSolverResult { +public abstract class SMTSolverResult { + + /** + * Solver this result belongs to + */ + private final SMTSolver solver; + private final SMTProblem problem; + private final long timeTaken; + private final SolverCommunication solverCommunication; /** * In the context of proving nodes/sequents these values mean the following: TRUE iff negation @@ -15,82 +25,178 @@ public class SMTSolverResult { * Note: Currently (1.12.'09) the SMT Solvers do not check if a node is FALSE. */ public enum ThreeValuedTruth { - VALID { - @Override - public String toString() { - return "valid"; - } - }, - FALSIFIABLE { - public String toString() { - return "there is a counter example"; - } - }, - UNKNOWN { - public String toString() { - return "unknown"; - } - } - } + VALID("valid"), + FALSIFIABLE("there is a counter example"), + UNKNOWN("unknown"); - // We should get rid of this constant because it does not track the source (the solver) of the - // result. - public static final SMTSolverResult NO_IDEA = - new SMTSolverResult(ThreeValuedTruth.UNKNOWN, "?"); + private final String description; + ThreeValuedTruth(String description) { + this.description = description; + } + @Override + public String toString() { + return description; + } + } - private final ThreeValuedTruth isValid; - private static int idCounter = 0; - private final int id = ++idCounter; + public static SMTValidResult getValidResult(SMTSolver solver, SMTProblem problem, + long timeTaken, SolverCommunication solverCommunication) { + return new SMTValidResult(solver, problem, timeTaken, solverCommunication); + } - /** This is to identify where the result comes from. E.g. for user feedback. */ - public final String solverName; + public static SMTFalsifiableResult getFalsifiableResult(SMTSolver solver, SMTProblem problem, + long timeTaken, SolverCommunication solverCommunication) { + return new SMTFalsifiableResult(solver, problem, timeTaken, solverCommunication); + } - private SMTSolverResult(ThreeValuedTruth isValid, String solverName) { - this.solverName = solverName; + public static SMTCEResult getCEResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication, ModelExtractor query) { + return new SMTCEResult(solver, problem, timeTaken, solverCommunication, query); + } - this.isValid = isValid; + public static SMTUnknownResult getUnknownResult(SMTSolver solver, SMTProblem problem, + long timeTaken, SolverCommunication solverCommunication) { + return new SMTUnknownResult(solver, problem, timeTaken, solverCommunication); } - public int getID() { - return id; + public static SMTTimeoutResult getTimeoutResult(SMTSolver solver, SMTProblem problem, + long timeTaken, SolverCommunication solverCommunication) { + return new SMTTimeoutResult(solver, problem, timeTaken, solverCommunication); } + public static SMTExceptionResult getExceptionResult(SMTSolver solver, SMTProblem problem, + long timeTaken, SolverCommunication solverCommunication, Throwable exception) { + return new SMTExceptionResult(solver, problem, timeTaken, solverCommunication, exception); + } - public static SMTSolverResult createValidResult(String name) { - return new SMTSolverResult(ThreeValuedTruth.VALID, name); + private SMTSolverResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication) { + this.solver = solver; + this.problem = problem; + this.timeTaken = timeTaken; + this.solverCommunication = solverCommunication; } + public abstract ThreeValuedTruth isValid(); - public static SMTSolverResult createInvalidResult(String name) { - return new SMTSolverResult(ThreeValuedTruth.FALSIFIABLE, name); + public String getRawSolverOutput() { + StringBuilder output = new StringBuilder(); + for (SolverCommunication.Message m : solverCommunication.getOutMessages()) { + String s = m.content(); + output.append(s).append("\n"); + } + return output.toString(); } + public String getRawSolverInput() { + StringBuilder input = new StringBuilder(); - public static SMTSolverResult createUnknownResult(String name) { - return new SMTSolverResult(ThreeValuedTruth.UNKNOWN, name); + for (SolverCommunication.Message m : solverCommunication + .getMessages(SolverCommunication.MessageType.INPUT)) { + String s = m.content(); + input.append(s).append("\n"); + } + return input.toString(); } + public SMTProblem getProblem() { + return problem; + } + public long getTimeTaken() { + return timeTaken; + } - public ThreeValuedTruth isValid() { - return isValid; + public String getName() { + return solver.name(); } + @Override public String toString() { - return isValid.toString(); + return isValid().toString(); } - + @Override public boolean equals(Object o) { if (!(o instanceof SMTSolverResult ssr)) { return false; } - return isValid == ssr.isValid; + return isValid() == ssr.isValid(); } + public static class SMTValidResult extends SMTSolverResult { + private SMTValidResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication) { + super(solver, problem, timeTaken, solverCommunication); + } + + @Override + public ThreeValuedTruth isValid() { + return ThreeValuedTruth.VALID; + } + } + + public static class SMTFalsifiableResult extends SMTSolverResult { + private SMTFalsifiableResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication) { + super(solver, problem, timeTaken, solverCommunication); + } + @Override + public ThreeValuedTruth isValid() { + return ThreeValuedTruth.FALSIFIABLE; + } + } + + public static class SMTCEResult extends SMTFalsifiableResult { + private final ModelExtractor query; + + private SMTCEResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication, ModelExtractor query) { + super(solver, problem, timeTaken, solverCommunication); + this.query = query; + } + + + public ModelExtractor getQuery() { + return query; + } + } + + public static class SMTUnknownResult extends SMTSolverResult { + private SMTUnknownResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication) { + super(solver, problem, timeTaken, solverCommunication); + } + + @Override + public ThreeValuedTruth isValid() { + return ThreeValuedTruth.UNKNOWN; + } + } + + public static class SMTExceptionResult extends SMTUnknownResult { + private final Throwable exception; + + private SMTExceptionResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication, Throwable exception) { + super(solver, problem, timeTaken, solverCommunication); + this.exception = exception; + } + + public Throwable getException() { + return exception; + } + } + + public static class SMTTimeoutResult extends SMTUnknownResult { + private SMTTimeoutResult(SMTSolver solver, SMTProblem problem, long timeTaken, + SolverCommunication solverCommunication) { + super(solver, problem, timeTaken, solverCommunication); + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java index 6dfacf097f6..99e35cd0cf8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java @@ -4,9 +4,9 @@ package de.uka.ilkd.key.smt; import java.util.*; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; import java.util.concurrent.Semaphore; -import java.util.concurrent.locks.Condition; -import java.util.concurrent.locks.ReentrantLock; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.smt.SMTSolver.ReasonOfInterruption; @@ -76,7 +76,11 @@ * can be accessed by solver.getException. */ -public class SolverLauncher implements SolverListener { +public class SolverLauncher { + + private ExecutorService threadPool; + + private Collection solvers; /* ############### Public Interface #################### */ @@ -133,42 +137,24 @@ public void launch(Collection solverTypes, Collection pr } /** - * Stops the execution of the launcher. + * If all permits of the semaphore are acquired the launcher must be stopped. */ - public void stop() { - stopSemaphore.tryAcquire(); - session.interruptAll(ReasonOfInterruption.User); + private boolean isInterrupted() { + return stopSemaphore.availablePermits() == 0; } - /* ################ Implementation ############################ */ - /** - * Period of a timer task. Sometimes it happens that a timer event got lost. Therefore the timer - * tasks are called periodly until it is canceld + * Stops the execution of the launcher. */ - private static final int PERIOD = 50; + public void stop() { + solvers.forEach((solver) -> solver.interrupt(ReasonOfInterruption.User)); + if (threadPool != null) { + threadPool.shutdownNow(); + } + notifyListenersOfStop(); + } - /** - * Used for synchronisation. This lock is used in the same way as the - * synchronizestatement. - */ - private final ReentrantLock lock = new ReentrantLock(); - /** - * This condition is used in order to make the launcher thread wait. The launcher goes to sleep - * when no more solvers can be started and some other solvers are still executed. Everytime a - * solver stops it sends a signal to the wait-condition in order to wake up the - * launcher. - */ - private final Condition wait = lock.newCondition(); - /** - * The timer that is responsible for the timeouts. - */ - private final Timer timer = new Timer(true); - /** - * A sesion encapsulates some attributes that should be accessed only by specified methods (in - * oder to maintain thread safety) - */ - private final Session session = new Session(); + /* ################ Implementation ############################ */ /** * The SMT settings that should be used @@ -193,12 +179,15 @@ public void stop() { */ private void prepareSolvers(Collection factories, Collection problems, Services services) { + threadPool = Executors.newFixedThreadPool(settings.getMaxConcurrentProcesses()); + this.solvers = new ArrayList<>(); for (SMTProblem problem : problems) { for (SolverType factory : factories) { if (factory.isInstalled(false)) { - SMTSolver solver = factory.createSolver(problem, this, services); - solver.setTimeout(settings.getTimeout(factory)); + SMTSolver solver = factory.createSolver(problem, null, services, settings, + settings.getTimeout(factory)); problem.addSolver(solver); + solvers.add(solver); } } } @@ -244,40 +233,6 @@ private void launchIntern(Collection problems, Collection solvers) { - while (startNextSolvers(solvers) && !isInterrupted()) { - SMTSolver solver = solvers.poll(); - Objects.requireNonNull(solver); - - SolverTimeout solverTimeout = new SolverTimeout(solver, session); - timer.schedule(solverTimeout, solver.getTimeout(), PERIOD); - session.addCurrentlyRunning(solver); - - // This cast is okay since there is only the class - // SMTSolverImplementation that implements SMTSolver. - solver.start(solverTimeout, settings); - } - } - - /** - * If all permits of the semaphore are acquired the launcher must be stopped. - */ - private boolean isInterrupted() { - return stopSemaphore.availablePermits() == 0; - } - - /** - * Checks whether it is possible to start another solver. - */ - private boolean startNextSolvers(Queue solvers) { - return !solvers.isEmpty() - && session.getCurrentlyRunningCount() < settings.getMaxConcurrentProcesses(); - } - private void launchSolvers(Queue solvers, Collection problems, Collection solverTypes) { // Show progress dialog @@ -286,9 +241,6 @@ private void launchSolvers(Queue solvers, Collection prob // Launch all solvers until the queue is empty or the launcher is // interrupted. launchLoop(solvers); - // at this point either there are no solvers left to start or - // the whole launching process was interrupted. - waitForRunningSolvers(); cleanUp(solvers); @@ -308,39 +260,11 @@ private void notifyListenersOfStart(Collection problems, */ private void launchLoop(Queue solvers) { // as long as there are jobs to do, start solvers - while (!solvers.isEmpty() && !isInterrupted()) { - lock.lock(); - try { - // start solvers as many as possible - fillRunningList(solvers); - if (!startNextSolvers(solvers) && !isInterrupted()) { - try { - // if there is nothing to do, wait for the next solver - // finishing its task. - wait.await(); - } catch (InterruptedException e) { - launcherInterrupted(e); - } - } - } finally { - lock.unlock(); - } - } - } - - /** - * The launcher should not be stopped until every solver has stopped. - */ - private void waitForRunningSolvers() { - while (session.getCurrentlyRunningCount() > 0) { - lock.lock(); - try { - wait.await(); - } catch (InterruptedException e) { - launcherInterrupted(e); - } finally { - lock.unlock(); - } + try { + threadPool.invokeAll(solvers); + } catch (InterruptedException e) { + launcherInterrupted(e); + notifyListenersOfStop(); } } @@ -354,13 +278,14 @@ private void cleanUp(Collection solvers) { solver.interrupt(ReasonOfInterruption.User); } } + threadPool.shutdown(); } private void notifyListenersOfStop() { - Collection problemSolvers = session.getProblemSolvers(); - Collection finishedSolvers = session.getFinishedSolvers(); + Collection finishedSolvers = new ArrayList<>(solvers.stream() + .filter((solver) -> solver.getState() == SMTSolver.SolverState.Stopped).toList()); - for (SMTSolver solver : problemSolvers) { + for (SMTSolver solver : solvers) { if (!finishedSolvers.contains(solver)) { finishedSolvers.add(solver); } @@ -370,22 +295,8 @@ private void notifyListenersOfStop() { listener.launcherStopped(this, finishedSolvers); } - if (!problemSolvers.isEmpty() && listeners.isEmpty()) { - throw new SolverException(problemSolvers); - } - } - - /** - * Is called when a solver has finished its task (Solver Thread). It removes the solver from the - * list of the currently running solvers and tries to wake up the launcher. - */ - private void notifySolverHasFinished(SMTSolver solver) { - lock.lock(); - try { - session.removeCurrentlyRunning(solver); - } finally { - wait.signal(); - lock.unlock(); + if (solvers.size() != finishedSolvers.size() && listeners.isEmpty()) { + throw new SolverLauncherException(solvers); } } @@ -396,148 +307,4 @@ private void notifySolverHasFinished(SMTSolver solver) { private void launcherInterrupted(Exception e) { throw new RuntimeException(e); } - - @Override - public void processStarted(SMTSolver solver, SMTProblem problem) { - } - - @Override - public void processStopped(SMTSolver solver, SMTProblem problem) { - session.addFinishedSolver(solver); - notifySolverHasFinished(solver); - } - - @Override - public void processInterrupted(SMTSolver solver, SMTProblem problem, Throwable e) { - session.addProblemSolver(solver); - notifySolverHasFinished(solver); - } - - @Override - public void processTimeout(SMTSolver solver, SMTProblem problem) { - notifySolverHasFinished(solver); - } - - @Override - public void processUser(SMTSolver solver, SMTProblem problem) { - } - -} - - -/** - * The session class encapsulates some attributes that should be only accessed by specified methods - * (in order to maintain thread safety) - */ -class Session { - - /** - * Locks the queue of the currently running solvers - */ - private final ReentrantLock lock = new ReentrantLock(); - /** - * Locks the collection of the problem solvers. - */ - private final ReentrantLock problemSolverLock = new ReentrantLock(); - private final ReentrantLock finishedSolverLock = new ReentrantLock(); - private final Collection finishedSolvers = new LinkedList<>(); - private final Collection problemSolvers = new LinkedList<>(); - private final LinkedList currentlyRunning = new LinkedList<>(); - - /** - * Adds a solver to the list of currently running solvers. Thread safe - */ - public void addCurrentlyRunning(SMTSolver solver) { - try { - lock.lock(); - currentlyRunning.add(solver); - } finally { - lock.unlock(); - } - } - - public void removeCurrentlyRunning(SMTSolver solver) { - try { - lock.lock(); - int i = currentlyRunning.indexOf(solver); - if (i >= 0) { - currentlyRunning.remove(i); - } - } finally { - lock.unlock(); - } - } - - public int getCurrentlyRunningCount() { - try { - lock.lock(); - return currentlyRunning.size(); - } finally { // finally trumps return - lock.unlock(); - } - } - - public void interruptSolver(SMTSolver solver, ReasonOfInterruption reason) { - try { - lock.lock(); - Iterator it = currentlyRunning.iterator(); - while (it.hasNext()) { - SMTSolver next = it.next(); - if (next.equals(solver)) { - next.interrupt(reason); - it.remove(); - break; - } - } - } finally { - lock.unlock(); - } - } - - public void interruptAll(ReasonOfInterruption reason) { - try { - lock.lock(); - for (SMTSolver solver : currentlyRunning) { - solver.interrupt(reason); - } - } finally { - lock.unlock(); - } - } - - public void addProblemSolver(SMTSolver solver) { - try { - problemSolverLock.lock(); - problemSolvers.add(solver); - } finally { - problemSolverLock.unlock(); - } - } - - public void addFinishedSolver(SMTSolver solver) { - try { - finishedSolverLock.lock(); - finishedSolvers.add(solver); - } finally { - finishedSolverLock.unlock(); - } - } - - public Collection getProblemSolvers() { - try { - problemSolverLock.lock(); - return new LinkedList<>(problemSolvers); // finally trumps return - } finally { - problemSolverLock.unlock(); - } - } - - public Collection getFinishedSolvers() { - try { - finishedSolverLock.lock(); - return new LinkedList<>(finishedSolvers); // finally trumps return - } finally { - finishedSolverLock.unlock(); - } - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverException.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncherException.java similarity index 89% rename from key.core/src/main/java/de/uka/ilkd/key/smt/SolverException.java rename to key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncherException.java index 10e0eb6e466..9499c98fdab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncherException.java @@ -8,11 +8,11 @@ /** * Encapsulates all exceptions that have occurred while executing the solvers. */ -public class SolverException extends RuntimeException { +public class SolverLauncherException extends RuntimeException { private static final long serialVersionUID = 1L; private final transient Collection solvers; - public SolverException(Collection solvers) { + public SolverLauncherException(Collection solvers) { super(); this.solvers = solvers; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverTimeout.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverTimeout.java index 1728ccf9722..a5c24cfb585 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverTimeout.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverTimeout.java @@ -7,24 +7,20 @@ import de.uka.ilkd.key.smt.SMTSolver.ReasonOfInterruption; +import org.jspecify.annotations.NonNull; + /** * The class controls the timer that checks for a solver whether it exceeds a pre-defined timeout. */ class SolverTimeout extends TimerTask { private final SMTSolver solver; - private final Session session; - public SolverTimeout(SMTSolver solver, Session session) { + public SolverTimeout(@NonNull SMTSolver solver) { this.solver = solver; - this.session = session; } @Override public void run() { - if (session != null) { - session.interruptSolver(solver, ReasonOfInterruption.Timeout); - } else { - solver.interrupt(ReasonOfInterruption.Timeout); - } + solver.interrupt(ReasonOfInterruption.Timeout); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractCESolverSocket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractCESolverSocket.java new file mode 100644 index 00000000000..fd63237eb02 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractCESolverSocket.java @@ -0,0 +1,114 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.smt.communication; + +import java.io.IOException; + +import de.uka.ilkd.key.smt.ModelExtractor; +import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.solvertypes.SolverType; + +import org.jspecify.annotations.NonNull; + +public abstract class AbstractCESolverSocket extends AbstractSolverSocket { + private ModelExtractor query; + + /** + * Creates a new solver socket with given solver name and ModelExtractor. + * + * @param solverType + * @param query the ModelExtractor used to extract a counterexample + */ + protected AbstractCESolverSocket(SolverType solverType, ModelExtractor query) { + super(solverType); + this.query = query; + } + + @Override + public SMTSolverResult.ThreeValuedTruth messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOException { + SolverCommunication sc = pipe.getSolverCommunication(); + if (msg.isBlank() || isFilteredMessage(msg)) { + return null; + } + + sc.addMessage(msg, SolverCommunication.MessageType.OUTPUT); + + if (isWarningMessage(msg)) { + handleWarningMessage(pipe, msg); + return null; + } + + if (isErrorMessage(msg)) { + handleErrorMessage(pipe, msg); + } + + return handleResultMessage(pipe, msg); + } + + @Override + protected SMTSolverResult.ThreeValuedTruth handleFalsifiableResultMessage(@NonNull Pipe pipe, + @NonNull String msg) throws IOException { + if (isFalsifiableResultMessage(msg)) { + pipe.getSolverCommunication().setState(WAIT_FOR_MODEL); + sendModelRequestMessages(pipe); + return null; + } + throw new IllegalStateException( + getName() + " encountered an error when parsing message: " + msg); + } + + @Override + protected SMTSolverResult.ThreeValuedTruth handleResultMessage(@NonNull Pipe pipe, + @NonNull String msg) throws IOException { + SolverCommunication sc = pipe.getSolverCommunication(); + switch (sc.getState()) { + case WAIT_FOR_RESULT -> { + if (isFalsifiableResultMessage(msg)) { + return handleFalsifiableResultMessage(pipe, msg); + } + return super.handleResultMessage(pipe, msg); + } + case WAIT_FOR_DETAILS -> { + return null; + } + // Currently we rely on the solver to terminate after receiving "(exit)". If this does + // not work in future, it may be that we have to forcibly close the pipe. + case WAIT_FOR_QUERY -> { + if (!isFilteredMessage(msg)) { + getQuery().messageIncoming(pipe, msg); + if (getQuery().getState() == ModelExtractor.FINISHED) { + return SMTSolverResult.ThreeValuedTruth.FALSIFIABLE; + } + } + return null; + } + case WAIT_FOR_MODEL -> { + if (isModelMessage(msg)) { + if (getQuery() != null && getQuery().getState() == ModelExtractor.DEFAULT) { + getQuery().getModel().setEmpty(false); + getQuery().start(pipe); + sc.setState(WAIT_FOR_QUERY); + } else { + sendExitMessages(pipe); + return SMTSolverResult.ThreeValuedTruth.FALSIFIABLE; + } + } + return null; + } + default -> throw new IllegalStateException("Unexpected value: " + sc.getState()); + } + } + + protected abstract boolean isModelMessage(String msg); + + protected abstract void sendModelRequestMessages(Pipe pipe) throws IOException; + + public ModelExtractor getQuery() { + return query; + } + + public void setQuery(ModelExtractor query) { + this.query = query; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractSolverSocket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractSolverSocket.java index d6ed1dfbb81..41d6ecacd57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractSolverSocket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/AbstractSolverSocket.java @@ -6,6 +6,7 @@ import java.io.IOException; import de.uka.ilkd.key.smt.ModelExtractor; +import de.uka.ilkd.key.smt.SMTSolverResult; import de.uka.ilkd.key.smt.solvertypes.SolverType; import org.jspecify.annotations.NonNull; @@ -40,32 +41,14 @@ public abstract class AbstractSolverSocket { protected static final int FINISH = 4; /** The name of the solver related to the socket. */ - private final String name; + protected final SolverType solverType; - /** The ModelExtractor that is to be used for CE generation (only used for CE socket). */ - private ModelExtractor query; - - /** - * Creates a new solver socket with given solver name and ModelExtractor. - * - * @param name the name of the solver in use - * @param query the ModelExtractor used to extract a counterexample - */ - protected AbstractSolverSocket(@NonNull String name, ModelExtractor query) { - this.name = name; - this.query = query; - } - - public ModelExtractor getQuery() { - return query; - } - - public void setQuery(ModelExtractor query) { - this.query = query; + protected AbstractSolverSocket(SolverType solverType) { + this.solverType = solverType; } protected String getName() { - return name; + return solverType.getName(); } /** @@ -75,8 +58,107 @@ protected String getName() { * @param msg the message as String * @throws IOException if an I/O error occurs */ - public abstract void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) - throws IOException; + public SMTSolverResult.ThreeValuedTruth messageIncoming(@NonNull Pipe pipe, @NonNull String msg) + throws IOException { + SolverCommunication sc = pipe.getSolverCommunication(); + if (msg.isBlank() || isFilteredMessage(msg)) { + return null; + } + + sc.addMessage(msg, SolverCommunication.MessageType.OUTPUT); + + if (isWarningMessage(msg)) { + handleWarningMessage(pipe, msg); + return null; + } + + if (isErrorMessage(msg)) { + handleErrorMessage(pipe, msg); + } + + if (pipe.getSolverCommunication().getState() == WAIT_FOR_RESULT) { + return handleResultMessage(pipe, msg); + } + return null; + } + + protected abstract boolean isValidResultMessage(@NonNull String msg); + + protected abstract boolean isFalsifiableResultMessage(@NonNull String msg); + + protected abstract boolean isUnknownResultMessage(@NonNull String msg); + + protected abstract boolean isFilteredMessage(String msg); + + protected abstract boolean isErrorMessage(String msg); + + protected abstract boolean isWarningMessage(String msg); + + + + protected abstract void sendValidResultMessages(Pipe pipe) throws IOException; + + protected abstract void sendFalsifiableResultMessages(Pipe pipe) throws IOException; + + protected abstract void sendUnknownResultMessages(Pipe pipe) throws IOException; + + protected abstract void sendExitMessages(Pipe pipe) throws IOException; + + protected void handleWarningMessage(@NonNull Pipe pipe, @NonNull String msg) + throws IOException { + pipe.getSolverCommunication().addMessage(msg, SolverCommunication.MessageType.ERROR); + } + + protected void handleErrorMessage(@NonNull Pipe pipe, @NonNull String msg) throws IOException { + pipe.getSolverCommunication().addMessage(msg, SolverCommunication.MessageType.ERROR); + throw new IOException(getName() + " encountered an error: " + msg); + } + + protected SMTSolverResult.ThreeValuedTruth handleResultMessage(@NonNull Pipe pipe, + @NonNull String msg) throws IOException { + if (isValidResultMessage(msg)) { + return handleValidResultMessage(pipe, msg); + } else if (isFalsifiableResultMessage(msg)) { + return handleFalsifiableResultMessage(pipe, msg); + } else if (isUnknownResultMessage(msg)) { + return handleUnknownResultMessage(pipe, msg); + } + throw new IllegalStateException( + getName() + " encountered an error when parsing message: " + msg); + } + + protected SMTSolverResult.ThreeValuedTruth handleValidResultMessage(@NonNull Pipe pipe, + @NonNull String msg) throws IOException { + if (isValidResultMessage(msg)) { + pipe.getSolverCommunication().setState(FINISH); + sendValidResultMessages(pipe); + return SMTSolverResult.ThreeValuedTruth.VALID; + } + throw new IllegalStateException( + getName() + " encountered an error when parsing message: " + msg); + } + + protected SMTSolverResult.ThreeValuedTruth handleFalsifiableResultMessage(@NonNull Pipe pipe, + @NonNull String msg) throws IOException { + if (isFalsifiableResultMessage(msg)) { + pipe.getSolverCommunication().setState(FINISH); + sendFalsifiableResultMessages(pipe); + return SMTSolverResult.ThreeValuedTruth.FALSIFIABLE; + } + throw new IllegalStateException( + getName() + " encountered an error when parsing message: " + msg); + } + + protected SMTSolverResult.ThreeValuedTruth handleUnknownResultMessage(@NonNull Pipe pipe, + @NonNull String msg) throws IOException { + if (isUnknownResultMessage(msg)) { + pipe.getSolverCommunication().setState(FINISH); + sendUnknownResultMessages(pipe); + return SMTSolverResult.ThreeValuedTruth.UNKNOWN; + } + throw new IllegalStateException( + getName() + " encountered an error when parsing message: " + msg); + } /** * Modify an SMT problem String in some way (e.g. prepend some SMT commands). By default, the diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java index a459b33378e..3eea35bf6f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java @@ -5,60 +5,69 @@ import java.io.IOException; -import de.uka.ilkd.key.smt.ModelExtractor; -import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.solvertypes.SolverType; import org.jspecify.annotations.NonNull; public class CVC4Socket extends AbstractSolverSocket { - public CVC4Socket(String name, ModelExtractor query) { - super(name, query); + public CVC4Socket(SolverType solverType) { + super(solverType); } @Override - public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOException { - SolverCommunication sc = pipe.getSolverCommunication(); - if ("".equals(msg.trim())) { - return; - } - - // used only to steer the interaction with the solver and thus filtered out currently - if (!msg.contains("success")) { - sc.addMessage(msg, SolverCommunication.MessageType.OUTPUT); - } - - if (msg.contains("error") || msg.contains("Error")) { - sc.addMessage(msg, SolverCommunication.MessageType.ERROR); - throw new IOException("Error while executing " + getName() + ": " + msg); - } - - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - if (sc.getState() == WAIT_FOR_RESULT) { - msg = msg.trim(); - if (msg.equals("unsat")) { - sc.setFinalResult(SMTSolverResult.createValidResult(getName())); - sc.setState(FINISH); - pipe.sendMessage("(exit)"); - // pipe.close(); - } else if (msg.equals("sat")) { - sc.setFinalResult(SMTSolverResult.createInvalidResult(getName())); - sc.setState(FINISH); - pipe.sendMessage("(exit)"); - // pipe.close(); - } else if (msg.equals("unknown")) { - sc.setFinalResult(SMTSolverResult.createUnknownResult(getName())); - sc.setState(FINISH); - pipe.sendMessage("(exit)"); - // pipe.close(); - } - } + protected boolean isValidResultMessage(@NonNull String msg) { + return msg.equals("unsat"); + } + + @Override + protected boolean isFalsifiableResultMessage(@NonNull String msg) { + return msg.equals("sat"); + } + + @Override + protected boolean isUnknownResultMessage(@NonNull String msg) { + return msg.equals("unknown"); + } + + @Override + protected boolean isFilteredMessage(String msg) { + return msg.contains("success"); + } + + @Override + protected boolean isErrorMessage(String msg) { + return msg.contains("error") || msg.contains("Error"); + } + + @Override + protected boolean isWarningMessage(String msg) { + return false; + } + + @Override + protected void sendValidResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendFalsifiableResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendUnknownResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendExitMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); } @Override public AbstractSolverSocket copy() { - return new CVC4Socket(getName(), getQuery()); + return new CVC4Socket(solverType); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java index fe50d3cf0d5..2208c7b6c81 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java @@ -5,8 +5,7 @@ import java.io.IOException; -import de.uka.ilkd.key.smt.ModelExtractor; -import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.solvertypes.SolverType; import org.jspecify.annotations.NonNull; @@ -17,57 +16,64 @@ public class CVC5Socket extends AbstractSolverSocket { /** * Create a new CVC5Socket. - * - * @param name the socket's name (usually "CVC5", but other solvers might also use it). - * @param query the ModelExtractor for model interpretation (currently not used by this socket) */ - public CVC5Socket(String name, ModelExtractor query) { - super(name, query); + public CVC5Socket(SolverType solverType) { + super(solverType); } @Override - public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOException { - SolverCommunication sc = pipe.getSolverCommunication(); - if ("".equals(msg.trim())) { - return; - } - - // used only to steer the interaction with the solver and thus filtered out currently - if (!msg.contains("success")) { - sc.addMessage(msg, SolverCommunication.MessageType.OUTPUT); - } - - if (msg.contains("error") || msg.contains("Error")) { - sc.addMessage(msg, SolverCommunication.MessageType.ERROR); - throw new IOException("Error while executing " + getName() + ": " + msg); - } - - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - if (sc.getState() == WAIT_FOR_RESULT) { - if (msg.contains("unsat")) { - sc.setFinalResult(SMTSolverResult.createValidResult(getName())); - sc.setState(FINISH); - pipe.sendMessage("(get-unsat-core)"); - pipe.sendMessage("(exit)"); - // pipe.close(); - } else if (msg.contains("sat")) { - sc.setFinalResult(SMTSolverResult.createInvalidResult(getName())); - sc.setState(FINISH); - pipe.sendMessage("(exit)"); - // pipe.close(); - } else if (msg.contains("unknown")) { - sc.setFinalResult(SMTSolverResult.createUnknownResult(getName())); - sc.setState(FINISH); - pipe.sendMessage("(exit)"); - // pipe.close(); - } - } + protected boolean isValidResultMessage(@NonNull String msg) { + return msg.equals("unsat"); + } + + @Override + protected boolean isFalsifiableResultMessage(@NonNull String msg) { + return msg.equals("sat"); + } + + @Override + protected boolean isUnknownResultMessage(@NonNull String msg) { + return msg.equals("unknown"); + } + + @Override + protected boolean isFilteredMessage(String msg) { + return msg.contains("success"); + } + + @Override + protected boolean isErrorMessage(String msg) { + return msg.contains("error") || msg.contains("Error"); + } + + @Override + protected boolean isWarningMessage(String msg) { + return false; + } + + @Override + protected void sendValidResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendFalsifiableResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendUnknownResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendExitMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)"); } @Override public AbstractSolverSocket copy() { - return new CVC5Socket(getName(), getQuery()); + return new CVC5Socket(solverType); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/SolverCommunication.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/SolverCommunication.java index 25b43d85694..b2e9840b54c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/SolverCommunication.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/SolverCommunication.java @@ -8,7 +8,6 @@ import java.util.List; import java.util.stream.Collectors; -import de.uka.ilkd.key.smt.SMTSolverResult; /** * Stores the communication between KeY and an external solver: Contains a list that stores the @@ -25,9 +24,6 @@ public class SolverCommunication { /** All messages (input/output/error) sent between KeY and SMT solver. */ private final List messages = Collections.synchronizedList(new LinkedList<>()); - /** The final result of the associated solver (unknown if not yet set). */ - private SMTSolverResult finalResult = SMTSolverResult.NO_IDEA; - /** The current state of the communication. The states are defined by the solver sockets. */ private int state = 0; @@ -101,14 +97,6 @@ void addMessage(String message, MessageType type) { messages.add(new Message(message, type)); } - public SMTSolverResult getFinalResult() { - return finalResult; - } - - void setFinalResult(SMTSolverResult finalResult) { - this.finalResult = finalResult; - } - public int getState() { return state; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java index 648c4968109..9692f9e8291 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java @@ -6,80 +6,84 @@ import java.io.IOException; import de.uka.ilkd.key.smt.ModelExtractor; -import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.solvertypes.SolverType; import org.jspecify.annotations.NonNull; -public class Z3CESocket extends AbstractSolverSocket { +public class Z3CESocket extends AbstractCESolverSocket { - public Z3CESocket(String name, ModelExtractor query) { - super(name, query); + public Z3CESocket(SolverType solverType, ModelExtractor query) { + super(solverType, query); } @Override - public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOException { - SolverCommunication sc = pipe.getSolverCommunication(); - - if (msg.startsWith("(error")) { - sc.addMessage(msg, SolverCommunication.MessageType.ERROR); - if (msg.contains("WARNING:")) { - return; - } - throw new IOException("Error while executing " + getName() + ": " + msg); - } - // These two messages are only used to steer the interaction with the solver and are thus - // currently filtered out to avoid cluttering up the output. - if (!msg.equals("success") && !msg.equals("endmodel")) { - sc.addMessage(msg, SolverCommunication.MessageType.OUTPUT); - } - - switch (sc.getState()) { - case WAIT_FOR_RESULT -> { - if (msg.equals("unsat")) { - sc.setFinalResult(SMTSolverResult.createValidResult(getName())); - pipe.sendMessage("(exit)"); - sc.setState(WAIT_FOR_DETAILS); - } - if (msg.equals("sat")) { - sc.setFinalResult(SMTSolverResult.createInvalidResult(getName())); - pipe.sendMessage("(get-model)"); - pipe.sendMessage("(echo \"endmodel\")"); - sc.setState(WAIT_FOR_MODEL); - } - if (msg.equals("unknown")) { - sc.setFinalResult(SMTSolverResult.createUnknownResult(getName())); - sc.setState(WAIT_FOR_DETAILS); - pipe.sendMessage("(exit)"); - } - } - case WAIT_FOR_DETAILS -> { - } - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - case WAIT_FOR_QUERY -> { - if (!msg.equals("success")) { - getQuery().messageIncoming(pipe, msg); - } - } - case WAIT_FOR_MODEL -> { - if (msg.equals("endmodel")) { - if (getQuery() != null && getQuery().getState() == ModelExtractor.DEFAULT) { - getQuery().getModel().setEmpty(false); - getQuery().start(pipe); - sc.setState(WAIT_FOR_QUERY); - } else { - pipe.sendMessage("(exit)\n"); - sc.setState(WAIT_FOR_DETAILS); - } - } - } - default -> throw new IllegalStateException("Unexpected value: " + sc.getState()); - } + protected boolean isValidResultMessage(@NonNull String msg) { + return msg.equals("unsat"); + } + + @Override + protected boolean isFalsifiableResultMessage(@NonNull String msg) { + return msg.equals("sat"); + } + + @Override + protected boolean isUnknownResultMessage(@NonNull String msg) { + return msg.equals("unknown"); + } + + @Override + protected boolean isFilteredMessage(String msg) { + return msg.equals("success"); + } + + @Override + protected boolean isErrorMessage(String msg) { + return msg.startsWith("(error") && !msg.contains("WARNING:"); + } + + @Override + protected boolean isWarningMessage(String msg) { + return msg.startsWith("(error") && msg.contains("WARNING:"); + } + + @Override + protected void sendValidResultMessages(Pipe pipe) throws IOException { + // TODO: proof production is currently completely disabled, since it does not work + // with the legacy Z3 translation (proof-production not enabled) and also not + // really needed + // pipe.sendMessage("(get-proof)"); + pipe.sendMessage("(get-unsat-core)"); + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendFalsifiableResultMessages(Pipe pipe) throws IOException { + } + + @Override + protected void sendUnknownResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)\n"); + } + + @Override + protected boolean isModelMessage(String msg) { + return msg.equals("endmodel"); + } + + @Override + protected void sendModelRequestMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(get-model)"); + pipe.sendMessage("(echo \"endmodel\")"); + } + + @Override + protected void sendExitMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)\n"); } @Override public AbstractSolverSocket copy() { - return new Z3CESocket(getName(), getQuery()); + return new Z3CESocket(solverType, getQuery()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java index 1ff6deac753..224a627f7c8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java @@ -5,72 +5,75 @@ import java.io.IOException; -import de.uka.ilkd.key.smt.ModelExtractor; -import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.solvertypes.SolverType; import org.jspecify.annotations.NonNull; public class Z3Socket extends AbstractSolverSocket { - public Z3Socket(String name, ModelExtractor query) { - super(name, query); + public Z3Socket(SolverType solverType) { + super(solverType); } @Override - public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOException { - SolverCommunication sc = pipe.getSolverCommunication(); - if (msg.startsWith("(error")) { - sc.addMessage(msg, SolverCommunication.MessageType.ERROR); - if (msg.contains("WARNING:")) { - return; - } - throw new IOException("Error while executing " + getName() + ": " + msg); - } - - // used only to steer the interaction with the solver and thus filtered out currently - if (!msg.equals("success")) { - sc.addMessage(msg, SolverCommunication.MessageType.OUTPUT); - } - - switch (sc.getState()) { - case WAIT_FOR_RESULT -> { - if (msg.equals("unsat")) { - sc.setFinalResult(SMTSolverResult.createValidResult(getName())); - // TODO: proof production is currently completely disabled, since it does not work - // with the legacy Z3 translation (proof-production not enabled) and also not - // really needed - // pipe.sendMessage("(get-proof)"); - pipe.sendMessage("(get-unsat-core)"); - pipe.sendMessage("(exit)"); - sc.setState(WAIT_FOR_DETAILS); - } - if (msg.equals("sat")) { - sc.setFinalResult(SMTSolverResult.createInvalidResult(getName())); - pipe.sendMessage("(get-model)"); - pipe.sendMessage("(exit)"); - sc.setState(WAIT_FOR_DETAILS); - - } - if (msg.equals("unknown")) { - sc.setFinalResult(SMTSolverResult.createUnknownResult(getName())); - pipe.sendMessage("(exit)\n"); - sc.setState(WAIT_FOR_DETAILS); - } - } - case WAIT_FOR_DETAILS -> { - } - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - // if (msg.equals("success")) { - // pipe.sendMessage("(exit)"); - // pipe.close(); - // } - } + protected boolean isValidResultMessage(@NonNull String msg) { + return msg.equals("unsat"); + } + + @Override + protected boolean isFalsifiableResultMessage(@NonNull String msg) { + return msg.equals("sat"); + } + + @Override + protected boolean isUnknownResultMessage(@NonNull String msg) { + return msg.equals("unknown"); + } + + @Override + protected boolean isFilteredMessage(String msg) { + return msg.equals("success"); + } + + @Override + protected boolean isErrorMessage(String msg) { + return msg.startsWith("(error") && !msg.contains("WARNING:"); + } + + @Override + protected boolean isWarningMessage(String msg) { + return msg.contains("WARNING:"); + } + + @Override + protected void sendValidResultMessages(Pipe pipe) throws IOException { + // TODO: proof production is currently completely disabled, since it does not work + // with the legacy Z3 translation (proof-production not enabled) and also not + // really needed + // pipe.sendMessage("(get-proof)"); + pipe.sendMessage("(get-unsat-core)"); + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendFalsifiableResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(get-model)"); + pipe.sendMessage("(exit)"); + } + + @Override + protected void sendUnknownResultMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)\n"); + } + + @Override + protected void sendExitMessages(Pipe pipe) throws IOException { + pipe.sendMessage("(exit)\n"); } @Override public AbstractSolverSocket copy() { - return new Z3Socket(getName(), getQuery()); + return new Z3Socket(solverType); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverType.java b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverType.java index d7758fd4298..d26fcfb9d91 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverType.java @@ -42,7 +42,8 @@ public interface SolverType { * {@link SMTObjTranslator}) * @return a concrete solver process of the type at hand */ - SMTSolver createSolver(SMTProblem problem, SolverListener listener, Services services); + SMTSolver createSolver(SMTProblem problem, SolverListener listener, Services services, + SMTSettings smtSettings, long timeout); /** * @return the name of the solver. diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java index c1a1a7d126c..d7ab1d86680 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.smt.*; +import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket; import de.uka.ilkd.key.smt.communication.AbstractSolverSocket; import de.uka.ilkd.key.smt.communication.Z3Socket; import de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator; @@ -230,15 +231,21 @@ public SolverTypeImplementation(String name, String info, String defaultParams, private AbstractSolverSocket makeSocket() { try { - return (AbstractSolverSocket) solverSocketClass - .getDeclaredConstructor(String.class, ModelExtractor.class) - .newInstance(name, null); + if (AbstractCESolverSocket.class.isAssignableFrom(solverSocketClass)) { + return (AbstractSolverSocket) solverSocketClass + .getDeclaredConstructor(SolverType.class, ModelExtractor.class) + .newInstance(this, null); + } else { + return (AbstractSolverSocket) solverSocketClass + .getDeclaredConstructor(SolverType.class) + .newInstance(this); + } } catch (NoSuchMethodException | IllegalArgumentException | ClassCastException | InstantiationException | IllegalAccessException | InvocationTargetException e) { LOGGER.warn(String.format( "Using default Z3Socket for solver communication due to exception:%s%s", System.lineSeparator(), e.getMessage())); - return new Z3Socket(name, null); + return new Z3Socket(this); } } @@ -332,8 +339,13 @@ private static boolean osIsLinux() { } @Override - public SMTSolver createSolver(SMTProblem problem, SolverListener listener, Services services) { - return new SMTSolverImplementation(problem, listener, services, this); + public SMTSolver createSolver(SMTProblem problem, SolverListener listener, Services services, + SMTSettings smtSettings, long timeout) { + if (timeout > 0) + return new SMTSolverImplementation(problem, listener, services, smtSettings, this, + timeout); + return new SMTSolverImplementation(problem, listener, services, smtSettings, this, + defaultTimeout); } @Override @@ -494,9 +506,7 @@ public boolean supportHasBeenChecked() { @Override public @NonNull AbstractSolverSocket getSocket(ModelExtractor query) { - AbstractSolverSocket socket = solverSocket.copy(); - socket.setQuery(query); - return socket; + return solverSocket.copy(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java index 0e984f23dbc..acdfc5bcd68 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java @@ -10,8 +10,8 @@ import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.sourceview.TextLineNumber; import de.uka.ilkd.key.smt.SMTSolver; +import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket; import de.uka.ilkd.key.smt.model.Model; -import de.uka.ilkd.key.smt.solvertypes.SolverTypes; /** @@ -85,15 +85,11 @@ public InformationWindow(Dialog parent, SMTSolver solver, Collection