diff --git a/.github/workflows/smack-ci.yaml b/.github/workflows/smack-ci.yaml new file mode 100644 index 000000000..aa4386ccc --- /dev/null +++ b/.github/workflows/smack-ci.yaml @@ -0,0 +1,66 @@ +name: SMACK CI + +on: [push, pull_request] + +jobs: + check-regressions: + env: + COMPILER_NAME: clang + COMPILER: clang++ + CXX: clang++ + CC: clang + runs-on: ubuntu-20.04 + strategy: + matrix: + travis_env: + [ + "--exhaustive --folder=c/basic", + "--exhaustive --folder=c/data", + "--exhaustive --folder=c/ntdrivers-simplified", + "--exhaustive --folder=c/ntdrivers", + "--exhaustive --folder=c/bits", + "--exhaustive --folder=c/float", + "--exhaustive --folder=c/locks", + "--exhaustive --folder=c/contracts", + "--exhaustive --folder=c/simd", + "--exhaustive --folder=c/memory-safety", + "--exhaustive --folder=c/pthread", + "--exhaustive --folder=c/pthread_extras", + "--exhaustive --folder=c/strings", + "--exhaustive --folder=c/special", + "--exhaustive --folder=rust/array --languages=rust", + "--exhaustive --folder=rust/basic --languages=rust", + "--exhaustive --folder=rust/box --languages=rust", + "--exhaustive --folder=rust/functions --languages=rust", + "--exhaustive --folder=rust/generics --languages=rust", + "--exhaustive --folder=rust/loops --languages=rust", + "--exhaustive --folder=rust/panic --languages=rust", + "--exhaustive --folder=rust/recursion --languages=rust", + "--exhaustive --folder=rust/structures --languages=rust", + "--exhaustive --folder=rust/vector --languages=rust" + ] + steps: + - uses: actions/checkout@v2 + + - name: install dependencies + env: + GITHUB_ACTIONS: true + run: INSTALL_DEV_DEPENDENCIES=1 INSTALL_RUST=1 ./bin/build.sh + + - run: python3 --version + - run: $CXX --version + - run: $CC --version + - run: clang --version + - run: clang++ --version + - run: llvm-link --version + - run: llvm-config --version + + - name: format checking + run: | + ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples + flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py + + - name: compile and test + env: + TRAVIS_ENV: ${{ matrix.travis_env }} + run: ./bin/build.sh diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 3dd689375..000000000 --- a/.travis.yml +++ /dev/null @@ -1,78 +0,0 @@ -language: generic -os: linux -dist: focal - -addons: - apt: - packages: - - git - - cmake - - python3-yaml - - python3-psutil - - python3-pip - - unzip - - ninja-build - - libboost-all-dev - -env: - global: - - COMPILER_NAME=clang COMPILER=clang++ CXX=clang++ CC=clang - jobs: - - TRAVIS_ENV="--exhaustive --folder=c/basic" - - TRAVIS_ENV="--exhaustive --folder=c/data" - - TRAVIS_ENV="--exhaustive --folder=c/ntdrivers-simplified" - - TRAVIS_ENV="--exhaustive --folder=c/ntdrivers" - - TRAVIS_ENV="--exhaustive --folder=c/bits" - - TRAVIS_ENV="--exhaustive --folder=c/float" - - TRAVIS_ENV="--exhaustive --folder=c/locks" - - TRAVIS_ENV="--exhaustive --folder=c/contracts" - - TRAVIS_ENV="--exhaustive --folder=c/simd" - - TRAVIS_ENV="--exhaustive --folder=c/memory-safety" - - TRAVIS_ENV="--exhaustive --folder=c/pthread" - - TRAVIS_ENV="--exhaustive --folder=c/pthread_extras" - - TRAVIS_ENV="--exhaustive --folder=c/strings" - - TRAVIS_ENV="--exhaustive --folder=c/special" - - TRAVIS_ENV="--exhaustive --folder=rust/array --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/basic --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/box --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/functions --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/generics --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/loops --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/panic --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/recursion --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/structures --languages=rust" - - TRAVIS_ENV="--exhaustive --folder=rust/vector --languages=rust" - -before_install: - - sudo rm -rf /usr/local/clang-7.0.0 - -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/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 - - sudo apt-get install -y clang-${LLVM_SHORT_VERSION} clang-format-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev dotnet-sdk-3.1 - - pip3 install -U flake8 - - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 20 - - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 20 - - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 20 - - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 20 - - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 20 - - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 20 - -before_script: - - python3 --version - - $CXX --version - - $CC --version - - clang --version - - clang++ --version - - llvm-link --version - - llvm-config --version - -script: - - ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples - - flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py - - INSTALL_RUST=1 ./bin/build.sh diff --git a/CMakeLists.txt b/CMakeLists.txt index 90c1d6b9c..b6959b051 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -7,7 +7,7 @@ project(smack) if (NOT WIN32 OR MSYS OR CYGWIN) - file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=[0-9]+") + file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=\"[0-9]+\"") string(REGEX MATCH "[0-9]+" LLVM_SHORT_VERSION "${LLVM_VERSION_STR}") find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION} llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") diff --git a/Doxyfile b/Doxyfile index 49ea31bce..1dac17777 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 2.6.2 +PROJECT_NUMBER = 2.6.3 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/README.md b/README.md index 03728e081..c455600c2 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,5 @@ - -[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=master)](https://travis-ci.com/smackers/smack) -[![Build Status](https://travis-ci.com/smackers/smack.svg?branch=develop)](https://travis-ci.com/smackers/smack) +[![master branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=master)](https://github.com/smackers/smack/actions) +[![develop branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=develop)](https://github.com/smackers/smack/actions) SMACK Logo diff --git a/bin/build.sh b/bin/build.sh index 6995aabd5..1094560b4 100755 --- a/bin/build.sh +++ b/bin/build.sh @@ -39,6 +39,9 @@ BUILD_LLVM=0 # LLVM is typically installed from packages (see below) INSTALL_OBJECTIVEC=0 INSTALL_RUST=${INSTALL_RUST:-0} +# Development dependencies +INSTALL_DEV_DEPENDENCIES=${INSTALL_DEV_DEPENDENCIES:-0} + # PATHS SMACK_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && cd .. && pwd )" ROOT_DIR="$( cd "${SMACK_DIR}" && cd .. && pwd )" @@ -459,6 +462,16 @@ if [ ${BUILD_LOCKPWN} -eq 1 ] ; then fi +if [ ${INSTALL_DEV_DEPENDENCIES} -eq 1 ] ; then + sudo apt-get install -y python3-pip clang-format-${LLVM_SHORT_VERSION} + sudo pip3 install -U flake8 + sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 30 + if [ "${GITHUB_ACTIONS}" = "true" ] ; then + exit 0 + fi +fi + + if [ ${BUILD_SMACK} -eq 1 ] ; then puts "Building SMACK" diff --git a/docs/people.md b/docs/people.md index ebaf02682..4be84414b 100644 --- a/docs/people.md +++ b/docs/people.md @@ -11,7 +11,7 @@ * [Marek Baranowski](https://github.com/keram88) ([SOAR Lab](http://soarlab.org), University of Utah) * [Jack J. Garzella](https://www.linkedin.com/in/jack-j-garzella-7140a716) ([SOAR Lab](http://soarlab.org), University of Utah) -* [Shaobo He](http://www.cs.utah.edu/~shaobo) ([SOAR Lab](http://soarlab.org), University of Utah) +* [Shaobo He](http://www.cs.utah.edu/~shaobo) (Baidu USA) * [Liam Machado](https://github.com/liammachado) ([SOAR Lab](http://soarlab.org), University of Utah) ### Former Contributors diff --git a/include/smack/MemorySafetyChecker.h b/include/smack/MemorySafetyChecker.h index dd1a64d41..e0f042a41 100644 --- a/include/smack/MemorySafetyChecker.h +++ b/include/smack/MemorySafetyChecker.h @@ -17,6 +17,7 @@ class MemorySafetyChecker : public llvm::FunctionPass, llvm::Function *getLeakCheckFunction(llvm::Module &M); llvm::Function *getSafetyCheckFunction(llvm::Module &M); + void copyDbgMetadata(llvm::Instruction *src, llvm::Instruction *dst); void insertMemoryLeakCheck(llvm::Instruction *I); void insertMemoryAccessCheck(llvm::Value *addr, llvm::Value *size, llvm::Instruction *I); diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index f5c137830..47c963ca3 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -91,6 +91,7 @@ class SmackInstGenerator : public llvm::InstVisitor { void visitPHINode(llvm::PHINode &i); void visitSelectInst(llvm::SelectInst &i); void visitCallInst(llvm::CallInst &i); + void visitCallBrInst(llvm::CallBrInst &i); void visitDbgValueInst(llvm::DbgValueInst &i); // TODO implement va_arg void visitLandingPadInst(llvm::LandingPadInst &i); diff --git a/lib/smack/BoogieAst.cpp b/lib/smack/BoogieAst.cpp index bc5a68fee..15781ac6f 100644 --- a/lib/smack/BoogieAst.cpp +++ b/lib/smack/BoogieAst.cpp @@ -555,7 +555,7 @@ void CallStmt::print(std::ostream &os) const { os << ";"; } -void Comment::print(std::ostream &os) const { os << "// " << str; } +void Comment::print(std::ostream &os) const { os << "/* " << str << " */"; } void GotoStmt::print(std::ostream &os) const { os << "goto "; diff --git a/lib/smack/CodifyStaticInits.cpp b/lib/smack/CodifyStaticInits.cpp index 60682c0c4..0f26e162f 100644 --- a/lib/smack/CodifyStaticInits.cpp +++ b/lib/smack/CodifyStaticInits.cpp @@ -39,18 +39,9 @@ bool CodifyStaticInits::runOnModule(Module &M) { std::deque>> worklist; for (auto &G : M.globals()) - if (G.hasInitializer()) - - // HACK: Normally only isRead should be necessary here. However, there - // seems to be a bug in the DSA code which fails to mark some globals that - // are read as read. Currently this has only been observed with globals - // that have named addresses, e.g., excluding string constants. Thus the - // second predicate here is a messy hack that has little to do with the - // intended property of being read. - if (DSA->isRead(&G) || !G.hasGlobalUnnamedAddr()) - - worklist.push_back( - std::make_tuple(G.getInitializer(), &G, std::vector())); + if (G.hasInitializer() && DSA->isRead(&G)) + worklist.push_back( + std::make_tuple(G.getInitializer(), &G, std::vector())); while (worklist.size()) { Constant *V = std::get<0>(worklist.front()); diff --git a/lib/smack/MemorySafetyChecker.cpp b/lib/smack/MemorySafetyChecker.cpp index fb7167cc6..fbb5fbabd 100644 --- a/lib/smack/MemorySafetyChecker.cpp +++ b/lib/smack/MemorySafetyChecker.cpp @@ -30,9 +30,14 @@ Function *MemorySafetyChecker::getSafetyCheckFunction(Module &M) { return F; } +void MemorySafetyChecker::copyDbgMetadata(Instruction *src, Instruction *dst) { + dst->setMetadata("dbg", src->getMetadata("dbg")); +} + void MemorySafetyChecker::insertMemoryLeakCheck(Instruction *I) { auto &M = *I->getParent()->getParent()->getParent(); - CallInst::Create(getLeakCheckFunction(M), "", I); + auto ci = CallInst::Create(getLeakCheckFunction(M), "", I); + copyDbgMetadata(I, ci); } void MemorySafetyChecker::insertMemoryAccessCheck(Value *addr, Value *size, @@ -40,10 +45,13 @@ void MemorySafetyChecker::insertMemoryAccessCheck(Value *addr, Value *size, auto &M = *I->getParent()->getParent()->getParent(); auto &C = M.getContext(); auto T = PointerType::getUnqual(Type::getInt8Ty(C)); - CallInst::Create(getSafetyCheckFunction(M), - {CastInst::Create(Instruction::BitCast, addr, T, "", I), - CastInst::CreateBitOrPointerCast(size, T, "", I)}, - "", I); + auto ptrArg = CastInst::Create(Instruction::BitCast, addr, T, "", I); + auto sizeArg = CastInst::CreateBitOrPointerCast(size, T, "", I); + auto ci = + CallInst::Create(getSafetyCheckFunction(M), {ptrArg, sizeArg}, "", I); + copyDbgMetadata(I, ptrArg); + copyDbgMetadata(I, sizeArg); + copyDbgMetadata(I, ci); } bool MemorySafetyChecker::runOnFunction(Function &F) { diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index e3584b15c..fd9c650bd 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -823,6 +823,13 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) { } } +void SmackInstGenerator::visitCallBrInst(llvm::CallBrInst &cbi) { + processInstruction(cbi); + SmackWarnings::warnUnsound("callbr instruction " + i2s(cbi), currBlock, &cbi, + cbi.getType()->isVoidTy()); + emit(Stmt::skip()); +} + bool isSourceLoc(const Stmt *stmt) { return (stmt->getKind() == Stmt::ASSUME && (llvm::cast(stmt))->hasAttr("sourceloc")) || diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 998966787..451ee725c 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -1305,7 +1305,9 @@ std::list SmackRep::globalDecl(const llvm::GlobalValue *v) { decls.push_back(Decl::axiom(Expr::eq( Expr::id(name), pointerLit(globalsOffset -= (size + globalsPadding))))); } - globalAllocations[v] = size; + + if (!llvm::isa(v)) + globalAllocations[v] = size; return decls; } diff --git a/share/smack/lib/smack-rust.c b/share/smack/lib/smack-rust.c index 48c1401fc..16e0d833f 100644 --- a/share/smack/lib/smack-rust.c +++ b/share/smack/lib/smack-rust.c @@ -29,7 +29,7 @@ return ret; \ } -#define mk_dummy_nondet_def(size) \ +#define mk_dummy_int_nondet_def(size) \ mk_signed_type(size) __VERIFIER_nondet_i##size(void) { \ return *((mk_signed_type(size) *)malloc(sizeof(mk_signed_type(size)))); \ } \ @@ -38,9 +38,14 @@ (mk_unsigned_type(size) *)malloc(sizeof(mk_unsigned_type(size)))); \ } +#define mk_dummy_fp_nondet_def(ty) \ + ty __VERIFIER_nondet_##ty(void) { return *((ty *)malloc(sizeof(ty))); } + #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) {} +mk_dummy_int_nondet_def(8) mk_dummy_int_nondet_def(16) + mk_dummy_int_nondet_def(32) mk_dummy_int_nondet_def(64) + mk_dummy_fp_nondet_def(float) + mk_dummy_fp_nondet_def(double) 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) diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index c4b79a802..28a98acbf 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -1742,14 +1742,15 @@ void __SMACK_decls(void) { D("procedure $free(p: ref);\n" "modifies $Alloc, $allocatedCounter;\n" - "requires $eq.ref.bool(p, $0.ref) || ($eq.ref.bool($base(p), p) && " - "$Alloc[p]);\n" - "requires $slt.ref.bool($0.ref, p);\n" + "requires $eq.ref.bool(p, $0.ref) || ($slt.ref.bool($0.ref, p) && " + "$eq.ref.bool($base(p), p) && $Alloc[p]);\n" "ensures $ne.ref.bool(p, $0.ref) ==> !$Alloc[p];\n" "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: {$Alloc[q]} q != p " "==> $Alloc[q] == old($Alloc[q]));\n" "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == " - "old($allocatedCounter) - 1;\n"); + "old($allocatedCounter) - 1;\n" + "ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == " + "old($allocatedCounter);\n"); #else // NO_REUSE does not reuse previously-allocated addresses D("var $Alloc: [ref] bool;"); @@ -1788,14 +1789,15 @@ void __SMACK_decls(void) { D("procedure $free(p: ref);\n" "modifies $Alloc, $allocatedCounter;\n" - "requires $eq.ref.bool(p, $0.ref) || ($eq.ref.bool($base(p), p) && " - "$Alloc[p]);\n" - "requires $slt.ref.bool($0.ref, p);\n" + "requires $eq.ref.bool(p, $0.ref) || ($slt.ref.bool($0.ref, p) && " + "$eq.ref.bool($base(p), p) && $Alloc[p]);\n" "ensures $ne.ref.bool(p, $0.ref) ==> !$Alloc[p];\n" "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: {$Alloc[q]} q != p " "==> $Alloc[q] == old($Alloc[q]));\n" "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == " - "old($allocatedCounter) - 1;\n"); + "old($allocatedCounter) - 1;\n" + "ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == " + "old($allocatedCounter);\n"); #endif #else diff --git a/share/smack/lib/smack.rs b/share/smack/lib/smack.rs index 86aa447be..06beb7a6d 100644 --- a/share/smack/lib/smack.rs +++ b/share/smack/lib/smack.rs @@ -12,6 +12,8 @@ extern "C" { pub fn __VERIFIER_nondet_u32() -> u32; pub fn __VERIFIER_nondet_i64() -> i64; pub fn __VERIFIER_nondet_u64() -> u64; + pub fn __VERIFIER_nondet_float() -> f32; + pub fn __VERIFIER_nondet_double() -> f64; 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); @@ -139,6 +141,8 @@ 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); +make_verifier_nondet!(f32, __VERIFIER_nondet_float); +make_verifier_nondet!(f64, __VERIFIER_nondet_double); #[cfg(not(verifier = "smack"))] #[cfg(feature = "std")] diff --git a/share/smack/reach.py b/share/smack/reach.py index 139dd2726..ccc21e531 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '2.6.2' +VERSION = '2.6.3' def reachParser(): diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 71970efeb..607e59aee 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -90,35 +90,22 @@ def verify_bpl_svcomp(args): or VProperty.INTEGER_OVERFLOW in args.check): inject_assert_false(args) + # Setting good loop unroll bound based on benchmark class + loopUnrollBar = 13 + time_limit = 880 + 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"] corral_command += ["/bopt:proverOpt:O:smt.arith.solver=2"] + corral_command += ["/timeLimit:%s" % time_limit] + corral_command += ["/v:1"] + corral_command += ["/recursionBound:65536"] + corral_command += ["/trackAllVars"] - with open(args.input_files[0], "r") as f: - csource = f.read() - - 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 = 13 - time_limit = 880 - - command = list(corral_command) - command += ["/timeLimit:%s" % time_limit] - command += ["/v:1"] - command += ["/recursionBound:65536"] - command += ["/irreducibleLoopUnroll:12"] - command += ["/trackAllVars"] - - verifier_output = smack.top.try_command(command, timeout=time_limit) + verifier_output = smack.top.try_command(corral_command, timeout=time_limit) result = smack.top.verification_result(verifier_output) if result in VResult.ERROR: #normal inlining diff --git a/share/smack/top.py b/share/smack/top.py index ed73f8a9c..daca4fdb0 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -13,7 +13,7 @@ from .frontend import link_bc_files, frontends, languages, extra_libs from .errtrace import error_trace, smackdOutput -VERSION = '2.6.2' +VERSION = '2.6.3' class VResult(Flag): diff --git a/test/c/memory-safety/free_null.c b/test/c/memory-safety/free_null.c new file mode 100644 index 000000000..9cd26621e --- /dev/null +++ b/test/c/memory-safety/free_null.c @@ -0,0 +1,9 @@ +#include + +// @expect verified + +int main(void) { + int *a = NULL; + free(a); + return 0; +} diff --git a/test/c/memory-safety/free_null_fail.c b/test/c/memory-safety/free_null_fail.c new file mode 100644 index 000000000..37291b609 --- /dev/null +++ b/test/c/memory-safety/free_null_fail.c @@ -0,0 +1,9 @@ +#include + +// @expect error + +int main(void) { + int *a = NULL; + free(a + 1); + return 0; +} diff --git a/test/c/memory-safety/test_sourceloc.c b/test/c/memory-safety/test_sourceloc.c new file mode 100644 index 000000000..f0ed3b912 --- /dev/null +++ b/test/c/memory-safety/test_sourceloc.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect verified + +int main(void) { + int *a; + int ret; + + if (__VERIFIER_nondet_int()) + a = (int *)malloc(sizeof(int)); + else + a = NULL; + + ret = a ? *a : 0; + free(a); + return ret; +} diff --git a/test/c/memory-safety/test_sourceloc_fail.c b/test/c/memory-safety/test_sourceloc_fail.c new file mode 100644 index 000000000..d48551460 --- /dev/null +++ b/test/c/memory-safety/test_sourceloc_fail.c @@ -0,0 +1,19 @@ +#include "smack.h" +#include + +// @expect error +// @checkout grep -v "test_sourceloc_fail.c(16,9)" + +int main(void) { + int *a; + int ret; + + if (__VERIFIER_nondet_int()) + a = (int *)malloc(sizeof(int)); + else + a = NULL; + + ret = *a; + free(a); + return ret; +} diff --git a/test/rust/basic/fp.rs b/test/rust/basic/fp.rs new file mode 100644 index 000000000..b7d1af69c --- /dev/null +++ b/test/rust/basic/fp.rs @@ -0,0 +1,14 @@ +#[macro_use] +extern crate smack; +use smack::*; + +// @expect verified +// @flag --float + +fn main() { + let a = 6.0f32.verifier_nondet(); + let b = 7.0f32.verifier_nondet(); + smack::assume!(a >= 0.0 && a <= 1.0); + smack::assume!(b == b); + smack::assert!(a + b >= b); +} diff --git a/test/rust/basic/fp_fail.rs b/test/rust/basic/fp_fail.rs new file mode 100644 index 000000000..477c4835a --- /dev/null +++ b/test/rust/basic/fp_fail.rs @@ -0,0 +1,14 @@ +#[macro_use] +extern crate smack; +use smack::*; + +// @expect error +// @flag --float + +fn main() { + let a = 6.0f32.verifier_nondet(); + let b = 7.0f32.verifier_nondet(); + smack::assume!(a >= 0.0); + smack::assume!(b == b); + smack::assert!(a + b >= b); +}