From 2028a81ae3ae21e48cbcdfd3c82fd4a6d98627ad Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 11 Nov 2024 18:02:40 +0000 Subject: [PATCH 01/18] Change codelenses to allow curried parameters --- .../workspace/lenses/ASTLaunchDebugLens.java | 18 +++++-- .../lenses/AbstractLaunchDebugLens.java | 46 ---------------- .../workspace/lenses/POLaunchDebugLens.java | 53 +++++++++++++++++++ .../workspace/lenses/TCLaunchDebugLens.java | 13 ++++- .../com/fujitsu/vdmj/pog/POLaunchFactory.java | 9 +++- 5 files changed, 87 insertions(+), 52 deletions(-) diff --git a/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java index 508555f55..80f0a44ed 100644 --- a/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java @@ -92,12 +92,24 @@ public JSONArray getDefinitionLenses(ASTDefinition def, ASTClassDefinition cls) } ASTFunctionType ftype = (ASTFunctionType) exdef.type; - ASTTypeList ptypes = ftype.parameters; int i = 0; - for (ASTPattern p: exdef.paramPatternList.get(0)) // Curried? + for (ASTPatternList pl: exdef.paramPatternList) { - applyArgs.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++)))); + JSONArray params = new JSONArray(); + ASTTypeList ptypes = ftype.parameters; + + for (ASTPattern p: pl) + { + params.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++)))); + } + + applyArgs.add(params); + + if (ftype.result instanceof ASTFunctionType) + { + ftype = (ASTFunctionType)ftype.result; + } } } } diff --git a/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java index b0b4db9ce..47fe86e2b 100644 --- a/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java @@ -24,11 +24,6 @@ package workspace.lenses; -import com.fujitsu.vdmj.pog.POLaunchFactory; -import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyArg; -import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyCall; -import com.fujitsu.vdmj.pog.ProofObligation; - import json.JSONArray; import json.JSONObject; @@ -68,45 +63,4 @@ protected JSONArray launchArgs(String launchName, String defaultName, return new JSONArray(launchArgs); // Array with one object } - - protected JSONArray launchArgs(ProofObligation po, String defaultName, boolean debug) - { - JSONObject launchArgs = new JSONObject(); - POLaunchFactory factory = new POLaunchFactory(po); - - ApplyCall apply = factory.getCexApply(); - - launchArgs.put("name", (debug ? "Debug " : "Launch ") + apply.applyName); - launchArgs.put("defaultName", defaultName); - launchArgs.put("type", "vdm"); - launchArgs.put("request", "launch"); - launchArgs.put("noDebug", !debug); // Note: inverted :) - launchArgs.put("remoteControl", null); - - launchArgs.put("applyName", apply.applyName); - - if (!apply.applyTypes.isEmpty()) - { - JSONArray applyTypes = new JSONArray(); - - for (String atype: apply.applyTypes) - { - applyTypes.add(atype); - } - - launchArgs.put("applyTypes", applyTypes); - } - - JSONArray applyArgs = new JSONArray(); - - for (ApplyArg arg: apply.applyArgs) - { - applyArgs.add(new JSONObject("name", arg.name, "type", arg.type, "value", arg.value)); - } - - launchArgs.put("applyArgs", applyArgs); - - return new JSONArray(launchArgs); - } - } diff --git a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java index 717e3ad88..896e5cf0c 100644 --- a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java @@ -23,10 +23,16 @@ ******************************************************************************/ package workspace.lenses; +import java.util.List; + import com.fujitsu.vdmj.po.definitions.PODefinition; +import com.fujitsu.vdmj.pog.POLaunchFactory; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyArg; +import com.fujitsu.vdmj.pog.POLaunchFactory.ApplyCall; import json.JSONArray; +import json.JSONObject; /** * A class to generate launch lenses for PO counterexamples. @@ -54,4 +60,51 @@ public JSONArray getLaunchLens() return results; } + + private JSONArray launchArgs(ProofObligation po, String defaultName, boolean debug) + { + JSONObject launchArgs = new JSONObject(); + POLaunchFactory factory = new POLaunchFactory(po); + + ApplyCall apply = factory.getCexApply(); + + launchArgs.put("name", (debug ? "Debug " : "Launch ") + apply.applyName); + launchArgs.put("defaultName", defaultName); + launchArgs.put("type", "vdm"); + launchArgs.put("request", "launch"); + launchArgs.put("noDebug", !debug); // Note: inverted :) + launchArgs.put("remoteControl", null); + + launchArgs.put("applyName", apply.applyName); + + if (!apply.applyTypes.isEmpty()) + { + JSONArray applyTypes = new JSONArray(); + + for (String atype: apply.applyTypes) + { + applyTypes.add(atype); + } + + launchArgs.put("applyTypes", applyTypes); + } + + JSONArray applyArgs = new JSONArray(); + + for (List arglist: apply.applyArgs) + { + JSONArray sublist = new JSONArray(); + + for (ApplyArg arg: arglist) + { + sublist.add(new JSONObject("name", arg.name, "type", arg.type, "value", arg.value)); + } + + applyArgs.add(sublist); + } + + launchArgs.put("applyArgs", applyArgs); + + return new JSONArray(launchArgs); + } } diff --git a/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java index d13cebdf7..a2f21ed6c 100644 --- a/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java @@ -89,7 +89,18 @@ public JSONArray getDefinitionLenses(TCDefinition def, TCClassDefinition cls) } TCFunctionType ftype = (TCFunctionType) exdef.type; - applyArgs = getParams(exdef.paramPatternList.get(0), ftype.parameters); + + applyArgs = new JSONArray(); + + for (TCPatternList pl: exdef.paramPatternList) + { + applyArgs.add(getParams(pl, ftype.parameters)); + + if (ftype.result instanceof TCFunctionType) + { + ftype = (TCFunctionType)ftype.result; + } + } } } else if (def instanceof TCImplicitFunctionDefinition) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java index 869c1d253..ed6dc2d70 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java @@ -55,7 +55,7 @@ public static class ApplyCall { public String applyName = null; public List applyTypes = new Vector(); - public List applyArgs = new Vector(); + public List> applyArgs = new Vector>(); } public static class ApplyArg @@ -207,6 +207,8 @@ private String launchArguments(POPatternList paramPatternList, TCTypeList types, String sep = ""; int i = 0; + applyCall.applyArgs.add(new Vector()); + for (POPattern p: paramPatternList) { String match = paramMatch(p.removeIgnorePatterns(), types.get(i++), ctxt); @@ -225,6 +227,8 @@ private String launchArguments(POPatternListTypePairList parameterPatterns, Cont String sep = ""; callString.append("("); + applyCall.applyArgs.add(new Vector()); + for (POPatternListTypePair pl: parameterPatterns) { for (POPattern p: pl.patterns) @@ -278,7 +282,8 @@ private String paramMatch(POPattern p, TCType type, Context ctxt) throws Excepti } else { - applyCall.applyArgs.add(new ApplyArg(p.toString(), type.toString(), result)); + List lastArgs = applyCall.applyArgs.get(applyCall.applyArgs.size() - 1); + lastArgs.add(new ApplyArg(p.toString(), type.toString(), result)); return result; } } From 7a5f79bb26b99ecd8eae4b3848c213c1af0169ec Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 11 Nov 2024 21:12:10 +0000 Subject: [PATCH 02/18] Correction to new code lens command --- .../java/workspace/lenses/ASTLaunchDebugLens.java | 12 +++++++++--- .../java/workspace/lenses/TCLaunchDebugLens.java | 9 ++++++--- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java index 80f0a44ed..6f60d4d54 100644 --- a/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java @@ -122,12 +122,14 @@ else if (def instanceof ASTImplicitFunctionDefinition) applyName = imdef.name.getName(); launchName = applyName; defaultName = imdef.name.module; + JSONArray params = new JSONArray(); + applyArgs.add(params); for (ASTPatternListTypePair param: imdef.parameterPatterns) { for (ASTPattern p: param.patterns) { - applyArgs.add(new JSONObject("name", p.toString(), "type", fix(param.type))); + params.add(new JSONObject("name", p.toString(), "type", fix(param.type))); } } } @@ -148,10 +150,12 @@ else if (def instanceof ASTExplicitOperationDefinition) ASTOperationType ftype = (ASTOperationType) exop.type; ASTTypeList ptypes = ftype.parameters; int i = 0; + JSONArray params = new JSONArray(); + applyArgs.add(params); for (ASTPattern p: exop.parameterPatterns) { - applyArgs.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++)))); + params.add(new JSONObject("name", p.toString(), "type", fix(ptypes.get(i++)))); } } } @@ -168,12 +172,14 @@ else if (def instanceof ASTImplicitOperationDefinition) if (!applyName.equals(defaultName)) // Not a constructor { launchName = applyName; + JSONArray params = new JSONArray(); + applyArgs.add(params); for (ASTPatternListTypePair param: imop.parameterPatterns) { for (ASTPattern p: param.patterns) { - applyArgs.add(new JSONObject("name", p.toString(), "type", fix(param.type))); + params.add(new JSONObject("name", p.toString(), "type", fix(param.type))); } } } diff --git a/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java index a2f21ed6c..d35e53b7b 100644 --- a/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/TCLaunchDebugLens.java @@ -112,7 +112,8 @@ else if (def instanceof TCImplicitFunctionDefinition) applyName = imdef.name.getName(); launchName = applyName; defaultName = imdef.name.getModule(); - applyArgs = getParams(imdef.parameterPatterns); + applyArgs = new JSONArray(); + applyArgs.add(getParams(imdef.parameterPatterns)); } } else if (def instanceof TCExplicitOperationDefinition) @@ -125,7 +126,8 @@ else if (def instanceof TCExplicitOperationDefinition) launchName = applyName; defaultName = exop.name.getModule(); TCOperationType ftype = (TCOperationType) exop.type; - applyArgs = getParams(exop.parameterPatterns, ftype.parameters); + applyArgs = new JSONArray(); + applyArgs.add(getParams(exop.parameterPatterns, ftype.parameters)); } } else if (def instanceof TCImplicitOperationDefinition) @@ -137,7 +139,8 @@ else if (def instanceof TCImplicitOperationDefinition) applyName = imop.name.getName(); launchName = applyName; defaultName = imop.name.getModule(); - applyArgs = getParams(imop.parameterPatterns); + applyArgs = new JSONArray(); + applyArgs.add(getParams(imop.parameterPatterns)); } } From 15208380a4889fe1c7b034eae0fdbf3f51092803 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Tue, 12 Nov 2024 09:30:49 +0000 Subject: [PATCH 03/18] Strengthen JSON validation --- lsp/src/main/java/json/JSONArray.java | 11 +--- lsp/src/main/java/json/JSONObject.java | 11 +--- lsp/src/main/java/json/JSONValue.java | 61 +++++++++++++++++++ .../main/java/workspace/lenses/CodeLens.java | 3 +- 4 files changed, 64 insertions(+), 22 deletions(-) create mode 100644 lsp/src/main/java/json/JSONValue.java diff --git a/lsp/src/main/java/json/JSONArray.java b/lsp/src/main/java/json/JSONArray.java index 41d4b6c25..a92f622f9 100644 --- a/lsp/src/main/java/json/JSONArray.java +++ b/lsp/src/main/java/json/JSONArray.java @@ -41,16 +41,7 @@ public JSONArray(Object... args) @Override public boolean add(Object value) { - if (value instanceof Integer) - { - value = ((Integer)value).longValue(); - } - else if (value instanceof Short) - { - value = ((Short)value).longValue(); - } - - return super.add(value); + return super.add(JSONValue.validate(value)); } @SuppressWarnings("unchecked") diff --git a/lsp/src/main/java/json/JSONObject.java b/lsp/src/main/java/json/JSONObject.java index 85249023b..4291d38c6 100644 --- a/lsp/src/main/java/json/JSONObject.java +++ b/lsp/src/main/java/json/JSONObject.java @@ -51,16 +51,7 @@ public JSONObject(Object... args) @Override public Object put(String name, Object value) { - if (value instanceof Integer) - { - value = ((Integer)value).longValue(); - } - else if (value instanceof Short) - { - value = ((Short)value).longValue(); - } - - return super.put(name, value); + return super.put(name, JSONValue.validate(value)); } @SuppressWarnings("unchecked") diff --git a/lsp/src/main/java/json/JSONValue.java b/lsp/src/main/java/json/JSONValue.java new file mode 100644 index 000000000..bf21c0ba9 --- /dev/null +++ b/lsp/src/main/java/json/JSONValue.java @@ -0,0 +1,61 @@ +/******************************************************************************* + * + * 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 json; + +/** + * A class to create valid JSON values. These can be added to JSONObject or JSONArray. + */ +public class JSONValue +{ + public static Object validate(Object value) + { + if (value == null) + { + // fine + } + else if (value instanceof Double || + value instanceof Float) + { + value = ((Number)value).doubleValue(); + } + else if (value instanceof Number) + { + value = ((Number)value).longValue(); + } + else if (value instanceof String || + value instanceof Boolean || + value instanceof JSONArray || + value instanceof JSONObject) + { + // fine + } + else + { + throw new IllegalArgumentException("Unexpected JSON value: " + value.getClass().getSimpleName()); + } + + return value; + } +} diff --git a/lsp/src/main/java/workspace/lenses/CodeLens.java b/lsp/src/main/java/workspace/lenses/CodeLens.java index 83f68817a..b4928f13f 100644 --- a/lsp/src/main/java/workspace/lenses/CodeLens.java +++ b/lsp/src/main/java/workspace/lenses/CodeLens.java @@ -66,8 +66,7 @@ protected boolean isClientType(String type) } /** - * These helper methods generate the lens response body. The JSONArray returned - * by getDefinitionLenses (above) is an array of these structures, one per lens. + * These helper methods generate the lens response body. */ protected JSONObject makeLens(LexLocation location, String title, String command) { From 741c0424a63f6cd88e791fa045f7b6122e30ce2e Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 12 Nov 2024 21:53:54 +0000 Subject: [PATCH 04/18] Fix for AST launch lenses --- lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java index 6f60d4d54..76cff4f4e 100644 --- a/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java @@ -92,12 +92,12 @@ public JSONArray getDefinitionLenses(ASTDefinition def, ASTClassDefinition cls) } ASTFunctionType ftype = (ASTFunctionType) exdef.type; - int i = 0; for (ASTPatternList pl: exdef.paramPatternList) { JSONArray params = new JSONArray(); ASTTypeList ptypes = ftype.parameters; + int i = 0; for (ASTPattern p: pl) { From 52fff044028ad36f61c24481fce2a2a42a048454 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 14 Nov 2024 11:41:06 +0000 Subject: [PATCH 05/18] Invariant types of the same name are always compatible --- .../vdmj/typechecker/TypeComparator.java | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java index 5d60ccce9..e806fa831 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/TypeComparator.java @@ -305,6 +305,30 @@ private static Result comptest(TCType to, TCType from, boolean paramOnly) { return Result.Yes; // Not defined "yet"...? } + + // Check (possibly opaque) invariant types early. These are always compatible, + // even allowing for opacity. + + if (from instanceof TCNamedType && to instanceof TCNamedType) + { + TCNamedType nfrom = (TCNamedType)from; + TCNamedType nto = (TCNamedType)to; + + if (nfrom.typename.equals(nto.typename)) + { + return Result.Yes; + } + } + else if (from instanceof TCRecordType && to instanceof TCRecordType) + { + TCRecordType rfrom = (TCRecordType)from; + TCRecordType rto = (TCRecordType)to; + + if (rfrom.name.equals(rto.name)) + { + return Result.Yes; + } + } // Obtain the fundamental type of BracketTypes, NamedTypes and // OptionalTypes. From 82143862462f70bcb9b2ea4a8544bbf3b9f849e2 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 14 Nov 2024 12:45:31 +0000 Subject: [PATCH 06/18] Add more markIfUpdated calls --- .../po/definitions/POAssignmentDefinition.java | 2 +- .../vdmj/po/patterns/POMultipleSeqBind.java | 4 +++- .../vdmj/po/patterns/POMultipleSetBind.java | 4 +++- .../com/fujitsu/vdmj/po/patterns/POSeqBind.java | 4 +++- .../com/fujitsu/vdmj/po/patterns/POSetBind.java | 4 +++- .../po/statements/POAssignmentStatement.java | 2 +- .../vdmj/po/statements/POExitStatement.java | 2 +- .../vdmj/po/statements/POForAllStatement.java | 4 ++-- .../vdmj/po/statements/POForIndexStatement.java | 6 +++--- .../po/statements/POForPatternBindStatement.java | 4 ++-- .../vdmj/po/statements/POIfStatement.java | 4 ++-- .../vdmj/po/statements/POLetBeStStatement.java | 2 +- .../vdmj/po/statements/POWhileStatement.java | 10 +++------- .../fujitsu/vdmj/pog/ProofObligationList.java | 16 ++++++++-------- 14 files changed, 36 insertions(+), 32 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java index 818aedd30..49b8ce017 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java @@ -71,7 +71,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { ProofObligationList obligations = new ProofObligationList(); obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, expression); + obligations.markIfUpdated(pogState, expression); if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java index c4709a94c..36b4222ce 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java @@ -51,7 +51,9 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return sequence.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = sequence.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, sequence); + return obligations; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java index 558a99a4b..d16644487 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java @@ -51,7 +51,9 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return set.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, set); + return obligations; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java index ea82c081f..4cadc811c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java @@ -64,7 +64,9 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return sequence.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = sequence.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, sequence); + return obligations; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java index d777966ee..f00fd8c75 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java @@ -64,7 +64,9 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return set.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, set); + return obligations; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java index 56a945c83..52fae99f3 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java @@ -87,7 +87,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog obligations.addAll(target.getProofObligations(ctxt)); obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, exp); + obligations.markIfUpdated(pogState, exp); TCNameSet updates = this.apply(new POStatementStateFinder(), true); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java index a50318293..2c7a8d302 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java @@ -57,7 +57,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog if (expression != null) { obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, expression); + obligations.markIfUpdated(pogState, expression); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java index 9fe2023a4..28cb55dfb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java @@ -60,10 +60,10 @@ public String toString() public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); - obligations.stateUpdate(pogState, set); + obligations.markIfUpdated(pogState, set); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); + if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java index 39a81535c..3970a4ab7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java @@ -67,17 +67,17 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { ProofObligationList obligations = from.getProofObligations(ctxt, pogState, env); obligations.addAll(to.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, from); + obligations.markIfUpdated(pogState, from); if (by != null) { obligations.addAll(by.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, by); + obligations.markIfUpdated(pogState, by); } ctxt.push(new POScopeContext()); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); + if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java index 736dd5cf8..71148fd77 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java @@ -69,7 +69,7 @@ public String toString() public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList list = exp.getProofObligations(ctxt, pogState, env); - list.stateUpdate(pogState, exp); + list.markIfUpdated(pogState, exp); if (patternBind.pattern != null) { @@ -99,7 +99,7 @@ else if (patternBind.bind instanceof POSeqBind) } ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); + if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); list.addAll(loops); return list; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java index f7d14e86a..eaf1d7b21 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java @@ -79,7 +79,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog POGStateList stateList = new POGStateList(); ProofObligationList obligations = ifExp.getProofObligations(ctxt, pogState, env); - obligations.stateUpdate(pogState, ifExp); + obligations.markIfUpdated(pogState, ifExp); ctxt.push(new POImpliesContext(ifExp)); obligations.addAll(thenStmt.getProofObligations(ctxt, stateList.addCopy(pogState), env)); @@ -90,7 +90,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POElseIfStatement stmt: elseList) { ProofObligationList oblist = stmt.elseIfExp.getProofObligations(ctxt, pogState, env); - oblist.stateUpdate(pogState, stmt.elseIfExp); + oblist.markIfUpdated(pogState, stmt.elseIfExp); oblist.addAll(stmt.thenStmt.getProofObligations(ctxt, stateList.addCopy(pogState), env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java index 03c49c712..69d4c2941 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java @@ -70,7 +70,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { ctxt.push(new POForAllContext(this)); ProofObligationList oblist = suchThat.getProofObligations(ctxt, pogState, env); - oblist.stateUpdate(pogState, suchThat); + oblist.markIfUpdated(pogState, suchThat); obligations.addAll(oblist); ctxt.pop(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java index a0cbabb42..f34822ffe 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java @@ -60,16 +60,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog obligations.add(new WhileLoopObligation(this, ctxt)); obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, exp); + obligations.markIfUpdated(pogState, exp); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); + return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 40534bf19..86d7d699c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -286,21 +286,21 @@ public ProofObligationList markUnchecked(String message) } /** - * Update the obligations in this list because of the current POGState and the state read - * by the expression. This is used by various statements and definitions, to suppress - * obligations that cannot yet be checked. + * Update the obligations in this list because of updates to the state read by the expression. + * This is used by various statements and definitions to suppress obligations that cannot + * yet be checked. */ - public void stateUpdate(POGState pstate, POExpression expression) + public void markIfUpdated(POGState pstate, POExpression expression) { - TCNameSet reads = expression.readsState(); + TCNameSet varreads = expression.readsState(); - if (!reads.isEmpty() && pstate.hasUpdatedState(reads)) + if (!varreads.isEmpty() && pstate.hasUpdatedState(varreads)) { - LexLocation at = pstate.getUpdatedLocation(reads); + LexLocation at = pstate.getUpdatedLocation(varreads); if (at == LexLocation.ANY) { - markUnchecked(ProofObligation.HAS_UPDATED_STATE + " " + reads); + markUnchecked(ProofObligation.HAS_UPDATED_STATE + " " + varreads); } else { From c0148da90e27085dbe7d366346a1bd6871e821d8 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 14 Nov 2024 13:05:34 +0000 Subject: [PATCH 07/18] Add more missing state updates --- .../com/fujitsu/vdmj/po/statements/POCasesStatement.java | 4 +++- .../com/fujitsu/vdmj/po/statements/POCyclesStatement.java | 5 ++++- .../com/fujitsu/vdmj/po/statements/PODurationStatement.java | 5 ++++- .../com/fujitsu/vdmj/po/statements/POForIndexStatement.java | 5 ++--- .../main/java/com/fujitsu/vdmj/pog/ProofObligationList.java | 4 +++- 5 files changed, 16 insertions(+), 7 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java index 8139a3b52..ce58f5684 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java @@ -75,7 +75,9 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = new ProofObligationList(); + ProofObligationList obligations = exp.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, exp); + POGStateList stateList = new POGStateList(); boolean hasIgnore = false; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCyclesStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCyclesStatement.java index 2cc90214f..a255216a4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCyclesStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCyclesStatement.java @@ -54,7 +54,10 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return statement.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = cycles.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, cycles); + obligations.addAll(statement.getProofObligations(ctxt, pogState, env)); + return obligations; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODurationStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODurationStatement.java index 582421918..00bb2c33a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODurationStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODurationStatement.java @@ -54,7 +54,10 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return statement.getProofObligations(ctxt, pogState, env); + ProofObligationList obligations = duration.getProofObligations(ctxt, pogState, env); + obligations.markIfUpdated(pogState, duration); + obligations.addAll(statement.getProofObligations(ctxt, pogState, env)); + return obligations; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java index 3970a4ab7..a65819ea6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java @@ -66,13 +66,12 @@ public String toString() public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = from.getProofObligations(ctxt, pogState, env); - obligations.addAll(to.getProofObligations(ctxt, pogState, env)); obligations.markIfUpdated(pogState, from); + obligations.addAll(to.getProofObligations(ctxt, pogState, env).markIfUpdated(pogState, to)); if (by != null) { - obligations.addAll(by.getProofObligations(ctxt, pogState, env)); - obligations.markIfUpdated(pogState, by); + obligations.addAll(by.getProofObligations(ctxt, pogState, env).markIfUpdated(pogState, by)); } ctxt.push(new POScopeContext()); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 86d7d699c..4092fded2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -290,7 +290,7 @@ public ProofObligationList markUnchecked(String message) * This is used by various statements and definitions to suppress obligations that cannot * yet be checked. */ - public void markIfUpdated(POGState pstate, POExpression expression) + public ProofObligationList markIfUpdated(POGState pstate, POExpression expression) { TCNameSet varreads = expression.readsState(); @@ -307,5 +307,7 @@ public void markIfUpdated(POGState pstate, POExpression expression) markUnchecked(ProofObligation.HAS_UPDATED_STATE + " " + at.toShortString()); } } + + return this; } } From f20934f01d943b2138df5a54deda53297aad53af Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 14 Nov 2024 15:21:06 +0000 Subject: [PATCH 08/18] Fixes for for-loops and cases statements --- .../vdmj/po/statements/POCasesStatement.java | 7 ++- .../vdmj/po/statements/POForAllStatement.java | 4 ++ .../po/statements/POForIndexStatement.java | 3 ++ .../vdmj/po/statements/POTrapStatement.java | 4 +- .../vdmj/pog/POForAllSequenceContext.java | 53 +++++++++++++++---- vdmj/src/main/resources/tc-po.mappings | 2 +- 6 files changed, 60 insertions(+), 13 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java index ce58f5684..4bbd629e4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java @@ -32,6 +32,7 @@ import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POGStateList; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; public class POCasesStatement extends POStatement @@ -40,14 +41,16 @@ public class POCasesStatement extends POStatement public final POExpression exp; public final POCaseStmtAlternativeList cases; public final POStatement others; + public final TCType expType; public POCasesStatement(LexLocation location, - POExpression exp, POCaseStmtAlternativeList cases, POStatement others) + POExpression exp, POCaseStmtAlternativeList cases, POStatement others, TCType expType) { super(location); this.exp = exp; this.cases = cases; this.others = others; + this.expType = expType; } @Override @@ -89,7 +92,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog } // Pushes PONotCaseContext - obligations.addAll(alt.getProofObligations(ctxt, stateList.addCopy(pogState), getStmttype(), env)); + obligations.addAll(alt.getProofObligations(ctxt, stateList.addCopy(pogState), expType, env)); } if (others != null && !hasIgnore) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java index 28cb55dfb..135722083 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POForAllSequenceContext; import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -62,7 +63,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); obligations.markIfUpdated(pogState, set); + ctxt.push(new POForAllSequenceContext(pattern, set)); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); + ctxt.pop(); + if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java index a65819ea6..1ad59fba2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POForAllSequenceContext; import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POScopeContext; import com.fujitsu.vdmj.pog.ProofObligation; @@ -75,10 +76,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog } ctxt.push(new POScopeContext()); + ctxt.push(new POForAllSequenceContext(var, from, to, by)); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); ctxt.pop(); + ctxt.pop(); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java index 83595e303..dc8cb6602 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java @@ -32,6 +32,7 @@ import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POGState; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SeqMemberObligation; import com.fujitsu.vdmj.pog.SetMemberObligation; @@ -89,7 +90,8 @@ else if (patternBind.bind instanceof POSeqBind) // The "with" clause sees the "body" state updates, potentially list.addAll(body.getProofObligations(ctxt, pogState, env)); - list.addAll(with.getProofObligations(ctxt, pogState, env)); + // We don't know the exception type to match against the trap pattern/bind, so unchecked + list.addAll(with.getProofObligations(ctxt, pogState, env).markUnchecked(ProofObligation.NOT_YET_SUPPORTED)); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java index 660a79124..91811162d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java @@ -25,17 +25,52 @@ package com.fujitsu.vdmj.pog; import com.fujitsu.vdmj.po.expressions.POExpression; -import com.fujitsu.vdmj.po.patterns.POBind; +import com.fujitsu.vdmj.po.patterns.POPattern; +import com.fujitsu.vdmj.po.patterns.POSeqBind; +import com.fujitsu.vdmj.po.patterns.POSetBind; +import com.fujitsu.vdmj.tc.lex.TCNameToken; public class POForAllSequenceContext extends POContext { - public final POBind bind; - public final POExpression sequence; + public final String pattern; + public final String exp; + public final String seqset; - public POForAllSequenceContext(POBind bind, POExpression exp) + public POForAllSequenceContext(POSetBind bind, POExpression exp) { - this.bind = bind; - this.sequence = exp; + this.pattern = bind.pattern.toString(); + this.exp = exp.toString(); + this.seqset = " in set "; + } + + public POForAllSequenceContext(POSeqBind bind, POExpression exp) + { + this.pattern = bind.pattern.toString(); + this.exp = exp.toString(); + this.seqset = " in seq "; + } + + public POForAllSequenceContext(POPattern pattern, POExpression exp) + { + this.pattern = pattern.toString(); + this.exp = exp.toString(); + this.seqset = " in set "; + } + + public POForAllSequenceContext(TCNameToken var, POExpression from, POExpression to, POExpression by) + { + this.pattern = var.getName(); + + if (by != null) + { + this.exp = String.format("[ %1$s + $var * %3$s | $var in set {0, ..., (%2$s - %1$s) / %3$s} ]", from, to, by); + } + else + { + this.exp = String.format("[ $var | $var in set {%1$s, ..., %2$s} ]", from, to); + } + + this.seqset = " in seq "; } @Override @@ -44,9 +79,9 @@ public String getSource() StringBuilder sb = new StringBuilder(); sb.append("forall "); - sb.append(bind.pattern); - sb.append(" in set elems "); - sb.append(sequence); + sb.append(pattern); + sb.append(seqset); + sb.append(exp); sb.append(" & "); return sb.toString(); diff --git a/vdmj/src/main/resources/tc-po.mappings b/vdmj/src/main/resources/tc-po.mappings index 7a7f3389b..745a91e5b 100644 --- a/vdmj/src/main/resources/tc-po.mappings +++ b/vdmj/src/main/resources/tc-po.mappings @@ -241,7 +241,7 @@ map TCAtomicStatement{location, assignments, stmttype} to POAtomicStatement(loca map TCBlockStatement{location, assignmentDefs, statements, stmttype} to POBlockStatement(location, assignmentDefs, statements) set stmttype; map TCCallObjectStatement{designator, classname, fieldname, args, fdef, stmttype} to POCallObjectStatement(designator, classname, fieldname, args, fdef) set stmttype; map TCCallStatement{name, args, opdef, stmttype} to POCallStatement(name, args, opdef) set stmttype; -map TCCasesStatement{location, exp, cases, others, stmttype} to POCasesStatement(location, exp, cases, others) set stmttype; +map TCCasesStatement{location, exp, cases, others, expType, stmttype} to POCasesStatement(location, exp, cases, others, expType) set stmttype; map TCCaseStmtAlternative{exp, pattern, statement} to POCaseStmtAlternative(exp, pattern, statement); map TCCaseStmtAlternativeList{} to POCaseStmtAlternativeList(this); map TCClassInvariantStatement{name, invdefs, stmttype} to POClassInvariantStatement(name, invdefs) set stmttype; From f768bc29fd3feadf411947ddb8d403daacff6779 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 14 Nov 2024 16:15:35 +0000 Subject: [PATCH 09/18] Corrections to for loop POs --- .../vdmj/po/statements/POForAllStatement.java | 2 +- .../statements/POForPatternBindStatement.java | 25 ++++++++++--------- .../visitors/POLeafStatementVisitor.java | 2 +- .../vdmj/pog/POForAllSequenceContext.java | 22 +++++++++++----- .../com/fujitsu/vdmj/runtime/Interpreter.java | 2 +- 5 files changed, 32 insertions(+), 21 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java index 135722083..ddc868a29 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java @@ -63,7 +63,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); obligations.markIfUpdated(pogState, set); - ctxt.push(new POForAllSequenceContext(pattern, set)); + ctxt.push(new POForAllSequenceContext(pattern, set, " in set ")); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java index 71148fd77..1795420bc 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java @@ -45,7 +45,7 @@ public class POForPatternBindStatement extends POStatement private static final long serialVersionUID = 1L; public final POPatternBind patternBind; public final boolean reverse; - public final POExpression exp; + public final POExpression sequence; public final POStatement statement; public POForPatternBindStatement(LexLocation location, @@ -54,7 +54,7 @@ public POForPatternBindStatement(LexLocation location, super(location); this.patternBind = patternBind; this.reverse = reverse; - this.exp = exp; + this.sequence = exp; this.statement = body; } @@ -62,43 +62,44 @@ public POForPatternBindStatement(LexLocation location, public String toString() { return "for " + patternBind + " in " + - (reverse ? " reverse " : "") + exp + " do\n" + statement; + (reverse ? " reverse " : "") + sequence + " do\n" + statement; } @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = exp.getProofObligations(ctxt, pogState, env); - list.markIfUpdated(pogState, exp); - + ProofObligationList list = sequence.getProofObligations(ctxt, pogState, env); + list.markIfUpdated(pogState, sequence); + if (patternBind.pattern != null) { - // Nothing to do + ctxt.push(new POForAllSequenceContext(patternBind.pattern, sequence)); } else if (patternBind.bind instanceof POTypeBind) { - // Nothing to do + POTypeBind bind = (POTypeBind)patternBind.bind; + ctxt.push(new POForAllSequenceContext(bind, sequence)); } else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); - ctxt.push(new POForAllSequenceContext(bind, exp)); + ctxt.push(new POForAllSequenceContext(bind, sequence)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); - ctxt.pop(); } else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); - ctxt.push(new POForAllSequenceContext(bind, exp)); + ctxt.push(new POForAllSequenceContext(bind, sequence)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); - ctxt.pop(); } ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); + ctxt.pop(); + if (statement.updatesState()) loops.markUnchecked(ProofObligation.LOOP_STATEMENT); list.addAll(loops); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POLeafStatementVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POLeafStatementVisitor.java index 04a4744b8..b99d1204b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POLeafStatementVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POLeafStatementVisitor.java @@ -301,7 +301,7 @@ public C caseForPatternBindStatement(POForPatternBindStatement node, S arg) C all = (allNodes) ? caseNonLeafNode(node, arg) : newCollection(); all.addAll(visitorSet.applyPatternVisitor(node.patternBind.pattern, arg)); all.addAll(visitorSet.applyBindVisitor(node.patternBind.bind, arg)); - all.addAll(visitorSet.applyExpressionVisitor(node.exp, arg)); + all.addAll(visitorSet.applyExpressionVisitor(node.sequence, arg)); all.addAll(node.statement.apply(this, arg)); return all; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java index 91811162d..d0e496cc0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POForAllSequenceContext.java @@ -28,33 +28,38 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POSeqBind; import com.fujitsu.vdmj.po.patterns.POSetBind; +import com.fujitsu.vdmj.po.patterns.POTypeBind; import com.fujitsu.vdmj.tc.lex.TCNameToken; public class POForAllSequenceContext extends POContext { public final String pattern; public final String exp; - public final String seqset; + + private String seqset = " in seq "; public POForAllSequenceContext(POSetBind bind, POExpression exp) { this.pattern = bind.pattern.toString(); this.exp = exp.toString(); - this.seqset = " in set "; } public POForAllSequenceContext(POSeqBind bind, POExpression exp) { this.pattern = bind.pattern.toString(); this.exp = exp.toString(); - this.seqset = " in seq "; + } + + public POForAllSequenceContext(POTypeBind bind, POExpression exp) + { + this.pattern = bind.pattern.toString(); + this.exp = exp.toString(); } public POForAllSequenceContext(POPattern pattern, POExpression exp) { this.pattern = pattern.toString(); this.exp = exp.toString(); - this.seqset = " in set "; } public POForAllSequenceContext(TCNameToken var, POExpression from, POExpression to, POExpression by) @@ -69,8 +74,13 @@ public POForAllSequenceContext(TCNameToken var, POExpression from, POExpression { this.exp = String.format("[ $var | $var in set {%1$s, ..., %2$s} ]", from, to); } - - this.seqset = " in seq "; + } + + public POForAllSequenceContext(POPattern pattern, POExpression set, String seqset) + { + this.pattern = pattern.toString(); + this.exp = set.toString(); + this.seqset = seqset; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java index 75f125367..427ea74e0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java @@ -414,7 +414,7 @@ public Breakpoint setBreakpoint(INExpression exp, String condition) throws Excep * Set an exception catchpoint. This stops execution at the point that a matching * exception is thrown. * - * @param exp The exception value(s) at which to stop, or null for any exception. + * @param sequence The exception value(s) at which to stop, or null for any exception. * @return The Breakpoint object created. * @throws Exception */ From f0dc8c3fe5c8b6d093557e46c8aaceba226c1a5f Mon Sep 17 00:00:00 2001 From: nick_battle Date: Thu, 14 Nov 2024 22:03:54 +0000 Subject: [PATCH 10/18] Improve POs for ForAllPatternBindStatements --- .../po/statements/POForPatternBindStatement.java | 15 ++++++++++++++- .../tc/statements/TCForPatternBindStatement.java | 8 +++++--- vdmj/src/main/resources/tc-po.mappings | 2 +- 3 files changed, 20 insertions(+), 5 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java index 1795420bc..7787ff2b7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java @@ -38,7 +38,11 @@ import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SeqMemberObligation; import com.fujitsu.vdmj.pog.SetMemberObligation; +import com.fujitsu.vdmj.pog.SubTypeObligation; +import com.fujitsu.vdmj.tc.types.TCSeqType; +import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; +import com.fujitsu.vdmj.typechecker.TypeComparator; public class POForPatternBindStatement extends POStatement { @@ -46,15 +50,17 @@ public class POForPatternBindStatement extends POStatement public final POPatternBind patternBind; public final boolean reverse; public final POExpression sequence; + public final TCType expType; public final POStatement statement; public POForPatternBindStatement(LexLocation location, - POPatternBind patternBind, boolean reverse, POExpression exp, POStatement body) + POPatternBind patternBind, boolean reverse, POExpression exp, TCType expType, POStatement body) { super(location); this.patternBind = patternBind; this.reverse = reverse; this.sequence = exp; + this.expType = expType; this.statement = body; } @@ -79,6 +85,13 @@ else if (patternBind.bind instanceof POTypeBind) { POTypeBind bind = (POTypeBind)patternBind.bind; ctxt.push(new POForAllSequenceContext(bind, sequence)); + + TCSeqType s = expType.isSeq(location) ? expType.getSeq() : null; + + if (s != null && !TypeComparator.isSubType(s.seqof, bind.type)) + { + list.add(new SubTypeObligation(bind.pattern.getMatchingExpression(), bind.type, s.seqof, ctxt)); + } } else if (patternBind.bind instanceof POSetBind) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCForPatternBindStatement.java index a6fe900bc..c2de42b2e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/statements/TCForPatternBindStatement.java @@ -46,6 +46,8 @@ public class TCForPatternBindStatement extends TCStatement public final boolean reverse; public final TCExpression exp; public final TCStatement statement; + + private TCType expType; public TCForPatternBindStatement(LexLocation location, TCPatternBind patternBind, boolean reverse, TCExpression exp, TCStatement body) @@ -67,12 +69,12 @@ public String toString() @Override public TCType typeCheck(Environment base, NameScope scope, TCType constraint, boolean mandatory) { - TCType stype = exp.typeCheck(base, null, scope, null); + expType = exp.typeCheck(base, null, scope, null); Environment local = base; - if (stype.isSeq(location)) + if (expType.isSeq(location)) { - TCSeqType st = stype.getSeq(); + TCSeqType st = expType.getSeq(); patternBind.typeCheck(base, scope, st.seqof); TCDefinitionList defs = patternBind.getDefinitions(); defs.typeCheck(base, scope); diff --git a/vdmj/src/main/resources/tc-po.mappings b/vdmj/src/main/resources/tc-po.mappings index 745a91e5b..eec764f8d 100644 --- a/vdmj/src/main/resources/tc-po.mappings +++ b/vdmj/src/main/resources/tc-po.mappings @@ -259,7 +259,7 @@ map TCExternalClauseList{} to POExternalClauseList(this); map TCFieldDesignator{object, field} to POFieldDesignator(object, field); map TCForAllStatement{location, pattern, set, statement, stmttype} to POForAllStatement(location, pattern, set, statement) set stmttype; map TCForIndexStatement{location, var, from, to, by, statement, stmttype} to POForIndexStatement(location, var, from, to, by, statement) set stmttype; -map TCForPatternBindStatement{location, patternBind, reverse, exp, statement, stmttype} to POForPatternBindStatement(location, patternBind, reverse, exp, statement) set stmttype; +map TCForPatternBindStatement{location, patternBind, reverse, exp, expType, statement, stmttype} to POForPatternBindStatement(location, patternBind, reverse, exp, expType, statement) set stmttype; map TCIdentifierDesignator{name} to POIdentifierDesignator(name); map TCIfStatement{location, ifExp, thenStmt, elseList, elseStmt, stmttype} to POIfStatement(location, ifExp, thenStmt, elseList, elseStmt) set stmttype; map TCLetBeStStatement{location, bind, suchThat, statement, stmttype} to POLetBeStStatement(location, bind, suchThat, statement) set stmttype; From 7e216ee4c1e4412ba790604ccde6d02a71b2021a Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 16 Nov 2024 11:53:22 +0000 Subject: [PATCH 11/18] Set a MultiModule environment for qcrun evaluations --- lsp/src/main/java/dap/ExpressionExecutor.java | 15 ++++++++++++--- .../java/quickcheck/commands/QCRunCommand.java | 18 ++++++++++++++++++ .../quickcheck/commands/QCRunLSPCommand.java | 13 +++++++++++-- .../fujitsu/vdmj/runtime/ClassInterpreter.java | 6 ++++++ .../com/fujitsu/vdmj/runtime/Interpreter.java | 6 ++++++ .../vdmj/runtime/ModuleInterpreter.java | 6 ++++++ 6 files changed, 59 insertions(+), 5 deletions(-) diff --git a/lsp/src/main/java/dap/ExpressionExecutor.java b/lsp/src/main/java/dap/ExpressionExecutor.java index aa0fe33b2..06c3f996c 100644 --- a/lsp/src/main/java/dap/ExpressionExecutor.java +++ b/lsp/src/main/java/dap/ExpressionExecutor.java @@ -27,6 +27,8 @@ import java.io.IOException; import com.fujitsu.vdmj.config.Properties; +import com.fujitsu.vdmj.runtime.Interpreter; +import com.fujitsu.vdmj.typechecker.Environment; import json.JSONObject; @@ -34,18 +36,21 @@ public class ExpressionExecutor extends AsyncExecutor { private final String expression; private final boolean maximal; + private final Environment env; + private String answer; - public ExpressionExecutor(String id, DAPRequest request, String expression, boolean maximal) + public ExpressionExecutor(String id, DAPRequest request, String expression, boolean maximal, Environment env) { super(id, request); this.expression = expression; this.maximal = maximal; + this.env = env; } public ExpressionExecutor(String id, DAPRequest request, String expression) { - this(id, request, expression, false); + this(id, request, expression, false, null); } @Override @@ -58,15 +63,19 @@ protected void head() protected void exec() throws Exception { boolean saved = Properties.parser_maximal_types; // Used by qcrun + Interpreter interpreter = manager.getInterpreter(); + Environment saved2 = interpreter.getGlobalEnvironment(); try { Properties.parser_maximal_types = maximal; - answer = manager.getInterpreter().execute(expression).toString(); + if (env != null) interpreter.setGlobalEnvironment(env); + answer = interpreter.execute(expression).toString(); } finally { Properties.parser_maximal_types = saved; + interpreter.setGlobalEnvironment(saved2); } } diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java index 45a170354..fc8dd3d8f 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java @@ -26,14 +26,18 @@ import static com.fujitsu.vdmj.plugins.PluginConsole.println; +import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.config.Properties; +import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.plugins.AnalysisCommand; import com.fujitsu.vdmj.plugins.analyses.POPlugin; import com.fujitsu.vdmj.plugins.commands.PrintCommand; +import com.fujitsu.vdmj.po.modules.MultiModuleEnvironment; 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 com.fujitsu.vdmj.typechecker.Environment; /** * Launch a "print" command for a PO counterexample or witness. @@ -130,16 +134,30 @@ else if (obligation.kind.isStandAlone()) // Temporarily allow maximal parsing, for invariant POs boolean saved = Properties.parser_maximal_types; + Interpreter interpreter = Interpreter.getInstance(); + Environment saved2 = interpreter.getGlobalEnvironment(); try { Properties.parser_maximal_types = true; + + // Set the default Environment to allow complex launches to run which + // use symbols outside the current module in VDM-SL. The default is + // put back afterwards! + if (Settings.dialect == Dialect.VDM_SL) + { + POPlugin tc = registry.getPlugin("PO"); + MultiModuleEnvironment menv = new MultiModuleEnvironment(tc.getPO()); + interpreter.setGlobalEnvironment(menv); + } + PrintCommand cmd = new PrintCommand(pline); return cmd.run(pline); } finally { Properties.parser_maximal_types = saved; + interpreter.setGlobalEnvironment(saved2); } } else diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java index 0e0d9f2f7..363f8ca77 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java @@ -25,10 +25,14 @@ import static com.fujitsu.vdmj.plugins.PluginConsole.println; +import com.fujitsu.vdmj.Settings; +import com.fujitsu.vdmj.lex.Dialect; +import com.fujitsu.vdmj.po.modules.MultiModuleEnvironment; 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 com.fujitsu.vdmj.typechecker.Environment; import dap.DAPMessageList; import dap.DAPRequest; @@ -130,8 +134,13 @@ else if (obligation.kind.isStandAlone()) if (launch != null) { println("=> print " + launch); - // This allows maximal types to parse, for invariant POs - ExpressionExecutor executor = new ExpressionExecutor("print", request, launch, true); + + // This allows maximal types to parse, for invariant POs, and allows POs to + // reference types outside their module in VDM-SL. + Environment env = (Settings.dialect == Dialect.VDM_SL) ? + new MultiModuleEnvironment(po.getPO()) : null; + + ExpressionExecutor executor = new ExpressionExecutor("print", request, launch, true, env); executor.start(); return null; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java index 3f5fb18e7..0bd31a82b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java @@ -153,6 +153,12 @@ public Environment getGlobalEnvironment() return env; } + + @Override + public void setGlobalEnvironment(Environment env) + { + // Ignored - global env created each time above + } @Override public String getDefaultName() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java index 427ea74e0..542fac07c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java @@ -133,6 +133,12 @@ public RootContext getInitialContext() * in VDM++ it is the global class environment. */ abstract public Environment getGlobalEnvironment(); + + /** + * Set the global environment. This is used rarely, in cases where the usual + * default is not appropriate. + */ + abstract public void setGlobalEnvironment(Environment env); /** * @return The Interpreter instance. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java index b7441edcc..462573a51 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java @@ -162,6 +162,12 @@ public Environment getGlobalEnvironment() { return defaultEnvironment; } + + @Override + public void setGlobalEnvironment(Environment env) + { + defaultEnvironment = env; + } /** * @return The current default module name. From 8d8aed0c2aa141016ba31dc59a96711c62940f91 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 17 Nov 2024 09:50:04 +0000 Subject: [PATCH 12/18] Change name of PO code lens --- lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java index 896e5cf0c..cbeba4a4e 100644 --- a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java @@ -68,7 +68,7 @@ private JSONArray launchArgs(ProofObligation po, String defaultName, boolean deb ApplyCall apply = factory.getCexApply(); - launchArgs.put("name", (debug ? "Debug " : "Launch ") + apply.applyName); + launchArgs.put("name", "PO #" + po.number); launchArgs.put("defaultName", defaultName); launchArgs.put("type", "vdm"); launchArgs.put("request", "launch"); From 166fe86b2c46b4bdf0354d0d9a7cd60fd8999bdd Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 17 Nov 2024 10:24:46 +0000 Subject: [PATCH 13/18] Neater way to set execute/typeCheck environment --- lsp/src/main/java/dap/ExpressionExecutor.java | 11 +++++------ .../java/quickcheck/commands/QCRunCommand.java | 9 ++++----- .../vdmj/plugins/commands/PrintCommand.java | 12 +++++++++++- .../fujitsu/vdmj/runtime/ClassInterpreter.java | 12 ++++++------ .../com/fujitsu/vdmj/runtime/Interpreter.java | 18 +++++++++--------- .../vdmj/runtime/ModuleInterpreter.java | 14 +++++++------- 6 files changed, 42 insertions(+), 34 deletions(-) diff --git a/lsp/src/main/java/dap/ExpressionExecutor.java b/lsp/src/main/java/dap/ExpressionExecutor.java index 06c3f996c..b96b5ec4c 100644 --- a/lsp/src/main/java/dap/ExpressionExecutor.java +++ b/lsp/src/main/java/dap/ExpressionExecutor.java @@ -36,8 +36,8 @@ public class ExpressionExecutor extends AsyncExecutor { private final String expression; private final boolean maximal; - private final Environment env; - + + private Environment env = null; private String answer; public ExpressionExecutor(String id, DAPRequest request, String expression, boolean maximal, Environment env) @@ -64,18 +64,17 @@ protected void exec() throws Exception { boolean saved = Properties.parser_maximal_types; // Used by qcrun Interpreter interpreter = manager.getInterpreter(); - Environment saved2 = interpreter.getGlobalEnvironment(); + + if (env == null) env = interpreter.getGlobalEnvironment(); try { Properties.parser_maximal_types = maximal; - if (env != null) interpreter.setGlobalEnvironment(env); - answer = interpreter.execute(expression).toString(); + answer = interpreter.execute(expression, env).toString(); } finally { Properties.parser_maximal_types = saved; - interpreter.setGlobalEnvironment(saved2); } } diff --git a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java index fc8dd3d8f..0df7e1042 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java @@ -135,7 +135,6 @@ else if (obligation.kind.isStandAlone()) // Temporarily allow maximal parsing, for invariant POs boolean saved = Properties.parser_maximal_types; Interpreter interpreter = Interpreter.getInstance(); - Environment saved2 = interpreter.getGlobalEnvironment(); try { @@ -144,20 +143,20 @@ else if (obligation.kind.isStandAlone()) // Set the default Environment to allow complex launches to run which // use symbols outside the current module in VDM-SL. The default is // put back afterwards! + Environment menv = interpreter.getGlobalEnvironment(); + if (Settings.dialect == Dialect.VDM_SL) { POPlugin tc = registry.getPlugin("PO"); - MultiModuleEnvironment menv = new MultiModuleEnvironment(tc.getPO()); - interpreter.setGlobalEnvironment(menv); + menv = new MultiModuleEnvironment(tc.getPO()); } - PrintCommand cmd = new PrintCommand(pline); + PrintCommand cmd = new PrintCommand(pline, menv); return cmd.run(pline); } finally { Properties.parser_maximal_types = saved; - interpreter.setGlobalEnvironment(saved2); } } else diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PrintCommand.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PrintCommand.java index b11572b3f..cbf97427a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PrintCommand.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PrintCommand.java @@ -36,6 +36,7 @@ import com.fujitsu.vdmj.runtime.DebuggerException; import com.fujitsu.vdmj.runtime.Interpreter; import com.fujitsu.vdmj.syntax.ParserException; +import com.fujitsu.vdmj.typechecker.Environment; import com.fujitsu.vdmj.values.Value; public class PrintCommand extends AnalysisCommand @@ -43,8 +44,15 @@ public class PrintCommand extends AnalysisCommand private final static String CMD = "print "; private final static String USAGE = "Usage: " + CMD; public final static String HELP = CMD + " - evaluate an expression"; + + private final Environment env; public PrintCommand(String line) + { + this(line, Interpreter.getInstance().getGlobalEnvironment()); + } + + public PrintCommand(String line, Environment env) { super(line); @@ -52,6 +60,8 @@ public PrintCommand(String line) { throw new IllegalArgumentException(USAGE); } + + this.env = env; } @Override @@ -74,7 +84,7 @@ public String run(String line) watch.start(); long before = System.currentTimeMillis(); - Value v = Interpreter.getInstance().execute(expression); + Value v = Interpreter.getInstance().execute(expression, env); long after = System.currentTimeMillis(); println("= " + v); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java index 0bd31a82b..2591ffe44 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java @@ -153,12 +153,6 @@ public Environment getGlobalEnvironment() return env; } - - @Override - public void setGlobalEnvironment(Environment env) - { - // Ignored - global env created each time above - } @Override public String getDefaultName() @@ -305,6 +299,12 @@ private Value execute(INExpression inex) throws Exception */ @Override public Value execute(String line) throws Exception + { + return execute(line, getGlobalEnvironment()); + } + + @Override + public Value execute(String line, Environment env) throws Exception { TCExpression expr = parseExpression(line, getDefaultName()); typeCheck(expr); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java index 542fac07c..ac5faaf6d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java @@ -133,12 +133,6 @@ public RootContext getInitialContext() * in VDM++ it is the global class environment. */ abstract public Environment getGlobalEnvironment(); - - /** - * Set the global environment. This is used rarely, in cases where the usual - * default is not appropriate. - */ - abstract public void setGlobalEnvironment(Environment env); /** * @return The Interpreter instance. @@ -198,6 +192,7 @@ public static Interpreter getInstance() * @throws Exception Parser, type checking or runtime errors. */ abstract public Value execute(String line) throws Exception; + abstract public Value execute(String line, Environment env) throws Exception; /** * Parse the line passed, and evaluate it as an expression in the context @@ -498,9 +493,14 @@ public void clearBreakpointHits() abstract protected TCExpression parseExpression(String line, String module) throws Exception; /** - * Type check a TC expression tree passed. + * Type check a TC expression tree passed, optionally in a given environment. */ public TCType typeCheck(TCNode tree) throws Exception + { + return typeCheck(tree, getGlobalEnvironment()); + } + + public TCType typeCheck(TCNode tree, Environment env) throws Exception { TypeChecker.clearErrors(); TCType type = null; @@ -508,12 +508,12 @@ public TCType typeCheck(TCNode tree) throws Exception if (tree instanceof TCExpression) { TCExpression exp = (TCExpression)tree; - type = exp.typeCheck(getGlobalEnvironment(), null, NameScope.NAMESANDSTATE, null); + type = exp.typeCheck(env, null, NameScope.NAMESANDSTATE, null); } else if (tree instanceof TCStatement) { TCStatement stmt = (TCStatement)tree; - type = stmt.typeCheck(getGlobalEnvironment(), NameScope.NAMESANDSTATE, null, false); + type = stmt.typeCheck(env, NameScope.NAMESANDSTATE, null, false); } else { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java index 462573a51..c9404dba4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java @@ -162,12 +162,6 @@ public Environment getGlobalEnvironment() { return defaultEnvironment; } - - @Override - public void setGlobalEnvironment(Environment env) - { - defaultEnvironment = env; - } /** * @return The current default module name. @@ -284,9 +278,15 @@ protected TCExpression parseExpression(String line, String module) throws Except */ @Override public Value execute(String line) throws Exception + { + return execute(line, getGlobalEnvironment()); + } + + @Override + public Value execute(String line, Environment env) throws Exception { TCExpression expr = parseExpression(line, getDefaultName()); - typeCheck(expr); + typeCheck(expr, env); Context mainContext = new StateContext(defaultModule.name.getLocation(), "module scope", null, defaultModule.getStateContext()); From ad2cb83862a9e927af1d864c9926bc992368606f Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 18 Nov 2024 12:26:05 +0000 Subject: [PATCH 14/18] Add clearIncludes and clean up timeout handling --- quickcheck/src/main/java/quickcheck/commands/QCConsole.java | 5 +++++ .../src/main/java/quickcheck/commands/QuickCheckCommand.java | 1 + .../main/java/quickcheck/commands/QuickCheckLSPCommand.java | 1 + 3 files changed, 7 insertions(+) diff --git a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java index f1c8c8da3..7555df5d9 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java @@ -64,6 +64,11 @@ public static List getIncludes() return includes; } + public static void clearIncludes() + { + includes.clear(); + } + public static void setVerbose(boolean verbose) { QCConsole.verbose = verbose; diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java index 04a20d3a6..47c2c2ec9 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java @@ -87,6 +87,7 @@ public String run(String line) QCConsole.setQuiet(false); QCConsole.setVerbose(false); + QCConsole.clearIncludes(); for (int i=0; i < arglist.size(); i++) // Should just be POs, or -? -help { diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java index b46a86219..056027b71 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java @@ -89,6 +89,7 @@ private DAPMessageList setup(DAPRequest request) QCConsole.setQuiet(false); QCConsole.setVerbose(false); + QCConsole.clearIncludes(); for (int i=0; i < arglist.size(); i++) // Should just be POs, or -? -help { From 37b53f9a131dff24d78cfe51ed599e8430f1adc7 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 18 Nov 2024 13:38:11 +0000 Subject: [PATCH 15/18] Clean up measure data on cancel/timeout --- .../src/main/java/quickcheck/QuickCheck.java | 2 +- vdmj/documentation/MESSAGES | 4 ++- .../com/fujitsu/vdmj/runtime/Breakpoint.java | 6 ++-- .../vdmj/runtime/ContextException.java | 2 +- .../fujitsu/vdmj/values/FunctionValue.java | 28 +++++++++++++++++++ 5 files changed, 37 insertions(+), 5 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 43baa40f3..19b2db5ac 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -511,7 +511,7 @@ else if (sresults.disprovedBy != null) } catch (ContextException e) { - if (e.rawMessage.equals("Execution cancelled")) + if (e.isUserCancel()) { execResult = new BooleanValue(false); timedOut = true; diff --git a/vdmj/documentation/MESSAGES b/vdmj/documentation/MESSAGES index 6946eb68f..802a360eb 100644 --- a/vdmj/documentation/MESSAGES +++ b/vdmj/documentation/MESSAGES @@ -951,9 +951,11 @@ as the expected and actual values. 4172, "Values cannot be compared: , " 4173, "Unknown annotation @" 4174, "Stack overflow" -4175, "Execution cancelled" +4175, - 4176, "Cannot evaluate power set of size " 4177, "Not permitted during initialization" +... +4999, "Execution cancelled" 5000, "Definition not used" 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 a2611d762..331c269ee 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java @@ -55,7 +55,7 @@ public class Breakpoint implements Serializable { private static final long serialVersionUID = 1L; - + /** The location of the breakpoint. */ public final LexLocation location; /** The number of the breakpoint. */ @@ -81,6 +81,8 @@ public class Breakpoint implements Serializable public int bpType = SOURCE; public static final int SOURCE = 0; // A file:line source breakpoint public static final int FUNCTION = 1; // A function or operation name breakpoint + + public static final int USER_CANCEL = 4999; // Special message for timeouts public Breakpoint(LexLocation location) { @@ -229,7 +231,7 @@ public void check(LexLocation execl, Context ctxt) case TERMINATE: setExecInterrupt(Breakpoint.NONE); - throw new ContextException(4175, "Execution cancelled", location, ctxt); + throw new ContextException(USER_CANCEL, "Execution cancelled", location, ctxt); } ThreadState state = ctxt.threadState; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java index 3c56bd98a..62ea70248 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java @@ -61,6 +61,6 @@ public boolean isStackOverflow() public boolean isUserCancel() { - return number == 4175; + return number == Breakpoint.USER_CANCEL; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java index d8eadea65..65f14514a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java @@ -317,6 +317,20 @@ public Value eval( ValueList args = new ValueList(arg); return eval(from, args, ctxt, null); } + catch (ContextException e) + { + if (e.isUserCancel()) + { + if (Settings.measureChecks && measure != null) + { + this.measureValues.clear(); + measure.measuringThreads.clear(); + measure.callingThreads.clear(); + } + } + + throw e; + } catch (StackOverflowError e) { throw new ContextException(4174, "Stack overflow", location, ctxt); @@ -330,6 +344,20 @@ public Value eval( { return eval(from, argValues, ctxt, null); } + catch (ContextException e) + { + if (e.isUserCancel()) + { + if (Settings.measureChecks && measure != null) + { + this.measureValues.clear(); + measure.measuringThreads.clear(); + measure.callingThreads.clear(); + } + } + + throw e; + } catch (StackOverflowError e) { throw new ContextException(4174, "Stack overflow", location, ctxt); From 5f39103860bd2afec7a122d60e971ad920d8bd38 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 18 Nov 2024 14:11:18 +0000 Subject: [PATCH 16/18] Cleaner stack overflow exceptions --- vdmj/documentation/MESSAGES | 3 +- .../vdmj/runtime/ContextException.java | 4 ++- .../fujitsu/vdmj/values/FunctionValue.java | 34 +++++++++++-------- .../fujitsu/vdmj/values/OperationValue.java | 2 +- 4 files changed, 26 insertions(+), 17 deletions(-) diff --git a/vdmj/documentation/MESSAGES b/vdmj/documentation/MESSAGES index 802a360eb..7b8ca5886 100644 --- a/vdmj/documentation/MESSAGES +++ b/vdmj/documentation/MESSAGES @@ -950,11 +950,12 @@ as the expected and actual values. 4171, "Cannot convert to " 4172, "Values cannot be compared: , " 4173, "Unknown annotation @" -4174, "Stack overflow" +4174, - 4175, - 4176, "Cannot evaluate power set of size " 4177, "Not permitted during initialization" ... +4998, "Stack overflow" 4999, "Execution cancelled" diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java index 62ea70248..d42d62d24 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java @@ -29,6 +29,8 @@ @SuppressWarnings("serial") public class ContextException extends RuntimeException { + public static final int STACK_OVERFLOW = 4998; + public final LexLocation location; public final Context ctxt; public final int number; @@ -56,7 +58,7 @@ public String toString() public boolean isStackOverflow() { - return number == 4174; + return number == STACK_OVERFLOW; } public boolean isUserCancel() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java index 65f14514a..25b47fba2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java @@ -308,6 +308,20 @@ public void setSelf(ObjectValue self) } } } + + /** + * This is used during catastrohpic exception handling to clear any data held + * from run to run that may need to be reset. + */ + private void clearData() + { + if (Settings.measureChecks && measure != null) + { + this.measureValues.clear(); + measure.measuringThreads.clear(); + measure.callingThreads.clear(); + } + } public Value eval( LexLocation from, Value arg, Context ctxt) throws ValueException @@ -321,19 +335,15 @@ public Value eval( { if (e.isUserCancel()) { - if (Settings.measureChecks && measure != null) - { - this.measureValues.clear(); - measure.measuringThreads.clear(); - measure.callingThreads.clear(); - } + clearData(); } throw e; } catch (StackOverflowError e) { - throw new ContextException(4174, "Stack overflow", location, ctxt); + clearData(); + throw new ContextException(ContextException.STACK_OVERFLOW, "Stack overflow", location, ctxt); } } @@ -348,19 +358,15 @@ public Value eval( { if (e.isUserCancel()) { - if (Settings.measureChecks && measure != null) - { - this.measureValues.clear(); - measure.measuringThreads.clear(); - measure.callingThreads.clear(); - } + clearData(); } throw e; } catch (StackOverflowError e) { - throw new ContextException(4174, "Stack overflow", location, ctxt); + clearData(); + throw new ContextException(ContextException.STACK_OVERFLOW, "Stack overflow", location, ctxt); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java index d4860c1ca..a56a79374 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java @@ -239,7 +239,7 @@ public Value eval(LexLocation from, ValueList argValues, Context ctxt) } catch (StackOverflowError e) { - throw new ContextException(4174, "Stack overflow", from, ctxt); + throw new ContextException(ContextException.STACK_OVERFLOW, "Stack overflow", from, ctxt); } } From 5a97255c469d29a13e8984d320c9801a8fd941b9 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 19 Nov 2024 11:19:26 +0000 Subject: [PATCH 17/18] Fix for opaque types in launch factory --- vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java index ed6dc2d70..826a5033c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java @@ -283,7 +283,8 @@ private String paramMatch(POPattern p, TCType type, Context ctxt) throws Excepti else { List lastArgs = applyCall.applyArgs.get(applyCall.applyArgs.size() - 1); - lastArgs.add(new ApplyArg(p.toString(), type.toString(), result)); + String stype = type.toString().replace(" /* opaque */", ""); // HACK! + lastArgs.add(new ApplyArg(p.toString(), stype, result)); return result; } } From 6455805c5aee966cc8004a7b765463d489321607 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Tue, 19 Nov 2024 15:29:05 +0000 Subject: [PATCH 18/18] Tidy user cancel and stack overflow again --- .../java/com/fujitsu/vdmj/runtime/Breakpoint.java | 4 +--- .../fujitsu/vdmj/runtime/ContextException.java | 15 +++++++++++++-- .../com/fujitsu/vdmj/values/FunctionValue.java | 6 ++++-- .../com/fujitsu/vdmj/values/OperationValue.java | 3 ++- 4 files changed, 20 insertions(+), 8 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 331c269ee..aeda3edeb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java @@ -82,8 +82,6 @@ public class Breakpoint implements Serializable public static final int SOURCE = 0; // A file:line source breakpoint public static final int FUNCTION = 1; // A function or operation name breakpoint - public static final int USER_CANCEL = 4999; // Special message for timeouts - public Breakpoint(LexLocation location) { this.location = location; @@ -231,7 +229,7 @@ public void check(LexLocation execl, Context ctxt) case TERMINATE: setExecInterrupt(Breakpoint.NONE); - throw new ContextException(USER_CANCEL, "Execution cancelled", location, ctxt); + ContextException.throwUserCancel(location, ctxt); } ThreadState state = ctxt.threadState; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java index d42d62d24..0b7e5971c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java @@ -29,7 +29,8 @@ @SuppressWarnings("serial") public class ContextException extends RuntimeException { - public static final int STACK_OVERFLOW = 4998; + private static final int STACK_OVERFLOW = 4998; + private static final int USER_CANCEL = 4999; public final LexLocation location; public final Context ctxt; @@ -56,13 +57,23 @@ public String toString() return getMessage(); } + public static void throwStackOverflow(LexLocation from, Context ctxt) throws ContextException + { + throw new ContextException(STACK_OVERFLOW, "Stack overflow", from, ctxt); + } + public boolean isStackOverflow() { return number == STACK_OVERFLOW; } + public static void throwUserCancel(LexLocation from, Context ctxt) throws ContextException + { + throw new ContextException(USER_CANCEL, "Execution cancelled", from, ctxt); + } + public boolean isUserCancel() { - return number == Breakpoint.USER_CANCEL; + return number == USER_CANCEL; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java index 25b47fba2..05aae0456 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java @@ -343,7 +343,8 @@ public Value eval( catch (StackOverflowError e) { clearData(); - throw new ContextException(ContextException.STACK_OVERFLOW, "Stack overflow", location, ctxt); + ContextException.throwStackOverflow(location, ctxt); + return null; // No reached } } @@ -366,7 +367,8 @@ public Value eval( catch (StackOverflowError e) { clearData(); - throw new ContextException(ContextException.STACK_OVERFLOW, "Stack overflow", location, ctxt); + ContextException.throwStackOverflow(location, ctxt); + return null; // No reached } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java index a56a79374..9a3163e55 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/OperationValue.java @@ -239,7 +239,8 @@ public Value eval(LexLocation from, ValueList argValues, Context ctxt) } catch (StackOverflowError e) { - throw new ContextException(ContextException.STACK_OVERFLOW, "Stack overflow", from, ctxt); + ContextException.throwStackOverflow(from, ctxt); + return null; // No reached } }