diff --git a/.travis.yml b/.travis.yml index 0ffdfd721..3dd689375 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,6 +1,6 @@ language: generic os: linux -dist: bionic +dist: focal addons: apt: @@ -49,8 +49,8 @@ before_install: install: - source ./bin/versions - wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add - - - sudo add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-${LLVM_SHORT_VERSION} main" - - wget -q https://packages.microsoft.com/config/ubuntu/18.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb + - sudo add-apt-repository "deb http://apt.llvm.org/focal/ llvm-toolchain-focal-${LLVM_SHORT_VERSION} main" + - wget -q https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb - sudo dpkg -i packages-microsoft-prod.deb - sudo apt-get install -y apt-transport-https - sudo apt-get update diff --git a/CMakeLists.txt b/CMakeLists.txt index f6ea010dc..90c1d6b9c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -131,7 +131,9 @@ add_library(smackTranslator STATIC include/smack/VectorOperations.h include/smack/MemorySafetyChecker.h include/smack/IntegerOverflowChecker.h + include/smack/RewriteBitwiseOps.h include/smack/NormalizeLoops.h + include/smack/RustFixes.h include/smack/SplitAggregateValue.h include/smack/Prelude.h include/smack/SmackWarnings.h @@ -155,7 +157,9 @@ add_library(smackTranslator STATIC lib/smack/VectorOperations.cpp lib/smack/MemorySafetyChecker.cpp lib/smack/IntegerOverflowChecker.cpp + lib/smack/RewriteBitwiseOps.cpp lib/smack/NormalizeLoops.cpp + lib/smack/RustFixes.cpp lib/smack/SplitAggregateValue.cpp lib/smack/Prelude.cpp lib/smack/SmackWarnings.cpp @@ -203,5 +207,28 @@ INSTALL(FILES INSTALL(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack DESTINATION share USE_SOURCE_PERMISSIONS - FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile" PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" + FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile" PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml" +) + +INSTALL(FILES + ${CMAKE_CURRENT_SOURCE_DIR}/bin/versions + DESTINATION share/smack + RENAME versions.py +) + +INSTALL(FILES + ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack/Cargo.toml + ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack/build.rs + DESTINATION share/smack/lib +) + +INSTALL(FILES + ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack-rust.c + DESTINATION share/smack/lib/src +) + +INSTALL(FILES + ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack.rs + DESTINATION share/smack/lib/src + RENAME lib.rs ) diff --git a/Doxyfile b/Doxyfile index 9bc8b160c..eb6599c0c 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 2.6.0 +PROJECT_NUMBER = 2.6.1 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/Vagrantfile b/Vagrantfile index bc66fc00b..67b33b4a7 100644 --- a/Vagrantfile +++ b/Vagrantfile @@ -10,7 +10,7 @@ Vagrant.configure(2) do |config| config.vm.synced_folder ".", "/home/vagrant/#{project_name}" config.vm.define :ubuntu do |ubuntu_config| - ubuntu_config.vm.box = "bento/ubuntu-18.04" + ubuntu_config.vm.box = "bento/ubuntu-20.04" end # This provision, 'fix-no-tty', gets rid of an error during build diff --git a/bin/build.sh b/bin/build.sh index 5751c9a3d..6995aabd5 100755 --- a/bin/build.sh +++ b/bin/build.sh @@ -63,7 +63,7 @@ CONFIGURE_INSTALL_PREFIX= CMAKE_INSTALL_PREFIX= # Partial list of dependencies; the rest are added depending on the platform -DEPENDENCIES="git cmake python3-yaml python3-psutil unzip wget ninja-build apt-transport-https dotnet-sdk-3.1 libboost-all-dev" +DEPENDENCIES="git cmake python3-yaml python3-psutil python3-toml unzip wget ninja-build apt-transport-https dotnet-sdk-3.1 libboost-all-dev" shopt -s extglob @@ -201,6 +201,11 @@ linux-@(ubuntu|neon)-18*) DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev" ;; +linux-@(ubuntu|neon)-20*) + Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip" + DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev" + ;; + *) puts "Distribution ${distro} not supported. Manual installation required." exit 1 @@ -237,7 +242,7 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then sudo zypper --non-interactive install ${DEPENDENCIES} ;; - linux-@(ubuntu|neon)-1[68]*) + linux-@(ubuntu|neon)-@(1[68]|20)*) RELEASE_VERSION=$(get-platform-trim "$(lsb_release -r)" | awk -F: '{print $2;}') case "$RELEASE_VERSION" in 16*) @@ -246,6 +251,9 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then 18*) UBUNTU_CODENAME="bionic" ;; + 20*) + UBUNTU_CODENAME="focal" + ;; *) puts "Release ${RELEASE_VERSION} for ${distro} not supported. Dependencies must be installed manually." exit 1 @@ -261,7 +269,7 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main" # Adding .NET repository - ${WGET} -q https://packages.microsoft.com/config/ubuntu/18.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb + ${WGET} -q https://packages.microsoft.com/config/ubuntu/${RELEASE_VERSION}/packages-microsoft-prod.deb -O packages-microsoft-prod.deb sudo dpkg -i packages-microsoft-prod.deb rm -f packages-microsoft-prod.deb sudo apt-get update @@ -327,12 +335,11 @@ fi if [ ${INSTALL_RUST} -eq 1 ] ; then puts "Installing Rust" - ${WGET} https://static.rust-lang.org/dist/${RUST_VERSION}/rust-nightly-x86_64-unknown-linux-gnu.tar.gz -O rust.tar.gz - tar xf rust.tar.gz - cd rust-nightly-x86_64-unknown-linux-gnu - sudo ./install.sh --without=rust-docs - cd .. - rm -rf rust-nightly-x86_64-unknown-linux-gnu rust.tar.gz + if ! [ -x "$(command -v rustup)" ]; then + ${WGET} -O - --secure-protocol=TLSv1_2 https://sh.rustup.rs | bash -s -- -y + source $HOME/.cargo/env + fi + rustup toolchain install ${RUST_VERSION} cargo install rustfilt puts "Installed Rust" fi @@ -463,7 +470,12 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then cd ${SMACK_DIR}/build cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja ninja - sudo ninja install + + if [ -n "${CMAKE_INSTALL_PREFIX}" ] ; then + ninja install + else + sudo ninja install + fi puts "Configuring shell environment" source ${SMACKENV} diff --git a/bin/smack-svcomp-wrapper.sh b/bin/smack-svcomp-wrapper.sh index 2db7b289b..5e3977d55 100755 --- a/bin/smack-svcomp-wrapper.sh +++ b/bin/smack-svcomp-wrapper.sh @@ -3,21 +3,14 @@ # This script has to be copied into the root folder of the SVCOMP package ROOT="$( cd "$(dirname "$(readlink -f "${0}")")" && pwd )" -SMACK_BIN="${ROOT}/smack/bin" -BOOGIE_BIN="${ROOT}/boogie" -CORRAL_BIN="${ROOT}/corral" -LOCKPWN_BIN="${ROOT}/lockpwn" -LLVM_BIN="${ROOT}/llvm/bin" -LLVM_LIB="${ROOT}/llvm/lib" +SMACK_BIN="${ROOT}/bin" +BOOGIE_BIN="${ROOT}/smack-deps/boogie" +CORRAL_BIN="${ROOT}/smack-deps/corral" +Z3_BIN="${ROOT}/smack-deps/z3/bin" +DOTNET_BIN="${ROOT}/smack-deps/dotnet" -# Setting mono heap size to 13GB -export MONO_GC_PARAMS=max-heap-size=13g - -export PATH=${LLVM_BIN}:$SMACK_BIN:$PATH -export BOOGIE="mono ${BOOGIE_BIN}/Boogie.exe" -export CORRAL="mono ${CORRAL_BIN}/corral.exe" -export LOCKPWN="mono ${LOCKPWN_BIN}/lockpwn.exe" -export LD_LIBRARY_PATH=${LLVM_LIB}:$LD_LIBRARY_PATH +export DOTNET_ROOT=${DOTNET_BIN} +export PATH=${DOTNET_BIN}:${SMACK_BIN}:${BOOGIE_BIN}:${CORRAL_BIN}:${Z3_BIN}:$PATH smack -x=svcomp --verifier=svcomp -q $@ diff --git a/bin/versions b/bin/versions index c71e9e983..4bb97308d 100644 --- a/bin/versions +++ b/bin/versions @@ -1,10 +1,10 @@ -Z3_VERSION=4.8.8 -CVC4_VERSION=1.8 -YICES2_VERSION=2.6.2 -BOOGIE_VERSION=2.7.15 -CORRAL_VERSION=1.0.12 -SYMBOOGLIX_COMMIT=ccb2e7f2b3 -LOCKPWN_COMMIT=12ba58f1ec -LLVM_SHORT_VERSION=10 -LLVM_FULL_VERSION=10.0.1 -RUST_VERSION=2020-08-23 +Z3_VERSION="4.8.9" +CVC4_VERSION="1.8" +YICES2_VERSION="2.6.2" +BOOGIE_VERSION="2.7.30" +CORRAL_VERSION="1.0.14" +SYMBOOGLIX_COMMIT="ccb2e7f2b3" +LOCKPWN_COMMIT="12ba58f1ec" +LLVM_SHORT_VERSION="10" +LLVM_FULL_VERSION="10.0.1" +RUST_VERSION="nightly-2020-08-23" \ No newline at end of file diff --git a/examples/rust-cargo/.cargo/config.toml b/examples/rust-cargo/.cargo/config.toml new file mode 100644 index 000000000..b42fc7700 --- /dev/null +++ b/examples/rust-cargo/.cargo/config.toml @@ -0,0 +1,2 @@ +[build] +rustflags = ["-A", "unused-imports", "-C", "opt-level=0", "-g", "--cfg", "verifier=\"smack\"", "--emit=llvm-ir"] diff --git a/examples/rust-cargo/.gitignore b/examples/rust-cargo/.gitignore new file mode 100644 index 000000000..693699042 --- /dev/null +++ b/examples/rust-cargo/.gitignore @@ -0,0 +1,3 @@ +/target +**/*.rs.bk +Cargo.lock diff --git a/examples/rust-cargo/Cargo.toml b/examples/rust-cargo/Cargo.toml new file mode 100644 index 000000000..1371b96e6 --- /dev/null +++ b/examples/rust-cargo/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "rust-cargo" +version = "0.1.0" +authors = ["Shaobo He "] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +smack = { path = "/usr/local/share/smack/lib" } + +[profile.dev] +incremental=false + diff --git a/examples/rust-cargo/src/main.rs b/examples/rust-cargo/src/main.rs new file mode 100644 index 000000000..b21f50b6d --- /dev/null +++ b/examples/rust-cargo/src/main.rs @@ -0,0 +1,11 @@ +#[macro_use] +extern crate smack; +use smack::*; + +// @expect error + +fn main() { + let a: u32 = 2.verifier_nondet(); + let b: u32 = 3.verifier_nondet(); + smack::assert!(a + b != 5); +} diff --git a/include/smack/Naming.h b/include/smack/Naming.h index 6e19318d3..e0abc112a 100644 --- a/include/smack/Naming.h +++ b/include/smack/Naming.h @@ -93,6 +93,7 @@ class Naming { static const std::string MEMORY_LEAK_FUNCTION; static const std::string RUST_ENTRY; + static const std::string RUST_LANG_START_INTERNAL; static const std::vector RUST_PANICS; static const std::string RUST_PANIC_ANNOTATION; diff --git a/include/smack/RewriteBitwiseOps.h b/include/smack/RewriteBitwiseOps.h new file mode 100644 index 000000000..da009d209 --- /dev/null +++ b/include/smack/RewriteBitwiseOps.h @@ -0,0 +1,21 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef REWRITEBITWISEOPS_H +#define REWRITEBITWISEOPS_H + +#include "llvm/IR/Module.h" +#include "llvm/Pass.h" + +namespace smack { + +class RewriteBitwiseOps : public llvm::ModulePass { +public: + static char ID; // Pass identification, replacement for typeid + RewriteBitwiseOps() : llvm::ModulePass(ID) {} + virtual llvm::StringRef getPassName() const; + virtual bool runOnModule(llvm::Module &m); +}; +} // namespace smack + +#endif // REWRITEBITWISEOPS_H diff --git a/include/smack/RustFixes.h b/include/smack/RustFixes.h new file mode 100644 index 000000000..887997839 --- /dev/null +++ b/include/smack/RustFixes.h @@ -0,0 +1,23 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +#ifndef RUSTFIXES_H +#define RUSTFIXES_H + +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#include "llvm/Pass.h" + +namespace smack { + +class RustFixes : public llvm::ModulePass { +public: + static char ID; // Pass identification, replacement for typeid + RustFixes() : llvm::ModulePass(ID) {} + virtual llvm::StringRef getPassName() const; + virtual bool runOnModule(llvm::Module &m); +}; +} // namespace smack + +#endif // RUSTFIXES_H diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index 15aa72a7e..6e6e69149 100644 --- a/include/smack/SmackOptions.h +++ b/include/smack/SmackOptions.h @@ -25,6 +25,7 @@ class SmackOptions { static const llvm::cl::opt SourceLocSymbols; static llvm::cl::opt BitPrecise; static const llvm::cl::opt BitPrecisePointers; + static const llvm::cl::opt RewriteBitwiseOps; static const llvm::cl::opt NoMemoryRegionSplitting; static const llvm::cl::opt NoByteAccessInference; static const llvm::cl::opt FloatEnabled; diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 53043330f..499930e6a 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -84,7 +84,8 @@ class SmackRep { const Expr *cast(unsigned opcode, const llvm::Value *v, const llvm::Type *t); bool isFpArithOp(unsigned opcode); const Expr *bop(unsigned opcode, const llvm::Value *lhs, - const llvm::Value *rhs, const llvm::Type *t); + const llvm::Value *rhs, const llvm::Type *t, + bool isUnsigned = false); const Expr *uop(const llvm::Value *op); const Expr *cmp(unsigned predicate, const llvm::Value *lhs, const llvm::Value *rhs, bool isUnsigned); @@ -128,7 +129,8 @@ class SmackRep { std::string type(const llvm::Type *t); std::string type(const llvm::Value *v); - const Expr *lit(const llvm::Value *v, bool isUnsigned = false); + const Expr *lit(const llvm::Value *v, bool isUnsigned = false, + bool isUnsignedInst = false); const Expr *lit(const llvm::Value *v, unsigned flag); const Expr *ptrArith(const llvm::GetElementPtrInst *I); @@ -137,7 +139,8 @@ class SmackRep { ptrArith(const llvm::Value *p, std::vector> args); - const Expr *expr(const llvm::Value *v, bool isConstIntUnsigned = false); + const Expr *expr(const llvm::Value *v, bool isConstIntUnsigned = false, + bool isUnsignedInst = false); const Expr *cast(const llvm::Instruction *I); const Expr *cast(const llvm::ConstantExpr *CE); diff --git a/include/smack/SmackWarnings.h b/include/smack/SmackWarnings.h index 3713f925d..800d4f84d 100644 --- a/include/smack/SmackWarnings.h +++ b/include/smack/SmackWarnings.h @@ -26,22 +26,30 @@ class SmackWarnings { Info = 20 // Memory length, etc. }; + enum class FlagRelation : unsigned { And = 0, Or = 1 }; + static UnsetFlagsT getUnsetFlags(RequiredFlagsT flags); + static bool isSatisfied(RequiredFlagsT flags, FlagRelation rel); // generate warnings about unsoundness static void warnUnsound(std::string unmodeledOpName, Block *currBlock, - const llvm::Instruction *i, bool ignore = false); + const llvm::Instruction *i, bool ignore = false, + FlagRelation rel = FlagRelation::And); static void warnUnsound(std::string name, UnsetFlagsT unsetFlags, Block *currBlock, const llvm::Instruction *i, - bool ignore = false); + bool ignore = false, + FlagRelation rel = FlagRelation::And); static void warnIfUnsound(std::string name, RequiredFlagsT requiredFlags, Block *currBlock, const llvm::Instruction *i, - bool ignore = false); + bool ignore = false, + FlagRelation rel = FlagRelation::And); static void warnIfUnsound(std::string name, FlagT &requiredFlag, - Block *currBlock, const llvm::Instruction *i); + Block *currBlock, const llvm::Instruction *i, + FlagRelation rel = FlagRelation::And); static void warnIfUnsound(std::string name, FlagT &requiredFlag1, FlagT &requiredFlag2, Block *currBlock, - const llvm::Instruction *i); + const llvm::Instruction *i, + FlagRelation rel = FlagRelation::And); // generate warnings about memcpy/memset length/DSA static void warnInfo(std::string info); diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp index 848e95b60..5b92cb3aa 100644 --- a/lib/smack/IntegerOverflowChecker.cpp +++ b/lib/smack/IntegerOverflowChecker.cpp @@ -52,15 +52,12 @@ std::string IntegerOverflowChecker::getMin(unsigned bits, bool isSigned) { */ Value *IntegerOverflowChecker::extendBitWidth(Value *v, int bits, bool isSigned, Instruction *i) { - if (SmackOptions::IntegerOverflow) { - if (isSigned) - return CastInst::CreateSExtOrBitCast( - v, IntegerType::get(i->getFunction()->getContext(), bits * 2), "", i); - else - return CastInst::CreateZExtOrBitCast( - v, IntegerType::get(i->getFunction()->getContext(), bits * 2), "", i); - } else - return v; + if (isSigned) + return CastInst::CreateSExtOrBitCast( + v, IntegerType::get(i->getFunction()->getContext(), bits * 2), "", i); + else + return CastInst::CreateZExtOrBitCast( + v, IntegerType::get(i->getFunction()->getContext(), bits * 2), "", i); } /* @@ -70,24 +67,19 @@ Value *IntegerOverflowChecker::extendBitWidth(Value *v, int bits, bool isSigned, BinaryOperator *IntegerOverflowChecker::createFlag(Value *v, int bits, bool isSigned, Instruction *i) { - if (SmackOptions::IntegerOverflow) { - ConstantInt *max = ConstantInt::get( - IntegerType::get(i->getFunction()->getContext(), bits * 2), - getMax(bits, isSigned), 10); - ConstantInt *min = ConstantInt::get( - IntegerType::get(i->getFunction()->getContext(), bits * 2), - getMin(bits, isSigned), 10); - CmpInst::Predicate maxCmpPred = - (isSigned ? CmpInst::ICMP_SGT : CmpInst::ICMP_UGT); - CmpInst::Predicate minCmpPred = - (isSigned ? CmpInst::ICMP_SLT : CmpInst::ICMP_ULT); - ICmpInst *gt = new ICmpInst(i, maxCmpPred, v, max, ""); - ICmpInst *lt = new ICmpInst(i, minCmpPred, v, min, ""); - return BinaryOperator::Create(Instruction::Or, gt, lt, "", i); - } else { - ConstantInt *a = ConstantInt::getFalse(i->getFunction()->getContext()); - return BinaryOperator::Create(Instruction::And, a, a, "", i); - } + ConstantInt *max = ConstantInt::get( + IntegerType::get(i->getFunction()->getContext(), bits * 2), + getMax(bits, isSigned), 10); + ConstantInt *min = ConstantInt::get( + IntegerType::get(i->getFunction()->getContext(), bits * 2), + getMin(bits, isSigned), 10); + CmpInst::Predicate maxCmpPred = + (isSigned ? CmpInst::ICMP_SGT : CmpInst::ICMP_UGT); + CmpInst::Predicate minCmpPred = + (isSigned ? CmpInst::ICMP_SLT : CmpInst::ICMP_ULT); + ICmpInst *gt = new ICmpInst(i, maxCmpPred, v, max, ""); + ICmpInst *lt = new ICmpInst(i, minCmpPred, v, min, ""); + return BinaryOperator::Create(Instruction::Or, gt, lt, "", i); } /* @@ -95,11 +87,8 @@ BinaryOperator *IntegerOverflowChecker::createFlag(Value *v, int bits, */ Value *IntegerOverflowChecker::createResult(Value *v, int bits, Instruction *i) { - if (SmackOptions::IntegerOverflow) - return CastInst::CreateTruncOrBitCast( - v, IntegerType::get(i->getFunction()->getContext(), bits), "", i); - else - return v; + return CastInst::CreateTruncOrBitCast( + v, IntegerType::get(i->getFunction()->getContext(), bits), "", i); } /* @@ -135,33 +124,27 @@ bool IntegerOverflowChecker::runOnModule(Module &m) { if (Naming::isSmackName(F.getName())) continue; for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) { - // Add check for UBSan left shift/signed division when needed - if (SmackOptions::IntegerOverflow) { - if (auto chkshft = dyn_cast(&*I)) { - Function *chkfn = chkshft->getCalledFunction(); - if (chkfn && chkfn->hasName() && - (chkfn->getName().find("__ubsan_handle_shift_out_of_bounds") != - std::string::npos || - chkfn->getName().find("__ubsan_handle_divrem_overflow") != - std::string::npos)) { + if (auto ci = dyn_cast(&*I)) { + Function *f = ci->getCalledFunction(); + if (f && f->hasName()) { + std::string fn = f->getName(); + if (fn.find("__ubsan_handle_shift_out_of_bounds") != + std::string::npos || + fn.find("__ubsan_handle_divrem_overflow") != std::string::npos) { // If the call to __ubsan_handle_* is reachable, // then an overflow is possible. - ConstantInt *flag = - ConstantInt::getTrue(chkshft->getFunction()->getContext()); - addCheck(co, flag, &*I); - addBlockingAssume(va, flag, &*I); - I->replaceAllUsesWith(flag); - instToErase.push_back(&*I); + if (SmackOptions::IntegerOverflow) { + // Add check for UBSan left shift/signed division when needed + ConstantInt *flag = + ConstantInt::getTrue(ci->getFunction()->getContext()); + addCheck(co, flag, ci); + addBlockingAssume(va, flag, ci); + ci->replaceAllUsesWith(flag); + instToErase.push_back(ci); + } } - } - } - if (auto ei = dyn_cast(&*I)) { - if (auto ci = dyn_cast(ei->getAggregateOperand())) { - Function *f = ci->getCalledFunction(); SmallVector info; - if (f && f->hasName() && - OVERFLOW_INTRINSICS.match(f->getName(), &info) && - ei->getIndices()[0] == 1) { + if (OVERFLOW_INTRINSICS.match(f->getName(), &info)) { /* * If ei is an ExtractValueInst whose value flows from an LLVM * checked value intrinsic f, then we do the following: @@ -181,29 +164,35 @@ bool IntegerOverflowChecker::runOnModule(Module &m) { bool isSigned = (info[1] == "s"); std::string op = info[2]; int bits = std::stoi(info[3]); - Instruction *prev = &*std::prev(I); Value *eo1 = - extendBitWidth(ci->getArgOperand(0), bits, isSigned, &*I); + extendBitWidth(ci->getArgOperand(0), bits, isSigned, ci); Value *eo2 = - extendBitWidth(ci->getArgOperand(1), bits, isSigned, &*I); + extendBitWidth(ci->getArgOperand(1), bits, isSigned, ci); SDEBUG(errs() << "Processing operator: " << op << "\n"); assert(INSTRUCTION_TABLE.count(op) != 0 && "Operator must be present in our instruction table."); BinaryOperator *ai = BinaryOperator::Create( - INSTRUCTION_TABLE.at(op), eo1, eo2, "", &*I); - if (auto pei = dyn_cast_or_null(prev)) { - if (ci == dyn_cast(pei->getAggregateOperand())) { - Value *r = createResult(ai, bits, &*I); - prev->replaceAllUsesWith(r); - instToErase.push_back(prev); + INSTRUCTION_TABLE.at(op), eo1, eo2, "", ci); + Value *r = createResult(ai, bits, &*I); + BinaryOperator *flag = createFlag(ai, bits, isSigned, ci); + if (SmackOptions::IntegerOverflow) + addCheck(co, flag, ci); + for (auto U : ci->users()) { + if (ExtractValueInst *ei = dyn_cast(U)) { + if (ei->getNumIndices() == 1) { + if (ei->getIndices()[0] == 0) + // value part + ei->replaceAllUsesWith(r); + else if (ei->getIndices()[0] == 1) { + // flag part + // addBlockingAssume(va, flag, ei); + ei->replaceAllUsesWith(flag); + } else + llvm_unreachable("Unexpected extractvalue inst!"); + instToErase.push_back(ei); + } } } - BinaryOperator *flag = createFlag(ai, bits, isSigned, &*I); - if (SmackOptions::IntegerOverflow) - addCheck(co, flag, &*I); - addBlockingAssume(va, flag, &*I); - I->replaceAllUsesWith(flag); - instToErase.push_back(&*I); instToErase.push_back(ci); } } diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp index f4dd71358..ad6ba73e0 100644 --- a/lib/smack/Naming.cpp +++ b/lib/smack/Naming.cpp @@ -62,6 +62,8 @@ const std::string Naming::REC_MEM_OP = "boogie_si_record_mop"; const std::string Naming::MEM_OP_VAL = "$MOP"; const std::string Naming::RUST_ENTRY = "_ZN3std2rt10lang_start"; +const std::string Naming::RUST_LANG_START_INTERNAL = + "_ZN3std2rt19lang_start_internal"; const std::vector Naming::RUST_PANICS = { "_ZN3std9panicking15begin_panic_fmt17h", "_ZN4core9panicking5panic17h", "_ZN3std9panicking11begin_panic17h", "_ZN4core9panicking9panic_fmt17h", diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index b72839886..ba20202ba 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -173,7 +173,7 @@ std::string getIntLimit(unsigned size) { } const std::vector IntOpGen::INTEGER_SIZES{ - 1, 5, 6, 8, 16, 24, 32, 40, 48, 56, 64, 80, 88, 96, 128, 160, 256}; + 1, 5, 6, 8, 16, 24, 32, 33, 40, 48, 56, 64, 80, 88, 96, 128, 160, 256}; // floating-point layout map: bit-width -> (exponent bit-width, significand // bit-width) diff --git a/lib/smack/RewriteBitwiseOps.cpp b/lib/smack/RewriteBitwiseOps.cpp new file mode 100644 index 000000000..63f558baa --- /dev/null +++ b/lib/smack/RewriteBitwiseOps.cpp @@ -0,0 +1,170 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// + +// This pass converts bitwise operations with certain constant operands +// into equivalent integer operations. + +#include "smack/RewriteBitwiseOps.h" +#include "smack/Debug.h" +#include "smack/Naming.h" +#include "smack/SmackOptions.h" +#include "llvm/ADT/APInt.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/IRBuilder.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/IR/ValueSymbolTable.h" +#include "llvm/Support/Regex.h" +#include "llvm/Support/raw_ostream.h" +#include "llvm/Transforms/Utils/BasicBlockUtils.h" +#include + +namespace smack { + +using namespace llvm; + +unsigned getOpBitWidth(const Value *V) { + const Type *T = V->getType(); + const IntegerType *iType = cast(T); + return iType->getBitWidth(); +} + +Optional getConstantIntValue(const Value *V) { + if (const ConstantInt *ci = dyn_cast(V)) { + const APInt &value = ci->getValue(); + return Optional(value); + } else { + return Optional(); + } +} + +bool isConstantInt(const Value *V) { + Optional constantValue = getConstantIntValue(V); + return constantValue.hasValue() && (*constantValue + 1).isPowerOf2(); +} + +bool RewriteBitwiseOps::runOnModule(Module &m) { + std::vector instsFrom; + std::vector instsTo; + + for (auto &F : m) { + if (Naming::isSmackName(F.getName())) + continue; + for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) { + if (I->isShift()) { + BinaryOperator *bi = cast(&*I); + Value *amount = bi->getOperand(1); + + if (ConstantInt *ci = dyn_cast(amount)) { + unsigned opcode = bi->getOpcode(); + Instruction::BinaryOps op; + if (opcode == Instruction::AShr || opcode == Instruction::LShr) { + // Shifting right by a constant amount is equivalent to dividing by + // 2^amount + op = Instruction::SDiv; + } else if (opcode == Instruction::Shl) { + // Shifting left by a constant amount is equivalent to dividing by + // 2^amount + op = Instruction::Mul; + } + + auto lhs = bi->getOperand(0); + unsigned bitWidth = getOpBitWidth(lhs); + APInt rhsVal = APInt(bitWidth, "1", 10); + const APInt &value = ci->getValue(); + rhsVal <<= value; + Value *rhs = ConstantInt::get(ci->getType(), rhsVal); + Instruction *replacement = BinaryOperator::Create(op, lhs, rhs, ""); + instsFrom.push_back(&*I); + instsTo.push_back(replacement); + } + } else if (I->isBitwiseLogicOp()) { + // If the operation is a bit-wise `and' and the mask variable is + // constant, it may be possible to replace this operation with a + // remainder operation. If one argument has only ones, and they're only + // in the least significant bit, then the mask is 2^(number of ones) + // - 1. This is equivalent to the remainder when dividing by 2^(number + // of ones). + BinaryOperator *bi = cast(&*I); + unsigned opcode = bi->getOpcode(); + if (opcode == Instruction::And) { + Value *args[] = {bi->getOperand(0), bi->getOperand(1)}; + int maskOperand = -1; + + if (isConstantInt(args[0])) { + maskOperand = 0; + } + // Zvonimir: Right-side constants do not work well on SVCOMP + // } else if (isConstantInt(args[1])) { + // maskOperand = 1; + // } + + if (maskOperand == -1) { + unsigned bitWidth = getOpBitWidth(&*I); + Function *co; + if (bitWidth == 64) { + co = m.getFunction("__SMACK_and64"); + } else if (bitWidth == 16) { + co = m.getFunction("__SMACK_and16"); + } else if (bitWidth == 8) { + co = m.getFunction("__SMACK_and8"); + } else if (bitWidth == 1) { + continue; + } else { + co = m.getFunction("__SMACK_and32"); + } + assert(co != NULL && "Function __SMACK_and should be present."); + std::vector args; + args.push_back(bi->getOperand(0)); + args.push_back(bi->getOperand(1)); + instsFrom.push_back(&*I); + instsTo.push_back(CallInst::Create(co, args, "")); + } else { + auto lhs = args[1 - maskOperand]; + Value *rhs = ConstantInt::get( + m.getContext(), *getConstantIntValue(args[maskOperand]) + 1); + Instruction *replacement = + BinaryOperator::Create(Instruction::URem, lhs, rhs, ""); + instsFrom.push_back(&*I); + instsTo.push_back(replacement); + } + } else if (opcode == Instruction::Or) { + unsigned bitWidth = getOpBitWidth(&*I); + Function *co; + if (bitWidth == 64) { + co = m.getFunction("__SMACK_or64"); + } else if (bitWidth == 16) { + co = m.getFunction("__SMACK_or16"); + } else if (bitWidth == 8) { + co = m.getFunction("__SMACK_or8"); + } else if (bitWidth == 1) { + continue; + } else { + co = m.getFunction("__SMACK_or32"); + } + assert(co != NULL && "Function __SMACK_or should be present."); + std::vector args; + args.push_back(bi->getOperand(0)); + args.push_back(bi->getOperand(1)); + instsFrom.push_back(&*I); + instsTo.push_back(CallInst::Create(co, args, "")); + } + } + } + } + + for (size_t i = 0; i < instsFrom.size(); ++i) { + ReplaceInstWithInst(instsFrom[i], instsTo[i]); + } + + return true; +} + +// Pass ID variable +char RewriteBitwiseOps::ID = 0; + +StringRef RewriteBitwiseOps::getPassName() const { + return "Translate bitwise operations with constant arguments to integer " + "operations"; +} +} // namespace smack diff --git a/lib/smack/RustFixes.cpp b/lib/smack/RustFixes.cpp new file mode 100644 index 000000000..32c5809de --- /dev/null +++ b/lib/smack/RustFixes.cpp @@ -0,0 +1,99 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +// This patches Rust programs by removing certain language specific functions, +// enabling later optimizations. +// + +#include "smack/RustFixes.h" +#include "smack/Naming.h" +#include "llvm/Analysis/CallGraph.h" +#include "llvm/IR/IRBuilder.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/IR/Module.h" +#include "llvm/Support/raw_ostream.h" +#include +#include + +namespace smack { + +using namespace llvm; + +/* +The main function of rust programs looks like this: +... +%r = call i32 @std::rt::lang_start(..., @real_main, ...) +... + +This patches the main function to: +... +%r = 0 +call void @real_main(...) +... +*/ +void fixEntry(Function &main) { + std::vector instToErase; + + for (inst_iterator I = inst_begin(main), E = inst_end(main); I != E; ++I) { + if (auto ci = dyn_cast(&*I)) { + if (Function *f = ci->getCalledFunction()) { + std::string name = f->hasName() ? f->getName() : ""; + if (name.find(Naming::RUST_ENTRY) != std::string::npos) { + // Get real Rust main + auto castExpr = ci->getArgOperand(0); + auto mainFunction = cast(castExpr); + auto callMain = CallInst::Create(mainFunction->getFunctionType(), + cast(mainFunction)); + + // Replace the call to lang_start with the real Rust main function + auto retType = f->getReturnType(); + // Create a fake return value for this instruction + Constant *zero = ConstantInt::get(retType, 0); + auto *result = BinaryOperator::Create(Instruction::Add, zero, zero); + result->insertAfter(ci); + // Call the real main function + callMain->insertAfter(result); + I->replaceAllUsesWith(result); + + instToErase.push_back(&*I); + } + } + } + } + + for (auto I : instToErase) { + I->eraseFromParent(); + } +} + +bool RustFixes::runOnModule(Module &m) { + std::set funcToErase; + + for (auto &F : m) { + if (F.hasName()) { + auto name = F.getName(); + if (Naming::isSmackName(name)) + continue; + if (name == "main") { + fixEntry(F); + } else if (name.find(Naming::RUST_LANG_START_INTERNAL) != + std::string::npos || + name.find(Naming::RUST_ENTRY) != std::string::npos) { + funcToErase.insert(&F); + } + } + } + + for (auto F : funcToErase) { + F->dropAllReferences(); + } + + return true; +} + +// Pass ID variable +char RustFixes::ID = 0; + +StringRef RustFixes::getPassName() const { return "Fixes for Rust programs"; } + +} // namespace smack diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index e3d147a55..e3584b15c 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -351,7 +351,7 @@ void SmackInstGenerator::visitUnreachableInst(llvm::UnreachableInst &ii) { void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) { processInstruction(I); - if (rep->isBitwiseOp(&I)) + if (rep->isBitwiseOp(&I) && I.getType()->getIntegerBitWidth() > 1) SmackWarnings::warnIfUnsound(std::string("bitwise operation ") + I.getOpcodeName(), SmackOptions::BitPrecise, currBlock, &I); @@ -646,6 +646,13 @@ void SmackInstGenerator::visitSelectInst(llvm::SelectInst &i) { void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) { processInstruction(ci); + if (ci.isInlineAsm()) { + SmackWarnings::warnUnsound("inline asm call " + i2s(ci), currBlock, &ci, + ci.getType()->isVoidTy()); + emit(Stmt::skip()); + return; + } + Function *f = ci.getCalledFunction(); if (!f) { assert(ci.getCalledValue() && "Called value is null"); @@ -654,18 +661,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) { std::string name = f->hasName() ? f->getName() : ""; - if (ci.isInlineAsm()) { - SmackWarnings::warnUnsound("inline asm call " + i2s(ci), currBlock, &ci, - ci.getType()->isVoidTy()); - emit(Stmt::skip()); - - } else if (name.find(Naming::RUST_ENTRY) != std::string::npos) { - // Set the entry point for Rust programs - auto castExpr = ci.getArgOperand(0); - auto mainFunction = cast(castExpr); - emit(Stmt::call(mainFunction->getName(), {}, {})); - - } else if (SmackOptions::RustPanics && isRustPanic(name)) { + if (SmackOptions::RustPanics && isRustPanic(name)) { // Convert Rust's panic functions into assertion violations emit(Stmt::assert_(Expr::lit(false), {Attr::attr(Naming::RUST_PANIC_ANNOTATION)})); @@ -902,15 +898,18 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) { //(CallInst -> Void) -> [Flags] -> (CallInst -> Void) static const auto conditionalModel = [this](std::function modelGenFunc, - std::initializer_list *> requiredFlags) { + std::initializer_list *> requiredFlags, + SmackWarnings::FlagRelation rel = + SmackWarnings::FlagRelation::And) { auto unsetFlags = SmackWarnings::getUnsetFlags(requiredFlags); - return [this, unsetFlags, modelGenFunc](CallInst *ci) { - if (unsetFlags.empty()) + auto satisfied = SmackWarnings::isSatisfied(requiredFlags, rel); + return [this, unsetFlags, modelGenFunc, satisfied, rel](CallInst *ci) { + if (satisfied) modelGenFunc(ci); else { SmackWarnings::warnUnsound( "call to " + ci->getCalledFunction()->getName().str(), - unsetFlags, currBlock, ci); + unsetFlags, currBlock, ci, false, rel); emit(rep->call(ci->getCalledFunction(), *ci)); } }; @@ -1084,20 +1083,37 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) { {&SmackOptions::BitPrecise}); // Count the population of 1s in a bv - static const auto ctpop = [this](Value *arg) { - auto width = arg->getType()->getIntegerBitWidth(); - auto var = rep->expr(arg); - auto body = Expr::lit(0, width); - auto type = rep->type(arg->getType()); - - for (unsigned i = 0; i < width; ++i) { - body = Expr::fn(indexedName("$add", {type}), - Expr::fn(indexedName("$zext", {"bv1", type}), - Expr::bvExtract(var, i + 1, i)), - body); - } - return body; - }; + static const auto ctpop = conditionalModel( + [this](CallInst *ci) { + Value *arg = ci->getArgOperand(0); + auto width = arg->getType()->getIntegerBitWidth(); + auto var = rep->expr(arg); + const Expr *body = nullptr; + auto type = rep->type(arg->getType()); + + if (SmackOptions::BitPrecise) { // Bitvector mode + body = Expr::lit(0, width); + for (unsigned i = 0; i < width; ++i) { + body = Expr::fn(indexedName("$add", {type}), + Expr::fn(indexedName("$zext", {"bv1", type}), + Expr::bvExtract(var, i + 1, i)), + body); + } + } else { // Otherwise, try with the integer encoding + body = Expr::lit(0ull); + for (unsigned i = 0; i < width; ++i) { + auto quotient = + Expr::fn(indexedName("$udiv", {type}), var, + Expr::lit((unsigned long long)(1ull << i))); + auto remainder = Expr::fn(indexedName("$urem", {type}), quotient, + Expr::lit(2ull)); + body = Expr::fn(indexedName("$add", {type}), remainder, body); + } + } + emit(Stmt::assign(rep->expr(ci), body)); + }, + {&SmackOptions::BitPrecise, &SmackOptions::RewriteBitwiseOps}, + SmackWarnings::FlagRelation::Or); static const auto assignBvExpr = [this](std::function exprGenFunc) { @@ -1172,7 +1188,7 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) { {llvm::Intrinsic::convert_from_fp16, f16UpCast}, {llvm::Intrinsic::convert_to_fp16, f16DownCast}, {llvm::Intrinsic::ctlz, ctlz}, - {llvm::Intrinsic::ctpop, assignBvExpr(ctpop)}, + {llvm::Intrinsic::ctpop, ctpop}, {llvm::Intrinsic::cttz, cttz}, {llvm::Intrinsic::dbg_declare, ignore}, {llvm::Intrinsic::dbg_label, ignore}, diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 295e397af..22f5f7a00 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -48,6 +48,11 @@ const llvm::cl::opt SmackOptions::AddTiming("timing-annotations", llvm::cl::desc("Add timing annotations.")); +const llvm::cl::opt SmackOptions::RewriteBitwiseOps( + "rewrite-bitwise-ops", + llvm::cl::desc( + "Provides models for bitwise operations in integer encoding.")); + 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 e78b5513b..998966787 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -624,13 +624,22 @@ const Expr *SmackRep::integerLit(long long v, unsigned width) { } } -const Expr *SmackRep::lit(const llvm::Value *v, bool isUnsigned) { +const Expr *SmackRep::lit(const llvm::Value *v, bool isUnsigned, + bool isUnsignedInst) { using namespace llvm; if (const ConstantInt *ci = llvm::dyn_cast(v)) { const APInt &API = ci->getValue(); unsigned width = ci->getBitWidth(); - bool neg = isUnsigned ? false : width > 1 && ci->isNegative(); + + // This is heuristics for choosing between generating an unsigned vs + // signed constant (since LLVM does not keep track of that). + // Signed values -1 is special since it appears often because i-- + // gets translated into i + (-1), and so in that context it should + // be a signed integer. + bool neg = width > 1 && + (isUnsigned ? (isUnsignedInst ? false : API.getSExtValue() == -1) + : ci->isNegative()); std::string str = (neg ? API.abs() : API).toString(10, false); const Expr *e = SmackOptions::BitPrecise ? Expr::lit(str, width) : Expr::lit(str, 0); @@ -784,7 +793,8 @@ const Expr *SmackRep::ptrArith( return e; } -const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned) { +const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned, + bool isUnsignedInst) { using namespace llvm; if (isa(v)) { @@ -827,7 +837,7 @@ const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned) { } } else if (const ConstantInt *ci = dyn_cast(constant)) { - return lit(ci, isConstIntUnsigned); + return lit(ci, isConstIntUnsigned, isUnsignedInst); } else if (const ConstantFP *cf = dyn_cast(constant)) { return lit(cf); @@ -907,11 +917,12 @@ const Expr *SmackRep::bop(const llvm::ConstantExpr *CE) { const Expr *SmackRep::bop(const llvm::BinaryOperator *BO) { return bop(BO->getOpcode(), BO->getOperand(0), BO->getOperand(1), - BO->getType()); + BO->getType(), !BO->hasNoSignedWrap()); } const Expr *SmackRep::bop(unsigned opcode, const llvm::Value *lhs, - const llvm::Value *rhs, const llvm::Type *t) { + const llvm::Value *rhs, const llvm::Type *t, + bool isUnsigned) { std::string fn = Naming::INSTRUCTION_TABLE.at(opcode); if (isFpArithOp(opcode)) { if (SmackOptions::FloatEnabled) { @@ -921,7 +932,19 @@ const Expr *SmackRep::bop(unsigned opcode, const llvm::Value *lhs, return Expr::fn(opName(fn, {t}), expr(lhs), expr(rhs)); } } - return Expr::fn(opName(fn, {t}), expr(lhs), expr(rhs)); + + bool isUnsignedInst = false; + if (opcode == llvm::Instruction::SDiv || opcode == llvm::Instruction::SRem) { + isUnsigned = false; + } else if (opcode == llvm::Instruction::UDiv || + opcode == llvm::Instruction::URem || + opcode == llvm::Instruction::Sub) { + isUnsignedInst = true; + isUnsigned = true; + } + + return Expr::fn(opName(fn, {t}), expr(lhs, isUnsigned, isUnsignedInst), + expr(rhs, isUnsigned, isUnsignedInst)); } const Expr *SmackRep::uop(const llvm::ConstantExpr *CE) { @@ -951,8 +974,8 @@ const Expr *SmackRep::cmp(unsigned predicate, const llvm::Value *lhs, const llvm::Value *rhs, bool isUnsigned) { std::string fn = opName(Naming::CMPINST_TABLE.at(predicate), {lhs->getType()}); - const Expr *e1 = expr(lhs, isUnsigned); - const Expr *e2 = expr(rhs, isUnsigned); + const Expr *e1 = expr(lhs, isUnsigned, true); + const Expr *e2 = expr(rhs, isUnsigned, true); if (lhs->getType()->isFloatingPointTy()) return Expr::ifThenElse(Expr::fn(fn + ".bool", e1, e2), integerLit(1ULL, 1), integerLit(0ULL, 1)); @@ -971,7 +994,9 @@ const Expr *SmackRep::select(const llvm::ConstantExpr *CE) { const Expr *SmackRep::select(const llvm::Value *condVal, const llvm::Value *trueVal, const llvm::Value *falseVal) { - const Expr *c = expr(condVal), *v1 = expr(trueVal), *v2 = expr(falseVal); + const Expr *c = expr(condVal); + const Expr *v1 = expr(trueVal, true, true); + const Expr *v2 = expr(falseVal, true, true); assert(!condVal->getType()->isVectorTy() && "Vector condition is not supported."); diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp index b7bc2b1cd..a6c22243e 100644 --- a/lib/smack/SmackWarnings.cpp +++ b/lib/smack/SmackWarnings.cpp @@ -36,35 +36,42 @@ SmackWarnings::getUnsetFlags(RequiredFlagsT requiredFlags) { return ret; } +bool SmackWarnings::isSatisfied(RequiredFlagsT requiredFlags, + FlagRelation rel) { + auto unsetFlags = getUnsetFlags(requiredFlags); + return rel == FlagRelation::And ? unsetFlags.empty() + : unsetFlags.size() < requiredFlags.size(); +} + std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) { - std::string ret = ""; + std::string ret = "{ "; for (auto f : flags) { if (f->ArgStr.str() == "bit-precise") ret += ("--integer-encoding=bit-vector "); else ret += ("--" + f->ArgStr.str() + " "); } - return ret; + return ret + "}"; } void SmackWarnings::warnIfUnsound(std::string name, RequiredFlagsT requiredFlags, Block *currBlock, const Instruction *i, - bool ignore) { - auto unsetFlags = getUnsetFlags(requiredFlags); - if (unsetFlags.size()) - warnUnsound(name, unsetFlags, currBlock, i, ignore); + bool ignore, FlagRelation rel) { + if (!isSatisfied(requiredFlags, rel)) + warnUnsound(name, getUnsetFlags(requiredFlags), currBlock, i, ignore); } void SmackWarnings::warnUnsound(std::string unmodeledOpName, Block *currBlock, - const Instruction *i, bool ignore) { + const Instruction *i, bool ignore, + FlagRelation rel) { warnUnsound("unmodeled operation " + unmodeledOpName, UnsetFlagsT(), - currBlock, i, ignore); + currBlock, i, ignore, rel); } void SmackWarnings::warnUnsound(std::string name, UnsetFlagsT unsetFlags, Block *currBlock, const Instruction *i, - bool ignore) { + bool ignore, FlagRelation rel) { if (!isSufficientWarningLevel(WarningLevel::Unsound)) return; std::string beginning = std::string("llvm2bpl: ") + buildDebugInfo(i); @@ -73,8 +80,9 @@ void SmackWarnings::warnUnsound(std::string name, UnsetFlagsT unsetFlags, if (currBlock) currBlock->addStmt(Stmt::comment(beginning + "warning: " + end)); std::string hint = ""; - if (unsetFlags.size()) - hint = (" try adding flag(s): " + getFlagStr(unsetFlags)); + if (!unsetFlags.empty()) + hint = (" try adding " + ((rel == FlagRelation::And ? "all the " : "any ") + + ("flag(s) in: " + getFlagStr(unsetFlags)))); errs() << beginning; (SmackOptions::ColoredWarnings ? errs().changeColor(raw_ostream::MAGENTA) : errs()) @@ -84,14 +92,16 @@ void SmackWarnings::warnUnsound(std::string name, UnsetFlagsT unsetFlags, } void SmackWarnings::warnIfUnsound(std::string name, FlagT &requiredFlag, - Block *currBlock, const Instruction *i) { - warnIfUnsound(name, {&requiredFlag}, currBlock, i); + Block *currBlock, const Instruction *i, + FlagRelation rel) { + warnIfUnsound(name, {&requiredFlag}, currBlock, i, false, rel); } void SmackWarnings::warnIfUnsound(std::string name, FlagT &requiredFlag1, FlagT &requiredFlag2, Block *currBlock, - const Instruction *i) { - warnIfUnsound(name, {&requiredFlag1, &requiredFlag2}, currBlock, i); + const Instruction *i, FlagRelation rel) { + warnIfUnsound(name, {&requiredFlag1, &requiredFlag2}, currBlock, i, false, + rel); } void SmackWarnings::warnInfo(std::string info) { diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp index ecb281a10..5be7fe530 100644 --- a/lib/utils/Devirt.cpp +++ b/lib/utils/Devirt.cpp @@ -456,7 +456,7 @@ Devirtualize::processCallSite (CallSite &CS) { // First, determine if this is a direct call. If so, then just ignore it. // Value * CalledValue = CS.getCalledValue(); - if (isa(CalledValue->stripPointerCastsAndAliases())) + if (!CS.isIndirectCall()) return; // diff --git a/share/smack/errtrace.py b/share/smack/errtrace.py new file mode 100644 index 000000000..72771ecda --- /dev/null +++ b/share/smack/errtrace.py @@ -0,0 +1,228 @@ +import re +import functools +import shutil +import subprocess +import json + + +def reformat_assignment(line): + '''Transform assignment RHS values''' + + def repl(m): + val = m.group(1) + if 'bv' in val: + return m.group(2) + 'UL' + else: + sig_size = int(m.group(7)) + exp_size = int(m.group(8)) + # assume we can only handle double + if sig_size > 53 or exp_size > 11: + return m.group() + + sign_val = -1 if m.group(3) != '' else 1 + sig_val = m.group(4) + exp_sign_val = -1 if m.group(5) != '' else 1 + # note that the exponent base is 16 + exp_val = 2**(4 * exp_sign_val * int(m.group(6))) + return str(sign_val * float.fromhex(sig_val) * exp_val) + + # Boogie FP const grammar: (-)0x[sig]e[exp]f[sigSize]e[expSize], where + # sig = hexdigit {hexdigit} '.' hexdigit {hexdigit} + # exp = digit {digit} + # sigSize = digit {digit} + # expSize = digit {digit} + return re.sub( + (r'((\d+)bv\d+|(-?)0x([0-9a-fA-F]+\.[0-9a-fA-F]+)e(-?)' + r'(\d+)f(\d+)e(\d+))'), + repl, + line.strip()) + + +def demangle(func): + '''Demangle C++/Rust function names''' + + def demangle_with(func, tool): + if shutil.which(tool): + p = subprocess.Popen( + tool, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE) + out, _ = p.communicate(input=func.encode()) + return out.decode() + return func + return functools.reduce(demangle_with, ['cxxfilt', 'rustfilt'], func) + + +def transform(info): + '''Transform an error trace line''' + + info = info.strip() + if info.startswith('CALL') or info.startswith('RETURN from'): + tokens = info.split() + tokens[-1] = demangle(tokens[-1]) + return ' '.join(tokens) + elif '=' in info: + tokens = info.split('=') + lhs = tokens[0].strip() + rhs = tokens[1].strip() + return demangle(lhs) + ' = ' + reformat_assignment(rhs) + else: + return info + + +def corral_error_step(step): + '''Produce an error trace step based on a line of Corral error trace''' + + m = re.match(r'([^\s]*)\s+Trace:\s+(Thread=\d+)\s+\((.*)[\)|;]', step) + if m: + path = m.group(1) + tid = m.group(2) + info = ','.join(map(transform, + [x for x in m.group(3).split(',') if not + re.search( + (r'((CALL|RETURN from)\s+(\$|__SMACK))|' + r'Done|ASSERTION'), x)])) + return '{0}\t{1} {2}'.format(path, tid, info) + else: + return step + + +def error_step(step): + '''Produce an error trace step based on a line of verifier output''' + + FILENAME = r'[\w#$~%.\/-]*' + step = re.match(r"(\s*)(%s)\((\d+),\d+\): (.*)" % FILENAME, step) + if step: + if re.match('.*[.]bpl$', step.group(2)): + line_no = int(step.group(3)) + message = step.group(4) + if re.match(r'.*\$bb\d+.*', message): + message = "" + with open(step.group(2)) as f: + for line in f.read().splitlines(True)[line_no:line_no + 10]: + src = re.match( + r".*{:sourceloc \"(%s)\", (\d+), (\d+)}" % + FILENAME, line) + if src: + return "%s%s(%s,%s): %s" % (step.group(1), src.group( + 1), src.group(2), src.group(3), message) + else: + return corral_error_step(step.group(0)) + else: + return None + + +def error_trace(verifier_output, args): + '''Generate string error trace.''' + + trace = "" + for line in verifier_output.splitlines(True): + step = error_step(line) + if step: + m = re.match('(.*): [Ee]rror [A-Z0-9]+: (.*)', step) + if m: + trace += "%s: %s\nExecution trace:\n" % ( + m.group(1), m.group(2)) + else: + trace += ('' if step[0] == ' ' else ' ') + step + "\n" + + return trace + + +def smackdOutput(result, corralOutput): + '''Convert error traces into JSON format''' + + from .top import VResult + + if not (result is VResult.VERIFIED or result in VResult.ERROR): + return + + FILENAME = r'[\w#$~%.\/-]+' + traceP = re.compile( + ('(' + + FILENAME + + r')\((\d+),(\d+)\): Trace: Thread=(\d+)\s+\((.*(;\n)?.*)\)')) + # test1.i(223,16): Trace: Thread=1 (ASSERTION FAILS assert false; + errorP = re.compile( + ('(' + + FILENAME + + r')\((\d+),(\d+)\): Trace: Thread=\d+\s+\(ASSERTION FAILS')) + + if result is VResult.VERIFIED: + json_data = { + 'verifier': 'corral', + 'passed?': True + } + else: + traces = [] + raw_data = re.findall(traceP, corralOutput) + for t in raw_data: + file_name = t[0] + line_num = t[1] + col_num = t[2] + thread_id = t[3] + description = t[4] + for token in description.split(','): + traces.append( + {'threadid': thread_id, + 'file': file_name, + 'line': line_num, + 'column': col_num, + 'description': token, + 'assumption': transform(token) if '=' in token else ''}) + + r"""filename = '' + lineno = 0 + colno = 0 + threadid = 0 + desc = '' + for traceLine in corralOutput.splitlines(True): + traceMatch = traceP.match(traceLine) + if traceMatch: + filename = str(traceMatch.group(1)) + lineno = int(traceMatch.group(2)) + colno = int(traceMatch.group(3)) + threadid = int(traceMatch.group(4)) + desc = str(traceMatch.group(6)) + for e in desc.split(','): + e = e.strip() + assm = re.sub( + r'=(\s*\d+)bv\d+', + r'=\1', + e) if '=' in e else '' + trace = {'threadid': threadid, + 'file': filename, + 'line': lineno, + 'column': colno, + 'description': e, + 'assumption': assm} + traces.append(trace) + else: + errorMatch = errorP.match(traceLine) + if errorMatch: + filename = str(errorMatch.group(1)) + lineno = int(errorMatch.group(2)) + colno = int(errorMatch.group(3)) + desc = str(errorMatch.group(4))""" + errorMatch = errorP.search(corralOutput) + assert errorMatch, 'Failed to obtain assertion failure info!' + filename = str(errorMatch.group(1)) + lineno = int(errorMatch.group(2)) + colno = int(errorMatch.group(3)) + + failsAt = { + 'file': filename, + 'line': lineno, + 'column': colno, + 'description': result.description()} + + json_data = { + 'verifier': 'corral', + 'passed?': False, + 'failsAt': failsAt, + 'threadCount': 1, + 'traces': traces + } + json_string = json.dumps(json_data) + return json_string diff --git a/share/smack/frontend.py b/share/smack/frontend.py index 35943bb02..417646c97 100644 --- a/share/smack/frontend.py +++ b/share/smack/frontend.py @@ -2,7 +2,14 @@ import sys import re import json -from .utils import temporary_file, try_command +from .utils import temporary_file, try_command, temporary_directory +from .versions import RUST_VERSION + +# Needed for cargo operations +try: + import toml +except ImportError: + pass def languages(): @@ -25,6 +32,7 @@ def languages(): 'f95': 'fortran', 'f03': 'fortran', 'rs': 'rust', + 'toml': 'cargo', } @@ -45,6 +53,7 @@ def frontends(): 'boogie': boogie_frontend, 'fortran': fortran_frontend, 'rust': rust_frontend, + 'cargo': cargo_frontend, } @@ -85,12 +94,16 @@ def default_clang_compile_command(args, lib=False): cmd += ['-I' + path for path in smack_headers(args)] cmd += args.clang_options.split() cmd += ['-DMEMORY_MODEL_' + args.mem_mod.upper().replace('-', '_')] - if ('memory-safety' in args.check or 'valid-deref' in args.check or - 'valid-free' in args.check or 'memleak' in args.check): + + from .top import VProperty + + if args.check.contains_mem_safe_props(): cmd += ['-DMEMORY_SAFETY'] - if 'integer-overflow' in args.check: + if VProperty.INTEGER_OVERFLOW in args.check: cmd += (['-fsanitize=signed-integer-overflow,shift'] if not lib else ['-DSIGNED_INTEGER_OVERFLOW_CHECK']) + if VProperty.ASSERTIONS not in args.check: + cmd += ['-DDISABLE_SMACK_ASSERTIONS'] if args.float: cmd += ['-DFLOAT_ENABLED'] if args.pthread: @@ -265,20 +278,65 @@ def json_compilation_database_frontend(input_file, args): llvm_to_bpl(args) -def default_rust_compile_command(args): +def default_cargo_compile_command(args): compile_command = [ - 'rustc', - '-A', - 'unused-imports', - '-C', - 'opt-level=0', - '-C', - 'no-prepopulate-passes', - '-g', - '--cfg', - 'verifier="smack"', - '-C', - 'passes=name-anon-globals'] + 'cargo', + '+' + RUST_VERSION, + 'build'] + return compile_command + args + + +def cargo_frontend(input_file, args): + """Generate LLVM bitcode from a cargo build.""" + targetdir = temporary_directory( + os.path.splitext( + os.path.basename(input_file))[0], + None, + args) + rustargs = (default_rust_compile_args(args) + + ['--emit=llvm-bc', '-Clto', '-Cembed-bitcode=yes']) + compile_command = default_cargo_compile_command( + ['--target-dir', targetdir, '--manifest-path', input_file]) + try_command(compile_command, console=True, + env={'RUSTFLAGS': " ".join(rustargs)}) + + crate_name = toml.load(input_file)['package']['name'].replace('-', '_') + + # Find the name of the crate's bc file + bcbase = targetdir + '/debug/deps/' + entries = os.listdir(bcbase) + bcs = [] + + for entry in entries: + if entry.startswith(crate_name + '-') and entry.endswith('.bc'): + bcs.append(bcbase + entry) + + bc_file = temporary_file( + os.path.splitext( + os.path.basename(input_file))[0], + '.bc', + args) + try_command(['llvm-link'] + bcs + ['-o', bc_file]) + return bc_file + + +def default_rust_compile_args(args): + return ['-A', + 'unused-imports', + '-C', + 'opt-level=0', + '-C', + 'no-prepopulate-passes', + '-g', + '--cfg', + 'verifier="smack"', + '-C', + 'passes=name-anon-globals'] + + +def default_rust_compile_command(args): + compile_command = (['rustc', '+' + RUST_VERSION] + + default_rust_compile_args(args)) return compile_command + args @@ -309,7 +367,7 @@ def rust_frontend(input_file, args): def default_build_libs(args): """Generate LLVM bitcodes for SMACK libraries.""" bitcodes = [] - libs = ['smack.c', 'stdlib.c', 'errno.c'] + libs = ['smack.c', 'stdlib.c', 'errno.c', 'smack-rust.c'] if args.pthread: libs += ['pthread.c'] diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index 19f755c50..2255b9864 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -19,10 +19,13 @@ extern "C" { #define __builtin_expect __builtinx_expect #define __builtin_memcpy __builtinx_memcpy #define __builtin_va_start __builtinx_va_start +#define __builtin_va_arg(ap, t) __builtinx_va_arg(ap) #define __builtin_object_size __builtinx_object_size +#define __builtin_expect __builtinx_expect -// For handling of va_start macro +// For handling of va macros void __builtinx_va_start(char *, char *); +void *__builtinx_va_arg(char *); #endif void __SMACK_code(const char *fmt, ...); diff --git a/share/smack/include/string.h b/share/smack/include/string.h index 8c7c6c7c3..d1f53980f 100644 --- a/share/smack/include/string.h +++ b/share/smack/include/string.h @@ -7,6 +7,7 @@ #include void *memcpy(void *str1, const void *str2, size_t n); +int memcmp(const void *str1, const void *str2, size_t n); void *memset(void *str, int c, size_t n); char *strcpy(char *dest, const char *src); diff --git a/share/smack/lib/smack-rust.c b/share/smack/lib/smack-rust.c new file mode 100644 index 000000000..48c1401fc --- /dev/null +++ b/share/smack/lib/smack-rust.c @@ -0,0 +1,49 @@ +#include +#include + +#define mk_signed_type(size) int##size##_t +#define mk_unsigned_type(size) uint##size##_t + +#define mk_signed_min(size) INT##size##_MIN +#define mk_signed_max(size) INT##size##_MAX +#define mk_unsigned_min(size) 0 +#define mk_unsigned_max(size) UINT##size##_MAX + +#define mk_smack_signed_nondet(size) __SMACK_nondet_i##size +#define mk_smack_unsigned_nondet(size) __SMACK_nondet_u##size +#define mk_smack_nondet_decl(size) \ + mk_signed_type(size) mk_smack_signed_nondet(size)(void); \ + mk_unsigned_type(size) mk_smack_unsigned_nondet(size)(void); + +#define mk_smack_nondet_def(size) \ + mk_signed_type(size) __VERIFIER_nondet_i##size(void) { \ + mk_signed_type(size) ret = mk_smack_signed_nondet(size)(); \ + if (ret < mk_signed_min(size) || ret > mk_signed_max(size)) \ + abort(); \ + return ret; \ + } \ + mk_unsigned_type(size) __VERIFIER_nondet_u##size(void) { \ + mk_unsigned_type(size) ret = mk_smack_unsigned_nondet(size)(); \ + if (ret < mk_unsigned_min(size) || ret > mk_unsigned_max(size)) \ + abort(); \ + return ret; \ + } + +#define mk_dummy_nondet_def(size) \ + mk_signed_type(size) __VERIFIER_nondet_i##size(void) { \ + return *((mk_signed_type(size) *)malloc(sizeof(mk_signed_type(size)))); \ + } \ + mk_unsigned_type(size) __VERIFIER_nondet_u##size(void) { \ + return *( \ + (mk_unsigned_type(size) *)malloc(sizeof(mk_unsigned_type(size)))); \ + } + +#if CARGO_BUILD +mk_dummy_nondet_def(8) mk_dummy_nondet_def(16) mk_dummy_nondet_def(32) + mk_dummy_nondet_def(64) void __VERIFIER_assert(int x) {} +void __VERIFIER_assume(int x) {} +#else +mk_smack_nondet_decl(8) mk_smack_nondet_decl(16) mk_smack_nondet_decl(32) + mk_smack_nondet_decl(64) mk_smack_nondet_def(8) mk_smack_nondet_def(16) + mk_smack_nondet_def(32) mk_smack_nondet_def(64) +#endif diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 61c7651c0..c4b79a802 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -33,6 +33,13 @@ * */ +void *__builtinx_va_arg(char *x) { + __SMACK_code("assume false;"); + return 0; +} + +long __builtinx_expect(long exp, long c) { return exp; } + void __VERIFIER_assume(int x) { __SMACK_dummy(x); __SMACK_code("assume @ != $0;", x); @@ -40,13 +47,1363 @@ void __VERIFIER_assume(int x) { #ifndef CUSTOM_VERIFIER_ASSERT void __VERIFIER_assert(int x) { -#if !MEMORY_SAFETY && !SIGNED_INTEGER_OVERFLOW_CHECK +#if !DISABLE_SMACK_ASSERTIONS __SMACK_dummy(x); __SMACK_code("assert @ != $0;", x); #endif } #endif +int __SMACK_and32(int a, int b) { + int c = 0; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 2147483647) { + c += 1; + } + } + a = a % 2147483648; + a += a; + b = b % 2147483648; + b += b; + + return c; +} + +long __SMACK_and64(long a, long b) { return (long)__SMACK_and32(a, b); } + +short __SMACK_and16(short a, short b) { + short c = 0; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 32767) { + c += 1; + } + } + a = a % 32768; + a += a; + b = b % 32768; + b += b; + + return c; +} + +char __SMACK_and8(char a, char b) { + char c = 0; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + c += c; + if (a < 0) { + if (b < 0 || b > 127) { + c += 1; + } + } + a = a % 128; + a += a; + b = b % 128; + b += b; + + return c; +} + +int __SMACK_or32(int a, int b) { + int c = 0; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + c += c; + if (a < 0) { + c += 1; + } else if (b < 0) { + c += 1; + } + a += a; + a = a % 2147483648; + b += b; + b = b % 2147483648; + + return c; +} + +long __SMACK_or64(long a, long b) { return (long)__SMACK_or32(a, b); } +short __SMACK_or16(short a, short b) { return (short)__SMACK_or32(a, b); } +char __SMACK_or8(char a, char b) { return (char)__SMACK_or32(a, b); } + void __SMACK_check_overflow(int flag) { __SMACK_dummy(flag); __SMACK_code("assert {:overflow} @ == $0;", flag); @@ -330,8 +1687,6 @@ void __SMACK_decls(void) { " 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" - " p := $0.ref;\n" " }\n" "}\n"); @@ -464,8 +1819,6 @@ void __SMACK_decls(void) { " 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" - " p := $0.ref;\n" " }\n" "}\n"); diff --git a/share/smack/lib/smack.rs b/share/smack/lib/smack.rs index 21ec33bc3..86aa447be 100644 --- a/share/smack/lib/smack.rs +++ b/share/smack/lib/smack.rs @@ -4,14 +4,14 @@ extern "C" { pub fn __VERIFIER_assert(x: i32); pub fn __VERIFIER_assume(x: i32); - pub fn __VERIFIER_nondet_signed_char() -> i8; - pub fn __VERIFIER_nondet_unsigned_char() -> u8; - pub fn __VERIFIER_nondet_signed_short() -> i16; - pub fn __VERIFIER_nondet_unsigned_short() -> u16; - pub fn __VERIFIER_nondet_signed_int() -> i32; - pub fn __VERIFIER_nondet_unsigned_int() -> u32; - pub fn __VERIFIER_nondet_signed_long_long() -> i64; - pub fn __VERIFIER_nondet_unsigned_long_long() -> u64; + pub fn __VERIFIER_nondet_i8() -> i8; + pub fn __VERIFIER_nondet_u8() -> u8; + pub fn __VERIFIER_nondet_i16() -> i16; + pub fn __VERIFIER_nondet_u16() -> u16; + pub fn __VERIFIER_nondet_i32() -> i32; + pub fn __VERIFIER_nondet_u32() -> u32; + pub fn __VERIFIER_nondet_i64() -> i64; + pub fn __VERIFIER_nondet_u64() -> u64; pub fn malloc(size: usize) -> *mut u8; pub fn __VERIFIER_memcpy(dest: *mut u8, src: *mut u8, count: usize) -> *mut u8; pub fn free(ptr: *mut u8); @@ -129,16 +129,16 @@ macro_rules! make_verifier_nondet { } /* Instantiate nondet for all integer types. */ -make_verifier_nondet!(i8, __VERIFIER_nondet_signed_char); -make_verifier_nondet!(u8, __VERIFIER_nondet_unsigned_char); -make_verifier_nondet!(i16, __VERIFIER_nondet_signed_short); -make_verifier_nondet!(u16, __VERIFIER_nondet_unsigned_short); -make_verifier_nondet!(i32, __VERIFIER_nondet_signed_int); -make_verifier_nondet!(u32, __VERIFIER_nondet_unsigned_int); -make_verifier_nondet!(i64, __VERIFIER_nondet_signed_long_long); -make_verifier_nondet!(u64, __VERIFIER_nondet_unsigned_long_long); -make_verifier_nondet!(isize, __VERIFIER_nondet_signed_long_long); -make_verifier_nondet!(usize, __VERIFIER_nondet_unsigned_long_long); +make_verifier_nondet!(i8, __VERIFIER_nondet_i8); +make_verifier_nondet!(u8, __VERIFIER_nondet_u8); +make_verifier_nondet!(i16, __VERIFIER_nondet_i16); +make_verifier_nondet!(u16, __VERIFIER_nondet_u16); +make_verifier_nondet!(i32, __VERIFIER_nondet_i32); +make_verifier_nondet!(u32, __VERIFIER_nondet_u32); +make_verifier_nondet!(i64, __VERIFIER_nondet_i64); +make_verifier_nondet!(u64, __VERIFIER_nondet_u64); +make_verifier_nondet!(isize, __VERIFIER_nondet_i64); +make_verifier_nondet!(usize, __VERIFIER_nondet_u64); #[cfg(not(verifier = "smack"))] #[cfg(feature = "std")] diff --git a/share/smack/lib/smack/.gitignore b/share/smack/lib/smack/.gitignore new file mode 100644 index 000000000..693699042 --- /dev/null +++ b/share/smack/lib/smack/.gitignore @@ -0,0 +1,3 @@ +/target +**/*.rs.bk +Cargo.lock diff --git a/share/smack/lib/smack/Cargo.toml b/share/smack/lib/smack/Cargo.toml new file mode 100644 index 000000000..7e6757f16 --- /dev/null +++ b/share/smack/lib/smack/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "smack" +version = "0.1.0" +authors = ["Shaobo He "] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +[lib] +crate-type = ['rlib'] + +[build-dependencies] +cc = "1.0" + +[profile.dev] +incremental=false diff --git a/share/smack/lib/smack/build.rs b/share/smack/lib/smack/build.rs new file mode 100644 index 000000000..2f6c58cca --- /dev/null +++ b/share/smack/lib/smack/build.rs @@ -0,0 +1,12 @@ +// build.rs + +fn main() { + cc::Build::new() + .file("src/smack-rust.c") + .define("CARGO_BUILD", None) + .include("src") + .compiler("clang") + .compile("libsmack.a"); + println!("cargo:rerun-if-changed=src/smack-rust.c"); +} + diff --git a/share/smack/lib/string.c b/share/smack/lib/string.c index 8530aa86f..e6c0077aa 100644 --- a/share/smack/lib/string.c +++ b/share/smack/lib/string.c @@ -5,6 +5,27 @@ #include #include +int memcmp(const void *str1, const void *str2, size_t n) { + const unsigned char *s1 = (const unsigned char *)str1; + const unsigned char *s2 = (const unsigned char *)str2; + + while (n--) { + if (*s1 != *s2) { + int result = __VERIFIER_nondet_int(); + if (*s1 < *s2) { + __VERIFIER_assume(result < 0); + } else { + __VERIFIER_assume(result > 0); + } + return result; + } + s1++; + s2++; + } + + return 0; +} + char *strcpy(char *dest, const char *src) { char *save = dest; while ((*dest++ = *src++)) diff --git a/share/smack/reach.py b/share/smack/reach.py index b06b7462a..a86dfb28c 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '2.6.0' +VERSION = '2.6.1' def reachParser(): diff --git a/share/smack/svcomp/filters.py b/share/smack/svcomp/filters.py deleted file mode 100644 index 8e0ccda6d..000000000 --- a/share/smack/svcomp/filters.py +++ /dev/null @@ -1,218 +0,0 @@ -import sys -import re -import subprocess - -def linecount(p1, p2, s): - valid_lines = [] - lines = s.split('\n') - regex_p1 = re.compile(p1) - regex_p2 = re.compile(p2) - for line in lines: - r1 = regex_p1.search(line) - if r1: - r2 = regex_p2.search(line) - if r2 is None: - valid_lines.append(r1.group(0)) - return valid_lines - -def raw_file_line_count(s): - lines = s.split('\n') - count = 0 - #grep -v extern | grep -vP "^\w*$" | grep -v "#" - crap = re.compile(r"""(extern|^\w*$|#)""") - for line in lines: - if crap.search(line) is None: - count += 1 - - return count - -def svcomp_filter(f): - lines = None - with open(f, 'r') as inputfile: - lines = inputfile.read() - - pruned_lines = raw_file_line_count(lines) - raw_lines = len(lines.split('\n')) - - executable = False - if raw_lines < 50 and len(linecount(r'__VERIFIER_nondet|fopen', r'void\s+|extern', lines)) == 0 and not ('while(1)' in lines): - executable = True - - if bv_filter(lines, raw_lines, pruned_lines): - return 'bitvector', executable - - if float_filter(lines, raw_lines, pruned_lines): - return 'float', executable - - return 'normal', executable - -def bv_filter(lines, raw_line_count, pruned_line_count): - if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or - "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or - "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines or - "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or - "isinf_float" in lines or "trunc_float" in lines or "exponent_less_127" in lines): - return 0 - elif ('4294967294u' in lines or '616783' in lines or '__main(argc' in lines): - return 1 - - if raw_line_count > 1500: - if 'ldv_usb_gadget' in lines or "SyncPush" in lines or "kaweth_set_receive_filter" in lines: - return 1 - else: - return 0 - - #line_count = raw_file_line_count(lines) - if pruned_line_count > 650: - return 0 - - #special case for Concurrent benchmarks - if "pthread_create" in lines: - return 0 - - #cast patterns - if pruned_line_count <= 210: - - if pruned_line_count < 25 and 'while(1)' in lines: - return 1 - - casts = re.compile(r'''4294967295|plus_one|minus_one|\(x % 2\) == \(y % 2\)|linear_search|while \(\('0' <= c\) && \(c <= '9'\)\)''') - if casts.search(lines): - return 1 - #bwops = re.compile(r'''[^\&]\&[^\&]|[^\|]\|[^\|]|\^|>>|<<''') - bwops = re.compile(r'''[=|\(][^,]*[^\&|\(|{]\&\s|[^\|]\|\s|\^|>>|<<''') - #bwops = re.compile(r'''\s\&\s|\s\|\s|\^|>>|<<''') - #dv = re.compile(r'''1\s+<<\s+[1|5]|cil''') - dv = re.compile(r'''1.*<<.*\"|cil|found|node''') - - for line in lines.split('\n'): - if bwops.search(line): - if dv.search(line) is None: - #print line - return 1 - #print raw_file_line_count(lines) - return 0 - -def float_filter(lines, raw_line_count, pruned_line_count): - fliteral = 0 - ddecl = 0 - - if ("bugBrokenOut" in lines or "returnsStructure" in lines or "__VERIFIER_nondet_double" in lines or - "__VERIFIER_nondet_float" in lines or "0x43300000" in lines or "float X, P;" in lines or "1415926538837245" in lines or - "huge_floor" in lines or "huge_ceil" in lines or "tiny_sqrt" in lines or "fmax_float" in lines or - "fabs_double" in lines or "round_double" in lines or "trunc_double" in lines or "zero_log" in lines or - "isinf_float" in lines or "trunc_float" in lines or "exponent_less_127" in lines): - return 1 - - #heuristic #-1: don't do test on too large programs - if raw_line_count >= 2000: - return 0 - #heuristic #0: more than Float.set maximum LOC ==> not - if pruned_line_count > 140: #(138 = maximum) - return 0 - #heuristic #1: __VERIFIER_nondet ==> float category - result = re.search(r"""(__VERIFIER_nondet_(float|double)|ieee754_float)""", lines) - if result: - return 1 - - #heuristic #2: check float literal # - valid_lines = linecount(r"""(0x)?\d+\.\d*(f|p|e)?""", r"""#|line|June|CIL|0\.000000|\"\d+|Created""", lines) - count = len(valid_lines) - if count > 60: - return 0 - if count == 0: - #heuristic #3: check double - #result = re.search(r"""0x\d+\.?.*p|double""", lines) - result = re.search(r"""double""", lines) - if result: - return 1 - else: - return 0 - else: - #heuristic #4: for loops/heapmanipulation - #print valid_lines - regex_special = re.compile(r"""1\.4p|1\.0e""") - for valid_line in valid_lines: - if regex_special.search(valid_line) is not None and count <= 4: - return 0 - if valid_line == '1.' or valid_line == '2.': - if 'double' not in lines: - return 0 - else: - return 1 - return 1 - - -def scrub_pthreads(s): - if 'pthread_create' not in s: - return s, False - - # special case for sequentialized benchmarks - if '__CS_pthread_create' in s: - return s, False - - # special case for machzwd benchmarks - if 'assert_context_process' in s: - return s, False - - #These are strings that will conflict with our pthread header files - #To generate additional strings, copy paste the text. - #Escape all characters that need to be escaped for regex (at least *[]() - # Then replace all newlines and spaces with \s+. Lastly, replace all - # \s+\s+ to \s+. Do this last step until string doesn't change anymore. - fltrs = list() - fltrs.append(r'typedef\s+unsigned\s+long\s+int\s+pthread_t;') - #pthread_attr_t - fltrs.append(r'typedef\s+union\s+{\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_attr_t;') - fltrs.append(r'union\s+pthread_attr_t\s+{\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+};\s+typedef\s+union\s+pthread_attr_t\s+pthread_attr_t;') - #pthread_mutexattr_t - fltrs.append(r'typedef\s+union\s+{\s+char\s+__size\[\d+\];\s+int\s+__align;\s+}\s+pthread_mutexattr_t;') - fltrs.append(r'typedef\s+union\s+{\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutexattr_t;') - #pthread_mutex_t - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+unsigned\s+int\s+__nusers;\s+int\s+__kind;\s+int\s+__spins;\s+__pthread_list_t\s+__list;\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+int\s+__kind;\s+unsigned\s+int\s+__nusers;\s+__extension__\s+union\s+{\s+struct\s+{\s+short\s+__espins;\s+short\s+__elision;\s+}\s+__elision_data;\s+__pthread_slist_t\s+__list;\s+};\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+int\s+__kind;\s+unsigned\s+int\s+__nusers;\s+__extension__\s+union\s+{\s+int\s+__spins;\s+__pthread_slist_t\s+__list;\s+};\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+unsigned\s+int\s+__nusers;\s+int\s+__kind;\s+short\s+__spins;\s+short\s+__elision;\s+__pthread_list_t\s+__list;\s+# 124 "/usr/include/x86_64-linux-gnu/bits/pthreadtypes\.h" 3 4\s+}\s+__data;\s+\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+} pthread_mutex_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+int\s+__kind;\s+unsigned\s+int\s+__nusers;\s+__extension__\s+union\s+{\s+struct\s+{\s+short\s+__espins;\s+short\s+__elision;\s+}\s+d;\s+__pthread_slist_t\s+__list;\s+};\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__count;\s+int\s+__owner;\s+unsigned\s+int\s+__nusers;\s+int\s+__kind;\s+short\s+__spins;\s+short\s+__elision;\s+__pthread_list_t\s+__list;\s+}\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_mutex_s\s+__data;\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_mutex_t;') - #pthread_cond_t - fltrs.append(r'typedef\s+union\s+{\s+struct\s+{\s+int\s+__lock;\s+unsigned\s+int\s+__futex;\s+__extension__\s+unsigned\s+long\s+long\s+int\s+__total_seq;\s+__extension__\s+unsigned\s+long\s+long\s+int\s+__wakeup_seq;\s+__extension__\s+unsigned\s+long\s+long\s+int\s+__woken_seq;\s+void\s+\*__mutex;\s+unsigned\s+int\s+__nwaiters;\s+unsigned\s+int\s+__broadcast_seq;\s+}\s+__data;\s+char\s+__size\[\d+\];\s+__extension__\s+long\s+long\s+int\s+__align;\s+}\s+pthread_cond_t;') - fltrs.append(r'typedef\s+union\s+{\s+struct\s+__pthread_cond_s\s+__data;\s+char\s+__size\[\d+\];\s+__extension__\s+long\s+long\s+int\s+__align;\s+}\s+pthread_cond_t;') - #pthread_condattr_t - fltrs.append(r'typedef\s+union\s+{\s+char\s+__size\[\d+\];\s+int\s+__align;\s+}\s+pthread_condattr_t;') - fltrs.append(r'typedef\s+union\s+{\s+char\s+__size\[\d+\];\s+long\s+int\s+__align;\s+}\s+pthread_condattr_t;') - #enums - fltrs.append(r'enum\s+{\s+PTHREAD_MUTEX_TIMED_NP,\s+PTHREAD_MUTEX_RECURSIVE_NP,\s+PTHREAD_MUTEX_ERRORCHECK_NP,\s+PTHREAD_MUTEX_ADAPTIVE_NP\s+,\s+PTHREAD_MUTEX_NORMAL\s+=\s+PTHREAD_MUTEX_TIMED_NP,\s+PTHREAD_MUTEX_RECURSIVE\s+=\s+PTHREAD_MUTEX_RECURSIVE_NP,\s+PTHREAD_MUTEX_ERRORCHECK\s+=\s+PTHREAD_MUTEX_ERRORCHECK_NP,\s+PTHREAD_MUTEX_DEFAULT\s+=\s+PTHREAD_MUTEX_NORMAL\s+};') - fltrs.append(r'enum\s+{\s+PTHREAD_MUTEX_TIMED_NP,\s+PTHREAD_MUTEX_RECURSIVE_NP,\s+PTHREAD_MUTEX_ERRORCHECK_NP,\s+PTHREAD_MUTEX_ADAPTIVE_NP\s+};') - #pthread_cond_init decl - fltrs.append(r'extern\s+int\s+pthread_cond_init\s+\(pthread_cond_t\s+\*__restrict\s+__cond,\s+__const\s+pthread_condattr_t\s+\*__restrict\s+__cond_attr\)\s+__attribute__\s+\(\(__nothrow__\s+,\s+__leaf__\)\)\s+__attribute__\s+\(\(__nonnull__\s+\(\d+\)\)\);') - fltrs.append(r'extern\s+int\s+pthread_cond_init\s*\(pthread_cond_t\s+\*__restrict\s+__cond,\s+const\s+pthread_condattr_t\s+\*__restrict\s+__cond_attr\)\s+__attribute__\s*\(\(__nothrow__\s+,\s+__leaf__\)\)\s+__attribute__\s+\(\(__nonnull__\s+\(1\)\)\);') - fltrs.append(r'extern\s+int\s+pthread_cond_init\s*\(pthread_cond_t\s+\*__restrict\s+__cond,\s+__const\s+pthread_condattr_t\s+\*__restrict\s+__cond_attr\)\s+__attribute__\s+\(\(__nothrow__\)\)\s+__attribute__\s+\(\(__nonnull__\s+\(1\)\)\);') - #__VERIFIER_atomic_begin definition removal - fltrs.append(r'int\s+__global_lock;\s+void\s+__VERIFIER_atomic_begin\(\)\s+{\s+__VERIFIER_assume\(__global_lock==0\);\s+__global_lock=1;\s+return;\s+}\s+void\s+__VERIFIER_atomic_end\(\)\s+{\s+__VERIFIER_assume\(__global_lock==1\);\s+__global_lock=0;\s+return;\s+}') - - - #Remove each occurrence - for fltr in fltrs: - #sold = s - pat = re.compile(fltr, re.MULTILINE); - s = pat.sub('', s) - #if sold == s: - # print("Didn't match - " + fltr) - #else: - # print("DID match - " + fltr) - - s = re.sub(r'(__VERIFIER_atomic_((?!begin|end).)*?\(.*?\);)', - r'__VERIFIER_atomic_begin(); \1 __VERIFIER_atomic_end();', - s) - - s = re.sub(r'\ninline ', r'\n', s) - - return s, True - - -if __name__ == '__main__': - print("What?") - print(svcomp_filter(sys.argv[1])) - diff --git a/share/smack/svcomp/random_testing.py b/share/smack/svcomp/random_testing.py deleted file mode 100644 index fa9d09aff..000000000 --- a/share/smack/svcomp/random_testing.py +++ /dev/null @@ -1,66 +0,0 @@ -import re -import os -import smack.top -import subprocess -import sys - -def random_test(args, result): - f = args.input_files[0] - - # test if a file can be tested - with open(f, 'r') as fi: - s = fi.read() - - l = s.split('\n') - if not (len(l) < 20 and len([x for x in l if re.search(r'=\s*__VERIFIER_nondet_uint', x)]) == 1): - return 'abort' - - UMAX_INT = 2**32 - 1 - for i in [8, 4, 2]: - status = compile_and_run(f, s, UMAX_INT/i, args) - if status != 'true': - return status - - return result - -def compile_and_run(f, s, n, args): - s = re.sub("=\s*(__VERIFIER_nondet_uint\(\))", "="+str(n), s) - s = re.sub("__VERIFIER_assert\((.+)\);", "assert(\\1);", s) - s = re.sub(r'(extern )?void reach_error()', '//', s) - s = re.sub(r'(extern )?void __VERIFIER_assume()', '//', s) - s = re.sub(r'reach_error\(\)', 'assert(0)', s) - s = '#include\n' + s - - name = os.path.splitext(os.path.basename(f))[0] - tmp1 = smack.top.temporary_file(name, '.c', args) - with open(tmp1, 'w') as fo: - fo.write(s) - - tmp2 = smack.top.temporary_file(name, '.bin', args) - tmp2 = tmp2.split('/')[-1] - #compile and run - cmd = ['clang', tmp1, '-o', tmp2] - - proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) - - out, err = proc.communicate() - rc = proc.returncode - - if rc: - print('Compiling error') - print(err) - return 'unknown' - else: - cmd = [r'./' + tmp2] - proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) - out, err = proc.communicate() - rc = proc.returncode - if rc: - if re.search(r'Assertion.*failed', err): - return 'false' - else: - print('Execution error') - print(err) - return 'unknown' - else: - return 'true' diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py index d9fe441d2..346ccbef5 100644 --- a/share/smack/svcomp/toSVCOMPformat.py +++ b/share/smack/svcomp/toSVCOMPformat.py @@ -30,6 +30,7 @@ def addKeyDefs(root): #keys are [attr.name, attr.type, for, id, hasDefault, defaultVal] keys.append(["assumption", "string", "edge", "assumption", False]) keys.append(["assumption.scope", "string", "edge", "assumption.scope", False]) + keys.append(["assumption.resultfunction", "string", "edge", "assumption.resultfunction", False]) keys.append(["sourcecode", "string", "edge", "sourcecode", False]) keys.append(["witness-type", "string", "graph", "witness-type", False]) keys.append(["sourcecodeLanguage", "string", "graph", "sourcecodelang", False]) @@ -153,7 +154,7 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status): lastNode = start lastEdge = None - pat = re.compile(".*smack\.[c|h]$") + pat = re.compile(".*/smack/lib/.+\.[c|h]$") prevLineNo = -1 prevColNo = -1 callStack = [('main', '0')] @@ -167,19 +168,25 @@ def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status): for vNode in vNodes: if vNode.attrib["id"] == newNode: addKey(vNode, "violation", "true") - attribs = {"startline":str(callStack[-1][1])} + attribs = {"startline":str(jsonViolation['line'])} addGraphEdge(tree, lastNode, newNode, attribs) break if not pat.match(jsonTrace["file"]): desc = jsonTrace["description"] formattedAssign = formatAssign(desc) # Make sure it is not return value - if formattedAssign and not ":" in formattedAssign: + if formattedAssign and formattedAssign.startswith('smack:ext:__VERIFIER_nondet'): + tokens = formattedAssign.split('==') + nondet_func = tokens[0].strip()[len('smack:ext:'):] + val = tokens[1].strip() + new_assumption = '\\result == %s;' % val # Create new node and edge newNode = addGraphNode(tree) attribs = {"startline":str(jsonTrace["line"])} - attribs["assumption"] = formattedAssign + ";" - attribs["assumption.scope"] = callStack[-1][0] + attribs["assumption"] = new_assumption + attribs['assumption.resultfunction'] = nondet_func + scope_func = callStack[-1][0] + attribs["assumption.scope"] = scope_func.split('.')[0] if '.' in scope_func else scope_func newEdge = addGraphEdge(tree, lastNode, newNode, attribs) prevLineNo = jsonTrace["line"] prevColNo = jsonTrace["column"] diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 2272df8e0..71970efeb 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -6,17 +6,19 @@ from shutil import copyfile import smack.top import smack.frontend -from . import filters from .toSVCOMPformat import smackJsonToXmlGraph -from .random_testing import random_test def svcomp_frontend(input_file, args): """Generate Boogie code from SVCOMP-style C-language source(s).""" # enable static LLVM unroll pass args.static_unroll = True - # disable dynamic execution - args.execute = False + + # attempt to rewrite bitwise ops into provided models + args.rewrite_bitwise_ops = True + + # Modeling of strings must be turned on by default + args.strings = True if len(args.input_files) > 1: raise RuntimeError("Expected a single SVCOMP input file.") @@ -24,33 +26,11 @@ def svcomp_frontend(input_file, args): # check svcomp properties and set flags accordingly svcomp_check_property(args) - # fix: disable float filter for memory safety benchmarks - if not ('memory-safety' in args.check or 'memleak' in args.check): - # test bv and executable benchmarks - file_type, executable = filters.svcomp_filter(args.input_files[0]) - if file_type == 'bitvector': - args.integer_encoding = 'bit-vector' - args.pointer_encoding = 'bit-vector' - if file_type == 'float' and not 'integer-overflow' in args.check: - args.float = True - args.integer_encoding = 'bit-vector' - with open(input_file, "r") as sf: - sc = sf.read() - if 'copysign(1' in sc: - args.pointer_encoding = 'bit-vector' - args.execute = executable - else: - with open(input_file, "r") as sf: - sc = sf.read() - if "unsigned char b:2" in sc or "4294967294u" in sc or "_ddv_module_init" in sc or "bb_process_escape_sequence" in sc: - args.integer_encoding = 'bit-vector' - #args.pointer_encoding = 'bit-vector' - - if 'memory-safety' in args.check or 'memleak' in args.check or 'integer-overflow' in args.check: - args.strings = True + if smack.top.VProperty.INTEGER_OVERFLOW in args.check: + args.integer_encoding = 'bit-vector' name, ext = os.path.splitext(os.path.basename(args.input_files[0])) - svcomp_process_file(args, name, ext) + args.orig_files = list(args.input_files) args.clang_options += " -fbracket-depth=2048" args.clang_options += " -Wno-unknown-attributes" @@ -71,293 +51,69 @@ def svcomp_frontend(input_file, args): smack.top.link_bc_files([bc],libs,args) def svcomp_check_property(args): - # Check if property is vanilla reachability, and return unknown otherwise if args.svcomp_property: with open(args.svcomp_property, "r") as f: prop = f.read() + from smack.top import VProperty + from smack.top import VResult if "valid-deref" in prop: - args.check = ['memory-safety'] + args.check = VProperty.VALID_DEREF elif "valid-memcleanup" in prop: - args.check = ['memleak'] + args.check = VProperty.MEMLEAK elif "overflow" in prop: - args.check = ['integer-overflow'] + args.check = VProperty.INTEGER_OVERFLOW elif not "reach_error" in prop: - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) - -def svcomp_process_file(args, name, ext): - args.orig_files = list(args.input_files) - with open(args.input_files[0], 'r') as fi: - s = fi.read() - args.input_files[0] = smack.top.temporary_file(name, ext, args) - # replace exit definition with exit_ - s = re.sub(r'void\s+exit\s*\(int s\)', r'void exit_(int s)', s) - if not ('direc_start' in s or 'just_echo' in s): - s = re.sub(r'argv\[i\]=malloc\(11\);\s+argv\[i\]\[10\]\s+=\s+0;\s+for\(int\s+j=0;\s+j<10;\s+\+\+j\)\s+argv\[i\]\[j\]=__VERIFIER_nondet_char\(\);', r'argv[i] = malloc(3);\n argv[i][0] = __VERIFIER_nondet_char();\n argv[i][1] = __VERIFIER_nondet_char();\n argv[i][2] = 0;', s) - s = re.sub(r'char\s+\*a\s+=\s+malloc\(11\);\s+a\[10\]\s+=\s+0;\s+for\(int\s+i=0;\s+i<10;\s+\+\+i\)\s+a\[i\]=__VERIFIER_nondet_char\(\);', r'char *a = malloc(3);\n a[0] = __VERIFIER_nondet_char();\n a[1] = __VERIFIER_nondet_char();\n a[2] = 0;', s) - s = re.sub(r'static\s+char\s+dir\[42\];\s+for\(int\s+i=0;\s+i<42;\s+\+\+i\)\s+dir\[i\]\s+=\s+__VERIFIER_nondet_char\(\);\s+dir\[41\]\s+=\s+\'\\0\';', r'static char dir[3];\n dir[0] = __VERIFIER_nondet_char();\n dir[1] = __VERIFIER_nondet_char();\n dir[2] = 0;', s) - s = re.sub(r'__VERIFIER_assume\(i < 16\);', r'__VERIFIER_assume(i >= 0 && i < 16);', s) - - if 'memory-safety' in args.check and not 'argv=malloc' in s: - s = re.sub(r'typedef long unsigned int size_t', r'typedef unsigned int size_t', s) - elif 'memory-safety' in args.check and re.search(r'getopt32\([^,)]+,[^,)]+,[^.)]+\);', s): - if not args.quiet: - print("Stumbled upon a benchmark that requires precise handling of vararg\n") - while (True): - pass - elif 'memory-safety' in args.check and ('count is too big' in s or 'pdRfilsLHarPv' in s or 'rnugG' in s): - if not args.quiet: - print("Stumbled upon a benchmark that contains undefined behavior\n") - while (True): - pass - - if 'argv=malloc' in s: -# args.integer_encoding = 'bit-vector' - if 'integer-overflow' in args.check and ('unsigned int d = (unsigned int)((signed int)(unsigned char)((signed int)*q | (signed int)(char)32) - 48);' in s or 'bb_ascii_isalnum' in s or 'ptm=localtime' in s or '0123456789.' in s): - args.integer_encoding = 'bit-vector' - args.pointer_encoding = 'bit-vector' - - length = len(s.split('\n')) - if length < 60: - # replace all occurrences of 100000 with 10 and 15000 with 5 - # Only target at small examples - s = re.sub(r'100000', r'10', s) - s = re.sub(r'15000', r'5', s) - s = re.sub(r'i<=10000', r'i<=1', s) - s = re.sub(r'500000', r'50', s) - elif length < 710 and 'dll_create_master' in s: - args.no_memory_splitting = True - - #Remove any preprocessed declarations of pthread types - #Also, if file contains 'pthread', set pthread mode - s,args.pthread = filters.scrub_pthreads(s) - if args.pthread: - s = "#include \n" + s - with open(args.input_files[0], 'w') as fo: - fo.write(s) + result = VResult.UNKNOWN + print(result.message(args)) + sys.exit(result.return_code()) def force_timeout(): sys.stdout.flush() time.sleep(1000) -def is_buggy_driver_benchmark(args, bpl): - if ("205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call" in bpl or - "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or - "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--media--dvb-core--dvb-core.ko-ldv_main5_sequence_infinite_withcheck_stateful" in bpl or - "32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--seq--snd-seq.ko-ldv_main2_sequence_infinite_withcheck_stateful" in bpl or - "43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call" in bpl or - "linux-3.14__complex_emg__linux-drivers-clk1__drivers-net-ethernet-ethoc_true-unreach-call" in bpl or - "linux-3.14__linux-usb-dev__drivers-media-usb-hdpvr-hdpvr_true-unreach-call" in bpl or - "linux-4.2-rc1.tar.xz-32_7a-drivers--net--usb--r8152.ko-entry_point_true-unreach-call" in bpl or - "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-smsc-smsc911x_true-unreach-call" in bpl or - "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call" in bpl or - "linux-4.2-rc1.tar.xz-32_7a-drivers--usb--gadget--libcomposite.ko-entry_point_true-unreach-call" in bpl or - "linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call" in bpl or - "linux-4.0-rc1---drivers--media--usb--uvc--uvcvideo.ko_false-unreach-call" in bpl or - "linux-4.0-rc1---drivers--char--ipmi--ipmi_msghandler.ko_true-unreach-call" in bpl or - "205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--libertas_tf--libertas_tf.ko-entry_point_true-unreach-call" in bpl or - "linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-raid.ko-entry_point_false-unreach-call" in bpl or - "linux-4.2-rc1.tar.xz-43_2a-drivers--net--ppp--ppp_generic.ko-entry_point_true-unreach-call" in bpl): - if not args.quiet: - print("Stumbled upon a buggy device driver benchmark\n") - force_timeout() - -def is_stack_benchmark(args, csource): - if ("getNumbers" in csource or "areNatural" in csource or "myPointerA" in csource or "if(i == 0) {" in csource or - "arr[194]" in csource or "if(1)" in csource or "alloca(10" in csource or "p[0] = 2;" in csource): - if not args.quiet: - print("Stumbled upon a stack-based memory safety benchmark\n") - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) - def inject_assert_false(args): - with open(args.bpl_file, 'r') as bf: - content = bf.read() - content = content.replace('call reach_error();', 'assert false; call reach_error();') - with open(args.bpl_file, 'w') as bf: - bf.write(content) + with open(args.bpl_file, 'r') as bf: + content = bf.read() + content = content.replace('call reach_error();', 'assert false; call reach_error();') + with open(args.bpl_file, 'w') as bf: + bf.write(content) def verify_bpl_svcomp(args): """Verify the Boogie source file using SVCOMP-tuned heuristics.""" heurTrace = "\n\nHeuristics Info:\n" - if not 'memory-safety' in args.check and not 'memleak' in args.check and not 'integer-overflow' in args.check: - inject_assert_false(args) - - if 'memory-safety' in args.check: - if len(args.check) == 1: - heurTrace = "engage valid deference checks.\n" - args.check.pop() - args.check.append('valid-deref') - args.prop_to_check = 'valid-deref' - args.bpl_with_all_props = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) - copyfile(args.bpl_file, args.bpl_with_all_props) - smack.top.memsafety_subproperty_selection(args) - args.check.append('memory-safety') - elif 'valid-deref' in args.check: - heurTrace = "engage valid free checks.\n" - args.check.pop() - args.check.pop() - args.prop_to_check = 'valid-free' - args.check.append('valid-free') - args.bpl_file = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) - copyfile(args.bpl_with_all_props, args.bpl_file) - smack.top.memsafety_subproperty_selection(args) - args.check.append('memory-safety') - elif 'valid-free' in args.check: - heurTrace = "engage memleak checks.\n" - args.check.pop() - args.check.pop() - args.prop_to_check = 'memleak' - args.check.append('memleak') - args.bpl_file = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) - copyfile(args.bpl_with_all_props, args.bpl_file) - smack.top.memsafety_subproperty_selection(args) - args.check.append('memory-safety') - elif 'memleak' in args.check: - heurTrace = "engage memcleanup checks.\n" - smack.top.memsafety_subproperty_selection(args) + from smack.top import VProperty + from smack.top import VResult - # If pthreads found, perform lock set analysis - if args.pthread: - lockpwn_command = ["lockpwn"] - lockpwn_command += [args.bpl_file] - lockpwn_command += ["/corral"] - args.bpl_file = smack.top.temporary_file(os.path.splitext(os.path.basename(args.bpl_file))[0], '.bpl', args) - lockpwn_command += ["/o:%s" % args.bpl_file] - lockpwn_output = smack.top.try_command(lockpwn_command); + if not (VProperty.MEMORY_SAFETY in args.check + or VProperty.MEMLEAK in args.check + or VProperty.INTEGER_OVERFLOW in args.check): + inject_assert_false(args) corral_command = ["corral"] corral_command += [args.bpl_file] corral_command += ["/tryCTrace", "/noTraceOnDisk", "/printDataValues:1"] corral_command += ["/useProverEvaluate", "/cex:1"] corral_command += ["/bopt:proverOpt:O:smt.qi.eager_threshold=100"] - - with open(args.bpl_file, "r") as f: - bpl = f.read() + corral_command += ["/bopt:proverOpt:O:smt.arith.solver=2"] with open(args.input_files[0], "r") as f: csource = f.read() - if 'memory-safety' in args.check: - is_stack_benchmark(args, csource) - else: - if "angleInRadian" in csource: - if not args.quiet: - print("Stumbled upon trigonometric function is float benchmark\n") - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) - elif "copysign(1" in csource: - if not args.quiet: - print("Stumbled upon tricky float benchmark\n") - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) - is_buggy_driver_benchmark(args, bpl) - - if args.pthread: - if "fib_bench" in bpl or "27_Boop_simple_vf_false-unreach-call" in bpl or "k < 5;" in csource or "k < 10;" in csource or "k < 20;" in csource: - heurTrace += "Increasing context switch bound for certain pthread benchmarks.\n" - corral_command += ["/k:30"] - else: - corral_command += ["/k:3"] - if not "qrcu_reader2" in bpl and not "__VERIFIER_atomic_take_write_lock" in bpl and not "fib_bench" in bpl: - corral_command += ["/cooperative"] - else: - corral_command += ["/k:1"] - if not ('memory-safety' in args.check or args.integer_encoding == 'bit-vector' or 'memleak' in args.check): - if not ("dll_create" in csource or "sll_create" in csource or "changeMethaneLevel" in csource): - corral_command += ["/di"] - - # we are not modeling strcpy - if args.pthread and "strcpy" in bpl: - heurTrace += "We are not modeling strcpy - aborting\n" - if not args.quiet: - print((heurTrace + "\n")) - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) + corral_command += ["/k:1"] + if not (VProperty.MEMORY_SAFETY in args.check + or args.integer_encoding == 'bit-vector' + or VProperty.MEMLEAK in args.check): + if not ("dll_create" in csource or "sll_create" in csource or "changeMethaneLevel" in csource): + corral_command += ["/di"] # Setting good loop unroll bound based on benchmark class - loopUnrollBar = 8 - staticLoopBound = 65536 - if not args.integer_encoding == 'bit-vector' and "ssl3_accept" in bpl and "s__s3__tmp__new_cipher__algorithms" in bpl: - heurTrace += "ControlFlow benchmark detected. Setting loop unroll bar to 23.\n" - loopUnrollBar = 23 - elif "s3_srvr.blast.10_false-unreach-call" in bpl or "s3_srvr.blast.15_false-unreach-call" in bpl: - heurTrace += "ControlFlow benchmark detected. Setting loop unroll bar to 23.\n" - loopUnrollBar = 23 - elif "NonTerminationSimple4_false-no-overflow" in bpl: - heurTrace += "Overflow benchmark detected. Setting loop unroll bar to 1024.\n" - loopUnrollBar = 1024 - elif " node3" in bpl: - heurTrace += "Sequentialized benchmark detected. Setting loop unroll bar to 100.\n" - loopUnrollBar = 100 - elif "calculate_output" in bpl or "psyco" in bpl: - heurTrace += "ECA benchmark detected. Setting loop unroll bar to 15.\n" - loopUnrollBar = 15 - elif "ldv" in bpl: - if "linux-4.2-rc1.tar.xz-08_1a-drivers--staging--lustre--lustre--llite--llite_lloop.ko-entry_point" in bpl or "linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-hdpvr-hdpvr" in bpl: - heurTrace += "Special LDV benchmark detected. Setting loop unroll bar to 32.\n" - loopUnrollBar = 32 - else: - heurTrace += "LDV benchmark detected. Setting loop unroll bar to 13.\n" - loopUnrollBar = 13 - staticLoopBound = 64 - elif "standard_strcpy_false-valid-deref_ground_true-termination" in bpl or "960521-1_false-valid-free" in bpl or "960521-1_false-valid-deref" in bpl or "lockfree-3.3" in bpl or "list-ext_false-unreach-call_false-valid-deref" in bpl: - heurTrace += "Memory safety benchmark detected. Setting loop unroll bar to 129.\n" - loopUnrollBar = 129 - elif "is_relaxed_prefix" in bpl: - heurTrace += "Benchmark relax_* detected. Setting loop unroll bar to 15.\n" - loopUnrollBar = 15 - elif "id_o1000_false-unreach-call" in bpl: - heurTrace += "Recursive benchmark detected. Setting loop unroll bar to 1024.\n" - loopUnrollBar = 1024 - elif "n.c24" in bpl or "array_false-unreach-call3" in bpl: - heurTrace += "Loops benchmark detected. Setting loop unroll bar to 1024.\n" - loopUnrollBar = 1024 - 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 'memory-safety' in args.check and "__main($i0" in bpl: - heurTrace += "BusyBox memory safety benchmark detected. Setting loop unroll bar to 4.\n" - loopUnrollBar = 4 - elif 'integer-overflow' in args.check and "__main($i0" in bpl: - heurTrace += "BusyBox overflows benchmark detected. Setting loop unroll bar to 40.\n" - loopUnrollBar = 40 - elif 'integer-overflow' in args.check and ("jain" in bpl or "TerminatorRec02" in bpl or "NonTerminationSimple" in bpl): - heurTrace += "Infinite loop in overflow benchmark. Setting loop unroll bar to INT_MAX.\n" - loopUnrollBar = 2**31 - 1 - elif 'integer-overflow' in args.check and ("(x != 0)" in csource or "(z > 0)" in csource or "(max > 0)" in csource or - "(k < N)" in csource or "partial_sum" in csource): - heurTrace += "Large overflow benchmark. Setting loop unroll bar to INT_MAX.\n" - loopUnrollBar = 2**31 - 1 - elif "i>>16" in csource: - heurTrace += "Large array reach benchmark. Setting loop unroll bar to INT_MAX.\n" - loopUnrollBar = 2**31 - 1 - elif "whoop_poll_table" in csource: - heurTrace += "Large concurrency benchmark. Setting loop unroll bar to INT_MAX.\n" - loopUnrollBar = 2**31 - 1 - - if not "forall" in bpl: - heurTrace += "No quantifiers detected. Setting z3 relevancy to 0.\n" - corral_command += ["/bopt:proverOpt:O:smt.relevancy=0"] - - if 'memory-safety' in args.check: - if args.prop_to_check == 'valid-deref': - if "memleaks_test12_false-valid-free" in bpl: - time_limit = 10 - else: - time_limit = 750 - elif args.prop_to_check == 'valid-free': - time_limit = 80 - elif args.prop_to_check == 'memleak': - time_limit = 50 - else: - time_limit = 880 + loopUnrollBar = 13 + time_limit = 880 command = list(corral_command) command += ["/timeLimit:%s" % time_limit] command += ["/v:1"] - command += ["/maxStaticLoopBound:%d" % staticLoopBound] command += ["/recursionBound:65536"] command += ["/irreducibleLoopUnroll:12"] command += ["/trackAllVars"] @@ -365,22 +121,14 @@ def verify_bpl_svcomp(args): verifier_output = smack.top.try_command(command, timeout=time_limit) result = smack.top.verification_result(verifier_output) - if result == 'error' or result == 'invalid-deref' or result == 'invalid-free' or result == 'invalid-memtrack' or result == 'overflow': #normal inlining + if result in VResult.ERROR: #normal inlining heurTrace += "Found a bug during normal inlining.\n" if not args.quiet: error = smack.top.error_trace(verifier_output, args) print(error) - if 'memory-safety' in args.check: - heurTrace += (args.prop_to_check + "has errors\n") - if args.prop_to_check == 'valid-free': - if args.valid_deref_check_result != 'verified': - force_timeout() - elif args.prop_to_check == 'memleak': - if args.valid_free_check_result == 'timeout': - force_timeout() - elif result == 'timeout': #normal inlining + elif result is VResult.TIMEOUT: #normal inlining heurTrace += "Timed out during normal inlining.\n" heurTrace += "Determining result based on how far we unrolled.\n" # If we managed to unroll more than loopUnrollBar times, then return verified @@ -399,42 +147,11 @@ def verify_bpl_svcomp(args): heurTrace += "Unrolling made it to a recursion bound of " heurTrace += str(unrollMax) + ".\n" heurTrace += "Reporting benchmark as 'verified'.\n" - if args.execute and not args.pthread: - heurTrace += "Hold on, let's see the execution result.\n" - execution_result = run_binary(args) - heurTrace += "Excecution result is " + execution_result + '\n' - if execution_result != 'true': - heurTrace += "Oops, execution result says {0}.\n".format(execution_result) - if not args.quiet: - print((heurTrace + "\n")) - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) - random_test_result = random_test(args, result) - if random_test_result == 'false' or random_test_result == 'unknown': - heurTrace += "Oops, random testing says {0}.\n".format(random_test_result) - if not args.quiet: - print((heurTrace + "\n")) - print(smack.top.results(args)['unknown'][0]) - sys.exit(smack.top.results(args)['unknown'][1]) if not args.quiet: print((heurTrace + "\n")) - if 'memory-safety' in args.check: - heurTrace += (args.prop_to_check + "is verified\n") - if args.prop_to_check == 'valid-deref': - args.valid_deref_check_result = 'verified' - elif args.prop_to_check == 'valid-free': - args.valid_free_check_result = 'verified' - elif args.prop_to_check == 'memleak': - if args.valid_deref_check_result == 'timeout': - force_timeout() - else: - print(smack.top.results(args)[args.valid_deref_check_result][0]) - sys.exit(smack.top.results(args)[args.valid_deref_check_result][1]) - verify_bpl_svcomp(args) - else: - write_error_file(args, 'verified', verifier_output) - print(smack.top.results(args)['verified'][0]) - sys.exit(smack.top.results(args)['verified'][1]) + write_error_file(args, VResult.VERIFIED, verifier_output) + print(VResult.VERIFIED.message(args)) + sys.exit(VResult.VERIFIED.return_code()) else: heurTrace += "Only unrolled " + str(unrollMax) + " times.\n" heurTrace += "Insufficient unrolls to consider 'verified'. " @@ -442,109 +159,34 @@ def verify_bpl_svcomp(args): if not args.quiet: print((heurTrace + "\n")) sys.stdout.flush() - if 'memory-safety' in args.check: - heurTrace += (args.prop_to_check + " times out\n") - if args.prop_to_check == 'valid-deref': - args.valid_deref_check_result = 'timeout' - force_timeout() - elif args.prop_to_check == 'valid-free': - args.valid_free_check_result = 'timeout' - elif args.prop_to_check == 'memleak': - if args.valid_deref_check_result == 'timeout': - force_timeout() - else: - print(smack.top.results(args)[args.valid_deref_check_result][0]) - sys.exit(smack.top.results(args)[args.valid_deref_check_result][1]) - verify_bpl_svcomp(args) - else: - force_timeout() - elif result == 'verified': #normal inlining + force_timeout() + elif result is VResult.VERIFIED: #normal inlining heurTrace += "Normal inlining terminated and found no bugs.\n" else: #normal inlining heurTrace += "Normal inlining returned 'unknown'. See errors above.\n" if not args.quiet: print((heurTrace + "\n")) - if 'memory-safety' in args.check and result == 'verified': - heurTrace += (args.prop_to_check + " is verified\n") - if args.prop_to_check == 'valid-deref': - args.valid_deref_check_result = 'verified' - elif args.prop_to_check == 'valid-free': - args.valid_free_check_result = 'verified' - elif args.prop_to_check == 'memleak': - if args.valid_deref_check_result == 'timeout': - force_timeout() - else: - print(smack.top.results(args)[args.valid_deref_check_result][0]) - sys.exit(smack.top.results(args)[args.valid_deref_check_result][1]) - verify_bpl_svcomp(args) - else: - write_error_file(args, result, verifier_output) - if 'memleak' in args.check and result == 'invalid-memtrack': - sys.exit('SMACK found an error: memory cleanup.') - else: - print(smack.top.results(args)[result][0]) - sys.exit(smack.top.results(args)[result][1]) + write_error_file(args, result, verifier_output) + print(result.message(args)) + sys.exit(result.return_code()) def write_error_file(args, status, verifier_output): + from smack.top import VProperty + from smack.top import VResult + from smack.errtrace import smackdOutput #return - if status == 'timeout' or status == 'unknown': + if status is VResult.UNKNOWN: return - hasBug = (status != 'verified') + hasBug = (status is not VResult.VERIFIED) #if not hasBug: # return if args.error_file: error = None if args.language == 'svcomp': - error = smackJsonToXmlGraph(smack.top.smackdOutput(verifier_output), args, hasBug, status) + error = smackJsonToXmlGraph(smackdOutput(status, verifier_output), args, hasBug, status) elif hasBug: error = smack.top.error_trace(verifier_output, args) if error is not None: with open(args.error_file, 'w') as f: f.write(error.decode('utf-8')) -def run_binary(args): - #process the file to make it runnable - with open(args.input_files[0], 'r') as fi: - s = fi.read() - - s = re.sub(r'(extern )?void reach_error()', '//', s) - s = re.sub(r'reach_error\(\)', 'assert(0)', s) - s = '#include\n' + s - - name = os.path.splitext(os.path.basename(args.input_files[0]))[0] - tmp1 = smack.top.temporary_file(name, '.c', args) - with open(tmp1, 'w') as fo: - fo.write(s) - - tmp2 = smack.top.temporary_file(name, '.bin', args) - tmp2 = tmp2.split('/')[-1] - #compile and run - cmd = ['clang', tmp1, '-o', tmp2] - #cmd += args.clang_options.split() - #if '-m32' in args.clang_options.split(): - #cmd += ['-m32'] - - - proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) - - out, err = proc.communicate() - rc = proc.returncode - - if rc: - print('Compiling error') - print(err) - return 'unknown' - else: - cmd = [r'./' + tmp2] - proc = subprocess.Popen(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE) - out, err = proc.communicate() - rc = proc.returncode - if rc: - if re.search(r'Assertion.*failed', err): - return 'false' - else: - print('Execution error') - print(err) - return 'unknown' - else: - return 'true' diff --git a/share/smack/top.py b/share/smack/top.py index 06343c8be..f1680db4a 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -1,37 +1,200 @@ import argparse -import json import os import re -import shutil import sys import shlex import subprocess import signal import functools +from enum import Flag, auto from .svcomp.utils import verify_bpl_svcomp from .utils import temporary_file, try_command, remove_temp_files from .replay import replay_error_trace from .frontend import link_bc_files, frontends, languages, extra_libs +from .errtrace import error_trace, smackdOutput + +VERSION = '2.6.1' + + +class VResult(Flag): + ''' + This class represents verification results. + `MEMSAFETY_ERROR` and `ERROR` do not correspond to any results. They are + used to group certain results. + ''' + + VERIFIED = auto() + ASSERTION_FAILURE = auto() + INVALID_DEREF = auto() + INVALID_FREE = auto() + INVALID_MEMTRACK = auto() + OVERFLOW = auto() + RUST_PANIC = auto() + TIMEOUT = auto() + UNKNOWN = auto() + MEMSAFETY_ERROR = INVALID_DEREF | INVALID_FREE | INVALID_MEMTRACK + ERROR = (ASSERTION_FAILURE | INVALID_DEREF | INVALID_FREE + | INVALID_MEMTRACK | OVERFLOW | RUST_PANIC) + + def __str__(self): + return self.name.lower().replace('_', '-') + + def description(self): + '''Return the description for certain result.''' + + descriptions = { + VResult.ASSERTION_FAILURE: '', + VResult.INVALID_DEREF: 'invalid pointer dereference', + VResult.INVALID_FREE: 'invalid memory deallocation', + VResult.INVALID_MEMTRACK: 'memory leak', + VResult.OVERFLOW: 'integer overflow', + VResult.RUST_PANIC: 'Rust panic'} + + if self in descriptions: + return descriptions[self] + else: + raise RuntimeError('No description associated with result: %s' + % self) + + def return_code(self): + '''Return the exit code for each result.''' + + return_codes = { + VResult.VERIFIED: 0, + VResult.ASSERTION_FAILURE: 1, + VResult.INVALID_DEREF: 2, + VResult.INVALID_FREE: 3, + VResult.INVALID_MEMTRACK: 4, + VResult.OVERFLOW: 5, + VResult.RUST_PANIC: 6, + VResult.TIMEOUT: 126, + VResult.UNKNOWN: 127} + + if self in return_codes: + return return_codes[self] + else: + raise RuntimeError('No return code associated with result: %s' + % self) + + def message(self, args): + '''Return SMACK's output for each result.''' + + if self is VResult.VERIFIED: + return ('SMACK found no errors' + + ('' if args.modular else ' with unroll bound %s' + % args.unroll) + '.') + elif self in VResult.ERROR: + description = self.description() + return ('SMACK found an error' + + (': %s' % description if description else '') + '.') + elif self is VResult.TIMEOUT: + return 'SMACK timed out.' + elif self is VResult.UNKNOWN: + return 'SMACK result is unknown.' + else: + raise RuntimeError('No message associated with result: %s' % self) + + +class PropertyAction(argparse.Action): + ''' + This class defines the argparse action when the arguments of the `--check` + option are consumed. + ''' -VERSION = '2.6.0' + def __init__(self, option_strings, dest, **kwargs): + super(PropertyAction, self).__init__(option_strings, dest, **kwargs) + def __call__(self, parser, namespace, values, option_string=None): + ''' + Fold the provided arguments with bitwise or. This is equivalent to + extending the property list with the arguments. + ''' + + setattr(namespace, self.dest, + functools.reduce(lambda x, y: x | y, values, + getattr(namespace, self.dest))) + + +# Shaobo: shamelessly borrowed it from https://stackoverflow.com/a/55500795 +class VProperty(Flag): + ''' + This class defines the properties that SMACK verifies. `NONE` is a special + value that does not correspond to any property. It's used simply to get + around the default value issue when the action similar to `extend`. + ''' + + NONE = 0 + ASSERTIONS = auto() + VALID_DEREF = auto() + VALID_FREE = auto() + MEMLEAK = auto() + MEMORY_SAFETY = VALID_DEREF | VALID_FREE | MEMLEAK + INTEGER_OVERFLOW = auto() + RUST_PANICS = auto() + + def __str__(self): + return self.name.lower().replace('_', '-') + + def __repr__(self): + return str(self) + + @staticmethod + def argparse(s): + try: + return VProperty[s.upper().replace('-', '_')] + except KeyError: + return s + + @staticmethod + def mem_safe_subprops(): + return [VProperty.VALID_DEREF, VProperty.VALID_FREE, VProperty.MEMLEAK] + + def contains_mem_safe_props(self): + ''' + Test if a property is either memory-safety or any of its subproperties. + ''' + + return bool(self & VProperty.MEMORY_SAFETY) + + def boogie_attr(self): + ''' + Return the attribute of Boogie assert command for certain property. + ''' + + def get_attr_from_result(x): + if x in VResult.MEMSAFETY_ERROR: + return x.name.lower()[2:] + else: + return x.name.lower() -def results(args): - """A dictionary of the result output messages.""" - return { - 'verified': ('SMACK found no errors' - + ('' if args.modular else - ' with unroll bound %s' % args.unroll) + '.', 0), - 'error': ('SMACK found an error.', 1), - 'invalid-deref': ('SMACK found an error: invalid pointer dereference.', - 2), - 'invalid-free': ('SMACK found an error: invalid memory deallocation.', - 3), - 'invalid-memtrack': ('SMACK found an error: memory leak.', 4), - 'overflow': ('SMACK found an error: integer overflow.', 5), - 'rust-panic': ('SMACK found an error: Rust panic.', 6), - 'timeout': ('SMACK timed out.', 126), - 'unknown': ('SMACK result is unknown.', 127)} + attrs = { + VProperty.VALID_DEREF: get_attr_from_result(VResult.INVALID_DEREF), + VProperty.VALID_FREE: get_attr_from_result(VResult.INVALID_FREE), + VProperty.MEMLEAK: get_attr_from_result(VResult.INVALID_MEMTRACK), + VProperty.INTEGER_OVERFLOW: get_attr_from_result(VResult.OVERFLOW), + VProperty.RUST_PANICS: get_attr_from_result(VResult.RUST_PANIC)} + + if self in attrs: + return attrs[self] + else: + raise RuntimeError('No assertion Boogie attribute associated with' + 'property: %s' % self) + + def result(self): + '''Link SMACK properties with results''' + + res = { + VProperty.VALID_DEREF: VResult.INVALID_DEREF, + VProperty.VALID_FREE: VResult.INVALID_FREE, + VProperty.MEMLEAK: VResult.INVALID_MEMTRACK, + VProperty.INTEGER_OVERFLOW: VResult.OVERFLOW, + VProperty.RUST_PANICS: VResult.RUST_PANIC} + + if self in res: + return res[self] + else: + raise RuntimeError(('No SMACK result associated with property: %s' + % self)) def inlined_procedures(): @@ -226,6 +389,13 @@ def arguments(): type=str, help='save (intermediate) Boogie code to FILE') + translate_group.add_argument( + '--rewrite-bitwise-ops', + action="store_true", + default=False, + help='''attempts to provide models for bitwise operations + when integer encoding is used''') + translate_group.add_argument( '--no-memory-splitting', action="store_true", @@ -303,11 +473,12 @@ def arguments(): '--check', metavar='PROPERTY', nargs='+', - choices=['assertions', 'memory-safety', 'valid-deref', 'valid-free', - 'memleak', 'integer-overflow', 'rust-panics'], - default=['assertions'], + choices=list(VProperty), + default=VProperty.NONE, + type=VProperty.argparse, + action=PropertyAction, help='''select properties to check - [choices: %(choices)s; default: %(default)s] + [choices: %(choices)s; default: assertions] (note that memory-safety is the union of valid-deref, valid-free, memleak)''') @@ -446,6 +617,9 @@ def arguments(): args.bpl_file = 'a.bpl' if args.no_verify else temporary_file( 'a', '.bpl', args) + if args.check == VProperty.NONE: + args.check = VProperty.ASSERTIONS + # TODO are we (still) using this? # with open(args.input_file, 'r') as f: # for line in f.readlines(): @@ -548,14 +722,15 @@ def llvm_to_bpl(args): cmd += ['-bit-precise-pointers'] if args.no_byte_access_inference: cmd += ['-no-byte-access-inference'] + if args.rewrite_bitwise_ops: + cmd += ['-rewrite-bitwise-ops'] if args.no_memory_splitting: cmd += ['-no-memory-splitting'] - if ('memory-safety' in args.check or 'valid-deref' in args.check or - 'valid-free' in args.check or 'memleak' in args.check): + if args.check.contains_mem_safe_props(): cmd += ['-memory-safety'] - if 'integer-overflow' in args.check: + if VProperty.INTEGER_OVERFLOW in args.check: cmd += ['-integer-overflow'] - if 'rust-panics' in args.check: + if VProperty.RUST_PANICS in args.check: cmd += ['-rust-panics'] if args.llvm_assumes: cmd += ['-llvm-assumes=' + args.llvm_assumes] @@ -600,15 +775,11 @@ def annotate_bpl(args): def memsafety_subproperty_selection(args): - selected_props = set() - if 'memory-safety' in args.check: + if VProperty.MEMORY_SAFETY in args.check: return - if 'valid-deref' in args.check: - selected_props.add('valid_deref') - if 'valid-free' in args.check: - selected_props.add('valid_free') - if 'memleak' in args.check: - selected_props.add('valid_memtrack') + + selected_props = [p.boogie_attr() for p in VProperty.mem_safe_subprops() + if p in args.check] def replace_assertion(m): if len(selected_props) > 0: @@ -663,36 +834,26 @@ def verification_result(verifier_output): if re.search( r'[1-9]\d* time out|Z3 ran out of resources|timed out|ERRORS_TIMEOUT', verifier_output): - return 'timeout' + return VResult.TIMEOUT elif re.search((r'[1-9]\d* verified, 0 errors?|no bugs|' r'NO_ERRORS_NO_TIMEOUT'), verifier_output): - return 'verified' + return VResult.VERIFIED elif re.search((r'\d* verified, [1-9]\d* errors?|can fail|' r'ERRORS_NO_TIMEOUT'), verifier_output): - if re.search( - r'ASSERTION FAILS assert {:valid_deref}', - verifier_output): - return 'invalid-deref' - elif re.search(r'ASSERTION FAILS assert {:valid_free}', - verifier_output): - return 'invalid-free' - elif re.search(r'ASSERTION FAILS assert {:valid_memtrack}', - verifier_output): - return 'invalid-memtrack' - elif re.search(r'ASSERTION FAILS assert {:overflow}', verifier_output): - return 'overflow' - elif re.search(r'ASSERTION FAILS assert {:rust_panic}', - verifier_output): - return 'rust-panic' + for p in (VProperty.mem_safe_subprops() + [VProperty.INTEGER_OVERFLOW] + + [VProperty.RUST_PANICS]): + if re.search(r'ASSERTION FAILS assert {:%s}' % p.boogie_attr(), + verifier_output): + return p.result() + + listCall = re.findall(r'\(CALL .+\)', verifier_output) + if len(listCall) > 0 and re.search( + r'free_', listCall[len(listCall) - 1]): + return VResult.INVALID_FREE else: - listCall = re.findall(r'\(CALL .+\)', verifier_output) - if len(listCall) > 0 and re.search( - r'free_', listCall[len(listCall) - 1]): - return 'invalid-free' - else: - return 'error' + return VResult.ASSERTION_FAILURE else: - return 'unknown' + return VResult.UNKNOWN def verify_bpl(args): @@ -711,6 +872,7 @@ def verify_bpl(args): command += ["/errorLimit:%s" % args.max_violations] command += ["/proverOpt:O:smt.array.extensional=false"] command += ["/proverOpt:O:smt.qi.eager_threshold=100"] + command += ["/proverOpt:O:smt.arith.solver=2"] if not args.modular: command += ["/loopUnroll:%d" % args.unroll] if args.solver == 'cvc4': @@ -729,6 +891,7 @@ def verify_bpl(args): command += ["/maxStaticLoopBound:%d" % args.loop_limit] command += ["/recursionBound:%d" % args.unroll] command += ["/bopt:proverOpt:O:smt.qi.eager_threshold=100"] + command += ["/bopt:proverOpt:O:smt.arith.solver=2"] if args.solver == 'cvc4': command += ["/bopt:proverOpt:SOLVER=cvc4"] elif args.solver == 'yices2': @@ -750,11 +913,9 @@ def verify_bpl(args): result = verification_result(verifier_output) if args.smackd: - print(smackdOutput(verifier_output)) + print(smackdOutput(result, verifier_output)) else: - if (result == 'error' or result == 'invalid-deref' or - result == 'invalid-free' or result == 'invalid-memtrack' or - result == 'overflow' or result == 'rust-panic'): + if result in VResult.ERROR: error = error_trace(verifier_output, args) if args.error_file: @@ -766,189 +927,8 @@ def verify_bpl(args): if args.replay: replay_error_trace(verifier_output, args) - print(results(args)[result][0]) - sys.exit(results(args)[result][1]) - - -def error_step(step): - FILENAME = r'[\w#$~%.\/-]*' - step = re.match(r"(\s*)(%s)\((\d+),\d+\): (.*)" % FILENAME, step) - if step: - if re.match('.*[.]bpl$', step.group(2)): - line_no = int(step.group(3)) - message = step.group(4) - if re.match(r'.*\$bb\d+.*', message): - message = "" - with open(step.group(2)) as f: - for line in f.read().splitlines(True)[line_no:line_no + 10]: - src = re.match( - r".*{:sourceloc \"(%s)\", (\d+), (\d+)}" % - FILENAME, line) - if src: - return "%s%s(%s,%s): %s" % (step.group(1), src.group( - 1), src.group(2), src.group(3), message) - else: - return corral_error_step(step.group(0)) - else: - return None - - -def reformat_assignment(line): - def repl(m): - val = m.group(1) - if 'bv' in val: - return m.group(2) + 'UL' - else: - sig_size = int(m.group(7)) - exp_size = int(m.group(8)) - # assume we can only handle double - if sig_size > 53 or exp_size > 11: - return m.group() - - sign_val = -1 if m.group(3) != '' else 1 - sig_val = m.group(4) - exp_sign_val = -1 if m.group(5) != '' else 1 - # note that the exponent base is 16 - exp_val = 2**(4 * exp_sign_val * int(m.group(6))) - return str(sign_val * float.fromhex(sig_val) * exp_val) - - # Boogie FP const grammar: (-)0x[sig]e[exp]f[sigSize]e[expSize], where - # sig = hexdigit {hexdigit} '.' hexdigit {hexdigit} - # exp = digit {digit} - # sigSize = digit {digit} - # expSize = digit {digit} - return re.sub( - (r'((\d+)bv\d+|(-?)0x([0-9a-fA-F]+\.[0-9a-fA-F]+)e(-?)' - r'(\d+)f(\d+)e(\d+))'), - repl, - line.strip()) - - -def demangle(func): - def demangle_with(func, tool): - if shutil.which(tool): - p = subprocess.Popen( - tool, - stdin=subprocess.PIPE, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE) - out, _ = p.communicate(input=func.encode()) - return out.decode() - return func - return functools.reduce(demangle_with, ['cxxfilt', 'rustfilt'], func) - - -def transform(info): - info = info.strip() - if info.startswith('CALL') or info.startswith('RETURN from'): - tokens = info.split() - tokens[-1] = demangle(tokens[-1]) - return ' '.join(tokens) - elif '=' in info: - tokens = info.split('=') - lhs = tokens[0].strip() - rhs = tokens[1].strip() - return demangle(lhs) + ' = ' + reformat_assignment(rhs) - else: - return info - - -def corral_error_step(step): - m = re.match(r'([^\s]*)\s+Trace:\s+(Thread=\d+)\s+\((.*)[\)|;]', step) - if m: - path = m.group(1) - tid = m.group(2) - info = ','.join(map(transform, - [x for x in m.group(3).split(',') if not - re.search( - (r'((CALL|RETURN from)\s+(\$|__SMACK))|' - r'Done|ASSERTION'), x)])) - return '{0}\t{1} {2}'.format(path, tid, info) - else: - return step - - -def error_trace(verifier_output, args): - trace = "" - for line in verifier_output.splitlines(True): - step = error_step(line) - if step: - m = re.match('(.*): [Ee]rror [A-Z0-9]+: (.*)', step) - if m: - trace += "%s: %s\nExecution trace:\n" % ( - m.group(1), m.group(2)) - else: - trace += ('' if step[0] == ' ' else ' ') + step + "\n" - - return trace - - -def smackdOutput(corralOutput): - FILENAME = r'[\w#$~%.\/-]+' - traceP = re.compile( - ('(' - + FILENAME - + r')\((\d+),(\d+)\): Trace: Thread=(\d+)(\((.*)[\);])?$')) - errorP = re.compile('(' + FILENAME + r')\((\d+),(\d+)\): (error .*)$') - - passedMatch = re.search('Program has no bugs', corralOutput) - if passedMatch: - json_data = { - 'verifier': 'corral', - 'passed?': True - } - - else: - traces = [] - filename = '' - lineno = 0 - colno = 0 - threadid = 0 - desc = '' - for traceLine in corralOutput.splitlines(True): - traceMatch = traceP.match(traceLine) - if traceMatch: - filename = str(traceMatch.group(1)) - lineno = int(traceMatch.group(2)) - colno = int(traceMatch.group(3)) - threadid = int(traceMatch.group(4)) - desc = str(traceMatch.group(6)) - for e in desc.split(','): - e = e.strip() - assm = re.sub( - r'=(\s*\d+)bv\d+', - r'=\1', - e) if '=' in e else '' - trace = {'threadid': threadid, - 'file': filename, - 'line': lineno, - 'column': colno, - 'description': e, - 'assumption': assm} - traces.append(trace) - else: - errorMatch = errorP.match(traceLine) - if errorMatch: - filename = str(errorMatch.group(1)) - lineno = int(errorMatch.group(2)) - colno = int(errorMatch.group(3)) - desc = str(errorMatch.group(4)) - - failsAt = { - 'file': filename, - 'line': lineno, - 'column': colno, - 'description': desc} - - json_data = { - 'verifier': 'corral', - 'passed?': False, - 'failsAt': failsAt, - 'threadCount': 1, - 'traces': traces - } - json_string = json.dumps(json_data) - return json_string + print(result.message(args)) + sys.exit(result.return_code()) def clean_up_upon_sigterm(main): diff --git a/share/smack/utils.py b/share/smack/utils.py index 2ba8e7978..fb16db72c 100644 --- a/share/smack/utils.py +++ b/share/smack/utils.py @@ -1,5 +1,6 @@ import os import sys +import shutil import tempfile import subprocess import signal @@ -17,10 +18,19 @@ def temporary_file(prefix, extension, args): return name +def temporary_directory(prefix, extension, args): + name = tempfile.mkdtemp(extension, prefix + '-', os.getcwd()) + if not args.debug: + temporary_files.append(name) + return name + + def remove_temp_files(): for f in temporary_files: if os.path.isfile(f): os.unlink(f) + elif os.path.isdir(f): + shutil.rmtree(f) def timeout_killer(proc, timed_out): @@ -29,13 +39,16 @@ def timeout_killer(proc, timed_out): os.killpg(os.getpgid(proc.pid), signal.SIGKILL) -def try_command(cmd, cwd=None, console=False, timeout=None): +def try_command(cmd, cwd=None, console=False, timeout=None, env=None): args = top.args console = (console or args.verbose or args.debug) and not args.quiet filelog = args.debug output = '' proc = None timer = None + if env is not None: + for k, v in env.items(): + os.putenv(k, v) try: if args.debug: print("Running %s" % " ".join(cmd)) diff --git a/test/c/failing/bitwise_and.c b/test/c/failing/bitwise_and.c new file mode 100644 index 000000000..b7591ae79 --- /dev/null +++ b/test/c/failing/bitwise_and.c @@ -0,0 +1,44 @@ +#include "smack.h" + +// @expect verified + +int main(void) { + unsigned char x = (unsigned char)__VERIFIER_nondet_unsigned_char(); + { // y = 0 + assert((x & 0) == (x % (0 + 1))); + assert((0 & x) == (x % (0 + 1))); + } + { // y = 1 + assert((x & 1) == (x % (1 + 1))); + assert((1 & x) == (x % (1 + 1))); + } + { // y = 3 + assert((x & 3) == (x % (3 + 1))); + assert((3 & x) == (x % (3 + 1))); + } + { // y = 7 + assert((x & 7) == (x % (7 + 1))); + assert((7 & x) == (x % (7 + 1))); + } + { // y = 15 + assert((x & 15) == (x % (15 + 1))); + assert((15 & x) == (x % (15 + 1))); + } + { // y = 31 + assert((x & 31) == (x % (31 + 1))); + assert((31 & x) == (x % (31 + 1))); + } + { // y = 63 + assert((x & 63) == (x % (63 + 1))); + assert((63 & x) == (x % (63 + 1))); + } + { // y = 127 + assert((x & 127) == (x % (127 + 1))); + assert((127 & x) == (x % (127 + 1))); + } + { // y = 255 + assert((x & 255) == x); + assert((255 & x) == x); + } + return 0; +} diff --git a/test/c/failing/bitwise_and_fail.c b/test/c/failing/bitwise_and_fail.c new file mode 100644 index 000000000..e42e4e31f --- /dev/null +++ b/test/c/failing/bitwise_and_fail.c @@ -0,0 +1,46 @@ +#include "smack.h" + +// @expect error + +int main(void) { + unsigned char x = (unsigned char)__VERIFIER_nondet_unsigned_char(); + int cond = 0; + { // y = 0 + cond = cond || ((x & 0) != (x % (0 + 1))); + cond = cond || ((0 & x) != (x % (0 + 1))); + } + { // y = 1 + cond = cond || ((x & 1) != (x % (1 + 1))); + cond = cond || ((1 & x) != (x % (1 + 1))); + } + { // y = 3 + cond = cond || ((x & 3) != (x % (3 + 1))); + cond = cond || ((3 & x) != (x % (3 + 1))); + } + { // y = 7 + cond = cond || ((x & 7) != (x % (7 + 1))); + cond = cond || ((7 & x) != (x % (7 + 1))); + } + { // y = 15 + cond = cond || ((x & 15) != (x % (15 + 1))); + cond = cond || ((15 & x) != (x % (15 + 1))); + } + { // y = 31 + cond = cond || ((x & 31) != (x % (31 + 1))); + cond = cond || ((31 & x) != (x % (31 + 1))); + } + { // y = 63 + cond = cond || ((x & 63) != (x % (63 + 1))); + cond = cond || ((63 & x) != (x % (63 + 1))); + } + { // y = 127 + cond = cond || ((x & 127) != (x % (127 + 1))); + cond = cond || ((127 & x) != (x % (127 + 1))); + } + { // y = 255 + cond = cond || ((x & 255) != x); + cond = cond || ((255 & x) != x); + } + assert(cond); + return 0; +} diff --git a/test/c/memory-safety/malloc_nondet.c b/test/c/memory-safety/malloc_nondet.c index fd29f42e6..9741ab826 100644 --- a/test/c/memory-safety/malloc_nondet.c +++ b/test/c/memory-safety/malloc_nondet.c @@ -5,10 +5,9 @@ int main(void) { int x = __VERIFIER_nondet_int(); + assume(x != 0); // malloc(0) can return anything char *p = (char *)malloc(x); - if (p != NULL) { - p[x - 1] = x; - free(p); - } + p[x - 1] = x; + free(p); return 0; } diff --git a/test/c/memory-safety/malloc_nondet_fail.c b/test/c/memory-safety/malloc_nondet_fail.c index 24fb37f76..52214619c 100644 --- a/test/c/memory-safety/malloc_nondet_fail.c +++ b/test/c/memory-safety/malloc_nondet_fail.c @@ -5,10 +5,9 @@ int main(void) { int x = __VERIFIER_nondet_int(); + assume(x != 0); // malloc(0) can return anything char *p = (char *)malloc(x); - if (p != NULL) { - p[x] = x; - free(p); - } + p[x] = x; + free(p); return 0; } diff --git a/test/c/pthread_extras/dekker_true-unreach-call.c b/test/c/pthread_extras/dekker_true-unreach-call.c index b26f12292..b98d24c3a 100644 --- a/test/c/pthread_extras/dekker_true-unreach-call.c +++ b/test/c/pthread_extras/dekker_true-unreach-call.c @@ -50,7 +50,7 @@ void *thr2(void *arg) { int main() { pthread_t t1, t2; - __VERIFIER_assume(0 <= turn && turn <= 1); + assume(0 <= turn && turn <= 1); pthread_create(&t1, 0, thr1, 0); pthread_create(&t2, 0, thr2, 0); pthread_join(t1, 0); diff --git a/test/c/pthread_extras/sigma_false-unreach-call.c b/test/c/pthread_extras/sigma_false-unreach-call.c index de1a09643..c7a692723 100644 --- a/test/c/pthread_extras/sigma_false-unreach-call.c +++ b/test/c/pthread_extras/sigma_false-unreach-call.c @@ -23,8 +23,8 @@ int main() { t = (pthread_t *)malloc(sizeof(pthread_t) * SIGMA); array = (int *)malloc(sizeof(int) * SIGMA); - //__VERIFIER_assume(t); - //__VERIFIER_assume(array); + // assume(t); + // assume(array); for (tid = 0; tid < SIGMA; tid++) { pthread_create(&t[tid], 0, thread, 0); diff --git a/test/c/pthread_extras/sigma_false_GREAT-unreach-call.c b/test/c/pthread_extras/sigma_false_GREAT-unreach-call.c index e4e4bcb8d..1ec417155 100644 --- a/test/c/pthread_extras/sigma_false_GREAT-unreach-call.c +++ b/test/c/pthread_extras/sigma_false_GREAT-unreach-call.c @@ -36,8 +36,8 @@ int main() { t = (pthread_t *)malloc(sizeof(pthread_t) * SIGMA); array = (int *)malloc(sizeof(int) * SIGMA); - //__VERIFIER_assume(t); - //__VERIFIER_assume(array); + // assume(t); + // assume(array); for (tid = 0; tid < SIGMA; tid++) { pthread_mutex_lock(&lock); diff --git a/test/c/pthread_extras/sssc12_true-unreach-call.c b/test/c/pthread_extras/sssc12_true-unreach-call.c index 994a64fd3..26cae599a 100644 --- a/test/c/pthread_extras/sssc12_true-unreach-call.c +++ b/test/c/pthread_extras/sssc12_true-unreach-call.c @@ -34,7 +34,7 @@ void main() { pthread_t t; next = 0; len = __VERIFIER_nondet_int(); - __VERIFIER_assume(len > 0); + assume(len > 0); data = malloc(sizeof(int) * len); while (1) { pthread_create(&t, 0, thr, 0); diff --git a/test/c/pthread_extras/time_var_mutex_true-unreach-call.c b/test/c/pthread_extras/time_var_mutex_true-unreach-call.c index 2e6237be5..4d94cd18e 100644 --- a/test/c/pthread_extras/time_var_mutex_true-unreach-call.c +++ b/test/c/pthread_extras/time_var_mutex_true-unreach-call.c @@ -44,7 +44,7 @@ void *de_allocator(void *arg) { int main() { pthread_t t1, t2; - __VERIFIER_assume(inode == busy); + assume(inode == busy); pthread_mutex_init(&m_inode, 0); pthread_mutex_init(&m_busy, 0); pthread_create(&t1, 0, allocator, 0); diff --git a/test/c/special/assume.c b/test/c/special/assume.c index eee18cc4d..530ff3cea 100644 --- a/test/c/special/assume.c +++ b/test/c/special/assume.c @@ -4,9 +4,11 @@ // @flag --llvm-assumes=use int main(void) { - unsigned int y = 2 * (unsigned int)__VERIFIER_nondet_unsigned_short(); + unsigned int x = __VERIFIER_nondet_unsigned_int(); + unsigned int y = __VERIFIER_nondet_unsigned_int(); // This assumption is used for verification, even though // integer-encoding=bit-vector is not enabled, the assertion will pass. - __builtin_assume((y & 1) == 0); - assert((y & 1) == 0); + __builtin_assume((x ^ y) == (y ^ x)); + assert((x ^ y) == (y ^ x)); + return 0; } diff --git a/test/c/special/assume2.c b/test/c/special/assume2.c index 03b70c663..4148c3f8a 100644 --- a/test/c/special/assume2.c +++ b/test/c/special/assume2.c @@ -4,9 +4,10 @@ // @flag --llvm-assumes=use int main(void) { - unsigned int y = (2 * (unsigned int)__VERIFIER_nondet_unsigned_short()) + 1; + unsigned int x = __VERIFIER_nondet_unsigned_int(); // This assumption is used for verification, even though the assumption // is false, the assertion will pass. - __builtin_assume((y & 1) == 0); - assert((y & 1) == 0); + __builtin_assume((x ^ x) == 1); + assert((x ^ x) == 1); + return 0; } diff --git a/test/c/special/assume_check.c b/test/c/special/assume_check.c index d1c2a37f8..709cc7b28 100644 --- a/test/c/special/assume_check.c +++ b/test/c/special/assume_check.c @@ -5,9 +5,11 @@ // @flag --integer-encoding=bit-vector int main(void) { - unsigned int y = 2 * (unsigned int)__VERIFIER_nondet_unsigned_short(); + unsigned int x = __VERIFIER_nondet_unsigned_int(); + unsigned int y = __VERIFIER_nondet_unsigned_int(); // This assumption is checked under integer-encoding=bit-vector and is // verified. - __builtin_assume((y & 1) == 0); - assert((y & 1) == 0); + __builtin_assume((x ^ y) == (y ^ x)); + assert((x ^ y) == (y ^ x)); + return 0; } diff --git a/test/c/special/assume_check2.c b/test/c/special/assume_check2.c index 9a98a02c6..431e30bdc 100644 --- a/test/c/special/assume_check2.c +++ b/test/c/special/assume_check2.c @@ -5,10 +5,10 @@ // @flag --integer-encoding=bit-vector int main(void) { - unsigned int y = (2 * (unsigned int)__VERIFIER_nondet_unsigned_short()) + 1; + unsigned int x = __VERIFIER_nondet_unsigned_int(); // This assumption is checked at verification time, and since - // integer-encoding=bit-vector is enabled, and y is clearly odd, the check - // will pass. - __builtin_assume((y & 1) == 1); - assert((y & 1) == 1); + // integer-encoding=bit-vector is enabled, the check will pass. + __builtin_assume((x ^ x) == 0); + assert((x ^ x) == 0); + return 0; } diff --git a/test/c/special/assume_check_fail.c b/test/c/special/assume_check_fail.c index f84470d22..a7fa947a3 100644 --- a/test/c/special/assume_check_fail.c +++ b/test/c/special/assume_check_fail.c @@ -5,10 +5,12 @@ // @flag --integer-encoding=bit-vector int main(void) { - unsigned int y = (2 * (unsigned int)__VERIFIER_nondet_unsigned_short()) + 1; + unsigned int x = __VERIFIER_nondet_unsigned_int(); + unsigned int y = __VERIFIER_nondet_unsigned_int(); // This assumption is checked at verification time, and since - // integer-encoding=bit-vector is enabled, and y is clearly odd, the - // assumption should be shown false. - __builtin_assume((y & 1) == 0); - assert((y & 1) == 0); + // integer-encoding=bit-vector is enabled, the assumption should + // be shown false. + __builtin_assume((x ^ y) != (y ^ x)); + assert((x ^ y) != (y ^ x)); + return 0; } diff --git a/test/c/special/assume_fail.c b/test/c/special/assume_fail.c index 8ab1c4e1b..5c3744665 100644 --- a/test/c/special/assume_fail.c +++ b/test/c/special/assume_fail.c @@ -4,9 +4,11 @@ // @flag --llvm-assumes=none int main(void) { - unsigned int y = 2 * (unsigned int)__VERIFIER_nondet_unsigned_short(); + unsigned int x = __VERIFIER_nondet_unsigned_int(); + unsigned int y = __VERIFIER_nondet_unsigned_int(); // This assumption is not used, and since integer-encoding=bit-vector is // not enabled, verification will fail. - __builtin_assume((y & 1) == 0); - assert((y & 1) == 0); + __builtin_assume((x ^ y) == (y ^ x)); + assert((x ^ y) == (y ^ x)); + return 0; } diff --git a/test/c/special/bitwise_constant_shifts.c b/test/c/special/bitwise_constant_shifts.c new file mode 100644 index 000000000..8b1e9433a --- /dev/null +++ b/test/c/special/bitwise_constant_shifts.c @@ -0,0 +1,42 @@ +#include "smack.h" + +// @expect verified +// @flag --rewrite-bitwise-ops + +int main(void) { + unsigned char x = __VERIFIER_nondet_unsigned_char(); + { // y = 0 + assert((x >> 0) == (x / 1)); + assert((x << 0) == (x * 1)); + } + { // y = 1 + assert((x >> 1) == (x / 2)); + assert((x << 1) == (x * 2)); + } + { // y = 3 + assert((x >> 3) == (x / 8)); + assert((x << 3) == (x * 8)); + } + { // y = 4 + assert((x >> 4) == (x / 16)); + assert((x << 4) == (x * 16)); + } + { // y = 5 + assert((x >> 5) == (x / 32)); + assert((x << 5) == (x * 32)); + } + { // y = 6 + assert((x >> 6) == (x / 64)); + assert((x << 6) == (x * 64)); + } + { // y = 7 + assert((x >> 7) == (x / 128)); + assert((x << 7) == (x * 128)); + } + { // y = 8 + assert((x >> 8) == 0); + // This may not be possible to handle correctly. + assert((x << 8) == x * 128 + x * 128); + } + return 0; +} diff --git a/test/c/special/bitwise_constant_shifts_fail.c b/test/c/special/bitwise_constant_shifts_fail.c new file mode 100644 index 000000000..ed11f16de --- /dev/null +++ b/test/c/special/bitwise_constant_shifts_fail.c @@ -0,0 +1,44 @@ +#include "smack.h" + +// @expect error +// @flag --rewrite-bitwise-ops + +int main(void) { + unsigned char x = __VERIFIER_nondet_unsigned_char(); + int cond = 0; + { // y = 0 + cond = cond || ((x >> 0) != (x / 1)); + cond = cond || ((x << 0) != (x * 1)); + } + { // y = 1 + cond = cond || ((x >> 1) != (x / 2)); + cond = cond || ((x << 1) != (x * 2)); + } + { // y = 3 + cond = cond || ((x >> 3) != (x / 8)); + cond = cond || ((x << 3) != (x * 8)); + } + { // y = 4 + cond = cond || ((x >> 4) != (x / 16)); + cond = cond || ((x << 4) != (x * 16)); + } + { // y = 5 + cond = cond || ((x >> 5) != (x / 32)); + cond = cond || ((x << 5) != (x * 32)); + } + { // y = 6 + cond = cond || ((x >> 6) != (x / 64)); + cond = cond || ((x << 6) != (x * 64)); + } + { // y = 7 + cond = cond || ((x >> 7) != (x / 128)); + cond = cond || ((x << 7) != (x * 128)); + } + { // y = 8 + cond = cond || ((x >> 8) != 0); + // This may not be possible to handle correctly. + cond = cond || ((x << 8) != x * 128 + x * 128); + } + assert(cond); + return 0; +} diff --git a/test/c/special/countpop8.c b/test/c/special/countpop8.c new file mode 100644 index 000000000..5ba59a24a --- /dev/null +++ b/test/c/special/countpop8.c @@ -0,0 +1,27 @@ +#include "smack.h" +#include + +// @flag --rewrite-bitwise-ops +// @expect verified + +uint8_t results[256] = { + 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3, 3, 4, + 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2, 2, 3, 2, 3, 3, 4, + 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, + 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, + 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, + 4, 5, 5, 6, 5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, + 4, 5, 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8}; + +uint8_t ctpop8(uint8_t x) { return results[x]; } + +int main(void) { + uint8_t x = __VERIFIER_nondet_unsigned_char(); + assume(x > 251 && x <= 255); + assert(__builtin_popcount(x) == ctpop8(x)); + return 0; +} diff --git a/test/c/special/countpop8_fail.c b/test/c/special/countpop8_fail.c new file mode 100644 index 000000000..1868415d3 --- /dev/null +++ b/test/c/special/countpop8_fail.c @@ -0,0 +1,27 @@ +#include "smack.h" +#include + +// @flag --rewrite-bitwise-ops +// @expect error + +uint8_t results[256] = { + 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3, 3, 4, + 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2, 2, 3, 2, 3, 3, 4, + 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, + 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, + 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, + 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, + 4, 5, 5, 6, 5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, + 4, 5, 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8}; + +uint8_t ctpop8(uint8_t x) { return results[x]; } + +int main(void) { + uint8_t x = __VERIFIER_nondet_unsigned_char(); + assume(x > 251 && x <= 255); + assert(__builtin_popcount(x) != ctpop8(x)); + return 0; +} diff --git a/test/c/strings/test_memcmp.c b/test/c/strings/test_memcmp.c new file mode 100644 index 000000000..f548437f7 --- /dev/null +++ b/test/c/strings/test_memcmp.c @@ -0,0 +1,20 @@ +#include "smack.h" +#include + +// @expect verified + +int main(void) { + char word1[] = "Test memcmp"; + char word2[] = "Test memcmp"; + char word3[] = "Test memcpy"; + int result; + + result = memcmp(word1, word2, 11); + assert(result == 0); + result = memcmp(word1, word3, 11); + assert(result < 0); + result = memcmp(word1, word3, 8); + assert(result == 0); + + return 0; +} diff --git a/test/c/strings/test_memcmp_fail.c b/test/c/strings/test_memcmp_fail.c new file mode 100644 index 000000000..ed65f13ef --- /dev/null +++ b/test/c/strings/test_memcmp_fail.c @@ -0,0 +1,17 @@ +#include "smack.h" +#include + +// @expect error + +int main(void) { + char word1[] = "Test memcmp"; + char word2[] = "Test memcpy"; + char word3[] = "Test memcmp"; + int result1, result2; + + result1 = memcmp(word1, word2, 11); + result2 = memcmp(word1, word3, 11); + assert(result1 >= 0 || result2 != 0); + + return 0; +} diff --git a/test/rust/cargo/cargo-test/Cargo.toml b/test/rust/cargo/cargo-test/Cargo.toml new file mode 100644 index 000000000..9e5aa6ccf --- /dev/null +++ b/test/rust/cargo/cargo-test/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "cargo-test" +version = "0.1.0" +authors = ["smackers"] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +num-traits = "0.2.12" +smack = { path = "/usr/local/share/smack/lib" } diff --git a/test/rust/cargo/cargo-test/src/main.rs b/test/rust/cargo/cargo-test/src/main.rs new file mode 100644 index 000000000..57adf0d55 --- /dev/null +++ b/test/rust/cargo/cargo-test/src/main.rs @@ -0,0 +1,13 @@ +extern crate num_traits; +#[macro_use] +extern crate smack; +use smack::*; + +fn main() { + let a: u32 = 5.verifier_nondet(); + let b: u32 = 3.verifier_nondet(); + let c: u32 = 8.verifier_nondet(); + verifier_assume!(a <= c); + let d = num_traits::clamp(b, a, c); + verifier_assert!(a <= d && d <= c); +} diff --git a/test/rust/basic/arith.rs b/test/rust/failing/arith.rs similarity index 100% rename from test/rust/basic/arith.rs rename to test/rust/failing/arith.rs diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 61427c5c9..a0ec23d28 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -33,8 +33,11 @@ #include "smack/InitializePasses.h" #include "smack/IntegerOverflowChecker.h" #include "smack/MemorySafetyChecker.h" +#include "smack/Naming.h" #include "smack/NormalizeLoops.h" #include "smack/RemoveDeadDefs.h" +#include "smack/RewriteBitwiseOps.h" +#include "smack/RustFixes.h" #include "smack/SimplifyLibCalls.h" #include "smack/SmackModuleGenerator.h" #include "smack/SmackOptions.h" @@ -154,6 +157,24 @@ int main(int argc, char **argv) { llvm::legacy::PassManager pass_manager; + // This runs before DSA because some Rust functions cause problems. + pass_manager.add(new smack::RustFixes); + + if (!Modular) { + auto PreserveKeyGlobals = [=](const llvm::GlobalValue &GV) { + std::string name = GV.getName(); + return smack::SmackOptions::isEntryPoint(name) || + smack::Naming::isSmackName(name) || + name.find("__VERIFIER_assume") != std::string::npos; + }; + pass_manager.add(llvm::createInternalizePass(PreserveKeyGlobals)); + pass_manager.add(llvm::createGlobalDCEPass()); + pass_manager.add(llvm::createDeadCodeEliminationPass()); + pass_manager.add(llvm::createGlobalDCEPass()); + pass_manager.add(llvm::createDeadCodeEliminationPass()); + pass_manager.add(new smack::RemoveDeadDefs()); + } + pass_manager.add(seadsa::createRemovePtrToIntPass()); pass_manager.add(llvm::createLowerSwitchPass()); // pass_manager.add(llvm::createCFGSimplificationPass()); @@ -190,6 +211,12 @@ int main(int argc, char **argv) { pass_manager.add(new smack::IntegerOverflowChecker()); + if (smack::SmackOptions::RewriteBitwiseOps && + !(smack::SmackOptions::BitPrecise || + smack::SmackOptions::BitPrecisePointers)) { + pass_manager.add(new smack::RewriteBitwiseOps()); + } + if (smack::SmackOptions::AddTiming) { Triple ModuleTriple(module->getTargetTriple()); assert(