From c7365ce0d92a615d4f58f7329f23ce1b2e1fe5b4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 27 Jan 2012 09:59:23 +0000 Subject: [PATCH] Bugfix: look for undefined constants recursively in referenced properties. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4499 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ASTElement.java | 29 +++++++-------- prism/src/parser/ast/PropertiesFile.java | 11 +++--- .../GetAllUndefinedConstantsRecursively.java | 35 ++++++++++++++----- 3 files changed, 47 insertions(+), 28 deletions(-) diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 2ecfd45d..abcf6d87 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -115,11 +115,11 @@ public abstract class ASTElement */ public Type getType() { - if (type != null) return type; + if (type != null) + return type; try { typeCheck(); - } - catch (PrismLangException e) { + } catch (PrismLangException e) { // Returns null (unknown) in case of error. // If you want to check for errors, use typeCheck(). return null; @@ -258,7 +258,7 @@ public abstract class ASTElement */ public Vector getAllConstants() { - Vector v= new Vector(); + Vector v = new Vector(); GetAllConstants visitor = new GetAllConstants(v); try { accept(visitor); @@ -270,20 +270,21 @@ public abstract class ASTElement } /** - * Get all undefined constants used (i.e. in ExpressionConstant objects) recursively and return as a list. - * Recursive descent means that we find e.g. constants that are used within other constants, labels. - * But note that we only look at/for constants in the passed in ConstantList. - * Any others discovered are ignored (and not descended into). + * Get all undefined constants used (i.e. in ExpressionConstant objects) recursively and return as a list. + * Recursive descent means that we also find constants that are used within other constants, labels, properties. + * We only recurse into constants/labels/properties in the passed in lists. + * Any others discovered are ignored (and not descended into). + * ConstantList must be non-null so that we can determine which constants are undefined; + * LabelList and PropertiesFile passed in as null are ignored. */ - public Vector getAllUndefinedConstantsRecursively(ConstantList constantList, LabelList labelList) + public Vector getAllUndefinedConstantsRecursively(ConstantList constantList, LabelList labelList, PropertiesFile propertiesFile) { - Vector v= new Vector(); - GetAllUndefinedConstantsRecursively visitor = new GetAllUndefinedConstantsRecursively(v, constantList, labelList); + Vector v = new Vector(); + GetAllUndefinedConstantsRecursively visitor = new GetAllUndefinedConstantsRecursively(v, constantList, labelList, propertiesFile); try { accept(visitor); } catch (PrismLangException e) { - // GetAllUndefinedConstantsRecursively can throw an exception (if a constant does not exist) - // but this would have been caught by earlier checks so we ignore. + // Should not happen; ignore. } return v; } @@ -321,7 +322,7 @@ public abstract class ASTElement */ public Vector getAllVars() throws PrismLangException { - Vector v =new Vector(); + Vector v = new Vector(); GetAllVars visitor = new GetAllVars(v); accept(visitor); return v; diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 4cc060cb..d86a8e13 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -366,6 +366,7 @@ public class PropertiesFile extends ASTElement /** * Get a list of undefined (properties file) constants appearing in labels of the properties file + * (including those that appear in definitions of other needed constants) * (undefined constants are those of form "const int x;" rather than "const int x = 1;") */ public Vector getUndefinedConstantsUsedInLabels() @@ -377,7 +378,7 @@ public class PropertiesFile extends ASTElement n = labelList.size(); for (i = 0; i < n; i++) { expr = labelList.getLabel(i); - tmp = expr.getAllUndefinedConstantsRecursively(constantList, combinedLabelList); + tmp = expr.getAllUndefinedConstantsRecursively(constantList, combinedLabelList, null); for (String s : tmp) { if (!consts.contains(s)) { consts.add(s); @@ -389,17 +390,17 @@ public class PropertiesFile extends ASTElement /** * Get a list of undefined (properties file) constants used in a property - * (including those that appear in required labels/properties) + * (including those that appear in definitions of other needed constants and labels/properties) * (undefined constants are those of form "const int x;" rather than "const int x = 1;") */ public Vector getUndefinedConstantsUsedInProperty(Property prop) { - return prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList); + return prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList, this); } /** * Get a list of undefined (properties file) constants used in a list of properties - * (including those that appear in required labels/properties) + * (including those that appear in definitions of other needed constants and labels/properties) * (undefined constants are those of form "const int x;" rather than "const int x = 1;") */ public Vector getUndefinedConstantsUsedInProperties(List props) @@ -407,7 +408,7 @@ public class PropertiesFile extends ASTElement Vector consts, tmp; consts = new Vector(); for (Property prop : props) { - tmp = prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList); + tmp = prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList, this); for (String s : tmp) { if (!consts.contains(s)) { consts.add(s); diff --git a/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java b/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java index baff391c..e1e2998c 100644 --- a/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java +++ b/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java @@ -33,23 +33,27 @@ import prism.PrismLangException; /** * Get all undefined constants used (i.e. in ExpressionConstant objects) recursively and return as a list. - * Recursive descent means that we find e.g. constants that are used within other constants, labels. - * But note that we only look at/for constants in the passed in ConstantList. + * Recursive descent means that we also find constants that are used within other constants, labels, properties. + * We only recurse into constants/labels/properties in the passed in lists. * Any others discovered are ignored (and not descended into). + * ConstantList must be non-null so that we can determine which constants are undefined; + * LabelList and PropertiesFile passed in as null are ignored. */ public class GetAllUndefinedConstantsRecursively extends ASTTraverse { private Vector v; private ConstantList constantList; private LabelList labelList; - - public GetAllUndefinedConstantsRecursively(Vector v, ConstantList constantList, LabelList labelList) + private PropertiesFile propertiesFile; + + public GetAllUndefinedConstantsRecursively(Vector v, ConstantList constantList, LabelList labelList, PropertiesFile propertiesFile) { this.v = v; this.constantList = constantList; this.labelList = labelList; + this.propertiesFile = propertiesFile; } - + public void visitPost(ExpressionConstant e) throws PrismLangException { // Look up this constant in the constant list @@ -69,20 +73,33 @@ public class GetAllUndefinedConstantsRecursively extends ASTTraverse expr.accept(this); } } - + public void visitPost(ExpressionLabel e) throws PrismLangException { // Ignore special cases of labels (no constants there) if (e.getName().equals("deadlock") || e.getName().equals("init")) { return; } - // Look up this label in the label list + // Look up this label in the label list, if possible + if (labelList == null) + return; int i = labelList.getLabelIndex(e.getName()); if (i == -1) - throw new PrismLangException("Unknown label \"" + e.getName() + "\""); + return; Expression expr = labelList.getLabel(i); // Check label definition recursively for more undefined constants expr.accept(this); } -} + public void visitPost(ExpressionProp e) throws PrismLangException + { + // Look up this property in the properties files, if possible + if (propertiesFile == null) + return; + Property prop = propertiesFile.lookUpPropertyObjectByName(e.getName()); + if (prop == null) + return; + // Check property recursively for more undefined constants + prop.getExpression().accept(this); + } +}