diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 000000000..09bf8b6a0 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,40 @@ +language: generic +dist: trusty +sudo: required +compiler: clang + +env: + global: + - COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang + matrix: + - TRAVIS_ENV="--exhaustive --folder=basic" + - TRAVIS_ENV="--exhaustive --folder=ntdrivers-simplified" + - TRAVIS_ENV="--exhaustive --folder=pthread_extras" + - TRAVIS_ENV="--exhaustive --folder=bits" + - TRAVIS_ENV="--exhaustive --folder=float" + - TRAVIS_ENV="--exhaustive --folder=locks" + - TRAVIS_ENV="--exhaustive --folder=contracts" + - TRAVIS_ENV="--exhaustive --folder=memory-safety" + - TRAVIS_ENV="--exhaustive --folder=pthread" + +before_install: + - sudo rm -rf /usr/local/clang-3.5.0 + - sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.7 main" + - wget -O - http://llvm-apt.ecranbleu.org/apt/llvm-snapshot.gpg.key | sudo apt-key add - + - sudo apt-get update + +install: + - sudo apt-get install -y clang-3.7 llvm-3.7 + - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.7 20 + - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.7 20 + - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.7 20 + - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.7 20 + - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.7 20 + +script: + - $CXX --version + - $CC --version + - clang --version + - clang++ --version + - ./bin/build.sh + diff --git a/CMakeLists.txt b/CMakeLists.txt index 80ad325c0..a8c47394f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,7 +6,7 @@ cmake_minimum_required(VERSION 2.8) project(smack) if (NOT WIN32 OR MSYS OR CYGWIN) - find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") + find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-3.8 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND") message(FATAL_ERROR "llvm-config could not be found!") @@ -18,7 +18,10 @@ if (NOT WIN32 OR MSYS OR CYGWIN) OUTPUT_STRIP_TRAILING_WHITESPACE ) - set(LLVM_CXXFLAGS "${LLVM_CXXFLAGS} -fno-exceptions -fno-rtti") + string(REGEX REPLACE "-O[0-9]" "" CMAKE_CXX_FLAGS "${LLVM_CXXFLAGS}") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-exceptions -fno-rtti") + set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0") + set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0") execute_process( COMMAND ${LLVM_CONFIG_EXECUTABLE} --libs @@ -52,7 +55,12 @@ else() message(FATAL_ERROR "Invalid LLVM build directory: ${LLVM_BUILD}") endif() - set(LLVM_CXXFLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800") + ## TODO how to enable debug mode on Windows? + # set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0") + # set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0") + + set(CMAKE_CXX_FLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800") + set(LLVM_LDFLAGS "") set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib" "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib" "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib" "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib" "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib") @@ -146,7 +154,7 @@ add_library(smackTranslator STATIC include/smack/BoogieAst.h include/smack/BplFilePrinter.h include/smack/BplPrinter.h - include/smack/DSAAliasAnalysis.h + include/smack/DSAWrapper.h include/smack/Naming.h include/smack/Regions.h include/smack/SmackInstGenerator.h @@ -157,13 +165,12 @@ add_library(smackTranslator STATIC include/smack/ExtractContracts.h include/smack/SimplifyLibCalls.h include/smack/SmackRep.h - include/smack/SmackRepFlatMem.h include/smack/MemorySafetyChecker.h include/smack/SignedIntegerOverflowChecker.h lib/smack/BoogieAst.cpp lib/smack/BplFilePrinter.cpp lib/smack/BplPrinter.cpp - lib/smack/DSAAliasAnalysis.cpp + lib/smack/DSAWrapper.cpp lib/smack/Naming.cpp lib/smack/Regions.cpp lib/smack/SmackInstGenerator.cpp @@ -174,7 +181,6 @@ add_library(smackTranslator STATIC lib/smack/ExtractContracts.cpp lib/smack/SimplifyLibCalls.cpp lib/smack/SmackRep.cpp - lib/smack/SmackRepFlatMem.cpp lib/smack/MemorySafetyChecker.cpp lib/smack/SignedIntegerOverflowChecker.cpp ) @@ -183,9 +189,6 @@ add_executable(llvm2bpl tools/llvm2bpl/llvm2bpl.cpp ) -set_target_properties(llvm2bpl smackTranslator assistDS dsa - PROPERTIES COMPILE_FLAGS "${LLVM_CXXFLAGS}") - target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS}) target_link_libraries(llvm2bpl smackTranslator assistDS dsa) diff --git a/Doxyfile b/Doxyfile index efb242cef..6b58ee608 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 1.7.2 +PROJECT_NUMBER = 1.8.0 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/README.md b/README.md index 6bee8d1f3..758140829 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ -[![Build Status](http://kornat.cs.utah.edu:8080/job/smack/badge/icon)](http://kornat.cs.utah.edu:8080/job/smack/) +| **master** | [![Build Status](https://travis-ci.org/smackers/smack.svg?branch=master)](https://travis-ci.org/smackers/smack) | **develop** | [![Build Status](https://travis-ci.org/smackers/smack.svg?branch=develop)](https://travis-ci.org/smackers/smack) | +| --- | --- | --- | --- | SMACK Logo diff --git a/bin/build.sh b/bin/build.sh index 5920c2d98..2eb6c2ebf 100755 --- a/bin/build.sh +++ b/bin/build.sh @@ -43,7 +43,7 @@ LLVM_DIR="${ROOT}/llvm" source ${SMACK_DIR}/bin/versions SMACKENV=${ROOT}/smack.environment -WGET="wget --no-verbose --method=GET" +WGET="wget --no-verbose" # Install prefix -- system default is used if left unspecified INSTALL_PREFIX= @@ -160,9 +160,9 @@ linux-opensuse*) DEPENDENCIES+=" ncurses-devel zlib-devel" ;; -linux-ubuntu-14*) +linux-ubuntu-1[46]*) Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip" - DEPENDENCIES+=" clang-3.7 llvm-3.7 mono-complete libz-dev libedit-dev" + DEPENDENCIES+=" clang-3.8 llvm-3.8 mono-complete libz-dev libedit-dev" ;; linux-ubuntu-12*) @@ -221,9 +221,9 @@ then sudo zypper --non-interactive install ${DEPENDENCIES} ;; - linux-ubuntu-14*) + linux-ubuntu-1[46]*) # Adding LLVM repository - sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.7 main" + sudo add-apt-repository "deb http://llvm-apt.ecranbleu.org/apt/trusty/ llvm-toolchain-trusty-3.8 main" ${WGET} -O - http://llvm-apt.ecranbleu.org/apt/llvm-snapshot.gpg.key | sudo apt-key add - # Adding MONO repository sudo add-apt-repository "deb http://download.mono-project.com/repo/debian wheezy main" @@ -231,11 +231,11 @@ then # echo "deb http://download.mono-project.com/repo/debian wheezy main" | sudo tee /etc/apt/sources.list.d/mono-xamarin.list sudo apt-get update sudo apt-get install -y ${DEPENDENCIES} - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.7 20 - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.7 20 - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.7 20 - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.7 20 - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.7 20 + sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.8 20 + sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.8 20 + sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.8 20 + sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.8 20 + sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.8 20 ;; linux-ubuntu-12*) @@ -299,16 +299,16 @@ then mkdir -p ${LLVM_DIR}/src/{tools/clang,projects/compiler-rt} mkdir -p ${LLVM_DIR}/build - ${WGET} http://llvm.org/releases/3.7.1/llvm-3.7.1.src.tar.xz - ${WGET} http://llvm.org/releases/3.7.1/cfe-3.7.1.src.tar.xz - ${WGET} http://llvm.org/releases/3.7.1/compiler-rt-3.7.1.src.tar.xz + ${WGET} http://llvm.org/releases/3.8.1/llvm-3.8.1.src.tar.xz + ${WGET} http://llvm.org/releases/3.8.1/cfe-3.8.1.src.tar.xz + ${WGET} http://llvm.org/releases/3.8.1/compiler-rt-3.8.1.src.tar.xz - tar -C ${LLVM_DIR}/src -xvf llvm-3.7.1.src.tar.xz --strip 1 - tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-3.7.1.src.tar.xz --strip 1 - tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-3.7.1.src.tar.xz --strip 1 + tar -C ${LLVM_DIR}/src -xvf llvm-3.8.1.src.tar.xz --strip 1 + tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-3.8.1.src.tar.xz --strip 1 + tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-3.8.1.src.tar.xz --strip 1 cd ${LLVM_DIR}/build/ - cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src + cmake -G "Unix Makefiles" ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src make sudo make install @@ -340,7 +340,7 @@ then ${WGET} https://nuget.org/nuget.exe mono ./nuget.exe restore Boogie.sln rm -rf /tmp/nuget/ - xbuild Boogie.sln /p:Configuration=Release + msbuild Boogie.sln /p:Configuration=Release ln -s ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe puts "Built Boogie" @@ -356,7 +356,7 @@ then git reset --hard ${CORRAL_COMMIT} git submodule init git submodule update - xbuild cba.sln /p:Configuration=Release + msbuild cba.sln /p:Configuration=Release ln -s ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe puts "Built Corral" @@ -370,7 +370,7 @@ then git clone https://github.com/smackers/lockpwn.git cd ${LOCKPWN_DIR} git reset --hard ${LOCKPWN_COMMIT} - xbuild lockpwn.sln /p:Configuration=Release + msbuild lockpwn.sln /p:Configuration=Release ln -s ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe puts "Built lockpwn" @@ -403,7 +403,7 @@ then puts "Running SMACK regression tests" cd ${SMACK_DIR}/test - ./regtest.py + ./regtest.py ${TRAVIS_ENV} res=$? puts "Regression tests complete" diff --git a/bin/package-smack.sh b/bin/package-smack.sh index 1cfeea4b7..008d30852 100755 --- a/bin/package-smack.sh +++ b/bin/package-smack.sh @@ -6,7 +6,7 @@ # Note: this script requires CDE to be downloaded from # http://www.pgbovine.net/cde.html -VERSION=1.7.2 +VERSION=1.8.0 PACKAGE=smack-$VERSION-64 # Create folder to export diff --git a/bin/versions b/bin/versions index a486ead0c..cfd848bf3 100644 --- a/bin/versions +++ b/bin/versions @@ -1,4 +1,4 @@ -MONO_VERSION=3.8.0 +MONO_VERSION=5.0.0.100 BOOGIE_COMMIT=4e4c3a5252 CORRAL_COMMIT=874a078e39 LOCKPWN_COMMIT=a4d802a1cb diff --git a/docs/installation.md b/docs/installation.md index 398a96324..6d3a471a9 100644 --- a/docs/installation.md +++ b/docs/installation.md @@ -59,10 +59,10 @@ vagrant destroy SMACK depends on the following projects: -* [LLVM][] version [3.7.1][LLVM-3.7.1] -* [Clang][] version [3.7.1][Clang-3.7.1] +* [LLVM][] version [3.8.1][LLVM-3.8.1] +* [Clang][] version [3.8.1][Clang-3.8.1] * [Python][] version 2.7 or greater -* [Mono][] version 3.8.0 or greater (except on Windows) +* [Mono][] version 5.0.0 or greater (except on Windows) * [Z3][] or compatible SMT-format theorem prover * [Boogie][] or [Corral][] or compatible Boogie-format verifier @@ -168,9 +168,9 @@ shell in the `test` directory by executing [CMake]: http://www.cmake.org [Python]: http://www.python.org [LLVM]: http://llvm.org -[LLVM-3.7.1]: http://llvm.org/releases/download.html#3.7.1 +[LLVM-3.8.1]: http://llvm.org/releases/download.html#3.8.1 [Clang]: http://clang.llvm.org -[Clang-3.7.1]: http://llvm.org/releases/download.html#3.7.1 +[Clang-3.8.1]: http://llvm.org/releases/download.html#3.8.1 [Boogie]: https://github.com/boogie-org/boogie [Corral]: https://corral.codeplex.com/ [Z3]: https://github.com/Z3Prover/z3/ diff --git a/include/smack/CodifyStaticInits.h b/include/smack/CodifyStaticInits.h index e97a88265..871c20b37 100644 --- a/include/smack/CodifyStaticInits.h +++ b/include/smack/CodifyStaticInits.h @@ -6,7 +6,6 @@ #include "llvm/IR/Instructions.h" #include "llvm/IR/Module.h" #include "llvm/Pass.h" -#include "smack/DSAAliasAnalysis.h" namespace smack { diff --git a/include/smack/DSAAliasAnalysis.h b/include/smack/DSAWrapper.h similarity index 77% rename from include/smack/DSAAliasAnalysis.h rename to include/smack/DSAWrapper.h index c4b8d6e5c..caf781d14 100644 --- a/include/smack/DSAAliasAnalysis.h +++ b/include/smack/DSAWrapper.h @@ -1,19 +1,11 @@ -//===- DataStructureAA.cpp - Data Structure Based Alias Analysis ----------===// // // The LLVM Compiler Infrastructure // // This file was developed by the LLVM research group and is distributed under -// the University of Illinois Open Source License. See LICENSE.TXT for details. +// the University of Illinois Open Source License. See LICENSE for details. // -//===----------------------------------------------------------------------===// -// -// This pass uses the top-down data structure graphs to implement a simple -// context sensitive alias analysis. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_ANALYSIS_DATA_STRUCTURE_AA_H -#define LLVM_ANALYSIS_DATA_STRUCTURE_AA_H +#ifndef DSAWRAPPER_H +#define DSAWRAPPER_H #include "assistDS/DSNodeEquivs.h" #include "dsa/DataStructure.h" @@ -61,7 +53,7 @@ class MemcpyCollector : public llvm::InstVisitor { } }; -class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis { +class DSAWrapper : public llvm::ModulePass { private: llvm::Module *module; llvm::TDDataStructures *TD; @@ -73,14 +65,16 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis { std::unordered_set intConversions; const DataLayout* dataLayout; + std::vector collectMemcpys(llvm::Module &M, MemcpyCollector* mcc); + std::vector collectStaticInits(llvm::Module &M); + llvm::DSGraph *getGraphForValue(const llvm::Value *V); + unsigned getOffset(const MemoryLocation* l); + public: static char ID; - DSAAliasAnalysis() : ModulePass(ID) {} - - void printDSAGraphs(const char* Filename); + DSAWrapper() : ModulePass(ID) {} virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const { - llvm::AliasAnalysis::getAnalysisUsage(AU); AU.setPreservesAll(); AU.addRequiredTransitive(); AU.addRequiredTransitive(); @@ -90,7 +84,6 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis { virtual bool runOnModule(llvm::Module &M) { dataLayout = &M.getDataLayout(); - InitializeAliasAnalysis(this, dataLayout); TD = &getAnalysis(); BU = &getAnalysis(); nodeEqs = &getAnalysis(); @@ -101,29 +94,19 @@ class DSAAliasAnalysis : public llvm::ModulePass, public llvm::AliasAnalysis { return false; } - const llvm::DSNode *getNode(const llvm::Value* v); - bool isAlloced(const llvm::Value* v); - bool isExternal(const llvm::Value* v); - bool isSingletonGlobal(const llvm::Value *V); + bool isMemcpyd(const llvm::DSNode* n); + bool isStaticInitd(const llvm::DSNode* n); bool isFieldDisjoint(const llvm::Value* V, const llvm::Function* F); bool isFieldDisjoint(const GlobalValue* V, unsigned offset); bool isRead(const llvm::Value* V); - bool isMemcpyd(const llvm::DSNode* n); - bool isStaticInitd(const llvm::DSNode* n); + bool isAlloced(const llvm::Value* v); + bool isExternal(const llvm::Value* v); + bool isSingletonGlobal(const llvm::Value *V); unsigned getPointedTypeSize(const Value* v); unsigned getOffset(const Value* v); - - virtual AliasResult alias(const MemoryLocation &LocA, const MemoryLocation &LocB); - -private: - bool isComplicatedNode(const llvm::DSNode* n); - std::vector collectMemcpys(llvm::Module &M, MemcpyCollector* mcc); - std::vector collectStaticInits(llvm::Module &M); - llvm::DSGraph *getGraphForValue(const llvm::Value *V); - bool equivNodes(const llvm::DSNode* n1, const llvm::DSNode* n2); - unsigned getOffset(const MemoryLocation* l); - bool disjoint(const MemoryLocation* l1, const MemoryLocation* l2); + const llvm::DSNode *getNode(const llvm::Value* v); + void printDSAGraphs(const char* Filename); }; } -#endif +#endif // DSAWRAPPER_H diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 7f54962e5..918c3d889 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -1,11 +1,11 @@ // // This file is distributed under the MIT License. See LICENSE for details. // -#ifndef REGION_H -#define REGION_H +#ifndef REGIONS_H +#define REGIONS_H #include "dsa/DSGraph.h" -#include "smack/DSAAliasAnalysis.h" +#include "smack/DSAWrapper.h" namespace smack { @@ -25,7 +25,7 @@ class Region { bool collapsed; static const DataLayout* DL; - static DSAAliasAnalysis* DSA; + static DSAWrapper* DSA; // static DSNodeEquivs* NEQS; static bool isSingleton(const DSNode* N, unsigned offset, unsigned length); @@ -55,7 +55,7 @@ class Region { }; class Regions : public ModulePass, public InstVisitor { - +private: std::vector regions; unsigned idx(Region& R); @@ -90,4 +90,4 @@ class Regions : public ModulePass, public InstVisitor { } -#endif // REGION_H +#endif // REGIONS_H diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index bb4a0162e..5402370de 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -37,6 +37,8 @@ class SmackInstGenerator : public llvm::InstVisitor { void nameInstruction(llvm::Instruction& i); void annotate(llvm::Instruction& i, Block* b); + const Stmt* recordProcedureCall(llvm::Value* V, std::list attrs); + public: void emit(const Stmt* s) { // stringstream str; diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h index 8ab5f4c9d..b11dded1b 100644 --- a/include/smack/SmackModuleGenerator.h +++ b/include/smack/SmackModuleGenerator.h @@ -6,8 +6,6 @@ #include "smack/BoogieAst.h" #include "smack/SmackInstGenerator.h" -#include "smack/DSAAliasAnalysis.h" -#include "llvm/Analysis/AliasAnalysis.h" #include "llvm/Analysis/LoopInfo.h" #include "llvm/IR/DataLayout.h" #include "llvm/IR/CFG.h" diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 680738711..86ea8488a 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -5,7 +5,6 @@ #define SMACKREP_H #include "smack/BoogieAst.h" -#include "smack/DSAAliasAnalysis.h" #include "smack/Naming.h" #include "smack/Regions.h" #include "smack/SmackOptions.h" diff --git a/include/smack/SmackRepFlatMem.h b/include/smack/SmackRepFlatMem.h deleted file mode 100644 index 00078f1eb..000000000 --- a/include/smack/SmackRepFlatMem.h +++ /dev/null @@ -1,24 +0,0 @@ -// -// This file is distributed under the MIT License. See LICENSE for details. -// -#ifndef SMACKREPFLATMEM_H -#define SMACKREPFLATMEM_H - -#include "smack/SmackRep.h" - -namespace smack { - -using llvm::Regex; -using llvm::SmallVector; -using llvm::StringRef; - -class SmackRepFlatMem : public SmackRep { - - int bottom; - -public: - SmackRepFlatMem(DSAAliasAnalysis* aa) : SmackRep(aa), bottom(0) {} -}; -} - -#endif // SMACKREPFLATMEM_H diff --git a/lib/AssistDS/ArgCast.cpp b/lib/AssistDS/ArgCast.cpp index 9f2039753..ae3cf37b8 100644 --- a/lib/AssistDS/ArgCast.cpp +++ b/lib/AssistDS/ArgCast.cpp @@ -52,18 +52,18 @@ STATISTIC(numChanged, "Number of Args bitcasted"); bool ArgCast::runOnModule(Module& M) { std::vector worklist; - for (Module::iterator I = M.begin(); I != M.end(); ++I) { - if (I->mayBeOverridden()) + for (Function &F : M) { + if (F.mayBeOverridden()) continue; // Find all uses of this function - for(Value::user_iterator ui = I->user_begin(), ue = I->user_end(); ui != ue; ) { + for (User *U : F.users()) { // check if is ever casted to a different function type - ConstantExpr *CE = dyn_cast(*ui++); + ConstantExpr *CE = dyn_cast(U++); if(!CE) continue; if (CE->getOpcode() != Instruction::BitCast) continue; - if(CE->getOperand(0) != I) + if(CE->getOperand(0) != &F) continue; const PointerType *PTy = dyn_cast(CE->getType()); if (!PTy) @@ -76,7 +76,7 @@ bool ArgCast::runOnModule(Module& M) { // or function with same number of arguments // possibly varying types of arguments - if(FTy->getNumParams() != I->arg_size() && !FTy->isVarArg()) + if(FTy->getNumParams() != F.arg_size() && !FTy->isVarArg()) continue; for(Value::user_iterator uii = CE->user_begin(), uee = CE->user_end(); uii != uee; ++uii) { @@ -88,11 +88,11 @@ bool ArgCast::runOnModule(Module& M) { continue; // Check that the number of arguments passed, and expected // by the function are the same. - if(!I->isVarArg()) { - if(CI->getNumOperands() != I->arg_size() + 1) + if(!F.isVarArg()) { + if(CI->getNumOperands() != F.arg_size() + 1) continue; } else { - if(CI->getNumOperands() < I->arg_size() + 1) + if(CI->getNumOperands() < F.arg_size() + 1) continue; } // If so, add to worklist diff --git a/lib/AssistDS/ArgSimplify.cpp b/lib/AssistDS/ArgSimplify.cpp index 26459eb80..93acdb15f 100644 --- a/lib/AssistDS/ArgSimplify.cpp +++ b/lib/AssistDS/ArgSimplify.cpp @@ -86,10 +86,9 @@ namespace { "argbounce", M); std::vector fargs; - for(Function::arg_iterator ai = NewF->arg_begin(), - ae= NewF->arg_end(); ai != ae; ++ai) { - fargs.push_back(ai); - ai->setName("arg"); + for (auto &Arg : NewF->args()) { + fargs.push_back(&Arg); + Arg.setName("arg"); } Value *CastedVal; BasicBlock* entryBB = BasicBlock:: @@ -105,12 +104,11 @@ namespace { } SmallVector Args; - for(Function::arg_iterator ai = NewF->arg_begin(), - ae= NewF->arg_end(); ai != ae; ++ai) { - if(ai->getArgNo() == arg_count) + for (auto &Arg : NewF->args()) { + if(Arg.getArgNo() == arg_count) Args.push_back(CastedVal); else - Args.push_back(ai); + Args.push_back(&Arg); } CallInst * CallI = CallInst::Create(F,Args, @@ -142,18 +140,16 @@ namespace { bool runOnModule(Module& M) { - for (Module::iterator I = M.begin(); I != M.end(); ++I) - if (!I->isDeclaration() && !I->mayBeOverridden()) { - if(I->getName().str() == "main") + for (Function &F : M) + if (!F.isDeclaration() && !F.mayBeOverridden()) { + if(F.getName().str() == "main") continue; std::vector Args; - for (Function::arg_iterator ii = I->arg_begin(), ee = I->arg_end(); - ii != ee; ++ii) { + for (auto &Arg : F.args()) { bool change = true; - for(Value::user_iterator ui = ii->user_begin(), ue = ii->user_end(); - ui != ue; ++ui) { + for (User *U : Arg.users()) { // check if the argument is used exclusively in ICmp Instructions - if(!isa(*ui)){ + if(!isa(U)) { change = false; break; } @@ -161,7 +157,7 @@ namespace { // if this argument is only used in ICMP instructions, we can // replace it. if(change) { - simplify(I, ii->getArgNo(), ii->getType()); + simplify(&F, Arg.getArgNo(), Arg.getType()); } } } diff --git a/lib/AssistDS/DSNodeEquivs.cpp b/lib/AssistDS/DSNodeEquivs.cpp index ea8e2c8ac..942e333d6 100644 --- a/lib/AssistDS/DSNodeEquivs.cpp +++ b/lib/AssistDS/DSNodeEquivs.cpp @@ -149,7 +149,7 @@ void DSNodeEquivs::equivNodesThroughCallsite(CallInst *CI) { if (isa(*ArgIt)) continue; - DSNodeHandle &CalleeArgNH = CalleeGraph.getNodeForValue(FArgIt); + DSNodeHandle &CalleeArgNH = CalleeGraph.getNodeForValue(&*FArgIt); DSNodeHandle &CSArgNH = Graph.getNodeForValue(*ArgIt); DSGraph::computeNodeMapping(CalleeArgNH, CSArgNH, NodeMap, false); } diff --git a/lib/AssistDS/DataStructureCallGraph.cpp b/lib/AssistDS/DataStructureCallGraph.cpp index 7f039a17a..ab373174f 100644 --- a/lib/AssistDS/DataStructureCallGraph.cpp +++ b/lib/AssistDS/DataStructureCallGraph.cpp @@ -41,8 +41,8 @@ bool DataStructureCallGraph::runOnModule(Module &M) { Root = 0; // Add every function to the call graph. - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - addToCallGraph(I); + for (Function &F : M) + addToCallGraph(&F); // If we didn't find a main function, use the external call graph node if (Root == 0) Root = ExternalCallingNode; diff --git a/lib/AssistDS/Devirt.cpp b/lib/AssistDS/Devirt.cpp index fe9ab7f34..cff6e7b9d 100644 --- a/lib/AssistDS/Devirt.cpp +++ b/lib/AssistDS/Devirt.cpp @@ -266,7 +266,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector& Targets) { for (P = ++F->arg_begin(), PE = F->arg_end(), T = FT->param_begin(), TE = FT->param_end(); P != PE && T != TE; ++P, ++T) - Args.push_back(castTo(P, *T, "", BL)); + Args.push_back(castTo(&*P, *T, "", BL)); Value* directCall = CallInst::Create (const_cast(FL), Args, @@ -305,7 +305,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector& Targets) { // pointer and branch to the appropriate basic block to call the function. // Type * VoidPtrType = getVoidPtrType (M->getContext()); - Value * FArg = castTo (F->arg_begin(), VoidPtrType, "", InsertPt); + Value * FArg = castTo (&*F->arg_begin(), VoidPtrType, "", InsertPt); BasicBlock * tailBB = failBB; for (unsigned index = 0; index < Targets.size(); ++index) { // diff --git a/lib/AssistDS/FuncSimplify.cpp b/lib/AssistDS/FuncSimplify.cpp index 2aec9cdcc..c42084a92 100644 --- a/lib/AssistDS/FuncSimplify.cpp +++ b/lib/AssistDS/FuncSimplify.cpp @@ -46,11 +46,11 @@ STATISTIC(numChanged, "Number of aliases deleted"); bool FuncSimplify::runOnModule(Module& M) { std::vector toDelete; - for (Module::alias_iterator I = M.alias_begin(); I != M.alias_end(); ++I) { - if(!I->hasInternalLinkage()) + for (GlobalAlias &GA : M.aliases()) { + if(!GA.hasInternalLinkage()) continue; - I->replaceAllUsesWith(I->getAliasee()); - toDelete.push_back(I); + GA.replaceAllUsesWith(GA.getAliasee()); + toDelete.push_back(&GA); } numChanged += toDelete.size(); diff --git a/lib/AssistDS/FuncSpec.cpp b/lib/AssistDS/FuncSpec.cpp index 2d6b4bd7d..99f6a7c40 100644 --- a/lib/AssistDS/FuncSpec.cpp +++ b/lib/AssistDS/FuncSpec.cpp @@ -50,33 +50,31 @@ bool FuncSpec::runOnModule(Module& M) { std::map > > cloneSites; std::map > >, Function* > toClone; - for (Module::iterator I = M.begin(); I != M.end(); ++I) - if (!I->isDeclaration() && !I->mayBeOverridden()) { + for (Function &F : M) + if (!F.isDeclaration() && !F.mayBeOverridden()) { std::vector FPArgs; - for (Function::arg_iterator ii = I->arg_begin(), ee = I->arg_end(); - ii != ee; ++ii) { + for (auto &Arg : F.args()) { // check if this function has a FunctionType(or a pointer to) argument - if (const PointerType* Ty = dyn_cast(ii->getType())) { + if (const PointerType* Ty = dyn_cast(Arg.getType())) { if (isa(Ty->getElementType())) { // Store the index of such an argument - FPArgs.push_back(ii->getArgNo()); - DEBUG(errs() << "Eligible: " << I->getName().str() << "\n"); + FPArgs.push_back(Arg.getArgNo()); + DEBUG(errs() << "Eligible: " << F.getName().str() << "\n"); } - } else if (isa(ii->getType())) { + } else if (isa(Arg.getType())) { // Store the index of such an argument - FPArgs.push_back(ii->getArgNo()); - DEBUG(errs() << "Eligible: " << I->getName().str() << "\n"); + FPArgs.push_back(Arg.getArgNo()); + DEBUG(errs() << "Eligible: " << F.getName().str() << "\n"); } } // Now find all call sites that it is called from - for(Value::user_iterator ui = I->user_begin(), ue = I->user_end(); - ui != ue; ++ui) { - if (CallInst* CI = dyn_cast(*ui)) { + for (User *U : F.users()) { + if (CallInst* CI = dyn_cast(U)) { // Check that it is the called value (and not an argument) - if(CI->getCalledValue()->stripPointerCasts() == I) { + if(CI->getCalledValue()->stripPointerCasts() == &F) { std::vector > Consts; for (unsigned x = 0; x < FPArgs.size(); ++x) - if (Constant* C = dyn_cast(ui->getOperand(FPArgs.at(x) + 1))) { + if (Constant* C = dyn_cast(U->getOperand(FPArgs.at(x) + 1))) { // If the argument passed, at any of the locations noted earlier // is a constant function, store the pair Consts.push_back(std::make_pair(FPArgs.at(x), C)); @@ -85,7 +83,7 @@ bool FuncSpec::runOnModule(Module& M) { // If at least one of the arguments is a constant function, // we must clone the function. cloneSites[CI] = Consts; - toClone[std::make_pair(I, Consts)] = 0; + toClone[std::make_pair(&F, Consts)] = 0; } } } diff --git a/lib/AssistDS/GEPExprArgs.cpp b/lib/AssistDS/GEPExprArgs.cpp index 7c30e39b7..cda681875 100644 --- a/lib/AssistDS/GEPExprArgs.cpp +++ b/lib/AssistDS/GEPExprArgs.cpp @@ -109,14 +109,14 @@ bool GEPExprArgs::runOnModule(Module& M) { F->getName().str() + ".TEST", &M); - Function::arg_iterator NI = NewF->arg_begin(); + auto NI = NewF->arg_begin(); NI->setName("GEParg"); ++NI; ValueToValueMapTy ValueMap; - for (Function::arg_iterator II = F->arg_begin(); NI != NewF->arg_end(); ++II, ++NI) { - ValueMap[II] = NI; + for (auto II = F->arg_begin(); NI != NewF->arg_end(); ++II, ++NI) { + ValueMap[&*II] = &*NI; NI->setName(II->getName()); NI->addAttr(F->getAttributes().getParamAttributes(II->getArgNo() + 1)); } @@ -126,9 +126,8 @@ bool GEPExprArgs::runOnModule(Module& M) { SmallVector Returns; CloneFunctionInto(NewF, F, ValueMap, false, Returns); std::vector fargs; - for(Function::arg_iterator ai = NewF->arg_begin(), - ae= NewF->arg_end(); ai != ae; ++ai) { - fargs.push_back(ai); + for (auto &Arg : NewF->args()) { + fargs.push_back(&Arg); } NewF->setAttributes(NewF->getAttributes().addAttributes( @@ -136,7 +135,7 @@ bool GEPExprArgs::runOnModule(Module& M) { //Get the point to insert the GEP instr. SmallVector Ops(CI->op_begin()+1, CI->op_end()); Instruction *InsertPoint; - for (BasicBlock::iterator insrt = NewF->front().begin(); + for (Instruction *insrt = &*NewF->front().begin(); isa(InsertPoint = insrt); ++insrt) {;} NI = NewF->arg_begin(); diff --git a/lib/AssistDS/IndCloner.cpp b/lib/AssistDS/IndCloner.cpp index 2618385bd..636b8bbab 100644 --- a/lib/AssistDS/IndCloner.cpp +++ b/lib/AssistDS/IndCloner.cpp @@ -62,7 +62,7 @@ IndClone::runOnModule(Module& M) { // by an indirect function call, add it to our worklist of functions to // clone. // - for (Module::iterator I = M.begin(); I != M.end(); ++I) { + for (Function &F : M) { // Flag whether the function should be cloned bool pleaseCloneTheFunction = false; @@ -70,11 +70,10 @@ IndClone::runOnModule(Module& M) { // Only clone functions which are defined and cannot be replaced by another // function by the linker. // - if (!I->isDeclaration() && !I->mayBeOverridden()) { - for (Value::user_iterator ui = I->user_begin(), ue = I->user_end(); - ui != ue; ++ui) { - if (!isa(*ui) && !isa(*ui)) { - if(!ui->use_empty()) + if (!F.isDeclaration() && !F.mayBeOverridden()) { + for (User *U : F.users()) { + if (!isa(U) && !isa(U)) { + if(!U->use_empty()) // // If this function is used for anything other than a direct function // call, then we want to clone it. @@ -87,8 +86,8 @@ IndClone::runOnModule(Module& M) { // function. That would make the function usable in an indirect // function call. // - for (unsigned index = 1; index < ui->getNumOperands(); ++index) { - if (ui->getOperand(index)->stripPointerCasts() == I) { + for (unsigned index = 1; index < U->getNumOperands(); ++index) { + if (U->getOperand(index)->stripPointerCasts() == &F) { pleaseCloneTheFunction = true; break; } @@ -100,7 +99,7 @@ IndClone::runOnModule(Module& M) { // call site, schedule it for cloning. // if (pleaseCloneTheFunction) { - toClone.push_back(I); + toClone.push_back(&F); break; } } diff --git a/lib/AssistDS/LoadArgs.cpp b/lib/AssistDS/LoadArgs.cpp index 595b82b02..8e055766f 100644 --- a/lib/AssistDS/LoadArgs.cpp +++ b/lib/AssistDS/LoadArgs.cpp @@ -144,17 +144,17 @@ bool LoadArgs::runOnModule(Module& M) { &M); fnCache[std::make_pair(F, NewFTy)] = NewF; - Function::arg_iterator NI = NewF->arg_begin(); + auto NI = NewF->arg_begin(); ValueToValueMapTy ValueMap; unsigned count = 0; - for (Function::arg_iterator II = F->arg_begin(); NI != NewF->arg_end(); ++count, ++NI) { + for (auto II = F->arg_begin(); NI != NewF->arg_end(); ++count, ++NI) { if(count == argNum) { NI->setName("LDarg"); continue; } - ValueMap[II] = NI; + ValueMap[&*II] = &*NI; NI->setName(II->getName()); NI->addAttr(F->getAttributes().getParamAttributes(II->getArgNo() + 1)); ++II; @@ -163,9 +163,8 @@ bool LoadArgs::runOnModule(Module& M) { SmallVector Returns; CloneFunctionInto(NewF, F, ValueMap, false, Returns); std::vector fargs; - for(Function::arg_iterator ai = NewF->arg_begin(), - ae= NewF->arg_end(); ai != ae; ++ai) { - fargs.push_back(ai); + for (auto &Arg : NewF->args()) { + fargs.push_back(&Arg); } NewF->setAttributes(NewF->getAttributes().addAttributes( @@ -174,7 +173,7 @@ bool LoadArgs::runOnModule(Module& M) { F->getContext(), ~0, F->getAttributes().getFnAttributes())); //Get the point to insert the GEP instr. Instruction *InsertPoint; - for (BasicBlock::iterator insrt = NewF->front().begin(); isa(InsertPoint = insrt); ++insrt) {;} + for (auto insrt = NewF->front().begin(); isa(InsertPoint = &*insrt); ++insrt) {;} LoadInst *LI_new = new LoadInst(fargs.at(argNum), "", InsertPoint); fargs.at(argNum+1)->replaceAllUsesWith(LI_new); } diff --git a/lib/AssistDS/StructReturnToPointer.cpp b/lib/AssistDS/StructReturnToPointer.cpp index c7853d9a1..288efec51 100644 --- a/lib/AssistDS/StructReturnToPointer.cpp +++ b/lib/AssistDS/StructReturnToPointer.cpp @@ -51,14 +51,14 @@ bool StructRet::runOnModule(Module& M) { const llvm::DataLayout targetData(&M); std::vector worklist; - for (Module::iterator I = M.begin(); I != M.end(); ++I) - if (!I->mayBeOverridden()) { - if(I->isDeclaration()) + for (Function &F : M) + if (!F.mayBeOverridden()) { + if(F.isDeclaration()) continue; - if(I->hasAddressTaken()) + if(F.hasAddressTaken()) continue; - if(I->getReturnType()->isStructTy()) { - worklist.push_back(I); + if(F.getReturnType()->isStructTy()) { + worklist.push_back(&F); } } @@ -82,11 +82,11 @@ bool StructRet::runOnModule(Module& M) { F->getLinkage(), F->getName(), &M); ValueToValueMapTy ValueMap; - Function::arg_iterator NI = NF->arg_begin(); + auto NI = NF->arg_begin(); NI->setName("ret"); ++NI; - for (Function::arg_iterator II = F->arg_begin(); II != F->arg_end(); ++II, ++NI) { - ValueMap[II] = NI; + for (auto II = F->arg_begin(); II != F->arg_end(); ++II, ++NI) { + ValueMap[&*II] = &*NI; NI->setName(II->getName()); AttributeSet attrs = F->getAttributes().getParamAttributes(II->getArgNo() + 1); if (!attrs.isEmpty()) @@ -97,9 +97,8 @@ bool StructRet::runOnModule(Module& M) { if (!F->isDeclaration()) CloneFunctionInto(NF, F, ValueMap, false, Returns); std::vector fargs; - for(Function::arg_iterator ai = NF->arg_begin(), - ae= NF->arg_end(); ai != ae; ++ai) { - fargs.push_back(ai); + for (auto &Arg : NF->args()) { + fargs.push_back(&Arg); } NF->setAttributes(NF->getAttributes().addAttributes( M.getContext(), 0, F->getAttributes().getRetAttributes())); diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index 2347e742c..578cabed9 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -578,7 +578,7 @@ void TypeChecks::optimizeChecks(Module &M) { if(hoist) { CI->removeFromParent(); - L->getLoopPreheader()->getInstList().insert(L->getLoopPreheader()->getTerminator(), CI); + L->getLoopPreheader()->getInstList().insert(L->getLoopPreheader()->getTerminator()->getIterator(), CI); } } } @@ -667,17 +667,16 @@ bool TypeChecks::visitAddressTakenFunction(Module &M, Function &F) { &M); // 3. Set the mapping for the args - Function::arg_iterator NI = NewF->arg_begin(); + auto NI = NewF->arg_begin(); ValueToValueMapTy ValueMap; NI->setName("TotalCount"); NI++; NI->setName("MD"); NI++; - for(Function::arg_iterator II = F.arg_begin(); - NI!=NewF->arg_end(); ++II, ++NI) { + for(auto II = F.arg_begin(); NI!=NewF->arg_end(); ++II, ++NI) { // Each new argument maps to the argument in the old function // For each of these also copy attributes - ValueMap[II] = NI; + ValueMap[&*II] = &*NI; NI->setName(II->getName()); NI->addAttr(F.getAttributes().getParamAttributes(II->getArgNo()+1)); } @@ -833,17 +832,16 @@ bool TypeChecks::visitInternalVarArgFunction(Module &M, Function &F) { &M); // 3. Set the mapping for the args - Function::arg_iterator NI = NewF->arg_begin(); + auto NI = NewF->arg_begin(); ValueToValueMapTy ValueMap; NI->setName("TotalArgCount"); NI++; NI->setName("MD"); NI++; - for(Function::arg_iterator II = F.arg_begin(); - NI!=NewF->arg_end(); ++II, ++NI) { + for(auto II = F.arg_begin(); NI!=NewF->arg_end(); ++II, ++NI) { // Each new argument maps to the argument in the old function // For each of these also copy attributes - ValueMap[II] = NI; + ValueMap[&*II] = &*NI; NI->setName(II->getName()); NI->addAttr(F.getAttributes().getParamAttributes(II->getArgNo()+1)); } @@ -862,11 +860,11 @@ bool TypeChecks::visitInternalVarArgFunction(Module &M, Function &F) { // Store the information inst_iterator InsPt = inst_begin(NewF); - Function::arg_iterator NII = NewF->arg_begin(); + auto NII = NewF->arg_begin(); // Subtract the number of initial arguments Constant *InitialArgs = ConstantInt::get(Int64Ty, F.arg_size()); Instruction *NewValue = BinaryOperator::Create(BinaryOperator::Sub, - NII, + &*NII, InitialArgs, "varargs", &*InsPt); @@ -877,7 +875,7 @@ bool TypeChecks::visitInternalVarArgFunction(Module &M, Function &F) { Value *Idx[1]; Idx[0] = InitialArgs; // For each vararg argument, also add its type information - GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(NII,Idx, "", &*InsPt); + GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(&*NII,Idx, "", &*InsPt); // visit all VAStarts and initialize the counter for (Function::iterator B = NewF->begin(), FE = NewF->end(); B != FE; ++B) { for (BasicBlock::iterator I = B->begin(), BE = B->end(); I != BE;I++) { @@ -1037,15 +1035,15 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { // for every byval argument // add an alloca, a load, and a store inst Instruction * InsertBefore = &(F.getEntryBlock().front()); - for (Function::arg_iterator I = F.arg_begin(); I != F.arg_end(); ++I) { - if (!I->hasByValAttr()) + for (auto &Arg : F.args()) { + if (!Arg.hasByValAttr()) continue; - assert(I->getType()->isPointerTy()); - Type *ETy = (cast(I->getType()))->getElementType(); + assert(Arg.getType()->isPointerTy()); + Type *ETy = (cast(Arg.getType()))->getElementType(); AllocaInst *AI = new AllocaInst(ETy, "", InsertBefore); // Do this before adding the load/store pair, so that those uses are not replaced. - I->replaceAllUsesWith(AI); - LoadInst *LI = new LoadInst(I, "", InsertBefore); + Arg.replaceAllUsesWith(AI); + LoadInst *LI = new LoadInst(&Arg, "", InsertBefore); new StoreInst(LI, AI, InsertBefore); } @@ -1169,21 +1167,21 @@ bool TypeChecks::visitExternalByValFunction(Module &M, Function &F) { // A list of the byval arguments that we are setting metadata for typedef SmallVector RegisteredArgTy; RegisteredArgTy registeredArguments; - for (Function::arg_iterator I = F.arg_begin(); I != F.arg_end(); ++I) { - if (I->hasByValAttr()) { - assert (isa(I->getType())); - PointerType * PT = cast(I->getType()); + for (auto &Arg : F.args()) { + if (Arg.hasByValAttr()) { + assert (isa(Arg.getType())); + PointerType * PT = cast(Arg.getType()); Type * ET = PT->getElementType(); Value * AllocSize = ConstantInt::get(Int64Ty, TD->getTypeAllocSize(ET)); Instruction * InsertPt = &(F.getEntryBlock().front()); - Value *BCI = castTo(I, VoidPtrTy, "", InsertPt); + Value *BCI = castTo(&Arg, VoidPtrTy, "", InsertPt); std::vector Args; Args.push_back(BCI); Args.push_back(AllocSize); Args.push_back(getTagCounter()); // Set the metadata for the byval argument to TOP/Initialized CallInst::Create(trackInitInst, Args, "", InsertPt); - registeredArguments.push_back(&*I); + registeredArguments.push_back(&Arg); } } @@ -1252,29 +1250,28 @@ bool TypeChecks::initShadow(Module &M) { Instruction *InsertPt = ReturnInst::Create(M.getContext(), BB); // record all globals - for (Module::global_iterator I = M.global_begin(), E = M.global_end(); - I != E; ++I) { - if(I->use_empty()) + for (GlobalVariable &G : M.globals()) { + if(G.use_empty()) continue; - if(I->getName().str() == "stderr" || - I->getName().str() == "stdout" || - I->getName().str() == "stdin" || - I->getName().str() == "optind" || - I->getName().str() == "optarg") { + if(G.getName().str() == "stderr" || + G.getName().str() == "stdout" || + G.getName().str() == "stdin" || + G.getName().str() == "optind" || + G.getName().str() == "optarg") { // assume initialized - Value *BCI = castTo(I, VoidPtrTy, "", InsertPt); + Value *BCI = castTo(&G, VoidPtrTy, "", InsertPt); std::vector Args; Args.push_back(BCI); - Args.push_back(getSizeConstant(I->getType()->getElementType())); + Args.push_back(getSizeConstant(G.getType()->getElementType())); Args.push_back(getTagCounter()); CallInst::Create(trackInitInst, Args, "", InsertPt); continue; } - if(!I->hasInitializer()) + if(!G.hasInitializer()) continue; SmallVectorindex; index.push_back(Zero); - visitGlobal(M, *I, I->getInitializer(), *InsertPt, index); + visitGlobal(M, G, G.getInitializer(), *InsertPt, index); } // // Insert the run-time ctor into the ctor list. @@ -1341,11 +1338,11 @@ bool TypeChecks::initShadow(Module &M) { // No need to register return false; - Function::arg_iterator AI = MainFunc.arg_begin(); - Value *Argc = AI; - Value *Argv = ++AI; + auto AI = MainFunc.arg_begin(); + Value *Argc = &*AI; + Value *Argv = &*(++AI); - Instruction *InsertPt = MainFunc.front().begin(); + Instruction *InsertPt = &*MainFunc.front().begin(); std::vector fargs; fargs.push_back (Argc); fargs.push_back (Argv); @@ -1354,7 +1351,7 @@ bool TypeChecks::initShadow(Module &M) { if(MainFunc.arg_size() < 3) return true; - Value *Envp = ++AI; + Value *Envp = &*(++AI); std::vector Args; Args.push_back(Envp); CallInst::Create(RegisterEnvp, Args, "", InsertPt); @@ -1550,7 +1547,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { CallInst *CI = CallInst::Create(F, Args); Instruction *InsertPt = I; if (InvokeInst *II = dyn_cast(InsertPt)) { - InsertPt = II->getNormalDest()->begin(); + InsertPt = &*II->getNormalDest()->begin(); while (isa(InsertPt)) ++InsertPt; } else @@ -1565,7 +1562,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { CallInst *CI = CallInst::Create(F, Args); Instruction *InsertPt = I; if (InvokeInst *II = dyn_cast(InsertPt)) { - InsertPt = II->getNormalDest()->begin(); + InsertPt = &*II->getNormalDest()->begin(); while (isa(InsertPt)) ++InsertPt; } else diff --git a/lib/DSA/AddressTakenAnalysis.cpp b/lib/DSA/AddressTakenAnalysis.cpp index f106f20cc..067322cd6 100644 --- a/lib/DSA/AddressTakenAnalysis.cpp +++ b/lib/DSA/AddressTakenAnalysis.cpp @@ -68,14 +68,15 @@ static bool isAddressTaken(Value* V) { } bool AddressTakenAnalysis::runOnModule(llvm::Module& M) { - for (Module::iterator FI = M.begin(), FE = M.end(); FI != FE; ++FI){ - if(isAddressTaken(FI)) { - addressTakenFunctions.insert(FI); + for (Function &F : M) { + if(isAddressTaken(&F)) { + addressTakenFunctions.insert(&F); } } return false; } + bool AddressTakenAnalysis::hasAddressTaken(llvm::Function *F){ return addressTakenFunctions.find(F) != addressTakenFunctions.end(); } diff --git a/lib/DSA/Basic.cpp b/lib/DSA/Basic.cpp index c5e9df5ff..46b429626 100644 --- a/lib/DSA/Basic.cpp +++ b/lib/DSA/Basic.cpp @@ -60,30 +60,29 @@ bool BasicDataStructures::runOnModule(Module &M) { // together the globals into equivalence classes. formGlobalECs(); - for (Module::iterator F = M.begin(), E = M.end(); F != E; ++F) { - if (!F->isDeclaration()) { + for (Function &F : M) { + if (!F.isDeclaration()) { DSGraph* G = new DSGraph(GlobalECs, getDataLayout(), *TypeSS, GlobalsGraph); DSNode * Node = new DSNode(G); - if (!F->hasInternalLinkage()) + if (!F.hasInternalLinkage()) Node->setExternalMarker(); // Create scalar nodes for all pointer arguments... - for (Function::arg_iterator I = F->arg_begin(), E = F->arg_end(); - I != E; ++I) { - if (isa(I->getType())) { - G->getNodeForValue(&*I).mergeWith(Node); + for (auto &Arg : F.args()) { + if (isa(Arg.getType())) { + G->getNodeForValue(&Arg).mergeWith(Node); } } - for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) { + for (inst_iterator I = inst_begin(&F), E = inst_end(&F); I != E; ++I) { G->getNodeForValue(&*I).mergeWith(Node); } Node->foldNodeCompletely(); Node->maskNodeTypes(DSNode::IncompleteNode); - setDSGraph(*F, G); + setDSGraph(F, G); } } diff --git a/lib/DSA/BottomUpClosure.cpp b/lib/DSA/BottomUpClosure.cpp index 2ebe53a55..f49de1d8e 100644 --- a/lib/DSA/BottomUpClosure.cpp +++ b/lib/DSA/BottomUpClosure.cpp @@ -63,9 +63,9 @@ bool BUDataStructures::runOnModuleInternal(Module& M) { // While we may not need them in this DSA pass, a later DSA pass may ask us // for their DSGraphs, and we want to have them if asked. // - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())){ - getOrCreateGraph(F); + for (Function &F : M) { + if (!(F.isDeclaration())){ + getOrCreateGraph(&F); } } @@ -99,9 +99,9 @@ bool BUDataStructures::runOnModuleInternal(Module& M) { // into the individual function's graph so that changes made to globals during // BU can be reflected. This is specifically needed for correct call graph // - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())){ - DSGraph *Graph = getOrCreateGraph(F); + for (Function &F : M) { + if (!(F.isDeclaration())){ + DSGraph *Graph = getOrCreateGraph(&F); cloneGlobalsInto(Graph, DSGraph::DontCloneCallNodes | DSGraph::DontCloneAuxCallNodes); Graph->buildCallGraph(callgraph, GlobalFunctionList, filterCallees); @@ -114,9 +114,9 @@ bool BUDataStructures::runOnModuleInternal(Module& M) { } // Once the correct flags have been calculated. Update the callgraph. - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())){ - DSGraph *Graph = getOrCreateGraph(F); + for (Function &F : M) { + if (!(F.isDeclaration())){ + DSGraph *Graph = getOrCreateGraph(&F); Graph->buildCompleteCallGraph(callgraph, GlobalFunctionList, filterCallees); } @@ -307,19 +307,19 @@ BUDataStructures::postOrderInline (Module & M) { // // Calculate the graphs for any functions that are unreachable from main... // - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration() && !ValMap.count(I)) { + for (Function &F : M) + if (!F.isDeclaration() && !ValMap.count(&F)) { if (MainFunc) DEBUG(errs() << debugname << ": Function unreachable from main: " - << I->getName() << "\n"); - calculateGraphs(I, Stack, NextID, ValMap); // Calculate all graphs. - CloneAuxIntoGlobal(getDSGraph(*I)); + << F.getName() << "\n"); + calculateGraphs(&F, Stack, NextID, ValMap); // Calculate all graphs. + CloneAuxIntoGlobal(getDSGraph(F)); // Mark this graph as processed. Do this by finding all functions // in the graph that map to it, and mark them visited. // Note that this really should be handled neatly by calculateGraphs // itself, not here. However this catches the worst offenders. - DSGraph *G = getDSGraph(*I); + DSGraph *G = getDSGraph(F); for(DSGraph::retnodes_iterator RI = G->retnodes_begin(), RE = G->retnodes_end(); RI != RE; ++RI) { if (getDSGraph(*RI->first) == G) { diff --git a/lib/DSA/CallTargets.cpp b/lib/DSA/CallTargets.cpp index 0814a43f8..2ae6629ad 100644 --- a/lib/DSA/CallTargets.cpp +++ b/lib/DSA/CallTargets.cpp @@ -51,12 +51,12 @@ void CallTargetFinder::findIndTargets(Module &M) const DSCallGraph & callgraph = T->getCallGraph(); DSGraph* G = T->getGlobalsGraph(); DSGraph::ScalarMapTy& SM = G->getScalarMap(); - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration()) - for (Function::iterator F = I->begin(), FE = I->end(); F != FE; ++F) - for (BasicBlock::iterator B = F->begin(), BE = F->end(); B != BE; ++B) - if (isa(B) || isa(B)) { - CallSite cs(B); + for (Function &F : M) + if (!F.isDeclaration()) + for (BasicBlock &B : F) + for (Instruction &I : B) + if (isa(&I) || isa(&I)) { + CallSite cs(&I); AllSites.push_back(cs); Function* CF = cs.getCalledFunction(); diff --git a/lib/DSA/CompleteBottomUp.cpp b/lib/DSA/CompleteBottomUp.cpp index df05215d6..e8c8b30b3 100644 --- a/lib/DSA/CompleteBottomUp.cpp +++ b/lib/DSA/CompleteBottomUp.cpp @@ -50,17 +50,17 @@ CompleteBUDataStructures::runOnModule (Module &M) { // formGlobalECs assumes that DSInfo is populated with a list of // DSgraphs for all the functions. - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())){ - getOrCreateGraph(F); + for (Function &F : M) { + if (!(F.isDeclaration())){ + getOrCreateGraph(&F); } } buildIndirectFunctionSets(); formGlobalECs(); - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())) { - if (DSGraph * Graph = getOrCreateGraph(F)) { + for (Function &F : M) { + if (!(F.isDeclaration())) { + if (DSGraph * Graph = getOrCreateGraph(&F)) { cloneIntoGlobals(Graph, DSGraph::DontCloneCallNodes | DSGraph::DontCloneAuxCallNodes | DSGraph::StripAllocaBit); @@ -68,9 +68,9 @@ CompleteBUDataStructures::runOnModule (Module &M) { } } - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())) { - if (DSGraph * Graph = getOrCreateGraph(F)) { + for (Function &F : M) { + if (!(F.isDeclaration())) { + if (DSGraph * Graph = getOrCreateGraph(&F)) { cloneGlobalsInto(Graph, DSGraph::DontCloneCallNodes | DSGraph::DontCloneAuxCallNodes); } diff --git a/lib/DSA/DSGraph.cpp b/lib/DSA/DSGraph.cpp index 97b6a3300..07eee4806 100644 --- a/lib/DSA/DSGraph.cpp +++ b/lib/DSA/DSGraph.cpp @@ -201,7 +201,7 @@ void DSGraph::cloneInto( DSGraph* G, unsigned CloneFlags) { "Forward nodes shouldn't be in node list!"); DSNode *New = new DSNode(*I, this); New->maskNodeTypes(~BitsToClear); - OldNodeMap[I] = New; + OldNodeMap[&*I] = New; } // Rewrite the links in the new nodes to point into the current graph now. @@ -296,10 +296,9 @@ void DSGraph::getFunctionArgumentsForCall(const Function *F, std::vector &Args) const { Args.push_back(getReturnNodeFor(*F)); Args.push_back(getVANodeFor(*F)); - for (Function::const_arg_iterator AI = F->arg_begin(), E = F->arg_end(); - AI != E; ++AI) - if (isa(AI->getType())) { - Args.push_back(getNodeForValue(AI)); + for (const auto &Arg : F->args()) + if (isa(Arg.getType())) { + Args.push_back(getNodeForValue(&Arg)); assert(!Args.back().isNull() && "Pointer argument w/o scalarmap entry!?"); } } @@ -528,9 +527,9 @@ void DSGraph::mergeInGraph(const DSCallSite &CS, const Function &F, DSCallSite DSGraph::getCallSiteForArguments(const Function &F) const { std::vector Args; - for (Function::const_arg_iterator I = F.arg_begin(), E = F.arg_end(); I != E; ++I) - if (isa(I->getType())) - Args.push_back(getNodeForValue(I)); + for (const auto &Arg : F.args()) + if (isa(Arg.getType())) + Args.push_back(getNodeForValue(&Arg)); return DSCallSite(CallSite(), getReturnNodeFor(F), getVANodeFor(F), &F, Args); } @@ -630,10 +629,9 @@ void DSGraph::markIncompleteNodes(unsigned Flags) { for (ReturnNodesTy::iterator FI = ReturnNodes.begin(), E =ReturnNodes.end(); FI != E; ++FI) { const Function &F = *FI->first; - for (Function::const_arg_iterator I = F.arg_begin(), E = F.arg_end(); - I != E; ++I) - if (isa(I->getType())) - markIncompleteNode(getNodeForValue(I).getNode()); + for (const auto &Arg : F.args()) + if (isa(Arg.getType())) + markIncompleteNode(getNodeForValue(&Arg).getNode()); markIncompleteNode(FI->second.getNode()); } // Mark all vanodes as incomplete (they are also arguments) @@ -666,7 +664,7 @@ void DSGraph::markIncompleteNodes(unsigned Flags) { if (Flags & DSGraph::MarkVAStart) { for (node_iterator i=node_begin(); i != node_end(); ++i) { if (i->isVAStartNode()) - markIncompleteNode(i); + markIncompleteNode(&*i); } } } @@ -757,14 +755,13 @@ void DSGraph::computeExternalFlags(unsigned Flags) { FI != E; ++FI) { const Function &F = *FI->first; // Mark its arguments, return value (and vanode) as external. - for (Function::const_arg_iterator I = F.arg_begin(), E = F.arg_end(); - I != E; ++I){ + for (const auto &Arg : F.args()) { if(TypeInferenceOptimize) { - if(I->getName().str() == "argv") + if(Arg.getName().str() == "argv") continue; } - if (isa(I->getType())) - markExternalNode(getNodeForValue(I).getNode(), processedNodes); + if (isa(Arg.getType())) + markExternalNode(getNodeForValue(&Arg).getNode(), processedNodes); } markExternalNode(FI->second.getNode(), processedNodes); markExternalNode(getVANodeFor(F).getNode(), processedNodes); @@ -1170,7 +1167,8 @@ void DSGraph::removeDeadNodes(unsigned Flags) { std::vector DeadNodes; DeadNodes.reserve(Nodes.size()); for (NodeListTy::iterator NI = Nodes.begin(), E = Nodes.end(); NI != E;) { - DSNode *N = NI++; + DSNode *N = &*NI; + ++NI; assert(!N->isForwarding() && "Forwarded node in nodes list?"); if (!Alive.count(N)) { @@ -1250,9 +1248,9 @@ void DSGraph::AssertGraphOK() const { E = ReturnNodes.end(); RI != E; ++RI) { const Function &F = *RI->first; - for (Function::const_arg_iterator AI = F.arg_begin(); AI != F.arg_end(); ++AI) - if (isa(AI->getType())) - assert(!getNodeForValue(AI).isNull() && + for (const auto &Arg : F.args()) + if (isa(Arg.getType())) + assert(!getNodeForValue(&Arg).isNull() && "Pointer argument must be in the scalar map!"); if (F.isVarArg()) assert(VANodes.find(&F) != VANodes.end() && @@ -1526,7 +1524,7 @@ llvm::functionIsCallable (ImmutableCallSite CS, const Function* F) { // if (!noDSACallConv) { Function::const_arg_iterator farg = F->arg_begin(), fend = F->arg_end(); - for (unsigned index = 1; index < (CS.arg_size() + 1) && farg != fend; + for (unsigned index = 0; index < CS.getNumArgOperands() && farg != fend; ++farg, ++index) { if (CS.isByValArgument(index) != farg->hasByValAttr()) { return false; diff --git a/lib/DSA/EntryPointAnalysis.cpp b/lib/DSA/EntryPointAnalysis.cpp index f070e6999..cf62ef8c5 100644 --- a/lib/DSA/EntryPointAnalysis.cpp +++ b/lib/DSA/EntryPointAnalysis.cpp @@ -53,9 +53,9 @@ EntryPointAnalysis::~EntryPointAnalysis() {} void EntryPointAnalysis::findEntryPoints(const Module& M, std::vector& dest) const { - for (Module::const_iterator ii = M.begin(), ee = M.end(); ii != ee; ++ii) - if (isEntryPoint(ii)) - dest.push_back(ii); + for (const Function &F : M) + if (isEntryPoint(&F)) + dest.push_back(&F); } void EntryPointAnalysis::print(llvm::raw_ostream& O, const Module* M) const { diff --git a/lib/DSA/EquivClassGraphs.cpp b/lib/DSA/EquivClassGraphs.cpp index 949d798f8..bb50742a1 100644 --- a/lib/DSA/EquivClassGraphs.cpp +++ b/lib/DSA/EquivClassGraphs.cpp @@ -44,10 +44,10 @@ bool EquivBUDataStructures::runOnModule(Module &M) { //make a list of all the DSGraphs std::setgraphList; - for(Module::iterator F = M.begin(); F != M.end(); ++F) + for(Function &F : M) { - if(!(F->isDeclaration())) - graphList.insert(getOrCreateGraph(F)); + if(!(F.isDeclaration())) + graphList.insert(getOrCreateGraph(&F)); } //update the EQ class from indirect calls @@ -56,10 +56,10 @@ bool EquivBUDataStructures::runOnModule(Module &M) { mergeGraphsByGlobalECs(); //remove all the DSGraph, that still have references - for(Module::iterator F = M.begin(); F != M.end(); ++F) + for(Function &F : M) { - if(!(F->isDeclaration())) - graphList.erase(getOrCreateGraph(F)); + if(!(F.isDeclaration())) + graphList.erase(getOrCreateGraph(&F)); } // free memory for the DSGraphs, no longer in use. for(std::set::iterator i = graphList.begin(),e = graphList.end(); @@ -70,9 +70,9 @@ bool EquivBUDataStructures::runOnModule(Module &M) { formGlobalECs(); - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())) { - if (DSGraph * Graph = getOrCreateGraph(F)) { + for (Function &F: M) { + if (!(F.isDeclaration())) { + if (DSGraph * Graph = getOrCreateGraph(&F)) { cloneGlobalsInto(Graph, DSGraph::DontCloneCallNodes | DSGraph::DontCloneAuxCallNodes); } diff --git a/lib/DSA/Local.cpp b/lib/DSA/Local.cpp index 51d30ca8d..02d63e478 100644 --- a/lib/DSA/Local.cpp +++ b/lib/DSA/Local.cpp @@ -154,9 +154,8 @@ namespace { << f.getName() << "\n"); // Create scalar nodes for all pointer arguments... - for (Function::arg_iterator I = f.arg_begin(), E = f.arg_end(); - I != E; ++I) { - if (isa(I->getType())) { + for (auto &Arg : f.args()) { + if (isa(Arg.getType())) { // WD: Why do we set the external marker so early in the analysis? // Functions we have definitions for, but are externally reachable have no external contexts // that we'd want to BU external information into (since those contexts are by definition @@ -167,7 +166,7 @@ namespace { if (!f.hasInternalLinkage() || !f.hasPrivateLinkage()) Node->setExternalMarker(); #else - getValueDest(I).getNode(); + getValueDest(&Arg).getNode(); #endif } @@ -1475,14 +1474,12 @@ void handleMagicSections(DSGraph* GlobalsGraph, Module& M) { std::string section; msf >> section; svset inSection; - for (Module::iterator MI = M.begin(), ME = M.end(); - MI != ME; ++MI) - if (MI->hasSection() && MI->getSection() == section) - inSection.insert(MI); - for (Module::global_iterator MI = M.global_begin(), ME = M.global_end(); - MI != ME; ++MI) - if (MI->hasSection() && MI->getSection() == section) - inSection.insert(MI); + for (Function &F : M) + if (F.hasSection() && F.getSection() == section) + inSection.insert(&F); + for (GlobalVariable &GV : M.globals()) + if (GV.hasSection() && GV.getSection() == section) + inSection.insert(&GV); for (unsigned x = 0; x < count; ++x) { std::string global; @@ -1517,18 +1514,17 @@ bool LocalDataStructures::runOnModule(Module &M) { GraphBuilder GGB(*GlobalsGraph, *this); // Add initializers for all of the globals to the globals graph. - for (Module::global_iterator I = M.global_begin(), E = M.global_end(); - I != E; ++I) - if (!(I->hasSection() && std::string(I->getSection()) == "llvm.metadata")) { - if (I->isDeclaration()) - GGB.mergeExternalGlobal(I); + for (GlobalVariable &GV : M.globals()) + if (!(GV.hasSection() && std::string(GV.getSection()) == "llvm.metadata")) { + if (GV.isDeclaration()) + GGB.mergeExternalGlobal(&GV); else - GGB.mergeInGlobalInitializer(I); + GGB.mergeInGlobalInitializer(&GV); } // Add Functions to the globals graph. - for (Module::iterator FI = M.begin(), FE = M.end(); FI != FE; ++FI){ - if(addrAnalysis->hasAddressTaken(FI)) { - GGB.mergeFunction(FI); + for (Function &F : M) { + if(addrAnalysis->hasAddressTaken(&F)) { + GGB.mergeFunction(&F); } } } @@ -1547,14 +1543,14 @@ bool LocalDataStructures::runOnModule(Module &M) { GlobalsGraph->maskIncompleteMarkers(); // Calculate all of the graphs... - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration()) { + for (Function &F : M) + if (!F.isDeclaration()) { DSGraph* G = new DSGraph(GlobalECs, getDataLayout(), *TypeSS, GlobalsGraph); - setDSGraph(*I, G); - GraphBuilder GGB(*I, *G, *this); + setDSGraph(F, G); + GraphBuilder GGB(F, *G, *this); G->getAuxFunctionCalls() = G->getFunctionCalls(); propagateUnknownFlag(G); - callgraph.insureEntry(I); + callgraph.insureEntry(&F); G->buildCallGraph(callgraph, GlobalFunctionList, true); G->maskIncompleteMarkers(); G->markIncompleteNodes(DSGraph::MarkFormalArgs @@ -1578,9 +1574,9 @@ bool LocalDataStructures::runOnModule(Module &M) { formGlobalECs(); propagateUnknownFlag(GlobalsGraph); - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration()) { - DSGraph *Graph = getOrCreateGraph(I); + for (Function &F : M) + if (!F.isDeclaration()) { + DSGraph *Graph = getOrCreateGraph(&F); Graph->maskIncompleteMarkers(); cloneGlobalsInto(Graph, DSGraph::DontCloneCallNodes | DSGraph::DontCloneAuxCallNodes); diff --git a/lib/DSA/StdLibPass.cpp b/lib/DSA/StdLibPass.cpp index a902b779a..2cb29ebb4 100644 --- a/lib/DSA/StdLibPass.cpp +++ b/lib/DSA/StdLibPass.cpp @@ -563,28 +563,26 @@ StdLibDataStructures::runOnModule (Module &M) { // Erase direct calls to functions that don't return a pointer and are marked // with the readnone annotation. // - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (I->isDeclaration() && I->doesNotAccessMemory() && - !isa(I->getReturnType())) - eraseCallsTo(I); + for (Function &F : M) + if (F.isDeclaration() && F.doesNotAccessMemory() && + !isa(F.getReturnType())) + eraseCallsTo(&F); // // Erase direct calls to external functions that are not varargs, do not // return a pointer, and do not take pointers. // - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (I->isDeclaration() && !I->isVarArg() && - !isa(I->getReturnType())) { + for (Function &F : M) + if (F.isDeclaration() && !F.isVarArg() && + !isa(F.getReturnType())) { bool hasPtr = false; - for (Function::arg_iterator ii = I->arg_begin(), ee = I->arg_end(); - ii != ee; - ++ii) - if (isa(ii->getType())) { + for (auto &Arg : F.args()) + if (isa(Arg.getType())) { hasPtr = true; break; } if (!hasPtr) - eraseCallsTo(I); + eraseCallsTo(&F); } if(!DisableStdLib) { @@ -663,9 +661,9 @@ StdLibDataStructures::runOnModule (Module &M) { |DSGraph::IgnoreGlobals); GlobalsGraph->computeExternalFlags(DSGraph::ProcessCallSites); DEBUG(GlobalsGraph->AssertGraphOK()); - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration()) { - DSGraph *Graph = getOrCreateGraph(I); + for (Function &F : M) + if (!F.isDeclaration()) { + DSGraph *Graph = getOrCreateGraph(&F); Graph->maskIncompleteMarkers(); cloneGlobalsInto(Graph, DSGraph::DontCloneCallNodes | DSGraph::DontCloneAuxCallNodes); diff --git a/lib/DSA/TopDownClosure.cpp b/lib/DSA/TopDownClosure.cpp index cbd8aa1a6..b370720de 100644 --- a/lib/DSA/TopDownClosure.cpp +++ b/lib/DSA/TopDownClosure.cpp @@ -105,9 +105,9 @@ bool TDDataStructures::runOnModule(Module &M) { GlobalsGraph->getAuxFunctionCalls().clear(); // Functions without internal linkage are definitely externally callable! - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration() && !I->hasInternalLinkage() && !I->hasPrivateLinkage()) - ExternallyCallable.insert(I); + for (Function &F : M) + if (!F.isDeclaration() && !F.hasInternalLinkage() && !F.hasPrivateLinkage()) + ExternallyCallable.insert(&F); // Debug code to print the functions that are externally callable #if 0 @@ -129,9 +129,9 @@ bool TDDataStructures::runOnModule(Module &M) { ComputePostOrder(*F, VisitedGraph, PostOrder); // Next calculate the graphs for each unreachable function... - for (Module::iterator I = M.begin(), E = M.end(); I != E; ++I) - if (!I->isDeclaration()) - ComputePostOrder(*I, VisitedGraph, PostOrder); + for (Function &F : M) + if (!F.isDeclaration()) + ComputePostOrder(F, VisitedGraph, PostOrder); VisitedGraph.clear(); // Release memory! } @@ -161,9 +161,9 @@ bool TDDataStructures::runOnModule(Module &M) { // Make sure each graph has updated external information about globals // in the globals graph. VisitedGraph.clear(); - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - if (!(F->isDeclaration())){ - DSGraph *Graph = getOrCreateGraph(F); + for (Function &F : M) { + if (!(F.isDeclaration())){ + DSGraph *Graph = getOrCreateGraph(&F); if (!VisitedGraph.insert(Graph).second) continue; cloneGlobalsInto(Graph, DSGraph::DontCloneCallNodes | diff --git a/lib/DSA/TypeSafety.cpp b/lib/DSA/TypeSafety.cpp index 065eac38a..33d9a9f56 100644 --- a/lib/DSA/TypeSafety.cpp +++ b/lib/DSA/TypeSafety.cpp @@ -522,10 +522,10 @@ TypeSafety::findTypeSafeDSNodes (const DSGraph * Graph) { DSGraph::node_const_iterator N = Graph->node_begin(); DSGraph::node_const_iterator NE = Graph->node_end(); for (; N != NE; ++N) { - if (isTypeSafe (N)) { + if (isTypeSafe (&*N)) { TypeSafeNodes.insert (&*N); } - fieldMapUpdate(N); + fieldMapUpdate(&*N); } } diff --git a/lib/smack/CodifyStaticInits.cpp b/lib/smack/CodifyStaticInits.cpp index 685474654..6d7a35750 100644 --- a/lib/smack/CodifyStaticInits.cpp +++ b/lib/smack/CodifyStaticInits.cpp @@ -4,9 +4,10 @@ #define DEBUG_TYPE "codify-static-inits" +#include "smack/CodifyStaticInits.h" +#include "smack/DSAWrapper.h" #include "smack/Naming.h" #include "smack/SmackOptions.h" -#include "smack/CodifyStaticInits.h" #include "llvm/IR/IRBuilder.h" #include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" @@ -60,7 +61,7 @@ namespace{ bool CodifyStaticInits::runOnModule(Module& M) { TD = &M.getDataLayout(); LLVMContext& C = M.getContext(); - DSAAliasAnalysis* DSA = &getAnalysis(); + DSAWrapper* DSA = &getAnalysis(); Function* F = dyn_cast( M.getOrInsertFunction(Naming::STATIC_INIT_PROC, @@ -131,7 +132,7 @@ bool CodifyStaticInits::runOnModule(Module& M) { void CodifyStaticInits::getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.setPreservesAll(); - AU.addRequired(); + AU.addRequired(); } // Pass ID variable diff --git a/lib/smack/DSAAliasAnalysis.cpp b/lib/smack/DSAWrapper.cpp similarity index 53% rename from lib/smack/DSAAliasAnalysis.cpp rename to lib/smack/DSAWrapper.cpp index 9c8d90e34..3b93e63a6 100644 --- a/lib/smack/DSAAliasAnalysis.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -1,37 +1,23 @@ -//===- DataStructureAA.cpp - Data Structure Based Alias Analysis ----------===// // // The LLVM Compiler Infrastructure // // This file was developed by the LLVM research group and is distributed under -// the University of Illinois Open Source License. See LICENSE.TXT for details. +// the University of Illinois Open Source License. See LICENSE for details. // -//===----------------------------------------------------------------------===// -// -// This pass uses the top-down data structure graphs to implement a simple -// context sensitive alias analysis. -// -//===----------------------------------------------------------------------===// -#include "smack/DSAAliasAnalysis.h" +#include "smack/DSAWrapper.h" #include "llvm/Support/FileSystem.h" -#define DEBUG_TYPE "dsa-aa" + +#define DEBUG_TYPE "dsa-wrapper" namespace smack { using namespace llvm; -RegisterPass A("ds-aa", "Data Structure Graph Based Alias Analysis"); -RegisterAnalysisGroup B(A); -char DSAAliasAnalysis::ID = 0; +char DSAWrapper::ID; +RegisterPass DSAWrapperPass("dsa-wrapper", + "SMACK Data Structure Graph Based Alias Analysis Wrapper"); -void DSAAliasAnalysis::printDSAGraphs(const char* Filename) { - std::error_code EC; - llvm::raw_fd_ostream F(Filename, EC, sys::fs::OpenFlags::F_None); - TD->print(F, module); - BU->print(F, module); - TS->print(F, module); -} - -std::vector DSAAliasAnalysis::collectMemcpys( +std::vector DSAWrapper::collectMemcpys( llvm::Module &M, MemcpyCollector *mcc) { for (llvm::Module::iterator func = M.begin(), e = M.end(); @@ -46,16 +32,11 @@ std::vector DSAAliasAnalysis::collectMemcpys( return mcc->getMemcpys(); } - -std::vector DSAAliasAnalysis::collectStaticInits(llvm::Module &M) { +std::vector DSAWrapper::collectStaticInits(llvm::Module &M) { std::vector sis; - - const llvm::EquivalenceClasses &eqs - = nodeEqs->getEquivalenceClasses(); - for (llvm::Module::const_global_iterator - g = M.global_begin(), e = M.global_end(); g != e; ++g) { - if (g->hasInitializer()) { - if (auto *N = getNode(g)) { + for (GlobalVariable &GV : M.globals()) { + if (GV.hasInitializer()) { + if (auto *N = getNode(&GV)) { sis.push_back(N); } } @@ -63,41 +44,7 @@ std::vector DSAAliasAnalysis::collectStaticInits(llvm::Modu return sis; } -bool DSAAliasAnalysis::isComplicatedNode(const llvm::DSNode* N) { - return - N->isIntToPtrNode() || N->isPtrToIntNode() || - N->isExternalNode() || N->isUnknownNode(); -} - -bool DSAAliasAnalysis::isMemcpyd(const llvm::DSNode* n) { - const llvm::EquivalenceClasses &eqs - = nodeEqs->getEquivalenceClasses(); - const llvm::DSNode* nn = eqs.getLeaderValue(n); - for (unsigned i=0; i &eqs - = nodeEqs->getEquivalenceClasses(); - const llvm::DSNode* nn = eqs.getLeaderValue(n); - for (unsigned i=0; iisFieldDisjoint(V, F); -} - -bool DSAAliasAnalysis::isFieldDisjoint(const GlobalValue* V, unsigned offset) { - return TS->isFieldDisjoint(V, offset); -} - -DSGraph *DSAAliasAnalysis::getGraphForValue(const Value *V) { +DSGraph *DSAWrapper::getGraphForValue(const Value *V) { if (const Instruction *I = dyn_cast(V)) return TD->getDSGraph(*I->getParent()->getParent()); else if (const Argument *A = dyn_cast(V)) @@ -115,51 +62,56 @@ DSGraph *DSAAliasAnalysis::getGraphForValue(const Value *V) { llvm_unreachable("Unexpected value."); } -bool DSAAliasAnalysis::equivNodes(const DSNode* n1, const DSNode* n2) { - const EquivalenceClasses &eqs - = nodeEqs->getEquivalenceClasses(); - - return eqs.getLeaderValue(n1) == eqs.getLeaderValue(n2); -} - -unsigned DSAAliasAnalysis::getOffset(const MemoryLocation* l) { +unsigned DSAWrapper::getOffset(const MemoryLocation* l) { const DSGraph::ScalarMapTy& S = getGraphForValue(l->Ptr)->getScalarMap(); DSGraph::ScalarMapTy::const_iterator I = S.find((const Value*)l->Ptr); return (I == S.end()) ? 0 : (I->second.getOffset()); } -bool DSAAliasAnalysis::disjoint(const MemoryLocation* l1, const MemoryLocation* l2) { - unsigned o1 = getOffset(l1); - unsigned o2 = getOffset(l2); - return - (o1 < o2 && o1 + l1->Size <= o2) - || (o2 < o1 && o2 + l2->Size <= o1); +bool DSAWrapper::isMemcpyd(const llvm::DSNode* n) { + const llvm::EquivalenceClasses &eqs + = nodeEqs->getEquivalenceClasses(); + const llvm::DSNode* nn = eqs.getLeaderValue(n); + for (unsigned i=0; i &eqs = nodeEqs->getEquivalenceClasses(); - auto *N = nodeEqs->getMemberForValue(v); - return N ? eqs.getLeaderValue(N) : nullptr; + const llvm::DSNode* nn = eqs.getLeaderValue(n); + for (unsigned i=0; iisFieldDisjoint(V, F); +} + +bool DSAWrapper::isFieldDisjoint(const GlobalValue* V, unsigned offset) { + return TS->isFieldDisjoint(V, offset); } -bool DSAAliasAnalysis::isRead(const Value* V) { +bool DSAWrapper::isRead(const Value* V) { const DSNode *N = getNode(V); return N && (N->isReadNode()); } -bool DSAAliasAnalysis::isAlloced(const Value* v) { +bool DSAWrapper::isAlloced(const Value* v) { const DSNode *N = getNode(v); return N && (N->isHeapNode() || N->isAllocaNode()); } -bool DSAAliasAnalysis::isExternal(const Value* v) { +bool DSAWrapper::isExternal(const Value* v) { const DSNode *N = getNode(v); return N && N->isExternalNode(); } -bool DSAAliasAnalysis::isSingletonGlobal(const Value *V) { +bool DSAWrapper::isSingletonGlobal(const Value *V) { const DSNode *N = getNode(V); if (!N || !N->isGlobalNode() || N->numGlobals() > 1) return false; @@ -191,7 +143,7 @@ bool DSAAliasAnalysis::isSingletonGlobal(const Value *V) { return true; } -unsigned DSAAliasAnalysis::getPointedTypeSize(const Value* v) { +unsigned DSAWrapper::getPointedTypeSize(const Value* v) { if (llvm::PointerType* t = llvm::dyn_cast(v->getType())) { llvm::Type* pointedType = t->getTypeAtIndex(0u); if (pointedType->isSized()) @@ -202,43 +154,24 @@ unsigned DSAAliasAnalysis::getPointedTypeSize(const Value* v) { llvm_unreachable("Type should be pointer."); } -unsigned DSAAliasAnalysis::getOffset(const Value* v) { +unsigned DSAWrapper::getOffset(const Value* v) { return getOffset(new MemoryLocation(v)); } -AliasResult DSAAliasAnalysis::alias(const MemoryLocation &LocA, const MemoryLocation &LocB) { - - if (LocA.Ptr == LocB.Ptr) - return MustAlias; - - const DSNode *N1 = nodeEqs->getMemberForValue(LocA.Ptr); - const DSNode *N2 = nodeEqs->getMemberForValue(LocB.Ptr); - - assert(N1 && "Expected non-null node."); - assert(N2 && "Expected non-null node."); - - if (N1->isIncompleteNode() && N2->isIncompleteNode()) - goto surrender; - - if (isComplicatedNode(N1) && isComplicatedNode(N2)) - goto surrender; - - if (!equivNodes(N1,N2)) - return NoAlias; - - if (isMemcpyd(N1) || isMemcpyd(N2)) - goto surrender; - - if (isStaticInitd(N1) || isStaticInitd(N2)) - goto surrender; - - if (disjoint(&LocA,&LocB)) - return NoAlias; - - // FIXME: we could improve on this by checking the globals graph for aliased - // global queries... -surrender: - return AliasAnalysis::alias(LocA, LocB); +// TODO: Should this return the node or its leader? +const DSNode *DSAWrapper::getNode(const Value* v) { + const llvm::EquivalenceClasses &eqs + = nodeEqs->getEquivalenceClasses(); + auto *N = nodeEqs->getMemberForValue(v); + return N ? eqs.getLeaderValue(N) : nullptr; } +void DSAWrapper::printDSAGraphs(const char* Filename) { + std::error_code EC; + llvm::raw_fd_ostream F(Filename, EC, sys::fs::OpenFlags::F_None); + TD->print(F, module); + BU->print(F, module); + TS->print(F, module); } + +} // namespace smack diff --git a/lib/smack/ExtractContracts.cpp b/lib/smack/ExtractContracts.cpp index 6fa27373b..60540db6b 100644 --- a/lib/smack/ExtractContracts.cpp +++ b/lib/smack/ExtractContracts.cpp @@ -300,9 +300,8 @@ ExtractContracts::extractExpression(Value* V, BasicBlock* E) { llvm_unreachable("Unexpected store instruction!"); } else if (auto I = dyn_cast(V)) { - auto B = I->getParent(); - assert(clones.count(B) && "Forgot to visit parent block."); - assert(clones[B] != B && "Forgot to clone parent block."); + assert(clones.count(I->getParent()) && "Forgot to visit parent block."); + assert(clones[I->getParent()] != I->getParent() && "Forgot to clone parent block."); auto II = I->clone(); clones[I] = II; diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index a67cc21e1..c8e70eaa1 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -10,7 +10,7 @@ namespace smack { const DataLayout* Region::DL = nullptr; -DSAAliasAnalysis* Region::DSA = nullptr; +DSAWrapper* Region::DSA = nullptr; // DSNodeEquivs* Region::NEQS = nullptr; namespace { @@ -29,7 +29,7 @@ namespace { llvm_unreachable("Unexpected value."); } - bool isFieldDisjoint(DSAAliasAnalysis* DSA, const Value* V, unsigned offset) { + bool isFieldDisjoint(DSAWrapper* DSA, const Value* V, unsigned offset) { if (const GlobalValue* G = dyn_cast(V)) return DSA->isFieldDisjoint(G, offset); else @@ -40,7 +40,7 @@ namespace { void Region::init(Module& M, Pass& P) { DL = &M.getDataLayout(); - DSA = &P.getAnalysis(); + DSA = &P.getAnalysis(); } namespace { @@ -197,7 +197,7 @@ void Regions::getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.addRequiredTransitive(); AU.addRequiredTransitive(); AU.addRequiredTransitive >(); - AU.addRequired(); + AU.addRequired(); } } diff --git a/lib/smack/RemoveDeadDefs.cpp b/lib/smack/RemoveDeadDefs.cpp index 6cd4e1451..fefce508c 100644 --- a/lib/smack/RemoveDeadDefs.cpp +++ b/lib/smack/RemoveDeadDefs.cpp @@ -22,10 +22,10 @@ bool RemoveDeadDefs::runOnModule(Module& M) { do { dead.clear(); - for (Module::iterator F = M.begin(); F != M.end(); ++F) { - std::string name = F->getName(); + for (Function &F : M) { + std::string name = F.getName(); - if (!(F->isDefTriviallyDead() || F->getNumUses() == 0)) + if (!(F.isDefTriviallyDead() || F.getNumUses() == 0)) continue; if (name.find("__SMACK_") != std::string::npos) @@ -35,7 +35,7 @@ bool RemoveDeadDefs::runOnModule(Module& M) { continue; DEBUG(errs() << "removing dead definition: " << name << "\n"); - dead.push_back(F); + dead.push_back(&F); } for (auto F : dead) diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index c854aced4..944f49055 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -42,6 +42,11 @@ std::string i2s(const llvm::Instruction& i) { return s; } +const Stmt* SmackInstGenerator::recordProcedureCall( + llvm::Value* V, std::list attrs) { + return Stmt::call("boogie_si_record_" + rep.type(V), {rep.expr(V)}, {}, attrs); +} + Block* SmackInstGenerator::createBlock() { Block* b = Block::block(naming.freshBlockName()); proc.getBlocks().push_back(b); @@ -93,6 +98,22 @@ void SmackInstGenerator::processInstruction(llvm::Instruction& inst) { void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock& bb) { nextInst = bb.begin(); currBlock = getBlock(&bb); + + auto* F = bb.getParent(); + if (SmackOptions::isEntryPoint(naming.get(*F)) && &bb == &F->getEntryBlock()) { + for (auto& I : bb.getInstList()) { + if (llvm::isa(I)) + continue; + if (I.getDebugLoc()) { + annotate(I, currBlock); + break; + } + } + emit(recordProcedureCall(F, {Attr::attr("cexpr", "smack:entry:" + naming.get(*F))})); + for (auto& A : F->getArgumentList()) { + emit(recordProcedureCall(&A, {Attr::attr("cexpr", "smack:arg:" + naming.get(*F) + ":" + naming.get(A))})); + } + } } void SmackInstGenerator::visitInstruction(llvm::Instruction& inst) { @@ -307,7 +328,7 @@ void SmackInstGenerator::visitInsertValueInst(llvm::InsertValueInst& ivi) { num_elements = at->getNumElements(); t = at->getElementType(); } else { - assert (false && "Unexpected aggregate type"); + llvm_unreachable("Unexpected aggregate type."); } for (unsigned j = 0; j < num_elements; j++) { @@ -495,12 +516,12 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { // emit(Stmt::assign(rep.expr(&ci), Expr::id(rep.getString(ci.getArgOperand(0))))); } else if (name == Naming::CONTRACT_FORALL) { - CallInst* cj; - Function* F; assert(ci.getNumArgOperands() == 2 - && (cj = dyn_cast(ci.getArgOperand(1))) - && (F = cj->getCalledFunction()) - && F->getName().find(Naming::CONTRACT_EXPR) != std::string::npos + && "Expected contract expression argument to contract function."); + CallInst* cj = dyn_cast(ci.getArgOperand(1)); + assert(cj && "Expected contract expression argument to contract function."); + Function* F = cj->getCalledFunction(); + assert(F && F->getName().find(Naming::CONTRACT_EXPR) != std::string::npos && "Expected contract expression argument to contract function."); auto binding = rep.getString(ci.getArgOperand(0)); @@ -525,12 +546,12 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { name == Naming::CONTRACT_ENSURES || name == Naming::CONTRACT_INVARIANT) { - CallInst* cj; - Function* F; assert(ci.getNumArgOperands() == 1 - && (cj = dyn_cast(ci.getArgOperand(0))) - && (F = cj->getCalledFunction()) - && F->getName().find(Naming::CONTRACT_EXPR) != std::string::npos + && "Expected contract expression argument to contract function."); + CallInst* cj = dyn_cast(ci.getArgOperand(0)); + assert(cj && "Expected contract expression argument to contract function."); + Function* F = cj->getCalledFunction(); + assert(F && F->getName().find(Naming::CONTRACT_EXPR) != std::string::npos && "Expected contract expression argument to contract function."); std::list args; @@ -597,6 +618,11 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { if (!EXTERNAL_PROC_IGNORE.match(name)) emit(Stmt::assume(Expr::fn(Naming::EXTERNAL_ADDR,rep.expr(&ci)))); } + + if ((naming.get(*f).find("__SMACK") == 0 || naming.get(*f).find("__VERIFIER") == 0) + && !f->getReturnType()->isVoidTy()) { + emit(recordProcedureCall(&ci, {Attr::attr("cexpr", "smack:ext:" + naming.get(*f))})); + } } bool isSourceLoc(const Stmt* stmt) { diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index d7982459f..6236000c3 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -705,8 +705,8 @@ const Expr* SmackRep::expr(const llvm::Value* v, bool isConstIntUnsigned) { v = v->stripPointerCasts(); } - if (const GlobalValue* g = dyn_cast(v)) { - assert(g->hasName()); + if (isa(v)) { + assert(v->hasName()); return Expr::id(naming.get(*v)); } else if (isa(v)) { diff --git a/lib/smack/SmackRepFlatMem.cpp b/lib/smack/SmackRepFlatMem.cpp deleted file mode 100644 index 8a28bdd1d..000000000 --- a/lib/smack/SmackRepFlatMem.cpp +++ /dev/null @@ -1,11 +0,0 @@ -// -// This file is distributed under the MIT License. See LICENSE for details. -// -#include "smack/SmackRep.h" -#include "smack/SmackOptions.h" - -namespace smack { - - - -} // namespace smack diff --git a/share/smack/include/smack-contracts.h b/share/smack/include/smack-contracts.h index 809f0082d..0128382fd 100644 --- a/share/smack/include/smack-contracts.h +++ b/share/smack/include/smack-contracts.h @@ -23,8 +23,4 @@ bool __CONTRACT_exists(const char *var, bool expr) __attribute__((const)); int old(int term); int result(void); -#undef bool -#undef true -#undef false - #endif diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index c7b8e1eb9..5f8954337 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -2022,6 +2022,11 @@ void __SMACK_decls() { D("var $exnv: int;"); D("function $extractvalue(p: int, i: int) returns (int);\n"); + D("procedure $alloc(n: ref) returns (p: ref)\n" + "{\n" + " call p := $$alloc(n);\n" + "}\n"); + #if MEMORY_SAFETY D("function $base(ref) returns (ref);"); D("var $allocatedCounter: int;\n"); @@ -2030,7 +2035,7 @@ void __SMACK_decls() { "modifies $allocatedCounter;\n" "{\n" " $allocatedCounter := $allocatedCounter + 1;\n" - " call p := $alloc(n);\n" + " call p := $$alloc(n);\n" "}\n"); #if MEMORY_MODEL_NO_REUSE_IMPLS @@ -2045,7 +2050,7 @@ void __SMACK_decls() { " $Alloc[base_addr] := true;\n" "}\n"); - D("procedure $alloc(n: ref) returns (p: ref)\n" + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n" "modifies $Alloc, $CurrAddr;\n" "{\n" " p := $CurrAddr;\n" @@ -2086,7 +2091,7 @@ void __SMACK_decls() { "ensures (forall q: ref :: {$Size[q]} q != base_addr ==> $Size[q] == old($Size[q]));\n" "ensures (forall q: ref :: {$Alloc[q]} q != base_addr ==> $Alloc[q] == old($Alloc[q]));\n"); - D("procedure $alloc(n: ref) returns (p: ref);\n" + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n" "modifies $Alloc, $Size;\n" "ensures $sgt.ref.bool(p, $0.ref);\n" "ensures $slt.ref.bool(p, $MALLOC_TOP);\n" @@ -2118,7 +2123,7 @@ void __SMACK_decls() { "ensures $Alloc[base_addr];\n" "ensures (forall q: ref :: {$Alloc[q]} q != base_addr ==> $Alloc[q] == old($Alloc[q]));\n"); - D("procedure $alloc(n: ref) returns (p: ref);\n" + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n" "modifies $Alloc, $CurrAddr;\n" "ensures p == old($CurrAddr);\n" "ensures $sgt.ref.bool(n, $0.ref) ==> $sle.ref.bool($add.ref(old($CurrAddr), n), $CurrAddr);\n" @@ -2142,13 +2147,13 @@ void __SMACK_decls() { #else D("procedure $malloc(n: ref) returns (p: ref)\n" "{\n" - " call p := $alloc(n);\n" + " call p := $$alloc(n);\n" "}\n"); #if MEMORY_MODEL_NO_REUSE_IMPLS D("var $CurrAddr:ref;\n"); - D("procedure $alloc(n: ref) returns (p: ref)\n" + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n" "modifies $CurrAddr;\n" "{\n" " p := $CurrAddr;\n" @@ -2166,7 +2171,7 @@ void __SMACK_decls() { D("var $Alloc: [ref] bool;"); D("var $Size: [ref] ref;\n"); - D("procedure $alloc(n: ref) returns (p: ref);\n" + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n" "modifies $Alloc, $Size;\n" "ensures $sgt.ref.bool(p, $0.ref);\n" "ensures $slt.ref.bool(p, $MALLOC_TOP);\n" @@ -2185,7 +2190,7 @@ void __SMACK_decls() { #else // NO_REUSE does not reuse previously-allocated addresses D("var $CurrAddr:ref;\n"); - D("procedure $alloc(n: ref) returns (p: ref);\n" + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n" "modifies $CurrAddr;\n" "ensures p == old($CurrAddr);\n" "ensures $sgt.ref.bool(n, $0.ref) ==> $sle.ref.bool($add.ref(old($CurrAddr), n), $CurrAddr);\n" @@ -2300,6 +2305,17 @@ char *strerror(int errnum) { return error_str; } +char *env_value_str = "xx"; +char *getenv(const char *name) { + if (__VERIFIER_nondet_int()) { + return 0; + } else { + env_value_str[0] = __VERIFIER_nondet_char(); + env_value_str[1] = __VERIFIER_nondet_char(); + return env_value_str; + } +} + void *realloc (void *__ptr, size_t __size) { free(__ptr); return malloc(__size); diff --git a/share/smack/reach.py b/share/smack/reach.py index 154947963..5b8280411 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '1.7.2' +VERSION = '1.8.0' def reachParser(): parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()]) diff --git a/share/smack/replay.py b/share/smack/replay.py new file mode 100644 index 000000000..3fb996920 --- /dev/null +++ b/share/smack/replay.py @@ -0,0 +1,156 @@ +import os +import re +import subprocess +import sys +from utils import temporary_file, try_command + +SPECIAL_NAMES = [ + '__VERIFIER_assert', + '__VERIFIER_assume' +] + +def replay_error_trace(verifier_output, args): + + if args.verifier != 'corral': + print "Replay for verifiers other than 'corral' currently unsupported; skipping replay" + return + + print "Attempting to replay error trace." + + missing_definitions = detect_missing_definitions(args.bc_file) + if '__SMACK_code' in missing_definitions: + print "warning: inline Boogie code found; replay may fail" + + arguments, return_values = extract_values(verifier_output) + + with open(args.replay_harness, 'w') as f: + f.write(harness(arguments, return_values, missing_definitions)) + print "Generated replay harness:", args.replay_harness + + stubs_bc = temporary_file('stubs', '.bc', args) + try_command(['clang', '-c', '-emit-llvm', '-o', stubs_bc, args.replay_harness]) + try_command(['clang', '-Wl,-e,_smack_replay_main', '-o', args.replay_exe_file, args.bc_file, stubs_bc]) + print "Generated replay executable:", args.replay_exe_file + + try: + if 'error reached!' in try_command(["./" + args.replay_exe_file]): + print "Error-trace replay successful." + return True + + else: + print "Error-trace replay failed." + + except Exception as err: + print "Error-trace replay caught", err.message + + return False + + +def detect_missing_definitions(bc_file): + missing = [] + try: + try_command(['clang', bc_file]) + except Exception as err: + for line in err.message.split("\n"): + m = re.search(r'\"_(.*)\", referenced from:', line) or re.search(r'undefined reference to `(.*)\'', line) + if m: + missing.append(m.group(1)) + return missing + + +def extract(line): + match = re.search(r'.*\((smack:.*) = (.*)\).*', line) + return match and [match.group(1), match.group(2)] + + +def extract_values(trace): + arguments = {} + return_values = {} + + for key, val in filter(lambda x: x, map(extract, trace.split('\n'))): + if 'smack:entry:' in key: + _, _, fn = key.split(':') + arguments[fn] = [] + + elif 'smack:arg:' in key: + _, _, fn, arg = key.split(':') + if not fn in arguments: + raise Exception("expected entry point key smack:entry:%s" % fn) + arguments[fn].append(val) + + elif 'smack:ext:' in key: + _, _, fn = key.split(':') + if not fn in return_values: + return_values[fn] = [] + return_values[fn].append(val) + + else: + print "warning: unexpected key %s" % key + + return arguments, return_values + + +def harness(arguments, return_values, missing_definitions): + code = [] + code.append("""// +// This file was automatically generated from a Boogie error trace. +// It contains stubs for unspecified functions that were called in that trace. +// These stubs will return the same values they did in the error trace. +// This file can be linked with the source program to reproduce the error. +// +#include +#include + +void __VERIFIER_assert(int b) { + if (!b) { + printf("error reached!\\n"); + exit(0); + } +} + +void __VERIFIER_assume(int b) { + if (!b) { + printf("assumption does not hold.\\n"); + exit(-1); + } +} +""") + + for fn in set(missing_definitions) - set(SPECIAL_NAMES): + if fn in return_values: + code.append("""// stub for function: %(fn)s +int %(fn)s$table[] = {%(vals)s}; +int %(fn)s$idx = 0; + +int %(fn)s() { + return %(fn)s$table[%(fn)s$idx++]; +} +""" % {'fn': fn, 'vals': ", ".join(return_values[fn])}) + + else: + print "warning: unknown return value for %s" % fn + code.append("""// stub for function %(fn)s +void %(fn)s() { + return; +} +""" % {'fn': fn}) + + if len(arguments) > 1: + print "warning: multiple entrypoint argument annotations found" + + elif len(arguments) < 1: + print "warning: no entrypoint argument annotations found" + + for fn, args in arguments.items(): + code.append("""// entry point wrapper +int _smack_replay_main() { + %(fn)s(%(vals)s); + return 0; +} +int smack_replay_main() { + %(fn)s(%(vals)s); + return 0; +} +""" % {'fn': fn, 'vals': ", ".join(args)}) + + return "\n".join(code) diff --git a/share/smack/top.py b/share/smack/top.py index ef686242b..753ff3c53 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -6,16 +6,13 @@ import platform import re import shutil -import signal -import subprocess import sys -import tempfile -from threading import Timer from svcomp.utils import svcomp_frontend from svcomp.utils import verify_bpl_svcomp +from utils import temporary_file, try_command, remove_temp_files +from replay import replay_error_trace -VERSION = '1.7.2' -temporary_files = [] +VERSION = '1.8.0' def frontends(): """A dictionary of front-ends per file extension.""" @@ -34,7 +31,7 @@ def frontends(): def results(args): """A dictionary of the result output messages.""" return { - 'verified': 'SMACK found no errors with unroll bound %s.' % args.unroll, + 'verified': 'SMACK found no errors.' if args.modular else 'SMACK found no errors with unroll bound %s.' % args.unroll, 'error': 'SMACK found an error.', 'invalid-deref': 'SMACK found an error: invalid pointer dereference.', 'invalid-free': 'SMACK found an error: invalid memory deallocation.', @@ -46,11 +43,16 @@ def results(args): def inlined_procedures(): return [ + '$galloc', '$alloc', + '$malloc', '$free', '$memset', '$memcpy', - '__VERIFIER_' + '__VERIFIER_', + '$initialize', + '__SMACK_static_init', + '__SMACK_init_func_memory_model' ] def validate_input_file(file): @@ -95,6 +97,7 @@ def arguments(): parser.add_argument('-w', '--error-file', metavar='FILE', default=None, type=str, help='save error trace/witness to FILE') + frontend_group = parser.add_argument_group('front-end options') frontend_group.add_argument('-x', '--language', metavar='LANG', @@ -104,12 +107,22 @@ def arguments(): frontend_group.add_argument('-bc', '--bc-file', metavar='FILE', default=None, type=str, help='save initial LLVM bitcode to FILE') + frontend_group.add_argument('--linked-bc-file', metavar='FILE', default=None, + type=str, help=argparse.SUPPRESS) + + frontend_group.add_argument('--replay-harness', metavar='FILE', default='replay-harness.c', + type=str, help=argparse.SUPPRESS) + + frontend_group.add_argument('--replay-exe-file', metavar='FILE', default='replay-exe', + type=str, help=argparse.SUPPRESS) + frontend_group.add_argument('-ll', '--ll-file', metavar='FILE', default=None, type=str, help='save final LLVM IR to FILE') frontend_group.add_argument('--clang-options', metavar='OPTIONS', default='', help='additional compiler arguments (e.g., --clang-options="-w -g")') + translate_group = parser.add_argument_group('translation options') translate_group.add_argument('-bpl', '--bpl-file', metavar='FILE', default=None, @@ -154,6 +167,10 @@ def arguments(): translate_group.add_argument('--signed-integer-overflow', action='store_true', default=False, help='enable signed integer overflow checks') + translate_group.add_argument('--float', action="store_true", default=False, + help='enable bit-precise floating-point functions') + + verifier_group = parser.add_argument_group('verifier options') verifier_group.add_argument('--verifier', @@ -184,15 +201,21 @@ def arguments(): verifier_group.add_argument('--svcomp-property', metavar='FILE', default=None, type=str, help='load SVCOMP property to check from FILE') - - translate_group.add_argument('--float', action="store_true", default=False, - help='enable bit-precise floating-point functions') + + verifier_group.add_argument('--modular', action="store_true", default=False, + help='enable contracts-based modular deductive verification (uses Boogie)') + + verifier_group.add_argument('--replay', action="store_true", default=False, + help='enable reply of error trace with test harness.') args = parser.parse_args() if not args.bc_file: args.bc_file = temporary_file('a', '.bc', args) + if not args.linked_bc_file: + args.linked_bc_file = temporary_file('b', '.bc', args) + if not args.bpl_file: args.bpl_file = 'a.bpl' if args.no_verify else temporary_file('a', '.bpl', args) @@ -208,71 +231,6 @@ def arguments(): return args -def temporary_file(prefix, extension, args): - f, name = tempfile.mkstemp(extension, prefix + '-', os.getcwd(), True) - os.close(f) - if not args.debug: - temporary_files.append(name) - return name - -def timeout_killer(proc, timed_out): - if not timed_out[0]: - timed_out[0] = True - os.killpg(os.getpgid(proc.pid), signal.SIGKILL) - -def try_command(cmd, cwd=None, console=False, timeout=None): - console = (console or args.verbose or args.debug) and not args.quiet - filelog = args.debug - output = '' - proc = None - timer = None - try: - if args.debug: - print "Running %s" % " ".join(cmd) - - proc = subprocess.Popen(cmd, cwd=cwd, preexec_fn=os.setsid, - stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - - if timeout: - timed_out = [False] - timer = Timer(timeout, timeout_killer, [proc, timed_out]) - timer.start() - - if console: - while True: - line = proc.stdout.readline() - if line: - output += line - print line, - elif proc.poll() is not None: - break - proc.wait - else: - output = proc.communicate()[0] - - if timeout: - timer.cancel() - - rc = proc.returncode - proc = None - if timeout and timed_out[0]: - return output + ("\n%s timed out." % cmd[0]) - elif rc: - raise RuntimeError("%s returned non-zero." % cmd[0]) - else: - return output - - except (RuntimeError, OSError) as err: - print >> sys.stderr, output - sys.exit("Error invoking command:\n%s\n%s" % (" ".join(cmd), err)) - - finally: - if timeout and timer: timer.cancel() - if proc: os.killpg(os.getpgid(proc.pid), signal.SIGKILL) - if filelog: - with open(temporary_file(cmd[0], '.log', args), 'w') as f: - f.write(output) - def target_selection(args): """Determine the target architecture based on flags and source files.""" # TODO more possible clang flags that determine the target? @@ -345,14 +303,14 @@ def boogie_frontend(args): def llvm_frontend(args): """Generate Boogie code from LLVM bitcodes.""" - bitcodes = build_libs(args) + args.input_files - try_command(['llvm-link', '-o', args.bc_file] + bitcodes) + try_command(['llvm-link', '-o', args.bc_file] + args.input_files) + try_command(['llvm-link', '-o', args.linked_bc_file, args.bc_file] + build_libs(args)) llvm_to_bpl(args) def clang_frontend(args): """Generate Boogie code from C-language source(s).""" - bitcodes = build_libs(args) + bitcodes = [] compile_command = default_clang_compile_command(args) for c in args.input_files: @@ -361,6 +319,7 @@ def clang_frontend(args): bitcodes.append(bc) try_command(['llvm-link', '-o', args.bc_file] + bitcodes) + try_command(['llvm-link', '-o', args.linked_bc_file, args.bc_file] + build_libs(args)) llvm_to_bpl(args) def json_compilation_database_frontend(args): @@ -372,14 +331,13 @@ def json_compilation_database_frontend(args): output_flags = re.compile(r"-o ([^ ]*)[.]o\b") optimization_flags = re.compile(r"-O[1-9]\b") - lib_bitcodes = build_libs(args) - with open(args.input_files[0]) as f: for cc in json.load(f): if 'objects' in cc: # TODO what to do when there are multiple linkings? bit_codes = map(lambda f: re.sub('[.]o$','.bc',f), cc['objects']) - try_command(['llvm-link', '-o', args.bc_file] + bit_codes + lib_bitcodes) + try_command(['llvm-link', '-o', args.bc_file] + bit_codes) + try_command(['llvm-link', '-o', args.linked_bc_file, args.bc_file] + build_libs(args)) else: out_file = output_flags.findall(cc['command'])[0] + '.bc' @@ -394,7 +352,7 @@ def json_compilation_database_frontend(args): def llvm_to_bpl(args): """Translate the LLVM bitcode file to a Boogie source file.""" - cmd = ['llvm2bpl', args.bc_file, '-bpl', args.bpl_file] + cmd = ['llvm2bpl', args.linked_bc_file, '-bpl', args.bpl_file] cmd += ['-warnings'] cmd += ['-source-loc-syms'] for ep in args.entry_points: @@ -410,6 +368,7 @@ def llvm_to_bpl(args): if args.memory_safety: cmd += ['-memory-safety'] if args.signed_integer_overflow: cmd += ['-signed-integer-overflow'] if args.float: cmd += ['-float'] + if args.modular: cmd += ['-modular'] try_command(cmd, console=True) annotate_bpl(args) property_selection(args) @@ -417,9 +376,9 @@ def llvm_to_bpl(args): def procedure_annotation(name, args): if name in args.entry_points: return "{:entrypoint}" - elif re.match("|".join(inlined_procedures()).replace("$","\$"), name): + elif args.modular and re.match("|".join(inlined_procedures()).replace("$","\$"), name): return "{:inline 1}" - elif args.verifier == 'boogie' or args.float: + elif (not args.modular) and (args.verifier == 'boogie' or args.float): return ("{:inline %s}" % args.unroll) else: return "" @@ -496,13 +455,14 @@ def verify_bpl(args): verify_bpl_svcomp(args) return - elif args.verifier == 'boogie': + elif args.verifier == 'boogie' or args.modular: command = ["boogie"] command += [args.bpl_file] command += ["/nologo", "/noinfer", "/doModSetAnalysis"] command += ["/timeLimit:%s" % args.time_limit] command += ["/errorLimit:%s" % args.max_violations] - command += ["/loopUnroll:%d" % args.unroll] + if not args.modular: + command += ["/loopUnroll:%d" % args.unroll] elif args.verifier == 'corral': command = ["corral"] @@ -551,6 +511,9 @@ def verify_bpl(args): if not args.quiet: print error + if args.replay: + replay_error_trace(verifier_output, args) + sys.exit(results(args)[result]) def error_step(step): @@ -664,6 +627,4 @@ def main(): sys.exit("SMACK aborted by keyboard interrupt.") finally: - for f in temporary_files: - if os.path.isfile(f): - os.unlink(f) + remove_temp_files() diff --git a/share/smack/utils.py b/share/smack/utils.py new file mode 100644 index 000000000..1ee05c838 --- /dev/null +++ b/share/smack/utils.py @@ -0,0 +1,82 @@ +import os +import sys +import tempfile +import subprocess +import signal +from threading import Timer +import top + +temporary_files = [] + +def temporary_file(prefix, extension, args): + f, name = tempfile.mkstemp(extension, prefix + '-', os.getcwd(), True) + os.close(f) + if not args.debug: + temporary_files.append(name) + return name + +def remove_temp_files(): + for f in temporary_files: + if os.path.isfile(f): + os.unlink(f) + +def timeout_killer(proc, timed_out): + if not timed_out[0]: + timed_out[0] = True + os.killpg(os.getpgid(proc.pid), signal.SIGKILL) + +def try_command(cmd, cwd=None, console=False, timeout=None): + args = top.args + console = (console or args.verbose or args.debug) and not args.quiet + filelog = args.debug + output = '' + proc = None + timer = None + try: + if args.debug: + print "Running %s" % " ".join(cmd) + + proc = subprocess.Popen(cmd, cwd=cwd, preexec_fn=os.setsid, + stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + + if timeout: + timed_out = [False] + timer = Timer(timeout, timeout_killer, [proc, timed_out]) + timer.start() + + if console: + while True: + line = proc.stdout.readline() + if line: + output += line + print line, + elif proc.poll() is not None: + break + proc.wait + else: + output = proc.communicate()[0] + + if timeout: + timer.cancel() + + rc = proc.returncode + proc = None + if timeout and timed_out[0]: + return output + ("\n%s timed out." % cmd[0]) + elif rc == -signal.SIGSEGV: + raise Exception("segmentation fault") + elif rc: + raise Exception(output) + else: + return output + + except (RuntimeError, OSError) as err: + print >> sys.stderr, output + sys.exit("Error invoking command:\n%s\n%s" % (" ".join(cmd), err)) + + finally: + if timeout and timer: timer.cancel() + if proc: os.killpg(os.getpgid(proc.pid), signal.SIGKILL) + if filelog: + with open(temporary_file(cmd[0], '.log', args), 'w') as f: + f.write(output) diff --git a/svcomp/bench/src/SMACKBench.py b/svcomp/bench/src/SMACKBench.py new file mode 100755 index 000000000..5b7f72db2 --- /dev/null +++ b/svcomp/bench/src/SMACKBench.py @@ -0,0 +1,315 @@ +#!/usr/bin/env python +import sys +sys.dont_write_bytecode = True # prevent creation of .pyc files + +import argparse +import daemon +import json +import os +import signal +import subprocess +import sys +import time +from datetime import datetime +from os import path +from socket import gethostname + +####################################### +### Common functions +####################################### +def get_args(): + parser = argparse.ArgumentParser(description='Executes a SMACKBench jobs queue') + subparsers = parser.add_subparsers(help = 'Sub-command help') + server = subparsers.add_parser('server', + help = 'Start SMACKBench in server mode', + formatter_class=argparse.ArgumentDefaultsHelpFormatter) + server.set_defaults(mode='server') + server.add_argument('-q', '--queue-file', + default='inputFiles/queue', metavar='FILE', + help='The file containing the list of jobs to process') + server.add_argument('-r', '--concurrentRuns', + default='8', metavar='NUM', + help='The number of concurrent benchmarks to run') + server.add_argument('-m', '--memoryPerRun', + default='15000', metavar='NUM', + help='Amount of memory per concurrent run (in MB)') + server.add_argument('-c', '--config-file', + default='inputFiles/config.json', metavar='FILE', + help='The json file with SMACKBench config settings') + server.add_argument('-d', '--description', + default='', metavar='DESC', + help='A description field (identifier) to be associated with each set') + + stop = subparsers.add_parser('stop', + help='Stop all instances of SMACKBench') + stop.set_defaults(mode='stop') + + run = subparsers.add_parser('run', + help='Run SMACKBench on a single svcomp set', + formatter_class=argparse.ArgumentDefaultsHelpFormatter) + run.set_defaults(mode='run') + run.add_argument('-s', '--svcomp-set', required=True, metavar='SET', + help='The svcomp set to execute') + run.add_argument('-x', '--inputXmlFile', required=True, metavar='FILE', + help='The input XML file with which to run svcomp-set') + run.add_argument('-r', '--concurrentRuns', default='8', metavar='NUM', + help='The number of concurrent benchmarks to run') + run.add_argument('-m', '--memoryPerRun', default='15000', metavar='NUM', + help='Amount of memory per concurrent run (in MB)') + run.add_argument('-c', '--config-file', + default='inputFiles/config.json', metavar='FILE', + help='The json file with SMACKBench config settings') + run.add_argument('-d', '--description', + default='', metavar='DESC', + help='A description field (identifier) to be associated with each set') + args = parser.parse_args() + return args + +def get_config(configFile): + with open(configFile, 'r') as f: + cfg = json.load(f) + return cfg + +def handle_sigterm(signum, frame): + #benchexec only runs cleanup routine when it sees + #sigint. To force this to run when receiving a sigterm, + #we'll intercept it and simulate a sigint instead + raise KeyboardInterrupt + +####################################### +## ## +## SMACKBenchServer ## +## ## +####################################### + +####################################### +### SMACKBench Queueing functions +####################################### + +#Creates a lock by making the directory lock_dir (in cwd) +#If directory exists, lock is already being held +def lock(lock_dir): + while True: + try: + os.mkdir(lock_dir) + return + except OSError as e: + if e.errno != 17: + raise + +#Releases a lock by deleting the directory lock_dir (from cwd) +def unlock(lock_dir): + try: + os.rmdir(lock_dir) + except: + pass + +def dequeue(filename, lock_folder): + #Pops and returns a line off the top of the input file + try: + cur = None + lock(lock_folder) + with open(filename,'r+') as f: + lines = f.readlines() + f.seek(0) + if len(lines)==0: + unlock(lock_folder) + return cur + cur = lines[0].strip() + lines = lines[1:] + for line in lines: + f.write(line) + f.truncate() + finally: + unlock(lock_folder) + return cur + +def enqueue(data, filename, lock_folder): + #Pushes a line to the end of the given filename + #(I think this is currently unused) + try: + lock(lock_folder) + with open(filename,'a') as f: + f.write(data + '\n') + finally: + unlock(lock_folder) + +####################################### +### SMACKBench Server +####################################### +def run_server(cfgObj, queueFile, concurRunCnt, memPerRun, desc): + #Register our sigterm handler, so we can catch it and raise + #KeyboardInterrupt instead. This way benchexec's cleanup + #routines run + signal.signal(signal.SIGTERM, handle_sigterm) + lock_folder = 'lck' + while(True): + # Pop a job + job = dequeue(queueFile, lock_folder) + # And run it if it exists (that is, if the queue is not empty) + if job: + # First, clean old .bc, .bpl, and .ll + # Deletes files modified more than 2 hours + cmdPre = ['find', './', '-maxdepth', '1', '-name'] + cmdPost = ['-mmin', '+120', '-delete'] + for ext in ['bpl','bc','ll','i','c','dot']: + subprocess.call(cmdPre + ['"*.' + ext + '"'] + cmdPost); + + job = job.split() #Splits into [, ] + runSMACKBench(cfgObj, job[0], job[1], concurRunCnt, memPerRun, desc) + else: + #If the queue file is empty, wait 10 seconds + time.sleep(10) + +####################################### +## ## +## runSMACKBench ## +## ## +####################################### +def generateOutFolder(cfgObj, svSet): + #Generate output folder name and create new directory + timestamp = datetime.now().strftime("%Y.%m.%d_%H.%M.%S.%f") + outFold = "exec_{0}_{1}".format(timestamp,svSet) + outPath = path.join(cfgObj['runsFolder'], outFold) + os.makedirs(outPath) + return outPath + +def copyInXmlAndInject(cfgObj, outPath, svSet, inXmlFile, memPerRun, desc): + #Deterime the destination input xml file location + dstInXmlFile = path.join(outPath, path.split(inXmlFile)[-1]) + #Read the input xml file template (must use .. since input xml + # file is relative to root, but we changed cwd to dataFolder, + # so we must adjust this path) + with open(path.join('..', inXmlFile), 'r') as inXml: + inXmlStr = inXml.read() + #NOTE: Replacement variables in input xml template that begin + # with a $ are used by benchexec (e.g., ${sourcefile_path}) + # Replacement vars in use by SMACKBench take the form {varname} + #Inject set name + inXmlStr = inXmlStr.replace('{SETNAME}', svSet) + #Inject description (we hijack the benchexec setdefinition_name field to + # contain description. This allows us to avoid changing xml schema of + # benchexec in/out xml files.) + inXmlStr = inXmlStr.replace('{DESCRIPTION}', + '' if not desc else '-'+desc.replace(' ','')) + #Inject memory per concurrent run limit + inXmlStr = inXmlStr.replace('{MEMLIMIT}', memPerRun) + #Inject number of cores allowed for each concurrently run benchmark + inXmlStr = inXmlStr.replace('{CORELIMIT}', cfgObj['coreLimit']) + #Determine the set definition file, relative to the dest input xml file + bmRel = path.relpath(cfgObj['benchmarkRoot'], path.dirname(dstInXmlFile)) + setDefFile = path.join(bmRel, svSet + ".set") + prpDefFile = path.join(bmRel, svSet + ".prp") + #Inject the set definition file (*.set) path (using relative path) + # (benchexec does everything relative to the input xml file) + inXmlStr = inXmlStr.replace('{SETDEFINITIONFILE}', setDefFile) + inXmlStr = inXmlStr.replace('{PROPERTYDEFINITIONFILE}', prpDefFile) + + #Write the input xml file + with open(dstInXmlFile, 'w') as dstXml: + dstXml.write(inXmlStr) + #Return the full file path of the injected input xml file + return dstInXmlFile + +def runBenchExec(cfgObj, inXmlFile, outPath, concurRunCnt, debug): + #This should probably be changed to use the benchexec python modules, + # rather than running as an executable + + #Config file passes benchexecPath as relative to root, but we changed + # cwd to dataFolder, and reference everything from this folder. As + # a result, we must patch the benchexecPath so it is relative to + # dataFolder + cmd = [path.join('..', cfgObj['benchexecPath'], 'benchexec')] + if debug: + cmd += ['-d'] + cmd += [inXmlFile] + #For some reason, benchexec needs to see a / on the end of the string + # to know the last item of the -o value is a folder. + cmd += ['-o', path.join(outPath, 'results') + '/'] + cmd += ['--no-compress'] + cmd += ['-N', concurRunCnt] + + print(cmd) + p = subprocess.Popen(cmd) + try: + p.wait() + except KeyboardInterrupt as e: + #If we get interrupted by a KeyboardInterrupt, pass it on to + # benchexec, so it can do its cleanup + p.send_signal(signal.SIGINT) + raise KeyboardInterrupt + +def witnessCheckingFunc(cfgObj, outPath): + #Get cwd, so we can return afterwards + execDir = os.getcwd() + print(execDir) + #change to root dir + os.chdir('..') + print(os.getcwd()) + cmd = ['./checkWitnesses.py'] + cmd += [os.path.join(cfgObj["dataFolder"], outPath)] + print(cmd) + p = subprocess.Popen(cmd) + try: + p.wait() + except KeyboardInterrupt as e: + #If we get interrupted by a KeyboardInterrupt, pass it on to + # benchexec, so it can do its cleanup + p.send_signal(signal.SIGINT) + raise KeyboardInterrupt + os.chdir(execDir) + +def runSMACKBench(cfgObj, svSet, inXmlFile, concurRunCnt, memPerRun, desc): + #Generate results folder name and create + outPath = generateOutFolder(cfgObj, svSet) + #Copy the input xml file template to the new output directory, + # and inject relevant variables + dstInXml = copyInXmlAndInject(cfgObj, outPath, svSet, inXmlFile, memPerRun, desc) + #Call benchexec + runBenchExec(cfgObj, dstInXml, outPath, concurRunCnt, debug = False) + #Run witness checking + witnessCheckingFunc(cfgObj, outPath) + +if __name__ == '__main__': + args = get_args() + #If stop command is given, stop all instances of SMACKBench + if (args.mode == 'stop'): + #Since only one instance of benchexec can run at a given time, + #we can blindly kill all running SMACKBench.py instances + subprocess.check_call(['pkill','-SIGTERM','-f','SMACKBench.py']) + #Read the config file + cfgObj = get_config(args.config_file) + #EVERYTHING in SMACKBench is relative to dataFolder (internally, that is) + # however, this must be adjusted within this program. (Except for config + # file location) + # Externally, (in config file, for example), paths are relative to root + #As a result, all paths that come as input to this program get adjusted + # from being relative to root to being relative to dataFolder before + # being used + os.chdir(cfgObj['dataFolder']) + #Make sure folders are created + for fold in [cfgObj['runsFolder'], cfgObj['logFolder']]: + try: + os.mkdir(fold) + except OSError: + #Already exists + pass + #If server command given + if(args.mode == 'server'): + #Determine the destination log file + logFile = path.join(cfgObj['logFolder'], gethostname() + '.log') + #Start the run_server function as a daemon, redirecting stderr to + #stdout, and stdout to the log file + print("To see benchexec console outputin real time, run 'tail -f {0}'".format(path.join(cfgObj['dataFolder'],logFile))) + with daemon.DaemonContext(working_directory = os.getcwd(), + stderr=sys.stdout, + stdout=open(logFile, 'a')): + run_server(cfgObj, path.join('..', args.queue_file), + args.concurrentRuns, args.memoryPerRun, args.description) + + else: + #if here, we're in run mode + #signal.signal(signal.SIGTERM, handle_sigterm) + runSMACKBench(cfgObj, args.svcomp_set, args.inputXmlFile, + args.concurrentRuns, args.memoryPerRun, + args.description) diff --git a/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py b/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py index 37b308c27..0de39cf61 100644 --- a/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py +++ b/svcomp/bench/src/benchexec/benchexec/tools/smack_benchexec_driver.py @@ -35,7 +35,7 @@ def version(self, executable): Sets the version number for SMACK, which gets displayed in the "Tool" row in BenchExec table headers. """ - return '1.7.2' + return '1.8.0' def name(self): """ diff --git a/svcomp/bench/src/benchexec/benchexec/tools/smack_built.py b/svcomp/bench/src/benchexec/benchexec/tools/smack_built.py new file mode 100644 index 000000000..1a2991b9a --- /dev/null +++ b/svcomp/bench/src/benchexec/benchexec/tools/smack_built.py @@ -0,0 +1,121 @@ +import os +import re + +import logging +import xml.etree.ElementTree as ET + +import benchexec.util as util +import benchexec.tools.template +import benchexec.result as result + +""" +This file defines Smack for BenchExec. It defines a class that inherits from +BenchExec's BaseTool class, which declares functions that the BenchExec framework +uses to interact with the tool. + +The 'tool' attribute for the root 'benchmark' nodes of input xml files should be +set to the name of this file without extension, i.e. 'smack_benchexec_driver'. +""" + +class Tool(benchexec.tools.template.BaseTool): + + REQUIRED_PATHS = [ + "corral", + "llvm", + "lockpwn", + "smack" + + ] + + def executable(self): + """ + Tells BenchExec to search for 'smack.py' as the main executable to be + called when running SMACK. + """ + return util.find_executable('smack') + + def version(self, executable): + """ + Sets the version number for SMACK, which gets displayed in the "Tool" row + in BenchExec table headers. + """ + #return self._version_from_tool(executable).split(' ')[2] + return "1.5.2" + + def name(self): + """ + Sets the name for SMACK, which gets displayed in the "Tool" row in + BenchExec table headers. + """ + return 'SMACK+Corral' + + def cmdline(self, executable, options, tasks, propertyfile=None, rlimits= +{}): + """ + Allows us to define special actions to be taken or command line argument + modifications to make just before calling SMACK. + """ + assert len(tasks) == 1 + assert propertyfile is not None + prop = ['--svcomp-property', propertyfile] + return [executable] + options + prop + tasks + + def determine_result(self, returncode, returnsignal, output, isTimeout): + """ + Returns a BenchExec result status based on the output of SMACK + """ + splitout = "\n".join(output) + if 'SMACK found no errors' in splitout: + return result.RESULT_TRUE_PROP + errmsg = re.search(r'SMACK found an error(:\s+([^\.]+))?\.', splitout) + if errmsg: + errtype = errmsg.group(2) + if errtype: + if 'invalid pointer dereference' == errtype: + return result.RESULT_FALSE_DEREF + elif 'invalid memory deallocation' == errtype: + return result.RESULT_FALSE_FREE + elif 'memory leak' == errtype: + return result.RESULT_FALSE_MEMTRACK + elif 'signed integer overflow' == errtype: + return result.RESULT_FALSE_OVERFLOW + else: + return result.RESULT_FALSE_REACH + return result.RESULT_UNKNOWN + + def get_value_from_output(self, lines, identifier): + """ + This function can be referenced in the input xml files (which can define + additional columns to be displayed in the output tables), and extracts + additional information from tool output (with the idea that extra + statistical information would be extracted from tool output, and included + as a column in the resulting output tables). + + We are using this to generate HTML links for output files, rather than + parsing output and providing additional statistical data about the run. + + This currently generates a drop-down menu item for the .bc, .bpl, + generated witness file, and the output from the witness checking tool. + + However, the witness file and checking links are hidden by default, as + they will not exist if the witness checking pass has not been performed, + or if the benchmark result was true (in which case there is no trace). + The visibility of these must be set to visible when witness checking is + performed for this execution. + """ + #identifier comes from pattern field of input xml node, + # which then has variable substitution performed on it first + #If identifier is the input source file path+name, this will create + # links in the output table for bpl, bc, and witness related files + ret = "" + ret += '
\n' + ret += ' \n' + ret += '
\n' + return ret diff --git a/svcomp/bench/src/benchexec/benchexec/tools/smack_packaged.py b/svcomp/bench/src/benchexec/benchexec/tools/smack_packaged.py new file mode 100644 index 000000000..0ce1de933 --- /dev/null +++ b/svcomp/bench/src/benchexec/benchexec/tools/smack_packaged.py @@ -0,0 +1,123 @@ +""" +BenchExec is a framework for reliable benchmarking. +This file is part of BenchExec. +Copyright (C) 2007-2015 Dirk Beyer +All rights reserved. +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + http://www.apache.org/licenses/LICENSE-2.0 +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +""" + +import benchexec.result as result +import benchexec.util as util +import benchexec.tools.template + +import os +import re + +class Tool(benchexec.tools.template.BaseTool): + + REQUIRED_PATHS = [ + "corral", + "llvm", + "lockpwn", + "smack", + "smack.sh" + ] + + def executable(self): + """ + Tells BenchExec to search for 'smack.sh' as the main executable to be + called when running SMACK. + """ + return util.find_executable('smack.sh') + + def version(self, executable): + """ + Sets the version number for SMACK, which gets displayed in the "Tool" row + in BenchExec table headers. + """ + #return self._version_from_tool(executable).split(' ')[2] + return "1.5.2" + + def name(self): + """ + Sets the name for SMACK, which gets displayed in the "Tool" row in + BenchExec table headers. + """ + return 'SMACK+Corral' + + def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}): + """ + Allows us to define special actions to be taken or command line argument + modifications to make just before calling SMACK. + """ + assert len(tasks) == 1 + assert propertyfile is not None + prop = ['--svcomp-property', propertyfile] + return [executable] + options + prop + tasks + + def determine_result(self, returncode, returnsignal, output, isTimeout): + """ + Returns a BenchExec result status based on the output of SMACK + """ + splitout = "\n".join(output) + if 'SMACK found no errors' in splitout: + return result.RESULT_TRUE_PROP + errmsg = re.search(r'SMACK found an error(:\s+([^\.]+))?\.', splitout) + if errmsg: + errtype = errmsg.group(2) + if errtype: + if 'invalid pointer dereference' == errtype: + return result.RESULT_FALSE_DEREF + elif 'invalid memory deallocation' == errtype: + return result.RESULT_FALSE_FREE + elif 'memory leak' == errtype: + return result.RESULT_FALSE_MEMTRACK + elif 'signed integer overflow' == errtype: + return result.RESULT_FALSE_OVERFLOW + else: + return result.RESULT_FALSE_REACH + return result.RESULT_UNKNOWN + + def get_value_from_output(self, lines, identifier): + """ + This function can be referenced in the input xml files (which can define + additional columns to be displayed in the output tables), and extracts + additional information from tool output (with the idea that extra + statistical information would be extracted from tool output, and included + as a column in the resulting output tables). + + We are using this to generate HTML links for output files, rather than + parsing output and providing additional statistical data about the run. + + This currently generates a drop-down menu item for the .bc, .bpl, + generated witness file, and the output from the witness checking tool. + + However, the witness file and checking links are hidden by default, as + they will not exist if the witness checking pass has not been performed, + or if the benchmark result was true (in which case there is no trace). + The visibility of these must be set to visible when witness checking is + performed for this execution. + """ + #identifier comes from pattern field of input xml node, + # which then has variable substitution performed on it first + #If identifier is the input source file path+name, this will create + # links in the output table for bpl, bc, and witness related files + ret = "" + ret += '
\n' + ret += ' \n' + ret += '
\n' + return ret diff --git a/svcomp/bench/src/checkWitnesses.py b/svcomp/bench/src/checkWitnesses.py index 802e9ff47..8e764bad4 100755 --- a/svcomp/bench/src/checkWitnesses.py +++ b/svcomp/bench/src/checkWitnesses.py @@ -33,46 +33,76 @@ print("\t\texecution result set, on which to check witnesses") exit() +#execDir is folder containing this script, checkWitnesses.py execDir = os.getcwd() +#targetDir is the run results folder we are trying to witness check +#(example data/runs/exec_2016.10.25._12.04.41.554365_WCTest) targetDir = sys.argv[1] +#Append results folder to targetDir +#(example data/runs/exec_2016.10.25._12.04.41.554365_WCTest/results) targetDir = os.path.join(targetDir, 'results') +#get a list of all results.xml files for this run outXmls = glob.glob(targetDir + '/*results*.xml') for outXml in outXmls: + #The last token when splitting by "." is the set name + #example file = svcomp_m32_witcheck.2016-10-25_1204.results.WCTest-WCTestDescription.WCTest.txt + #The last field here (WCTest) is the set name (coming from the file WCTest.set) + #The second to last field name is the set name + description, separated by a - baseXml,setName = os.path.splitext(os.path.splitext(outXml)[0]) + # skip certain sets + if 'DeviceDriversLinux64' in setName or 'HeapReach' in setName or 'Concurrency' in setName: + exit() + #outXmlNew will be the new output xml file with the witnesschecked results, + #leaveing the original file intact. outXmlNew = baseXml + '.witchecked' + setName + '.xml' tree = ET.parse(outXml) root = tree.getroot() + #runName is the setname + description (WCTest-WCTestDescription) runName = root.get('name') + #benchmarkname is the name of the input xml file, minus the extension + #example = svcomp_m32_witcheck benchmarkName = root.get('benchmarkname') runDate = root.get('date') runDate = time.strptime(runDate, "%Y-%m-%d %H:%M:%S %Z") + #Reformatted runDate example = 2016-10-25_1204 runDate = "{0:04d}-{1:02d}-{2:02d}_{3:02d}{4:02d}".format(runDate.tm_year, runDate.tm_mon, runDate.tm_mday, runDate.tm_hour, runDate.tm_min) runTimelimit = root.get('timelimit') - witTimelimit = int(runTimelimit.split()[0])/10 + #witness checking timelimit should be 10% of time limit for tool to solve + witTimelimit = int(runTimelimit.split()[0].replace("s",""))/10 + #pathPrefix example = svcomp_m32_witcheck.2016-10-25_1204 pathPrefix = benchmarkName + "." + runDate + #logFolder example = + #../data/runs/exec_2016.10.25_12.04.41.554365_WCTest/results/svcomp_m32_witcheck.2016-10-25_1204.logfiles/ logFolder = os.path.join(targetDir, pathPrefix + ".logfiles") - fileRoot = os.path.join(logFolder, runName) + #Loop through each benchmark file in the run for run in root.findall('run'): + #sourcefile is input *.c or *.i file (including path) sourcefile = run.get('name') # Get property file from input benchmark folder - propfile = os.path.join(os.path.join('data', os.path.split(sourcefile)[0]), 'ALL.prp') - # Now set sourcefile to where it WOULD be in output folders, - # given the folder structure of the actual input folder - tokenizedInputFile = os.path.join('data', sourcefile) - print(tokenizedInputFile) - sourcefile = os.path.join(fileRoot,sourcefile) - basefile = os.path.splitext(sourcefile)[0] + propfile = os.path.join(os.path.join('data', os.path.split(os.path.split(sourcefile)[0])[0]), 'PropertyUnreachCall.prp') + #split the sourcefile into its svcomp source path, and the actual filename + #(that is, get rid of the original source path) + _,targetfile = os.path.split(sourcefile) + targetfile = os.path.join(logFolder, runName + "." + targetfile) - witnessfile = sourcefile + '.witness.graphml' - witnesscheckOutput = sourcefile + '.witnessCheckOutput' + #Get the input and output witness checking file names + witnessfile = targetfile + '.witness.graphml' + #benchexecWitnesscheckOutput will be the console output of whatever witness checking + #tool gets executed (currently the cpachecker web validator). This file will contain + #the running time for the cpachecker web validator. + benchexecWitnesscheckOutput = targetfile + '.witnessCheckOutput' + #webValidatorWitnesscheckOutput will be the log file written by the cpachecker web + #validator. This file will contain the witness checking outcome, such as FALSE, TRUE, + # or TIMEOUT + webValidatorWitnesscheckOutput = targetfile + 'output.log' categoryCol = run.find('./column[@title="category"]') statusCol = run.find('./column[@title="status"]') outputfilesCol = run.find('./column[@title="Output Files"]') @@ -82,40 +112,89 @@ status = statusCol.get('value') # We only need to witness check if we got the answer right # and the verification result was false - if 'correct' in category and 'false' in status: + #if 'correct' in category and 'false' in status: + correct = None + if 'false' in status: + correct = False + elif 'true' in status: + correct = True + if correct is not None and os.path.isfile(witnessfile): # Use runexec to enforce time limit # cpachecker complains if working directory isn't the cpachecker # directory, so we have to adjust paths to match this requirement - cmd = ['../benchexec/bin/runexec'] - cmd += ['--output', '../' + witnesscheckOutput] + cmd = ['../../benchexec/bin/runexec'] + cmd += ['--output', '../../' + benchexecWitnesscheckOutput] + #cmd += ['--output', benchexecWitnesscheckOutput] + #cmd = ['./benchexec/bin/runexec'] + #cmd += ['--output', benchexecWitnesscheckOutput] cmd += ['--timelimit', str(witTimelimit)] cmd += ['--'] # Below this point are the witness checking commands cmd += ['./scripts/cpa.sh'] - cmd += ['-noout'] - cmd += ['-heap', '16000M'] - cmd += ['-spec', '../' + witnessfile] - cmd += ['-spec', '../' + propfile] - cmd += ['../' + tokenizedInputFile] - os.chdir('cpachecker') + ##### Simple CPAchecker Args + if correct: + cmd += ['-correctness-witness-validation'] + cmd += ['-setprop', 'invariantGeneration.kInduction.invariantsAutomatonFile='+os.path.abspath(witnessfile)] + else: + cmd += ['-violation-witness-validation'] + cmd += ['-spec', os.path.abspath(witnessfile)] + cmd += ['-spec', os.path.abspath(propfile)] + cmd += [os.path.abspath('data/' + sourcefile)] + cmd += ['-outputpath', os.path.abspath( targetfile)] + + ##### Complex CPAchecker Args + #cmd += ['-noout'] + #cmd += ['-heap', '16000M'] + #cmd += ['-witness-check'] + #cmd += ['-spec', '../' + witnessfile] + #cmd += ['-spec', '../' + propfile] + #cmd += ['../' + sourcefile] + #os.chdir('cpachecker/CPAchecker-1.6.1-unix') + os.chdir('cpachecker/cpachecker') + + #cmd += ['./witness_validation_web_cloud.py'] + #cmd += ['--program', "../data/" + sourcefile] + #cmd += ['--witness', "../" + witnessfile] + #cmd += ['-o', "../" + targetfile] p = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - cmdOut = p.communicate()[0] - checktime = float(re.search('cputime=(.*)s', cmdOut.decode('utf-8')).group(1)) + #This console output (p.communicate()[0]) is ignored, and is only called to + #block execution until the web validator finishes running. The console output + #here will contain the running time for the web validator script only, not the + #actual running time of the validation, so it gets ignored. + cmdOut = p.communicate()[0] + #print(cmdOut.decode('utf-8')) + #checktime = float(re.search('cputime=(.*)s', cmdOut.decode('utf-8')).group(1)) os.chdir(execDir) + #cmdOut = "" + with open(benchexecWitnesscheckOutput,"r") as f: + output = f.read() + print(cmdOut) + checktime = float(re.search('cputime=(.*)s', cmdOut).group(1)) + 10 + witSuccess = False witTimeout = False - with open(witnesscheckOutput, 'r') as witout: - output = witout.read() - witSuccess = re.search('Verification result:\s*FALSE', output) - witTimeout = re.search('EDIT THIS WHEN YOU KNOW TIMEOUT STRING', output) + #with open(webValidatorWitnesscheckOutput, 'r') as witout: + # output = witout.read() + witSuccess = re.search('Verification result:\s*FALSE', output) if not correct else re.search('Verification result: TRUE.*', output) + witTimeout = re.search('Verification result: UNKNOWN, incomplete analysis.', output) + witFailure = re.search('Verification result: TRUE.*', output) if not correct else re.search('Verification result:\s*FALSE', output) if witSuccess: statusCol.set('value','witness confirmed') else: - statusCol.set('value', 'something went wrong') + if witTimeout: + statusCol.set('value', 'witness timeout') + categoryCol.set('value', 'error') + else: + if witFailure: + statusCol.set('value', 'witness unconfirmed') + categoryCol.set('value', 'error') + else: + statusCol.set('value', 'something went wrong') + categoryCol.set('value', 'unknown') if outputfilesCol is not None: newVal = outputfilesCol.get('value').replace(' hidden','') outputfilesCol.set('value', newVal) ET.SubElement(run, 'column', {'title':'time(s)\nfor\nwitness', 'value':"{0:.3f}s".format(checktime)}) - tree.write(outXmlNew) + tree.write(outXmlNew) diff --git a/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck.xml b/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck.xml index 76c1dae31..5e164d0e8 100644 --- a/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck.xml +++ b/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck.xml @@ -1,28 +1,31 @@ - + - ${sourcefile_path}/ALL.prp + + {PROPERTYDEFINITIONFILE} - + + + + + - ../sv-benchmarks/{SETNAME}.set + {SETDEFINITIONFILE} - - - - - - + + - ${logfile_path}/${rundefinition_name}/${sourcefile_path}/${sourcefile_name} + ${logfile_path}/${rundefinition_name}.${sourcefile_name} diff --git a/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck_packaged.xml b/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck_packaged.xml new file mode 100644 index 000000000..3c9d3bedf --- /dev/null +++ b/svcomp/bench/src/inputXMLFiles/svcomp_m32_witcheck_packaged.xml @@ -0,0 +1,31 @@ + + + + + + {PROPERTYDEFINITIONFILE} + + + + + + + + + + {SETDEFINITIONFILE} + + + + + + + + ${logfile_path}/${rundefinition_name}.${sourcefile_name} + + diff --git a/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck.xml b/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck.xml index 9e49bd591..3ad791069 100644 --- a/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck.xml +++ b/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck.xml @@ -1,28 +1,31 @@ - + - ${sourcefile_path}/ALL.prp + + {PROPERTYDEFINITIONFILE} - + + + + + - ../sv-benchmarks/{SETNAME}.set + {SETDEFINITIONFILE} - - - - - - + + - ${logfile_path}/${rundefinition_name}/${sourcefile_path}/${sourcefile_name} + ${logfile_path}/${rundefinition_name}.${sourcefile_name} diff --git a/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck_packaged.xml b/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck_packaged.xml new file mode 100644 index 000000000..e00248292 --- /dev/null +++ b/svcomp/bench/src/inputXMLFiles/svcomp_m64_witcheck_packaged.xml @@ -0,0 +1,31 @@ + + + + + + {PROPERTYDEFINITIONFILE} + + + + + + + + + + {SETDEFINITIONFILE} + + + + + + + + ${logfile_path}/${rundefinition_name}.${sourcefile_name} + + diff --git a/svcomp/bench/src/queueStdBuiltNew b/svcomp/bench/src/queueStdBuiltNew new file mode 100644 index 000000000..751152a31 --- /dev/null +++ b/svcomp/bench/src/queueStdBuiltNew @@ -0,0 +1,23 @@ +ArraysMemSafety inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +ArraysReach inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +BitVectorsOverflows inputFiles/inputXMLFiles/svcomp_m64_witcheck.xml +BitVectorsReach inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +BusyBox inputFiles/inputXMLFiles/svcomp_m64_witcheck.xml +ControlFlow inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Floats inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +HeapMemSafety inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +HeapReach inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Loops inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +ProductLines inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Recursive inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Sequentialized inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Concurrency inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +DeviceDriversLinux64 inputFiles/inputXMLFiles/svcomp_m64_witcheck.xml +ECA inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +MemSafety-Other inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +MemSafety-LinkedLists inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Overflows-Other inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml +Systems_BusyBox_Overflows inputFiles/inputXMLFiles/svcomp_m64_witcheck.xml +Termination-MainControlFlow inputFiles/inputXMLFiles/svcomp_m64_witcheck.xml +Termination-MainHeap inputFiles/inputXMLFiles/svcomp_m64_witcheck.xml +Termination-Other inputFiles/inputXMLFiles/svcomp_m32_witcheck.xml diff --git a/svcomp/bench/src/queueStdPackagedNew b/svcomp/bench/src/queueStdPackagedNew new file mode 100644 index 000000000..c90b8cc6e --- /dev/null +++ b/svcomp/bench/src/queueStdPackagedNew @@ -0,0 +1,23 @@ +ArraysMemSafety inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +ArraysReach inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +BitVectorsReach inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +BitVectorsOverflows inputFiles/inputXMLFiles/svcomp_m64_witcheck_packaged.xml +BusyBox inputFiles/inputXMLFiles/svcomp_m64_witcheck_packaged.xml +ControlFlow inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Floats inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +HeapMemSafety inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +HeapReach inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Loops inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Recursive inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Sequentialized inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +ProductLines inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Concurrency inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +DeviceDriversLinux64 inputFiles/inputXMLFiles/svcomp_m64_witcheck_packaged.xml +ECA inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +MemSafety-Other inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +MemSafety-LinkedLists inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Overflows-Other inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml +Systems_BusyBox_Overflows inputFiles/inputXMLFiles/svcomp_m64_witcheck_packaged.xml +Termination-MainControlFlow inputFiles/inputXMLFiles/svcomp_m64_witcheck_packaged.xml +Termination-MainHeap inputFiles/inputXMLFiles/svcomp_m64_witcheck_packaged.xml +Termination-Other inputFiles/inputXMLFiles/svcomp_m32_witcheck_packaged.xml diff --git a/svcomp/emulabSetup/smackbench_compute_common_buildscript.sh b/svcomp/emulabSetup/smackbench_compute_common_buildscript.sh new file mode 100644 index 000000000..41a5672e1 --- /dev/null +++ b/svcomp/emulabSetup/smackbench_compute_common_buildscript.sh @@ -0,0 +1,42 @@ +#!/bin/bash + +#Set permissions on local ephemeral storage, +#so sudo is not needed +sudo chgrp SMACK /mnt/local +sudo chmod g+w /mnt/local + +#Change apt-get mirror to local cs.utah.edu mirror (makes it much faster) +sudo sed -i "s|us.archive.ubuntu.com/ubuntu/|ubuntu.cs.utah.edu/ubuntu/|g" /etc/apt/sources.list + +#Install packages +sudo apt-get update +# Packages: +# htop - interactive convenience +# vim - interactive convenience +# cgroup-bin - benchexec (cgroups) +# cgroup-lite - benchexec (cgroups) +# cgmanager - benchexec (cgroups) +# software-properties-common - SMACK buildscript +# python-daemon - SMACKBench Server +# openjdk-7-jre - cpachecker witness checker +sudo apt-get install htop vim cgroup-bin cgroup-lite cgmanager software-properties-common python-daemon libc6-dev-i386 -y + +#Install java8 (required by cpachecker) +sudo add-apt-repository ppa:openjdk-r/ppa -y +sudo apt-get update -y +sudo apt-get install openjdk-8-jdk -y +echo 2 | sudo update-alternatives --config java + +#Upgrade kernel +sudo apt-get install --install-recommends linux-generic-lts-vivid -y + +#And all packages (except grub, because it requires interactive after kernel upgrade) +sudo apt-mark hold grub-common grub-pc grub-pc-bin grub2-common +sudo apt-get upgrade -y +sudo apt-get upgrade -y + +#Enable tracking of memory swapping for processes (requires reboot) +sudo sed -i '/GRUB_CMDLINE_LINUX=/ s/^\(.*\)\("\)/\1 swapaccount=1\2/' /etc/default/grub +sudo update-grub + +#Calling script must reboot after it finishes its portion! diff --git a/svcomp/emulabSetup/smackbench_compute_packaged_buildscript.sh b/svcomp/emulabSetup/smackbench_compute_packaged_buildscript.sh new file mode 100755 index 000000000..6347ec145 --- /dev/null +++ b/svcomp/emulabSetup/smackbench_compute_packaged_buildscript.sh @@ -0,0 +1,16 @@ +#!/bin/bash + +#Call common buildscript +sh /proj/SMACK/scripts/smackbench_compute_common_buildscript.sh + +#Install mono (needed by packaged SMACK) +sudo apt-get install mono-complete -y + +#Set up boot script to start on reboot +sudo bash -c "echo -e \"su -c '. /mnt/local/smack-project/smack.environment && cd /proj/SMACK/SMACKBenchResults && ./runServer.sh' mcarter &\" >> /etc/rc.local" + +#Copy console log of this script off ephemeral storage +cp /tmp/smackbench_compute_build.out /mnt/local/ + +#Reboot +sudo reboot now diff --git a/svcomp/emulabSetup/smackbench_compute_repo_buildscript.sh b/svcomp/emulabSetup/smackbench_compute_repo_buildscript.sh new file mode 100755 index 000000000..7b730e8fb --- /dev/null +++ b/svcomp/emulabSetup/smackbench_compute_repo_buildscript.sh @@ -0,0 +1,33 @@ +#!/bin/bash + +#Call common buildscript +sh /proj/SMACK/scripts/smackbench_compute_common_buildscript.sh + +export DEBIAN_FRONTEND=noninteractive + +#Create directory for smack, clone smack, +#checkout develop and enter dir +mkdir -p /mnt/local/smack-project +cd /mnt/local/smack-project +git clone https://github.com/smackers/smack.git +cd smack/bin +#git checkout svcomp2016 +git checkout develop +#git checkout llvm-3.7 +#git checkout svcomp2017 +#git checkout avoid-mem-safety-region-collapse + +#Build SMACK (using 64 processors during call to make) +sed -i 's/^ make$/ make -j 64/g' build.sh +sed -i 's/^ sudo make install$/ sudo make install -j 64/g' build.sh +./build.sh + +#Set up boot script to start on reboot +#sudo bash -c "echo -e \"su -c '. /mnt/local/smack-project/smack.environment && cd /proj/SMACK/SMACKBenchResults && ./runServer.sh' mcarter &\" >> /etc/rc.local" + +#Copy console log of this script off ephemeral storage +cp /tmp/smackbench_compute_build.out /mnt/local/ + +#Reboot +sudo reboot now + diff --git a/test/config.yml b/test/config.yml index 875772f60..9a11baab8 100644 --- a/test/config.yml +++ b/test/config.yml @@ -1,4 +1,4 @@ -verifiers: [boogie, corral] +verifiers: [corral, boogie] memory: [no-reuse-impls, no-reuse, reuse] time-limit: 120 memory-limit: 450 diff --git a/test/contracts/array_forall.c b/test/contracts/array_forall.c index b6bcc7417..f1d63eefc 100644 --- a/test/contracts/array_forall.c +++ b/test/contracts/array_forall.c @@ -4,15 +4,16 @@ #include // @expect verified +// @flag --verifier-options=/z3opt:SMT.MBQI=true #define SIZE 10 int g[SIZE]; void p() { - ensures(forall("i", qvar("i") < 0 || qvar("i") >= SIZE || g[qvar("i")] == qvar("i"))); + ensures(forall("i", qvar("i", int) < 0 || qvar("i", int) >= SIZE || g[qvar("i", int)] == qvar("i", int))); for (int i=0; i= i || g[qvar("x")] == qvar("x"))); + invariant(forall("x", qvar("x", int) < 0 || qvar("x", int) >= i || g[qvar("x", int)] == qvar("x", int))); g[i] = i; } } diff --git a/test/contracts/array_forall_fail.c b/test/contracts/array_forall_fail.c deleted file mode 100644 index 13b1311aa..000000000 --- a/test/contracts/array_forall_fail.c +++ /dev/null @@ -1,18 +0,0 @@ -#include -#include -#include -#include - -// @expect error - -#define SIZE 10 -int g[SIZE]; - -void p() { - ensures(forall("i", qvar("i") < 0 || qvar("i") >= SIZE || g[qvar("i")] == qvar("i"))); - - for (int i=0; i i || g[qvar("x")] == qvar("x"))); - g[i] = i; - } -} diff --git a/test/contracts/config.yml b/test/contracts/config.yml index f28fd5927..371879ceb 100644 --- a/test/contracts/config.yml +++ b/test/contracts/config.yml @@ -1,3 +1,2 @@ verifiers: [boogie] -memory: [no-reuse] -skip: true +flags: [--modular] diff --git a/test/contracts/failing/array_forall_fail.c b/test/contracts/failing/array_forall_fail.c new file mode 100644 index 000000000..6f5ab1e2e --- /dev/null +++ b/test/contracts/failing/array_forall_fail.c @@ -0,0 +1,19 @@ +#include +#include +#include +#include + +// @expect error +// @flag --verifier-options=/z3opt:SMT.MBQI=true + +#define SIZE 10 +int g[SIZE]; + +void p() { + ensures(forall("i", qvar("i", int) < 0 || qvar("i", int) >= SIZE || g[qvar("i", int)] == qvar("i", int))); + + for (int i=0; i i || g[qvar("x", int)] == qvar("x", int))); + g[i] = i; + } +} diff --git a/test/contracts/failing/old.c b/test/contracts/failing/old.c index 5ad4f02d7..278b6ab3c 100644 --- a/test/contracts/failing/old.c +++ b/test/contracts/failing/old.c @@ -1,8 +1,9 @@ #include #include -#include "smack.h" +#include +#include -// @expect 2 verified, 0 errors? +// @expect verified int g; @@ -14,4 +15,4 @@ void p() { int main(void) { p(); return 0; -} \ No newline at end of file +} diff --git a/test/contracts/failing/old_fail.c b/test/contracts/failing/old_fail.c index b81e7fd05..7f8a6e0e4 100644 --- a/test/contracts/failing/old_fail.c +++ b/test/contracts/failing/old_fail.c @@ -1,8 +1,9 @@ #include #include -#include "smack.h" +#include +#include -// @expect 1 verified, 1 errors? +// @expect error int g; @@ -14,4 +15,4 @@ void p() { int main(void) { p(); return 0; -} \ No newline at end of file +} diff --git a/test/contracts/result.c b/test/contracts/failing/result.c similarity index 100% rename from test/contracts/result.c rename to test/contracts/failing/result.c diff --git a/test/contracts/result_fail.c b/test/contracts/failing/result_fail.c similarity index 100% rename from test/contracts/result_fail.c rename to test/contracts/failing/result_fail.c diff --git a/test/contracts/forall.c b/test/contracts/forall.c index f52071f13..dc483843f 100644 --- a/test/contracts/forall.c +++ b/test/contracts/forall.c @@ -8,6 +8,6 @@ int g[10]; int main(void) { - ensures(forall("x", g[qvar("x")] == 0 || qvar("x") < 0 || qvar("x") > 9)); + ensures(forall("x", g[qvar("x", int)] == 0 || qvar("x", int) < 0 || qvar("x", int) > 9)); return 0; -} \ No newline at end of file +} diff --git a/test/contracts/forall_fail.c b/test/contracts/forall_fail.c index ec69109c4..ad2b40fb6 100644 --- a/test/contracts/forall_fail.c +++ b/test/contracts/forall_fail.c @@ -8,6 +8,6 @@ int g[10]; int main(void) { - ensures(forall("x", g[qvar("x")] == 0 || qvar("x") < 0 || qvar("x") > 10)); + ensures(forall("x", g[qvar("x", int)] == 0 || qvar("x", int) < 0 || qvar("x", int) > 10)); return 0; -} \ No newline at end of file +} diff --git a/test/contracts/failing/requires_const.c b/test/contracts/requires_const.c similarity index 51% rename from test/contracts/failing/requires_const.c rename to test/contracts/requires_const.c index 7796de1ce..f61c03926 100644 --- a/test/contracts/failing/requires_const.c +++ b/test/contracts/requires_const.c @@ -1,8 +1,9 @@ #include #include -#include "smack.h" +#include +#include -// @expect 1 verified, 0 errors? +// @expect verified void p() { requires(true); diff --git a/test/memory-safety/config.yml b/test/memory-safety/config.yml index 47037e75f..778f5ee6c 100644 --- a/test/memory-safety/config.yml +++ b/test/memory-safety/config.yml @@ -1 +1,2 @@ flags: [--memory-safety] +time-limit: 180 diff --git a/test/pthread_extras/config.yml b/test/pthread_extras/config.yml index a04b697fe..5adc340a1 100644 --- a/test/pthread_extras/config.yml +++ b/test/pthread_extras/config.yml @@ -1,5 +1,5 @@ verifiers: [corral] memory: [no-reuse-impls] -time-limit: 600 +time-limit: 800 flags: [--pthread, --context-bound=2] skip: ok diff --git a/test/regtest.py b/test/regtest.py index 29240c431..70176ade6 100755 --- a/test/regtest.py +++ b/test/regtest.py @@ -151,6 +151,8 @@ def main(): parser.add_argument("--exhaustive", help="check all configurations on all examples", action="store_true") parser.add_argument("--all-configs", help="check all configurations per example", action="store_true") parser.add_argument("--all-examples", help="check all examples", action="store_true") + parser.add_argument("--folder", action="store", default="**", type=str, + help="sets the regressions folder to run") parser.add_argument("--threads", action="store", dest="n_threads", default=num_cpus, type=int, help="execute regressions using the selected number of threads in parallel") parser.add_argument("--log", action="store", dest="log_level", default="DEBUG", type=str, @@ -189,7 +191,7 @@ def main(): # start processing the tests. results = [] - for test in sorted(glob.glob("./**/*.c")): + for test in sorted(glob.glob("./" + args.folder + "/*.c")): # get the meta data for this test meta = metadata(test) @@ -246,7 +248,7 @@ def main(): # if there are any failed tests or tests that timed out, set the system # exit code to a failure status - if timeouts > 0 or failed > 0: + if timeouts > 0 or failed > 0 or unknowns > 0: sys.exit(1) if __name__=="__main__": diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 09af791aa..2eb5dad5a 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -20,7 +20,6 @@ #include "llvm/Support/FormattedStream.h" #include "smack/BplFilePrinter.h" -#include "smack/DSAAliasAnalysis.h" #include "smack/SmackModuleGenerator.h" #include "assistDS/StructReturnToPointer.h" #include "assistDS/SimplifyExtractValue.h" @@ -58,6 +57,10 @@ static llvm::cl::opt SignedIntegerOverflow("signed-integer-overflow", llvm::cl::desc("Enable signed integer overflow checks"), llvm::cl::init(false)); +static llvm::cl::opt +Modular("modular", llvm::cl::desc("Enable contracts-based modular deductive verification"), + llvm::cl::init(false)); + std::string filenamePrefix(const std::string &str) { return str.substr(0, str.find_last_of(".")); } @@ -123,7 +126,9 @@ int main(int argc, char **argv) { pass_manager.add(new smack::ExtractContracts()); pass_manager.add(llvm::createDeadCodeEliminationPass()); pass_manager.add(new smack::CodifyStaticInits()); - pass_manager.add(new smack::RemoveDeadDefs()); + if (!Modular) { + pass_manager.add(new smack::RemoveDeadDefs()); + } pass_manager.add(new llvm::MergeArrayGEP()); // pass_manager.add(new smack::SimplifyLibCalls()); pass_manager.add(new llvm::Devirtualize());