From 3899688b8ae38cf42eb0d901ef104de600a10b9e Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 7 Nov 2023 21:15:27 +0000 Subject: [PATCH 1/4] Inherit PluginConsole methods in QCConsole --- .../java/quickcheck/commands/QCConsole.java | 45 ++++--------------- 1 file changed, 9 insertions(+), 36 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/examples/quickcheck/src/main/java/quickcheck/commands/QCConsole.java index 293d4f5ea..50c237ce5 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QCConsole.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QCConsole.java @@ -24,16 +24,17 @@ package quickcheck.commands; -import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.messages.Console; +import com.fujitsu.vdmj.plugins.PluginConsole; /** - * This copies the PluginConsole from VDMJ to allow us to have "global" quiet + * This extends the PluginConsole from VDMJ to allow us to have "global" quiet * setting within the QC command environment, without affecting the outer - * environment. + * environment. By extending PluginConsole, we get a "private" quiet flag + * that won't interfere with the global one, but we can still use the inherited + * methods as well. */ - -public class QCConsole +public class QCConsole extends PluginConsole { private static boolean quiet = false; @@ -46,20 +47,12 @@ public static boolean getQuiet() { return quiet; } - - public static void verbose(String format, Object... args) - { - if (Settings.verbose) - { - Console.out.printf(format, args); - } - } - public static void verboseln(String m) + public static void info(String m) { - if (Settings.verbose) + if (!quiet) { - Console.out.println(m); + Console.out.print(m); } } @@ -78,24 +71,4 @@ public static void infoln(Object m) Console.out.println(m.toString()); } } - - public static void println(Object m) - { - Console.out.println(m.toString()); - } - - public static void printf(String format, Object... args) - { - Console.out.printf(format, args); - } - - public static void errorln(Object m) - { - Console.err.println(m.toString()); - } - - public static void errorf(String format, Object... args) - { - Console.err.printf(format, args); - } } From 0ede29ec89cc1e69b63a477e6b272aaaac50da6c Mon Sep 17 00:00:00 2001 From: nick_battle Date: Wed, 8 Nov 2023 17:33:43 +0000 Subject: [PATCH 2/4] Clean up measure name detection with isMeasureName() --- .../vdmj/in/definitions/INExplicitFunctionDefinition.java | 2 +- .../vdmj/in/definitions/INImplicitFunctionDefinition.java | 2 +- .../vdmj/po/definitions/POExplicitFunctionDefinition.java | 2 +- .../vdmj/po/definitions/POImplicitFunctionDefinition.java | 2 +- .../vdmj/tc/definitions/TCExplicitFunctionDefinition.java | 4 ++-- .../vdmj/tc/definitions/TCImplicitFunctionDefinition.java | 2 +- vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java | 5 +++++ 7 files changed, 12 insertions(+), 7 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java index 20d0c4108..11bb6a56d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java @@ -145,7 +145,7 @@ public NameValuePairList getNamedValues(Context ctxt) postfunc.uninstantiated = (typeParams != null); } - if (measureDef != null && measureDef.name.getName().startsWith("measure_")) + if (measureDef != null && measureDef.name.isMeasureName()) { // Add implicit measure_* functions and any pre_measure_*s too. nvl.addAll(measureDef.getNamedValues(ctxt)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java index bcd810665..7bc9e8a74 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java @@ -157,7 +157,7 @@ public NameValuePairList getNamedValues(Context ctxt) postfunc.uninstantiated = (typeParams != null); } - if (measureDef != null && measureDef.name.getName().startsWith("measure_")) + if (measureDef != null && measureDef.name.isMeasureName()) { // Add implicit measure_* functions and any pre_measure_*s too. nvl.addAll(measureDef.getNamedValues(ctxt)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java index fd65871d9..dbe5f6020 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java @@ -185,7 +185,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment } } - if (measureDef != null && measureName != null && measureName.getName().startsWith("measure_")) + if (measureDef != null && measureName != null && measureName.isMeasureName()) { ctxt.push(new PONameContext(new TCNameList(measureName))); obligations.addAll(measureDef.getProofObligations(ctxt, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java index 54a206583..58a2d68a4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java @@ -179,7 +179,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment } } - if (measureDef != null && measureName != null && measureName.getName().startsWith("measure_")) + if (measureDef != null && measureName != null && measureName.isMeasureName()) { ctxt.push(new PONameContext(new TCNameList(measureName))); obligations.addAll(measureDef.getProofObligations(ctxt, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java index fb9084536..5be045511 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java @@ -368,7 +368,7 @@ else if (measureExp != null) if (!(body instanceof TCNotYetSpecifiedExpression) && !(body instanceof TCSubclassResponsibilityExpression) && - !(name.getName().startsWith("measure_"))) + !(name.isMeasureName())) { checked.unusedCheck(); // Look underneath qualified definitions, if any } @@ -646,7 +646,7 @@ public TCDefinitionList getDefinitions() defs.add(postdef); } - if (measureName != null && measureName.getName().startsWith("measure_")) + if (measureName != null && measureName.isMeasureName()) { defs.add(measureDef); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java index aaae8e29c..f0c623a96 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java @@ -513,7 +513,7 @@ public TCDefinitionList getDefinitions() defs.add(postdef); } - if (measureName != null && measureName.getName().startsWith("measure_")) + if (measureName != null && measureName.isMeasureName()) { defs.add(measureDef); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java index 02f6ca149..0724d5c11 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java @@ -212,6 +212,11 @@ public TCNameToken getMeasureName(LexLocation l) return new TCNameToken(l, getModule(), "measure_" + getName(), false, false); } + public boolean isMeasureName() + { + return lexname.name.startsWith("measure_"); // True, if a generated measure function + } + public TCNameToken getResultName(LexLocation l) { return new TCNameToken(l, getModule(), "RESULT", false, false); From a448c2d4694ecc1a09f6e10d52cb42775bb22ff8 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Thu, 9 Nov 2023 09:55:23 +0000 Subject: [PATCH 3/4] Set "quickCheckProvider: true" in QC plugin's server capabilities --- .../java/quickcheck/plugin/QuickCheckLSPPlugin.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java index 7b922d386..4bc638c9f 100644 --- a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java +++ b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.util.Utils; +import json.JSONObject; import quickcheck.commands.QuickCheckLSPCommand; import vdmj.commands.AnalysisCommand; import vdmj.commands.HelpList; @@ -51,6 +52,17 @@ public void init() // Get everything from PO? } + @Override + public void setServerCapabilities(JSONObject capabilities) + { + JSONObject experimental = capabilities.get("experimental"); + + if (experimental != null) + { + experimental.put("quickCheckProvider", true); + } + } + @Override public AnalysisCommand getCommand(String line) { From b91a1e4d90d541dd25de26aec6f5eafef27dd23f Mon Sep 17 00:00:00 2001 From: nick_battle Date: Fri, 10 Nov 2023 09:44:48 +0000 Subject: [PATCH 4/4] Only allow breakpoint entry from SchedulableThreads --- .../com/fujitsu/vdmj/runtime/Breakpoint.java | 10 ++++++++-- .../main/java/com/fujitsu/vdmj/util/Utils.java | 17 ++++++++++++----- 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java index f33b2d989..2d4e5852d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java @@ -270,13 +270,19 @@ public void enterDebugger(Context ctxt) { Thread current = Thread.currentThread(); + /** + * We can only debug expression breakpoints that occur from within SchedulableThreads, + * usually MainThread or InitThread etc. But it is possible to perform very high + * performance evaluations without creating extra SchedulableThreads, though these + * cannot be debugged and they are responsible for handling their own ContextExceptions + * and so on... + */ if (current instanceof SchedulableThread) { SchedulableThread th = (SchedulableThread)current; th.suspendOthers(); + DebugLink.getInstance().breakpoint(ctxt, this); } - - DebugLink.getInstance().breakpoint(ctxt, this); } /** diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/util/Utils.java b/vdmj/src/main/java/com/fujitsu/vdmj/util/Utils.java index 07e425950..2b89838be 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/util/Utils.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/util/Utils.java @@ -237,11 +237,18 @@ public static String getVersion() { String path = VDMJ.class.getName().replaceAll("\\.", "/"); URL url = VDMJ.class.getResource("/" + path + ".class"); - JarURLConnection conn = (JarURLConnection)url.openConnection(); - JarFile jar = conn.getJarFile(); - Manifest mf = jar.getManifest(); - String version = (String)mf.getMainAttributes().get(Attributes.Name.IMPLEMENTATION_VERSION); - return version; + + if (url.getProtocol().equals("jar")) + { + JarURLConnection conn = (JarURLConnection)url.openConnection(); + JarFile jar = conn.getJarFile(); + Manifest mf = jar.getManifest(); + return (String)mf.getMainAttributes().get(Attributes.Name.IMPLEMENTATION_VERSION); + } + else + { + return "(no version available in " + url.getProtocol() + ")"; + } } catch (Exception e) {