Merge branch 'release-2.6.1'

.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

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
 )

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

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

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}

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 $@
 

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"

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"] 

examples/rust-cargo/.gitignore

@@ -0,0 +1,3 @@
+/target
+**/*.rs.bk
+Cargo.lock

examples/rust-cargo/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "rust-cargo"
+version = "0.1.0"
+authors = ["Shaobo He <[email protected]>"]
+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
+

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);
+}

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<std::string> RUST_PANICS;
   static const std::string RUST_PANIC_ANNOTATION;
 

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

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

include/smack/SmackOptions.h

@@ -25,6 +25,7 @@ class SmackOptions {
   static const llvm::cl::opt<bool> SourceLocSymbols;
   static llvm::cl::opt<bool> BitPrecise;
   static const llvm::cl::opt<bool> BitPrecisePointers;
+  static const llvm::cl::opt<bool> RewriteBitwiseOps;
   static const llvm::cl::opt<bool> NoMemoryRegionSplitting;
   static const llvm::cl::opt<bool> NoByteAccessInference;
   static const llvm::cl::opt<bool> FloatEnabled;

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<std::pair<llvm::Value *, llvm::gep_type_iterator>> 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);

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);