From 9a0e42babbc01734a35e2d87beb70ac0261b6788 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
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<IntegerVariable> 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<storm::expressions::Variable> 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<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
+ std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
+ for(auto const& module : this->getModules()) {
+ std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
+ std::set<std::pair<std::string, std::string>> 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;