From 4b35d9deb56626a241b536fe317c62af25de2d9c Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 2 Dec 2023 13:19:55 +0000 Subject: [PATCH 1/7] Remove test and TODO files --- quickcheck/TODO | 5 ----- quickcheck/test.vdm | 14 -------------- 2 files changed, 19 deletions(-) delete mode 100644 quickcheck/TODO delete mode 100644 quickcheck/test.vdm diff --git a/quickcheck/TODO b/quickcheck/TODO deleted file mode 100644 index def382cda..000000000 --- a/quickcheck/TODO +++ /dev/null @@ -1,5 +0,0 @@ -Things still to do with QuickCheck - -. Make getValues interruptible as well as checkObligations? -. Move QC to be part of POPlugin(s)? -. Separate IO from calculations (and allow LSP control) diff --git a/quickcheck/test.vdm b/quickcheck/test.vdm deleted file mode 100644 index 2957f1fc1..000000000 --- a/quickcheck/test.vdm +++ /dev/null @@ -1,14 +0,0 @@ -values - MAX_T = 9; - -types - T = nat - inv t == t <= MAX_T; - -functions - f: T -> T - f(a) == - if a = 0 - then 1 - else a * f(a-1) - measure a; From 6c74f626f8e099edb569b1c6d1d8adfcffb8296c Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 2 Dec 2023 14:37:30 +0000 Subject: [PATCH 2/7] First draft of hidden variable detection for POG defence --- .../po/expressions/POCasesExpression.java | 17 +++++- .../fujitsu/vdmj/po/patterns/POPattern.java | 10 ++++ .../visitors/POHiddenVariablesVisitor.java | 60 +++++++++++++++++++ .../com/fujitsu/vdmj/pog/ProofObligation.java | 10 ++++ .../fujitsu/vdmj/pog/ProofObligationList.java | 15 ++++- .../com/fujitsu/vdmj/tc/lex/TCNameToken.java | 12 ++++ .../fujitsu/vdmj/typechecker/Environment.java | 1 + 7 files changed, 119 insertions(+), 6 deletions(-) create mode 100644 vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POHiddenVariablesVisitor.java diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java index 5e0e6bb8c..844169987 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.pog.CasesExhaustiveObligation; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.tc.lex.TCNameList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; import com.fujitsu.vdmj.util.Utils; @@ -67,6 +68,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment int count = 0; boolean hasIgnore = false; + TCNameList hidden = new TCNameList(); for (POCaseAlternative alt: cases) { @@ -74,12 +76,21 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment { hasIgnore = true; } - + + hidden.addAll(alt.pattern.getHiddenVariables()); // cumulative + // PONotCaseContext pushed by the POCaseAlternative... - obligations.addAll(alt.getProofObligations(ctxt, expType, env)); + ProofObligationList _obligations = alt.getProofObligations(ctxt, expType, env); + + if (!hidden.isEmpty()) + { + _obligations.markUnchecked("Obligation patterns contain hidden variables: " + hidden); + } + + obligations.addAll(_obligations); count++; } - + if (others != null) { obligations.addAll(others.getProofObligations(ctxt, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java index 9a2bd1d84..64d2223b8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java @@ -35,6 +35,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.POGetAllVarNamesVisitor; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.po.patterns.visitors.POGetPossibleTypeVisitor; +import com.fujitsu.vdmj.po.patterns.visitors.POHiddenVariablesVisitor; import com.fujitsu.vdmj.po.patterns.visitors.POPatternVisitor; import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; import com.fujitsu.vdmj.tc.lex.TCNameList; @@ -169,6 +170,15 @@ public void setMaximal(boolean maximal) { return; // Only used in PORecordPattern } + + /** + * Search the pattern for identifiers that hide other definitions. This is + * used during PO generation to avoid TC errors. + */ + public TCNameList getHiddenVariables() + { + return apply(new POHiddenVariablesVisitor(), null); + } /** * Implemented by all patterns to allow visitor processing. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POHiddenVariablesVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POHiddenVariablesVisitor.java new file mode 100644 index 000000000..1c0d7b059 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POHiddenVariablesVisitor.java @@ -0,0 +1,60 @@ +/******************************************************************************* + * + * Copyright (c) 2023 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package com.fujitsu.vdmj.po.patterns.visitors; + +import com.fujitsu.vdmj.po.patterns.POIdentifierPattern; +import com.fujitsu.vdmj.po.patterns.POPattern; +import com.fujitsu.vdmj.tc.lex.TCNameList; +import com.fujitsu.vdmj.tc.lex.TCNameToken; + +/** + * Search a pattern for hidden variables, and return a list. + */ +public class POHiddenVariablesVisitor extends POLeafPatternVisitor +{ + @Override + protected TCNameList newCollection() + { + return new TCNameList(); + } + + @Override + public TCNameList casePattern(POPattern node, Object arg) + { + return newCollection(); + } + + @Override + public TCNameList caseIdentifierPattern(POIdentifierPattern node, Object arg) + { + TCNameList result = newCollection(); + + if (node.name.getHides() != null) + { + result.add(node.name); + } + + return result; + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 7803ee623..6846878df 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -135,6 +135,16 @@ public void setMessage(String message) this.message = message; } + /** + * This is used to mark obligations as unchecked, with a reason. + */ + public void markUnchecked(String message) + { + this.isCheckable = false; + this.setStatus(POStatus.UNCHECKED); + this.setMessage(message); + } + public boolean isExistential() { return existential; 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 e9a1c6523..329608c93 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -227,9 +227,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env { // Probably an implicit missing measure iter.remove(); - obligation.status = POStatus.UNCHECKED; - obligation.isCheckable = false; - obligation.message = "PO #" + obligation.number + ": Missing measure function"; + obligation.markUnchecked("Obligation for missing measure function"); } break; @@ -250,4 +248,15 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env obligation.setCheckedExpression(tcexp); } + + /** + * This is used by POG to mark obligations as unchecked, with a reason. + */ + public void markUnchecked(String message) + { + for (ProofObligation obligation: this) + { + obligation.markUnchecked(message); + } + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java index 0724d5c11..31e7403e0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.lex.LexNameToken; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.tc.definitions.TCDefinition; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.TypeComparator; @@ -43,6 +44,7 @@ public class TCNameToken extends TCToken implements Serializable, Comparable Date: Sat, 2 Dec 2023 14:53:12 +0000 Subject: [PATCH 3/7] Correction to POG stack isExistential --- vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java index 69f586dc2..ca4d68b48 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -138,8 +138,10 @@ public PODefinition getDefinition() public boolean isExistential() { - for (POContext ctxt: this) + for (int i = size() - 1; i >= 0; i--) // NB. reverse order, for tail "exists" { + POContext ctxt = get(i); + if (ctxt instanceof PONameContext || ctxt instanceof PONoCheckContext || ctxt instanceof POScopeContext) From fa5c8cad80f15c4f7c1758a2f2f72d716063f1e9 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 2 Dec 2023 17:15:46 +0000 Subject: [PATCH 4/7] Attempt to improve newspeakSL POG errors --- .../po/expressions/POApplyExpression.java | 69 ++++++++++++------- 1 file changed, 44 insertions(+), 25 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java index c44008a38..d5970dcc8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java @@ -105,36 +105,16 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!type.isUnknown(location) && (type.isFunction(location) || type.isOperation(location))) { - TCTypeList paramTypes = type.isFunction(location) ? - type.getFunction().parameters : type.getOperation().parameters; - String prename = root.getPreName(); - if (type.isFunction(location) && prename != null && !prename.equals("")) + if (type.isFunction(location) && prename != null && !prename.isEmpty()) { - boolean needed = true; - - if (type.definitions != null) - { - TCDefinition def = type.definitions.firstElement(); - - // If the apply is of an explicit curried function, we don't want to - // generate a precondition obligation, because we haven't collected - // all the curried parameters yet. - - if (def instanceof TCExplicitFunctionDefinition) - { - TCExplicitFunctionDefinition edef = (TCExplicitFunctionDefinition)def; - needed =!edef.isCurried; - } - } - - if (needed) - { - obligations.add(new FunctionApplyObligation(root, args, prename, ctxt)); - } + obligations.add(new FunctionApplyObligation(root, args, prename, ctxt)); } + TCTypeList paramTypes = type.isFunction(location) ? + type.getFunction().parameters : type.getOperation().parameters; + int i=0; for (TCType at: argtypes) @@ -227,6 +207,45 @@ else if (root instanceof POFuncInstantiationExpression) sb.append(")"); return sb.toString(); } + + /** + * This is used in apply chains or curried calls, where the precondition is needed + * at the end of the chain. + */ + @Override + public String getPreName() + { + if (root instanceof POFuncInstantiationExpression) + { + String pn = root.getPreName(); + + if (pn != null && !pn.isEmpty()) + { + return pn + "(" + Utils.listToString(args) + ")"; + } + } + else if (type.definitions != null && !type.definitions.isEmpty()) + { + TCDefinition def = type.definitions.firstElement(); + + if (def instanceof TCExplicitFunctionDefinition) + { + TCExplicitFunctionDefinition exdef = (TCExplicitFunctionDefinition)def; + + if (exdef.isCurried) + { + String pn = root.getPreName(); + + if (pn != null && !pn.isEmpty()) + { + return pn + "(" + Utils.listToString(args) + ")"; + } + } + } + } + + return null; // Already generated elsewhere + } @Override public R apply(POExpressionVisitor visitor, S arg) From 0b412f908e70cde329380d02bf95de93beaae609 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 2 Dec 2023 18:08:28 +0000 Subject: [PATCH 5/7] Try to clean up complex fn apply obligations --- .../po/expressions/POApplyExpression.java | 32 ++----------------- .../vdmj/pog/FunctionApplyObligation.java | 4 ++- 2 files changed, 6 insertions(+), 30 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java index d5970dcc8..457506c6c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java @@ -34,8 +34,6 @@ import com.fujitsu.vdmj.pog.RecursiveObligation; import com.fujitsu.vdmj.pog.SeqApplyObligation; import com.fujitsu.vdmj.pog.SubTypeObligation; -import com.fujitsu.vdmj.tc.definitions.TCDefinition; -import com.fujitsu.vdmj.tc.definitions.TCExplicitFunctionDefinition; import com.fujitsu.vdmj.tc.types.TCMapType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; @@ -215,36 +213,12 @@ else if (root instanceof POFuncInstantiationExpression) @Override public String getPreName() { - if (root instanceof POFuncInstantiationExpression) + if (root.getPreName() == null) { - String pn = root.getPreName(); - - if (pn != null && !pn.isEmpty()) - { - return pn + "(" + Utils.listToString(args) + ")"; - } - } - else if (type.definitions != null && !type.definitions.isEmpty()) - { - TCDefinition def = type.definitions.firstElement(); - - if (def instanceof TCExplicitFunctionDefinition) - { - TCExplicitFunctionDefinition exdef = (TCExplicitFunctionDefinition)def; - - if (exdef.isCurried) - { - String pn = root.getPreName(); - - if (pn != null && !pn.isEmpty()) - { - return pn + "(" + Utils.listToString(args) + ")"; - } - } - } + return null; } - return null; // Already generated elsewhere + return FunctionApplyObligation.UNKNOWN; // Use pre_(root, args) form } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/FunctionApplyObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/FunctionApplyObligation.java index 4028f0823..614cdfe5e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/FunctionApplyObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/FunctionApplyObligation.java @@ -30,12 +30,14 @@ public class FunctionApplyObligation extends ProofObligation { + public static final String UNKNOWN = "???"; // Use pre_(root, args) form + public FunctionApplyObligation(POExpression root, POExpressionList args, String prename, POContextStack ctxt) { super(root.location, POType.FUNC_APPLY, ctxt); StringBuilder sb = new StringBuilder(); - if (prename == null) + if (prename == UNKNOWN) { sb.append("pre_("); sb.append(root); From 8957ef387ace129b5c0144046c8a079abf278454 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 2 Dec 2023 18:37:30 +0000 Subject: [PATCH 6/7] Better hidden variable detection --- .../po/expressions/POCasesExpression.java | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java index 844169987..fa4ab17ae 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java @@ -69,6 +69,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment int count = 0; boolean hasIgnore = false; TCNameList hidden = new TCNameList(); + ProofObligationList _obligations = new ProofObligationList(); for (POCaseAlternative alt: cases) { @@ -80,20 +81,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment hidden.addAll(alt.pattern.getHiddenVariables()); // cumulative // PONotCaseContext pushed by the POCaseAlternative... - ProofObligationList _obligations = alt.getProofObligations(ctxt, expType, env); - - if (!hidden.isEmpty()) - { - _obligations.markUnchecked("Obligation patterns contain hidden variables: " + hidden); - } - - obligations.addAll(_obligations); + _obligations.addAll(alt.getProofObligations(ctxt, expType, env)); count++; } if (others != null) { - obligations.addAll(others.getProofObligations(ctxt, env)); + _obligations.addAll(others.getProofObligations(ctxt, env)); } for (int i=0; i