diff --git a/dbgpc/src/main/java/com/fujitsu/vdmjc/config/Config.java b/dbgpc/src/main/java/com/fujitsu/vdmjc/config/Config.java index c9b69ac68..b98692a3c 100644 --- a/dbgpc/src/main/java/com/fujitsu/vdmjc/config/Config.java +++ b/dbgpc/src/main/java/com/fujitsu/vdmjc/config/Config.java @@ -123,7 +123,6 @@ private static boolean get(java.util.Properties local, String key, boolean def) return value; } - @SuppressWarnings("unused") private static String get(java.util.Properties local, String key, String def) { String value = System.getProperty(key); diff --git a/lsp/src/main/java/dap/AsyncExecutor.java b/lsp/src/main/java/dap/AsyncExecutor.java index a36d7f1db..4d51014df 100644 --- a/lsp/src/main/java/dap/AsyncExecutor.java +++ b/lsp/src/main/java/dap/AsyncExecutor.java @@ -39,8 +39,6 @@ public abstract class AsyncExecutor extends CancellableThread protected final DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); protected final DAPRequest request; - protected static String running = null; - public AsyncExecutor(String id, DAPRequest request) { super(id); @@ -115,9 +113,4 @@ public void setCancelled() Breakpoint.setExecInterrupt(Breakpoint.TERMINATE); Diag.info("Set the exec interrupt value to TERMINATE"); } - - public static String currentlyRunning() - { - return running; - } } diff --git a/lsp/src/main/java/dap/DAPDispatcher.java b/lsp/src/main/java/dap/DAPDispatcher.java index 7a511cdb2..f0dee8193 100644 --- a/lsp/src/main/java/dap/DAPDispatcher.java +++ b/lsp/src/main/java/dap/DAPDispatcher.java @@ -30,9 +30,26 @@ public class DAPDispatcher { + private static DAPDispatcher INSTANCE = null; + private Map handlers = new HashMap(); private DAPHandler unknownHandler = null; + private DAPDispatcher() + { + // Nothing to do + } + + public static DAPDispatcher getInstance() + { + if (INSTANCE == null) + { + INSTANCE = new DAPDispatcher(); + } + + return INSTANCE; + } + public void register(DAPHandler handler, String... methods) { if (methods.length == 0) diff --git a/lsp/src/main/java/dap/DAPServer.java b/lsp/src/main/java/dap/DAPServer.java index ae8663557..e48fcf37e 100644 --- a/lsp/src/main/java/dap/DAPServer.java +++ b/lsp/src/main/java/dap/DAPServer.java @@ -71,7 +71,7 @@ public static DAPServer getInstance() private DAPDispatcher getDispatcher() throws IOException { - DAPDispatcher dispatcher = new DAPDispatcher(); + DAPDispatcher dispatcher = DAPDispatcher.getInstance(); dispatcher.register(new InitializeHandler(), "initialize"); dispatcher.register(new LaunchHandler(), "launch"); diff --git a/lsp/src/main/java/dap/handlers/DisconnectHandler.java b/lsp/src/main/java/dap/handlers/DisconnectHandler.java index d1e1848c0..6da6a59c9 100644 --- a/lsp/src/main/java/dap/handlers/DisconnectHandler.java +++ b/lsp/src/main/java/dap/handlers/DisconnectHandler.java @@ -29,6 +29,7 @@ import dap.DAPHandler; import dap.DAPMessageList; import dap.DAPRequest; +import dap.DAPServer; import json.JSONObject; import lsp.CancellableThread; import lsp.Utils; @@ -65,7 +66,9 @@ public DAPMessageList run(DAPRequest request) throws IOException { JSONObject arguments = request.get("arguments"); Boolean terminateDebuggee = Utils.getBoolean(arguments, "terminateDebuggee"); - return manager.dapDisconnect(request, terminateDebuggee); + DAPMessageList result = manager.dapDisconnect(request, terminateDebuggee); + DAPServer.getInstance().setRunning(false); + return result; } } } diff --git a/lsp/src/main/java/dap/handlers/SourceHandler.java b/lsp/src/main/java/dap/handlers/SourceHandler.java index bd26c0f5e..34a0a7bd9 100644 --- a/lsp/src/main/java/dap/handlers/SourceHandler.java +++ b/lsp/src/main/java/dap/handlers/SourceHandler.java @@ -26,11 +26,11 @@ import java.io.IOException; -import dap.AsyncExecutor; import dap.DAPHandler; import dap.DAPMessageList; import dap.DAPRequest; import json.JSONObject; +import lsp.CancellableThread; public class SourceHandler extends DAPHandler { @@ -50,7 +50,7 @@ public DAPMessageList run(DAPRequest request) throws IOException switch (reference.intValue()) { case 0: // Executing command - result = AsyncExecutor.currentlyRunning(); + result = CancellableThread.currentlyRunning(); break; default: diff --git a/lsp/src/main/java/dap/handlers/TerminateHandler.java b/lsp/src/main/java/dap/handlers/TerminateHandler.java index 1b837bf9e..9aaf6ae72 100644 --- a/lsp/src/main/java/dap/handlers/TerminateHandler.java +++ b/lsp/src/main/java/dap/handlers/TerminateHandler.java @@ -29,7 +29,6 @@ import dap.DAPHandler; import dap.DAPMessageList; import dap.DAPRequest; -import dap.DAPServer; import json.JSONObject; import lsp.CancellableThread; import vdmj.DAPDebugReader; @@ -67,7 +66,6 @@ public DAPMessageList run(DAPRequest request) throws IOException JSONObject arguments = request.get("arguments"); Boolean restart = arguments.get("restart"); DAPMessageList result = manager.dapTerminate(request, restart); - DAPServer.getInstance().setRunning(false); return result; } } diff --git a/lsp/src/main/java/lsp/CancellableThread.java b/lsp/src/main/java/lsp/CancellableThread.java index 5ea5475c6..11190c5f7 100644 --- a/lsp/src/main/java/lsp/CancellableThread.java +++ b/lsp/src/main/java/lsp/CancellableThread.java @@ -34,7 +34,8 @@ abstract public class CancellableThread extends Thread private static final Map active = new HashMap(); protected final Object myId; protected boolean cancelled = false; - + protected static String running = null; + public CancellableThread(Object myId) { this.myId = myId; @@ -87,6 +88,27 @@ public static void cancelAll() } } + public static void joinId(Object id) + { + CancellableThread thread = active.get(id); + + if (thread == null) + { + Diag.error("Cannot join thread id %s", id.toString()); + } + else + { + try + { + thread.join(); + } + catch (InterruptedException e) + { + // ignore + } + } + } + public void setCancelled() { cancelled = true; @@ -99,4 +121,9 @@ public static CancellableThread find(Object id) } abstract protected void body(); + + public static String currentlyRunning() + { + return running; + } } diff --git a/lsp/src/main/java/lsp/LSPServer.java b/lsp/src/main/java/lsp/LSPServer.java index 6214962f7..8e4632782 100644 --- a/lsp/src/main/java/lsp/LSPServer.java +++ b/lsp/src/main/java/lsp/LSPServer.java @@ -96,7 +96,7 @@ public static LSPServer getInstance() private RPCDispatcher getDispatcher() throws IOException { - RPCDispatcher dispatcher = new RPCDispatcher(); + RPCDispatcher dispatcher = RPCDispatcher.getInstance(); dispatcher.register(new InitializeHandler(), "initialize", "initialized", "client/registerCapability"); dispatcher.register(new ShutdownHandler(), "shutdown"); diff --git a/lsp/src/main/java/rpc/RPCDispatcher.java b/lsp/src/main/java/rpc/RPCDispatcher.java index 82b4f86ac..327509131 100644 --- a/lsp/src/main/java/rpc/RPCDispatcher.java +++ b/lsp/src/main/java/rpc/RPCDispatcher.java @@ -30,9 +30,26 @@ public class RPCDispatcher { + private static RPCDispatcher INSTANCE = null; + private Map handlers = new HashMap(); private RPCHandler unknownHandler = null; + private RPCDispatcher() + { + // Nothing to do + } + + public static RPCDispatcher getInstance() + { + if (INSTANCE == null) + { + INSTANCE = new RPCDispatcher(); + } + + return INSTANCE; + } + public void register(RPCHandler handler, String... methods) { if (methods.length == 0) diff --git a/lsp/src/main/java/vdmj/commands/QuitCommand.java b/lsp/src/main/java/vdmj/commands/QuitCommand.java index 570753769..4731739c2 100644 --- a/lsp/src/main/java/vdmj/commands/QuitCommand.java +++ b/lsp/src/main/java/vdmj/commands/QuitCommand.java @@ -24,7 +24,6 @@ package vdmj.commands; -import dap.AsyncExecutor; import dap.DAPMessageList; import dap.DAPRequest; import dap.DAPServer; @@ -51,7 +50,7 @@ public DAPMessageList run(DAPRequest request) { DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); - if (AsyncExecutor.currentlyRunning() != null) + if (CancellableThread.currentlyRunning() != null) { CancellableThread.cancelAll(); manager.stopDebugReader(); diff --git a/lsp/src/main/java/workspace/DAPWorkspaceManager.java b/lsp/src/main/java/workspace/DAPWorkspaceManager.java index c856102dc..d67d58296 100644 --- a/lsp/src/main/java/workspace/DAPWorkspaceManager.java +++ b/lsp/src/main/java/workspace/DAPWorkspaceManager.java @@ -64,7 +64,6 @@ import com.fujitsu.vdmj.scheduler.SchedulableThread; import com.fujitsu.vdmj.tc.lex.TCNameToken; -import dap.AsyncExecutor; import dap.DAPInitializeResponse; import dap.DAPMessageList; import dap.DAPRequest; @@ -74,6 +73,7 @@ import dap.RemoteControlExecutor; import json.JSONArray; import json.JSONObject; +import lsp.CancellableThread; import lsp.Utils; import vdmj.DAPDebugReader; import vdmj.commands.AnalysisCommand; @@ -752,9 +752,9 @@ public DAPMessageList dapEvaluate(DAPRequest request, String expression, String AnalysisCommand command = AnalysisCommand.parse(expression); - if (command.notWhenRunning() && AsyncExecutor.currentlyRunning() != null) + if (command.notWhenRunning() && CancellableThread.currentlyRunning() != null) { - return new DAPMessageList(request, false, "Still running " + AsyncExecutor.currentlyRunning(), null); + return new DAPMessageList(request, false, "Still running " + CancellableThread.currentlyRunning(), null); } // If we are about to evaluate something, check that we can execute. diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index 60b929e5e..53eb124fb 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,14 +25,9 @@ package workspace.plugins; import java.io.File; -import java.util.List; -import java.util.Vector; import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.mapper.Mappable; -import com.fujitsu.vdmj.messages.VDMMessage; -import com.fujitsu.vdmj.messages.VDMWarning; -import com.fujitsu.vdmj.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -43,6 +38,7 @@ import rpc.RPCRequest; import workspace.Diag; import workspace.EventListener; +import workspace.MessageHub; import workspace.events.CheckCompleteEvent; import workspace.events.CheckPrepareEvent; import workspace.events.LSPEvent; @@ -140,9 +136,9 @@ protected void preCheck(CheckPrepareEvent event) abstract public ProofObligationList getProofObligations(); - abstract protected JSONObject getCexLaunch(ProofObligation po); + abstract public JSONObject getCexLaunch(ProofObligation po); - abstract protected JSONObject getWitnessLaunch(ProofObligation po); + abstract public JSONObject getWitnessLaunch(ProofObligation po); protected JSONArray splitPO(String value) { @@ -159,13 +155,9 @@ protected JSONArray splitPO(String value) public RPCMessageList getJSONObligations(RPCRequest request, File file) { - ProofObligationList poGeneratedList = getProofObligations(); JSONArray poList = new JSONArray(); - messagehub.clearPluginMessages(this); - List messages = new Vector(); - - for (ProofObligation po: poGeneratedList) + for (ProofObligation po: getProofObligations()) { if (file != null) { @@ -202,66 +194,13 @@ else if (file.isDirectory()) "source", splitPO(po.value), "status", po.status.toString()); - if (po.counterexample != null) - { - JSONObject cexample = new JSONObject(); - cexample.put("variables", Utils.contextToJSON(po.counterexample)); - JSONObject launch = getCexLaunch(po); - - if (launch != null) - { - cexample.put("launch", launch); - } - - json.put("counterexample", cexample); - - StringBuilder sb = new StringBuilder(); - sb.append("PO #"); - sb.append(po.number); - sb.append(" counterexample: "); - sb.append(po.counterexample.toStringLine()); - messages.add(new VDMWarning(9000, sb.toString(), po.location)); - } - - if (po.status == POStatus.FAILED) - { - if (po.message != null) // Add failed messages as a warning too - { - messages.add(new VDMWarning(9000, po.message, po.location)); - } - } - - if (po.witness != null) - { - JSONObject witness = new JSONObject(); - witness.put("variables", Utils.contextToJSON(po.witness)); - JSONObject launch = getWitnessLaunch(po); - - if (launch != null) - { - witness.put("launch", launch); - } - - json.put("witness", witness); - } - - if (po.provedBy != null) - { - json.put("provedBy", po.provedBy); - } - - if (po.message != null) - { - json.put("message", po.message); - } - poList.add(json); } + + + RPCMessageList response = new RPCMessageList(request, poList); + response.addAll(MessageHub.getInstance().getDiagnosticResponses()); - messagehub.addPluginMessages(this, messages); - RPCMessageList result = new RPCMessageList(request, poList); - result.addAll(messagehub.getDiagnosticResponses()); - - return result; + return response; } } diff --git a/lsp/src/main/java/workspace/plugins/POPluginPR.java b/lsp/src/main/java/workspace/plugins/POPluginPR.java index 1fb2eb368..536227fe9 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginPR.java +++ b/lsp/src/main/java/workspace/plugins/POPluginPR.java @@ -72,6 +72,7 @@ public ProofObligationList getProofObligations() { if (obligationList == null) { + messagehub.clearPluginMessages(this); POAnnotation.init(); obligationList = poClassList.getProofObligations(); POAnnotation.close(); @@ -82,13 +83,13 @@ public ProofObligationList getProofObligations() } @Override - protected JSONObject getCexLaunch(ProofObligation po) + public JSONObject getCexLaunch(ProofObligation po) { return null; // Needs to create new object? } @Override - protected JSONObject getWitnessLaunch(ProofObligation po) + public JSONObject getWitnessLaunch(ProofObligation po) { return null; // Needs to create new object? } diff --git a/lsp/src/main/java/workspace/plugins/POPluginSL.java b/lsp/src/main/java/workspace/plugins/POPluginSL.java index 8a4df8c9c..2058b6306 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginSL.java +++ b/lsp/src/main/java/workspace/plugins/POPluginSL.java @@ -72,6 +72,7 @@ public ProofObligationList getProofObligations() { if (obligationList == null) { + messagehub.clearPluginMessages(this); POAnnotation.init(); obligationList = poModuleList.getProofObligations(); POAnnotation.close(); @@ -82,7 +83,7 @@ public ProofObligationList getProofObligations() } @Override - protected JSONObject getCexLaunch(ProofObligation po) + public JSONObject getCexLaunch(ProofObligation po) { String launch = po.getCexLaunch(); @@ -102,7 +103,7 @@ protected JSONObject getCexLaunch(ProofObligation po) } @Override - protected JSONObject getWitnessLaunch(ProofObligation po) + public JSONObject getWitnessLaunch(ProofObligation po) { String launch = po.getWitnessLaunch(); diff --git a/lsp/src/test/java/rpc/RPCTest.java b/lsp/src/test/java/rpc/RPCTest.java index 43d79e929..1849905b8 100644 --- a/lsp/src/test/java/rpc/RPCTest.java +++ b/lsp/src/test/java/rpc/RPCTest.java @@ -47,7 +47,7 @@ public void test1() throws IOException StringReader ireader = new StringReader(json); JSONReader reader = new JSONReader(ireader); JSONObject map = reader.readObject(); - RPCDispatcher d = new RPCDispatcher(); + RPCDispatcher d = RPCDispatcher.getInstance(); d.register(new RPCHandler() { @@ -84,7 +84,7 @@ public void test2() throws IOException StringReader ireader = new StringReader(json); JSONReader reader = new JSONReader(ireader); JSONObject map = reader.readObject(); - RPCDispatcher d = new RPCDispatcher(); + RPCDispatcher d = RPCDispatcher.getInstance(); d.register(new RPCHandler() { @@ -121,7 +121,7 @@ public void testUnknownMethod() throws IOException StringReader ireader = new StringReader(json); JSONReader reader = new JSONReader(ireader); JSONObject map = reader.readObject(); - RPCDispatcher d = new RPCDispatcher(); + RPCDispatcher d = RPCDispatcher.getInstance(); RPCMessageList responses = d.dispatch(RPCRequest.create(map)); StringWriter out = new StringWriter(); JSONWriter writer = new JSONWriter(new PrintWriter(out)); diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index bbdf524a0..91fa512cf 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -34,6 +34,7 @@ import static quickcheck.commands.QCConsole.verboseln; import java.lang.reflect.Constructor; +import java.lang.reflect.InvocationTargetException; import java.util.HashMap; import java.util.Iterator; import java.util.List; @@ -105,7 +106,7 @@ public void resetErrors() errorCount = 0; } - public void loadStrategies(List argv) + public void loadStrategies(List argv) { strategies = new Vector(); disabled = new Vector(); @@ -124,7 +125,7 @@ public void loadStrategies(List argv) Class clazz = Class.forName(classname); Constructor ctor = clazz.getDeclaredConstructor(List.class); int argvSize = argv.size(); - QCStrategy instance = (QCStrategy) ctor.newInstance((Object)argv); + QCStrategy instance = (QCStrategy) ctor.newInstance(argv); if (instance.hasErrors()) { @@ -139,7 +140,7 @@ else if ((names.isEmpty() && instance.useByDefault()) || names.contains(instance { disabled.add(instance); - if (argvSize != argv.size()) + if (argv != null && argvSize != argv.size()) { // Constructor took some arguments errorln("The " + instance.getName() + " strategy is not enabled. Add -s " + instance.getName()); @@ -157,6 +158,11 @@ else if ((names.isEmpty() && instance.useByDefault()) || names.contains(instance errorln("Strategy " + classname + " must implement ctor(List argv)"); errorCount++; } + catch (InvocationTargetException e) + { + errorln("Strategy " + classname + ": " + e.getTargetException()); + errorCount++; + } catch (Throwable th) { errorln("Strategy " + classname + ": " + th.toString()); @@ -670,29 +676,52 @@ else if (globals.hasMaybe() && execCompleted) } } - private List strategyNames(List arglist) + private List strategyNames(List arglist) { List names = new Vector(); - Iterator iter = arglist.iterator(); - while (iter.hasNext()) + if (arglist != null && !arglist.isEmpty()) { - String arg = iter.next(); - - if (arg.equals("-s")) + if (arglist.get(0) instanceof String) { - iter.remove(); + @SuppressWarnings("unchecked") + Iterator iter = (Iterator) arglist.iterator(); - if (iter.hasNext()) + while (iter.hasNext()) { - arg = iter.next(); - iter.remove(); - names.add(arg); + String arg = iter.next(); + + if (arg.equals("-s")) + { + iter.remove(); + + if (iter.hasNext()) + { + arg = iter.next(); + iter.remove(); + names.add(arg); + } + else + { + errorln("-s must be followed by a strategy name"); + names.add("unknown"); + } + } } - else + } + else + { + for (int i=0; i map = (Map) arglist.get(i); + + Boolean enabled = (Boolean) map.getOrDefault("enabled", true); + + if (enabled) + { + names.add((String) map.get("name")); + } } } } diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java index c1d37e839..4a342934b 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java @@ -32,6 +32,7 @@ import com.fujitsu.vdmj.plugins.commands.PrintCommand; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.pog.RecursiveObligation; import com.fujitsu.vdmj.runtime.Interpreter; /** @@ -91,6 +92,17 @@ public String run(String line) { if (obligation.counterexample != null) { + if (obligation instanceof RecursiveObligation) + { + RecursiveObligation rec = (RecursiveObligation)obligation; + + if (rec.mutuallyRecursive) + { + return "Mutually recursive measures fail for these bindings: " + + obligation.counterexample.toStringLine(); + } + } + launch = obligation.getCexLaunch(); } else if (obligation.witness != null) diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java index c409bc224..37716ec4f 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java @@ -27,11 +27,13 @@ import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.pog.RecursiveObligation; import com.fujitsu.vdmj.runtime.Interpreter; import dap.DAPMessageList; import dap.DAPRequest; import dap.ExpressionExecutor; +import json.JSONObject; import vdmj.commands.AnalysisCommand; import workspace.PluginRegistry; import workspace.plugins.POPlugin; @@ -91,6 +93,18 @@ public DAPMessageList run(DAPRequest request) { if (obligation.counterexample != null) { + if (obligation instanceof RecursiveObligation) + { + RecursiveObligation rec = (RecursiveObligation)obligation; + + if (rec.mutuallyRecursive) + { + return new DAPMessageList(request, new JSONObject("result", + "Mutually recursive measures fail for these bindings: " + + obligation.counterexample.toStringLine())); + } + } + launch = obligation.getCexLaunch(); } else if (obligation.witness != null) diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckHandler.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckHandler.java new file mode 100644 index 000000000..2b50a37c1 --- /dev/null +++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckHandler.java @@ -0,0 +1,49 @@ +/******************************************************************************* + * + * Copyright (c) 2023 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package quickcheck.plugin; + +import lsp.LSPHandler; +import rpc.RPCMessageList; +import rpc.RPCRequest; +import workspace.PluginRegistry; + +/** + * LSP Handler for QC DAP commands + */ +public class QuickCheckHandler extends LSPHandler +{ + @Override + public RPCMessageList request(RPCRequest request) + { + try + { + QuickCheckLSPPlugin qc = PluginRegistry.getInstance().getPlugin("QC"); + return qc.quickCheck(request); + } + catch (Exception e) + { + return new RPCMessageList(request, e); + } + } +} diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java index 77bbf9f53..ffa76d1cf 100644 --- a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java +++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java @@ -24,15 +24,34 @@ package quickcheck.plugin; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Vector; + import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.plugins.HelpList; +import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.runtime.Interpreter; import com.fujitsu.vdmj.util.Utils; +import json.JSONArray; import json.JSONObject; +import lsp.CancellableThread; +import quickcheck.QuickCheck; +import quickcheck.commands.QCConsole; import quickcheck.commands.QCRunLSPCommand; import quickcheck.commands.QuickCheckLSPCommand; +import rpc.RPCDispatcher; +import rpc.RPCErrors; +import rpc.RPCMessageList; +import rpc.RPCRequest; import vdmj.commands.AnalysisCommand; +import workspace.DAPWorkspaceManager; +import workspace.Diag; +import workspace.PluginRegistry; import workspace.plugins.AnalysisPlugin; +import workspace.plugins.POPlugin; public class QuickCheckLSPPlugin extends AnalysisPlugin { @@ -50,9 +69,137 @@ public String getName() @Override public void init() { - // Get everything from PO? + // Register handler with RPCDispatcher + RPCDispatcher dispatcher = RPCDispatcher.getInstance(); + dispatcher.register(new QuickCheckHandler(), "slsp/POG/quickcheck"); } + public RPCMessageList quickCheck(RPCRequest request) + { + if (messagehub.hasErrors()) + { + Diag.error("Spec has errors"); + return new RPCMessageList(request, RPCErrors.InternalError, "Spec has errors"); + } + else if (CancellableThread.currentlyRunning() != null) + { + Diag.error("Running " + CancellableThread.currentlyRunning()); + return new RPCMessageList(request, RPCErrors.InternalError, "Running " + CancellableThread.currentlyRunning()); + } + + DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + Interpreter interpreter = manager.getInterpreter(); + + if (interpreter.getInitialContext() == null) // eg. from unit tests + { + try + { + interpreter.init(); + } + catch (Exception e) + { + Diag.error(e); + return new RPCMessageList(request, RPCErrors.InternalError, "Init has errors"); + } + } + + QuickCheck qc = new QuickCheck(); + + QCConsole.setQuiet(true); + QCConsole.setVerbose(false); + + qc.loadStrategies(getParams(request)); + + if (qc.hasErrors()) + { + Diag.error("Failed to load QC strategies"); + return new RPCMessageList(request, RPCErrors.InternalError, "Failed to load QC strategies"); + } + + Vector poList = new Vector(); + Vector poNames = new Vector(); + long timeout = 1L; + + if (request.get("params") != null) + { + JSONObject params = request.get("params"); + + if (params.get("config") != null) + { + JSONObject config = params.get("config"); + JSONArray obligations = config.get("obligations"); + timeout = config.get("timeout", 1L); + + if (obligations != null && !obligations.isEmpty()) + { + for (int i=0; i < obligations.size(); i++) + { + long po = obligations.index(i); + poList.add((int) po); + } + } + else + { + poNames.add(".*"); + } + } + } + + POPlugin pog = PluginRegistry.getInstance().getPlugin("PO"); + ProofObligationList all = pog.getProofObligations(); + ProofObligationList chosen = qc.getPOs(all, poList, poNames); + + if (qc.hasErrors()) + { + Diag.error("Failed to find POs"); + return new RPCMessageList(request, RPCErrors.InternalError, "Failed to find POs"); + } + else if (chosen.isEmpty()) + { + Diag.error("No POs in scope"); + return new RPCMessageList(request, RPCErrors.InternalError, "No POs in scope"); + } + else if (qc.initStrategies(timeout)) + { + QuickCheckThread executor = new QuickCheckThread(request, qc, chosen); + executor.start(); + } + else + { + Diag.error("No strategy to run"); + return new RPCMessageList(request, RPCErrors.InternalError, "No strategy to run"); + } + + return null; + } + + private List> getParams(RPCRequest request) + { + List> list = new Vector>(); + JSONObject params = request.get("params"); + + if (params != null && params.get("strategies") != null) + { + JSONArray strategies = params.get("strategies"); + + for (int i=0; i map = new HashMap(); + JSONObject entry = (JSONObject) strategies.get(i); + + for (String key: entry.keySet()) + { + Object value = entry.get(key); + map.put(key, value); + } + + list.add(map); + } + } + + return list; + } + @Override public void setServerCapabilities(JSONObject capabilities) { diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java new file mode 100644 index 000000000..564a84157 --- /dev/null +++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java @@ -0,0 +1,238 @@ +/******************************************************************************* + * + * Copyright (c) 2023 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package quickcheck.plugin; + +import java.io.IOException; +import java.util.List; +import java.util.Vector; + +import com.fujitsu.vdmj.messages.VDMMessage; +import com.fujitsu.vdmj.messages.VDMWarning; +import com.fujitsu.vdmj.pog.POStatus; +import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.pog.RecursiveObligation; + +import json.JSONArray; +import json.JSONObject; +import lsp.CancellableThread; +import lsp.LSPServer; +import lsp.Utils; +import quickcheck.QuickCheck; +import quickcheck.strategies.StrategyResults; +import rpc.RPCMessageList; +import rpc.RPCRequest; +import rpc.RPCResponse; +import workspace.Diag; +import workspace.MessageHub; +import workspace.PluginRegistry; +import workspace.plugins.POPlugin; + +public class QuickCheckThread extends CancellableThread +{ + private final RPCRequest request; + private final QuickCheck qc; + private final ProofObligationList chosen; + private final POPlugin pog; + private final Object workDoneToken; + + public QuickCheckThread(RPCRequest request, QuickCheck qc, ProofObligationList chosen) + { + super(request.get("id")); + this.request = request; + this.qc = qc; + this.chosen = chosen; + this.pog = PluginRegistry.getInstance().getPlugin("PO"); + + JSONObject params = request.get("params"); + this.workDoneToken = params.get("workDoneToken"); + } + + @Override + protected void body() + { + try + { + running = "quickcheck"; + RPCMessageList responses = new RPCMessageList(); + + LSPServer server = LSPServer.getInstance(); + MessageHub.getInstance().clearPluginMessages(pog); + List messages = new Vector(); + JSONArray list = new JSONArray(); + long percentDone = -1; + int count = 0; + + for (ProofObligation po: chosen) + { + StrategyResults results = qc.getValues(po); + + if (!qc.hasErrors()) + { + qc.checkObligation(po, results); + } + + list.add(getQCResponse(po, messages)); + count++; + + if (workDoneToken != null) + { + long done = (100 * count)/chosen.size(); + + if (done != percentDone) // Only if changed %age + { + JSONObject value = null; + + if (percentDone < 0) + { + value = new JSONObject( + "kind", "begin", + "title", "Executing QuickCheck", + "message", "Processing QuickCheck", + "percentage", done); + } + else + { + value = new JSONObject( + "kind", "report", + "message", "Processing QuickCheck", + "percentage", done); + } + + JSONObject params = new JSONObject("token", workDoneToken, "value", value); + Diag.fine("Sending QC work done = %d%%", done); + server.writeMessage(RPCRequest.notification("$/progress", params)); + percentDone = done; + } + } + + if (cancelled) + { + list.clear(); + break; + } + } + + responses.add(RPCResponse.result(request, list)); + + if (!cancelled) + { + MessageHub.getInstance().addPluginMessages(pog, messages); + responses.addAll(MessageHub.getInstance().getDiagnosticResponses()); + } + + for (JSONObject message: responses) + { + server.writeMessage(message); + } + } + catch (IOException e) + { + Diag.error(e); + } + finally + { + running = null; + } + } + + private JSONObject getQCResponse(ProofObligation po, List messages) + { + JSONObject json = new JSONObject( + "id", Long.valueOf(po.number), + "status", po.status.toString()); + + if (po.counterexample != null) + { + JSONObject cexample = new JSONObject(); + cexample.put("variables", Utils.contextToJSON(po.counterexample)); + JSONObject launch = pog.getCexLaunch(po); + + if (po instanceof RecursiveObligation) + { + RecursiveObligation rec = (RecursiveObligation)po; + + if (rec.mutuallyRecursive) + { + // Recursive function obligations check the measure_f value for each + // (mutually) recursive call. So a launch would have to make two comparisons + // of measure values. Until we can figure out how to do this, we don't + // send a launch string, but set a message to display instead. + + json.put("message", "Mutually recursive measures fail for these bindings"); + launch = null; + } + } + + if (launch != null) + { + cexample.put("launch", launch); + } + + json.put("counterexample", cexample); + + StringBuilder sb = new StringBuilder(); + sb.append("PO #"); + sb.append(po.number); + sb.append(" counterexample: "); + sb.append(po.counterexample.toStringLine()); + messages.add(new VDMWarning(9000, sb.toString(), po.location)); + } + + if (po.status == POStatus.FAILED) + { + if (po.message != null) // Add failed messages as a warning too + { + messages.add(new VDMWarning(9000, po.message, po.location)); + } + } + + if (po.witness != null) + { + JSONObject witness = new JSONObject(); + witness.put("variables", Utils.contextToJSON(po.witness)); + JSONObject launch = pog.getWitnessLaunch(po); + + if (launch != null) + { + witness.put("launch", launch); + } + + json.put("witness", witness); + } + + if (po.provedBy != null) + { + json.put("provedBy", po.provedBy); + } + + if (po.message != null) + { + json.put("message", po.message); + } + + return json; + } +} diff --git a/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java index 8325f8ddf..f4bb9592a 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java @@ -31,6 +31,7 @@ import java.math.BigInteger; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import com.fujitsu.vdmj.in.expressions.INCaseAlternative; @@ -66,19 +67,29 @@ public class DirectQCStrategy extends QCStrategy { private int errorCount = 0; - - public DirectQCStrategy(List argv) + + public DirectQCStrategy(List argv) { - for (int i=0; i < argv.size(); i++) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - if (argv.get(i).startsWith("-direct:")) + for (int i=0; i < argv.size(); i++) { - println("Unknown direct option: " + argv.get(i)); - println(help()); - errorCount ++; - argv.remove(i); + String arg = (String)argv.get(i); + + if (arg.startsWith("-direct:")) + { + println("Unknown direct option: " + argv); + println(help()); + errorCount ++; + argv.remove(i); + } } } + else + { + @SuppressWarnings({ "unchecked", "unused" }) + Map map = getParams((List>) argv, "direct"); + } } @Override diff --git a/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index 8bb41503c..4e7502c9f 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -30,6 +30,7 @@ import java.util.HashMap; import java.util.Iterator; import java.util.List; +import java.util.Map; import com.fujitsu.vdmj.in.patterns.INBindingOverride; import com.fujitsu.vdmj.in.types.visitors.INGetAllValuesVisitor; @@ -46,50 +47,60 @@ public class FiniteQCStrategy extends QCStrategy private int expansionLimit = 1024; // Small and fast? private int errorCount = 0; - public FiniteQCStrategy(List argv) + public FiniteQCStrategy(List argv) { - Iterator iter = argv.iterator(); - - while (iter.hasNext()) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - try + @SuppressWarnings("unchecked") + Iterator iter = (Iterator) argv.iterator(); + + while (iter.hasNext()) { - String arg = iter.next(); - - switch (arg) + try { - case "-finite:size": // Total top level size = type size - iter.remove(); - - if (iter.hasNext()) - { - expansionLimit = Integer.parseInt(iter.next()); - iter.remove(); - } - break; - - default: - if (arg.startsWith("-finite:")) - { - println("Unknown finite option: " + arg); - println(help()); - errorCount++; + String arg = iter.next(); + + switch (arg) + { + case "-finite:size": // Total top level size = type size iter.remove(); - } + + if (iter.hasNext()) + { + expansionLimit = Integer.parseInt(iter.next()); + iter.remove(); + } + break; + + default: + if (arg.startsWith("-finite:")) + { + println("Unknown finite option: " + arg); + println(help()); + errorCount++; + iter.remove(); + } + } + } + catch (NumberFormatException e) + { + println("Argument must be numeric"); + println(help()); + errorCount++; + } + catch (ArrayIndexOutOfBoundsException e) + { + println("Missing argument"); + println(help()); + errorCount++; } } - catch (NumberFormatException e) - { - println("Argument must be numeric"); - println(help()); - errorCount++; - } - catch (ArrayIndexOutOfBoundsException e) - { - println("Missing argument"); - println(help()); - errorCount++; - } + } + else + { + @SuppressWarnings("unchecked") + Map map = getParams((List>) argv, "finite"); + expansionLimit = get(map, "size", expansionLimit); } } diff --git a/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java index 7a406ffda..bd5098cae 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java @@ -110,74 +110,84 @@ public class FixedQCStrategy extends QCStrategy private Map allRanges = null; - public FixedQCStrategy(List argv) + public FixedQCStrategy(List argv) { - Iterator iter = argv.iterator(); - - while (iter.hasNext()) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - try + @SuppressWarnings("unchecked") + Iterator iter = (Iterator) argv.iterator(); + + while (iter.hasNext()) { - String arg = iter.next(); - - switch (arg) + try { - case "-fixed:file": // Use this as ranges.qc - iter.remove(); - - if (iter.hasNext()) - { - rangesFile = iter.next(); - iter.remove(); - } - - createFile = false; - break; - - case "-fixed:create": // Create ranges.qc - iter.remove(); - - if (iter.hasNext()) - { - rangesFile = iter.next(); + String arg = iter.next(); + + switch (arg) + { + case "-fixed:file": // Use this as ranges.qc iter.remove(); - } - - createFile = true; - break; - - case "-fixed:size": // Total top level size - iter.remove(); - - if (iter.hasNext()) - { - expansionLimit = Integer.parseInt(iter.next()); + + if (iter.hasNext()) + { + rangesFile = iter.next(); + iter.remove(); + } + + createFile = false; + break; + + case "-fixed:create": // Create ranges.qc iter.remove(); - } - break; - - default: - if (arg.startsWith("-fixed:")) - { - println("Unknown fixed option: " + arg); - println(help()); - errorCount++; + + if (iter.hasNext()) + { + rangesFile = iter.next(); + iter.remove(); + } + + createFile = true; + break; + + case "-fixed:size": // Total top level size iter.remove(); - } + + if (iter.hasNext()) + { + expansionLimit = Integer.parseInt(iter.next()); + iter.remove(); + } + break; + + default: + if (arg.startsWith("-fixed:")) + { + println("Unknown fixed option: " + arg); + println(help()); + errorCount++; + iter.remove(); + } + } + } + catch (NumberFormatException e) + { + println("Argument must be numeric"); + println(help()); + errorCount++; + } + catch (ArrayIndexOutOfBoundsException e) + { + println("Missing argument"); + println(help()); + errorCount++; } } - catch (NumberFormatException e) - { - println("Argument must be numeric"); - println(help()); - errorCount++; - } - catch (ArrayIndexOutOfBoundsException e) - { - println("Missing argument"); - println(help()); - errorCount++; - } + } + else + { + @SuppressWarnings("unchecked") + Map map = getParams((List>) argv, "fixed"); + expansionLimit = get(map, "size", expansionLimit); } } diff --git a/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java index bb3e9820e..84ebeae7e 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java @@ -24,7 +24,9 @@ package quickcheck.strategies; +import java.util.HashMap; import java.util.List; +import java.util.Map; import com.fujitsu.vdmj.in.patterns.INBindingOverride; import com.fujitsu.vdmj.pog.ProofObligation; @@ -40,4 +42,42 @@ abstract public class QCStrategy abstract public boolean init(QuickCheck qc); abstract public StrategyResults getValues(ProofObligation po, List binds, Context ctxt); abstract public String help(); + + /** + * These methods help with access to the JSON parameters passed from VSCode. + */ + + protected Map getParams(List> list, String name) + { + if (list != null) + { + for (Map entry: list) + { + if (name.equals(entry.get("name"))) + { + return entry; + } + } + } + + return new HashMap(); + } + + protected int get(Map map, String key, int def) + { + Long value = (Long) map.get(key); + return (value != null) ? value.intValue() : def; + } + + protected long get(Map map, String key, long def) + { + Long value = (Long) map.get(key); + return (value != null) ? value.longValue() : def; + } + + protected boolean get(Map map, String key, boolean def) + { + Boolean value = (Boolean) map.get(key); + return (value != null) ? value.booleanValue() : def; + } } diff --git a/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java index 4376d098b..56d40119f 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java @@ -30,6 +30,7 @@ import java.util.HashMap; import java.util.Iterator; import java.util.List; +import java.util.Map; import com.fujitsu.vdmj.in.patterns.INBindingOverride; import com.fujitsu.vdmj.pog.ProofObligation; @@ -44,64 +45,74 @@ public class RandomQCStrategy extends QCStrategy { private int expansionLimit = 20; // Overall returned value limit - private long seed; + private long seed = System.currentTimeMillis(); private int errorCount = 0; - public RandomQCStrategy(List argv) + public RandomQCStrategy(List argv) { - seed = System.currentTimeMillis(); - Iterator iter = argv.iterator(); - - while (iter.hasNext()) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - try + @SuppressWarnings("unchecked") + Iterator iter = (Iterator) argv.iterator(); + + while (iter.hasNext()) { - String arg = iter.next(); - - switch (arg) + try { - case "-random:size": // Total top level size - iter.remove(); - - if (iter.hasNext()) - { - expansionLimit = Integer.parseInt(iter.next()); - iter.remove(); - } - break; - - case "-random:seed": // Seed - iter.remove(); - - if (iter.hasNext()) - { - seed = Long.parseLong(iter.next()); + String arg = iter.next(); + + switch (arg) + { + case "-random:size": // Total top level size iter.remove(); - } - break; - - default: - if (arg.startsWith("-random:")) - { - println("Unknown random option: " + arg); - println(help()); - errorCount++; + + if (iter.hasNext()) + { + expansionLimit = Integer.parseInt(iter.next()); + iter.remove(); + } + break; + + case "-random:seed": // Seed iter.remove(); - } + + if (iter.hasNext()) + { + seed = Long.parseLong(iter.next()); + iter.remove(); + } + break; + + default: + if (arg.startsWith("-random:")) + { + println("Unknown random option: " + arg); + println(help()); + errorCount++; + iter.remove(); + } + } + } + catch (NumberFormatException e) + { + println("Argument must be numeric"); + println(help()); + errorCount++; + } + catch (ArrayIndexOutOfBoundsException e) + { + println("Missing argument"); + println(help()); + errorCount++; } } - catch (NumberFormatException e) - { - println("Argument must be numeric"); - println(help()); - errorCount++; - } - catch (ArrayIndexOutOfBoundsException e) - { - println("Missing argument"); - println(help()); - errorCount++; - } + } + else + { + @SuppressWarnings("unchecked") + Map map = getParams((List>) argv, "random"); + expansionLimit = get(map, "size", expansionLimit); + seed = get(map, "seed", seed); } } diff --git a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index f4c7bd4f8..2abefd16d 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -24,11 +24,12 @@ package quickcheck.strategies; -import static quickcheck.commands.QCConsole.println; +import static com.fujitsu.vdmj.plugins.PluginConsole.println; import static quickcheck.commands.QCConsole.verbose; import java.util.HashMap; import java.util.List; +import java.util.Map; import com.fujitsu.vdmj.in.patterns.INBindingOverride; import com.fujitsu.vdmj.pog.ProofObligation; @@ -47,20 +48,28 @@ public class SearchQCStrategy extends QCStrategy { private int errorCount = 0; - public SearchQCStrategy(List argv) + public SearchQCStrategy(List argv) { - for (int i=0; i < argv.size(); i++) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - // No plugin arguments yet? - - if (argv.get(i).startsWith("-search:")) + for (int i=0; i < argv.size(); i++) { - println("Unknown search option: " + argv.get(i)); - println(help()); - errorCount ++; - argv.remove(i); + String arg = (String)argv.get(i); + + if (arg.startsWith("-search:")) + { + println("Unknown search option: " + arg); + println(help()); + errorCount ++; + argv.remove(i); + } } } + else + { + @SuppressWarnings({ "unchecked", "unused" }) + Map map = getParams((List>) argv, "search"); + } } @Override diff --git a/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java index cc2168bfb..2d9d82057 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java @@ -28,6 +28,7 @@ import static quickcheck.commands.QCConsole.verbose; import java.util.List; +import java.util.Map; import java.util.Stack; import com.fujitsu.vdmj.in.patterns.INBindingOverride; @@ -42,20 +43,28 @@ public class TrivialQCStrategy extends QCStrategy { private int errorCount = 0; - public TrivialQCStrategy(List argv) + public TrivialQCStrategy(List argv) { - for (int i=0; i < argv.size(); i++) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - // No plugin arguments yet? - - if (argv.get(i).startsWith("-trivial:")) + for (int i=0; i < argv.size(); i++) { - println("Unknown trivial option: " + argv.get(i)); - println(help()); - errorCount ++; - argv.remove(i); + String arg = (String)argv.get(i); + + if (arg.startsWith("-trivial:")) + { + println("Unknown trivial option: " + arg); + println(help()); + errorCount ++; + argv.remove(i); + } } } + else + { + @SuppressWarnings({ "unchecked", "unused" }) + Map map = getParams((List>) argv, "trivial"); + } } @Override diff --git a/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java b/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java index c727e2489..df7340878 100644 --- a/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -44,34 +44,45 @@ public class ExampleQCStrategy extends QCStrategy private boolean provedResult = false; private int errorCount = 0; - public ExampleQCStrategy(List argv) + @SuppressWarnings("unchecked") + public ExampleQCStrategy(List argv) { - // Remove your "qc" plugin arguments from the list here - // It's useful to include the strategy name, like "-example:n" - for (int i=0; i < argv.size(); i++) + if (!argv.isEmpty() && argv.get(0) instanceof String) { - switch (argv.get(i)) + List args = (List)argv; + + // Remove your "qc" plugin arguments from the list here + // It's useful to include the strategy name, like "-example:n" + for (int i=0; i < args.size(); i++) { - case "-example:proved": - argv.remove(i); - - if (i < argv.size()) - { - provedResult = Boolean.parseBoolean(argv.get(i)); - argv.remove(i); - } - break; - - default: - if (argv.get(i).startsWith("-example:")) - { - errorln("Unknown exmaple option: " + argv.get(i)); - errorln(help()); - errorCount++; - argv.remove(i); - } + switch (args.get(i)) + { + case "-example:proved": + args.remove(i); + + if (i < args.size()) + { + provedResult = Boolean.parseBoolean(args.get(i)); + args.remove(i); + } + break; + + default: + if (args.get(i).startsWith("-example:")) + { + errorln("Unknown exmaple option: " + args.get(i)); + errorln(help()); + errorCount++; + args.remove(i); + } + } } } + else + { + Map map = getParams((List>) argv, "example"); + provedResult = get(map, "proved", false); + } } @Override diff --git a/quickcheck/src/test/java/tests/LSPTest.java b/quickcheck/src/test/java/tests/LSPTest.java new file mode 100644 index 000000000..d0084b400 --- /dev/null +++ b/quickcheck/src/test/java/tests/LSPTest.java @@ -0,0 +1,85 @@ +/******************************************************************************* + * + * Copyright (c) 2020 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package tests; + +import static org.junit.Assert.assertEquals; + +import java.io.File; +import java.io.IOException; +import java.io.PrintWriter; + +import com.fujitsu.vdmj.Settings; +import com.fujitsu.vdmj.lex.Dialect; + +import json.JSONObject; +import json.JSONWriter; +import rpc.RPCMessageList; +import rpc.RPCRequest; +import workspace.DAPWorkspaceManager; +import workspace.DAPXWorkspaceManager; +import workspace.Diag; +import workspace.LSPWorkspaceManager; +import workspace.LSPXWorkspaceManager; + +abstract public class LSPTest +{ + protected LSPWorkspaceManager lspManager = null; + protected LSPXWorkspaceManager lspxManager = null; + protected DAPWorkspaceManager dapManager = null; + protected DAPXWorkspaceManager dapxManager = null; + + static + { + Diag.init(false); // No logging, if lsp.log.level is unset + } + + protected void setupWorkspace(Dialect dialect) throws IOException + { + Settings.dialect = dialect; + LSPWorkspaceManager.reset(); // resets other managers, registry and hubs + lspManager = LSPWorkspaceManager.getInstance(); + lspxManager = LSPXWorkspaceManager.getInstance(); + dapManager = DAPWorkspaceManager.getInstance(); + dapxManager = DAPXWorkspaceManager.getInstance(); + } + + protected RPCMessageList initialize(File root, JSONObject capabilities) throws Exception + { + RPCMessageList result = lspManager.lspInitialize(RPCRequest.create("initialize", null), + new JSONObject(), root.getAbsoluteFile(), capabilities); + assertEquals("init result", (Object)null, result.get(0).get("error")); + + return lspManager.afterChangeWatchedFiles(null, 1, null); // Cause parse and typecheck + } + + protected void dump(JSONObject obj) throws IOException + { + PrintWriter pw = new PrintWriter(System.out); + JSONWriter writer = new JSONWriter(pw); + writer.writeObject(obj); + pw.println(); + writer.flush(); + } +} diff --git a/quickcheck/src/test/java/tests/QCTest.java b/quickcheck/src/test/java/tests/QCTest.java new file mode 100644 index 000000000..0d8e8905e --- /dev/null +++ b/quickcheck/src/test/java/tests/QCTest.java @@ -0,0 +1,81 @@ +/******************************************************************************* + * + * Copyright (c) 2024 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package tests; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + +import java.io.File; + +import org.junit.Test; + +import com.fujitsu.vdmj.lex.Dialect; + +import json.JSONArray; +import json.JSONObject; +import quickcheck.plugin.QuickCheckHandler; +import rpc.RPCMessageList; +import rpc.RPCRequest; + +public class QCTest extends LSPTest +{ + private JSONObject capabilities = new JSONObject( + "experimental", new JSONObject("proofObligationGeneration", true)); + @Test + public void testQC() throws Exception + { + setupWorkspace(Dialect.VDM_SL); + File testdir = new File("src/test/resources/qctest"); + RPCMessageList notify = initialize(testdir, capabilities); + assertEquals(3, notify.size()); + + dump(notify.get(0)); + assertEquals("slsp/POG/updated", notify.get(0).getPath("method")); + assertEquals(true, notify.get(0).getPath("params.successful")); + + dump(notify.get(1)); + assertEquals("textDocument/publishDiagnostics", notify.get(1).getPath("method")); + assertTrue(notify.get(1).getPath("params.diagnostics") instanceof JSONArray); + + QuickCheckHandler handler = new QuickCheckHandler(); + + JSONObject params = new JSONObject + ( + "workDoneToken", "12345678", // random + + "config", + new JSONObject + ( + "timeout", 2L, + "obligations", new JSONArray(1, 2) + ) + ); + + RPCRequest request = RPCRequest.create(123L, "slsp/POG/quickcheck", params); + + RPCMessageList response = handler.request(request); + assertEquals(null, response); + } +} diff --git a/quickcheck/src/test/resources/qctest/qctest.vdmsl b/quickcheck/src/test/resources/qctest/qctest.vdmsl new file mode 100644 index 000000000..6eb0e896a --- /dev/null +++ b/quickcheck/src/test/resources/qctest/qctest.vdmsl @@ -0,0 +1,4 @@ +functions + f: real -> nat + f(a) == 1/a + pre a > 0; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/commands/CommandReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/commands/CommandReader.java index 1e7e911ee..19f242ac3 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/commands/CommandReader.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/commands/CommandReader.java @@ -776,7 +776,7 @@ protected boolean doAllTraces(String line) return notAvailable(line); } - protected boolean doQuit(@SuppressWarnings("unused") String line) + protected boolean doQuit(String line) { if (RTLogger.getLogSize() > 0) { @@ -993,7 +993,7 @@ protected boolean doDefault(String line) throws Exception return notAvailable(line); } - protected boolean doInit(@SuppressWarnings("unused") String line) + protected boolean doInit(String line) { LexLocation.clearLocations(); println("Cleared all coverage information"); @@ -1030,7 +1030,7 @@ protected boolean doInit(@SuppressWarnings("unused") String line) return true; } - protected boolean doEnv(@SuppressWarnings("unused") String line) + protected boolean doEnv(String line) { print(interpreter.getInitialContext().toString()); return true; @@ -1587,7 +1587,7 @@ public boolean assertFile(File filename) return assertErrors == 0; } - protected void doHelp(@SuppressWarnings("unused") String line) + protected void doHelp(String line) { println("print - evaluate expression"); println("runtrace [start test [end test]] - run CT trace"); @@ -1633,7 +1633,7 @@ protected void doHelp(@SuppressWarnings("unused") String line) * The method just prints "Command not available in this context" and * returns true. */ - protected boolean notAvailable(@SuppressWarnings("unused") String line) + protected boolean notAvailable(String line) { println("Command not available in this context"); return true; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/config/Properties.java b/vdmj/src/main/java/com/fujitsu/vdmj/config/Properties.java index a6c361b61..081ce6386 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/config/Properties.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/config/Properties.java @@ -259,7 +259,6 @@ private static boolean get(java.util.Properties local, String key, boolean def) return value; } - @SuppressWarnings("unused") private static String get(java.util.Properties local, String key, String def) { String value = System.getProperty(key); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/debug/BreakpointReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/debug/BreakpointReader.java index 8e9826755..c2a600a6b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/debug/BreakpointReader.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/debug/BreakpointReader.java @@ -109,7 +109,7 @@ private boolean doException(Exception e) return true; } - public boolean doList(@SuppressWarnings("unused") String line) + public boolean doList(String line) { Map map = interpreter.getBreakpoints(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/statements/INStateDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/statements/INStateDesignator.java index 49e9728dc..3ba630a5c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/statements/INStateDesignator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/statements/INStateDesignator.java @@ -48,8 +48,7 @@ public INStateDesignator(LexLocation location) @Override abstract public String toString(); - public INDefinition targetDefinition( - @SuppressWarnings("unused") Environment env) + public INDefinition targetDefinition(Environment env) { return null; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java index 84441613c..cc74197b7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java @@ -97,8 +97,7 @@ public class Position /** * Create a Position from the outer class' current position details. */ - @SuppressWarnings("synthetic-access") - public Position() + public Position() { lc = linecount; cc = charpos; @@ -114,7 +113,6 @@ public Position() /** * Set the outer class position details to those contained in this. */ - @SuppressWarnings("synthetic-access") public void set() { linecount = lc; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java index dc7da6349..59a8be671 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java @@ -39,9 +39,14 @@ public class RecursiveObligation extends ProofObligation { + public final boolean mutuallyRecursive; + public RecursiveObligation(LexLocation location, PODefinitionList defs, POApplyExpression apply, POContextStack ctxt) { super(location, POType.RECURSIVE, ctxt); + + mutuallyRecursive = (defs.size() > 2); // Simple recursion = [f, f] + int measureLexical = getLex(getMeasureDef(defs.get(0))); String lhs = getLHS(defs.get(0)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCStateDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCStateDesignator.java index 1d865607d..1f7899ad6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCStateDesignator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCStateDesignator.java @@ -50,7 +50,7 @@ public TCStateDesignator(LexLocation location) abstract public TCType typeCheck(Environment env); - public TCDefinition targetDefinition(@SuppressWarnings("unused") Environment env) + public TCDefinition targetDefinition(Environment env) { return null; }