From 7a5ffe67bf9a7ce30376f8900d50369d55f4247f Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 29 Nov 2020 23:53:31 -0700 Subject: [PATCH 01/18] Added VerifierNonDet implementations for f32 and f64 --- share/smack/lib/smack-rust.c | 11 ++++++++--- share/smack/lib/smack.rs | 4 ++++ test/rust/basic/fp.rs | 14 ++++++++++++++ test/rust/basic/fp_fail.rs | 14 ++++++++++++++ 4 files changed, 40 insertions(+), 3 deletions(-) create mode 100644 test/rust/basic/fp.rs create mode 100644 test/rust/basic/fp_fail.rs 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.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/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); +} From 6b5629ce28ca93af3dbffea742004fcb46348c54 Mon Sep 17 00:00:00 2001 From: Shaobo <5892703+shaobo-he@users.noreply.github.com> Date: Fri, 4 Dec 2020 17:41:00 -0800 Subject: [PATCH 02/18] Update people.md --- docs/people.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From e69dbc0948e0c3236faf543b98eb6d42fdaf485d Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Fri, 4 Dec 2020 22:39:54 -0700 Subject: [PATCH 03/18] Removed irreducible loop unroll from SVCOMP setup The results on systems SVCOMP benchmarks indicate that we do no need this option any more. --- share/smack/svcomp/utils.py | 1 - 1 file changed, 1 deletion(-) diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 71970efeb..8efe500cc 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -115,7 +115,6 @@ def verify_bpl_svcomp(args): 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) From c300866f47671b361c5216de2ae9d0035d192b01 Mon Sep 17 00:00:00 2001 From: Shaobo <5892703+shaobo-he@users.noreply.github.com> Date: Sun, 13 Dec 2020 13:38:26 -0800 Subject: [PATCH 04/18] GitHub actions (#654) Switched to using GitHub actions instead of travis. --- .github/workflows/smack-ci.yaml | 66 +++++++++++++++++++++++++++++++++ .travis.yml | 4 ++ CMakeLists.txt | 2 +- bin/build.sh | 13 +++++++ 4 files changed, 84 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/smack-ci.yaml 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 index 3dd689375..ce0e21954 100644 --- a/.travis.yml +++ b/.travis.yml @@ -2,6 +2,10 @@ language: generic os: linux dist: focal +branches: + except: + - github-actions + addons: apt: packages: 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/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" From f9803f08a8b57d33fa77721c836dd3a3879d79a4 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 13 Dec 2020 15:32:58 -0700 Subject: [PATCH 05/18] Reverted temporary changes in travis.yml --- .travis.yml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index ce0e21954..3dd689375 100644 --- a/.travis.yml +++ b/.travis.yml @@ -2,10 +2,6 @@ language: generic os: linux dist: focal -branches: - except: - - github-actions - addons: apt: packages: From 3b3f4e85fab12deae15d016b97725b8abb938dd7 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 13 Dec 2020 15:34:50 -0700 Subject: [PATCH 06/18] Disable Travis CI --- .travis.yml | 78 ----------------------------------------------------- 1 file changed, 78 deletions(-) delete mode 100644 .travis.yml 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 From f2ae16dae87f867a0d671e04a3df895d2f84c811 Mon Sep 17 00:00:00 2001 From: Shaobo <5892703+shaobo-he@users.noreply.github.com> Date: Sun, 13 Dec 2020 14:50:30 -0800 Subject: [PATCH 07/18] Update README.md --- README.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 03728e081..6d9a21987 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) +![develop branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=develop) SMACK Logo From 2e64460178a77472406e0e8b670daf77d00dbff2 Mon Sep 17 00:00:00 2001 From: Shaobo <5892703+shaobo-he@users.noreply.github.com> Date: Sun, 13 Dec 2020 17:27:00 -0800 Subject: [PATCH 08/18] Update README.md --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 6d9a21987..c455600c2 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ -![master branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=master) -![develop branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=develop) +[![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 From ddda5e9393aa12cb8eb8a3da5dc5d79d53eaf0f2 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Mon, 14 Dec 2020 09:17:14 -0700 Subject: [PATCH 09/18] Removed /di Corral option from SVCOMP heuristics It has very small effect on the runtime. For example, on device drivers having `/di` leads to 8 less time outs, which is not significant. --- share/smack/svcomp/utils.py | 30 +++++++++--------------------- 1 file changed, 9 insertions(+), 21 deletions(-) diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 8efe500cc..607e59aee 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -90,34 +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 += ["/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 From 0d125d1c05fa7da15b4606f99dd9c2534c517e8b Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 14 Dec 2020 17:52:43 -0700 Subject: [PATCH 10/18] Translate callbr instruction to skip statement Fixes #623 Btw, the string converted from a callbr instruction can span multiple lines, so I changed comments from starting with ``//'' to starting with ``/*'' and ending with ``*/''. --- include/smack/SmackInstGenerator.h | 1 + lib/smack/BoogieAst.cpp | 2 +- lib/smack/SmackInstGenerator.cpp | 7 +++++++ 3 files changed, 9 insertions(+), 1 deletion(-) 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/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")) || From 8478a654fed2f5a7f7a4bd0f7438493340e09c12 Mon Sep 17 00:00:00 2001 From: Shaobo <5892703+shaobo-he@users.noreply.github.com> Date: Fri, 18 Dec 2020 17:50:53 -0800 Subject: [PATCH 11/18] Removed a stale hack in the CodifyStaticInits pass (#656) Removed a stale hack in the CodifyStaticInits pass --- lib/smack/CodifyStaticInits.cpp | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) 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()); From c5a8675d173b73fe33f379c50424ff897ef52cd8 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 20 Dec 2020 00:00:17 -0700 Subject: [PATCH 12/18] Allow the `free` function to take NULL pointers for mem-mod reuse and no-reuse Fixes #668 This commit also fixes incorrectly reported memory leaks for freeing NULL pointers. This is because `allocatedCounter` seems havoced but unconstrained when the argument is a NULL pointer. --- share/smack/lib/smack.c | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) 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 From 70d93110806bf5bfe72debdb3ea90c07b345a39e Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 20 Dec 2020 00:03:46 -0700 Subject: [PATCH 13/18] Added regressions. --- test/c/memory-safety/free_null.c | 9 +++++++++ test/c/memory-safety/free_null_fail.c | 9 +++++++++ 2 files changed, 18 insertions(+) create mode 100644 test/c/memory-safety/free_null.c create mode 100644 test/c/memory-safety/free_null_fail.c 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; +} From b8b9e0129c1e7a1e280e696c6d981726d05bef44 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 14 Dec 2020 00:07:13 -0700 Subject: [PATCH 14/18] Make memory-safety instrumentations copy dbg metadata Fixes #663 --- include/smack/MemorySafetyChecker.h | 1 + lib/smack/MemorySafetyChecker.cpp | 18 +++++++++++++----- 2 files changed, 14 insertions(+), 5 deletions(-) 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/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) { From df5c77ce8fa980070b5741a22f37104a78511e07 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 14 Dec 2020 00:16:29 -0700 Subject: [PATCH 15/18] Added regressions --- test/c/memory-safety/test_sourceloc.c | 18 ++++++++++++++++++ test/c/memory-safety/test_sourceloc_fail.c | 19 +++++++++++++++++++ 2 files changed, 37 insertions(+) create mode 100644 test/c/memory-safety/test_sourceloc.c create mode 100644 test/c/memory-safety/test_sourceloc_fail.c diff --git a/test/c/memory-safety/test_sourceloc.c b/test/c/memory-safety/test_sourceloc.c new file mode 100644 index 000000000..524e1c00c --- /dev/null +++ b/test/c/memory-safety/test_sourceloc.c @@ -0,0 +1,18 @@ +#include "smack.h" +#include + +// @expect verified + +int main() { + 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..c43f8b032 --- /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() { + int *a; + int ret; + + if (__VERIFIER_nondet_int()) + a = (int *)malloc(sizeof(int)); + else + a = NULL; + + ret = *a; + free(a); + return ret; +} From 63389cd187f18a1e7c97aafc92c73731305931aa Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Wed, 16 Dec 2020 22:47:10 -0700 Subject: [PATCH 16/18] Fixed regressions --- test/c/memory-safety/test_sourceloc.c | 2 +- test/c/memory-safety/test_sourceloc_fail.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test/c/memory-safety/test_sourceloc.c b/test/c/memory-safety/test_sourceloc.c index 524e1c00c..f0ed3b912 100644 --- a/test/c/memory-safety/test_sourceloc.c +++ b/test/c/memory-safety/test_sourceloc.c @@ -3,7 +3,7 @@ // @expect verified -int main() { +int main(void) { int *a; int ret; diff --git a/test/c/memory-safety/test_sourceloc_fail.c b/test/c/memory-safety/test_sourceloc_fail.c index c43f8b032..d48551460 100644 --- a/test/c/memory-safety/test_sourceloc_fail.c +++ b/test/c/memory-safety/test_sourceloc_fail.c @@ -4,7 +4,7 @@ // @expect error // @checkout grep -v "test_sourceloc_fail.c(16,9)" -int main() { +int main(void) { int *a; int ret; From e1f2339d2e1904ab6a5c0863d602e5b41fd07681 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Mon, 21 Dec 2020 15:36:26 -0700 Subject: [PATCH 17/18] Do not generate calls to $galloc procedures for functions --- lib/smack/SmackRep.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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; } From ce272be936bdd614be27482aa11cec74d3ef00e0 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Tue, 22 Dec 2020 11:16:02 -0700 Subject: [PATCH 18/18] Bumped version number to 2.6.3 --- Doxyfile | 2 +- share/smack/reach.py | 2 +- share/smack/top.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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/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/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):