From 616dd47fb230ecc96a21a90275eacffd41cf477e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 14 Feb 2021 13:50:10 +0000 Subject: [PATCH] Refactor/improve processing of identifier usage in model/properties. Implementation pushed into a helper class IdentUsage, used in both ModulesFile and PropertiesFile. Also, slightly improve error messages for identifier clashes (say where the original use was, e.g. "constant"). Also, add isIdentUsed and checkIdent to ModelInfo, with default implementations. This removes another dependency of PropertiesFile on ModulesFile. --- prism/src/parser/IdentUsage.java | 114 +++++++++++++++++++++++ prism/src/parser/ast/ModulesFile.java | 46 ++++----- prism/src/parser/ast/PropertiesFile.java | 35 +++---- prism/src/prism/ModelInfo.java | 33 +++++++ 4 files changed, 186 insertions(+), 42 deletions(-) create mode 100644 prism/src/parser/IdentUsage.java diff --git a/prism/src/parser/IdentUsage.java b/prism/src/parser/IdentUsage.java new file mode 100644 index 00000000..9823fcbd --- /dev/null +++ b/prism/src/parser/IdentUsage.java @@ -0,0 +1,114 @@ +//============================================================================== +// +// Copyright (c) 2021- +// Authors: +// * Dave Parker (University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM 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 2 of the License, or +// (at your option) any later version. +// +// PRISM 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 PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser; + +import java.util.HashMap; + +import parser.ast.ASTElement; +import prism.PrismLangException; + +/** + * Helper class to keep track of a set of identifiers that have been used. + */ +public class IdentUsage +{ + // Where identifiers were declared (AST element) + private HashMap identDecls; + // Uses of identifiers (e.g. "constant") + private HashMap identUses; + // Location of identifiers (e.g. "the model") + private HashMap identLocs; + + public IdentUsage() + { + identDecls = new HashMap<>(); + identUses = new HashMap<>(); + identLocs = new HashMap<>(); + } + + public void clear() + { + identDecls.clear(); + identUses.clear(); + identLocs.clear(); + } + + /** + * Check if an identifier is already used somewhere + * and throw an exception if it is. Otherwise, add it to the list. + * @param ident The name of the (new) identifier + * @param decl Where the identifier is declared in the model + * @param use Optionally, the identifier's usage (e.g. "constant") + * @param loc Optionally, the identifier's location (e.g. "the model") + */ + public void checkAndAddIdentifier(String ident, ASTElement decl, String use, String loc) throws PrismLangException + { + checkIdent(ident, decl, use); + identDecls.put(ident, decl); + identUses.put(ident, use); + identLocs.put(ident, loc); + } + + /** + * Check if an identifier is already used somewhere + * @param ident The name of the identifier to check + */ + public boolean isIdentUsed(String ident) + { + return identDecls.containsKey(ident); + } + + /** + * Check if an identifier is already used somewhere + * and throw an exception if it is. + * @param ident The name of the identifier to check + * @param decl Where the identifier is declared in the model (for the error message) + * @param use Optionally, the identifier's usage (e.g. "constant") + */ + public void checkIdent(String ident, ASTElement decl, String use) throws PrismLangException + { + ASTElement existing = identDecls.get(ident); + if (existing != null) { + // Construct error message if identifier exists already + String identStr = use != null ? ("Name of " + use) : "Identifier"; + identStr += " " + ident + ""; + String existingUse = identUses.get(ident); + existingUse = (existingUse == null) ? "" : " for a " + existingUse; + String existingLoc = identLocs.get(ident); + existingLoc = (existingLoc == null) ? "" : " in " + existingLoc; + throw new PrismLangException(identStr + " is already used" + existingUse + existingLoc, decl); + } + } + + @SuppressWarnings("unchecked") + public IdentUsage deepCopy() + { + IdentUsage ret = new IdentUsage(); + ret.identDecls = (HashMap) identDecls.clone(); + return ret; + } +} diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 4a20463a..18182e58 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -27,12 +27,12 @@ package parser.ast; import java.util.ArrayList; -import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Vector; import param.BigRational; +import parser.IdentUsage; import parser.State; import parser.Values; import parser.VarList; @@ -71,8 +71,8 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato private boolean hasObservables; // Observables info private List obsVars; - // Lists of all identifiers used and where - private HashMap identUsage; + // Info about all identifiers used + private IdentUsage identUsage; // List of all module names private String[] moduleNames; // List of synchronising actions @@ -105,7 +105,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato initStates = null; hasObservables = false; obsVars = new ArrayList(); - identUsage = new HashMap<>(); + identUsage = new IdentUsage(); varDecls = new Vector(); varNames = new Vector(); varTypes = new Vector(); @@ -580,24 +580,28 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato * (as a formula, constant or variable) * and throw an exception if it is. Otherwise, add it to the list. * @param ident The name of the (new) identifier - * @param e Where the identifier is declared in the model + * @param decl Where the identifier is declared in the model + * @param use Optionally, the identifier's usage (e.g. "constant") */ - private void checkAndAddIdentifier(String ident, ASTElement e) throws PrismLangException + private void checkAndAddIdentifier(String ident, ASTElement decl, String use) throws PrismLangException { - ASTElement existing = identUsage.get(ident); - if (existing != null) { - throw new PrismLangException("Identifier \"" + ident + "\" is already used in the model", e); - } - identUsage.put(ident, e); + identUsage.checkAndAddIdentifier(ident, decl, use, "the model"); } - /** - * Check if an identifier is already used somewhere in the model - * (as a formula, constant or variable) - */ + @Override public boolean isIdentUsed(String ident) { - return identUsage.containsKey(ident); + // Goes beyond default implementation in ModelInfo: + // also looks at formulas + return identUsage.isIdentUsed(ident); + } + + @Override + public void checkIdent(String ident, ASTElement decl, String use) throws PrismLangException + { + // Goes beyond default implementation in ModelInfo: + // also looks at formulas, and produces better error messages + identUsage.checkIdent(ident, decl, use); } // get individual module name @@ -841,7 +845,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int n = formulaList.size(); for (int i = 0; i < n; i++) { String s = formulaList.getFormulaName(i); - checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i)); + checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i), "formula"); } } @@ -988,7 +992,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int n = constantList.size(); for (int i = 0; i < n; i++) { String s = constantList.getConstantName(i); - checkAndAddIdentifier(s, constantList.getConstantNameIdent(i)); + checkAndAddIdentifier(s, constantList.getConstantNameIdent(i), "constant"); } } @@ -1003,7 +1007,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int n = getNumGlobals(); for (int i = 0; i < n; i++) { String s = getGlobal(i).getName(); - checkAndAddIdentifier(s, getGlobal(i)); + checkAndAddIdentifier(s, getGlobal(i), "variable"); varDecls.add(getGlobal(i)); varNames.add(s); varTypes.add(getGlobal(i).getType()); @@ -1017,7 +1021,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int numLocals = module.getNumDeclarations(); for (int j = 0; j < numLocals; j++) { String s = module.getDeclaration(j).getName(); - checkAndAddIdentifier(s, module.getDeclaration(j)); + checkAndAddIdentifier(s, module.getDeclaration(j), "variable"); varDecls.add(module.getDeclaration(j)); varNames.add(s); varTypes.add(module.getDeclaration(j).getType()); @@ -1522,7 +1526,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato for (String ov : obsVars) ret.addObservableVar(ov); // Copy other (generated) info - ret.identUsage = (identUsage == null) ? null : (HashMap) identUsage.clone(); + ret.identUsage = (identUsage == null) ? null : identUsage.deepCopy(); ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone(); ret.synchs = (synchs == null) ? null : (Vector)synchs.clone(); if (varDecls != null) { diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 0ff51f7a..35dacfc3 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -49,8 +49,8 @@ public class PropertiesFile extends ASTElement private ConstantList constantList; private Vector properties; // Properties - // Lists of all identifiers used and where - private HashMap identUsage; + // Info about all identifiers used + private IdentUsage identUsage; // Values set for undefined constants (null if none) private Values undefinedConstantValues; @@ -67,7 +67,7 @@ public class PropertiesFile extends ASTElement combinedLabelList = new LabelList(); constantList = new ConstantList(); properties = new Vector(); - identUsage = new HashMap<>(); + identUsage = new IdentUsage(); undefinedConstantValues = null; constantValues = null; } @@ -253,21 +253,15 @@ public class PropertiesFile extends ASTElement * (as a formula, constant or variable) * and throw an exception if it is. Otherwise, add it to the list. * @param ident The name of the (new) identifier - * @param e Where the identifier is declared in the model + * @param decl Where the identifier is declared + * @param use Optionally, the identifier's usage (e.g. "constant") */ - private void checkAndAddIdentifier(String ident, ASTElement e) throws PrismLangException + private void checkAndAddIdentifier(String ident, ASTElement decl, String use) throws PrismLangException { - // Check model file first - if (modulesFile.isIdentUsed(ident)) { - throw new PrismLangException("Identifier \"" + ident + "\" is already used in the model file", e); - } - // Then check here in the properties file - ASTElement existing = identUsage.get(ident); - if (existing != null) { - throw new PrismLangException("Identifier \"" + ident + "\" is already used", e); - } - // Finally, add - identUsage.put(ident, e); + // Check model first + modelInfo.checkIdent(ident, decl, use); + // Then check/add here in the properties file + identUsage.checkAndAddIdentifier(ident, decl, use, "the properties"); } /** @@ -276,7 +270,7 @@ public class PropertiesFile extends ASTElement */ public boolean isIdentUsed(String ident) { - return identUsage.containsKey(ident); + return identUsage.isIdentUsed(ident); } // method to tidy up (called after parsing) @@ -343,7 +337,7 @@ public class PropertiesFile extends ASTElement int n = formulaList.size(); for (int i = 0; i < n; i++) { String s = formulaList.getFormulaName(i); - checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i)); + checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i), "formula"); } } @@ -395,7 +389,7 @@ public class PropertiesFile extends ASTElement int n = constantList.size(); for (int i = 0; i < n; i++) { String s = constantList.getConstantName(i); - checkAndAddIdentifier(s, constantList.getConstantNameIdent(i)); + checkAndAddIdentifier(s, constantList.getConstantNameIdent(i), "constant"); } } @@ -674,7 +668,6 @@ public class PropertiesFile extends ASTElement /** * Perform a deep copy. */ - @SuppressWarnings("unchecked") public ASTElement deepCopy() { int i, n; @@ -691,7 +684,7 @@ public class PropertiesFile extends ASTElement ret.addProperty((Property) getPropertyObject(i).deepCopy()); } // Copy other (generated) info - ret.identUsage = (identUsage == null) ? null : (HashMap) identUsage.clone(); + ret.identUsage = (identUsage == null) ? null : identUsage.deepCopy(); ret.constantValues = (constantValues == null) ? null : new Values(constantValues); return ret; diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index 171e7335..9c0851bc 100644 --- a/prism/src/prism/ModelInfo.java +++ b/prism/src/prism/ModelInfo.java @@ -32,6 +32,7 @@ import java.util.List; import parser.Values; import parser.VarList; +import parser.ast.ASTElement; import parser.ast.DeclarationBool; import parser.ast.DeclarationIntUnbounded; import parser.ast.DeclarationType; @@ -284,4 +285,36 @@ public interface ModelInfo // Default implementation just extracts from getLabelNames() return getLabelNames().indexOf(name); } + + /** + * Check if an identifier is used in the model + * (e.g., as a constant or variable) + */ + public default boolean isIdentUsed(String ident) + { + // Default implementation looks up any vars/consts + if (getVarIndex(ident) != -1) { + return true; + } + Values v = getConstantValues(); + if (v != null & v.contains(ident)) { + return true; + } + return false; + } + + /** + * Check if an identifier is already used in the model + * (e.g., as a constant or variable) and throw an exception if it is. + * @param ident The name of the identifier to check + * @param decl Where the identifier is declared in the model (for the error message) + * @param use Optionally, the identifier's usage (e.g. "constant") + */ + public default void checkIdent(String ident, ASTElement decl, String use) throws PrismLangException + { + // Default implementation via isIdentUsed + if (isIdentUsed(ident)) { + throw new PrismLangException("Identifier " + ident + " is already used in the model", decl); + } + } }