diff --git a/lsp/src/main/java/dap/ExpressionExecutor.java b/lsp/src/main/java/dap/ExpressionExecutor.java index aa0fe33b2..b96b5ec4c 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 Environment env = null; 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,11 +63,14 @@ protected void head() protected void exec() throws Exception { boolean saved = Properties.parser_maximal_types; // Used by qcrun + Interpreter interpreter = manager.getInterpreter(); + + if (env == null) env = interpreter.getGlobalEnvironment(); try { Properties.parser_maximal_types = maximal; - answer = manager.getInterpreter().execute(expression).toString(); + answer = interpreter.execute(expression, env).toString(); } finally { 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/ASTLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/ASTLaunchDebugLens.java index 508555f55..76cff4f4e 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; + int i = 0; + + 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; + } } } } @@ -110,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))); } } } @@ -136,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++)))); } } } @@ -156,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/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/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) { diff --git a/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/POLaunchDebugLens.java index 717e3ad88..cbeba4a4e 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", "PO #" + po.number); + 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..d35e53b7b 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) @@ -101,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) @@ -114,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) @@ -126,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)); } } 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/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/QCRunCommand.java b/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java index 45a170354..0df7e1042 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,11 +134,24 @@ else if (obligation.kind.isStandAlone()) // Temporarily allow maximal parsing, for invariant POs boolean saved = Properties.parser_maximal_types; + Interpreter interpreter = Interpreter.getInstance(); try { Properties.parser_maximal_types = true; - PrintCommand cmd = new PrintCommand(pline); + + // 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"); + menv = new MultiModuleEnvironment(tc.getPO()); + } + + PrintCommand cmd = new PrintCommand(pline, menv); return cmd.run(pline); } finally 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/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 { diff --git a/vdmj/documentation/MESSAGES b/vdmj/documentation/MESSAGES index 6946eb68f..7b8ca5886 100644 --- a/vdmj/documentation/MESSAGES +++ b/vdmj/documentation/MESSAGES @@ -950,10 +950,13 @@ as the expected and actual values. 4171, "Cannot convert to " 4172, "Values cannot be compared: , " 4173, "Unknown annotation @" -4174, "Stack overflow" -4175, "Execution cancelled" +4174, - +4175, - 4176, "Cannot evaluate power set of size " 4177, "Not permitted during initialization" +... +4998, "Stack overflow" +4999, "Execution cancelled" 5000, "Definition not used" 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/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/POCasesStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCasesStatement.java index 8139a3b52..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 @@ -75,7 +78,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; @@ -87,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/POCyclesStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCyclesStatement.java index 551114cc5..d7908865d 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 eb097e169..da85cf549 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/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..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 @@ -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; @@ -60,10 +61,13 @@ 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); + ctxt.push(new POForAllSequenceContext(pattern, set, " in set ")); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); + ctxt.pop(); + + 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..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; @@ -66,20 +67,21 @@ 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.stateUpdate(pogState, from); + 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.stateUpdate(pogState, by); + obligations.addAll(by.getProofObligations(ctxt, pogState, env).markIfUpdated(pogState, by)); } ctxt.push(new POScopeContext()); + ctxt.push(new POForAllSequenceContext(var, from, to, by)); 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(); + ctxt.pop(); return obligations; } 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..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,23 +38,29 @@ 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 { private static final long serialVersionUID = 1L; public final POPatternBind patternBind; public final boolean reverse; - public final POExpression exp; + 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.exp = exp; + this.sequence = exp; + this.expType = expType; this.statement = body; } @@ -62,44 +68,52 @@ 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.stateUpdate(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)); + + 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) { 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); - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); + ctxt.pop(); + + 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/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/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/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 660a79124..d0e496cc0 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,62 @@ 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.po.patterns.POTypeBind; +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; + + private String seqset = " in seq "; - 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(); + } + + public POForAllSequenceContext(POSeqBind bind, POExpression exp) + { + this.pattern = bind.pattern.toString(); + this.exp = exp.toString(); + } + + 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(); + } + + 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); + } + } + + public POForAllSequenceContext(POPattern pattern, POExpression set, String seqset) + { + this.pattern = pattern.toString(); + this.exp = set.toString(); + this.seqset = seqset; } @Override @@ -44,9 +89,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/java/com/fujitsu/vdmj/pog/POLaunchFactory.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLaunchFactory.java index 869c1d253..826a5033c 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,9 @@ 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); + String stype = type.toString().replace(" /* opaque */", ""); // HACK! + lastArgs.add(new ApplyArg(p.toString(), stype, result)); return result; } } 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..4092fded2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -286,26 +286,28 @@ 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 ProofObligationList 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 { markUnchecked(ProofObligation.HAS_UPDATED_STATE + " " + at.toShortString()); } } + + return this; } } 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 3ccdcdd8c..598500ce9 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,7 +81,7 @@ 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 Breakpoint(LexLocation location) { this.location = location; @@ -229,7 +229,7 @@ public void check(LexLocation execl, Context ctxt) case TERMINATE: setExecInterrupt(Breakpoint.NONE); - throw new ContextException(4175, "Execution cancelled", location, ctxt); + ContextException.throwUserCancel(location, ctxt); } ThreadState state = ctxt.threadState; 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..2591ffe44 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ClassInterpreter.java @@ -299,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/ContextException.java b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ContextException.java index 3c56bd98a..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,6 +29,9 @@ @SuppressWarnings("serial") public class ContextException extends RuntimeException { + private static final int STACK_OVERFLOW = 4998; + private static final int USER_CANCEL = 4999; + public final LexLocation location; public final Context ctxt; public final int number; @@ -54,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 == 4174; + 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 == 4175; + return number == USER_CANCEL; } } 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..ac5faaf6d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/Interpreter.java @@ -192,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 @@ -414,7 +415,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 */ @@ -492,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; @@ -502,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 b7441edcc..c9404dba4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/runtime/ModuleInterpreter.java @@ -278,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()); 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/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. 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..05aae0456 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 @@ -317,9 +331,20 @@ public Value eval( ValueList args = new ValueList(arg); return eval(from, args, ctxt, null); } + catch (ContextException e) + { + if (e.isUserCancel()) + { + clearData(); + } + + throw e; + } catch (StackOverflowError e) { - throw new ContextException(4174, "Stack overflow", location, ctxt); + clearData(); + ContextException.throwStackOverflow(location, ctxt); + return null; // No reached } } @@ -330,9 +355,20 @@ public Value eval( { return eval(from, argValues, ctxt, null); } + catch (ContextException e) + { + if (e.isUserCancel()) + { + clearData(); + } + + throw e; + } catch (StackOverflowError e) { - throw new ContextException(4174, "Stack overflow", location, ctxt); + clearData(); + 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 d4860c1ca..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(4174, "Stack overflow", from, ctxt); + ContextException.throwStackOverflow(from, ctxt); + return null; // No reached } } diff --git a/vdmj/src/main/resources/tc-po.mappings b/vdmj/src/main/resources/tc-po.mappings index 7a7f3389b..eec764f8d 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; @@ -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;