From 826ee21e8d0c38e9461a656aa3c808f91896432f Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 16 Nov 2023 10:33:27 +0000 Subject: [PATCH 01/10] Type check tixe when no exists possible --- .../vdmj/tc/statements/TCTixeStatement.java | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCTixeStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCTixeStatement.java index c5f8fd1dc..2ff493778 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCTixeStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCTixeStatement.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.tc.statements.visitors.TCStatementVisitor; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeSet; +import com.fujitsu.vdmj.tc.types.TCUnknownType; import com.fujitsu.vdmj.typechecker.Environment; import com.fujitsu.vdmj.typechecker.NameScope; @@ -56,14 +57,16 @@ public TCType typeCheck(Environment env, NameScope scope, TCType constraint, boo TCType rt = body.typeCheck(env, scope, constraint, mandatory); TCTypeSet extypes = body.exitCheck(env); - // if (!extypes.isEmpty()) + if (extypes.isEmpty()) { - TCType union = extypes.getType(location); + extypes.add(new TCUnknownType(location)); // Force TC of alts anyway + } + + TCType union = extypes.getType(location); - for (TCTixeStmtAlternative tsa: traps) - { - tsa.typeCheck(env, scope, union, constraint, mandatory); - } + for (TCTixeStmtAlternative tsa: traps) + { + tsa.typeCheck(env, scope, union, constraint, mandatory); } return setType(rt); From 4a2f927b387d15cbcb1d8e6a7349657504e7e19d Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 16 Nov 2023 11:44:27 +0000 Subject: [PATCH 02/10] Add empty list assertion in TCTypeList --- vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCTypeList.java | 1 + 1 file changed, 1 insertion(+) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCTypeList.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCTypeList.java index 96c64fc32..978714bbd 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCTypeList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/TCTypeList.java @@ -60,6 +60,7 @@ public boolean add(TCType t) public TCType getType(LexLocation location) { + assert this.size() > 0 : "Getting type of empty TypeList"; TCType result = null; if (this.size() == 1) From 4430036fb40d2082670997c26775239c66cda3a7 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Fri, 17 Nov 2023 22:08:50 +0000 Subject: [PATCH 03/10] Add WSPlugin and use to set a "global" warning about extracted files --- .../main/java/examples/ExamplePluginPR.java | 6 +- .../main/java/examples/ExamplePluginSL.java | 4 +- .../main/java/workspace/EventListener.java | 11 ++-- .../java/workspace/LSPWorkspaceManager.java | 31 +++++++++ lsp/src/main/java/workspace/MessageHub.java | 37 ++++++----- .../events/AbstractCheckFilesEvent.java | 4 +- .../main/java/workspace/plugins/WSPlugin.java | 63 +++++++++++++++++++ 7 files changed, 127 insertions(+), 29 deletions(-) create mode 100644 lsp/src/main/java/workspace/plugins/WSPlugin.java diff --git a/examples/lspplugin/src/main/java/examples/ExamplePluginPR.java b/examples/lspplugin/src/main/java/examples/ExamplePluginPR.java index 1e530d094..e9bf1a903 100644 --- a/examples/lspplugin/src/main/java/examples/ExamplePluginPR.java +++ b/examples/lspplugin/src/main/java/examples/ExamplePluginPR.java @@ -27,9 +27,7 @@ import java.io.File; 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.tc.definitions.TCClassDefinition; import com.fujitsu.vdmj.tc.definitions.TCClassList; @@ -98,9 +96,7 @@ private void addFirstWarning(CheckCompleteEvent event) throws IOException if (def.name != null) { VDMWarning warning = new VDMWarning(9999, "Example warning from plugin", def.name.getLocation()); - List list = new Vector(); - list.add(warning); - MessageHub.getInstance().addPluginMessages(this, list); // Add the warning to the hub + MessageHub.getInstance().addPluginMessage(this, warning); // Add the warning to the hub break; } } diff --git a/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java b/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java index 8367f9c96..8df42b2cc 100644 --- a/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java +++ b/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java @@ -103,9 +103,7 @@ private void addFirstWarning(CheckCompleteEvent event) throws IOException if (def.name != null) { VDMWarning warning = new VDMWarning(9999, "Example warning from plugin", def.name.getLocation()); - List list = new Vector(); - list.add(warning); - MessageHub.getInstance().addPluginMessages(this, list); // Add the warning to the hub + MessageHub.getInstance().addPluginMessage(this, warning); // Add the warning to the hub break; } } diff --git a/lsp/src/main/java/workspace/EventListener.java b/lsp/src/main/java/workspace/EventListener.java index 7ec5b7629..7ec085634 100644 --- a/lsp/src/main/java/workspace/EventListener.java +++ b/lsp/src/main/java/workspace/EventListener.java @@ -34,11 +34,12 @@ */ public interface EventListener { - public final static int AST_PRIORITY = Integer.getInteger("lspx.plugins.priority.ast", 100); - public final static int TC_PRIORITY = Integer.getInteger("lspx.plugins.priority.tc", 200); - public final static int IN_PRIORITY = Integer.getInteger("lspx.plugins.priority.in", 300); - public final static int PO_PRIORITY = Integer.getInteger("lspx.plugins.priority.po", 400); - public final static int CT_PRIORITY = Integer.getInteger("lspx.plugins.priority.co", 500); + public final static int WS_PRIORITY = Integer.getInteger("lspx.plugins.priority.ws", 100); + public final static int AST_PRIORITY = Integer.getInteger("lspx.plugins.priority.ast", 200); + public final static int TC_PRIORITY = Integer.getInteger("lspx.plugins.priority.tc", 300); + public final static int IN_PRIORITY = Integer.getInteger("lspx.plugins.priority.in", 400); + public final static int PO_PRIORITY = Integer.getInteger("lspx.plugins.priority.po", 500); + public final static int CT_PRIORITY = Integer.getInteger("lspx.plugins.priority.co", 600); public final static int USER_PRIORITY = Integer.getInteger("lspx.plugins.priority.user", 1000); diff --git a/lsp/src/main/java/workspace/LSPWorkspaceManager.java b/lsp/src/main/java/workspace/LSPWorkspaceManager.java index c020ab1d2..b8efcbcbb 100644 --- a/lsp/src/main/java/workspace/LSPWorkspaceManager.java +++ b/lsp/src/main/java/workspace/LSPWorkspaceManager.java @@ -53,6 +53,8 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.config.Properties; import com.fujitsu.vdmj.lex.BacktrackInputReader; +import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.messages.VDMWarning; import com.fujitsu.vdmj.runtime.SourceFile; import com.fujitsu.vdmj.tc.definitions.TCClassDefinition; import com.fujitsu.vdmj.tc.definitions.TCClassList; @@ -95,6 +97,7 @@ import workspace.plugins.ASTPlugin; import workspace.plugins.INPlugin; import workspace.plugins.TCPlugin; +import workspace.plugins.WSPlugin; public class LSPWorkspaceManager { @@ -155,6 +158,7 @@ public static synchronized LSPWorkspaceManager getInstance() * when the client capabilities have been received. */ PluginRegistry registry = PluginRegistry.getInstance(); + registry.registerPlugin(WSPlugin.factory(Settings.dialect)); registry.registerPlugin(ASTPlugin.factory(Settings.dialect)); registry.registerPlugin(TCPlugin.factory(Settings.dialect)); registry.registerPlugin(INPlugin.factory(Settings.dialect)); @@ -524,6 +528,7 @@ private void loadExternalFile(File file) throws IOException Diag.info("Not overwriting existing extract file: %s", extract); externalFiles.put(extract, FileTime.fromMillis(0)); loadFile(extract); + modifiedExtractWarning(extract); } else { @@ -548,6 +553,29 @@ private void loadExternalFile(File file) throws IOException } } } + + private void modifiedExtractWarning(File extract) throws IOException + { + SourceFile source = new SourceFile(extract); + String line1 = source.getLine(1); + String line2 = source.getLine(2); + LexLocation loc = null; + + // Look for standard extract header (see ExternalFileFormats), else + // highlight the first line. + + if (line2.startsWith("-- Document created from")) + { + loc = new LexLocation(extract, "", 2, 4, 2, line2.length() + 4); + } + else + { + loc = new LexLocation(extract, "", 1, 1, 1, line1.length()); + } + + WSPlugin ws = registry.getPlugin("WS"); + messagehub.addPluginMessage(ws, new VDMWarning(0, "This extracted file has been modified", loc)); + } private boolean onDotPath(File file) { @@ -850,6 +878,7 @@ else if (!openFiles.contains(file)) { sendMessage(WARNING_MSG, "WARNING: Changing extracted VDM source: " + file); externalFilesWarned.add(file); + modifiedExtractWarning(file); } StringBuilder buffer = projectFiles.get(file); @@ -906,6 +935,8 @@ else if (!openFiles.contains(file)) if (externalFiles.containsKey(file)) { sendMessage(WARNING_MSG, "WARNING: Saving extracted VDM source: " + file); + modifiedExtractWarning(file); + } if (text != null) diff --git a/lsp/src/main/java/workspace/MessageHub.java b/lsp/src/main/java/workspace/MessageHub.java index df27b955d..160b50e70 100644 --- a/lsp/src/main/java/workspace/MessageHub.java +++ b/lsp/src/main/java/workspace/MessageHub.java @@ -106,32 +106,39 @@ public synchronized void addFile(File file) * Add a list of messages for files (assumed to be already added). */ public synchronized void addPluginMessages(AnalysisPlugin plugin, List messages) + { + for (VDMMessage message: messages) + { + addPluginMessage(plugin, message); + } + } + + /** + * Add a single message for a plugin. + */ + public void addPluginMessage(AnalysisPlugin plugin, VDMMessage message) { String pname = plugin.getName(); + Map> pmap = messageMap.get(message.location.file); - for (VDMMessage message: messages) + if (pmap != null) { - Map> pmap = messageMap.get(message.location.file); + Set pmessages = pmap.get(pname); - if (pmap != null) + if (pmessages != null) { - Set pmessages = pmap.get(pname); - - if (pmessages != null) - { - pmessages.add(message); - Diag.fine("Added %s MSG %s", pname, message); - } - else - { - Diag.error("Cannot add message for plugin %s", pname); - } + pmessages.add(message); + Diag.fine("Added %s MSG %s", pname, message); } else { - Diag.error("File %s not in MessageHub", message.location.file); + Diag.error("Cannot add message for plugin %s", pname); } } + else + { + Diag.error("File %s not in MessageHub", message.location.file); + } } /** diff --git a/lsp/src/main/java/workspace/events/AbstractCheckFilesEvent.java b/lsp/src/main/java/workspace/events/AbstractCheckFilesEvent.java index 6bb38a744..53a5f146e 100644 --- a/lsp/src/main/java/workspace/events/AbstractCheckFilesEvent.java +++ b/lsp/src/main/java/workspace/events/AbstractCheckFilesEvent.java @@ -24,10 +24,12 @@ package workspace.events; +import rpc.RPCRequest; + abstract public class AbstractCheckFilesEvent extends LSPEvent { public AbstractCheckFilesEvent() { - super(null); + super(RPCRequest.create("AbstractFileRequest", "")); } } diff --git a/lsp/src/main/java/workspace/plugins/WSPlugin.java b/lsp/src/main/java/workspace/plugins/WSPlugin.java new file mode 100644 index 000000000..1cdb28a4e --- /dev/null +++ b/lsp/src/main/java/workspace/plugins/WSPlugin.java @@ -0,0 +1,63 @@ +/******************************************************************************* + * + * 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 workspace.plugins; + +import com.fujitsu.vdmj.lex.Dialect; + +import workspace.EventListener; + +/** + * The workspace plugin. This may grow in use, if it makes sense + * to move the workspace manager tasks here, driven by LSP events. + */ +public class WSPlugin extends AnalysisPlugin implements EventListener +{ + public static AnalysisPlugin factory(Dialect dialect) + { + switch (dialect) + { + default: + return new WSPlugin(); + } + } + + @Override + public int getPriority() + { + return EventListener.WS_PRIORITY; + } + + @Override + public String getName() + { + return "WS"; + } + + @Override + public void init() + { + // No need to handle any events yet + } +} From aefa0c4676944bda79234a08705e45a977d4e943 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 18 Nov 2023 16:34:37 +0000 Subject: [PATCH 04/10] Fix some warnings --- examples/lspplugin/src/main/java/examples/ExamplePluginSL.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java b/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java index 8df42b2cc..e9e277bc4 100644 --- a/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java +++ b/examples/lspplugin/src/main/java/examples/ExamplePluginSL.java @@ -27,9 +27,7 @@ import java.io.File; 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.tc.definitions.TCDefinition; import com.fujitsu.vdmj.tc.modules.TCModule; From 5b43ed9da0ec6e7e5ddecf9c8149ac7b0bc3f098 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Wed, 22 Nov 2023 12:51:41 +0000 Subject: [PATCH 05/10] Check for async cancelled in QC --- .../main/java/quickcheck/commands/QuickCheckExecutor.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java index 61f6c9caa..fed17f1ee 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java @@ -95,10 +95,15 @@ protected void exec() throws Exception { qc.checkObligation(po, results); } + + if (cancelled) + { + break; + } } } - answer = qc.hasErrors() ? "Failed" : "OK"; + answer = qc.hasErrors() ? "Failed" : cancelled ? "Cancelled" : "OK"; } @Override From 8c76259636e6d9dae23fd6ee353f5dbdbf6faf2d Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 23 Nov 2023 12:52:30 +0000 Subject: [PATCH 06/10] Existential false with hasAllValues => FAILED --- .../src/main/java/quickcheck/QuickCheck.java | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index f0de76392..ccbca2012 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -528,8 +528,19 @@ else if (results.hasAllValues && execCompleted) } else if (po.isExistential()) // Principal exp is "exists..." { - infof("PO #%d, MAYBE %s\n", po.number, duration(before, after)); - po.setStatus(POStatus.MAYBE); + if (results.hasAllValues) + { + infof("PO #%d, FAILED (unsatisfiable) %s\n", po.number, duration(before, after)); + po.setStatus(POStatus.FAILED); + infoln("----"); + infoln(po); + } + else + { + infof("PO #%d, MAYBE %s\n", po.number, duration(before, after)); + po.setStatus(POStatus.MAYBE); + } + po.setCounterexample(null); po.setMessage(null); po.setWitness(null); From 5712468d931919024ec00977b561c04b931a905a Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 23 Nov 2023 15:56:52 +0000 Subject: [PATCH 07/10] Display QC message for any FAILED obligation --- .../quickcheck/src/main/java/quickcheck/QuickCheck.java | 3 ++- lsp/src/main/java/workspace/plugins/POPlugin.java | 8 ++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index ccbca2012..1b4890929 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -532,6 +532,7 @@ else if (po.isExistential()) // Principal exp is "exists..." { infof("PO #%d, FAILED (unsatisfiable) %s\n", po.number, duration(before, after)); po.setStatus(POStatus.FAILED); + po.setMessage("Unsatisfiable"); infoln("----"); infoln(po); } @@ -539,10 +540,10 @@ else if (po.isExistential()) // Principal exp is "exists..." { infof("PO #%d, MAYBE %s\n", po.number, duration(before, after)); po.setStatus(POStatus.MAYBE); + po.setMessage(null); } po.setCounterexample(null); - po.setMessage(null); po.setWitness(null); } else diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index 3654fa280..ab471cab8 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -32,6 +32,7 @@ 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; import com.fujitsu.vdmj.runtime.Context; @@ -219,8 +220,11 @@ else if (file.isDirectory()) sb.append(" counterexample: "); sb.append(po.counterexample.toStringLine()); messages.add(new VDMWarning(9000, sb.toString(), po.location)); - - if (po.message != null) // Add any message as a warning too + } + + 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)); } From 9f81a5f4e357403613265b8633ace81a018371d8 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 24 Nov 2023 17:45:29 +0000 Subject: [PATCH 08/10] Move launch generation from POPlugin to ProofObligation --- .../main/java/workspace/plugins/POPlugin.java | 9 +- .../java/workspace/plugins/POPluginPR.java | 12 +- .../java/workspace/plugins/POPluginSL.java | 124 ++++-------------- .../com/fujitsu/vdmj/pog/ProofObligation.java | 122 +++++++++++++++++ 4 files changed, 160 insertions(+), 107 deletions(-) diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index ab471cab8..c12385374 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -35,7 +35,6 @@ import com.fujitsu.vdmj.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; -import com.fujitsu.vdmj.runtime.Context; import json.JSONArray; import json.JSONObject; @@ -141,7 +140,9 @@ protected void preCheck(CheckPrepareEvent event) abstract public ProofObligationList getProofObligations(); - abstract protected JSONObject getLaunch(ProofObligation po, Context ctxt); + abstract protected JSONObject getCexLaunch(ProofObligation po); + + abstract protected JSONObject getWitnessLaunch(ProofObligation po); protected JSONArray splitPO(String value) { @@ -205,7 +206,7 @@ else if (file.isDirectory()) { JSONObject cexample = new JSONObject(); cexample.put("variables", Utils.contextToJSON(po.counterexample)); - JSONObject launch = getLaunch(po, po.counterexample); + JSONObject launch = getCexLaunch(po); if (launch != null) { @@ -234,7 +235,7 @@ else if (file.isDirectory()) { JSONObject witness = new JSONObject(); witness.put("variables", Utils.contextToJSON(po.witness)); - JSONObject launch = getLaunch(po, po.witness); + JSONObject launch = getWitnessLaunch(po); if (launch != null) { diff --git a/lsp/src/main/java/workspace/plugins/POPluginPR.java b/lsp/src/main/java/workspace/plugins/POPluginPR.java index 3de772b25..1fb2eb368 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginPR.java +++ b/lsp/src/main/java/workspace/plugins/POPluginPR.java @@ -31,7 +31,6 @@ import com.fujitsu.vdmj.po.definitions.POClassList; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; -import com.fujitsu.vdmj.runtime.Context; import json.JSONObject; import workspace.events.CheckPrepareEvent; @@ -83,9 +82,14 @@ public ProofObligationList getProofObligations() } @Override - protected JSONObject getLaunch(ProofObligation po, Context ctxt) + protected JSONObject getCexLaunch(ProofObligation po) { - // TODO More complex than SL as we have to think about constructors... - return null; + return null; // Needs to create new object? + } + + @Override + protected 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 5bf489406..803acea74 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginSL.java +++ b/lsp/src/main/java/workspace/plugins/POPluginSL.java @@ -28,19 +28,9 @@ import com.fujitsu.vdmj.mapper.Mappable; import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.annotations.POAnnotation; -import com.fujitsu.vdmj.po.definitions.PODefinition; -import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; -import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; -import com.fujitsu.vdmj.po.definitions.POTypeDefinition; import com.fujitsu.vdmj.po.modules.POModuleList; -import com.fujitsu.vdmj.po.patterns.POPattern; -import com.fujitsu.vdmj.po.patterns.POPatternList; -import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; -import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; -import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; -import com.fujitsu.vdmj.runtime.Context; import json.JSONObject; import workspace.events.CheckPrepareEvent; @@ -92,106 +82,42 @@ public ProofObligationList getProofObligations() } @Override - protected JSONObject getLaunch(ProofObligation po, Context ctxt) + protected JSONObject getCexLaunch(ProofObligation po) { - PODefinition def = po.definition; - JSONObject result = null; + String launch = po.getCexLaunch(); - if (def instanceof POExplicitFunctionDefinition) + if (launch == null) { - POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)def; - result = launchExplicitFunction(po, efd, ctxt); + return null; // No counterexample or definition or mismatched params } - else if (def instanceof POImplicitFunctionDefinition) - { - POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)def; - StringBuilder callString = new StringBuilder(); - callString.append("("); - String sep = ""; - PORemoveIgnoresVisitor.init(); - - for (POPatternListTypePair pl: ifd.parameterPatterns) - { - for (POPattern p: pl.patterns) - { - String match = paramMatch(p.removeIgnorePatterns(), ctxt); - - if (match == null) - { - return null; // Can't match some params - } - - callString.append(sep); - callString.append(match); - sep = ", "; - } - } - - callString.append(")"); - - result = new JSONObject( - "name", "PO #" + po.number + " counterexample", - "type", "vdm", - "request", "launch", - "noDebug", false, - "defaultName", def.name.getModule(), - "command", "print " + def.name.getName() + callString + + return new JSONObject( + "name", "PO #" + po.number + " counterexample", + "type", "vdm", + "request", "launch", + "noDebug", false, + "defaultName", po.definition.name.getModule(), + "command", "print " + launch ); - } - else if (def instanceof POTypeDefinition) - { - POTypeDefinition td = (POTypeDefinition)def; - - if (td.invdef != null) - { - result = launchExplicitFunction(po, td.invdef, ctxt); - } - } - - return result; } - - private JSONObject launchExplicitFunction(ProofObligation po, POExplicitFunctionDefinition efd, Context ctxt) + + @Override + protected JSONObject getWitnessLaunch(ProofObligation po) { - StringBuilder callString = new StringBuilder(); - PORemoveIgnoresVisitor.init(); + String launch = po.getWitnessLaunch(); - for (POPatternList pl: efd.paramPatternList) + if (launch == null) { - callString.append("("); - String sep = ""; - - for (POPattern p: pl) - { - String match = paramMatch(p.removeIgnorePatterns(), ctxt); - - if (match == null) - { - return null; // Can't match some params - } - - callString.append(sep); - callString.append(match); - sep = ", "; - } - - callString.append(")"); + return null; // No witness or definition or mismatched params } return new JSONObject( - "name", "PO #" + po.number + " counterexample", - "type", "vdm", - "request", "launch", - "noDebug", false, - "defaultName", efd.name.getModule(), - "command", "print " + efd.name.getName() + callString - ); - } - - private String paramMatch(POPattern p, Context ctxt) - { - POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor(); - String result = p.apply(visitor, ctxt); - return visitor.hasFailed() ? null : result; + "name", "PO #" + po.number + " witness", + "type", "vdm", + "request", "launch", + "noDebug", false, + "defaultName", po.definition.name.getModule(), + "command", "print " + launch + ); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 7758370aa..80f4527aa 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -27,7 +27,15 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.definitions.PODefinition; +import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POTypeDefinition; +import com.fujitsu.vdmj.po.patterns.POPattern; +import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; +import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; +import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.types.TCType; @@ -197,4 +205,118 @@ protected String explicitType(TCType type, LexLocation poLoc) { return type.toExplicitString(poLoc); } + + /** + * Generate a string invocation for the context passed. + */ + public String getCexLaunch() + { + if (counterexample.isEmpty()) + { + return null; + } + + return getLaunch(counterexample); + } + + public String getWitnessLaunch() + { + if (witness.isEmpty()) + { + return null; + } + + return getLaunch(witness); + } + + private String getLaunch(Context ctxt) + { + if (definition instanceof POExplicitFunctionDefinition) + { + POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)definition; + return launchExplicitFunction(efd, ctxt); + } + else if (definition instanceof POImplicitFunctionDefinition) + { + POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)definition; + return launchImplicitFunction(ifd, ctxt); + } + else if (definition instanceof POTypeDefinition) + { + POTypeDefinition td = (POTypeDefinition)definition; + + if (td.invdef != null) + { + return launchExplicitFunction(td.invdef, ctxt); + } + } + + return null; // Unexpected definition + } + + private String launchExplicitFunction(POExplicitFunctionDefinition efd, Context ctxt) + { + StringBuilder callString = new StringBuilder(efd.name.getName()); + PORemoveIgnoresVisitor.init(); + + for (POPatternList pl: efd.paramPatternList) + { + callString.append("("); + String sep = ""; + + for (POPattern p: pl) + { + String match = paramMatch(p.removeIgnorePatterns(), ctxt); + + if (match == null) + { + return null; // Can't match some params + } + + callString.append(sep); + callString.append(match); + sep = ", "; + } + + callString.append(")"); + } + + return callString.toString(); + } + + private String launchImplicitFunction(POImplicitFunctionDefinition ifd, Context ctxt) + { + StringBuilder callString = new StringBuilder(ifd.name.getName()); + callString.append("("); + String sep = ""; + PORemoveIgnoresVisitor.init(); + + for (POPatternListTypePair pl: ifd.parameterPatterns) + { + for (POPattern p: pl.patterns) + { + String match = paramMatch(p.removeIgnorePatterns(), ctxt); + + if (match == null) + { + return null; // Can't match some params + } + + callString.append(sep); + callString.append(match); + sep = ", "; + } + } + + callString.append(")"); + + return callString.toString(); + } + + private String paramMatch(POPattern p, Context ctxt) + { + POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor(); + String result = p.apply(visitor, ctxt); + return visitor.hasFailed() ? null : result; + } } From 436c94e1325b8c2945a065cc866b1f5d8beb4b06 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 24 Nov 2023 18:19:32 +0000 Subject: [PATCH 09/10] Added VDMJ qcrun command --- .../quickcheck/commands/QCRunCommand.java | 110 ++++++++++++++++++ .../quickcheck/plugin/QuickCheckPlugin.java | 11 +- 2 files changed, 119 insertions(+), 2 deletions(-) create mode 100644 examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java new file mode 100644 index 000000000..d77726ae4 --- /dev/null +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java @@ -0,0 +1,110 @@ +/******************************************************************************* + * + * 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.commands; + +import static com.fujitsu.vdmj.plugins.PluginConsole.println; + +import com.fujitsu.vdmj.plugins.AnalysisCommand; +import com.fujitsu.vdmj.plugins.analyses.POPlugin; +import com.fujitsu.vdmj.plugins.commands.PrintCommand; +import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.pog.ProofObligationList; + +/** + * Launch a "print" command for a PO counterexample or witness. + */ +public class QCRunCommand extends AnalysisCommand +{ + private final static String CMD = "qcrun "; + private final static String USAGE = "Usage: " + CMD; + + public QCRunCommand(String line) + { + super(line); + + if (!argv[0].equals("qcrun")) + { + throw new IllegalArgumentException(USAGE); + } + } + + @Override + public String run(String line) + { + POPlugin po = registry.getPlugin("PO"); + ProofObligationList all = po.getProofObligations(); + + if (argv.length == 2) + { + int number = 0; + + try + { + number = Integer.parseInt(argv[1]); + } + catch (NumberFormatException e) + { + return USAGE; + } + + for (ProofObligation obligation: all) + { + if (obligation.number == number) + { + String launch = null; + + if (!obligation.counterexample.isEmpty()) + { + launch = obligation.getCexLaunch(); + } + else if (!obligation.witness.isEmpty()) + { + launch = obligation.getWitnessLaunch(); + } + else + { + return "Obligation does not have a counterexample/witness. Run qc?"; + } + + String pline = "print " + launch; + println("> " + pline); + PrintCommand cmd = new PrintCommand(pline); + return cmd.run(pline); + } + } + + return "No such obligation: " + number; + } + else + { + return USAGE; + } + } + + public static void help() + { + println(CMD + " - execute counterexample/witness"); + } +} diff --git a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java index 405ca7aaf..da79e729f 100644 --- a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java +++ b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.plugins.AnalysisPlugin; import com.fujitsu.vdmj.util.Utils; +import quickcheck.commands.QCRunCommand; import quickcheck.commands.QuickCheckCommand; public class QuickCheckPlugin extends AnalysisPlugin @@ -55,9 +56,14 @@ public AnalysisCommand getCommand(String line) { String[] argv = Utils.toArgv(line); - if (argv[0].equals("quickcheck") || argv[0].equals("qc")) + switch (argv[0]) { - return new QuickCheckCommand(line); + case "quickcheck": + case "qc": + return new QuickCheckCommand(line); + + case "qcrun": + return new QCRunCommand(line); } return null; @@ -67,5 +73,6 @@ public AnalysisCommand getCommand(String line) public void help() { QuickCheckCommand.help(); + QCRunCommand.help(); } } From 64439ab1c7c0df731a83d3d8c3484982f2313152 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 24 Nov 2023 18:50:10 +0000 Subject: [PATCH 10/10] Added VSCode qcrun command --- .../quickcheck/commands/QCRunLSPCommand.java | 109 ++++++++++++++++++ .../plugin/QuickCheckLSPPlugin.java | 14 ++- 2 files changed, 120 insertions(+), 3 deletions(-) create mode 100644 examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java new file mode 100644 index 000000000..0f9d735ca --- /dev/null +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java @@ -0,0 +1,109 @@ +/******************************************************************************* + * + * 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.commands; + +import static com.fujitsu.vdmj.plugins.PluginConsole.println; + +import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.pog.ProofObligationList; + +import dap.DAPMessageList; +import dap.DAPRequest; +import dap.ExpressionExecutor; +import vdmj.commands.AnalysisCommand; +import workspace.PluginRegistry; +import workspace.plugins.POPlugin; + +/** + * Launch a "print" command for a PO counterexample or witness. + */ +public class QCRunLSPCommand extends AnalysisCommand +{ + public static final String USAGE = "Usage: qcrun "; + public static final String HELP = "qcrun - execute counterexample/witness"; + + private final int number; + + public QCRunLSPCommand(String line) + { + super(line); + String[] parts = line.split("\\s+", 2); + + if (parts.length != 2) + { + throw new IllegalArgumentException(USAGE); + } + + try + { + number = Integer.parseInt(argv[1]); + } + catch (NumberFormatException e) + { + throw new IllegalArgumentException(USAGE); + } + } + + @Override + public DAPMessageList run(DAPRequest request) + { + POPlugin po = PluginRegistry.getInstance().getPlugin("PO"); + ProofObligationList all = po.getProofObligations(); + + for (ProofObligation obligation: all) + { + if (obligation.number == number) + { + String launch = null; + + if (!obligation.counterexample.isEmpty()) + { + launch = obligation.getCexLaunch(); + } + else if (!obligation.witness.isEmpty()) + { + launch = obligation.getWitnessLaunch(); + } + else + { + return new DAPMessageList(request, false, + "Obligation does not have a counterexample/witness. Run qc?", null); + } + + println("print " + launch); + ExpressionExecutor executor = new ExpressionExecutor("print", request, launch); + executor.start(); + return null; + } + } + + return new DAPMessageList(request, false, "No such obligation: " + number, null); + } + + @Override + public boolean notWhenRunning() + { + return true; + } +} diff --git a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java index a2d5d8e29..22fc51bea 100644 --- a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java +++ b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.util.Utils; import json.JSONObject; +import quickcheck.commands.QCRunLSPCommand; import quickcheck.commands.QuickCheckLSPCommand; import vdmj.commands.AnalysisCommand; import vdmj.commands.HelpList; @@ -68,9 +69,14 @@ public AnalysisCommand getCommand(String line) { String[] argv = Utils.toArgv(line); - if (argv[0].equals("quickcheck") || argv[0].equals("qc")) + switch (argv[0]) { - return new QuickCheckLSPCommand(line); + case "quickcheck": + case "qc": + return new QuickCheckLSPCommand(line); + + case "qcrun": + return new QCRunLSPCommand(line); } return null; @@ -79,6 +85,8 @@ public AnalysisCommand getCommand(String line) @Override public HelpList getCommandHelp() { - return new HelpList(QuickCheckLSPCommand.SHORT + " - lightweight PO verification"); + return new HelpList( + QuickCheckLSPCommand.SHORT + " - lightweight PO verification", + QCRunLSPCommand.HELP); } }