From d3c80dca1653f79dc58ad1d38e29f23df1300598 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 20 May 2013 21:48:19 +0200 Subject: [PATCH] Updated CMakeLists.txt - Added more sub-folders in the source-structure - Added an option for MSVC to use /bigobj with the Compiler as PrismParser.cpp bloats the object instance count - Edited CUDD Link Targets for MSVC Edited SymbolicModelAdapter.h, added an alternative implementation for log2 (NOT part of C90, not of Cxx!) Edited Program.cpp, promoted vars from int to uint to conquer warnings related to loss of precision Likewise in DeterministicSparseTransitionParser.cpp, IntegerConstantExpression.h Edited storm.cpp, reimplemented Usage-Query for non-Unix platforms. Edited CuddUtility.h, added an include for int Type definitions as they do not fall from the sky Edited ErrorHandling.h. reimplemented ErrorHandling for non-Unix platforms. Backtraces can not yet be provided. --- CMakeLists.txt | 41 ++++++++++++++++--- src/adapters/SymbolicModelAdapter.h | 13 +++++- src/ir/Program.cpp | 14 +++---- .../expressions/IntegerConstantExpression.h | 2 +- .../DeterministicSparseTransitionParser.cpp | 2 +- src/storm.cpp | 36 ++++++++++++++-- src/utility/CuddUtility.h | 2 + src/utility/ErrorHandling.h | 38 +++++++++++++++-- src/utility/OsDetection.h | 15 +++++++ 9 files changed, 140 insertions(+), 23 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a78fb8925..bec5a07dc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -90,6 +90,8 @@ elseif(MSVC) message(STATUS "Using MSVC") # required for GMM to compile, ugly error directive in their code add_definitions(/D_SCL_SECURE_NO_DEPRECATE) + # required as the PRCTL Parser bloats object files (COFF) beyond their maximum size (see http://msdn.microsoft.com/en-us/library/8578y171(v=vs.110).aspx) + add_definitions(/bigobj) else(CLANG) message(STATUS "Using CLANG") # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. @@ -120,13 +122,19 @@ file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE}") file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) -file(GLOB_RECURSE STORM_FORMULA_FILES ${PROJECT_SOURCE_DIR}/src/formula/*.h ${PROJECT_SOURCE_DIR}/src/formula/*.cpp) +file(GLOB STORM_FORMULA_FILES ${PROJECT_SOURCE_DIR}/src/formula/*.h ${PROJECT_SOURCE_DIR}/src/formula/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_ABSTRACT_FILES ${PROJECT_SOURCE_DIR}/src/formula/abstract/*.h ${PROJECT_SOURCE_DIR}/src/formula/abstract/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_CSL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Csl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Csl/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_LTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) -file(GLOB_RECURSE STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) +file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) +file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) -file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) +file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) +file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp) # Test Sources # Note that the tests also need the source files, except for the main file @@ -138,12 +146,18 @@ source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(formula FILES ${STORM_FORMULA_FILES}) +source_group(formula\\abstract FILES ${STORM_FORMULA_ABSTRACT_FILES}) +source_group(formula\\csl FILES ${STORM_FORMULA_CSL_FILES}) +source_group(formula\\ltl FILES ${STORM_FORMULA_LTL_FILES}) +source_group(formula\\prctl FILES ${STORM_FORMULA_PRCTL_FILES}) source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) +source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(ir FILES ${STORM_IR_FILES}) +source_group(ir\\expressions FILES ${STORM_IR_EXPRESSIONS_FILES}) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) @@ -236,6 +250,14 @@ target_link_libraries(storm ${Boost_LIBRARIES}) target_link_libraries(storm-functional-tests ${Boost_LIBRARIES}) target_link_libraries(storm-performance-tests ${Boost_LIBRARIES}) +if (MSVC) + # Add the DebugHelper DLL + set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib") + target_link_libraries(storm "Dbghelp.lib") + target_link_libraries(storm-functional-tests "Dbghelp.lib") + target_link_libraries(storm-performance-tests "Dbghelp.lib") +endif(MSVC) + if (USE_INTELTBB) target_link_libraries(storm tbb tbbmalloc) target_link_libraries(storm-functional-tests tbb tbbmalloc) @@ -318,9 +340,16 @@ if (LOG4CPLUS_INCLUDE_DIR) endif(LOG4CPLUS_INCLUDE_DIR) if (CUDD_LIBRARY_DIRS) - target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") - target_link_libraries(storm-functional-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") - target_link_libraries(storm-performance-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + if (MSVC) + set(cuddMsvcLibs "optimized" "${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/CUDD_Win32/x64/Release/CUDD_Win32.lib" "debug" "${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/CUDD_Win32/x64/Debug/CUDD_Win32.lib") + target_link_libraries(storm ${cuddMsvcLibs}) + target_link_libraries(storm-functional-tests ${cuddMsvcLibs}) + target_link_libraries(storm-performance-tests ${cuddMsvcLibs}) + else () + target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-functional-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-performance-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + endif () endif(CUDD_LIBRARY_DIRS) if (THREADS_FOUND) diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index 06b7dd37f..819133a23 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/src/adapters/SymbolicModelAdapter.h @@ -16,6 +16,7 @@ #include "cuddObj.hh" #include #include +#include namespace storm { @@ -138,6 +139,16 @@ private: SymbolicExpressionAdapter rowExpressionAdapter; SymbolicExpressionAdapter columnExpressionAdapter; + // As log2 is not part of C90, only of C99 which no Compiler fully supports, this feature is unavailable on MSVC + inline double log2(uint_fast64_t number) { +# include "src/utility/OsDetection.h" +# ifndef WINDOWS + return std::log2(number); +# else + return std::log(number) / std::log(2); +# endif + } + ADD* getInitialStateDecisionDiagram(storm::ir::Program const& program) { ADD* initialStates = cuddUtility->getOne(); for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { @@ -258,7 +269,7 @@ private: throw storm::exceptions::WrongFormatException() << "Range of variable " << integerVariable.getName() << " is empty or negativ."; } - uint_fast64_t numberOfDecisionDiagramVariables = static_cast(std::ceil(std::log2(integerRange))); + uint_fast64_t numberOfDecisionDiagramVariables = static_cast(std::ceil(log2(integerRange))); std::vector allRowDecisionDiagramVariablesForVariable; std::vector allColumnDecisionDiagramVariablesForVariable; diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 96ad94b2b..c854bc645 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -119,24 +119,24 @@ std::map> P } std::string Program::getVariableString() const { - std::map bools; - std::map ints; - unsigned maxInt = 0, maxBool = 0; + std::map bools; + std::map ints; + uint_fast64_t maxInt = 0, maxBool = 0; for (Module module: this->modules) { - for (unsigned int i = 0; i < module.getNumberOfBooleanVariables(); i++) { + for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); i++) { storm::ir::BooleanVariable var = module.getBooleanVariable(i); bools[var.getIndex()] = var.getName(); if (var.getIndex() >= maxBool) maxBool = var.getIndex()+1; } - for (unsigned int i = 0; i < module.getNumberOfIntegerVariables(); i++) { + for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); i++) { storm::ir::IntegerVariable var = module.getIntegerVariable(i); ints[var.getIndex()] = var.getName(); if (var.getIndex() >= maxInt) maxInt = var.getIndex()+1; } } std::stringstream ss; - for (unsigned int i = 0; i < maxBool; i++) ss << bools[i] << "\t"; - for (unsigned int i = 0; i < maxInt; i++) ss << ints[i] << "\t"; + for (uint_fast64_t i = 0; i < maxBool; i++) ss << bools[i] << "\t"; + for (uint_fast64_t i = 0; i < maxInt; i++) ss << ints[i] << "\t"; return ss.str(); } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index c4ad56ed7..1cc3450e5 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -62,7 +62,7 @@ public: return defined; } - int getValue() { + int_fast64_t getValue() { return value; } diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 62e6481cc..d28e1c0d3 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -59,7 +59,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas * Check all transitions for non-zero diagonal entries and deadlock states. */ int_fast64_t lastRow = -1; - int_fast64_t row, col; + uint_fast64_t row, col; uint_fast64_t readTransitionCount = 0; bool rowHadDiagonalEntry = false; double val; diff --git a/src/storm.cpp b/src/storm.cpp index 548399d38..3c3d47679 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -45,17 +45,47 @@ #include "src/exceptions/InvalidSettingsException.h" -#include -#include #include #include void printUsage() { +#ifndef WINDOWS struct rusage ru; getrusage(RUSAGE_SELF, &ru); std::cout << "Memory Usage: " << ru.ru_maxrss << "kB" << std::endl; - std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << "CPU Time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; +#else + HANDLE hProcess = GetCurrentProcess (); + FILETIME ftCreation, ftExit, ftUser, ftKernel; + PROCESS_MEMORY_COUNTERS pmc; + if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { + std::cout << "Memory Usage: " << std::endl; + std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; + std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; + std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; + std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; + std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; + std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; + std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; + std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; + std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; + } + + GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); + + ULARGE_INTEGER uLargeInteger; + uLargeInteger.LowPart = ftKernel.dwLowDateTime; + uLargeInteger.HighPart = ftKernel.dwHighDateTime; + double kernelTime = uLargeInteger.QuadPart / 10000.0; // 100 ns Resolution to milliseconds + uLargeInteger.LowPart = ftUser.dwLowDateTime; + uLargeInteger.HighPart = ftUser.dwHighDateTime; + double userTime = uLargeInteger.QuadPart / 10000.0; + + std::cout << "CPU Time: " << std::endl; + std::cout << "\tKernel Time: " << std::setprecision(3) << kernelTime << std::endl; + std::cout << "\tUser Time: " << std::setprecision(3) << userTime << std::endl; +#endif } diff --git a/src/utility/CuddUtility.h b/src/utility/CuddUtility.h index 8102eb012..2832884a2 100644 --- a/src/utility/CuddUtility.h +++ b/src/utility/CuddUtility.h @@ -10,6 +10,8 @@ #include "cuddObj.hh" +#include "boost/integer/integer_mask.hpp" + namespace storm { namespace utility { diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h index ea65ab03a..b832b7c69 100644 --- a/src/utility/ErrorHandling.h +++ b/src/utility/ErrorHandling.h @@ -8,9 +8,9 @@ #ifndef ERRORHANDLING_H #define ERRORHANDLING_H +#include "src/utility/OsDetection.h" #include -#include -#include + /* * Demangles the given string. This is needed for the correct display of backtraces. @@ -22,16 +22,42 @@ std::string demangle(char const* symbol) { // Attention: sscanf format strings rely on the size being 128. char temp[128]; - char* demangled; - // Check for C++ symbol. + // Check for C++ symbol, on Non-MSVC Only if (sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp) == 1) { +#ifndef WINDOWS + char* demangled; if (NULL != (demangled = abi::__cxa_demangle(temp, NULL, NULL, &status))) { std::string result(demangled); free(demangled); return result; } +#else + DWORD error; + HANDLE hProcess; + + SymSetOptions(SYMOPT_UNDNAME | SYMOPT_DEFERRED_LOADS); + + hProcess = GetCurrentProcess(); + + if (!SymInitialize(hProcess, NULL, TRUE)) { + // SymInitialize failed + error = GetLastError(); + LOG4CPLUS_ERROR(logger, "SymInitialize returned error : " << error); + return FALSE; + } else { + char demangled[1024]; + if (UnDecorateSymbolName(temp, demangled, sizeof(demangled), UNDNAME_COMPLETE)) { + return std::string(demangled); + } else { + // UnDecorateSymbolName failed + DWORD error = GetLastError(); + LOG4CPLUS_ERROR(logger, "UnDecorateSymbolName returned error: " << error); + } + } +#endif } + // Check for C symbol. if (sscanf(symbol, "%127s", temp) == 1) { return temp; @@ -50,6 +76,7 @@ void signalHandler(int sig) { #define SIZE 128 LOG4CPLUS_FATAL(logger, "The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal."); +#ifndef WINDOWS void *buffer[SIZE]; char **strings; int nptrs; @@ -68,6 +95,9 @@ void signalHandler(int sig) { LOG4CPLUS_FATAL(logger, nptrs-j << ": " << demangle(strings[j])); } free(strings); +#else + LOG4CPLUS_WARN(logger, "No Backtrace Support available on Platform Windows!"); +#endif LOG4CPLUS_FATAL(logger, "Exiting."); exit(2); } diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h index bc459d40c..8fb6c7c6e 100644 --- a/src/utility/OsDetection.h +++ b/src/utility/OsDetection.h @@ -4,17 +4,32 @@ #if defined __linux__ || defined __linux # define LINUX # include +#include // Required by ErrorHandling.h +#include // Required by ErrorHandling.h +#include // Required by storm.cpp, Memory Usage +#include // Required by storm.cpp, Memory Usage #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ # define MACOSX # define _DARWIN_USE_64_BIT_INODE # include # include +# include // Required by ErrorHandling.h +# include // Required by ErrorHandling.h +# include // Required by storm.cpp, Memory Usage +# include // Required by storm.cpp, Memory Usage #elif defined _WIN32 || defined _WIN64 # define WINDOWS # define NOMINMAX # include # include +# include +# include # define strncpy strncpy_s +# define sscanf sscanf_s + +// This disables Warning C4250 - Diamond Inheritance Dominance +#pragma warning(disable:4250) + #else # error Could not detect Operating System #endif