diff --git a/.travis.yml b/.travis.yml index 09bf8b6a0..9d473ab70 100644 --- a/.travis.yml +++ b/.travis.yml @@ -9,7 +9,6 @@ env: 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" @@ -19,19 +18,21 @@ env: 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 add-apt-repository "deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.9 main" + - wget -O - http://apt.llvm.org/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 + - sudo apt-get install -y clang-3.9 llvm-3.9 + - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.9 20 + - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.9 20 + - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-3.9 20 + - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-3.9 20 + - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-3.9 20 + - sudo pip install pyyaml psutil script: + - python --version - $CXX --version - $CC --version - clang --version diff --git a/CMakeLists.txt b/CMakeLists.txt index a8c47394f..aeec6ef7c 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-3.8 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") + find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-3.9 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,8 +18,13 @@ if (NOT WIN32 OR MSYS OR CYGWIN) OUTPUT_STRIP_TRAILING_WHITESPACE ) + string(REPLACE "-DNDEBUG" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}") + string(REPLACE "-Wno-maybe-uninitialized" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}") + string(REPLACE "-fuse-ld=gold" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}") + string(REPLACE "-Wl," "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}") + string(REPLACE "-gsplit-dwarf" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}") 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 "${CMAKE_CXX_FLAGS} -fno-exceptions -fno-rtti -Wno-undefined-var-template") set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0") set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0") @@ -151,6 +156,7 @@ add_library(dsa STATIC ) add_library(smackTranslator STATIC + include/smack/AddTiming.h include/smack/BoogieAst.h include/smack/BplFilePrinter.h include/smack/BplPrinter.h @@ -163,13 +169,17 @@ add_library(smackTranslator STATIC include/smack/CodifyStaticInits.h include/smack/RemoveDeadDefs.h include/smack/ExtractContracts.h + include/smack/VerifierCodeMetadata.h include/smack/SimplifyLibCalls.h include/smack/SmackRep.h include/smack/MemorySafetyChecker.h include/smack/SignedIntegerOverflowChecker.h + include/smack/SplitAggregateLoadStore.h + lib/smack/AddTiming.cpp lib/smack/BoogieAst.cpp lib/smack/BplFilePrinter.cpp lib/smack/BplPrinter.cpp + lib/smack/Debug.cpp lib/smack/DSAWrapper.cpp lib/smack/Naming.cpp lib/smack/Regions.cpp @@ -179,10 +189,12 @@ add_library(smackTranslator STATIC lib/smack/CodifyStaticInits.cpp lib/smack/RemoveDeadDefs.cpp lib/smack/ExtractContracts.cpp + lib/smack/VerifierCodeMetadata.cpp lib/smack/SimplifyLibCalls.cpp lib/smack/SmackRep.cpp lib/smack/MemorySafetyChecker.cpp lib/smack/SignedIntegerOverflowChecker.cpp + lib/smack/SplitAggregateLoadStore.cpp ) add_executable(llvm2bpl diff --git a/Doxyfile b/Doxyfile index d8269fce0..20d5ae219 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 1.8.1 +PROJECT_NUMBER = 1.9.0 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/bin/build.sh b/bin/build.sh index 2eb6c2ebf..e5f2b840c 100755 --- a/bin/build.sh +++ b/bin/build.sh @@ -53,6 +53,8 @@ CMAKE_INSTALL_PREFIX= # Partial list of dependnecies; the rest are added depending on the platform DEPENDENCIES="git cmake python-yaml python-psutil unzip wget" +shopt -s extglob + ################################################################################ # # A FEW HELPER FUNCTIONS @@ -155,18 +157,18 @@ puts "Detected distribution: $distro" # Set platform-dependent flags case "$distro" in linux-opensuse*) - Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-debian-8.2.zip" + Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-debian-8.2.zip" DEPENDENCIES+=" llvm-clang llvm-devel gcc-c++ mono-complete make" DEPENDENCIES+=" ncurses-devel zlib-devel" ;; -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.8 llvm-3.8 mono-complete libz-dev libedit-dev" +linux-@(ubuntu|neon)-1[46]*) + Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip" + DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION} mono-complete libz-dev libedit-dev" ;; linux-ubuntu-12*) - Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip" + Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-14.04.zip" DEPENDENCIES+=" g++-4.8 autoconf automake bison flex libtool gettext gdb" DEPENDENCIES+=" libglib2.0-dev libfontconfig1-dev libfreetype6-dev libxrender-dev" DEPENDENCIES+=" libtiff-dev libjpeg-dev libgif-dev libpng-dev libcairo2-dev" @@ -221,21 +223,36 @@ then sudo zypper --non-interactive install ${DEPENDENCIES} ;; - linux-ubuntu-1[46]*) + linux-@(ubuntu|neon)-1[46]*) + RELEASE_VERSION=$(get-platform-trim "$(lsb_release -r)" | awk -F: '{print $2;}') + UBUNTU_CODENAME="trusty" + case "$RELEASE_VERSION" in + 14*) + UBUNTU_CODENAME="trusty" + ;; + 16*) + UBUNTU_CODENAME="xenial" + ;; + *) + puts "Release ${RELEASE_VERSION} for ${distro} not supported. Dependencies must be installed manually." + exit 1 + ;; + esac + # Adding LLVM repository - 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 - + sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main" + ${WGET} -O - http://apt.llvm.org/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" sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF # 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.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 + sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30 + sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 30 + sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 30 + sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 30 + sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 30 ;; linux-ubuntu-12*) @@ -299,13 +316,13 @@ then mkdir -p ${LLVM_DIR}/src/{tools/clang,projects/compiler-rt} mkdir -p ${LLVM_DIR}/build - ${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 + ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/llvm-${LLVM_FULL_VERSION}.src.tar.xz + ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/cfe-${LLVM_FULL_VERSION}.src.tar.xz + ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz - 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 + tar -C ${LLVM_DIR}/src -xvf llvm-${LLVM_FULL_VERSION}.src.tar.xz --strip 1 + tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-${LLVM_FULL_VERSION}.src.tar.xz --strip 1 + tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz --strip 1 cd ${LLVM_DIR}/build/ cmake -G "Unix Makefiles" ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Release ../src @@ -322,7 +339,7 @@ then ${WGET} ${Z3_DOWNLOAD_LINK} -O z3-downloaded.zip unzip -o z3-downloaded.zip -d z3-extracted - mv z3-extracted/z3-* ${Z3_DIR} + mv -f --backup=numbered z3-extracted/z3-* ${Z3_DIR} rm -rf z3-downloaded.zip z3-extracted puts "Installed Z3" @@ -333,15 +350,17 @@ if [ ${BUILD_BOOGIE} -eq 1 ] then puts "Building Boogie" - git clone https://github.com/boogie-org/boogie.git ${BOOGIE_DIR} + if [ ! -d "$BOOGIE_DIR" ] ; then + git clone https://github.com/boogie-org/boogie.git ${BOOGIE_DIR} + fi cd ${BOOGIE_DIR} git reset --hard ${BOOGIE_COMMIT} cd ${BOOGIE_DIR}/Source - ${WGET} https://nuget.org/nuget.exe + ${WGET} https://dist.nuget.org/win-x86-commandline/latest/nuget.exe mono ./nuget.exe restore Boogie.sln rm -rf /tmp/nuget/ msbuild Boogie.sln /p:Configuration=Release - ln -s ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe + ln -sf ${Z3_DIR}/bin/z3 ${BOOGIE_DIR}/Binaries/z3.exe puts "Built Boogie" fi @@ -351,13 +370,15 @@ if [ ${BUILD_CORRAL} -eq 1 ] then puts "Building Corral" - git clone https://github.com/boogie-org/corral.git ${CORRAL_DIR} + if [ ! -d "$CORRAL_DIR" ] ; then + git clone https://github.com/boogie-org/corral.git ${CORRAL_DIR} + fi cd ${CORRAL_DIR} git reset --hard ${CORRAL_COMMIT} git submodule init git submodule update msbuild cba.sln /p:Configuration=Release - ln -s ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe + ln -sf ${Z3_DIR}/bin/z3 ${CORRAL_DIR}/bin/Release/z3.exe puts "Built Corral" fi @@ -367,11 +388,13 @@ then puts "Building lockpwn" cd ${ROOT} - git clone https://github.com/smackers/lockpwn.git + if [ ! -d "$LOCKPWN_DIR" ] ; then + git clone https://github.com/smackers/lockpwn.git + fi cd ${LOCKPWN_DIR} git reset --hard ${LOCKPWN_COMMIT} msbuild lockpwn.sln /p:Configuration=Release - ln -s ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe + ln -sf ${Z3_DIR}/bin/z3 ${LOCKPWN_DIR}/Binaries/z3.exe puts "Built lockpwn" fi diff --git a/bin/package-smack.sh b/bin/package-smack.sh deleted file mode 100755 index 4ff2def67..000000000 --- a/bin/package-smack.sh +++ /dev/null @@ -1,44 +0,0 @@ -#!/bin/bash -# -# This file is distributed under the MIT License. See LICENSE for details. -# - -# Note: this script requires CDE to be downloaded from -# http://www.pgbovine.net/cde.html - -VERSION=1.8.1 -PACKAGE=smack-$VERSION-64 - -# Create folder to export -mkdir $PACKAGE -cd $PACKAGE - -# Create file to verify -echo int main\(void\) \{ >> test.c -echo int a\; >> test.c -echo a = 2\; >> test.c -echo if \(a != 3\) __VERIFIER_error\(\)\; >> test.c -echo return 0\; >> test.c -echo \} >> test.c - -# Run SMACK with CDE -../cde_2011-08-15_64bit smack test.c -x svcomp --verifier corral --clang-options=-m32 -../cde_2011-08-15_64bit smack test.c -x svcomp --verifier corral --clang-options=-m64 -../cde_2011-08-15_64bit smack test.c -x svcomp --verifier svcomp --clang-options=-m32 -../cde_2011-08-15_64bit smack test.c -x svcomp --verifier svcomp --clang-options=-m64 - -# Clean up temporary files -rm test.* cde.options - -# Copy license file -cp ../../LICENSE . - -# Create wrapper script -echo \#\!/bin/sh > smack.sh -echo HERE=\"\$\(dirname \"\$\(readlink -f \"\$\{0\}\"\)\"\)\" >> smack.sh -echo \$HERE/cde-package/cde-exec \'smack\' \'-x=svcomp\' \'--verifier=svcomp\' \'-q\' \"\$\@\" >> smack.sh -chmod u+x smack.sh - -# Package it up -cd .. -tar -cvzf $PACKAGE.tgz $PACKAGE diff --git a/bin/versions b/bin/versions index 7ae0508fb..7a2e11fcb 100644 --- a/bin/versions +++ b/bin/versions @@ -1,4 +1,7 @@ MONO_VERSION=5.0.0.100 -BOOGIE_COMMIT=4e4c3a5252 -CORRAL_COMMIT=6f6926e3bb +Z3_VERSION=4.5.0 +BOOGIE_COMMIT=c609ee2864 +CORRAL_COMMIT=b2738b4839 LOCKPWN_COMMIT=a4d802a1cb +LLVM_SHORT_VERSION=3.9 +LLVM_FULL_VERSION=3.9.1 diff --git a/docs/installation.md b/docs/installation.md index 6d3a471a9..98f9920f7 100644 --- a/docs/installation.md +++ b/docs/installation.md @@ -59,8 +59,8 @@ vagrant destroy SMACK depends on the following projects: -* [LLVM][] version [3.8.1][LLVM-3.8.1] -* [Clang][] version [3.8.1][Clang-3.8.1] +* [LLVM][] version [3.9.1][LLVM-3.9.1] +* [Clang][] version [3.9.1][Clang-3.9.1] * [Python][] version 2.7 or greater * [Mono][] version 5.0.0 or greater (except on Windows) * [Z3][] or compatible SMT-format theorem prover @@ -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.8.1]: http://llvm.org/releases/download.html#3.8.1 +[LLVM-3.9.1]: http://llvm.org/releases/download.html#3.9.1 [Clang]: http://clang.llvm.org -[Clang-3.8.1]: http://llvm.org/releases/download.html#3.8.1 +[Clang-3.9.1]: http://llvm.org/releases/download.html#3.9.1 [Boogie]: https://github.com/boogie-org/boogie [Corral]: https://corral.codeplex.com/ [Z3]: https://github.com/Z3Prover/z3/ diff --git a/docs/publications.md b/docs/publications.md index 964dc84b9..3012a042f 100644 --- a/docs/publications.md +++ b/docs/publications.md @@ -14,6 +14,11 @@ Zvonimir Rakamaric, Michael Emmi, This is an incomplete list of publications that use, leverage, or extend SMACK. If you have a publication for this list, please email [Zvonimir](mailto:zvonimir@cs.utah.edu). +1. [Refining Interprocedural Change-Impact Analysis using Equivalence Relations](https://www.microsoft.com/en-us/research/publication/refining-interprocedural-change-impact-analysis-using-equivalence-relations), +Alex Gyori, Shuvendu Lahiri, Nimrod Partush, +26th ACM SIGSOFT International Symposium on Software Testing and Analysis +(ISSTA 2017) + 1. [Verifying Constant-Time Implementations](https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida), Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi, 25th USENIX Security Symposium diff --git a/include/assistDS/DataStructureCallGraph.h b/include/assistDS/DataStructureCallGraph.h index 623564112..ed5dcf9bf 100644 --- a/include/assistDS/DataStructureCallGraph.h +++ b/include/assistDS/DataStructureCallGraph.h @@ -20,7 +20,6 @@ #include "llvm/IR/Module.h" #include "llvm/Analysis/CallGraph.h" -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" namespace llvm { diff --git a/include/dsa/DSGraphTraits.h b/include/dsa/DSGraphTraits.h index eb051bb27..e744c27e0 100644 --- a/include/dsa/DSGraphTraits.h +++ b/include/dsa/DSGraphTraits.h @@ -97,27 +97,6 @@ template <> struct GraphTraits { static ChildIteratorType child_end(NodeType *N) { return N->end(); } }; -static DSNode &dereference ( DSNode *N) { return *N; } - -template <> struct GraphTraits { - typedef DSNode NodeType; - typedef DSNode::iterator ChildIteratorType; - - typedef std::pointer_to_unary_function DerefFun; - - // nodes_iterator/begin/end - Allow iteration over all nodes in the graph - typedef mapped_iterator nodes_iterator; - static nodes_iterator nodes_begin(DSGraph *G) { - return map_iterator(G->node_begin(), DerefFun(dereference)); - } - static nodes_iterator nodes_end(DSGraph *G) { - return map_iterator(G->node_end(), DerefFun(dereference)); - } - - static ChildIteratorType child_begin(NodeType *N) { return N->begin(); } - static ChildIteratorType child_end(NodeType *N) { return N->end(); } -}; - template <> struct GraphTraits { typedef const DSNode NodeType; typedef DSNode::const_iterator ChildIteratorType; diff --git a/include/dsa/DSNode.h b/include/dsa/DSNode.h index 614d97a27..26a3138f9 100644 --- a/include/dsa/DSNode.h +++ b/include/dsa/DSNode.h @@ -17,12 +17,10 @@ #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/ilist_node.h" #include "llvm/ADT/ilist.h" -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include "dsa/svset.h" #include "dsa/super_set.h" #include "dsa/keyiterator.h" -#include "dsa/DSGraph.h" #include "dsa/DSSupport.h" #include diff --git a/include/dsa/TypeSafety.h b/include/dsa/TypeSafety.h index 653636c35..f018cf9f3 100644 --- a/include/dsa/TypeSafety.h +++ b/include/dsa/TypeSafety.h @@ -88,4 +88,3 @@ struct TypeSafety : public ModulePass { } #endif - diff --git a/include/smack/AddTiming.h b/include/smack/AddTiming.h new file mode 100644 index 000000000..87984bdec --- /dev/null +++ b/include/smack/AddTiming.h @@ -0,0 +1,52 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef ADDTIMING_H +#define ADDTIMING_H + +#include "llvm/Pass.h" +#include "llvm/IR/Instructions.h" + +namespace llvm { +class TargetTransformInfo; +} + +namespace smack { + using namespace llvm; + + class AddTiming : public FunctionPass { + + enum Flags { NO_TIMING_INFO = -1}; + static const std::string INT_TIMING_COST_METADATA; + static const std::string INSTRUCTION_NAME_METADATA; + + public: + static char ID; // Class identification, replacement for typeinfo + AddTiming() : FunctionPass(ID), F(nullptr), TTI(nullptr) {} + + /// Returns the expected cost of the instruction. + /// Returns -1 if the cost is unknown. + /// Note, this method does not cache the cost calculation and it + /// can be expensive in some cases. + unsigned getInstructionCost(const Instruction *I) const; + + private: + void addMetadata(Instruction *Inst, const std::string &name, const std::string& value) const; + void addMetadata(Instruction *Inst, const std::string &name, unsigned cost) const; + void addNamingMetadata(Instruction *Inst) const; + void addTimingMetadata(Instruction* Inst) const; + + void getAnalysisUsage(AnalysisUsage &AU) const override; + bool runOnFunction(Function &F) override; + void print(raw_ostream &OS, const Module*) const override; + std::string nameInstruction(Instruction *Inst) const; + + /// The function that we analyze. + Function *F; + /// Target information. + const TargetTransformInfo *TTI; + }; + +}//namespace smack + +#endif //ADDTIMING_H diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index 9c76685c1..cb8205756 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -4,14 +4,9 @@ #ifndef BOOGIEAST_H #define BOOGIEAST_H -#include "llvm/Support/Casting.h" - -#include #include #include -#include #include -#include namespace smack { @@ -193,6 +188,7 @@ class Attr { std::list vals; public: Attr(std::string n, std::initializer_list vs) : name(n), vals(vs) {} + Attr(std::string n, std::list vs) : name(n), vals(vs) {} void print(std::ostream& os) const; std::string getName() const { return name; } @@ -202,6 +198,7 @@ class Attr { static const Attr* attr(std::string s, std::string v, int i); static const Attr* attr(std::string s, std::string v, int i, int j); static const Attr* attr(std::string s, std::initializer_list vs); + static const Attr* attr(std::string s, std::list vs); }; class Stmt { diff --git a/include/smack/BplFilePrinter.h b/include/smack/BplFilePrinter.h index 0e2415580..6cc22212d 100644 --- a/include/smack/BplFilePrinter.h +++ b/include/smack/BplFilePrinter.h @@ -4,31 +4,27 @@ #ifndef BPLFILEPRINTER_H #define BPLFILEPRINTER_H -#include "smack/SmackModuleGenerator.h" +#include "llvm/Pass.h" namespace smack { class BplFilePrinter : public llvm::ModulePass { private: llvm::raw_ostream &out; - + public: static char ID; // Pass identification, replacement for typeid BplFilePrinter(llvm::raw_ostream &out) : llvm::ModulePass(ID), out(out) {} - + virtual bool runOnModule(llvm::Module& m); - + virtual const char *getPassName() const { return "Boogie file printing"; } - - virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const { - AU.setPreservesAll(); - AU.addRequired(); - } + + virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const; }; } #endif // BPLPRINTER_H - diff --git a/include/smack/BplPrinter.h b/include/smack/BplPrinter.h index 2979c97a9..554e01af7 100644 --- a/include/smack/BplPrinter.h +++ b/include/smack/BplPrinter.h @@ -4,7 +4,7 @@ #ifndef BPLPRINTER_H #define BPLPRINTER_H -#include "smack/SmackModuleGenerator.h" +#include "llvm/Pass.h" namespace smack { @@ -15,12 +15,8 @@ class BplPrinter : public llvm::ModulePass { BplPrinter() : llvm::ModulePass(ID) {} virtual bool runOnModule(llvm::Module& m); - virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const { - AU.setPreservesAll(); - AU.addRequired(); - } + virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const; }; } #endif // BPLPRINTER_H - diff --git a/include/smack/Contracts.h b/include/smack/Contracts.h index 4d36251b0..bb4760dd7 100644 --- a/include/smack/Contracts.h +++ b/include/smack/Contracts.h @@ -4,24 +4,24 @@ #include "llvm/IR/InstVisitor.h" #include "llvm/IR/CFG.h" -#include "smack/Slicing.h" -#include "smack/SmackRep.h" -#include "smack/SmackInstGenerator.h" -#include "smack/BoogieAst.h" namespace smack { using namespace llvm; +class Naming; +class SmackRep; +class Slices; + class ContractsExtractor : public InstVisitor { private: - SmackRep& rep; - ProcDecl& proc; - Naming& naming; - Slices& slices; + SmackRep* rep; + ProcDecl* proc; + Naming* naming; + Slices* slices; static unsigned uniqueSliceId; public: - ContractsExtractor(SmackRep& R, ProcDecl& P, Naming& N, Slices& S) + ContractsExtractor(SmackRep* R, ProcDecl* P, Naming* N, Slices* S) : rep(R), proc(P), naming(N), slices(S) {} void visitCallInst(CallInst& ci); diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h index caf781d14..c0ca61519 100644 --- a/include/smack/DSAWrapper.h +++ b/include/smack/DSAWrapper.h @@ -7,21 +7,26 @@ #ifndef DSAWRAPPER_H #define DSAWRAPPER_H -#include "assistDS/DSNodeEquivs.h" -#include "dsa/DataStructure.h" -#include "dsa/DSGraph.h" -#include "dsa/TypeSafety.h" -#include "llvm/Analysis/AliasAnalysis.h" -#include "llvm/Analysis/Passes.h" -#include "llvm/ADT/EquivalenceClasses.h" -#include "llvm/IR/Constants.h" -#include "llvm/IR/DerivedTypes.h" +#include "llvm/Analysis/MemoryLocation.h" #include "llvm/IR/InstVisitor.h" -#include "llvm/IR/Module.h" #include +namespace llvm { +class DSNode; +class DSGraph; +class TDDataStructures; +class BUDataStructures; +class DSNodeEquivs; +} + +namespace dsa { +template +struct TypeSafety; +} + namespace smack { + class MemcpyCollector : public llvm::InstVisitor { private: llvm::DSNodeEquivs *nodeEqs; @@ -29,25 +34,7 @@ class MemcpyCollector : public llvm::InstVisitor { public: MemcpyCollector(llvm::DSNodeEquivs *neqs) : nodeEqs(neqs) { } - - void visitMemCpyInst(llvm::MemCpyInst& mci) { - const llvm::EquivalenceClasses &eqs - = nodeEqs->getEquivalenceClasses(); - const llvm::DSNode *n1 = eqs.getLeaderValue( - nodeEqs->getMemberForValue(mci.getOperand(0)) ); - const llvm::DSNode *n2 = eqs.getLeaderValue( - nodeEqs->getMemberForValue(mci.getOperand(1)) ); - - bool f1 = false, f2 = false; - for (unsigned i=0; i getMemcpys() { return memcpys; } @@ -63,47 +50,30 @@ class DSAWrapper : public llvm::ModulePass { std::vector staticInits; std::vector memcpys; std::unordered_set intConversions; - const DataLayout* dataLayout; + const llvm::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); + int getOffset(const llvm::MemoryLocation* l); public: static char ID; DSAWrapper() : ModulePass(ID) {} - virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const { - AU.setPreservesAll(); - AU.addRequiredTransitive(); - AU.addRequiredTransitive(); - AU.addRequiredTransitive(); - AU.addRequired >(); - } - - virtual bool runOnModule(llvm::Module &M) { - dataLayout = &M.getDataLayout(); - TD = &getAnalysis(); - BU = &getAnalysis(); - nodeEqs = &getAnalysis(); - TS = &getAnalysis >(); - memcpys = collectMemcpys(M, new MemcpyCollector(nodeEqs)); - staticInits = collectStaticInits(M); - module = &M; - return false; - } + virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const; + virtual bool runOnModule(llvm::Module &M); 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 isFieldDisjoint(const llvm::GlobalValue* V, unsigned offset); bool isRead(const llvm::Value* V); 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); + unsigned getPointedTypeSize(const llvm::Value* v); + int getOffset(const llvm::Value* v); const llvm::DSNode *getNode(const llvm::Value* v); void printDSAGraphs(const char* Filename); }; diff --git a/include/smack/Debug.h b/include/smack/Debug.h new file mode 100644 index 000000000..ce7fe770b --- /dev/null +++ b/include/smack/Debug.h @@ -0,0 +1,38 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#ifndef SMACK_DEBUG_H +#define SMACK_DEBUG_H + +#include "llvm/Support/raw_ostream.h" + +namespace smack { + +#ifndef NDEBUG + +bool isCurrentDebugType(const char *Type); +void setCurrentDebugType(const char *Type); +void setCurrentDebugTypes(const char **Types, unsigned Count); + +#define SMACK_DEBUG_WITH_TYPE(TYPE, X) \ + do { if (::smack::DebugFlag && ::smack::isCurrentDebugType(TYPE)) { X; } \ + } while (false) + +#else +#define isCurrentDebugType(X) (false) +#define setCurrentDebugType(X) +#define setCurrentDebugTypes(X, N) +#define SMACK_DEBUG_WITH_TYPE(TYPE, X) do { } while (false) +#endif + +extern bool DebugFlag; + +llvm::raw_ostream &dbgs(); + +#undef DEBUG +#define DEBUG(X) SMACK_DEBUG_WITH_TYPE(DEBUG_TYPE, X) + +} + +#endif diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 918c3d889..b0ee5a985 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -4,11 +4,18 @@ #ifndef REGIONS_H #define REGIONS_H -#include "dsa/DSGraph.h" -#include "smack/DSAWrapper.h" +#include "llvm/IR/InstVisitor.h" + +using namespace llvm; + +namespace llvm { + class DSNode; +} namespace smack { +class DSAWrapper; + class Region { private: LLVMContext* context; diff --git a/include/smack/Slicing.h b/include/smack/Slicing.h index 7b80e41d6..d82f09e7d 100644 --- a/include/smack/Slicing.h +++ b/include/smack/Slicing.h @@ -7,15 +7,15 @@ #include "llvm/IR/InstVisitor.h" #include "llvm/Analysis/AliasAnalysis.h" -#include "smack/BoogieAst.h" -#include "smack/Naming.h" -#include "smack/SmackRep.h" #include using namespace llvm; namespace smack { +class Naming; +class SmackRep; + class Slice; typedef vector Slices; @@ -36,9 +36,9 @@ class Slice { void remove(); string getName(); - const Expr* getCode(Naming& naming, SmackRep& rep); - const Decl* getBoogieDecl(Naming& naming, SmackRep& rep); - const Expr* getBoogieExpression(Naming& naming, SmackRep& rep); + const Expr* getCode(Naming* naming, SmackRep* rep); + const Decl* getBoogieDecl(Naming* naming, SmackRep* rep); + const Expr* getBoogieExpression(Naming* naming, SmackRep* rep); }; } diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index 5402370de..75d30c4cc 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -4,9 +4,6 @@ #ifndef SMACKINSTVISITOR_H #define SMACKINSTVISITOR_H -#include "smack/BoogieAst.h" -#include "smack/SmackRep.h" -#include "smack/Naming.h" #include "llvm/IR/InstVisitor.h" #include "llvm/Analysis/LoopInfo.h" #include @@ -14,13 +11,22 @@ namespace smack { +class Naming; +class Program; +class ProcDecl; +class Block; +class Stmt; +class Expr; +class Attr; +class SmackRep; + class SmackInstGenerator : public llvm::InstVisitor { private: - LoopInfo& loops; - SmackRep& rep; - ProcDecl& proc; - Naming& naming; + llvm::LoopInfo& loops; + SmackRep* rep; + ProcDecl* proc; + Naming* naming; Block* currBlock; llvm::BasicBlock::const_iterator nextInst; @@ -40,15 +46,10 @@ class SmackInstGenerator : public llvm::InstVisitor { const Stmt* recordProcedureCall(llvm::Value* V, std::list attrs); public: - void emit(const Stmt* s) { - // stringstream str; - // s->print(str); - // DEBUG(llvm::errs() << "emit: " << str.str() << "\n"); - currBlock->addStmt(s); - } + void emit(const Stmt* s); public: - SmackInstGenerator(LoopInfo& LI, SmackRep& R, ProcDecl& P, Naming& N) + SmackInstGenerator(llvm::LoopInfo& LI, SmackRep* R, ProcDecl* P, Naming* N) : loops(LI), rep(R), proc(P), naming(N) {} diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h index b11dded1b..a3156e112 100644 --- a/include/smack/SmackModuleGenerator.h +++ b/include/smack/SmackModuleGenerator.h @@ -4,44 +4,24 @@ #ifndef SMACKMODULEGENERATOR_H #define SMACKMODULEGENERATOR_H -#include "smack/BoogieAst.h" -#include "smack/SmackInstGenerator.h" -#include "llvm/Analysis/LoopInfo.h" -#include "llvm/IR/DataLayout.h" -#include "llvm/IR/CFG.h" -#include "llvm/Support/CommandLine.h" -#include "llvm/Support/Debug.h" -#include "llvm/Support/GraphWriter.h" -#include -#include - -using llvm::errs; +#include "llvm/Pass.h" namespace smack { +class Program; + class SmackModuleGenerator : public llvm::ModulePass { private: - Program program; + Program* program; public: static char ID; // Pass identification, replacement for typeid - SmackModuleGenerator() : ModulePass(ID) {} - - virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const { - AU.setPreservesAll(); - AU.addRequired(); - AU.addRequired(); - } - - virtual bool runOnModule(llvm::Module& m) { - generateProgram(m); - return false; - } - + SmackModuleGenerator(); + virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const; + virtual bool runOnModule(llvm::Module& m); void generateProgram(llvm::Module& m); - - Program& getProgram() { + Program* getProgram() { return program; } }; diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index 665861043..811679c32 100644 --- a/include/smack/SmackOptions.h +++ b/include/smack/SmackOptions.h @@ -24,6 +24,7 @@ class SmackOptions { static const llvm::cl::opt NoByteAccessInference; static const llvm::cl::opt FloatEnabled; static const llvm::cl::opt MemorySafety; + static const llvm::cl::opt AddTiming; static bool isEntryPoint(std::string); }; diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 86ea8488a..d0e305ccd 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -4,21 +4,25 @@ #ifndef SMACKREP_H #define SMACKREP_H -#include "smack/BoogieAst.h" -#include "smack/Naming.h" -#include "smack/Regions.h" -#include "smack/SmackOptions.h" #include "llvm/IR/InstVisitor.h" #include "llvm/IR/DataLayout.h" #include "llvm/IR/InstrTypes.h" -#include "llvm/Support/Debug.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/Support/GraphWriter.h" #include "llvm/Support/Regex.h" #include +#include namespace smack { +class Naming; +class Program; +class Decl; +class ProcDecl; +class Stmt; +class Expr; +class Regions; + using llvm::Regex; using llvm::SmallVector; using llvm::StringRef; @@ -26,9 +30,9 @@ using llvm::StringRef; class SmackRep { protected: const llvm::DataLayout* targetData; - Naming& naming; - Program& program; - Regions& regions; + Naming* naming; + Program* program; + Regions* regions; std::vector bplGlobals; std::map globalAllocations; @@ -41,8 +45,8 @@ class SmackRep { std::map auxDecls; public: - SmackRep(const DataLayout* L, Naming& N, Program& P, Regions& R); - Program& getProgram() { return program; } + SmackRep(const llvm::DataLayout* L, Naming* N, Program* P, Regions* R); + Program* getProgram() { return program; } private: @@ -63,7 +67,7 @@ class SmackRep { std::string opName(const std::string& operation, std::initializer_list types); std::string opName(const std::string& operation, std::initializer_list types); - const Stmt* store(unsigned R, const Type* T, const Expr* P, const Expr* V); + const Stmt* store(unsigned R, const llvm::Type* T, const Expr* P, const Expr* V); const Expr* cast(unsigned opcode, const llvm::Value* v, const llvm::Type* t); const Expr* bop(unsigned opcode, const llvm::Value* lhs, const llvm::Value* rhs, const llvm::Type* t); @@ -124,14 +128,14 @@ class SmackRep { const Stmt* memcpy(const llvm::MemCpyInst& msi); const Stmt* memset(const llvm::MemSetInst& msi); const Expr* load(const llvm::Value* P); - const Stmt* store(const Value* P, const Value* V); - const Stmt* store(const Value* P, const Expr* V); + const Stmt* store(const llvm::Value* P, const llvm::Value* V); + const Stmt* store(const llvm::Value* P, const Expr* V); - const Stmt* valueAnnotation(const CallInst& CI); - const Stmt* returnValueAnnotation(const CallInst& CI); + const Stmt* valueAnnotation(const llvm::CallInst& CI); + const Stmt* returnValueAnnotation(const llvm::CallInst& CI); - std::list procedure(Function* F); - ProcDecl* procedure(Function* F, CallInst* C); + std::list procedure(llvm::Function* F); + ProcDecl* procedure(llvm::Function* F, llvm::CallInst* C); // used in Slicing unsigned getElementSize(const llvm::Value* v); @@ -140,12 +144,7 @@ class SmackRep { std::string memType(unsigned region); std::string memPath(unsigned region); - std::list< std::pair< std::string, std::string > > memoryMaps() { - std::list< std::pair< std::string, std::string > > mms; - for (unsigned i=0; i > memoryMaps(); // used in SmackInstGenerator std::string getString(const llvm::Value* v); diff --git a/include/smack/SplitAggregateLoadStore.h b/include/smack/SplitAggregateLoadStore.h new file mode 100644 index 000000000..897222b5e --- /dev/null +++ b/include/smack/SplitAggregateLoadStore.h @@ -0,0 +1,31 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#include "llvm/IR/DataLayout.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#include "llvm/Pass.h" +#include "llvm/IR/IRBuilder.h" + +#include +#include + +namespace smack { + +class SplitAggregateLoadStore : public llvm::BasicBlockPass { +public: + static char ID; + + SplitAggregateLoadStore() : llvm::BasicBlockPass(ID) {} + virtual bool runOnBasicBlock(llvm::BasicBlock& BB); + +private: + void splitAggregateLoad(llvm::LoadInst* li); + llvm::Value* buildAggregateValues(llvm::IRBuilder<> *irb, llvm::Value* ptr, llvm::Type* ct, + llvm::Value* val, std::vector> idxs); + void splitAggregateStore(llvm::StoreInst* si, llvm::Value* ptr, llvm::Value* val); + void copyAggregateValues(llvm::IRBuilder<> *irb, llvm::Value* ptr, llvm::Type* ct, + llvm::Value* val, std::vector> idxs); +}; +} diff --git a/include/smack/VerifierCodeMetadata.h b/include/smack/VerifierCodeMetadata.h new file mode 100644 index 000000000..4e41c7008 --- /dev/null +++ b/include/smack/VerifierCodeMetadata.h @@ -0,0 +1,28 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#include "llvm/IR/Instructions.h" +#include "llvm/IR/InstVisitor.h" +#include "llvm/IR/Module.h" +#include "llvm/Pass.h" +#include + +namespace smack { + +using namespace llvm; + +class VerifierCodeMetadata : public ModulePass, public InstVisitor { +private: + std::queue workList; + +public: + static char ID; + VerifierCodeMetadata() : ModulePass(ID) {} + virtual bool runOnModule(Module& M); + virtual void getAnalysisUsage(AnalysisUsage &AU) const; + void visitCallInst(CallInst&); + void visitInstruction(Instruction&); + static bool isMarked(const Instruction& I); +}; +} diff --git a/lib/AssistDS/ArgCast.cpp b/lib/AssistDS/ArgCast.cpp index ae3cf37b8..418914e8a 100644 --- a/lib/AssistDS/ArgCast.cpp +++ b/lib/AssistDS/ArgCast.cpp @@ -19,7 +19,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include @@ -53,7 +53,7 @@ bool ArgCast::runOnModule(Module& M) { std::vector worklist; for (Function &F : M) { - if (F.mayBeOverridden()) + if (F.isInterposable()) continue; // Find all uses of this function for (User *U : F.users()) { diff --git a/lib/AssistDS/ArgSimplify.cpp b/lib/AssistDS/ArgSimplify.cpp index 93acdb15f..2ddb0521a 100644 --- a/lib/AssistDS/ArgSimplify.cpp +++ b/lib/AssistDS/ArgSimplify.cpp @@ -15,7 +15,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include @@ -141,7 +141,7 @@ namespace { bool runOnModule(Module& M) { for (Function &F : M) - if (!F.isDeclaration() && !F.mayBeOverridden()) { + if (!F.isDeclaration() && !F.isInterposable()) { if(F.getName().str() == "main") continue; std::vector Args; diff --git a/lib/AssistDS/DSNodeEquivs.cpp b/lib/AssistDS/DSNodeEquivs.cpp index 942e333d6..68ac8e352 100644 --- a/lib/AssistDS/DSNodeEquivs.cpp +++ b/lib/AssistDS/DSNodeEquivs.cpp @@ -19,6 +19,7 @@ #include "llvm/IR/Module.h" #include "llvm/IR/InstIterator.h" #include "llvm/ADT/SmallSet.h" +#include "smack/Debug.h" #include diff --git a/lib/AssistDS/Devirt.cpp b/lib/AssistDS/Devirt.cpp index cff6e7b9d..99ed0af14 100644 --- a/lib/AssistDS/Devirt.cpp +++ b/lib/AssistDS/Devirt.cpp @@ -11,7 +11,7 @@ #include "assistDS/Devirt.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/CommandLine.h" #include "llvm/ADT/Statistic.h" diff --git a/lib/AssistDS/FuncSimplify.cpp b/lib/AssistDS/FuncSimplify.cpp index c42084a92..4640fb86c 100644 --- a/lib/AssistDS/FuncSimplify.cpp +++ b/lib/AssistDS/FuncSimplify.cpp @@ -14,7 +14,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include diff --git a/lib/AssistDS/FuncSpec.cpp b/lib/AssistDS/FuncSpec.cpp index 99f6a7c40..9b969e44b 100644 --- a/lib/AssistDS/FuncSpec.cpp +++ b/lib/AssistDS/FuncSpec.cpp @@ -18,7 +18,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include @@ -51,7 +51,7 @@ bool FuncSpec::runOnModule(Module& M) { std::map > >, Function* > toClone; for (Function &F : M) - if (!F.isDeclaration() && !F.mayBeOverridden()) { + if (!F.isDeclaration() && !F.isInterposable()) { std::vector FPArgs; for (auto &Arg : F.args()) { // check if this function has a FunctionType(or a pointer to) argument @@ -95,7 +95,7 @@ bool FuncSpec::runOnModule(Module& M) { for (std::map > >, Function* >::iterator I = toClone.begin(), E = toClone.end(); I != E; ++I) { // Clone all the functions we need cloned ValueToValueMapTy VMap; - Function* DirectF = CloneFunction(I->first.first, VMap, false); + Function* DirectF = CloneFunction(I->first.first, VMap); DirectF->setName(I->first.first->getName().str() + "_SPEC"); DirectF->setLinkage(GlobalValue::InternalLinkage); I->first.first->getParent()->getFunctionList().push_back(DirectF); diff --git a/lib/AssistDS/GEPExprArgs.cpp b/lib/AssistDS/GEPExprArgs.cpp index cda681875..7972d70c5 100644 --- a/lib/AssistDS/GEPExprArgs.cpp +++ b/lib/AssistDS/GEPExprArgs.cpp @@ -21,7 +21,7 @@ #include "llvm/ADT/Statistic.h" #include "llvm/IR/ValueMap.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include @@ -64,7 +64,7 @@ bool GEPExprArgs::runOnModule(Module& M) { // or might be changed, ignore this call site. Function *F = CI->getCalledFunction(); - if (!F || (F->isDeclaration() || F->mayBeOverridden())) + if (!F || (F->isDeclaration() || F->isInterposable())) continue; if(F->hasStructRetAttr()) continue; diff --git a/lib/AssistDS/IndCloner.cpp b/lib/AssistDS/IndCloner.cpp index 636b8bbab..bdc0cd5e5 100644 --- a/lib/AssistDS/IndCloner.cpp +++ b/lib/AssistDS/IndCloner.cpp @@ -70,7 +70,7 @@ IndClone::runOnModule(Module& M) { // Only clone functions which are defined and cannot be replaced by another // function by the linker. // - if (!F.isDeclaration() && !F.mayBeOverridden()) { + if (!F.isDeclaration() && !F.isInterposable()) { for (User *U : F.users()) { if (!isa(U) && !isa(U)) { if(!U->use_empty()) @@ -127,7 +127,7 @@ IndClone::runOnModule(Module& M) { // Function * Original = toClone[index]; ValueToValueMapTy VMap; - Function* DirectF = CloneFunction(Original, VMap, false); + Function* DirectF = CloneFunction(Original, VMap); DirectF->setName(Original->getName() + "_DIRECT"); // diff --git a/lib/AssistDS/Int2PtrCmp.cpp b/lib/AssistDS/Int2PtrCmp.cpp index 7e22affdf..f06b9267e 100644 --- a/lib/AssistDS/Int2PtrCmp.cpp +++ b/lib/AssistDS/Int2PtrCmp.cpp @@ -17,7 +17,7 @@ #include "assistDS/Int2PtrCmp.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/PatternMatch.h" #include diff --git a/lib/AssistDS/LoadArgs.cpp b/lib/AssistDS/LoadArgs.cpp index 8e055766f..677f73ae1 100644 --- a/lib/AssistDS/LoadArgs.cpp +++ b/lib/AssistDS/LoadArgs.cpp @@ -22,7 +22,7 @@ #include "llvm/ADT/Statistic.h" #include "llvm/IR/ValueMap.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include #include @@ -66,7 +66,7 @@ bool LoadArgs::runOnModule(Module& M) { // if the CallInst calls a function, that is externally defined, // or might be changed, ignore this call site. Function *F = CI->getCalledFunction(); - if (!F || (F->isDeclaration() || F->mayBeOverridden())) + if (!F || (F->isDeclaration() || F->isInterposable())) continue; if(F->hasStructRetAttr()) continue; diff --git a/lib/AssistDS/MergeGEP.cpp b/lib/AssistDS/MergeGEP.cpp index ab33ad007..173900959 100644 --- a/lib/AssistDS/MergeGEP.cpp +++ b/lib/AssistDS/MergeGEP.cpp @@ -22,7 +22,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include // Pass statistics diff --git a/lib/AssistDS/SimplifyExtractValue.cpp b/lib/AssistDS/SimplifyExtractValue.cpp index 5a4eb9597..5edfece09 100644 --- a/lib/AssistDS/SimplifyExtractValue.cpp +++ b/lib/AssistDS/SimplifyExtractValue.cpp @@ -19,7 +19,7 @@ #include "llvm/ADT/Statistic.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/PatternMatch.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/AssistDS/SimplifyGEP.cpp b/lib/AssistDS/SimplifyGEP.cpp index 2f8b59c40..6c5d44c5a 100644 --- a/lib/AssistDS/SimplifyGEP.cpp +++ b/lib/AssistDS/SimplifyGEP.cpp @@ -17,7 +17,7 @@ #include "assistDS/SimplifyGEP.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DataLayout.h" #include "llvm/IR/Operator.h" diff --git a/lib/AssistDS/SimplifyInsertValue.cpp b/lib/AssistDS/SimplifyInsertValue.cpp index b4f7053c6..7bf59dd91 100644 --- a/lib/AssistDS/SimplifyInsertValue.cpp +++ b/lib/AssistDS/SimplifyInsertValue.cpp @@ -17,7 +17,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/PatternMatch.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/AssistDS/SimplifyLoad.cpp b/lib/AssistDS/SimplifyLoad.cpp index 1716d6e3c..d79dcbc48 100644 --- a/lib/AssistDS/SimplifyLoad.cpp +++ b/lib/AssistDS/SimplifyLoad.cpp @@ -15,7 +15,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/PatternMatch.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/AssistDS/StructReturnToPointer.cpp b/lib/AssistDS/StructReturnToPointer.cpp index 288efec51..0cb5869a1 100644 --- a/lib/AssistDS/StructReturnToPointer.cpp +++ b/lib/AssistDS/StructReturnToPointer.cpp @@ -20,7 +20,7 @@ #include "llvm/ADT/Statistic.h" #include "llvm/IR/ValueMap.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include @@ -52,7 +52,7 @@ bool StructRet::runOnModule(Module& M) { std::vector worklist; for (Function &F : M) - if (!F.mayBeOverridden()) { + if (!F.isInterposable()) { if(F.isDeclaration()) continue; if(F.hasAddressTaken()) @@ -110,13 +110,26 @@ bool StructRet::runOnModule(Module& M) { ReturnInst * RI = dyn_cast(I++); if(!RI) continue; - LoadInst *LI = dyn_cast(RI->getOperand(0)); - assert(LI && "Return should be preceded by a load instruction"); IRBuilder<> Builder(RI); - Builder.CreateMemCpy(fargs.at(0), - LI->getPointerOperand(), - targetData.getTypeStoreSize(LI->getType()), - targetData.getPrefTypeAlignment(LI->getType())); + if (auto LI = dyn_cast(RI->getOperand(0))) { + Builder.CreateMemCpy(fargs.at(0), + LI->getPointerOperand(), + targetData.getTypeStoreSize(LI->getType()), + targetData.getPrefTypeAlignment(LI->getType())); + } else if (auto CS = dyn_cast(RI->getReturnValue())) { + StructType* ST = CS->getType(); + // We could store the struct into the allocated space pointed by the first + // argument and then load it once SMACK can handle store inst of structs. + for (unsigned i = 0; i < ST->getNumElements(); ++i) { + std::vector idxs = {ConstantInt::get(Type::getInt32Ty(CS->getContext()),0), + ConstantInt::get(Type::getInt32Ty(CS->getContext()),i)}; + Builder.CreateStore(CS->getAggregateElement(i), + Builder.CreateGEP(fargs.at(0), ArrayRef(idxs))); + } + assert(RI->getNumOperands() == 1 && "Return should only have one operand"); + RI->setOperand(0, UndefValue::get(ST)); + } else + llvm_unreachable("Unexpected struct-type return value."); } } diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index 578cabed9..904cc3d5f 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -17,7 +17,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Module.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/InstIterator.h" #include "llvm/Support/raw_ostream.h" #include "llvm/IR/Intrinsics.h" @@ -349,19 +349,8 @@ bool TypeChecks::runOnModule(Module &M) { } } - // - // Do replacements in the worklist. - // Special case for ContantArray(triggered by 253.perl) - // ConstantArray::replaceUsesOfWithOnConstant, replace all uses - // in that constant, unlike the other versions, which only - // replace the use specified in ReplaceWorklist. - // - if(isa(C)) { - C->handleOperandChange(F, CNew, ReplaceWorklist[0]); - } else { - for (unsigned index = 0; index < ReplaceWorklist.size(); ++index) { - C->handleOperandChange(F, CNew, ReplaceWorklist[index]); - } + if (ReplaceWorklist.size() > 0) { + C->handleOperandChange(F, CNew); } continue; } @@ -786,7 +775,7 @@ bool TypeChecks::visitVarArgFunction(Module &M, Function &F) { // create internal clone ValueToValueMapTy VMap; - Function *F_clone = CloneFunction(&F, VMap, false); + Function *F_clone = CloneFunction(&F, VMap); F_clone->setName(F.getName().str() + "internal"); F.setLinkage(GlobalValue::InternalLinkage); F.getParent()->getFunctionList().push_back(F_clone); @@ -1019,7 +1008,7 @@ bool TypeChecks::visitByValFunction(Module &M, Function &F) { } else { // create internal clone ValueToValueMapTy VMap; - Function *F_clone = CloneFunction(&F, VMap, false); + Function *F_clone = CloneFunction(&F, VMap); F_clone->setName(F.getName().str() + "internal"); F.setLinkage(GlobalValue::InternalLinkage); F.getParent()->getFunctionList().push_back(F_clone); diff --git a/lib/AssistDS/TypeChecksOpt.cpp b/lib/AssistDS/TypeChecksOpt.cpp index b8ec53b73..874de2077 100644 --- a/lib/AssistDS/TypeChecksOpt.cpp +++ b/lib/AssistDS/TypeChecksOpt.cpp @@ -17,7 +17,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Module.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/InstIterator.h" #include "llvm/Support/raw_ostream.h" #include "llvm/IR/Intrinsics.h" diff --git a/lib/DSA/AddressTakenAnalysis.cpp b/lib/DSA/AddressTakenAnalysis.cpp index 067322cd6..281e0c63f 100644 --- a/lib/DSA/AddressTakenAnalysis.cpp +++ b/lib/DSA/AddressTakenAnalysis.cpp @@ -21,7 +21,7 @@ #include "llvm/IR/Instructions.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/CallSite.h" #include diff --git a/lib/DSA/AllocatorIdentification.cpp b/lib/DSA/AllocatorIdentification.cpp index ce95ceb69..9a12792fc 100644 --- a/lib/DSA/AllocatorIdentification.cpp +++ b/lib/DSA/AllocatorIdentification.cpp @@ -20,7 +20,7 @@ #include "llvm/Transforms/Utils/Cloning.h" #include "llvm/ADT/Statistic.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include diff --git a/lib/DSA/BottomUpClosure.cpp b/lib/DSA/BottomUpClosure.cpp index f49de1d8e..3dd8b64f4 100644 --- a/lib/DSA/BottomUpClosure.cpp +++ b/lib/DSA/BottomUpClosure.cpp @@ -20,7 +20,7 @@ #include "dsa/DSGraph.h" #include "llvm/IR/Module.h" #include "llvm/ADT/Statistic.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" using namespace llvm; diff --git a/lib/DSA/CallTargets.cpp b/lib/DSA/CallTargets.cpp index 2ae6629ad..c7f37d9b4 100644 --- a/lib/DSA/CallTargets.cpp +++ b/lib/DSA/CallTargets.cpp @@ -24,7 +24,7 @@ #include "dsa/DSGraph.h" #include "dsa/CallTargets.h" #include "llvm/ADT/Statistic.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" #include "llvm/IR/Constants.h" #include @@ -41,7 +41,8 @@ namespace { } namespace dsa { - template + +template char CallTargetFinder::ID = 0; template diff --git a/lib/DSA/CompleteBottomUp.cpp b/lib/DSA/CompleteBottomUp.cpp index e8c8b30b3..17adf0cfb 100644 --- a/lib/DSA/CompleteBottomUp.cpp +++ b/lib/DSA/CompleteBottomUp.cpp @@ -18,7 +18,7 @@ #include "dsa/DSGraph.h" #include "llvm/IR/Module.h" #include "llvm/ADT/Statistic.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" using namespace llvm; diff --git a/lib/DSA/DSGraph.cpp b/lib/DSA/DSGraph.cpp index 07eee4806..9ef2d7924 100644 --- a/lib/DSA/DSGraph.cpp +++ b/lib/DSA/DSGraph.cpp @@ -25,7 +25,7 @@ #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/DataLayout.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/ADT/DepthFirstIterator.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/SCCIterator.h" diff --git a/lib/DSA/DataStructure.cpp b/lib/DSA/DataStructure.cpp index c1159ec50..b94f65e30 100644 --- a/lib/DSA/DataStructure.cpp +++ b/lib/DSA/DataStructure.cpp @@ -25,7 +25,7 @@ #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/DataLayout.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/ADT/DepthFirstIterator.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/SCCIterator.h" @@ -1187,7 +1187,7 @@ void DSNode::markReachableNodes(DenseSet &ReachableNodes) const { // warning: 'this' pointer cannot be null in well-defined C++ code; // comparison may be assumed to always evaluate to false // [-Wtautological-undefined-compare] - if (this == 0) return; + if (this == ((void*) 0)) return; assert(!isForwarding() && "Cannot mark a forwarded node!"); if (ReachableNodes.insert(this).second) // Is newly reachable? for (DSNode::const_edge_iterator I = edge_begin(), E = edge_end(); diff --git a/lib/DSA/DataStructureStats.cpp b/lib/DSA/DataStructureStats.cpp index fafbd18bd..6992f5997 100644 --- a/lib/DSA/DataStructureStats.cpp +++ b/lib/DSA/DataStructureStats.cpp @@ -22,7 +22,7 @@ #include "llvm/IR/InstVisitor.h" #include "llvm/Pass.h" #include "llvm/ADT/Statistic.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" #include diff --git a/lib/DSA/EntryPointAnalysis.cpp b/lib/DSA/EntryPointAnalysis.cpp index cf62ef8c5..07399e6b4 100644 --- a/lib/DSA/EntryPointAnalysis.cpp +++ b/lib/DSA/EntryPointAnalysis.cpp @@ -19,7 +19,7 @@ #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/FormattedStream.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include diff --git a/lib/DSA/EquivClassGraphs.cpp b/lib/DSA/EquivClassGraphs.cpp index bb50742a1..3df33c6c1 100644 --- a/lib/DSA/EquivClassGraphs.cpp +++ b/lib/DSA/EquivClassGraphs.cpp @@ -21,7 +21,7 @@ #include "llvm/Pass.h" #include "dsa/DSGraph.h" #include "llvm/IR/CallSite.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/ADT/SCCIterator.h" #include "llvm/ADT/Statistic.h" #include "llvm/ADT/EquivalenceClasses.h" diff --git a/lib/DSA/Local.cpp b/lib/DSA/Local.cpp index 02d63e478..ff6a21eb1 100644 --- a/lib/DSA/Local.cpp +++ b/lib/DSA/Local.cpp @@ -30,7 +30,7 @@ #include "llvm/IR/IntrinsicInst.h" #include "llvm/IR/Use.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/InstVisitor.h" diff --git a/lib/DSA/StdLibPass.cpp b/lib/DSA/StdLibPass.cpp index 2cb29ebb4..2f95503a1 100644 --- a/lib/DSA/StdLibPass.cpp +++ b/lib/DSA/StdLibPass.cpp @@ -22,7 +22,7 @@ #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/DataLayout.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" #include "llvm/Support/Timer.h" #include diff --git a/lib/DSA/TopDownClosure.cpp b/lib/DSA/TopDownClosure.cpp index b370720de..7d8212e88 100644 --- a/lib/DSA/TopDownClosure.cpp +++ b/lib/DSA/TopDownClosure.cpp @@ -19,7 +19,7 @@ #include "llvm/IR/Module.h" #include "llvm/IR/DerivedTypes.h" #include "dsa/DSGraph.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" #include "llvm/Support/Timer.h" #include "llvm/ADT/Statistic.h" diff --git a/lib/DSA/TypeSafety.cpp b/lib/DSA/TypeSafety.cpp index 33d9a9f56..fd0c49c19 100644 --- a/lib/DSA/TypeSafety.cpp +++ b/lib/DSA/TypeSafety.cpp @@ -19,7 +19,7 @@ #include "llvm/IR/Module.h" #include "llvm/IR/DerivedTypes.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/FormattedStream.h" #include "llvm/Support/CommandLine.h" #include "llvm/ADT/Statistic.h" @@ -551,4 +551,3 @@ TypeSafety::runOnModule(Module & M) { } } - diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp new file mode 100644 index 000000000..5ac78eb0f --- /dev/null +++ b/lib/smack/AddTiming.cpp @@ -0,0 +1,278 @@ +//===- CostModel.cpp ------ Cost Model Analysis ---------------------------===// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// This file defines the cost model analysis. It provides a very basic cost +// estimation for LLVM-IR. This analysis uses the services of the codegen +// to approximate the cost of any IR instruction when lowered to machine +// instructions. The cost results are unit-less and the cost number represents +// the throughput of the machine assuming that all loads hit the cache, all +// branches are predicted, etc. The cost numbers can be added in order to +// compare two or more transformation alternatives. +// +//===----------------------------------------------------------------------===// +#include "smack/AddTiming.h" + +#include "llvm/ADT/STLExtras.h" +#include "llvm/Analysis/Passes.h" +#include "llvm/Analysis/TargetLibraryInfo.h" +#include "llvm/Analysis/TargetTransformInfo.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Value.h" +#include "llvm/Pass.h" +#include "llvm/Support/CommandLine.h" +#include "smack/Debug.h" +#include "llvm/Support/raw_ostream.h" + +#include "smack/VerifierCodeMetadata.h" + +#include + +using namespace llvm; + +#define CM_NAME "cost-model" +#define DEBUG_TYPE CM_NAME + +namespace smack { + +// Register this pass. +char AddTiming::ID = 0; +static RegisterPass +X("add-timing-info", "Add Timing Info"); + +const std::string AddTiming::INT_TIMING_COST_METADATA = "smack.InstTimingCost.Int64"; +const std::string AddTiming::INSTRUCTION_NAME_METADATA = "smack.LLVMInstructionName"; + +static bool begins_with(const std::string& possible_prefix, + const std::string& the_string) { + return (0 == the_string.find(possible_prefix)); +} + +static bool isAutogeneratedSmackFunction(Function& F) { + auto name = F.getName(); + return + (begins_with("__SMACK", name) || + begins_with("__VERIFIER", name)); +} + +void +AddTiming::getAnalysisUsage(AnalysisUsage &AU) const { + AU.setPreservesAll(); + AU.addRequired(); + AU.addRequired(); + AU.addRequired(); +} + +bool +AddTiming::runOnFunction(Function &F) { + this->F = &F; + if (isAutogeneratedSmackFunction(F)) { + //No need to annotate autogenerated functions like __VERIFIER_assume or __SMACK_dummy + return false; + } + + TTI = &(getAnalysis().getTTI(F)); + for (Function::iterator B = F.begin(), BE = F.end(); B != BE; ++B) { + for (BasicBlock::iterator it = B->begin(), e = B->end(); it != e; ++it) { + Instruction *Inst = &*it; + //Add the naming metadata first, so we don't get unnecessary metadata in the print + addNamingMetadata(Inst); + addTimingMetadata(Inst); + } + } + + return false; +} + +void +AddTiming::addTimingMetadata(Instruction* Inst) const { + unsigned Cost = getInstructionCost(Inst); + if (Cost != (unsigned)NO_TIMING_INFO) { + addMetadata(Inst, "smack.InstTimingCost.Int64", Cost); + } +} + +void +AddTiming::addNamingMetadata(Instruction* Inst) const { + std::string nameString; + llvm::raw_string_ostream os(nameString); + Inst->print(os); + addMetadata(Inst, INSTRUCTION_NAME_METADATA, os.str()); +} + + +static TargetTransformInfo::OperandValueKind getOperandInfo(Value *V) { + TargetTransformInfo::OperandValueKind OpInfo = + TargetTransformInfo::OK_AnyValue; + + // Check for a splat of a constant or for a non uniform vector of constants. + if (isa(V) || isa(V)) { + OpInfo = TargetTransformInfo::OK_NonUniformConstantValue; + if (cast(V)->getSplatValue() != nullptr) + OpInfo = TargetTransformInfo::OK_UniformConstantValue; + } + + return OpInfo; +} + +unsigned AddTiming::getInstructionCost(const Instruction *I) const { + if (!TTI) + return NO_TIMING_INFO; + + // When an assume statement appears in the C code + // llvm turns it into a series of IR instructions + // e.g. __VERIFIER_assume(x > y) would create a icmp instruction + // which timing annotations would assign a cost to. Since these instructions do not + // occur in the executed code, this leads to an inaccurate timing model. + // The VerifierCodeMetadata marks such nodes in the IR. We can then just return 0 + + if(VerifierCodeMetadata::isMarked(*I)) { + return 0; + } + + switch (I->getOpcode()) { + case Instruction::GetElementPtr:{ + Type *ValTy = I->getOperand(0)->getType()->getPointerElementType(); + return TTI->getAddressComputationCost(ValTy); + } + + case Instruction::Ret: + case Instruction::PHI: + case Instruction::Br: { + return TTI->getCFInstrCost(I->getOpcode()); + } + case Instruction::Add: + case Instruction::FAdd: + case Instruction::Sub: + case Instruction::FSub: + case Instruction::Mul: + case Instruction::FMul: + case Instruction::UDiv: + case Instruction::SDiv: + case Instruction::FDiv: + case Instruction::URem: + case Instruction::SRem: + case Instruction::FRem: + case Instruction::Shl: + case Instruction::LShr: + case Instruction::AShr: + case Instruction::And: + case Instruction::Or: + case Instruction::Xor: { + TargetTransformInfo::OperandValueKind Op1VK = + getOperandInfo(I->getOperand(0)); + TargetTransformInfo::OperandValueKind Op2VK = + getOperandInfo(I->getOperand(1)); + return TTI->getArithmeticInstrCost(I->getOpcode(), I->getType(), Op1VK, + Op2VK); + } + case Instruction::Select: { + const SelectInst *SI = cast(I); + Type *CondTy = SI->getCondition()->getType(); + return TTI->getCmpSelInstrCost(I->getOpcode(), I->getType(), CondTy); + } + case Instruction::ICmp: + case Instruction::FCmp: { + Type *ValTy = I->getOperand(0)->getType(); + return TTI->getCmpSelInstrCost(I->getOpcode(), ValTy); + } + case Instruction::Store: { + const StoreInst *SI = cast(I); + Type *ValTy = SI->getValueOperand()->getType(); + assert(!ValTy->isStructTy() && "Timing annotations do not currently work for struct sized stores"); + return TTI->getMemoryOpCost(I->getOpcode(), ValTy, + SI->getAlignment(), + SI->getPointerAddressSpace()); + } + case Instruction::Load: { + const LoadInst *LI = cast(I); + assert(!I->getType()->isStructTy() && "Timing annotations do not currently work for struct sized loads"); + return TTI->getMemoryOpCost(I->getOpcode(), I->getType(), + LI->getAlignment(), + LI->getPointerAddressSpace()); + } + case Instruction::ZExt: + case Instruction::SExt: + case Instruction::FPToUI: + case Instruction::FPToSI: + case Instruction::FPExt: + case Instruction::PtrToInt: + case Instruction::IntToPtr: + case Instruction::SIToFP: + case Instruction::UIToFP: + case Instruction::Trunc: + case Instruction::FPTrunc: + case Instruction::BitCast: + case Instruction::AddrSpaceCast: { + Type *SrcTy = I->getOperand(0)->getType(); + return TTI->getCastInstrCost(I->getOpcode(), I->getType(), SrcTy); + } + case Instruction::ExtractElement: { + return NO_TIMING_INFO; + } + case Instruction::InsertElement: { + return NO_TIMING_INFO; + } + case Instruction::ShuffleVector: { + return NO_TIMING_INFO; + } + case Instruction::Call: { + if (const IntrinsicInst *II = dyn_cast(I)) { + SmallVector Tys; + for (unsigned J = 0, JE = II->getNumArgOperands(); J != JE; ++J) + Tys.push_back(II->getArgOperand(J)->getType()); + + FastMathFlags FMF; + if (auto *FPMO = dyn_cast(II)) { + FMF = FPMO->getFastMathFlags(); + } + return TTI->getIntrinsicInstrCost(II->getIntrinsicID(), II->getType(), + Tys, FMF); + } + + return NO_TIMING_INFO; + } + default: + // We don't have any information on this instruction. + return NO_TIMING_INFO; + } +} + +void AddTiming::addMetadata(Instruction *Inst, const std::string &name, const std::string& value) const { + LLVMContext& C = Inst->getContext(); + MDNode* N = MDNode::get(C, MDString::get(C, value)); + Inst->setMetadata(name, N); +} + + +void AddTiming::addMetadata(Instruction *Inst, const std::string &name, unsigned cost) const { + LLVMContext& C = Inst->getContext(); + MDNode* N = MDNode::get(C, ConstantAsMetadata::get(ConstantInt::get(C, llvm::APInt(64, (uint64_t)cost, false)))); + Inst->setMetadata(name, N); +} + +void AddTiming::print(raw_ostream &OS, const Module*) const { + if (!F) + return; + + for (Function::iterator B = F->begin(), BE = F->end(); B != BE; ++B) { + for (BasicBlock::iterator it = B->begin(), e = B->end(); it != e; ++it) { + Instruction *Inst = &*it; + unsigned Cost = getInstructionCost(Inst); + if (Cost != (unsigned)NO_TIMING_INFO) { + OS << "Cost Model: Found an estimated cost of " << Cost; + } else { + OS << "Cost Model: Unknown cost"; + } + OS << " for instruction: "<< *Inst << "\n"; + } + } +} +}//namespace smack diff --git a/lib/smack/BoogieAst.cpp b/lib/smack/BoogieAst.cpp index ca2be2254..c4b5d4688 100644 --- a/lib/smack/BoogieAst.cpp +++ b/lib/smack/BoogieAst.cpp @@ -6,6 +6,7 @@ #include "llvm/IR/Constants.h" #include #include +#include namespace smack { @@ -118,6 +119,10 @@ const Attr* Attr::attr(std::string s, std::initializer_list vs) { return new Attr(s,vs); } +const Attr* Attr::attr(std::string s, std::list vs) { + return new Attr(s,vs); +} + const Attr* Attr::attr(std::string s) { return attr(s, {}); } diff --git a/lib/smack/BplFilePrinter.cpp b/lib/smack/BplFilePrinter.cpp index fc5989cf2..96b3bfe3d 100644 --- a/lib/smack/BplFilePrinter.cpp +++ b/lib/smack/BplFilePrinter.cpp @@ -2,6 +2,8 @@ // This file is distributed under the MIT License. See LICENSE for details. // #include "smack/BplFilePrinter.h" +#include "smack/BoogieAst.h" +#include "smack/SmackModuleGenerator.h" #include "llvm/Support/Debug.h" #include "llvm/Support/GraphWriter.h" #include @@ -12,11 +14,16 @@ using llvm::errs; char BplFilePrinter::ID = 0; +void BplFilePrinter::getAnalysisUsage(llvm::AnalysisUsage& AU) const { + AU.setPreservesAll(); + AU.addRequired(); +} + bool BplFilePrinter::runOnModule(llvm::Module& m) { SmackModuleGenerator& smackGenerator = getAnalysis(); - Program& program = smackGenerator.getProgram(); + Program* program = smackGenerator.getProgram(); std::ostringstream s; - program.print(s); + program->print(s); out << s.str(); // DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); return false; diff --git a/lib/smack/BplPrinter.cpp b/lib/smack/BplPrinter.cpp index e7d2e2514..41e8d377c 100644 --- a/lib/smack/BplPrinter.cpp +++ b/lib/smack/BplPrinter.cpp @@ -2,6 +2,8 @@ // This file is distributed under the MIT License. See LICENSE for details. // #include "smack/BplPrinter.h" +#include "smack/BoogieAst.h" +#include "smack/SmackModuleGenerator.h" #include "llvm/Support/Debug.h" #include "llvm/Support/GraphWriter.h" #include @@ -13,11 +15,16 @@ using llvm::errs; llvm::RegisterPass Y("bpl_print", "BoogiePL printer pass"); char BplPrinter::ID = 0; +void BplPrinter::getAnalysisUsage(llvm::AnalysisUsage& AU) const { + AU.setPreservesAll(); + AU.addRequired(); +} + bool BplPrinter::runOnModule(llvm::Module& m) { SmackModuleGenerator& smackGenerator = getAnalysis(); - Program& program = smackGenerator.getProgram(); + Program* program = smackGenerator.getProgram(); std::ostringstream s; - program.print(s); + program->print(s); DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); return false; } diff --git a/lib/smack/CodifyStaticInits.cpp b/lib/smack/CodifyStaticInits.cpp index 6d7a35750..71de62ccd 100644 --- a/lib/smack/CodifyStaticInits.cpp +++ b/lib/smack/CodifyStaticInits.cpp @@ -9,7 +9,7 @@ #include "smack/Naming.h" #include "smack/SmackOptions.h" #include "llvm/IR/IRBuilder.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Regex.h" #include "llvm/IR/DataLayout.h" @@ -23,41 +23,6 @@ namespace smack { using namespace llvm; -namespace{ - Regex STRING_CONSTANT("^\\.str[.0-9]*$"); - - bool isStringConstant(Value& V) { - return STRING_CONSTANT.match(V.getName().str()); - } - - bool isBoogieCode(Value& V) { - std::queue worklist; - std::set covered; - worklist.push(&V); - covered.insert(&V); - while (worklist.size()) { - Value* U = worklist.front(); - worklist.pop(); - - if (CallInst* CI = dyn_cast(U)) - if (Function* F = CI->getCalledFunction()) - if (F->hasName()) - if (F->getName().find(Naming::MOD_PROC) != std::string::npos - || F->getName().find(Naming::CODE_PROC) != std::string::npos - || F->getName().find(Naming::DECL_PROC) != std::string::npos - || F->getName().find(Naming::TOP_DECL_PROC) != std::string::npos) - return true; - - for (auto W : U->users()) - if (!covered.count(W)) { - worklist.push(W); - covered.insert(W); - } - } - return false; - } -} - bool CodifyStaticInits::runOnModule(Module& M) { TD = &M.getDataLayout(); LLVMContext& C = M.getContext(); @@ -81,7 +46,7 @@ bool CodifyStaticInits::runOnModule(Module& M) { // that have named addresses, e.g., excluding string constants. Thus the // second predicate here is a messy hack that has little to do with the // intended property of being read. - if (DSA->isRead(&G) || !G.hasUnnamedAddr()) + if (DSA->isRead(&G) || !G.hasGlobalUnnamedAddr()) worklist.push_back(std::make_tuple( G.getInitializer(), &G, std::vector())); diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 3b93e63a6..ac599c588 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -5,6 +5,10 @@ // the University of Illinois Open Source License. See LICENSE for details. // #include "smack/DSAWrapper.h" +#include "dsa/DataStructure.h" +#include "assistDS/DSNodeEquivs.h" +#include "dsa/DSGraph.h" +#include "dsa/TypeSafety.h" #include "llvm/Support/FileSystem.h" #define DEBUG_TYPE "dsa-wrapper" @@ -17,6 +21,44 @@ char DSAWrapper::ID; RegisterPass DSAWrapperPass("dsa-wrapper", "SMACK Data Structure Graph Based Alias Analysis Wrapper"); +void MemcpyCollector::visitMemCpyInst(llvm::MemCpyInst& mci) { + const llvm::EquivalenceClasses &eqs + = nodeEqs->getEquivalenceClasses(); + const llvm::DSNode *n1 = eqs.getLeaderValue( + nodeEqs->getMemberForValue(mci.getOperand(0)) ); + const llvm::DSNode *n2 = eqs.getLeaderValue( + nodeEqs->getMemberForValue(mci.getOperand(1)) ); + + bool f1 = false, f2 = false; + for (unsigned i=0; i(); + AU.addRequiredTransitive(); + AU.addRequiredTransitive(); + AU.addRequired >(); +} + +bool DSAWrapper::runOnModule(llvm::Module &M) { + dataLayout = &M.getDataLayout(); + TD = &getAnalysis(); + BU = &getAnalysis(); + nodeEqs = &getAnalysis(); + TS = &getAnalysis >(); + memcpys = collectMemcpys(M, new MemcpyCollector(nodeEqs)); + staticInits = collectStaticInits(M); + module = &M; + return false; +} + std::vector DSAWrapper::collectMemcpys( llvm::Module &M, MemcpyCollector *mcc) { @@ -62,10 +104,16 @@ DSGraph *DSAWrapper::getGraphForValue(const Value *V) { llvm_unreachable("Unexpected value."); } -unsigned DSAWrapper::getOffset(const MemoryLocation* l) { +int 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()); + if (I == S.end()) + return 0; + if (I->second.getNode() && I->second.getNode()->isCollapsedNode()) + return -1; + unsigned offset = I->second.getOffset(); + assert(offset <= INT_MAX && "Cannot handle large offsets"); + return (int) offset; } bool DSAWrapper::isMemcpyd(const llvm::DSNode* n) { @@ -154,7 +202,7 @@ unsigned DSAWrapper::getPointedTypeSize(const Value* v) { llvm_unreachable("Type should be pointer."); } -unsigned DSAWrapper::getOffset(const Value* v) { +int DSAWrapper::getOffset(const Value* v) { return getOffset(new MemoryLocation(v)); } diff --git a/lib/smack/Debug.cpp b/lib/smack/Debug.cpp new file mode 100644 index 000000000..95f3818de --- /dev/null +++ b/lib/smack/Debug.cpp @@ -0,0 +1,90 @@ +#include "smack/Debug.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/ManagedStatic.h" +#include "llvm/Support/Signals.h" +#include "llvm/Support/circular_raw_ostream.h" +#include "llvm/Support/raw_ostream.h" + +#undef isCurrentDebugType +#undef setCurrentDebugType +#undef setCurrentDebugTypes + +using namespace llvm; +using namespace smack; + +namespace smack { +bool DebugFlag = false; + +static ManagedStatic> CurrentDebugType; + +bool isCurrentDebugType(const char *DebugType) { + if (CurrentDebugType->empty()) + return true; + for (auto &d : *CurrentDebugType) { + if (d == DebugType) + return true; + } + return false; +} + +void setCurrentDebugTypes(const char **Types, unsigned Count); + +void setCurrentDebugType(const char *Type) { + setCurrentDebugTypes(&Type, 1); +} + +void setCurrentDebugTypes(const char **Types, unsigned Count) { + CurrentDebugType->clear(); + for (size_t T = 0; T < Count; ++T) + CurrentDebugType->push_back(Types[T]); +} +} + +#ifndef NDEBUG + +static ::llvm::cl::opt +Debug("debug", cl::desc("Enable debug output"), cl::Hidden, + cl::location(DebugFlag)); + +namespace { + +struct DebugOnlyOpt { + void operator=(const std::string &Val) const { + if (Val.empty()) + return; + DebugFlag = true; + SmallVector dbgTypes; + StringRef(Val).split(dbgTypes, ',', -1, false); + for (auto dbgType : dbgTypes) + CurrentDebugType->push_back(dbgType); + } +}; + +} + +static DebugOnlyOpt DebugOnlyOptLoc; + +static ::llvm::cl::opt > +DebugOnly("debug-only", cl::desc("Enable a specific type of debug output (comma separated list of types)"), + cl::Hidden, cl::ZeroOrMore, cl::value_desc("debug string"), + cl::location(DebugOnlyOptLoc), cl::ValueRequired); + +raw_ostream &smack::dbgs() { + static struct dbgstream { + circular_raw_ostream strm; + + dbgstream() : + strm(errs(), "*** Debug Log Output ***\n", 0) { } + } thestrm; + + return thestrm.strm; +} + +#else +namespace smack { + raw_ostream &dbgs() { + return llvm::errs(); + } +} + +#endif diff --git a/lib/smack/ExtractContracts.cpp b/lib/smack/ExtractContracts.cpp index 60540db6b..c60563913 100644 --- a/lib/smack/ExtractContracts.cpp +++ b/lib/smack/ExtractContracts.cpp @@ -7,10 +7,10 @@ #include "smack/SmackOptions.h" #include "smack/Naming.h" #include "smack/ExtractContracts.h" -#include "llvm/Support/Debug.h" #include "llvm/IR/DataLayout.h" #include "llvm/IR/Dominators.h" #include "llvm/Analysis/LoopInfo.h" +#include "smack/Debug.h" #include #include diff --git a/lib/smack/MemorySafetyChecker.cpp b/lib/smack/MemorySafetyChecker.cpp index a86723472..7e716b3e1 100644 --- a/lib/smack/MemorySafetyChecker.cpp +++ b/lib/smack/MemorySafetyChecker.cpp @@ -8,7 +8,7 @@ #include "llvm/IR/Instructions.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/Constants.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/ValueSymbolTable.h" #include "llvm/IR/IntrinsicInst.h" diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index c8e70eaa1..2b4b956f8 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -1,9 +1,16 @@ // // This file is distributed under the MIT License. See LICENSE for details. // +#include "dsa/DSNode.h" +#include "dsa/DSGraph.h" +#include "dsa/DataStructure.h" +#include "dsa/TypeSafety.h" +#include "assistDS/DSNodeEquivs.h" #include "smack/Regions.h" #include "smack/SmackOptions.h" +#include "smack/DSAWrapper.h" #include "llvm/IR/GetElementPtrTypeIterator.h" +#include "smack/Debug.h" #define DEBUG_TYPE "regions" @@ -125,8 +132,14 @@ void Region::init(const Value* V, unsigned length) { representative = (DSA && !dyn_cast(V)) ? DSA->getNode(V) : nullptr; this->type = T; - this->offset = DSA ? DSA->getOffset(V) : 0; - this->length = length; + int offset = DSA ? DSA->getOffset(V) : 0; + if (offset < 0) { + this->offset = 0; + this->length = -1U; + } else { + this->offset = offset; + this->length = length; + } singleton = DL && representative && isSingleton(representative, offset, length); @@ -192,11 +205,11 @@ RegisterPass RegionsPass("smack-regions", "SMACK Memory Regions Pass"); void Regions::getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.setPreservesAll(); if (!SmackOptions::NoMemoryRegionSplitting) { - AU.addRequiredTransitive(); - AU.addRequiredTransitive(); - AU.addRequiredTransitive(); - AU.addRequiredTransitive(); - AU.addRequiredTransitive >(); + AU.addRequiredTransitive(); + AU.addRequiredTransitive(); + AU.addRequiredTransitive(); + AU.addRequiredTransitive(); + AU.addRequiredTransitive >(); AU.addRequired(); } } diff --git a/lib/smack/RemoveDeadDefs.cpp b/lib/smack/RemoveDeadDefs.cpp index fefce508c..129c73665 100644 --- a/lib/smack/RemoveDeadDefs.cpp +++ b/lib/smack/RemoveDeadDefs.cpp @@ -6,7 +6,7 @@ #include "smack/SmackOptions.h" #include "smack/RemoveDeadDefs.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Support/raw_ostream.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/smack/SignedIntegerOverflowChecker.cpp b/lib/smack/SignedIntegerOverflowChecker.cpp index 65d02f9de..07d505698 100644 --- a/lib/smack/SignedIntegerOverflowChecker.cpp +++ b/lib/smack/SignedIntegerOverflowChecker.cpp @@ -7,7 +7,7 @@ #include "llvm/IR/Instructions.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/Constants.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/ValueSymbolTable.h" #include "llvm/IR/IRBuilder.h" #include "llvm/Support/Regex.h" @@ -35,21 +35,7 @@ std::map SignedIntegerOverflowChecker::INT_MIN_TABLE { {64, "-9223372036854775808"} }; -void SignedIntegerOverflowChecker::replaceValue(Value* ee, Value* er) { - for (auto u : ee->users()) { - if (auto inst = dyn_cast(u)) { - if (inst != cast(ee)) { - for (unsigned i = 0; i < inst->getNumOperands(); ++i) { - if (inst->getOperand(i) == ee) - inst->setOperand(i, er); - } - } - } - } -} - bool SignedIntegerOverflowChecker::runOnModule(Module& m) { - DataLayout* dataLayout = new DataLayout(&m); Function* va = m.getFunction("__SMACK_overflow_false"); Function* co = m.getFunction("__SMACK_check_overflow"); @@ -70,25 +56,27 @@ bool SignedIntegerOverflowChecker::runOnModule(Module& m) { std::string op = ar->begin()[1].str(); std::string len = ar->begin()[2].str(); int bits = std::stoi(len); - if (ei->getIndices()[0] == 0) { + if (ei->getIndices()[0] == 1) { + Instruction* prev = &*std::prev(I); Value* o1 = ci->getArgOperand(0); Value* o2 = ci->getArgOperand(1); CastInst* so1 = CastInst::CreateSExtOrBitCast(o1, IntegerType::get(F.getContext(), bits*2), "", &*I); CastInst* so2 = CastInst::CreateSExtOrBitCast(o2, IntegerType::get(F.getContext(), bits*2), "", &*I); BinaryOperator* ai = BinaryOperator::Create(INSTRUCTION_TABLE.at(op), so1, so2, "", &*I); - CastInst* tr = CastInst::CreateTruncOrBitCast(ai, IntegerType::get(F.getContext(), bits), "", &*I); - //replaceValue(&*I, tr); - (*I).replaceAllUsesWith(tr); - //I->eraseFromParent(); - } - if (ei->getIndices()[0] == 1) { - auto ai = std::prev(std::prev(std::prev(I))); + if (prev && isa(prev)) { + ExtractValueInst* pei = cast(prev); + if (auto pci = dyn_cast(pei->getAggregateOperand())) { + if (pci == ci) { + CastInst* tr = CastInst::CreateTruncOrBitCast(ai, IntegerType::get(F.getContext(), bits), "", &*I); + prev->replaceAllUsesWith(tr); + } + } + } ConstantInt* max = ConstantInt::get(IntegerType::get(F.getContext(), bits*2), INT_MAX_TABLE.at(bits), 10); ConstantInt* min = ConstantInt::get(IntegerType::get(F.getContext(), bits*2), INT_MIN_TABLE.at(bits), 10); - ICmpInst* gt = new ICmpInst(&*I, CmpInst::ICMP_SGT, &*ai, max, ""); - ICmpInst* lt = new ICmpInst(&*I, CmpInst::ICMP_SLT, &*ai, min, ""); + ICmpInst* gt = new ICmpInst(&*I, CmpInst::ICMP_SGT, ai, max, ""); + ICmpInst* lt = new ICmpInst(&*I, CmpInst::ICMP_SLT, ai, min, ""); BinaryOperator* flag = BinaryOperator::Create(Instruction::Or, gt, lt, "", &*I); - //replaceValue(&*I, flag); (*I).replaceAllUsesWith(flag); } } @@ -108,9 +96,8 @@ bool SignedIntegerOverflowChecker::runOnModule(Module& m) { ICmpInst* lt = new ICmpInst(&*I, CmpInst::ICMP_SLT, lsdi, min, ""); BinaryOperator* flag = BinaryOperator::Create(Instruction::Or, gt, lt, "", &*I); CastInst* tf = CastInst::CreateSExtOrBitCast(flag, co->getArgumentList().begin()->getType(), "", &*I); - CallInst* ci = CallInst::Create(co, {tf}, "", &*I); + CallInst::Create(co, {tf}, "", &*I); CastInst* tv = CastInst::CreateTruncOrBitCast(lsdi, sdi->getType(), "", &*I); - //replaceValue(&*I, tv); (*I).replaceAllUsesWith(tv); } } diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp index 1223ce062..48a259ea0 100644 --- a/lib/smack/SimplifyLibCalls.cpp +++ b/lib/smack/SimplifyLibCalls.cpp @@ -7,7 +7,7 @@ #include "smack/SmackOptions.h" #include "smack/Naming.h" #include "smack/SimplifyLibCalls.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/Analysis/TargetLibraryInfo.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" diff --git a/lib/smack/Slicing.cpp b/lib/smack/Slicing.cpp index 058ed2fad..cc792225c 100644 --- a/lib/smack/Slicing.cpp +++ b/lib/smack/Slicing.cpp @@ -7,7 +7,7 @@ #include "llvm/Transforms/Utils/BasicBlockUtils.h" #include "llvm/Analysis/CFG.h" #include "llvm/IR/Instructions.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include #include #include diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 944f49055..b08714ac2 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -3,11 +3,13 @@ // #define DEBUG_TYPE "smack-inst-gen" #include "smack/SmackInstGenerator.h" +#include "smack/BoogieAst.h" +#include "smack/SmackRep.h" #include "smack/SmackOptions.h" #include "smack/Naming.h" #include "llvm/IR/InstVisitor.h" #include "llvm/IR/DebugInfo.h" -#include "llvm/Support/Debug.h" +#include "smack/Debug.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/Support/GraphWriter.h" #include "llvm/Analysis/LoopInfo.h" @@ -20,6 +22,7 @@ namespace smack { using llvm::errs; +using namespace llvm; const bool CODE_WARN = true; const bool SHOW_ORIG = false; @@ -42,14 +45,21 @@ std::string i2s(const llvm::Instruction& i) { return s; } +void SmackInstGenerator::emit(const Stmt* s) { + // stringstream str; + // s->print(str); + // DEBUG(llvm::errs() << "emit: " << str.str() << "\n"); + currBlock->addStmt(s); +} + const Stmt* SmackInstGenerator::recordProcedureCall( llvm::Value* V, std::list attrs) { - return Stmt::call("boogie_si_record_" + rep.type(V), {rep.expr(V)}, {}, 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); + Block* b = Block::block(naming->freshBlockName()); + proc->getBlocks().push_back(b); return b; } @@ -62,8 +72,8 @@ Block* SmackInstGenerator::getBlock(llvm::BasicBlock* bb) { void SmackInstGenerator::nameInstruction(llvm::Instruction& inst) { if (inst.getType()->isVoidTy()) return; - proc.getDeclarations().push_back( - Decl::variable(naming.get(inst), rep.type(&inst)) + proc->getDeclarations().push_back( + Decl::variable(naming->get(inst), rep->type(&inst)) ); } @@ -85,8 +95,35 @@ void SmackInstGenerator::annotate(llvm::Instruction& I, Block* B) { B->addStmt(Stmt::annot(Attr::attr("sourceloc", scope->getFilename().str(), DL.getLine(), DL.getCol()))); } + + //https://stackoverflow.com/questions/22138947/reading-metadata-from-instruction + SmallVector, 4> MDForInst; + I.getAllMetadata(MDForInst); + SmallVector Names; + I.getModule()->getMDKindNames(Names); + + // for(auto II = MDForInst.begin(), EE = MDForInst.end(); II !=EE; ++II) { + for (auto II : MDForInst){ + std::string name = Names[II.first]; + if(name.find("smack.") == 0 || name.find("verifier.") == 0) { + std::list attrs; + for(auto AI = II.second->op_begin(), AE = II.second->op_end(); AI != AE; ++AI){ + if (auto *CI = mdconst::dyn_extract(*AI)){ + auto value = CI->getZExtValue(); + attrs.push_back(Expr::lit((long) value)); + } else if (auto *CI = dyn_cast(*AI)){ + auto value = CI->getString(); + attrs.push_back(Expr::lit(value)); + } else { + llvm_unreachable("unexpected attribute type in smack metadata"); + } + } + B->addStmt(Stmt::annot(Attr::attr(name, attrs))); + } + } } + void SmackInstGenerator::processInstruction(llvm::Instruction& inst) { DEBUG(errs() << "Inst: " << inst << "\n"); annotate(inst, currBlock); @@ -100,7 +137,7 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock& bb) { currBlock = getBlock(&bb); auto* F = bb.getParent(); - if (SmackOptions::isEntryPoint(naming.get(*F)) && &bb == &F->getEntryBlock()) { + if (SmackOptions::isEntryPoint(naming->get(*F)) && &bb == &F->getEntryBlock()) { for (auto& I : bb.getInstList()) { if (llvm::isa(I)) continue; @@ -109,9 +146,9 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock& bb) { break; } } - emit(recordProcedureCall(F, {Attr::attr("cexpr", "smack:entry:" + naming.get(*F))})); + 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))})); + emit(recordProcedureCall(&A, {Attr::attr("cexpr", "smack:arg:" + naming->get(*F) + ":" + naming->get(A))})); } } } @@ -135,8 +172,8 @@ void SmackInstGenerator::generatePhiAssigns(llvm::TerminatorInst& ti) { llvm::PHINode* phi = llvm::cast(s); if (llvm::Value* v = phi->getIncomingValueForBlock(block)) { v = v->stripPointerCasts(); - lhs.push_back(rep.expr(phi)); - rhs.push_back(rep.expr(v)); + lhs.push_back(rep->expr(phi)); + rhs.push_back(rep->expr(v)); } } } @@ -187,7 +224,7 @@ void SmackInstGenerator::visitReturnInst(llvm::ReturnInst& ri) { llvm::Value* v = ri.getReturnValue(); if (v) - emit(Stmt::assign(Expr::id(Naming::RET_VAR), rep.expr(v))); + emit(Stmt::assign(Expr::id(Naming::RET_VAR), rep->expr(v))); emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false))); emit(Stmt::return_()); } @@ -207,14 +244,14 @@ void SmackInstGenerator::visitBranchInst(llvm::BranchInst& bi) { // Conditional branch assert(bi.getNumSuccessors() == 2); - const Expr* e = Expr::eq(rep.expr(bi.getCondition()), rep.integerLit(1UL,1)); + const Expr* e = Expr::eq(rep->expr(bi.getCondition()), rep->integerLit(1UL,1)); targets.push_back({e,bi.getSuccessor(0)}); targets.push_back({Expr::not_(e),bi.getSuccessor(1)}); } generatePhiAssigns(bi); if (bi.getNumSuccessors() > 1) emit(Stmt::annot(Attr::attr(Naming::BRANCH_CONDITION_ANNOTATION, - {rep.expr(bi.getCondition())}))); + {rep->expr(bi.getCondition())}))); generateGotoStmts(bi, targets); } @@ -224,13 +261,13 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst& si) { // Collect the list of tarets std::vector > targets; - const Expr* e = rep.expr(si.getCondition()); + const Expr* e = rep->expr(si.getCondition()); const Expr* n = Expr::lit(true); for (llvm::SwitchInst::CaseIt i = si.case_begin(); i != si.case_begin(); ++i) { - const Expr* v = rep.expr(i.getCaseValue()); + const Expr* v = rep->expr(i.getCaseValue()); targets.push_back({Expr::eq(e,v),i.getCaseSuccessor()}); // Add the negation of this case to the default case @@ -242,7 +279,7 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst& si) { generatePhiAssigns(si); emit(Stmt::annot(Attr::attr(Naming::BRANCH_CONDITION_ANNOTATION, - {rep.expr(si.getCondition())}))); + {rep->expr(si.getCondition())}))); generateGotoStmts(si, targets); } @@ -250,7 +287,7 @@ void SmackInstGenerator::visitInvokeInst(llvm::InvokeInst& ii) { processInstruction(ii); llvm::Function* f = ii.getCalledFunction(); if (f) { - emit(rep.call(f, ii)); + emit(rep->call(f, ii)); } else { // llvm_unreachable("Unexpected invoke instruction."); WARN("unsoundly ignoring invoke instruction... "); @@ -270,7 +307,7 @@ void SmackInstGenerator::visitInvokeInst(llvm::InvokeInst& ii) { void SmackInstGenerator::visitResumeInst(llvm::ResumeInst& ri) { processInstruction(ri); emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(true))); - emit(Stmt::assign(Expr::id(Naming::EXN_VAL_VAR), rep.expr(ri.getValue()))); + emit(Stmt::assign(Expr::id(Naming::EXN_VAL_VAR), rep->expr(ri.getValue()))); emit(Stmt::return_()); } @@ -286,7 +323,7 @@ void SmackInstGenerator::visitUnreachableInst(llvm::UnreachableInst& ii) { void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator& I) { processInstruction(I); - emit(Stmt::assign(rep.expr(&I),rep.bop(&I))); + emit(Stmt::assign(rep->expr(&I),rep->bop(&I))); } /******************************************************************************/ @@ -302,10 +339,10 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator& I) { void SmackInstGenerator::visitExtractValueInst(llvm::ExtractValueInst& evi) { processInstruction(evi); if (!SmackOptions::BitPrecise) { - const Expr* e = rep.expr(evi.getAggregateOperand()); + const Expr* e = rep->expr(evi.getAggregateOperand()); for (unsigned i = 0; i < evi.getNumIndices(); i++) e = Expr::fn(Naming::EXTRACT_VALUE, e, Expr::lit((unsigned long) evi.getIndices()[i])); - emit(Stmt::assign(rep.expr(&evi),e)); + emit(Stmt::assign(rep->expr(&evi),e)); } else { WARN("Ignoring extract instruction under bit vector mode."); } @@ -313,8 +350,8 @@ void SmackInstGenerator::visitExtractValueInst(llvm::ExtractValueInst& evi) { void SmackInstGenerator::visitInsertValueInst(llvm::InsertValueInst& ivi) { processInstruction(ivi); - const Expr* old = rep.expr(ivi.getAggregateOperand()); - const Expr* res = rep.expr(&ivi); + const Expr* old = rep->expr(ivi.getAggregateOperand()); + const Expr* res = rep->expr(&ivi); const llvm::Type* t = ivi.getType(); for (unsigned i = 0; i < ivi.getNumIndices(); i++) { @@ -342,7 +379,7 @@ void SmackInstGenerator::visitInsertValueInst(llvm::InsertValueInst& ivi) { res = Expr::fn(Naming::EXTRACT_VALUE, res, Expr::lit(idx)); old = Expr::fn(Naming::EXTRACT_VALUE, old, Expr::lit(idx)); } - emit(Stmt::assume(Expr::eq(res,rep.expr(ivi.getInsertedValueOperand())))); + emit(Stmt::assume(Expr::eq(res,rep->expr(ivi.getInsertedValueOperand())))); } /******************************************************************************/ @@ -351,7 +388,7 @@ void SmackInstGenerator::visitInsertValueInst(llvm::InsertValueInst& ivi) { void SmackInstGenerator::visitAllocaInst(llvm::AllocaInst& ai) { processInstruction(ai); - emit(rep.alloca(ai)); + emit(rep->alloca(ai)); } void SmackInstGenerator::visitLoadInst(llvm::LoadInst& li) { @@ -360,13 +397,13 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst& li) { // TODO what happens with aggregate types? // assert (!li.getType()->isAggregateType() && "Unexpected load value."); - emit(Stmt::assign(rep.expr(&li), rep.load(li.getPointerOperand()))); + emit(Stmt::assign(rep->expr(&li), rep->load(li.getPointerOperand()))); if (SmackOptions::MemoryModelDebug) { emit(Stmt::call(Naming::REC_MEM_OP, {Expr::id(Naming::MEM_OP_VAL)})); emit(Stmt::call("boogie_si_record_int", {Expr::lit(0L)})); - emit(Stmt::call("boogie_si_record_int", {rep.expr(li.getPointerOperand())})); - emit(Stmt::call("boogie_si_record_int", {rep.expr(&li)})); + emit(Stmt::call("boogie_si_record_int", {rep->expr(li.getPointerOperand())})); + emit(Stmt::call("boogie_si_record_int", {rep->expr(&li)})); } } @@ -376,14 +413,14 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst& si) { const llvm::Value* V = si.getOperand(0)->stripPointerCasts(); assert (!V->getType()->isAggregateType() && "Unexpected store value."); - emit(rep.store(P,V)); + emit(rep->store(P,V)); if (SmackOptions::SourceLocSymbols) { if (const llvm::GlobalVariable* G = llvm::dyn_cast(P)) { if (const llvm::PointerType* t = llvm::dyn_cast(G->getType())) { if (!t->getElementType()->isPointerTy()) { assert(G->hasName() && "Expected named global variable."); - emit(Stmt::call("boogie_si_record_" + rep.type(V), {rep.expr(V)}, {}, {Attr::attr("cexpr", G->getName().str())})); + emit(Stmt::call("boogie_si_record_" + rep->type(V), {rep->expr(V)}, {}, {Attr::attr("cexpr", G->getName().str())})); } } } @@ -392,29 +429,29 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst& si) { if (SmackOptions::MemoryModelDebug) { emit(Stmt::call(Naming::REC_MEM_OP, {Expr::id(Naming::MEM_OP_VAL)})); emit(Stmt::call("boogie_si_record_int", {Expr::lit(1L)})); - emit(Stmt::call("boogie_si_record_int", {rep.expr(P)})); - emit(Stmt::call("boogie_si_record_int", {rep.expr(V)})); + emit(Stmt::call("boogie_si_record_int", {rep->expr(P)})); + emit(Stmt::call("boogie_si_record_int", {rep->expr(V)})); } } void SmackInstGenerator::visitAtomicCmpXchgInst(llvm::AtomicCmpXchgInst& i) { processInstruction(i); - const Expr* res = rep.expr(&i); - const Expr* mem = rep.load(i.getOperand(0)); - const Expr* cmp = rep.expr(i.getOperand(1)); - const Expr* swp = rep.expr(i.getOperand(2)); + const Expr* res = rep->expr(&i); + const Expr* mem = rep->load(i.getOperand(0)); + const Expr* cmp = rep->expr(i.getOperand(1)); + const Expr* swp = rep->expr(i.getOperand(2)); emit(Stmt::assign(res,mem)); - emit(rep.store(i.getOperand(0), Expr::cond(Expr::eq(mem, cmp), swp, mem))); + emit(rep->store(i.getOperand(0), Expr::cond(Expr::eq(mem, cmp), swp, mem))); } void SmackInstGenerator::visitAtomicRMWInst(llvm::AtomicRMWInst& i) { using llvm::AtomicRMWInst; processInstruction(i); - const Expr* res = rep.expr(&i); - const Expr* mem = rep.load(i.getPointerOperand()); - const Expr* val = rep.expr(i.getValOperand()); + const Expr* res = rep->expr(&i); + const Expr* mem = rep->load(i.getPointerOperand()); + const Expr* val = rep->expr(i.getValOperand()); emit(Stmt::assign(res,mem)); - emit(rep.store(i.getPointerOperand(), + emit(rep->store(i.getPointerOperand(), i.getOperation() == AtomicRMWInst::Xchg ? val : Expr::fn(Naming::ATOMICRMWINST_TABLE.at(i.getOperation()),mem,val) )); @@ -422,7 +459,7 @@ void SmackInstGenerator::visitAtomicRMWInst(llvm::AtomicRMWInst& i) { void SmackInstGenerator::visitGetElementPtrInst(llvm::GetElementPtrInst& I) { processInstruction(I); - emit(Stmt::assign(rep.expr(&I), rep.ptrArith(&I))); + emit(Stmt::assign(rep->expr(&I), rep->ptrArith(&I))); } /******************************************************************************/ @@ -431,7 +468,7 @@ void SmackInstGenerator::visitGetElementPtrInst(llvm::GetElementPtrInst& I) { void SmackInstGenerator::visitCastInst(llvm::CastInst& I) { processInstruction(I); - emit(Stmt::assign(rep.expr(&I),rep.cast(&I))); + emit(Stmt::assign(rep->expr(&I),rep->cast(&I))); } /******************************************************************************/ @@ -440,7 +477,7 @@ void SmackInstGenerator::visitCastInst(llvm::CastInst& I) { void SmackInstGenerator::visitCmpInst(llvm::CmpInst& I) { processInstruction(I); - emit(Stmt::assign(rep.expr(&I),rep.cmp(&I))); + emit(Stmt::assign(rep->expr(&I),rep->cmp(&I))); } void SmackInstGenerator::visitPHINode(llvm::PHINode& phi) { @@ -451,16 +488,16 @@ void SmackInstGenerator::visitPHINode(llvm::PHINode& phi) { void SmackInstGenerator::visitSelectInst(llvm::SelectInst& i) { processInstruction(i); - std::string x = naming.get(i); + std::string x = naming->get(i); const Expr - *c = rep.expr(i.getOperand(0)), - *v1 = rep.expr(i.getOperand(1)), - *v2 = rep.expr(i.getOperand(2)); + *c = rep->expr(i.getOperand(0)), + *v1 = rep->expr(i.getOperand(1)), + *v2 = rep->expr(i.getOperand(2)); emit(Stmt::havoc(x)); emit(Stmt::assume(Expr::and_( - Expr::impl(Expr::eq(c,rep.integerLit(1L,1)), Expr::eq(Expr::id(x), v1)), - Expr::impl(Expr::neq(c,rep.integerLit(1L,1)), Expr::eq(Expr::id(x), v2)) + Expr::impl(Expr::eq(c,rep->integerLit(1L,1)), Expr::eq(Expr::id(x), v1)), + Expr::impl(Expr::neq(c,rep->integerLit(1L,1)), Expr::eq(Expr::id(x), v2)) ))); } @@ -484,27 +521,27 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { emit(Stmt::skip()); } else if (name.find(Naming::VALUE_PROC) != std::string::npos) { - emit(rep.valueAnnotation(ci)); + emit(rep->valueAnnotation(ci)); } else if (name.find(Naming::RETURN_VALUE_PROC) != std::string::npos) { - emit(rep.returnValueAnnotation(ci)); + emit(rep->returnValueAnnotation(ci)); } else if (name.find(Naming::MOD_PROC) != std::string::npos) { - proc.getModifies().push_back(rep.code(ci)); + proc->getModifies().push_back(rep->code(ci)); } else if (name.find(Naming::CODE_PROC) != std::string::npos) { - emit(Stmt::code(rep.code(ci))); + emit(Stmt::code(rep->code(ci))); } else if (name.find(Naming::DECL_PROC) != std::string::npos) { - std::string code = rep.code(ci); - proc.getDeclarations().push_back(Decl::code(code, code)); + std::string code = rep->code(ci); + proc->getDeclarations().push_back(Decl::code(code, code)); } else if (name.find(Naming::TOP_DECL_PROC) != std::string::npos) { - std::string decl = rep.code(ci); - rep.getProgram().getDeclarations().push_back(Decl::code(decl, decl)); + std::string decl = rep->code(ci); + rep->getProgram()->getDeclarations().push_back(Decl::code(decl, decl)); if (VAR_DECL.match(decl)) { std::string var = VAR_DECL.sub("\\1",decl); - rep.addBplGlobal(var); + rep->addBplGlobal(var); } } else if (name.find(Naming::CONTRACT_EXPR) != std::string::npos) { @@ -513,7 +550,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { } else if (name == "__CONTRACT_int_variable") { // TODO assume that all variables are within an expression scope (?) - // emit(Stmt::assign(rep.expr(&ci), Expr::id(rep.getString(ci.getArgOperand(0))))); + // emit(Stmt::assign(rep->expr(&ci), Expr::id(rep->getString(ci.getArgOperand(0))))); } else if (name == Naming::CONTRACT_FORALL) { assert(ci.getNumArgOperands() == 2 @@ -524,7 +561,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { 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)); + auto binding = rep->getString(ci.getArgOperand(0)); std::list args; auto AX = F->getAttributes(); @@ -533,14 +570,14 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { if (AX.hasAttribute(i+1, "contract-var")) var = AX.getAttribute(i+1, "contract-var").getValueAsString(); args.push_back( - var == binding ? Expr::id(binding) : rep.expr(cj->getArgOperand(i))); + var == binding ? Expr::id(binding) : rep->expr(cj->getArgOperand(i))); } - for (auto m : rep.memoryMaps()) + for (auto m : rep->memoryMaps()) args.push_back(Expr::id(m.first)); auto E = Expr::fn(F->getName(), args); - emit(Stmt::assign(rep.expr(&ci), + emit(Stmt::assign(rep->expr(&ci), Expr::cond(Expr::forall(binding, "int", E), - rep.integerLit(1U,1), rep.integerLit(0U,1)))); + rep->integerLit(1U,1), rep->integerLit(0U,1)))); } else if (name == Naming::CONTRACT_REQUIRES || name == Naming::CONTRACT_ENSURES || @@ -556,14 +593,14 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { std::list args; for (auto& V : cj->arg_operands()) - args.push_back(rep.expr(V)); - for (auto m : rep.memoryMaps()) + args.push_back(rep->expr(V)); + for (auto m : rep->memoryMaps()) args.push_back(Expr::id(m.first)); auto E = Expr::fn(F->getName(), args); if (name == Naming::CONTRACT_REQUIRES) - proc.getRequires().push_back(E); + proc->getRequires().push_back(E); else if (name == Naming::CONTRACT_ENSURES) - proc.getEnsures().push_back(E); + proc->getEnsures().push_back(E); else { auto L = loops[ci.getParent()]; assert(L); @@ -575,34 +612,34 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { // } else if (name == "result") { // assert(ci.getNumArgOperands() == 0 && "Unexpected operands to result."); - // emit(Stmt::assign(rep.expr(&ci),Expr::id(Naming::RET_VAR))); + // emit(Stmt::assign(rep->expr(&ci),Expr::id(Naming::RET_VAR))); // // } else if (name == "qvar") { // assert(ci.getNumArgOperands() == 1 && "Unexpected operands to qvar."); - // emit(Stmt::assign(rep.expr(&ci),Expr::id(rep.getString(ci.getArgOperand(0))))); + // emit(Stmt::assign(rep->expr(&ci),Expr::id(rep->getString(ci.getArgOperand(0))))); // // } else if (name == "old") { // assert(ci.getNumArgOperands() == 1 && "Unexpected operands to old."); // llvm::LoadInst* LI = llvm::dyn_cast(ci.getArgOperand(0)); // assert(LI && "Expected value from Load."); - // emit(Stmt::assign(rep.expr(&ci), - // Expr::fn("old",rep.load(LI->getPointerOperand())) )); + // emit(Stmt::assign(rep->expr(&ci), + // Expr::fn("old",rep->load(LI->getPointerOperand())) )); // } else if (name == "forall") { // assert(ci.getNumArgOperands() == 2 && "Unexpected operands to forall."); // Value* var = ci.getArgOperand(0); // Value* arg = ci.getArgOperand(1); // Slice* S = getSlice(arg); - // emit(Stmt::assign(rep.expr(&ci), - // Expr::forall(rep.getString(var), "int", S->getBoogieExpression(naming,rep)))); + // emit(Stmt::assign(rep->expr(&ci), + // Expr::forall(rep->getString(var), "int", S->getBoogieExpression(naming,rep)))); // // } else if (name == "exists") { // assert(ci.getNumArgOperands() == 2 && "Unexpected operands to forall."); // Value* var = ci.getArgOperand(0); // Value* arg = ci.getArgOperand(1); // Slice* S = getSlice(arg); - // emit(Stmt::assign(rep.expr(&ci), - // Expr::exists(rep.getString(var), "int", S->getBoogieExpression(naming,rep)))); + // emit(Stmt::assign(rep->expr(&ci), + // Expr::exists(rep->getString(var), "int", S->getBoogieExpression(naming,rep)))); // // } else if (name == "invariant") { // assert(ci.getNumArgOperands() == 1 && "Unexpected operands to invariant."); @@ -610,18 +647,18 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst& ci) { // emit(Stmt::assert_(S->getBoogieExpression(naming,rep))); } else { - emit(rep.call(f, ci)); + emit(rep->call(f, ci)); } - if (f->isDeclaration() && rep.isExternal(&ci)) { - std::string name = naming.get(*f); + if (f->isDeclaration() && rep->isExternal(&ci)) { + std::string name = naming->get(*f); if (!EXTERNAL_PROC_IGNORE.match(name)) - emit(Stmt::assume(Expr::fn(Naming::EXTERNAL_ADDR,rep.expr(&ci)))); + emit(Stmt::assume(Expr::fn(Naming::EXTERNAL_ADDR,rep->expr(&ci)))); } - if ((naming.get(*f).find("__SMACK") == 0 || naming.get(*f).find("__VERIFIER") == 0) + 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))})); + emit(recordProcedureCall(&ci, {Attr::attr("cexpr", "smack:ext:" + naming->get(*f))})); } } @@ -650,8 +687,8 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst& dvi) { WARN(i2s(pi)); if (!llvm::isa(&pi) && V == llvm::dyn_cast(&pi)) { std::stringstream recordProc; - recordProc << "boogie_si_record_" << rep.type(V); - emit(Stmt::call(recordProc.str(), {rep.expr(V)}, {}, {Attr::attr("cexpr", var->getName().str())})); + recordProc << "boogie_si_record_" << rep->type(V); + emit(Stmt::call(recordProc.str(), {rep->expr(V)}, {}, {Attr::attr("cexpr", var->getName().str())})); } } } @@ -661,7 +698,7 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst& dvi) { void SmackInstGenerator::visitLandingPadInst(llvm::LandingPadInst& lpi) { processInstruction(lpi); // TODO what exactly!? - emit(Stmt::assign(rep.expr(&lpi),Expr::id(Naming::EXN_VAL_VAR))); + emit(Stmt::assign(rep->expr(&lpi),Expr::id(Naming::EXN_VAL_VAR))); if (lpi.isCleanup()) emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false))); WARN("unsoundly ignoring landingpad clauses..."); @@ -674,13 +711,13 @@ void SmackInstGenerator::visitLandingPadInst(llvm::LandingPadInst& lpi) { void SmackInstGenerator::visitMemCpyInst(llvm::MemCpyInst& mci) { processInstruction(mci); assert (mci.getNumOperands() == 6); - emit(rep.memcpy(mci)); + emit(rep->memcpy(mci)); } void SmackInstGenerator::visitMemSetInst(llvm::MemSetInst& msi) { processInstruction(msi); assert (msi.getNumOperands() == 6); - emit(rep.memset(msi)); + emit(rep->memset(msi)); } } // namespace smack diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index adc646c44..8b6cad53d 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -3,18 +3,39 @@ // #define DEBUG_TYPE "smack-mod-gen" #include "smack/SmackModuleGenerator.h" +#include "smack/SmackInstGenerator.h" +#include "smack/BoogieAst.h" +#include "smack/Naming.h" +#include "smack/Regions.h" +#include "smack/SmackRep.h" #include "smack/SmackOptions.h" +#include "smack/Debug.h" namespace smack { llvm::RegisterPass X("smack", "SMACK generator pass"); char SmackModuleGenerator::ID = 0; +SmackModuleGenerator::SmackModuleGenerator() : ModulePass(ID) { + program = new Program(); +} + +void SmackModuleGenerator::getAnalysisUsage(llvm::AnalysisUsage& AU) const { + AU.setPreservesAll(); + AU.addRequired(); + AU.addRequired(); +} + +bool SmackModuleGenerator::runOnModule(llvm::Module& m) { + generateProgram(m); + return false; +} + void SmackModuleGenerator::generateProgram(llvm::Module& M) { Naming naming; - SmackRep rep(&M.getDataLayout(), naming, program, getAnalysis()); - std::list& decls = program.getDeclarations(); + SmackRep rep(&M.getDataLayout(), &naming, program, &getAnalysis()); + std::list& decls = program->getDeclarations(); DEBUG(errs() << "Analyzing globals...\n"); @@ -48,7 +69,7 @@ void SmackModuleGenerator::generateProgram(llvm::Module& M) { DEBUG(errs() << "Analyzing function body: " << naming.get(F) << "\n"); for (auto P : procs) { - SmackInstGenerator igen(getAnalysis(F).getLoopInfo(), rep, *P, naming); + SmackInstGenerator igen(getAnalysis(F).getLoopInfo(), &rep, P, &naming); DEBUG(errs() << "Generating body for " << naming.get(F) << "\n"); igen.visit(F); DEBUG(errs() << "\n"); @@ -73,10 +94,10 @@ void SmackModuleGenerator::generateProgram(llvm::Module& M) { // NOTE we must do this after instruction generation, since we would not // otherwise know how many regions to declare. - program.appendPrelude(rep.getPrelude()); + program->appendPrelude(rep.getPrelude()); std::list kill_list; - for (auto D : program) { + for (auto D : *program) { if (auto P = dyn_cast(D)) { if (D->getName().find(Naming::CONTRACT_EXPR) != std::string::npos) { decls.insert(decls.end(), Decl::code(P)); diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index d2e2327f7..82f5b02e1 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -38,6 +38,8 @@ const llvm::cl::opt SmackOptions::BitPrecisePointers( "bit-precise-pointers", llvm::cl::desc("Model pointers as bit vectors.") ); +const llvm::cl::opt SmackOptions::AddTiming("timing-annotations", llvm::cl::desc("Add timing annotations.")); + const llvm::cl::opt SmackOptions::NoMemoryRegionSplitting( "no-memory-splitting", llvm::cl::desc("Disable splitting memory into regions.") ); diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index cd871515a..6281070f4 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -5,7 +5,15 @@ #include "smack/SmackRep.h" #include "smack/SmackOptions.h" #include "smack/CodifyStaticInits.h" + +#include "smack/BoogieAst.h" +#include "smack/Naming.h" +#include "smack/Regions.h" +#include "smack/Debug.h" + +#include #include +#include namespace { using namespace llvm; @@ -45,12 +53,6 @@ namespace smack { const unsigned MEMORY_INTRINSIC_THRESHOLD = 0; -Regex PROC_MALLOC_FREE("^(malloc|free_)$"); -Regex PROC_IGNORE("^(" - "llvm\\.memcpy\\..*|llvm\\.memset\\..*|llvm\\.dbg\\..*|" - "__SMACK_code|__SMACK_decl|__SMACK_top_decl" -")$"); - const std::vector INTEGER_SIZES = {1, 8, 16, 24, 32, 40, 48, 56, 64, 88, 96, 128}; const std::vector REF_CONSTANTS = { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, @@ -102,7 +104,7 @@ bool isCodeString(const llvm::Value* V) { return false; } -SmackRep::SmackRep(const DataLayout* L, Naming& N, Program& P, Regions& R) +SmackRep::SmackRep(const DataLayout* L, Naming* N, Program* P, Regions* R) : targetData(L), naming(N), program(P), regions(R), globalsBottom(0), externsBottom(-32768), uniqueFpNum(0), ptrSizeInBits(targetData->getPointerSizeInBits()) @@ -185,7 +187,7 @@ std::string SmackRep::procName(llvm::Function* F, const llvm::User& U) { std::string SmackRep::procName(llvm::Function* F, std::list types) { std::stringstream name; - name << naming.get(*F); + name << naming->get(*F); if (F->isVarArg()) for (auto* T : types) name << "." << type(T); @@ -239,10 +241,10 @@ std::string SmackRep::memReg(unsigned idx) { std::string SmackRep::memType(unsigned region) { std::stringstream s; - if (!regions.get(region).isSingleton() || + if (!regions->get(region).isSingleton() || (SmackOptions::BitPrecise && SmackOptions::NoByteAccessInference)) s << "[" << Naming::PTR_TYPE << "] "; - const Type* T = regions.get(region).getType(); + const Type* T = regions->get(region).getType(); s << (T ? type(T) : intType(8)); return s.str(); } @@ -251,9 +253,16 @@ std::string SmackRep::memPath(unsigned region) { return memReg(region); } +std::list< std::pair< std::string, std::string > > SmackRep::memoryMaps() { + std::list< std::pair< std::string, std::string > > mms; + for (unsigned i=0; isize(); i++) + mms.push_back({memReg(i), memType(i)}); + return mms; +} + bool SmackRep::isExternal(const llvm::Value* v) { return v->getType()->isPointerTy() - && !regions.get(regions.idx(v)).isAllocated(); + && !regions->get(regions->idx(v)).isAllocated(); } const Stmt* SmackRep::alloca(llvm::AllocaInst& i) { @@ -263,7 +272,7 @@ const Stmt* SmackRep::alloca(llvm::AllocaInst& i) { integerToPointer(expr(i.getArraySize()), getIntSize(i.getArraySize()))); // TODO this should not be a pointer type. - return Stmt::call(Naming::ALLOC,{size},{naming.get(i)}); + return Stmt::call(Naming::ALLOC,{size},{naming->get(i)}); } const Stmt* SmackRep::memcpy(const llvm::MemCpyInst& mci) { @@ -273,10 +282,10 @@ const Stmt* SmackRep::memcpy(const llvm::MemCpyInst& mci) { else length = std::numeric_limits::max(); - unsigned r1 = regions.idx(mci.getOperand(0),length); - unsigned r2 = regions.idx(mci.getOperand(1),length); + unsigned r1 = regions->idx(mci.getOperand(0),length); + unsigned r2 = regions->idx(mci.getOperand(1),length); - const Type* T = regions.get(r1).getType(); + const Type* T = regions->get(r1).getType(); Decl* P = memcpyProc(T ? type(T) : intType(8), length); auxDecls[P->getName()] = P; @@ -305,9 +314,9 @@ const Stmt* SmackRep::memset(const llvm::MemSetInst& msi) { else length = std::numeric_limits::max(); - unsigned r = regions.idx(msi.getOperand(0),length); + unsigned r = regions->idx(msi.getOperand(0),length); - const Type* T = regions.get(r).getType(); + const Type* T = regions->get(r).getType(); Decl* P = memsetProc(T ? type(T) : intType(8), length); auxDecls[P->getName()] = P; @@ -331,7 +340,7 @@ const Stmt* SmackRep::memset(const llvm::MemSetInst& msi) { const Stmt* SmackRep::valueAnnotation(const CallInst& CI) { std::string name; std::list args({ expr(CI.getArgOperand(0)) }); - std::list rets({ naming.get(CI) }); + std::list rets({ naming->get(CI) }); std::list attrs; assert(CI.getNumArgOperands() > 0 && "Expected at least one argument."); @@ -344,7 +353,7 @@ const Stmt* SmackRep::valueAnnotation(const CallInst& CI) { name = indexedName(Naming::VALUE_PROC, {type(V->getType())}); if (dyn_cast(V)) { assert(V->hasName() && "Expected named argument."); - attrs.push_back(Attr::attr("name", {Expr::id(naming.get(*V))})); + attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*V))})); } else if (auto LI = dyn_cast(V)) { auto GEP = dyn_cast(LI->getPointerOperand()); @@ -355,9 +364,9 @@ const Stmt* SmackRep::valueAnnotation(const CallInst& CI) { auto T = GEP->getType()->getElementType(); const unsigned bits = T->getIntegerBitWidth(); const unsigned bytes = bits / 8; - const unsigned R = regions.idx(GEP); - bool bytewise = regions.get(R).bytewiseAccess(); - attrs.push_back(Attr::attr("name", {Expr::id(naming.get(*A))})); + const unsigned R = regions->idx(GEP); + bool bytewise = regions->get(R).bytewiseAccess(); + attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); attrs.push_back(Attr::attr("field", { Expr::lit(Naming::LOAD + "." + (bytewise ? "bytes." : "") + intType(bits)), Expr::id(memPath(R)), @@ -410,10 +419,10 @@ const Stmt* SmackRep::valueAnnotation(const CallInst& CI) { const unsigned bits = T->getIntegerBitWidth(); const unsigned bytes = bits / 8; const unsigned length = count * bytes; - const unsigned R = regions.idx(V, length); - bool bytewise = regions.get(R).bytewiseAccess(); + const unsigned R = regions->idx(V, length); + bool bytewise = regions->get(R).bytewiseAccess(); args.push_back(expr(CI.getArgOperand(1))); - attrs.push_back(Attr::attr("name", {Expr::id(naming.get(*A))})); + attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); attrs.push_back(Attr::attr("array", { Expr::lit(Naming::LOAD + "." + (bytewise ? "bytes." : "") + intType(bits)), Expr::id(memPath(R)), @@ -438,7 +447,7 @@ const Stmt* SmackRep::returnValueAnnotation(const CallInst& CI) { return Stmt::call( name, std::list({ Expr::id(Naming::RET_VAR) }), - std::list({ naming.get(CI) }), + std::list({ naming->get(CI) }), {Attr::attr("name", {Expr::id(Naming::RET_VAR)})}); } @@ -457,15 +466,15 @@ const Stmt* SmackRep::returnValueAnnotation(const CallInst& CI) { // const unsigned bits = T->getElementType()->getIntegerBitWidth(); // const unsigned bytes = bits / 8; // const unsigned length = bound * bytes; -// const unsigned R = regions.idx(V, length); -// bool bytewise = regions.get(R).bytewiseAccess(); +// const unsigned R = regions->idx(V, length); +// bool bytewise = regions->get(R).bytewiseAccess(); // std::string L = Naming::LOAD + "." + (bytewise ? "bytes." : "") + intType(bits); // return Stmt::call(Naming::OBJECT_PROC, // std::vector({ // Expr::id(Naming::RET_VAR), // Expr::lit(bound) // }), -// std::vector({ naming.get(CI) }), +// std::vector({ naming->get(CI) }), // std::vector({ // Attr::attr(L, { // Expr::id(memPath(R)), @@ -483,9 +492,9 @@ const Stmt* SmackRep::returnValueAnnotation(const CallInst& CI) { const Expr* SmackRep::load(const llvm::Value* P) { const PointerType* T = dyn_cast(P->getType()); assert(T && "Expected pointer type."); - const unsigned R = regions.idx(P); - bool bytewise = regions.get(R).bytewiseAccess(); - bool singleton = regions.get(R).isSingleton(); + const unsigned R = regions->idx(P); + bool bytewise = regions->get(R).bytewiseAccess(); + bool singleton = regions->get(R).isSingleton(); const Expr* M = Expr::id(memPath(R)); std::string N = Naming::LOAD + "." + (bytewise ? "bytes." : "") + type(T->getElementType()); @@ -499,13 +508,13 @@ const Stmt* SmackRep::store(const Value* P, const Value* V) { const Stmt* SmackRep::store(const Value* P, const Expr* V) { const PointerType* T = dyn_cast(P->getType()); assert(T && "Expected pointer type."); - return store(regions.idx(P), T->getElementType(), expr(P), V); + return store(regions->idx(P), T->getElementType(), expr(P), V); } const Stmt* SmackRep::store(unsigned R, const Type* T, const Expr* P, const Expr* V) { - bool bytewise = regions.get(R).bytewiseAccess(); - bool singleton = regions.get(R).isSingleton(); + bool bytewise = regions->get(R).bytewiseAccess(); + bool singleton = regions->get(R).isSingleton(); std::string N = Naming::STORE + "." + (bytewise ? "bytes." : "") + type(T); const Expr* M = Expr::id(memPath(R)); @@ -604,19 +613,17 @@ const Expr* SmackRep::lit(const llvm::Value* v, bool isUnsigned) { } else if (const ConstantFP* CFP = dyn_cast(v)) { if (SmackOptions::BitPrecise) { const APFloat APF = CFP->getValueAPF(); - std::string str; - raw_string_ostream ss(str); - ss << *CFP; - std::istringstream iss(str); - std::string float_type; - iss >> float_type; + const Type* type = CFP->getType(); unsigned expSize, sigSize; - if (float_type=="float") { + if (type->isFloatTy()) { expSize = 8; sigSize = 24; - } else if (float_type=="double") { + } else if (type->isDoubleTy()) { expSize = 11; sigSize = 53; + } else if (type->isX86_FP80Ty()) { + expSize = 15; + sigSize = 65; } else { llvm_unreachable("Unsupported floating-point type."); } @@ -707,15 +714,15 @@ const Expr* SmackRep::expr(const llvm::Value* v, bool isConstIntUnsigned) { if (isa(v)) { assert(v->hasName()); - return Expr::id(naming.get(*v)); + return Expr::id(naming->get(*v)); } else if (isa(v)) { - std::string name = naming.get(*v); + std::string name = naming->get(*v); auxDecls[name] = Decl::constant(name,type(v)); return Expr::id(name); - } else if (naming.get(*v) != "") { - return Expr::id(naming.get(*v)); + } else if (naming->get(*v) != "") { + return Expr::id(naming->get(*v)); } else if (const Constant* constant = dyn_cast(v)) { @@ -803,13 +810,13 @@ const Expr* SmackRep::cmp(unsigned predicate, const llvm::Value* lhs, const llvm ProcDecl* SmackRep::procedure(Function* F, CallInst* CI) { assert(F && "Unknown function call."); - std::string name = naming.get(*F); + std::string name = naming->get(*F); std::list< std::pair > params, rets; std::list decls; std::list blocks; for (auto &A : F->getArgumentList()) - params.push_back({naming.get(A), type(A.getType())}); + params.push_back({naming->get(A), type(A.getType())}); if (!F->getReturnType()->isVoidTy()) rets.push_back({Naming::RET_VAR, type(F->getReturnType())}); @@ -902,7 +909,7 @@ const Stmt* SmackRep::call(llvm::Function* f, const llvm::User& ci) { assert(f && "Call encountered unresolved function."); - std::string name = naming.get(*f); + std::string name = naming->get(*f); std::list args; std::list rets; @@ -916,7 +923,7 @@ const Stmt* SmackRep::call(llvm::Function* f, const llvm::User& ci) { args.push_back(arg(f, i, ci.getOperand(i))); if (!ci.getType()->isVoidTy()) - rets.push_back(naming.get(ci)); + rets.push_back(naming->get(ci)); return Stmt::call(procName(f, ci), args, rets); } @@ -969,7 +976,7 @@ std::string SmackRep::getPrelude() { } s << "\n"; - s << "// Memory maps (" << regions.size() << " regions)" << "\n"; + s << "// Memory maps (" << regions->size() << " regions)" << "\n"; for (auto M : memoryMaps()) s << "var " << M.first << ": " << M.second << ";" << "\n"; @@ -1090,7 +1097,7 @@ void SmackRep::addInitFunc(const llvm::Function* f) { && "Init functions cannot return a value"); assert(f->getArgumentList().empty() && "Init functions cannot take parameters"); - initFuncs.push_back(naming.get(*f)); + initFuncs.push_back(naming->get(*f)); } Decl* SmackRep::getInitFuncs() { @@ -1108,7 +1115,7 @@ std::list SmackRep::globalDecl(const llvm::GlobalValue* v) { using namespace llvm; std::list decls; std::list ax; - std::string name = naming.get(*v); + std::string name = naming->get(*v); if (isCodeString(v)) return decls; diff --git a/lib/smack/SplitAggregateLoadStore.cpp b/lib/smack/SplitAggregateLoadStore.cpp new file mode 100644 index 000000000..94dacd547 --- /dev/null +++ b/lib/smack/SplitAggregateLoadStore.cpp @@ -0,0 +1,143 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#include "smack/SplitAggregateLoadStore.h" +#include "llvm/IR/InstIterator.h" + +namespace smack { + +using namespace llvm; + +std::vector getFirsts(std::vector> lst) { + std::vector ret; + for (auto& p : lst) + ret.push_back(std::get<0>(p)); + return ret; +} + +std::vector getSeconds(std::vector> lst) { + std::vector ret; + for (auto p = lst.begin()+1; p != lst.end(); ++p) + ret.push_back(std::get<1>(*p)); + return ret; +} + +static bool isUsedByReturnInst(Value* v) { + for (auto u = v->user_begin(); u != v->user_end(); ++u) { + if (isa(*u)) { + return true; + } + } + return false; +} + +bool SplitAggregateLoadStore::runOnBasicBlock(BasicBlock& BB) { + std::vector toRemove; + for(Instruction& I : BB) { + if (LoadInst* li = dyn_cast(&I)) { + if (!isUsedByReturnInst(li) && li->getType()->isAggregateType()) { + splitAggregateLoad(li); + toRemove.push_back(li); + } + } else if (StoreInst* si = dyn_cast(&I)) { + Value* P = si->getPointerOperand(); + Value* V = si->getOperand(0)->stripPointerCasts(); + if (V->getType()->isAggregateType()) { + splitAggregateStore(si, P, V); + toRemove.push_back(si); + } + } + } + + for (auto& i : toRemove) + i->eraseFromParent(); + return true; +} + +void SplitAggregateLoadStore::splitAggregateLoad(LoadInst* li) { + std::vector> idx; + IRBuilder<> irb(li); + li->replaceAllUsesWith(buildAggregateValues(&irb, li->getPointerOperand(), li->getType(), nullptr, idx)); +} + +Value* SplitAggregateLoadStore::buildAggregateValues(IRBuilder<> *irb, Value* ptr, Type* ct, Value* val, + std::vector > idxs) { + LLVMContext& C = ptr->getContext(); + Value* cv = val? val : UndefValue::get(ct); + + if (ct->isIntegerTy() || ct->isPointerTy() || ct->isFloatingPointTy()) + return irb->CreateInsertValue(val, + irb->CreateLoad(irb->CreateGEP(ptr, ArrayRef(getFirsts(idxs)))), + ArrayRef(getSeconds(idxs))); + else if (ArrayType* AT = dyn_cast(ct)) { + for (unsigned i = 0; i < AT->getNumElements(); ++i) { + std::vector > lidxs(idxs); + if (lidxs.empty()) + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt32Ty(C),0), 0)); + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt64Ty(C),i), i)); + cv = buildAggregateValues(irb, ptr, AT->getElementType(), cv, lidxs); + } + } else if (StructType* ST = dyn_cast(ct)) { + for (unsigned i = 0; i < ST->getNumElements(); ++i) { + std::vector > lidxs(idxs); + if (lidxs.empty()) + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt32Ty(C),0), 0)); + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt32Ty(C),i), i)); + cv = buildAggregateValues(irb, ptr, ST->getElementType(i), cv, lidxs); + } + } else + llvm_unreachable("Unsupported type"); + + return cv; +} + +void SplitAggregateLoadStore::splitAggregateStore(StoreInst* si, Value* ptr, Value* val) { + std::vector> idx; + IRBuilder<> irb(si); + copyAggregateValues(&irb, ptr, val->getType(), val, idx); +} + +void SplitAggregateLoadStore::copyAggregateValues(IRBuilder<> *irb, Value* ptr, Type* ct, Value* val, + std::vector > idxs) { + LLVMContext& C = ptr->getContext(); + Constant* cv = dyn_cast(val); + + if (ct->isIntegerTy() || ct->isPointerTy() || ct->isFloatingPointTy()) { + std::vector vidxs = getFirsts(idxs); + if (cv) + irb->CreateStore(val, irb->CreateGEP(ptr, ArrayRef(vidxs))); + else + irb->CreateStore(irb->CreateExtractValue( + val, ArrayRef(getSeconds(idxs))), + irb->CreateGEP(ptr, ArrayRef(vidxs))); + } else if (ArrayType* AT = dyn_cast(ct)) { + for (unsigned i = 0; i < AT->getNumElements(); ++i) { + auto A = cv? cv->getAggregateElement(i) : val; + std::vector > lidxs(idxs); + if (lidxs.empty()) + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt32Ty(C),0), 0)); + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt64Ty(C),i), i)); + copyAggregateValues(irb, ptr, AT->getElementType(), A, lidxs); + } + } else if (StructType* ST = dyn_cast(ct)) { + for (unsigned i = 0; i < ST->getNumElements(); ++i) { + auto A = cv? cv->getAggregateElement(i) : val; + std::vector > lidxs(idxs); + if (lidxs.empty()) + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt32Ty(C),0), 0)); + lidxs.push_back(std::make_pair(ConstantInt::get(Type::getInt32Ty(C),i), i)); + copyAggregateValues(irb, ptr, ST->getElementType(i), A, lidxs); + } + } else + llvm_unreachable("Unsupported type"); +} + +// Pass ID variable +char SplitAggregateLoadStore::ID = 0; + +// Register the pass +static RegisterPass +X("split-aggregate-load-store", "Split Load/Store to Aggregate Types"); + +} + diff --git a/lib/smack/VerifierCodeMetadata.cpp b/lib/smack/VerifierCodeMetadata.cpp new file mode 100644 index 000000000..327952340 --- /dev/null +++ b/lib/smack/VerifierCodeMetadata.cpp @@ -0,0 +1,131 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#define DEBUG_TYPE "verifier-code-metadata" + +#include "smack/SmackOptions.h" +#include "smack/VerifierCodeMetadata.h" +#include "llvm/IR/DataLayout.h" +#include "smack/Debug.h" + +#include + +namespace smack { + +using namespace llvm; + +namespace { + void mark(Instruction &I, bool V = true) { + auto& C = I.getContext(); + I.setMetadata("verifier.code", + MDNode::get(C, ConstantAsMetadata::get( + V ? ConstantInt::getTrue(C) : ConstantInt::getFalse(C) + ))); + } + + bool isVerifierFunctionCall(CallInst &I) { + if (auto F = I.getCalledFunction()) { + auto N = F->getName(); + + if (N.find("__VERIFIER_") == 0) + return true; + + if (N.find("__SMACK_") == 0) + return true; + + if (N.find("__CONTRACT_") == 0) + return true; + } + return false; + } + + bool onlyVerifierUsers(Instruction &I) { + std::queue users; + std::set known; + + for (auto U : I.users()) { + users.push(U); + known.insert(U); + } + + while (!users.empty()) { + if (auto K = dyn_cast(users.front())) { + if (!VerifierCodeMetadata::isMarked(*K)) + return false; + + } else { + for (auto UU : users.front()->users()) { + if (known.count(UU) == 0) { + users.push(UU); + known.insert(UU); + } + } + } + users.pop(); + } + return true; + } +} + +bool VerifierCodeMetadata::isMarked(const Instruction& I) { + auto *N = I.getMetadata("verifier.code"); + assert(N && "expected metadata"); + assert(N->getNumOperands() == 1); + auto *M = dyn_cast(N->getOperand(0).get()); + assert(M && "expected constant-valued metadata"); + auto *C = dyn_cast(M->getValue()); + assert(C && "expected constant-int-valued metadata"); + return C->isOne(); +} + +void VerifierCodeMetadata::getAnalysisUsage(AnalysisUsage &AU) const { +} + +bool VerifierCodeMetadata::runOnModule(Module &M) { + + // first mark verifier function calls + visit(M); + + // then mark values which flow only into marked instructions + while (!workList.empty()) { + auto &I = *workList.front(); + for (auto V : I.operand_values()) { + if (auto J = dyn_cast(V)) { + if (!isMarked(*J) && !dyn_cast(J)) { + if (onlyVerifierUsers(*J)) { + mark(*J); + workList.push(J); + } + } + } + } + workList.pop(); + } + + return true; +} + +void VerifierCodeMetadata::visitCallInst(CallInst &I) { + auto marked = false; + + if (isVerifierFunctionCall(I)) { + marked = true; + workList.push(&I); + } + + mark(I, marked); +} + +void VerifierCodeMetadata::visitInstruction(Instruction &I) { + mark(I, false); +} + +// Pass ID variable +char VerifierCodeMetadata::ID = 0; + +// Register the pass +static RegisterPass +X("verifier-code-metadata", "Verifier Code Metadata"); + +} diff --git a/share/smack/include/math/math.h b/share/smack/include/math/math.h new file mode 100644 index 000000000..88b543c4a --- /dev/null +++ b/share/smack/include/math/math.h @@ -0,0 +1,87 @@ +// This file is distributed under the MIT License. See LICENSE for details. +// + +#ifndef MATH_H +#define MATH_H + +//floats +float fabsf(float x); +float fdimf(float x, float y); +float roundf(float x); +//The following 3 functions are incomplete pending rounding mode implementation +float rintf(float x); +float nearbyintf(float x); +long lrintf(float x); +long lroundf(float x); +float floorf(float x); +float ceilf(float x); +float truncf(float x); +float sqrtf(float x); +float remainderf(float x, float y); +float fminf(float x, float y); +float fmaxf(float x, float y); +float fmodf(float x, float y); +float modff(float x, float* y); +float copysignf(float x, float y); +int __isnormalf(float x); +int __isSubnormalf(float x); +int __iszerof(float x); +int __isinff(float x); +int __isnanf(float x); +int __isnegativef(float x); +int __ispositivef(float x); +int __signbitf(float x); +int signbitf(float x); +int __fpclassifyf(float x); +int fpclassifyf(float x); +int __finitef(float x); +//float nan(float x); + +//doubles +double fabs(double x); +double fdim(double x, double y); +double round(double x); +long lround(double x); +//The following 3 functions are incomplete pending rounding mode implementation +double rint(double x); +double nearbyint(double x); +long lrint(double x); +double floor(double x); +double ceil(double x); +double trunc(double x); +double sqrt(double x); +double remainder(double x, double y); +double fmin(double x, double y); +double fmax(double x, double y); +double fmod(double x, double y); +double modf(double x, double* y); +double copysign(double x, double y); +double nan(const char* x); +int __isnormal(double x); +int __isSubnormal(double x); +int __iszero(double x); +int __isinf(double x); +int __isnan(double x); +int __isnegative(double x); +int __ispositive(double x); +int __signbit(double x); +int signbit(double x); +int __fpclassify(double x); +int fpclassify(double x); +int __finite(double x); + +//long doubles +/*int __isnormall(long double x); +int __isSubnormall(long double x); +int __iszerol(long double x); +int __isinfl(long double x); +int __isnanl(long double x); +int __isnegativel(long double x); +int __ispositivel(long double x); +int __signbitl(long double x); +int signbitl(long double x); +int __fpclassifyl(long double x); +int fpclassifyl(long double x); +int __finitel(long double x);*/ + +#endif diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index a44a32137..e6df7f30d 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -13,6 +13,7 @@ extern "C" { #endif +#ifdef SVCOMP // Apprently needed by SVCOMP benchmarks #define __inline #define __builtin_expect __builtinx_expect @@ -22,6 +23,7 @@ extern "C" { // For handling of va_start macro void __builtinx_va_start(char*,char*); +#endif void __SMACK_code(const char *fmt, ...); void __SMACK_mod(const char *fmt, ...); @@ -40,7 +42,7 @@ smack_value_t __SMACK_return_value(void); // Inserts memory access checks in form of assert to check null pointer access // and buffer overflow errors void __SMACK_check_memory_safety(void*, unsigned long); -void __SMACK_check_memory_leak(); +void __SMACK_check_memory_leak(void); #endif // We need this to enforce that assert/assume are function calls @@ -73,7 +75,7 @@ void exit(int); #define S(...) TY(__VA_ARGS__, S4, S3, S2, S1)(__VA_ARGS__) #define U(...) TY(__VA_ARGS__, U4, U3, U2, U1)(__VA_ARGS__) -#define NONDET_DECL(P, ty...) S(ty) U(P,U(ty)) () +#define NONDET_DECL(P, ty...) S(ty) U(P,U(ty)) (void) void* __VERIFIER_nondet(void); NONDET_DECL(__SMACK_nondet,char); @@ -130,88 +132,6 @@ NONDET_DECL(__VERIFIER_nondet,float); NONDET_DECL(__VERIFIER_nondet,double); NONDET_DECL(__VERIFIER_nondet,long,double); -#if FLOAT_ENABLED -//floats -float fabsf(float x); -float fdimf(float x, float y); -float roundf(float x); -//The following 3 functions are incomplete pending rounding mode implementation -float rintf(float x); -float nearbyintf(float x); -long lrintf(float x); -long lroundf(float x); -float floorf(float x); -float ceilf(float x); -float truncf(float x); -float sqrtf(float x); -float remainderf(float x, float y); -float fminf(float x, float y); -float fmaxf(float x, float y); -float fmodf(float x, float y); -float modff(float x, float* y); -float copysignf(float x, float y); -int __isnormalf(float x); -int __isSubnormalf(float x); -int __iszerof(float x); -int __isinff(float x); -int __isnanf(float x); -int __isnegativef(float x); -int __ispositivef(float x); -int __signbitf(float x); -int signbitf(float x); -int __fpclassifyf(float x); -int fpclassifyf(float x); -int __finitef(float x); -//float nan(float x); - -//doubles -double fabs(double x); -double fdim(double x, double y); -double round(double x); -long lround(double x); -//The following 3 functions are incomplete pending rounding mode implementation -double rint(double x); -double nearbyint(double x); -long lrint(double x); -double floor(double x); -double ceil(double x); -double trunc(double x); -double sqrt(double x); -double remainder(double x, double y); -double fmin(double x, double y); -double fmax(double x, double y); -double fmod(double x, double y); -double modf(double x, double* y); -double copysign(double x, double y); -double nan(const char* x); -int __isnormal(double x); -int __isSubnormal(double x); -int __iszero(double x); -int __isinf(double x); -int __isnan(double x); -int __isnegative(double x); -int __ispositive(double x); -int __signbit(double x); -int signbit(double x); -int __fpclassify(double x); -int fpclassify(double x); -int __finite(double x); - -//long doubles -/*int __isnormall(long double x); -int __isSubnormall(long double x); -int __iszerol(long double x); -int __isinfl(long double x); -int __isnanl(long double x); -int __isnegativel(long double x); -int __ispositivel(long double x); -int __signbitl(long double x); -int signbitl(long double x); -int __fpclassifyl(long double x); -int fpclassifyl(long double x); -int __finitel(long double x);*/ -#endif - #undef S1 #undef S2 #undef S3 @@ -225,7 +145,7 @@ int __finitel(long double x);*/ #undef U #undef NONDET_DECL -// Apparently used in SVCOMP benchmarks +// Used in SVCOMP benchmarks _Bool __VERIFIER_nondet_bool(void); unsigned char __VERIFIER_nondet_uchar(void); unsigned short __VERIFIER_nondet_ushort(void); @@ -234,7 +154,7 @@ unsigned long __VERIFIER_nondet_ulong(void); void* __VERIFIER_nondet_pointer(void); -void __SMACK_decls(); +void __SMACK_decls(void); #ifdef __cplusplus } diff --git a/share/smack/include/string/string.h b/share/smack/include/string/string.h new file mode 100644 index 000000000..cefabd4e0 --- /dev/null +++ b/share/smack/include/string/string.h @@ -0,0 +1,19 @@ +// This file is distributed under the MIT License. See LICENSE for details. +// + +#ifndef STRING_H +#define STRING_H + +#include + +char *strcpy(char *dest, const char *src); +size_t strlen(const char *str); +char *strrchr(const char *src, int c); +size_t strspn(const char *cs, const char *ct); +unsigned long int strtoul(const char *nptr, char **endptr, int base); +double strtod(const char *nptr, char **endptr); +char *strerror(int errnum); +char *getenv(const char *name); +void *realloc (void *__ptr, size_t __size); + +#endif diff --git a/share/smack/lib/math.c b/share/smack/lib/math.c new file mode 100644 index 000000000..d841acf84 --- /dev/null +++ b/share/smack/lib/math.c @@ -0,0 +1,456 @@ +// This file is distributed under the MIT License. See LICENSE for details. +// +#include +#include + +//Check the length of pointers +//#if ( __WORDSIZE == 64 ) +#if defined(__LP64__) || defined(_LP64) +#define BUILD_64 1 +#endif + +float fabsf(float x) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $abs.bvfloat(@);", ret, x); + return ret; +} + +float fdimf(float x, float y) { + if(x>y) + return x-y; + else + return 0; +} + +float roundf(float x) { + if (__isnan(x) || __isinf(x) || __iszero(x)) + return x; + double rete = __VERIFIER_nondet_double(); + double reta = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv32td($round.rne.bvfloat(@));", rete, x); + __SMACK_code("@ := sbv32td($round.rna.bvfloat(@));", reta, x); + if (x > 0) + return fmax(rete, reta); + return fmin(rete, reta); +} + +long lroundf(float x) { + long ret = __VERIFIER_nondet_long(); + __SMACK_code("@ := $lround.bvfloat(dtf(@));", ret, x); + return ret; +} + +float rintf(float x) { + return roundf(x); +} + +float nearbyintf(float x) { + return roundf(x); +} + +long lrintf(float x) { + long ret = __VERIFIER_nondet_long(); + __SMACK_code("@ := $lround.bvfloat(dtf(@));", ret, x); + return ret; +} + +float floorf(float x) { + if (__isnanf(x) || __isinff(x) || __iszerof(x)) + return x; + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv32td($floor.bvfloat(dtf(@)));", ret, x); + return ret; +} + +float ceilf(float x) { + if (__isnanf(x) || __isinff(x) || __iszerof(x)) + return x; + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv32td($ceil.bvfloat(dtf(@)));", ret, x); + return ret; +} + +float truncf(float x) { + if (__isnanf(x) || __isinff(x) || __iszerof(x)) + return x; + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv32td($trunc.bvfloat(dtf(@)));", ret, x); + return ret; +} + +float sqrtf(float x) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $sqrt.bvfloat(dtf(@));", ret, x); + return ret; +} + +float remainderf(float x, float y) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := ftd($rem.bvfloat(dtf(@), dtf(@)));", ret, x, y); + return ret; +} + +float fminf(float x, float y) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $min.bvfloat(dtf(@), dtf(@));", ret, x, y); + return ret; +} + +float fmaxf(float x, float y) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $max.bvfloat(dtf(@), dtf(@));", ret, x, y); + return ret; +} + +float fmodf(float x, float y) { + float result = remainderf(fabsf(x), fabsf(y)); + if (signbitf(result)) + result += fabsf(y); + return copysignf(result, x); +} + +float modff(float x, float* y) { + *y = floorf(x); + return x -*y; +} + +float copysignf(float x, float y) { + double ret = __VERIFIER_nondet_double(); + if (__isnegativef(x)^__isnegativef(y)) + __SMACK_code("@ := $fmul.bvfloat(dtf(@), -0e127f24e8);", ret, x); + else + ret = x; + return ret; +} + +int __isnormalf(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnormal.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isSubnormalf(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $issubnormal.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __iszerof(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $iszero.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isinff(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isinfinite.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isnanf(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnan.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isnegativef(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnegative.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __ispositivef(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $ispositive.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __signbitf(float x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if (dtf(@) <= 0e0f24e8) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int signbitf(float x) { + return __signbitf(x); +} + +int __fpclassifyf(float x) { + if (__isnanf(x)) + return 0; + if (__isinff(x)) + return 1; + if (__iszerof(x)) + return 2; + if (__isSubnormalf(x)) + return 3; + return 4; +} + +int fpclassifyf(float x) { + return __fpclassifyf(x); +} + +int __finitef(float x) { + return !__isinf(x) && !__isnanf(x); +} + +double fabs(double x) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $abs.bvdouble(@);", ret, x); + return ret; +} + +double fdim(double x, double y) { + if(x>y) + return x-y; + else + return 0; +} + +double round(double x) { + if (__isnan(x) || __isinf(x) || __iszero(x)) + return x; + double rete = __VERIFIER_nondet_double(); + double reta = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv64td($round.rne.bvdouble(@));", rete, x); + __SMACK_code("@ := sbv64td($round.rna.bvdouble(@));", reta, x); + if (x > 0) + return fmax(rete, reta); + return fmin(rete, reta); +} + +long lround(double x) { + long ret = __VERIFIER_nondet_long(); + __SMACK_code("@ := $lround.bvdouble(@);", ret, x); + return ret; +} + +double rint(double x) { + return round(x); +} + +double nearbyint(double x) { + return round(x); +} + +long lrint(double x) { + return lround(x); +} + +double floor(double x) { + if (__isnan(x) || __isinf(x) || __iszero(x)) + return x; + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv64td($floor.bvdouble(@));", ret, x); + return ret; +} + +double ceil(double x) { + if (__isnan(x) || __isinf(x) || __iszero(x)) + return x; + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv64td($ceil.bvdouble(@));", ret, x); + return ret; +} + +double trunc(double x) { + if (__isnan(x) || __isinf(x) || __iszero(x)) + return x; + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := sbv64td($trunc.bvdouble(@));", ret, x); + return ret; +} + +double sqrt(double x) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $sqrt.bvdouble(@);", ret, x); + return ret; +} + +double remainder(double x, double y) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := ftd(dtf($rem.bvdouble(ftd(dtf(@)), ftd(dtf(@)))));", ret, x, y); + return ret; +} + +double fmin(double x, double y) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $min.bvdouble(@, @);", ret, x, y); + return ret; +} + +double fmax(double x, double y) { + double ret = __VERIFIER_nondet_double(); + __SMACK_code("@ := $max.bvdouble(@, @);", ret, x, y); + return ret; +} + +double fmod(double x, double y) { + double result = remainder(fabs(x), fabs(y)); + if (signbit(result)) + result += fabs(y); + return copysign(result, x); +} + +double modf(double x, double* y) { + *y = floor(x); + return x - *y; +} + +double copysign(double x, double y) { + double ret = __VERIFIER_nondet_double(); + if (__isnegative(x)^__isnegative(y)) + __SMACK_code("@ := $fmul.bvdouble(@, -0e1023f53e11);", ret, x); + else + ret = x; + return ret; +} + +double nan(const char* x) { + return 0.0/0.0; +} + +int __isnormal(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnormal.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isSubnormal(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $issubnormal.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __iszero(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $iszero.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isinf(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isinfinite.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isnan(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnan.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isnegative(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnegative.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __ispositive(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $ispositive.bvdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __signbit(double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if (@ <= 0e0f53e11) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int signbit(double x) { + return __signbit(x); +} + +int __fpclassify(double x) { + if (__isnan(x)) + return 0; + if (__isinf(x)) + return 1; + if (__iszero(x)) + return 2; + if (__isSubnormal(x)) + return 3; + return 4; +} + +int fpclassify(double x) { + return __fpclassify(x); +} + +int __finite(double x) { + return !__isinf(x) && !__isnan(x); +} + +/*int __isnormall(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnormal.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isSubnormall(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $issubnormal.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __iszerol(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $iszero.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isinfl(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isinfinite.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isnanl(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnan.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __isnegativel(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $isnegative.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __ispositivel(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if $ispositive.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int __signbitl(long double x) { + int ret = __VERIFIER_nondet_int(); + __SMACK_code("@ := if (@ <= 0e0f53e11) then 1bv32 else 0bv32;", ret, x); + return ret; +} + +int signbitl(long double x) { + return __signbitl(x); +} + +int __fpclassifyl(long double x) { + if (__isnanl(x)) + return 0; + if (__isinfl(x)) + return 1; + if (__iszerol(x)) + return 2; + if (__isSubnormall(x)) + return 3; + return 4; +} + +int fpclassifyl(long double x) { + return __fpclassifyl(x); +} + +int __finitel(long double x) { + return !__isinfl(x) && !__isnanl(x); +}*/ diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 190810d6d..ec844899c 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -3,7 +3,7 @@ #include #include -#include +#include #include /** @@ -68,151 +68,151 @@ void exit(int x) { while(1); } -char __VERIFIER_nondet_char() { +char __VERIFIER_nondet_char(void) { char x = __SMACK_nondet_char(); __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX); return x; } -signed char __VERIFIER_nondet_signed_char() { +signed char __VERIFIER_nondet_signed_char(void) { signed char x = __SMACK_nondet_signed_char(); __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX); return x; } -unsigned char __VERIFIER_nondet_unsigned_char() { +unsigned char __VERIFIER_nondet_unsigned_char(void) { unsigned char x = __SMACK_nondet_unsigned_char(); __VERIFIER_assume(x >= 0 && x <= UCHAR_MAX); return x; } -short __VERIFIER_nondet_short() { +short __VERIFIER_nondet_short(void) { short x = __SMACK_nondet_short(); __VERIFIER_assume(x >= SHRT_MIN && x <= SHRT_MAX); return x; } -signed short __VERIFIER_nondet_signed_short() { +signed short __VERIFIER_nondet_signed_short(void) { signed short x = __SMACK_nondet_signed_short(); __VERIFIER_assume(x >= SHRT_MIN && x <= SHRT_MAX); return x; } -signed short int __VERIFIER_nondet_signed_short_int() { +signed short int __VERIFIER_nondet_signed_short_int(void) { signed short int x = __SMACK_nondet_signed_short_int(); __VERIFIER_assume(x >= SHRT_MIN && x <= SHRT_MAX); return x; } -unsigned short __VERIFIER_nondet_unsigned_short() { +unsigned short __VERIFIER_nondet_unsigned_short(void) { unsigned short x = __SMACK_nondet_unsigned_short(); __VERIFIER_assume(x >= 0 && x <= USHRT_MAX); return x; } -unsigned short int __VERIFIER_nondet_unsigned_short_int() { +unsigned short int __VERIFIER_nondet_unsigned_short_int(void) { unsigned short int x = __SMACK_nondet_unsigned_short_int(); __VERIFIER_assume(x >= 0 && x <= USHRT_MAX); return x; } -int __VERIFIER_nondet_int() { +int __VERIFIER_nondet_int(void) { int x = __SMACK_nondet_int(); __VERIFIER_assume(x >= INT_MIN && x <= INT_MAX); return x; } -signed int __VERIFIER_nondet_signed_int() { +signed int __VERIFIER_nondet_signed_int(void) { signed int x = __SMACK_nondet_signed_int(); __VERIFIER_assume(x >= INT_MIN && x <= INT_MAX); return x; } -unsigned __VERIFIER_nondet_unsigned() { +unsigned __VERIFIER_nondet_unsigned(void) { unsigned x = __SMACK_nondet_unsigned(); __VERIFIER_assume(x >= 0 && x <= UINT_MAX); return x; } -unsigned int __VERIFIER_nondet_unsigned_int() { +unsigned int __VERIFIER_nondet_unsigned_int(void) { unsigned int x = __SMACK_nondet_unsigned_int(); __VERIFIER_assume(x >= 0 && x <= UINT_MAX); return x; } -long __VERIFIER_nondet_long() { +long __VERIFIER_nondet_long(void) { long x = __SMACK_nondet_long(); __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); return x; } -long int __VERIFIER_nondet_long_int() { +long int __VERIFIER_nondet_long_int(void) { long int x = __SMACK_nondet_long_int(); __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); return x; } -signed long __VERIFIER_nondet_signed_long() { +signed long __VERIFIER_nondet_signed_long(void) { signed long x = __SMACK_nondet_signed_long(); __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); return x; } -signed long int __VERIFIER_nondet_signed_long_int() { +signed long int __VERIFIER_nondet_signed_long_int(void) { signed long int x = __SMACK_nondet_signed_long_int(); __VERIFIER_assume(x >= LONG_MIN && x <= LONG_MAX); return x; } -unsigned long __VERIFIER_nondet_unsigned_long() { +unsigned long __VERIFIER_nondet_unsigned_long(void) { unsigned long x = __SMACK_nondet_unsigned_long(); __VERIFIER_assume(x >= 0 && x <= ULONG_MAX); return x; } -unsigned long int __VERIFIER_nondet_unsigned_long_int() { +unsigned long int __VERIFIER_nondet_unsigned_long_int(void) { unsigned long int x = __SMACK_nondet_unsigned_long_int(); __VERIFIER_assume(x >= 0 && x <= ULONG_MAX); return x; } -long long __VERIFIER_nondet_long_long() { +long long __VERIFIER_nondet_long_long(void) { long long x = __SMACK_nondet_long_long(); __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); return x; } -long long int __VERIFIER_nondet_long_long_int() { +long long int __VERIFIER_nondet_long_long_int(void) { long long int x = __SMACK_nondet_long_long_int(); __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); return x; } -signed long long __VERIFIER_nondet_signed_long_long() { +signed long long __VERIFIER_nondet_signed_long_long(void) { signed long long x = __SMACK_nondet_signed_long_long(); __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); return x; } -signed long long int __VERIFIER_nondet_signed_long_long_int() { +signed long long int __VERIFIER_nondet_signed_long_long_int(void) { signed long long int x = __SMACK_nondet_signed_long_long_int(); __VERIFIER_assume(x >= LLONG_MIN && x <= LLONG_MAX); return x; } -unsigned long long __VERIFIER_nondet_unsigned_long_long() { +unsigned long long __VERIFIER_nondet_unsigned_long_long(void) { unsigned long long x = __SMACK_nondet_unsigned_long_long(); __VERIFIER_assume(x >= 0 && x <= ULLONG_MAX); return x; } -unsigned long long int __VERIFIER_nondet_unsigned_long_long_int() { +unsigned long long int __VERIFIER_nondet_unsigned_long_long_int(void) { unsigned long long int x = __SMACK_nondet_unsigned_long_long_int(); __VERIFIER_assume(x >= 0 && x <= ULLONG_MAX); return x; } -// Apparently used in SVCCOMP benchmarks +// Used in SVCCOMP benchmarks _Bool __VERIFIER_nondet_bool(void) { _Bool x = (_Bool)__VERIFIER_nondet_int(); __VERIFIER_assume(x == 0 || x == 1); @@ -254,460 +254,7 @@ void* calloc(size_t num, size_t size) { return ret; } -#if FLOAT_ENABLED - - //Check the length of pointers - //#if ( __WORDSIZE == 64 ) - #if defined(__LP64__) || defined(_LP64) - #define BUILD_64 1 - #endif - -float fabsf(float x) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $abs.bvfloat(@);", ret, x); - return ret; -} - -float fdimf(float x, float y) { - if(x>y) - return x-y; - else - return 0; -} - -float roundf(float x) { - if (__isnan(x) || __isinf(x) || __iszero(x)) - return x; - double rete = __VERIFIER_nondet_double(); - double reta = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv32td($round.rne.bvfloat(@));", rete, x); - __SMACK_code("@ := sbv32td($round.rna.bvfloat(@));", reta, x); - if (x > 0) - return fmax(rete, reta); - return fmin(rete, reta); -} - -long lroundf(float x) { - long ret = __VERIFIER_nondet_long(); - __SMACK_code("@ := $lround.bvfloat(dtf(@));", ret, x); - return ret; -} - -float rintf(float x) { - return roundf(x); -} - -float nearbyintf(float x) { - return roundf(x); -} - -long lrintf(float x) { - long ret = __VERIFIER_nondet_long(); - __SMACK_code("@ := $lround.bvfloat(dtf(@));", ret, x); - return ret; -} - -float floorf(float x) { - if (__isnanf(x) || __isinff(x) || __iszerof(x)) - return x; - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv32td($floor.bvfloat(dtf(@)));", ret, x); - return ret; -} - -float ceilf(float x) { - if (__isnanf(x) || __isinff(x) || __iszerof(x)) - return x; - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv32td($ceil.bvfloat(dtf(@)));", ret, x); - return ret; -} - -float truncf(float x) { - if (__isnanf(x) || __isinff(x) || __iszerof(x)) - return x; - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv32td($trunc.bvfloat(dtf(@)));", ret, x); - return ret; -} - -float sqrtf(float x) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $sqrt.bvfloat(dtf(@));", ret, x); - return ret; -} - -float remainderf(float x, float y) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := ftd($rem.bvfloat(dtf(@), dtf(@)));", ret, x, y); - return ret; -} - -float fminf(float x, float y) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $min.bvfloat(dtf(@), dtf(@));", ret, x, y); - return ret; -} - -float fmaxf(float x, float y) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $max.bvfloat(dtf(@), dtf(@));", ret, x, y); - return ret; -} - -float fmodf(float x, float y) { - float result = remainderf(fabsf(x), fabsf(y)); - if (signbitf(result)) - result += fabsf(y); - return copysignf(result, x); -} - -float modff(float x, float* y) { - *y = floorf(x); - return x -*y; -} -float copysignf(float x, float y) { - double ret = __VERIFIER_nondet_double(); - if (__isnegativef(x)^__isnegativef(y)) - __SMACK_code("@ := $fmul.bvfloat(dtf(@), -0e127f24e8);", ret, x); - else - ret = x; - return ret; -} - -int __isnormalf(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnormal.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isSubnormalf(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $issubnormal.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __iszerof(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $iszero.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isinff(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isinfinite.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isnanf(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnan.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isnegativef(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnegative.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __ispositivef(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $ispositive.bvfloat(dtf(@)) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __signbitf(float x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if (dtf(@) <= 0e0f24e8) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int signbitf(float x) { - return __signbitf(x); -} - -int __fpclassifyf(float x) { - if (__isnanf(x)) - return 0; - if (__isinff(x)) - return 1; - if (__iszerof(x)) - return 2; - if (__isSubnormalf(x)) - return 3; - return 4; -} - -int fpclassifyf(float x) { - return __fpclassifyf(x); -} - -int __finitef(float x) { - return !__isinf(x) && !__isnanf(x); -} - -double fabs(double x) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $abs.bvdouble(@);", ret, x); - return ret; -} - -double fdim(double x, double y) { - if(x>y) - return x-y; - else - return 0; -} - -double round(double x) { - if (__isnan(x) || __isinf(x) || __iszero(x)) - return x; - double rete = __VERIFIER_nondet_double(); - double reta = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv64td($round.rne.bvdouble(@));", rete, x); - __SMACK_code("@ := sbv64td($round.rna.bvdouble(@));", reta, x); - if (x > 0) - return fmax(rete, reta); - return fmin(rete, reta); -} - -long lround(double x) { - long ret = __VERIFIER_nondet_long(); - __SMACK_code("@ := $lround.bvdouble(@);", ret, x); - return ret; -} - -double rint(double x) { - return round(x); -} - -double nearbyint(double x) { - return round(x); -} - -long lrint(double x) { - return lround(x); -} - -double floor(double x) { - if (__isnan(x) || __isinf(x) || __iszero(x)) - return x; - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv64td($floor.bvdouble(@));", ret, x); - return ret; -} - -double ceil(double x) { - if (__isnan(x) || __isinf(x) || __iszero(x)) - return x; - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv64td($ceil.bvdouble(@));", ret, x); - return ret; -} - -double trunc(double x) { - if (__isnan(x) || __isinf(x) || __iszero(x)) - return x; - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := sbv64td($trunc.bvdouble(@));", ret, x); - return ret; -} - -double sqrt(double x) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $sqrt.bvdouble(@);", ret, x); - return ret; -} - -double remainder(double x, double y) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := ftd(dtf($rem.bvdouble(ftd(dtf(@)), ftd(dtf(@)))));", ret, x, y); - return ret; -} - -double fmin(double x, double y) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $min.bvdouble(@, @);", ret, x, y); - return ret; -} - -double fmax(double x, double y) { - double ret = __VERIFIER_nondet_double(); - __SMACK_code("@ := $max.bvdouble(@, @);", ret, x, y); - return ret; -} - -double fmod(double x, double y) { - double result = remainder(fabs(x), fabs(y)); - if (signbit(result)) - result += fabs(y); - return copysign(result, x); -} - -double modf(double x, double* y) { - *y = floor(x); - return x - *y; -} - -double copysign(double x, double y) { - double ret = __VERIFIER_nondet_double(); - if (__isnegative(x)^__isnegative(y)) - __SMACK_code("@ := $fmul.bvdouble(@, -0e1023f53e11);", ret, x); - else - ret = x; - return ret; -} - -double nan(const char* x) { - return 0.0/0.0; -} - -int __isnormal(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnormal.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isSubnormal(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $issubnormal.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __iszero(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $iszero.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isinf(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isinfinite.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isnan(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnan.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isnegative(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnegative.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __ispositive(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $ispositive.bvdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __signbit(double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if (@ <= 0e0f53e11) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int signbit(double x) { - return __signbit(x); -} - -int __fpclassify(double x) { - if (__isnan(x)) - return 0; - if (__isinf(x)) - return 1; - if (__iszero(x)) - return 2; - if (__isSubnormal(x)) - return 3; - return 4; -} - -int fpclassify(double x) { - return __fpclassify(x); -} - -int __finite(double x) { - return !__isinf(x) && !__isnan(x); -} - -/*int __isnormall(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnormal.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isSubnormall(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $issubnormal.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __iszerol(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $iszero.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isinfl(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isinfinite.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isnanl(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnan.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __isnegativel(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $isnegative.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __ispositivel(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if $ispositive.bvlongdouble(@) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int __signbitl(long double x) { - int ret = __VERIFIER_nondet_int(); - __SMACK_code("@ := if (@ <= 0e0f53e11) then 1bv32 else 0bv32;", ret, x); - return ret; -} - -int signbitl(long double x) { - return __signbitl(x); -} - -int __fpclassifyl(long double x) { - if (__isnanl(x)) - return 0; - if (__isinfl(x)) - return 1; - if (__iszerol(x)) - return 2; - if (__isSubnormall(x)) - return 3; - return 4; -} - -int fpclassifyl(long double x) { - return __fpclassifyl(x); -} - -int __finitel(long double x) { - return !__isinfl(x) && !__isnanl(x); -}*/ -#endif void __SMACK_dummy(int v) { __SMACK_code("assume true;"); @@ -834,7 +381,7 @@ void __SMACK_dummy(int v) { D(xstr(M(bvdouble,args))); \ D(xstr(M(bvlongdouble,args))); -void __SMACK_decls() { +void __SMACK_decls(void) { DECLARE(INLINE_CONVERSION,ref,ref,$bitcast,{i}); @@ -1515,21 +1062,21 @@ void __SMACK_decls() { DECLARE_EACH_FLOAT_TYPE(FPBUILTIN_BINARY_OP, $frem, fp.rem) D("function $ffalse.bvfloat(f1:bvfloat, f2:bvfloat) returns (i1);"); D("function $ftrue.bvfloat(f1:bvfloat, f2:bvfloat) returns (i1);"); - + D("function {:builtin \"fp.abs\"} $abs.bvfloat(bvfloat) returns (bvfloat);"); D("function {:builtin \"fp.fma\"} $fma.bvfloat(bvfloat, bvfloat, bvfloat) returns (bvfloat);"); D("function {:builtin \"fp.sqrt\"} $sqrt.bvfloat(bvfloat) returns (bvfloat);"); D("function {:builtin \"fp.rem\"} $rem.bvfloat(bvfloat, bvfloat) returns (bvfloat);"); D("function {:builtin \"fp.min\"} $min.bvfloat(bvfloat, bvfloat) returns (bvfloat);"); D("function {:builtin \"fp.max\"} $max.bvfloat(bvfloat, bvfloat) returns (bvfloat);"); - + D("function {:builtin \"fp.abs\"} $abs.bvdouble(bvdouble) returns (bvdouble);"); D("function {:builtin \"fp.fma\"} $fma.bvdouble(bvdouble, bvdouble, bvdouble) returns (bvdouble);"); D("function {:builtin \"fp.sqrt\"} $sqrt.bvdouble(bvdouble) returns (bvdouble);"); D("function {:builtin \"fp.rem\"} $rem.bvdouble(bvdouble, bvdouble) returns (bvdouble);"); D("function {:builtin \"fp.min\"} $min.bvdouble(bvdouble, bvdouble) returns (bvdouble);"); D("function {:builtin \"fp.max\"} $max.bvdouble(bvdouble, bvdouble) returns (bvdouble);"); - + D("function {:builtin \"fp.isNormal\"} $isnormal.bvfloat(bvfloat) returns (bool);"); D("function {:builtin \"fp.isSubnormal\"} $issubnormal.bvfloat(bvfloat) returns (bool);"); D("function {:builtin \"fp.isZero\"} $iszero.bvfloat(bvfloat) returns (bool);"); @@ -1545,7 +1092,7 @@ void __SMACK_decls() { D("function {:builtin \"fp.isNaN\"} $isnan.bvdouble(bvdouble) returns (bool);"); D("function {:builtin \"fp.isNegative\"} $isnegative.bvdouble(bvdouble) returns (bool);"); D("function {:builtin \"fp.isPositive\"} $ispositive.bvdouble(bvdouble) returns (bool);"); - + D("function {:builtin \"fp.isNormal\"} $isnormal.bvlongdouble(bvlongdouble) returns (bool);"); D("function {:builtin \"fp.isSubnormal\"} $issubnormal.bvlongdouble(bvlongdouble) returns (bool);"); D("function {:builtin \"fp.isZero\"} $iszero.bvlongdouble(bvlongdouble) returns (bool);"); @@ -1631,7 +1178,7 @@ void __SMACK_decls() { D("function {:builtin \"(_ fp.to_ubv 24) RNE\"} ftubv24(bvfloat) returns (bv24);"); D("function {:builtin \"(_ fp.to_ubv 16) RNE\"} ftubv16(bvfloat) returns (bv16);"); D("function {:builtin \"(_ fp.to_ubv 8) RNE\"} ftubv8(bvfloat) returns (bv8);"); - + // Add truncation for default casts to int D("function {:builtin \"(_ fp.to_sbv 128) RTZ\"} ftsi128(bvfloat) returns (bv128);"); D("function {:builtin \"(_ fp.to_sbv 96) RTZ\"} ftsi96(bvfloat) returns (bv96);"); @@ -1644,7 +1191,7 @@ void __SMACK_decls() { D("function {:builtin \"(_ fp.to_sbv 24) RTZ\"} ftsi24(bvfloat) returns (bv24);"); D("function {:builtin \"(_ fp.to_sbv 16) RTZ\"} ftsi16(bvfloat) returns (bv16);"); D("function {:builtin \"(_ fp.to_sbv 8) RTZ\"} ftsi8(bvfloat) returns (bv8);"); - + DECLARE(INLINE_CONVERSION, bvfloat, bv128, $fp2si, {ftsi128(i)}); DECLARE(INLINE_CONVERSION, bvfloat, bv128, $fp2ui, {ftubv128(i)}); DECLARE(INLINE_CONVERSION, bv128, bvfloat, $si2fp, {sbv128tf(i)}); @@ -1689,21 +1236,21 @@ void __SMACK_decls() { DECLARE(INLINE_CONVERSION, bvfloat, bv8, $fp2ui, {ftubv8(i)}); DECLARE(INLINE_CONVERSION, bv8, bvfloat, $si2fp, {sbv8tf(i)}); DECLARE(INLINE_CONVERSION, bv8, bvfloat, $ui2fp, {ubv8tf(i)}); - + D("function {:builtin \"(_ fp.to_sbv 32) RNE\"} $round.rne.bvfloat(bvfloat) returns (bv32);"); D("function {:builtin \"(_ fp.to_sbv 32) RNA\"} $round.rna.bvfloat(bvfloat) returns (bv32);"); D("function {:builtin \"(_ fp.to_sbv 32) RTN\"} $floor.bvfloat(bvfloat) returns (bv32);"); D("function {:builtin \"(_ fp.to_sbv 32) RTP\"} $ceil.bvfloat(bvfloat) returns (bv32);"); D("function {:builtin \"(_ fp.to_sbv 32) RTZ\"} $trunc.bvfloat(bvfloat) returns (bv32);"); - + #if BUILD_64 D("function {:builtin \"(_ fp.to_sbv 64) RNA\"} $lround.bvfloat(bvfloat) returns (bv64);"); - + #else D("function {:builtin \"(_ fp.to_sbv 32) RNA\"} $lround.bvfloat(bvfloat) returns (bv32);"); #endif - + //This isn't the correct implementation, so change as needed D("function {:inline} $ford.bvdouble(f1:bvdouble, f2:bvdouble) returns (bv1);"); D("function {:inline} $funo.bvdouble(f1:bvdouble, f2:bvdouble) returns (bv1);"); @@ -1755,7 +1302,7 @@ void __SMACK_decls() { D("function {:builtin \"(_ fp.to_ubv 24) RNE\"} dtubv24(bvdouble) returns (bv24);"); D("function {:builtin \"(_ fp.to_ubv 16) RNE\"} dtubv16(bvdouble) returns (bv16);"); D("function {:builtin \"(_ fp.to_ubv 8) RNE\"} dtubv8(bvdouble) returns (bv8);"); - + // Add truncation for default casts to int D("function {:builtin \"(_ fp.to_sbv 128) RTZ\"} dtsi128(bvdouble) returns (bv128);"); D("function {:builtin \"(_ fp.to_sbv 96) RTZ\"} dtsi96(bvdouble) returns (bv96);"); @@ -1768,7 +1315,7 @@ void __SMACK_decls() { D("function {:builtin \"(_ fp.to_sbv 24) RTZ\"} dtsi24(bvdouble) returns (bv24);"); D("function {:builtin \"(_ fp.to_sbv 16) RTZ\"} dtsi16(bvdouble) returns (bv16);"); D("function {:builtin \"(_ fp.to_sbv 8) RTZ\"} dtsi8(bvdouble) returns (bv8);"); - + DECLARE(INLINE_CONVERSION, bvdouble, bv128, $fp2si, {dtsi128(i)}); DECLARE(INLINE_CONVERSION, bvdouble, bv128, $fp2ui, {dtubv128(i)}); DECLARE(INLINE_CONVERSION, bv128, bvdouble, $si2fp, {sbv128td(i)}); @@ -1813,21 +1360,21 @@ void __SMACK_decls() { DECLARE(INLINE_CONVERSION, bvdouble, bv8, $fp2ui, {dtubv8(i)}); DECLARE(INLINE_CONVERSION, bv8, bvdouble, $si2fp, {sbv8td(i)}); DECLARE(INLINE_CONVERSION, bv8, bvdouble, $ui2fp, {ubv8td(i)}); - + D("function {:builtin \"(_ fp.to_sbv 64) RNE\"} $round.rne.bvdouble(bvdouble) returns (bv64);"); D("function {:builtin \"(_ fp.to_sbv 64) RNA\"} $round.rna.bvdouble(bvdouble) returns (bv64);"); D("function {:builtin \"(_ fp.to_sbv 64) RTN\"} $floor.bvdouble(bvdouble) returns (bv64);"); D("function {:builtin \"(_ fp.to_sbv 64) RTP\"} $ceil.bvdouble(bvdouble) returns (bv64);"); D("function {:builtin \"(_ fp.to_sbv 64) RTZ\"} $trunc.bvdouble(bvdouble) returns (bv64);"); - + #if BUILD_64 D("function {:builtin \"(_ fp.to_sbv 64) RNA\"} $lround.bvdouble(bvdouble) returns (bv64);"); - + #else D("function {:builtin \"(_ fp.to_sbv 32) RNA\"} $lround.bvdouble(bvdouble) returns (bv32);"); #endif - + #endif // Memory Model @@ -2034,7 +1581,9 @@ void __SMACK_decls() { D("procedure $malloc(n: ref) returns (p: ref)\n" "modifies $allocatedCounter;\n" "{\n" - " $allocatedCounter := $allocatedCounter + 1;\n" + " if ($ne.ref.bool(n, $0.ref)) {\n" + " $allocatedCounter := $allocatedCounter + 1;\n" + " }\n" " call p := $$alloc(n);\n" "}\n"); @@ -2053,19 +1602,18 @@ void __SMACK_decls() { D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n" "modifies $Alloc, $CurrAddr;\n" "{\n" - " p := $CurrAddr;\n" - " havoc $CurrAddr;\n" - " if ($sgt.ref.bool(n, $0.ref)) {\n" + " assume $sle.ref.bool($0.ref, n);\n" + " if ($slt.ref.bool($0.ref, n)) {\n" + " p := $CurrAddr;\n" + " havoc $CurrAddr;\n" " assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n" " assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP);\n" " assume $Size(p) == n;\n" " assume (forall q: ref :: {$base(q)} $sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n" + " $Alloc[p] := true;\n" " } else {\n" - " assume $sle.ref.bool($add.ref(p, $1.ref), $CurrAddr);\n" - " assume $Size(p) == $1.ref;\n" - " assume $eq.ref.bool($base(p), p);\n" + " p := $0.ref;\n" " }\n" - " $Alloc[p] := true;\n" "}\n"); D("procedure $free(p: ref)\n" @@ -2073,8 +1621,8 @@ void __SMACK_decls() { "{\n" " if ($ne.ref.bool(p, $0.ref)) {\n" " assert {:valid_free} $eq.ref.bool($base(p), p);\n" - " assert {:valid_free} $Alloc[p] == true;\n" - " assert {:valid_free} $sgt.ref.bool(p, $0.ref);\n" + " assert {:valid_free} $Alloc[p];\n" + " assert {:valid_free} $slt.ref.bool($0.ref, p);\n" " $Alloc[p] := false;\n" " $allocatedCounter := $allocatedCounter - 1;\n" " }\n" @@ -2085,7 +1633,7 @@ void __SMACK_decls() { D("var $Size: [ref] ref;\n"); D("procedure $galloc(base_addr: ref, size: ref);\n" - "modifies $Alloc, $Size;" + "modifies $Alloc, $Size;\n" "ensures $Size[base_addr] == size;\n" "ensures (forall addr: ref :: {$base(addr)} $sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, size)) ==> $base(addr) == base_addr);\n" "ensures $Alloc[base_addr];\n" @@ -2094,20 +1642,21 @@ void __SMACK_decls() { 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" + "ensures $sle.ref.bool($0.ref, n);\n" + "ensures $slt.ref.bool($0.ref, n) ==> $slt.ref.bool($0.ref, p) && $slt.ref.bool(p, $sub.ref($MALLOC_TOP, n));\n" + "ensures $eq.ref.bool(n, $0.ref) ==> p == $0.ref;\n" "ensures !old($Alloc[p]);\n" - "ensures (forall q: ref :: old($Alloc[q]) ==> ($slt.ref.bool($add.ref(p, n), q) || $sgt.ref.bool(p, $add.ref(q, $Size[q]))));\n" + "ensures (forall q: ref :: old($Alloc[q]) ==> ($slt.ref.bool($add.ref(p, n), q) || $slt.ref.bool($add.ref(q, $Size[q]), p)));\n" "ensures $Alloc[p];\n" "ensures $Size[p] == n;\n" "ensures (forall q: ref :: {$Size[q]} q != p ==> $Size[q] == old($Size[q]));\n" "ensures (forall q: ref :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n" - "ensures $sge.ref.bool(n, $0.ref) ==> (forall q: ref :: {$base(q)} $sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n"); + "ensures (forall q: ref :: {$base(q)} $sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n"); D("procedure $free(p: ref);\n" "modifies $Alloc, $allocatedCounter;\n" "requires $eq.ref.bool(p, $0.ref) || ($eq.ref.bool($base(p), p) && $Alloc[p]);\n" - "requires $sgt.ref.bool(p, $0.ref);\n" + "requires $slt.ref.bool($0.ref, p);\n" "ensures $ne.ref.bool(p, $0.ref) ==> !$Alloc[p];\n" "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n" "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == old($allocatedCounter) - 1;\n"); @@ -2118,7 +1667,7 @@ void __SMACK_decls() { D("var $CurrAddr:ref;\n"); D("procedure $galloc(base_addr: ref, size: ref);\n" - "modifies $Alloc;" + "modifies $Alloc;\n" "ensures $Size(base_addr) == size;\n" "ensures (forall addr: ref :: {$base(addr)} $sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, size)) ==> $base(addr) == base_addr);\n" "ensures $Alloc[base_addr];\n" @@ -2126,20 +1675,20 @@ void __SMACK_decls() { 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" - "ensures $sgt.ref.bool(n, $0.ref) ==> $Size(p) == n;\n" - "ensures $sgt.ref.bool(n, $0.ref) ==> (forall q: ref :: {$base(q)} $sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n" - "ensures !$sgt.ref.bool(n, $0.ref) ==> $sle.ref.bool($add.ref(old($CurrAddr), $1.ref), $CurrAddr);\n" - "ensures !$sgt.ref.bool(n, $0.ref) ==> $Size(p) == $1.ref;\n" - "ensures !$sgt.ref.bool(n, $0.ref) ==> $eq.ref.bool($base(p), p);\n" - "ensures $Alloc[p];\n" + "ensures $sle.ref.bool($0.ref, n);\n" + "ensures $slt.ref.bool($0.ref, n) ==> $sge.ref.bool($sub.ref($CurrAddr, n), old($CurrAddr)) && p == old($CurrAddr);\n" + "ensures $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP);\n" + "ensures $slt.ref.bool($0.ref, n) ==> $Size(p) == n;\n" + "ensures $slt.ref.bool($0.ref, n) ==> (forall q: ref :: {$base(q)} $sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n" + "ensures $slt.ref.bool($0.ref, n) ==> $Alloc[p];\n" + "ensures $eq.ref.bool(n, $0.ref) ==> old($CurrAddr) == $CurrAddr && p == $0.ref;\n" + "ensures $eq.ref.bool(n, $0.ref)==> $Alloc[p] == old($Alloc)[p];\n" "ensures (forall q: ref :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n"); D("procedure $free(p: ref);\n" "modifies $Alloc, $allocatedCounter;\n" "requires $eq.ref.bool(p, $0.ref) || ($eq.ref.bool($base(p), p) && $Alloc[p]);\n" - "requires $sgt.ref.bool(p, $0.ref);\n" + "requires $slt.ref.bool($0.ref, p);\n" "ensures $ne.ref.bool(p, $0.ref) ==> !$Alloc[p];\n" "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: {$Alloc[q]} q != p ==> $Alloc[q] == old($Alloc[q]));\n" "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == old($allocatedCounter) - 1;\n"); @@ -2157,13 +1706,14 @@ void __SMACK_decls() { D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n" "modifies $CurrAddr;\n" "{\n" - " p := $CurrAddr;\n" - " havoc $CurrAddr;\n" + " assume $sge.ref.bool(n, $0.ref);\n" " if ($sgt.ref.bool(n, $0.ref)) {\n" + " p := $CurrAddr;\n" + " havoc $CurrAddr;\n" " assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n" " assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP);\n" " } else {\n" - " assume $sle.ref.bool($add.ref(p, $1.ref), $CurrAddr);\n" + " p := $0.ref;\n" " }\n" "}\n"); @@ -2175,10 +1725,11 @@ void __SMACK_decls() { 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" + "ensures $sle.ref.bool($0.ref, n);\n" + "ensures $slt.ref.bool($0.ref, n) ==> $slt.ref.bool($0.ref, p) && $slt.ref.bool(p, $sub.ref($MALLOC_TOP, n));\n" + "ensures $eq.ref.bool(n, $0.ref) ==> p == $0.ref;\n" "ensures !old($Alloc[p]);\n" - "ensures (forall q: ref :: old($Alloc[q]) ==> ($slt.ref.bool($add.ref(p, n), q) || $sgt.ref.bool(p, $add.ref(q, $Size[q]))));\n" + "ensures (forall q: ref :: old($Alloc[q]) ==> ($slt.ref.bool($add.ref(p, n), q) || $slt.ref.bool($add.ref(q, $Size[q]), p)));\n" "ensures $Alloc[p];\n" "ensures $Size[p] == n;\n" "ensures (forall q: ref :: {$Size[q]} q != p ==> $Size[q] == old($Size[q]));\n" @@ -2194,9 +1745,10 @@ void __SMACK_decls() { 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" - "ensures !$sgt.ref.bool(n, $0.ref) ==> $sle.ref.bool($add.ref(old($CurrAddr), $1.ref), $CurrAddr);\n"); + "ensures $sle.ref.bool($0.ref, n);\n" + "ensures $slt.ref.bool($0.ref, n) ==> $sge.ref.bool($sub.ref($CurrAddr, n), old($CurrAddr)) && p == old($CurrAddr);\n" + "ensures $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, $MALLOC_TOP);\n" + "ensures $eq.ref.bool(n, $0.ref) ==> old($CurrAddr) == $CurrAddr && p == $0.ref;\n"); D("procedure $free(p: ref);\n"); #endif @@ -2209,7 +1761,7 @@ void __SMACK_decls() { // The size parameter represents number of bytes that are being accessed void __SMACK_check_memory_safety(void* pointer, unsigned long size) { void* sizeRef = (void*)size; - __SMACK_code("assert {:valid_deref} $Alloc[$base(@)] == true;", pointer); + __SMACK_code("assert {:valid_deref} $Alloc[$base(@)];", pointer); __SMACK_code("assert {:valid_deref} $sle.ref.bool($base(@), @);", pointer, pointer); #if MEMORY_MODEL_NO_REUSE_IMPLS __SMACK_code("assert {:valid_deref} $sle.ref.bool($add.ref(@, @), $add.ref($base(@), $Size($base(@))));", pointer, sizeRef, pointer, pointer); @@ -2220,7 +1772,7 @@ void __SMACK_check_memory_safety(void* pointer, unsigned long size) { #endif } -void __SMACK_check_memory_leak() { +void __SMACK_check_memory_leak(void) { __SMACK_code("assert {:valid_memtrack} $allocatedCounter == 0;"); } #endif @@ -2233,94 +1785,3 @@ void __SMACK_init_func_memory_model(void) { __SMACK_code("$allocatedCounter := 0;"); #endif } - - -#if MEMORY_SAFETY || SIGNED_INTEGER_OVERFLOW_CHECK -char *strcpy(char *dest, const char *src) { - char *save = dest; - while (*dest++ = *src++); - return save; -} - -size_t strlen(const char *str) { - size_t count = 0; - while (str[count] != 0) count++; - return count; -} - -char *strrchr(const char *src, int c) { - char *result = (char *)0; - - while (*src != 0) { - if (*src == c) { - result = src; - } - src++; - } - return result; -} - -size_t strspn(const char *cs, const char *ct) { - size_t n; - const char *p; - for (n = 0; *cs; cs++, n++) { - for (p = ct; *p && *p != *cs; p++); - if (!*p) break; - } - return n; -} - -unsigned long int strtoul(const char *nptr, char **endptr, int base) { - if (__VERIFIER_nondet_int()) { - if (endptr != 0) { - *endptr = nptr; - } - return 0; - } else { - if (endptr != 0) { - size_t size = strlen(nptr); - *endptr = nptr + size; - } - return __VERIFIER_nondet_ulong(); - } -} - -double strtod(const char *nptr, char **endptr) { - if (__VERIFIER_nondet_int()) { - if (endptr != 0) { - *endptr = nptr; - } - return 0.0; - } else { - if (endptr != 0) { - size_t size = strlen(nptr); - *endptr = nptr + size; - } - return __VERIFIER_nondet_long(); - } -} - -char *error_str = "xx"; -char *strerror(int errnum) { - error_str[0] = __VERIFIER_nondet_char(); - error_str[1] = __VERIFIER_nondet_char(); - 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); -} -#endif - diff --git a/share/smack/lib/string.c b/share/smack/lib/string.c new file mode 100644 index 000000000..946a5213d --- /dev/null +++ b/share/smack/lib/string.c @@ -0,0 +1,92 @@ +// This file is distributed under the MIT License. See LICENSE for details. +// + +#include +#include + +char *strcpy(char *dest, const char *src) { + char *save = dest; + while (*dest++ = *src++); + return save; +} + +size_t strlen(const char *str) { + size_t count = 0; + while (str[count] != 0) count++; + return count; +} + +char *strrchr(const char *src, int c) { + char *result = (char *)0; + + while (*src != 0) { + if (*src == c) { + result = src; + } + src++; + } + return result; +} + +size_t strspn(const char *cs, const char *ct) { + size_t n; + const char *p; + for (n = 0; *cs; cs++, n++) { + for (p = ct; *p && *p != *cs; p++); + if (!*p) break; + } + return n; +} + +unsigned long int strtoul(const char *nptr, char **endptr, int base) { + if (__VERIFIER_nondet_int()) { + if (endptr != 0) { + *endptr = nptr; + } + return 0; + } else { + if (endptr != 0) { + size_t size = strlen(nptr); + *endptr = nptr + size; + } + return __VERIFIER_nondet_ulong(); + } +} + +double strtod(const char *nptr, char **endptr) { + if (__VERIFIER_nondet_int()) { + if (endptr != 0) { + *endptr = nptr; + } + return 0.0; + } else { + if (endptr != 0) { + size_t size = strlen(nptr); + *endptr = nptr + size; + } + return __VERIFIER_nondet_long(); + } +} + +char *error_str = "xx"; +char *strerror(int errnum) { + error_str[0] = __VERIFIER_nondet_char(); + error_str[1] = __VERIFIER_nondet_char(); + 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 0b39400c8..5c6063456 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '1.8.1' +VERSION = '1.9.0' def reachParser(): parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()]) diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 5f6a64583..d4d113b3f 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -36,7 +36,7 @@ def svcomp_frontend(args): args.bit_precise = True args.bit_precise_pointers = True #args.verifier = 'boogie' - args.time_limit = 890 + args.time_limit = 1000 args.unroll = 100 args.execute = executable else: @@ -49,6 +49,7 @@ def svcomp_frontend(args): name, ext = os.path.splitext(os.path.basename(args.input_files[0])) svcomp_process_file(args, name, ext) + args.clang_options += " -DSVCOMP" args.clang_options += " -DAVOID_NAME_CONFLICTS" args.clang_options += " -DCUSTOM_VERIFIER_ASSERT" args.clang_options += " -DNO_FORALL" @@ -282,10 +283,10 @@ def verify_bpl_svcomp(args): elif "printf_false-unreach-call" in bpl or "echo_true-no-overflow" in bpl: heurTrace += "BusyBox benchmark detected. Setting loop unroll bar to 11.\n" loopUnrollBar = 11 - elif args.memory_safety and "__main(argc:" in bpl: + elif args.memory_safety and "__main($i0" in bpl: heurTrace += "BusyBox memory safety benchmark detected. Setting loop unroll bar to 4.\n" loopUnrollBar = 4 - elif args.signed_integer_overflow and "__main(argc:" in bpl: + elif args.signed_integer_overflow and "__main($i0" in bpl: heurTrace += "BusyBox overflows benchmark detected. Setting loop unroll bar to 4.\n" loopUnrollBar = 4 elif args.signed_integer_overflow and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl): diff --git a/share/smack/top.py b/share/smack/top.py index ca69d269c..753d08543 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -7,12 +7,14 @@ import re import shutil import sys +import shlex +import subprocess 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.8.1' +VERSION = '1.9.0' def frontends(): """A dictionary of front-ends per file extension.""" @@ -91,6 +93,9 @@ def arguments(): noise_group.add_argument('-d', '--debug', action="store_true", default=False, help='enable debugging output') + noise_group.add_argument('--debug-only', metavar='MODULES', default=None, + type=str, help='limit debugging output to given MODULES') + parser.add_argument('-t', '--no-verify', action="store_true", default=False, help='perform only translation, without verification.') @@ -143,6 +148,9 @@ def arguments(): translate_group.add_argument('--bit-precise', action="store_true", default=False, help='enable bit precision for non-pointer values') + translate_group.add_argument('--timing-annotations', action="store_true", default=False, + help='enable timing annotations') + translate_group.add_argument('--bit-precise-pointers', action="store_true", default=False, help='enable bit precision for pointer values') @@ -170,6 +178,9 @@ def arguments(): translate_group.add_argument('--float', action="store_true", default=False, help='enable bit-precise floating-point functions') + translate_group.add_argument('--split-aggregate-values', action='store_true', default=False, + help='enable splitting of load/store instructions of LLVM aggregate types') + verifier_group = parser.add_argument_group('verifier options') @@ -208,6 +219,14 @@ def arguments(): verifier_group.add_argument('--replay', action="store_true", default=False, help='enable reply of error trace with test harness.') + plugins_group = parser.add_argument_group('plugins') + + plugins_group.add_argument('--transform-bpl', metavar='COMMAND', default=None, + type=str, help='transform generated Boogie code via COMMAND') + + plugins_group.add_argument('--transform-out', metavar='COMMAND', default=None, + type=str, help='transform verifier output via COMMAND') + args = parser.parse_args() if not args.bc_file: @@ -262,15 +281,24 @@ def frontend(args): def smack_root(): return os.path.dirname(os.path.dirname(os.path.abspath(sys.argv[0]))) -def smack_headers(): +def smack_header_path(): return os.path.join(smack_root(), 'share', 'smack', 'include') +def smack_headers(): + paths = [] + paths.append(smack_header_path()) + if args.memory_safety or args.signed_integer_overflow: + paths.append(os.path.join(smack_header_path(), 'string')) + if args.float: + paths.append(os.path.join(smack_header_path(), 'math')) + return paths + def smack_lib(): return os.path.join(smack_root(), 'share', 'smack', 'lib') def default_clang_compile_command(args, lib = False): cmd = ['clang', '-c', '-emit-llvm', '-O0', '-g', '-gcolumn-info'] - cmd += ['-I' + smack_headers()] + cmd += map(lambda path: '-I' + path, smack_headers()) cmd += args.clang_options.split() cmd += ['-DMEMORY_MODEL_' + args.mem_mod.upper().replace('-','_')] if args.memory_safety: cmd += ['-DMEMORY_SAFETY'] @@ -286,6 +314,12 @@ def build_libs(args): if args.pthread: libs += ['pthread.c'] + if args.memory_safety or args.signed_integer_overflow: + libs += ['string.c'] + + if args.float: + libs += ['math.c'] + for c in map(lambda c: os.path.join(smack_lib(), c), libs): bc = temporary_file(os.path.splitext(os.path.basename(c))[0], '.bc', args) try_command(default_clang_compile_command(args, True) + ['-o', bc, c]) @@ -358,10 +392,12 @@ def llvm_to_bpl(args): for ep in args.entry_points: cmd += ['-entry-points', ep] if args.debug: cmd += ['-debug'] + if args.debug_only: cmd += ['-debug-only', args.debug_only] if args.ll_file: cmd += ['-ll', args.ll_file] if "impls" in args.mem_mod:cmd += ['-mem-mod-impls'] if args.static_unroll: cmd += ['-static-unroll'] if args.bit_precise: cmd += ['-bit-precise'] + if args.timing_annotations: cmd += ['-timing-annotations'] if args.bit_precise_pointers: cmd += ['-bit-precise-pointers'] if args.no_byte_access_inference: cmd += ['-no-byte-access-inference'] if args.no_memory_splitting: cmd += ['-no-memory-splitting'] @@ -369,9 +405,11 @@ def llvm_to_bpl(args): if args.signed_integer_overflow: cmd += ['-signed-integer-overflow'] if args.float: cmd += ['-float'] if args.modular: cmd += ['-modular'] + if args.split_aggregate_values: cmd += ['-split-aggregate-values'] try_command(cmd, console=True) annotate_bpl(args) property_selection(args) + transform_bpl(args) def procedure_annotation(name, args): if name in args.entry_points: @@ -425,6 +463,22 @@ def replace_assertion(m): line = re.sub(r'^(\s*assert\s*)({:(.+)})?(.+);', replace_assertion, line) f.write(line) +def transform_bpl(args): + if args.transform_bpl: + with open(args.bpl_file, 'r+') as bpl: + old = bpl.read() + bpl.seek(0) + bpl.truncate() + tx = subprocess.Popen(shlex.split(args.transform_bpl), stdin=subprocess.PIPE, stdout=bpl) + tx.communicate(input = old) + +def transform_out(args, old): + out = old + if args.transform_out: + tx = subprocess.Popen(shlex.split(args.transform_out), stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + out, err = tx.communicate(input = old) + return out + def verification_result(verifier_output): if re.search(r'[1-9]\d* time out|Z3 ran out of resources|timed out', verifier_output): return 'timeout' @@ -492,6 +546,7 @@ def verify_bpl(args): command += args.verifier_options.split() verifier_output = try_command(command, timeout=args.time_limit) + verifier_output = transform_out(args, verifier_output) result = verification_result(verifier_output) if args.smackd: 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 68bbc385e..24b03b6f3 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.8.1' + return '1.9.0' def name(self): """ diff --git a/test/basic/checking.c b/test/basic/checking.c new file mode 100644 index 000000000..2d1525cac --- /dev/null +++ b/test/basic/checking.c @@ -0,0 +1,17 @@ +#include +#include +#include "smack.h" + +// @expect error +// @checkbpl grep "call foo" +// @checkout grep "checking.c(11,1)" + +void foo(void) { + +} + +int main(void) { + foo(); + assert(0); + return 0; +} diff --git a/test/basic/checking_invert_bpl.c b/test/basic/checking_invert_bpl.c new file mode 100644 index 000000000..b5249c9ca --- /dev/null +++ b/test/basic/checking_invert_bpl.c @@ -0,0 +1,17 @@ +#include +#include +#include "smack.h" + +// @expect error +// @checkbpl grep -v "call bar" +// @checkout grep "checking_invert_bpl.c(11,1)" + +void foo(void) { + +} + +int main(void) { + foo(); + assert(0); + return 0; +} diff --git a/test/basic/checking_invert_out.c b/test/basic/checking_invert_out.c new file mode 100644 index 000000000..41b746fca --- /dev/null +++ b/test/basic/checking_invert_out.c @@ -0,0 +1,17 @@ +#include +#include +#include "smack.h" + +// @expect error +// @checkbpl grep "call foo" +// @checkout grep -v "checking_invert_out.c(10,1)" + +void foo(void) { + +} + +int main(void) { + foo(); + assert(0); + return 0; +} diff --git a/test/basic/func_ptr_alias.c b/test/basic/func_ptr_alias.c index d2f582ace..c09f58a27 100644 --- a/test/basic/func_ptr_alias.c +++ b/test/basic/func_ptr_alias.c @@ -6,7 +6,11 @@ int __incr(int x) { return x + 1; } +#ifdef __MACH__ +int (*incr)(int) = __incr; +#else int incr(int) __attribute__((alias ("__incr"))); +#endif int main(void) { int x = __VERIFIER_nondet_int(); diff --git a/test/basic/func_ptr_alias1.c b/test/basic/func_ptr_alias1.c index bea21dab2..18e77e53e 100644 --- a/test/basic/func_ptr_alias1.c +++ b/test/basic/func_ptr_alias1.c @@ -10,8 +10,13 @@ int __decr(int x) { return --x; } +#ifdef __MACH__ +int (*incr)(int) = __incr; +int (*decr)(int) = __decr; +#else int incr(int) __attribute__((alias ("__incr"))); int decr(int) __attribute__((alias ("__decr"))); +#endif int main(void) { int (*fp)(int); diff --git a/test/basic/func_ptr_alias1_fail.c b/test/basic/func_ptr_alias1_fail.c index 93ed32787..4c23ac4fe 100644 --- a/test/basic/func_ptr_alias1_fail.c +++ b/test/basic/func_ptr_alias1_fail.c @@ -10,8 +10,13 @@ int __decr(int x) { return --x; } +#ifdef __MACH__ +int (*incr)(int) = __incr; +int (*decr)(int) = __decr; +#else int incr(int) __attribute__((alias ("__incr"))); int decr(int) __attribute__((alias ("__decr"))); +#endif int main(void) { int (*fp)(int); diff --git a/test/basic/func_ptr_alias_fail.c b/test/basic/func_ptr_alias_fail.c index 74bc1b0f6..7e4d4a614 100644 --- a/test/basic/func_ptr_alias_fail.c +++ b/test/basic/func_ptr_alias_fail.c @@ -6,7 +6,11 @@ int __incr(int x) { return x + 2; } +#ifdef __MACH__ +int (*incr)(int) = __incr; +#else int incr(int) __attribute__((alias ("__incr"))); +#endif int main(void) { int x = __VERIFIER_nondet_int(); diff --git a/test/basic/limits.c b/test/basic/limits.c new file mode 100644 index 000000000..f7ab33414 --- /dev/null +++ b/test/basic/limits.c @@ -0,0 +1,97 @@ +#include +#include "smack.h" + +// @expect verified + +int main(void) { + char x1 = __VERIFIER_nondet_char(); + assert(x1 >= SCHAR_MIN && x1 <= SCHAR_MAX); + + signed char x2 = __VERIFIER_nondet_signed_char(); + assert(x2 >= SCHAR_MIN && x2 <= SCHAR_MAX); + + unsigned char x3 = __VERIFIER_nondet_unsigned_char(); + assert(x3 >= 0 && x3 <= UCHAR_MAX); + + short x4 = __VERIFIER_nondet_short(); + assert(x4 >= SHRT_MIN && x4 <= SHRT_MAX); + + signed short x5 = __VERIFIER_nondet_signed_short(); + assert(x5 >= SHRT_MIN && x5 <= SHRT_MAX); + + signed short int x6 = __VERIFIER_nondet_signed_short_int(); + assert(x6 >= SHRT_MIN && x6 <= SHRT_MAX); + + unsigned short x7 = __VERIFIER_nondet_unsigned_short(); + assert(x7 >= 0 && x7 <= USHRT_MAX); + + unsigned short int x8 = __VERIFIER_nondet_unsigned_short_int(); + assert(x8 >= 0 && x8 <= USHRT_MAX); + + int x9 = __VERIFIER_nondet_int(); + assert(x9 >= INT_MIN && x9 <= INT_MAX); + + signed int x10 = __VERIFIER_nondet_signed_int(); + assert(x10 >= INT_MIN && x10 <= INT_MAX); + + unsigned x11 = __VERIFIER_nondet_unsigned(); + assert(x11 >= 0 && x11 <= UINT_MAX); + + unsigned int x12 = __VERIFIER_nondet_unsigned_int(); + assert(x12 >= 0 && x12 <= UINT_MAX); + + long x13 = __VERIFIER_nondet_long(); + assert(x13 >= LONG_MIN && x13 <= LONG_MAX); + + long int x14 = __VERIFIER_nondet_long_int(); + assert(x14 >= LONG_MIN && x14 <= LONG_MAX); + + signed long x15 = __VERIFIER_nondet_signed_long(); + assert(x15 >= LONG_MIN && x15 <= LONG_MAX); + + signed long int x16 = __VERIFIER_nondet_signed_long_int(); + assert(x16 >= LONG_MIN && x16 <= LONG_MAX); + + unsigned long x17 = __VERIFIER_nondet_unsigned_long(); + assert(x17 >= 0 && x17 <= ULONG_MAX); + + unsigned long int x18 = __VERIFIER_nondet_unsigned_long_int(); + assert(x18 >= 0 && x18 <= ULONG_MAX); + + long long x19 = __VERIFIER_nondet_long_long(); + assert(x19 >= LLONG_MIN && x19 <= LLONG_MAX); + + long long int x20 = __VERIFIER_nondet_long_long_int(); + assert(x20 >= LLONG_MIN && x20 <= LLONG_MAX); + + signed long long x21 = __VERIFIER_nondet_signed_long_long(); + assert(x21 >= LLONG_MIN && x21 <= LLONG_MAX); + + signed long long int x22 = __VERIFIER_nondet_signed_long_long_int(); + assert(x22 >= LLONG_MIN && x22 <= LLONG_MAX); + + unsigned long long x23 = __VERIFIER_nondet_unsigned_long_long(); + assert(x23 >= 0 && x23 <= ULLONG_MAX); + + unsigned long long int x24 = __VERIFIER_nondet_unsigned_long_long_int(); + assert(x24 >= 0 && x24 <= ULLONG_MAX); + +// Used in SVCCOMP benchmarks + _Bool x25 = __VERIFIER_nondet_bool(); + assert(x25 == 0 || x25 == 1); + + unsigned char x26 = __VERIFIER_nondet_uchar(); + assert(x26 >= 0 && x26 <= UCHAR_MAX); + + unsigned short x27 = __VERIFIER_nondet_ushort(); + assert(x27 >= 0 && x27 <= USHRT_MAX); + + unsigned int x28 = __VERIFIER_nondet_uint(); + assert(x28 >= 0 && x28 <= UINT_MAX); + + unsigned long x29 = __VERIFIER_nondet_ulong(); + assert(x29 >= 0 && x29 <= ULONG_MAX); + + return 0; +} + diff --git a/test/basic/limits_fail.c b/test/basic/limits_fail.c new file mode 100644 index 000000000..ce61725a4 --- /dev/null +++ b/test/basic/limits_fail.c @@ -0,0 +1,97 @@ +#include +#include "smack.h" + +// @expect error + +int main(void) { + char x1 = __VERIFIER_nondet_char(); + assert(x1 >= SCHAR_MIN && x1 <= SCHAR_MAX); + + signed char x2 = __VERIFIER_nondet_signed_char(); + assert(x2 >= SCHAR_MIN && x2 <= SCHAR_MAX); + + unsigned char x3 = __VERIFIER_nondet_unsigned_char(); + assert(x3 >= 0 && x3 <= UCHAR_MAX); + + short x4 = __VERIFIER_nondet_short(); + assert(x4 >= SHRT_MIN && x4 <= SHRT_MAX); + + signed short x5 = __VERIFIER_nondet_signed_short(); + assert(x5 >= SHRT_MIN && x5 <= SHRT_MAX); + + signed short int x6 = __VERIFIER_nondet_signed_short_int(); + assert(x6 >= SHRT_MIN && x6 <= SHRT_MAX); + + unsigned short x7 = __VERIFIER_nondet_unsigned_short(); + assert(x7 >= 0 && x7 <= USHRT_MAX); + + unsigned short int x8 = __VERIFIER_nondet_unsigned_short_int(); + assert(x8 >= 0 && x8 <= USHRT_MAX); + + int x9 = __VERIFIER_nondet_int(); + assert(x9 >= INT_MIN && x9 <= INT_MAX); + + signed int x10 = __VERIFIER_nondet_signed_int(); + assert(x10 >= INT_MIN && x10 <= INT_MAX); + + unsigned x11 = __VERIFIER_nondet_unsigned(); + assert(x11 >= 0 && x11 <= UINT_MAX); + + unsigned int x12 = __VERIFIER_nondet_unsigned_int(); + assert(x12 >= 0 && x12 <= UINT_MAX); + + long x13 = __VERIFIER_nondet_long(); + assert(x13 >= LONG_MIN && x13 <= LONG_MAX); + + long int x14 = __VERIFIER_nondet_long_int(); + assert(x14 >= LONG_MIN && x14 <= LONG_MAX); + + signed long x15 = __VERIFIER_nondet_signed_long(); + assert(x15 >= LONG_MIN && x15 <= LONG_MAX); + + signed long int x16 = __VERIFIER_nondet_signed_long_int(); + assert(x16 >= LONG_MIN && x16 <= LONG_MAX); + + unsigned long x17 = __VERIFIER_nondet_unsigned_long(); + assert(x17 >= 0 && x17 <= ULONG_MAX); + + unsigned long int x18 = __VERIFIER_nondet_unsigned_long_int(); + assert(x18 >= 0 && x18 <= ULONG_MAX); + + long long x19 = __VERIFIER_nondet_long_long(); + assert(x19 >= LLONG_MIN && x19 <= LLONG_MAX); + + long long int x20 = __VERIFIER_nondet_long_long_int(); + assert(x20 >= LLONG_MIN && x20 <= LLONG_MAX); + + signed long long x21 = __VERIFIER_nondet_signed_long_long(); + assert(x21 >= LLONG_MIN && x21 <= LLONG_MAX); + + signed long long int x22 = __VERIFIER_nondet_signed_long_long_int(); + assert(x22 >= LLONG_MIN && x22 <= LLONG_MAX); + + unsigned long long x23 = __VERIFIER_nondet_unsigned_long_long(); + assert(x23 >= 0 && x23 <= ULLONG_MAX); + + unsigned long long int x24 = __VERIFIER_nondet_unsigned_long_long_int(); + assert(x24 >= 0 && x24 <= ULLONG_MAX); + +// Used in SVCCOMP benchmarks + _Bool x25 = __VERIFIER_nondet_bool(); + assert(x25 == 0 || x25 == 1); + + unsigned char x26 = __VERIFIER_nondet_uchar(); + assert(x26 >= 0 && x26 <= UCHAR_MAX); + + unsigned short x27 = __VERIFIER_nondet_ushort(); + assert(x27 >= 0 && x27 <= USHRT_MAX); + + unsigned int x28 = __VERIFIER_nondet_uint(); + assert(x28 >= 0 && x28 <= UINT_MAX); + + unsigned long x29 = __VERIFIER_nondet_ulong(); + assert(x29 >= 1 && x29 <= ULONG_MAX); + + return 0; +} + diff --git a/test/basic/split_aggregate_values.c b/test/basic/split_aggregate_values.c new file mode 100644 index 000000000..6b65460de --- /dev/null +++ b/test/basic/split_aggregate_values.c @@ -0,0 +1,26 @@ +#include "smack.h" + +// The assertion will fail without flag `--split-aggregate-values`. + +// @flag --split-aggregate-values +// @expect verified + +typedef struct { + int x; + int y; + int z; +} S; + +S foo() { + S s; + s.x = 1; + s.y = 2; + s.z = 3; + return s; +} + +int main() { + S s = foo(); + assert(s.z == 3); + return 0; +} diff --git a/test/basic/split_aggregate_values_fail.c b/test/basic/split_aggregate_values_fail.c new file mode 100644 index 000000000..1c44e8bd6 --- /dev/null +++ b/test/basic/split_aggregate_values_fail.c @@ -0,0 +1,24 @@ +#include "smack.h" + +// @flag --split-aggregate-values +// @expect error + +typedef struct { + int x; + int y; + int z; +} S; + +S foo() { + S s; + s.x = 1; + s.y = 2; + s.z = 3; + return s; +} + +int main() { + S s = foo(); + assert(s.z == 2); + return 0; +} diff --git a/test/basic/struct_alias.c b/test/basic/struct_alias.c new file mode 100644 index 000000000..9fa3dba80 --- /dev/null +++ b/test/basic/struct_alias.c @@ -0,0 +1,36 @@ +#include + +// @expect verified + +struct S { + int w; +}; + +struct T { + int x; + struct S y; + struct S z; +}; + +void f(struct S *state) +{ + state->w = 0; +} + +void g(struct S *state) +{ + state->w = 1; +} + +int main(void) { + struct T t; + + f(&t.y); + f(&t.z); + g(&t.z); + + assert(t.y.w == 0); + assert(t.z.w == 1); + + return 0; +} diff --git a/test/basic/struct_alias_fail.c b/test/basic/struct_alias_fail.c new file mode 100644 index 000000000..086483c36 --- /dev/null +++ b/test/basic/struct_alias_fail.c @@ -0,0 +1,35 @@ +#include + +// @expect error + +struct S { + int w; +}; + +struct T { + int x; + struct S y; + struct S z; +}; + +void f(struct S *state) +{ + state->w = 0; +} + +void g(struct S *state) +{ + state->w = 1; +} + +int main(void) { + struct T t; + + f(&t.y); + f(&t.z); + g(&t.z); + + assert(t.y.w == 1); + + return 0; +} diff --git a/test/basic/struct_const_return.c b/test/basic/struct_const_return.c new file mode 100644 index 000000000..f70ad49a6 --- /dev/null +++ b/test/basic/struct_const_return.c @@ -0,0 +1,21 @@ +#include "smack.h" + +// @flag --clang-options=-O1 +// @expect verified + +typedef struct { + int a; + long b; +} S; + +S foo() { + S x = {1, 2L}; + assert(1); + return x; +} + +int main() { + S y = foo(); + assert(y.a == 1); + return 0; +} diff --git a/test/basic/struct_const_return_fail.c b/test/basic/struct_const_return_fail.c new file mode 100644 index 000000000..54c48ecb7 --- /dev/null +++ b/test/basic/struct_const_return_fail.c @@ -0,0 +1,21 @@ +#include "smack.h" + +// @flag --clang-options=-O1 +// @expect error + +typedef struct { + int a; + long b; +} S; + +S foo() { + S x = {1, 2L}; + assert(1); + return x; +} + +int main() { + S y = foo(); + assert(y.a == 3); + return 0; +} diff --git a/test/basic/timing-annotations.c b/test/basic/timing-annotations.c new file mode 100644 index 000000000..dcadf7fc8 --- /dev/null +++ b/test/basic/timing-annotations.c @@ -0,0 +1,24 @@ +#include +#include +#include "smack.h" + +//This test ensures that the timing-annotations are respected +//and show up in the generated boogie. +//Currently, we just do the simplest thing and make sure that +//there is at least one instruction with expected cost. + +// @flag --timing-annotations +// @expect verified +// @checkbpl grep "smack.InstTimingCost.Int64 1" + +int foo(int a, int b) { + return a + b; +} + +int main(void) { + int a = 10; + int b = 9; + int c = foo(a,b); + assert(c != 0); + return 0; +} diff --git a/test/basic/transform-bpl.c b/test/basic/transform-bpl.c new file mode 100644 index 000000000..af998879a --- /dev/null +++ b/test/basic/transform-bpl.c @@ -0,0 +1,21 @@ +#include +#include +#include "smack.h" + +// @expect verified +// @flag --transform-bpl "sed 's/\(call .*\) bar/\1 foo/'" + +int foo(void) { + return 0; +} + +int bar(void) { + return 1; +} + +int main(void) { + int x = foo(); + int y = bar(); + assert (y == 0); + return 0; +} diff --git a/test/basic/transform-out.c b/test/basic/transform-out.c new file mode 100644 index 000000000..eca04b279 --- /dev/null +++ b/test/basic/transform-out.c @@ -0,0 +1,11 @@ +#include +#include +#include "smack.h" + +// @expect verified +// @flag --transform-out "sed -e 's/[[:digit:]]* verified, [[:digit:]]* error/1 verified, 0 errors/' -e 's/can fail/no bugs/'" + +int main(void) { + assert (0); + return 0; +} diff --git a/test/bits/config.yml b/test/bits/config.yml index 295e1f394..c1ce00c1a 100644 --- a/test/bits/config.yml +++ b/test/bits/config.yml @@ -1,2 +1,2 @@ flags: [--bit-precise] -time-limit: 240 +time-limit: 90 diff --git a/test/bits/interleave_bits_fail.c b/test/bits/interleave_bits_fail.c index 740ccfaff..f68d840b1 100644 --- a/test/bits/interleave_bits_fail.c +++ b/test/bits/interleave_bits_fail.c @@ -1,8 +1,8 @@ /* https://graphics.stanford.edu/~seander/bithacks.html#InterleaveTableObvious */ #include "smack.h" -// @flag --loop-limit=33 -// @flag --unroll=33 +// @flag --loop-limit=17 +// @flag --unroll=17 // @expect error int main() @@ -19,7 +19,7 @@ int main() unsigned int z = 0; /* z gets the resulting Morton Number. */ unsigned int i = 0; - while (i < 32U) { + while (i < sizeof(x) * 8) { z |= ((x & (1U << i)) << i) | ((y & (1U << i)) << (i + 1)); i += 1U; } diff --git a/test/bits/interleave_bits_true.c b/test/bits/interleave_bits_true.c index 8a1c30f08..6067a6850 100644 --- a/test/bits/interleave_bits_true.c +++ b/test/bits/interleave_bits_true.c @@ -1,8 +1,8 @@ /* https://graphics.stanford.edu/~seander/bithacks.html#InterleaveTableObvious */ #include "smack.h" -// @flag --loop-limit=33 -// @flag --unroll=33 +// @flag --loop-limit=17 +// @flag --unroll=17 // @expect verified int main() @@ -19,7 +19,7 @@ int main() unsigned int z = 0; /* z gets the resulting Morton Number. */ unsigned int i = 0; - while (i < 32U) { + while (i < sizeof(x) * 8) { z |= ((x & (1U << i)) << i) | ((y & (1U << i)) << (i + 1)); i += 1U; } diff --git a/test/bits/malloc_non_alias.c b/test/bits/malloc_non_alias.c new file mode 100644 index 000000000..02f28d33e --- /dev/null +++ b/test/bits/malloc_non_alias.c @@ -0,0 +1,17 @@ +#include "smack.h" +#include + +// @flag --bit-precise-pointers +// @expect verified + +int main() { + int* x = (int*)malloc(sizeof(int)); + int* y = (int*)malloc(sizeof(int)); + int* z = (int*)malloc(sizeof(int)); + if (x == y) + y = z; + *y = 1; + *z = 2; + assert(*y == 1); + return 0; +} diff --git a/test/config.yml b/test/config.yml index 9a11baab8..f703d3d0c 100644 --- a/test/config.yml +++ b/test/config.yml @@ -3,4 +3,6 @@ memory: [no-reuse-impls, no-reuse, reuse] time-limit: 120 memory-limit: 450 flags: [--unroll=2] +checkbpl: [] +checkout: [] skip: false diff --git a/test/float/double_op_fail.c b/test/float/double_op_fail.c index 5bd82899c..c970d87de 100755 --- a/test/float/double_op_fail.c +++ b/test/float/double_op_fail.c @@ -4,7 +4,7 @@ // @expect error -int main() { +int main(void) { double a; double b; double c; diff --git a/test/float/double_ops.c b/test/float/double_ops.c index 5d3fa88fd..9f21e9cb2 100755 --- a/test/float/double_ops.c +++ b/test/float/double_ops.c @@ -4,7 +4,7 @@ // @expect verified -int main() { +int main(void) { double a; double b; double c; diff --git a/test/float/float_op_fail.c b/test/float/float_op_fail.c index 5223e4d0d..1a6165fa2 100755 --- a/test/float/float_op_fail.c +++ b/test/float/float_op_fail.c @@ -4,7 +4,7 @@ // @expect error -int main() { +int main(void) { float a; float b; float c; diff --git a/test/float/float_ops.c b/test/float/float_ops.c index 9f7aff394..4ff824e23 100755 --- a/test/float/float_ops.c +++ b/test/float/float_ops.c @@ -4,7 +4,7 @@ // @expect verified -int main() { +int main(void) { float a; float b; float c; diff --git a/test/float/floats_in_memory.c b/test/float/floats_in_memory.c index ec098421a..42aa97e8d 100644 --- a/test/float/floats_in_memory.c +++ b/test/float/floats_in_memory.c @@ -7,14 +7,14 @@ void ff2(float *f1, float *f2) { *f1 = *f2; } -int main() { +int main(void) { float f1; float f2 = 0.0; float f3 = 1.0; ff1(f1); ff1(f2); - ff2(&f2,&f3); + ff2(&f2, &f3); assert(f2 == f3); diff --git a/test/float/floats_in_memory_fail.c b/test/float/floats_in_memory_fail.c index 0ec43fd68..afd8d638c 100644 --- a/test/float/floats_in_memory_fail.c +++ b/test/float/floats_in_memory_fail.c @@ -7,14 +7,14 @@ void ff2(float *f1, float *f2) { *f1 = *f2 + 2.0f; } -int main() { +int main(void) { float f1; float f2 = 0.0f; float f3 = 1.0f; ff1(f1); ff1(f2); - ff2(&f2,&f3); + ff2(&f2, &f3); assert(f2 == f3); diff --git a/test/float/floor.c b/test/float/floor.c new file mode 100644 index 000000000..a71e2f8fa --- /dev/null +++ b/test/float/floor.c @@ -0,0 +1,20 @@ +#include "smack.h" +#include + +// @expect verified + +int main(void) { + assert(floor(2.7) == 2.0); + assert(floor(-2.7) == -3.0); + double c = floor(-0.0); + assert(c == -0.0); + assert(sizeof(c) == sizeof(float) ? + __signbitf(c) : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c)); + c = floor(-(__builtin_inff())); + assert(sizeof((__builtin_inff())) == sizeof(float) ? __isinff((__builtin_inff())) : + sizeof((__builtin_inff())) == sizeof(double) ? __isinf((__builtin_inff())) : __isinfl((__builtin_inff()))); + assert(sizeof(c) == sizeof(float) ? + __signbitf(c) : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c)); + return 0; +} + diff --git a/test/float/floor_fail.c b/test/float/floor_fail.c new file mode 100644 index 000000000..cbe01e4fc --- /dev/null +++ b/test/float/floor_fail.c @@ -0,0 +1,20 @@ +#include "smack.h" +#include + +// @expect error + +int main(void) { + assert(floor(2.7) == 2.0); + assert(floor(-2.7) == -3.0); + double c = floor(-0.0); + assert(c == -0.0); + assert(sizeof(c) == sizeof(float) ? + __signbitf(c) : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c)); + c = floor(__builtin_inff()); + assert(sizeof((__builtin_inff())) == sizeof(float) ? __isinff((__builtin_inff())) : + sizeof((__builtin_inff())) == sizeof(double) ? __isinf((__builtin_inff())) : __isinfl((__builtin_inff()))); + assert(sizeof(c) == sizeof(float) ? + __signbitf(c) : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c)); + return 0; +} + diff --git a/test/float/simple_double.c b/test/float/simple_double.c index 77c1cd161..6ec9aa9ef 100755 --- a/test/float/simple_double.c +++ b/test/float/simple_double.c @@ -4,7 +4,7 @@ // @expect verified -int main() { +int main(void) { double a; a = 3.0; diff --git a/test/float/simple_double_fail.c b/test/float/simple_double_fail.c index f635ff284..3ad0bb465 100755 --- a/test/float/simple_double_fail.c +++ b/test/float/simple_double_fail.c @@ -4,7 +4,7 @@ // @expect error -int main() { +int main(void) { double a; a = 3.0; diff --git a/test/float/simple_float.c b/test/float/simple_float.c index df492305f..6e92fa91a 100755 --- a/test/float/simple_float.c +++ b/test/float/simple_float.c @@ -4,7 +4,7 @@ // @expect verified -int main() { +int main(void) { float a; a = 3.0f; diff --git a/test/float/simple_float_fail.c b/test/float/simple_float_fail.c index c83953657..cf96cddc9 100755 --- a/test/float/simple_float_fail.c +++ b/test/float/simple_float_fail.c @@ -4,7 +4,7 @@ // @expect error -int main() { +int main(void) { float a; a = 3.0f; diff --git a/test/memory-safety/malloc_nondet.c b/test/memory-safety/malloc_nondet.c new file mode 100644 index 000000000..f4a2b3729 --- /dev/null +++ b/test/memory-safety/malloc_nondet.c @@ -0,0 +1,15 @@ +#include +#include "smack.h" + +// @expect verified + +int main(void) { + int x = __VERIFIER_nondet_int(); + char *p = (char*)malloc(x); + if (p != NULL) { + p[x-1] = x; + free(p); + } + return 0; +} + diff --git a/test/memory-safety/malloc_nondet_fail.c b/test/memory-safety/malloc_nondet_fail.c new file mode 100644 index 000000000..7060b42fd --- /dev/null +++ b/test/memory-safety/malloc_nondet_fail.c @@ -0,0 +1,15 @@ +#include +#include "smack.h" + +// @expect error + +int main(void) { + int x = __VERIFIER_nondet_int(); + char *p = (char*)malloc(x); + if (p != NULL) { + p[x] = x; + free(p); + } + return 0; +} + diff --git a/test/pthread_extras/config.yml b/test/pthread_extras/config.yml index 5adc340a1..055610e53 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: 800 -flags: [--pthread, --context-bound=2] +flags: [--pthread, --context-bound=2, --verifier-options=/trackAllVars] skip: ok diff --git a/test/regtest.py b/test/regtest.py index 70176ade6..374f587c5 100755 --- a/test/regtest.py +++ b/test/regtest.py @@ -15,9 +15,10 @@ import glob import time import sys +import shlex OVERRIDE_FIELDS = ['verifiers', 'memory', 'time-limit', 'memory-limit', 'skip'] -APPEND_FIELDS = ['flags'] +APPEND_FIELDS = ['flags', 'checkbpl', 'checkout'] def bold(text): return '\033[1m' + text + '\033[0m' @@ -77,21 +78,33 @@ def metadata(file): match = re.search(r'@flag (.*)',line) if match: - m['flags'] += [match.group(1).strip()] + m['flags'] += shlex.split(match.group(1).strip()) match = re.search(r'@expect (.*)',line) if match: m['expect'] = match.group(1).strip() - if not m['skip'] and not 'expect' in m: - print red("WARNING: @expect MISSING IN %s" % file, None) - m['expect'] = 'verified' + match = re.search(r'@checkbpl (.*)', line) + if match: + m['checkbpl'].append(match.group(1).strip()) + + match = re.search(r'@checkout (.*)', line) + if match: + m['checkout'].append(match.group(1).strip()) + + if not m['skip']: + if not 'expect' in m: + print red("WARNING: @expect MISSING IN %s" % file, None) + m['expect'] = 'verified' + + if not m['expect'] in ['verified', 'error', 'timeout', 'unknown']: + print red("WARNING: unexpected @expect annotation '%s'" % m['expect'], None) return m # integer constants PASSED = 0; TIMEDOUT = 1; UNKNOWN = 2; FAILED = -1; -def process_test(cmd, test, memory, verifier, expect, log_file): +def process_test(cmd, test, memory, verifier, expect, checkbpl, checkout, log_file): """ This is the worker function for each process. This function process the supplied test and returns a tuple containing indicating the test results. @@ -105,10 +118,24 @@ def process_test(cmd, test, memory, verifier, expect, log_file): p = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) out, err = p.communicate() elapsed = time.time() - t0 + status = 0 + + bplfile = cmd[cmd.index('-bpl')+1] + with open(os.devnull, 'w') as devnull: + for f in checkbpl: + with open(bplfile) as bpl: + checker = subprocess.Popen(shlex.split(f), stdin=bpl, stdout=devnull, stderr=devnull) + checker.wait() + status = status or checker.returncode + + for f in checkout: + checker = subprocess.Popen(shlex.split(f), stdin=subprocess.PIPE, stdout=devnull, stderr=devnull) + checker.communicate(input=out) + status = status or checker.returncode # get the test results result = get_result(out+err) - if result == expect: + if result == expect and status == 0: str_result += green('PASSED ', log_file) elif result == 'timeout': str_result += red('TIMEOUT', log_file) @@ -218,7 +245,7 @@ def main(): cmd += ['-bc', "%s-%s-%s.bc" % (name, memory, verifier)] cmd += ['-bpl', "%s-%s-%s.bpl" % (name, memory, verifier)] r = p.apply_async(process_test, - args=(cmd[:], test, memory, verifier, meta['expect'], args.log_path,), + args=(cmd[:], test, memory, verifier, meta['expect'], meta['checkbpl'], meta['checkout'], args.log_path,), callback=tally_result) results.append(r) diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 2eb5dad5a..61f564be7 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -3,6 +3,8 @@ // This file is distributed under the MIT License. See LICENSE for details. // +#include "llvm/Analysis/TargetLibraryInfo.h" +#include "llvm/Analysis/TargetTransformInfo.h" #include "llvm/LinkAllPasses.h" #include "llvm/IR/LegacyPassManager.h" #include "llvm/IR/LLVMContext.h" @@ -15,10 +17,14 @@ #include "llvm/Support/Signals.h" #include "llvm/Support/SourceMgr.h" #include "llvm/Support/FileSystem.h" +#include "llvm/Support/TargetRegistry.h" +#include "llvm/Support/TargetSelect.h" #include "llvm/Support/ToolOutputFile.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Support/FormattedStream.h" +#include "llvm/Target/TargetMachine.h" +#include "smack/SmackOptions.h" #include "smack/BplFilePrinter.h" #include "smack/SmackModuleGenerator.h" #include "assistDS/StructReturnToPointer.h" @@ -26,12 +32,15 @@ #include "assistDS/SimplifyInsertValue.h" #include "assistDS/MergeGEP.h" #include "assistDS/Devirt.h" +#include "smack/AddTiming.h" #include "smack/CodifyStaticInits.h" #include "smack/RemoveDeadDefs.h" #include "smack/ExtractContracts.h" +#include "smack/VerifierCodeMetadata.h" #include "smack/SimplifyLibCalls.h" #include "smack/MemorySafetyChecker.h" #include "smack/SignedIntegerOverflowChecker.h" +#include "smack/SplitAggregateLoadStore.h" static llvm::cl::opt InputFilename(llvm::cl::Positional, llvm::cl::desc(""), @@ -61,6 +70,10 @@ static llvm::cl::opt Modular("modular", llvm::cl::desc("Enable contracts-based modular deductive verification"), llvm::cl::init(false)); +static llvm::cl::opt +SplitStructs("split-aggregate-values", llvm::cl::desc("Split load/store instructions of LLVM aggregate types"), + llvm::cl::init(false)); + std::string filenamePrefix(const std::string &str) { return str.substr(0, str.find_last_of(".")); } @@ -80,18 +93,50 @@ namespace { exit(1); } } + + // Returns the TargetMachine instance or zero if no triple is provided. + static TargetMachine* GetTargetMachine(Triple TheTriple, StringRef CPUStr, + StringRef FeaturesStr, + const TargetOptions &Options) { + std::string Error; + + StringRef MArch; + + const Target *TheTarget = TargetRegistry::lookupTarget(MArch, TheTriple, + Error); + + assert(TheTarget && "If we don't have a target machine, can't do timing analysis"); + + return TheTarget-> + createTargetMachine(TheTriple.getTriple(), + CPUStr, + FeaturesStr, + Options, + Reloc::Static, /* was getRelocModel(),*/ + CodeModel::Default, /* was CMModel,*/ + CodeGenOpt::None /*GetCodeGenOptLevel())*/ + ); + + } } int main(int argc, char **argv) { llvm::llvm_shutdown_obj shutdown; // calls llvm_shutdown() on exit llvm::cl::ParseCommandLineOptions(argc, argv, "llvm2bpl - LLVM bitcode to Boogie transformation\n"); - llvm::sys::PrintStackTraceOnErrorSignal(); + llvm::sys::PrintStackTraceOnErrorSignal(argv[0]); llvm::PrettyStackTraceProgram PSTP(argc, argv); llvm::EnableDebugBuffering = true; llvm::SMDiagnostic err; - std::unique_ptr module = llvm::parseIRFile(InputFilename, err, llvm::getGlobalContext()); + llvm::LLVMContext Context; + + InitializeAllTargets(); + InitializeAllTargetMCs(); + InitializeAllAsmPrinters(); + InitializeAllAsmParsers(); + + std::unique_ptr module = llvm::parseIRFile(InputFilename, err, Context); if (!err.getMessage().empty()) check("Problem reading input bitcode/IR: " + err.getMessage().str()); @@ -124,6 +169,7 @@ int main(int argc, char **argv) { pass_manager.add(new llvm::SimplifyEV()); pass_manager.add(new llvm::SimplifyIV()); pass_manager.add(new smack::ExtractContracts()); + pass_manager.add(new smack::VerifierCodeMetadata()); pass_manager.add(llvm::createDeadCodeEliminationPass()); pass_manager.add(new smack::CodifyStaticInits()); if (!Modular) { @@ -133,6 +179,9 @@ int main(int argc, char **argv) { // pass_manager.add(new smack::SimplifyLibCalls()); pass_manager.add(new llvm::Devirtualize()); + if (SplitStructs) + pass_manager.add(new smack::SplitAggregateLoadStore()); + if (smack::SmackOptions::MemorySafety) { pass_manager.add(new smack::MemorySafetyChecker()); } @@ -140,6 +189,26 @@ int main(int argc, char **argv) { if (SignedIntegerOverflow) pass_manager.add(new smack::SignedIntegerOverflowChecker()); + + if(smack::SmackOptions::AddTiming){ + Triple ModuleTriple(module->getTargetTriple()); + assert (ModuleTriple.getArch() && "Module has no defined architecture: unable to add timing annotations"); + + const TargetOptions Options; /* = InitTargetOptionsFromCodeGenFlags();*/ + std::string CPUStr = ""; /*getCPUStr();*/ + std::string FeaturesStr = ""; /*getFeaturesStr();*/ + TargetMachine *Machine = GetTargetMachine(ModuleTriple, CPUStr, FeaturesStr, Options); + + assert(Machine && "Module did not have a Target Machine: Cannot set up timing pass"); + // Add an appropriate TargetLibraryInfo pass for the module's triple. + TargetLibraryInfoImpl TLII(ModuleTriple); + pass_manager.add(new TargetLibraryInfoWrapperPass(TLII)); + + // Add internal analysis passes from the target machine. + pass_manager.add(createTargetTransformInfoWrapperPass(Machine->getTargetIRAnalysis())); + pass_manager.add(new smack::AddTiming()); + } + std::vector files; if (!FinalIrFilename.empty()) {