From 82836f1ad1d5ad06fd0541636b130a1377135819 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 2 May 2014 00:01:14 +0200 Subject: [PATCH] Added some checks for validity of identifiers in PRISM programs. Added some illegal tests to test suite. Former-commit-id: fc44db75a74221692e6a1ec36ec4f15a8892b17f --- src/parser/PrismParser.cpp | 67 +++++++++++++----- src/parser/PrismParser.h | 2 +- test/functional/parser/PrismParserTest.cpp | 79 ++++++++++++++++++++++ 3 files changed, 129 insertions(+), 19 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index ed15050cb..b96a0b823 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -147,13 +147,7 @@ namespace storm { globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)])); globalVariableDefinition.name("global variable declaration list"); - - programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] - > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)]) - > *(formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1)]) - > *(globalVariableDefinition(qi::_r1)); - programHeader.name("program header"); - + stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); @@ -199,7 +193,19 @@ namespace storm { moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)]; moduleDefinitionList.name("module list"); - start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(initialStatesConstruct(qi::_a) | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)]; + start = (qi::eps + > modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1] + > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] + | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] + | globalVariableDefinition(qi::_a) + | (moduleRenaming(qi::_a) | moduleDefinition(qi::_a))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_a), qi::_1)] + | initialStatesConstruct(qi::_a) + | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] + | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] + ) + > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)]; start.name("probabilistic program"); // Enable error reporting. @@ -258,7 +264,7 @@ namespace storm { } bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { - LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::InvalidArgumentException, "Program must not define two initial constructs."); + LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Program must not define two initial constructs."); if (globalProgramInformation.hasInitialStatesExpression) { return false; } @@ -483,37 +489,56 @@ namespace storm { } storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); } storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const { - if (this->secondRun) { + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << formulaName << "'."); this->identifiers_.add(formulaName, expression); } return storm::prism::Formula(formulaName, expression, this->getFilename()); @@ -550,12 +575,18 @@ namespace storm { } storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { - this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'."); + this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); + } return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename()); } storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const { - this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'."); + this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); + } return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 6a31ef367..b5013eee8 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -189,7 +189,7 @@ namespace storm { qi::rule modelTypeDefinition; // Rules for parsing the program header. - qi::rule programHeader; + qi::rule undefinedConstantDefinition; qi::rule undefinedBooleanConstantDefinition; qi::rule undefinedIntegerConstantDefinition; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 81731114b..dca09244a 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -54,6 +54,21 @@ TEST(PrismParser, SimpleFullTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true)); EXPECT_EQ(1, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); + + testInput = + R"(mdp + + module main + x : [1..5] init 1; + [] x=1 -> 1:(x'=2); + [] x=2 -> 1:(x'=3); + [] x=3 -> 1:(x'=1); + [] x=3 -> 1:(x'=4); + [] x=4 -> 1:(x'=5); + endmodule)"; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true)); + EXPECT_EQ(1, result.getNumberOfModules()); + EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); } TEST(PrismParser, ComplexFullTest) { @@ -167,4 +182,68 @@ TEST(PrismParser, ComplexParsingTest) { EXPECT_EQ(2, result.getNumberOfRewardModels()); EXPECT_EQ(1, result.getNumberOfLabels()); EXPECT_TRUE(result.definesInitialStatesExpression()); +} + +TEST(PrismParser, IllegalInputTest) { + std::string testInput = + R"(ctmc + + const int a; + const bool a = true; + + module mod1 + c : [0 .. 8] init 1; + [] c < 3 -> 2: (c' = c+1); + endmodule + )"; + + storm::prism::Program result; + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); + + testInput = + R"(dtmc + + const int a; + + module mod1 + a : [0 .. 8] init 1; + [] a < 3 -> 1: (a' = a+1); + endmodule)"; + + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); + + testInput = + R"(dtmc + + const int a = 2; + formula a = 41; + + module mod1 + c : [0 .. 8] init 1; + [] c < 3 -> 1: (c' = c+1); + endmodule)"; + + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); + + testInput = + R"(dtmc + + const int a = 2; + + init + c > 3 + endinit + + module mod1 + c : [0 .. 8] init 1; + [] c < 3 -> 1: (c' = c+1); + endmodule + + init + c > 3 + endinit + + )"; + + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); } \ No newline at end of file