From 9a0e42babbc01734a35e2d87beb70ac0261b6788 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 28 Jul 2015 19:07:52 +0200 Subject: [PATCH] static analysis for global variables Former-commit-id: ef846aa804a69829b0b1b5be24ccb060ab0c6fa4 --- src/storage/prism/Program.cpp | 50 ++++++++++++++++++++++++++++++---- src/storage/prism/Program.h | 16 +++++++++++ src/storage/prism/Variable.cpp | 2 +- src/storage/prism/Variable.h | 1 + 4 files changed, 63 insertions(+), 6 deletions(-) diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 258d4e14d..0b61fd795 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -179,6 +179,16 @@ namespace storm { std::vector const& Program::getGlobalIntegerVariables() const { return this->globalIntegerVariables; } + + bool Program::globalBooleanVariableExists(std::string const& variableName) const { + return this->globalBooleanVariableToIndexMap.count(variableName) > 0; + } + + bool Program::globalIntegerVariableExists(std::string const& variableName) const { + return this->globalIntegerVariableToIndexMap.count(variableName) > 0; + } + + BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const { auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName); @@ -592,6 +602,41 @@ namespace storm { std::set variablesAndConstants; std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin())); + // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable. + std::set> globalBVarsWrittenToByCommand; + std::set> globalIVarsWrittenToByCommand; + for(auto const& module : this->getModules()) { + std::set> globalBVarsWrittenToByCommandInThisModule; + std::set> globalIVarsWrittenToByCommandInThisModule; + for (auto const& command : module.getCommands()) { + if(!command.isLabeled()) continue; + for (auto const& update : command.getUpdates()) { + for (auto const& assignment : update.getAssignments()) { + if(this->globalBooleanVariableExists(assignment.getVariable().getName())) { + globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()}); + } + else if(this->globalIntegerVariableExists(assignment.getVariable().getName())) { + globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()}); + } + } + } + } + for(auto const& entry : globalIVarsWrittenToByCommandInThisModule) { + if(globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'."); + } + } + for(auto const& entry : globalBVarsWrittenToByCommandInThisModule) { + if(globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": assignment of (possibly) synchronizing command with label '" << entry.second << "' writes to global variable '" << entry.first << "'."); + } + } + + globalBVarsWrittenToByCommand.insert(globalBVarsWrittenToByCommandInThisModule.begin(), globalBVarsWrittenToByCommandInThisModule.end()); + globalIVarsWrittenToByCommand.insert(globalIVarsWrittenToByCommandInThisModule.begin(), globalIVarsWrittenToByCommandInThisModule.end()); + + } + // Check the commands of the modules. bool hasProbabilisticCommand = false; bool hasMarkovianCommand = false; @@ -636,11 +681,6 @@ namespace storm { for (auto const& assignment : update.getAssignments()) { storm::expressions::Variable assignedVariable = manager->getVariable(assignment.getVariableName()); - // If the command is labeled, i.e. may synchronize, we need to make sure no global variable is written. - if (command.isLabeled()) { - STORM_LOG_THROW(globalVariables.find(assignedVariable) == globalVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment of (possibly) synchronizing command writes to global variable '" << assignment.getVariableName() << "'."); - } - if (legalVariables.find(assignedVariable) == legalVariables.end()) { if (all.find(assignedVariable) != all.end()) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'."); diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 5bb241a24..94bcf7353 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -118,6 +118,22 @@ namespace storm { */ std::size_t getNumberOfConstants() const; + /*! + * Retrieves whether a global Boolean variable with the given name exists + * + * @param variableName The name of the variable + * @return true iff a global variable of type Boolean with the given name exists. + */ + bool globalBooleanVariableExists(std::string const& variableName) const; + + /** + * Retrieves whether a global Integer variable with the given name exists + * + * @param variableName The name of the variable + * @return true iff a global variable of type Integer with the given name exists. + */ + bool globalIntegerVariableExists(std::string const& variableName) const; + /*! * Retrieves the global boolean variables of the program. * diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp index 2660a60ff..7d347bcec 100644 --- a/src/storage/prism/Variable.cpp +++ b/src/storage/prism/Variable.cpp @@ -32,6 +32,6 @@ namespace storm { storm::expressions::Expression Variable::getExpression() const { return variable.getExpression(); } - + } // namespace prism } // namespace storm diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h index 692b9ea64..3a19c2b75 100644 --- a/src/storage/prism/Variable.h +++ b/src/storage/prism/Variable.h @@ -55,6 +55,7 @@ namespace storm { */ storm::expressions::Expression getExpression() const; + // Make the constructors protected to forbid instantiation of this class. protected: Variable() = default;