Release 2.10.0

.github/workflows/smack-ci.yaml

@@ -4,7 +4,7 @@ on: [push, pull_request]
 
 jobs:
   check-regressions:
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     strategy:
       matrix:
         regtest_env:
@@ -41,7 +41,7 @@ jobs:
             "--exhaustive --folder=llvm --languages=llvm-ir"
           ]
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v7
 
       - name: install dependencies
         env:
@@ -59,22 +59,22 @@ jobs:
         run: ./bin/build.sh
 
   build-and-push-docker:
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     needs: check-regressions
 
     steps:
       - name: Check Out Repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v7
 
       - name: Login to Docker Hub
-        uses: docker/login-action@v1
+        uses: docker/login-action@v4
         with:
           username: ${{ secrets.DOCKER_HUB_USERNAME }}
           password: ${{ secrets.DOCKER_HUB_ACCESS_TOKEN }}
 
       - name: Set up Docker Buildx
         id: buildx
-        uses: docker/setup-buildx-action@v1
+        uses: docker/setup-buildx-action@v4
 
       # borrowed from:
       # https://stackoverflow.com/questions/58033366/how-to-get-current-branch-within-github-actions/58035262
@@ -94,7 +94,7 @@ jobs:
       - name: Build and push
         if: ${{ steps.set_tag.outputs.docker_tag != 'none' }}
         id: docker_build
-        uses: docker/build-push-action@v2
+        uses: docker/build-push-action@v7
         with:
           context: ./
           file: ./Dockerfile

Dockerfile

@@ -1,4 +1,4 @@
-FROM ubuntu:22.04
+FROM ubuntu:24.04
 MAINTAINER Shaobo He <polarishehn@gmail.com>
 
 ENV SMACKDIR /home/user/smack

Doxyfile

@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.9.0
+PROJECT_NUMBER         = 2.10.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

README.md

@@ -1,5 +1,5 @@
-[![main branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=main)](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)
+[![main branch ci status](https://github.com/smackers/smack/actions/workflows/smack-ci.yaml/badge.svg?branch=main)](https://github.com/smackers/smack/actions)
+[![develop branch ci status](https://github.com/smackers/smack/actions/workflows/smack-ci.yaml/badge.svg?branch=develop)](https://github.com/smackers/smack/actions)
 
 <img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
 
@@ -62,4 +62,3 @@ benchmarking of SMACK.
 1. [Projects](docs/projects.md)
 1. [Publications](docs/publications.md)
 1. [People](docs/people.md)
-

bin/build.sh

@@ -200,7 +200,7 @@ linux-opensuse*)
   DEPENDENCIES+=" ncurses-devel"
   ;;
 
-linux-@(ubuntu|neon)-@(16|18|20|22)*)
+linux-@(ubuntu|neon)-@(16|18|20|22|24)*)
   if [ ${INSTALL_LLVM} -eq 1 ] ; then
     DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
   fi
@@ -248,7 +248,7 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] ; then
     sudo zypper --non-interactive install ${DEPENDENCIES}
     ;;
 
-  linux-@(ubuntu|neon)-@(1[68]|20|22)*)
+  linux-@(ubuntu|neon)-@(1[68]|20|22|24)*)
     RELEASE_VERSION=$(get-platform-trim "$(lsb_release -r)" | awk -F: '{print $2;}')
     case "$RELEASE_VERSION" in
     16*)
@@ -263,6 +263,9 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] ; then
     22*)
       UBUNTU_CODENAME="jammy"
       ;;
+    24*)
+      UBUNTU_CODENAME="noble"
+      ;;
     *)
       puts "Release ${RELEASE_VERSION} for ${distro} not supported. Dependencies must be installed manually."
       exit 1
@@ -274,13 +277,25 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] ; then
     fi
 
     # Adding LLVM repository
-    if [ ${INSTALL_LLVM} -eq 1 ] ; then
+    # Ubuntu 24.04 (noble) ships the pinned Clang/LLVM version in its own
+    # (universe) repositories, and apt.llvm.org has no llvm-toolchain-noble feed
+    # for it, so on 24.04 the LLVM packages are installed directly from the Ubuntu
+    # archive instead of adding an apt.llvm.org repository (which also avoids the
+    # removed apt-key on noble).
+    if [ ${INSTALL_LLVM} -eq 1 ] && [[ "$RELEASE_VERSION" != 24* ]] ; then
       ${WGET} -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add -
       sudo add-apt-repository "deb http://apt.llvm.org/${UBUNTU_CODENAME}/ llvm-toolchain-${UBUNTU_CODENAME}-${LLVM_SHORT_VERSION} main"
     fi
 
-    # Adding .NET repository (skip for 22.04+ as it provides .NET 6 natively)
-    if [[ "$RELEASE_VERSION" != 22* ]]; then
+    # Adding .NET repository for dotnet-sdk-6.0 (required by Boogie and Corral):
+    # - 20.04 and older: use Microsoft's package feed
+    # - 22.04: .NET 6 is available in the default Ubuntu repositories
+    # - 24.04: .NET 6 is neither in the Ubuntu archive nor Microsoft's feed
+    #   (Microsoft stopped publishing to packages.microsoft.com for 24.04), so
+    #   use Canonical's dotnet backports PPA
+    if [[ "$RELEASE_VERSION" == 24* ]]; then
+      sudo add-apt-repository -y ppa:dotnet/backports
+    elif [[ "$RELEASE_VERSION" != 22* ]]; then
       ${WGET} -q https://packages.microsoft.com/config/ubuntu/${RELEASE_VERSION}/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
       sudo DEBIAN_FRONTEND=noninteractive dpkg -i --force-confdef --force-confold packages-microsoft-prod.deb
       rm -f packages-microsoft-prod.deb

bin/versions

@@ -5,6 +5,6 @@ BOOGIE_VERSION="2.15.7"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
-LLVM_SHORT_VERSION="13"
-LLVM_FULL_VERSION="13.0.1"
-RUST_VERSION="nightly-2022-01-01"
+LLVM_SHORT_VERSION="14"
+LLVM_FULL_VERSION="14.0.0"
+RUST_VERSION="nightly-2022-08-12"

examples/rise4fun/rise_simple.c

@@ -1,4 +1,5 @@
 #include "smack.h"
+#include <assert.h>
 
 int main(void) {
   int x, y, z;

examples/rise4fun/rise_simple_buggy.c

@@ -1,4 +1,5 @@
 #include "smack.h"
+#include <assert.h>
 
 int main(void) {
   int x, y, z;

include/smack/MemorySafetyChecker.h

@@ -21,6 +21,7 @@ class MemorySafetyChecker : public llvm::FunctionPass,
   void insertMemoryLeakCheck(llvm::Instruction *I);
   void insertMemoryAccessCheck(llvm::Value *addr, llvm::Value *size,
                                llvm::Instruction *I);
+  bool visitSplitAggregateAccess(llvm::Value *addr, llvm::Instruction *I);
 
 public:
   static char ID; // Pass identification, replacement for typeid

include/smack/NormalizeLoops.h

@@ -4,19 +4,19 @@
 #ifndef NORMALIZELOOPS_H
 #define NORMALIZELOOPS_H
 
+#include "llvm/Analysis/LoopPass.h"
 #include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
 #include "llvm/Pass.h"
 #include <map>
 
 namespace smack {
 
-class NormalizeLoops : public llvm::ModulePass {
+class NormalizeLoops : public llvm::LoopPass {
 public:
   static char ID; // Pass identification, replacement for typeid
-  NormalizeLoops() : llvm::ModulePass(ID) {}
+  NormalizeLoops() : llvm::LoopPass(ID) {}
   virtual llvm::StringRef getPassName() const override;
-  virtual bool runOnModule(llvm::Module &m) override;
+  virtual bool runOnLoop(llvm::Loop *L, llvm::LPPassManager &LPM) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
 } // namespace smack

include/smack/SmackInstGenerator.h

@@ -6,6 +6,7 @@
 
 #include "llvm/Analysis/LoopInfo.h"
 #include "llvm/IR/InstVisitor.h"
+#include <map>
 #include <set>
 #include <unordered_set>
 

include/smack/SmackRep.h

@@ -12,6 +12,7 @@
 #include "llvm/Support/GraphWriter.h"
 #include "llvm/Support/Regex.h"
 #include <list>
+#include <map>
 #include <sstream>
 
 namespace smack {

include/smack/SplitAggregateValue.h

@@ -14,6 +14,11 @@
 
 namespace smack {
 
+namespace SplitAggregateValueMetadata {
+extern const char MemoryAccess[];
+extern const char WholeMemoryAccess[];
+} // namespace SplitAggregateValueMetadata
+
 class SplitAggregateValue : public llvm::FunctionPass {
 public:
   typedef std::vector<std::pair<llvm::Value *, unsigned>> IndexT;
@@ -25,9 +30,11 @@ class SplitAggregateValue : public llvm::FunctionPass {
 private:
   llvm::Value *splitAggregateLoad(llvm::Type *T, llvm::Value *P,
                                   std::vector<InfoT> &info,
-                                  llvm::IRBuilder<> &irb);
+                                  llvm::IRBuilder<> &irb,
+                                  bool preserveWholeAccessCheck);
   void splitAggregateStore(llvm::Value *P, llvm::Value *V,
-                           std::vector<InfoT> &info, llvm::IRBuilder<> &irb);
+                           std::vector<InfoT> &info, llvm::IRBuilder<> &irb,
+                           bool preserveWholeAccessCheck);
   void splitConstantReturn(llvm::ReturnInst *ri, std::vector<InfoT> &info);
   void splitConstantArg(llvm::CallInst *ci, unsigned i,
                         std::vector<InfoT> &info);

include/utils/Devirt.h

@@ -25,6 +25,7 @@
 
 #include "seadsa/CompleteCallGraph.hh"
 
+#include <map>
 #include <set>
 
 using namespace llvm;
@@ -79,4 +80,3 @@ namespace llvm {
       }
   };
 }
-

lib/smack/AddTiming.cpp

@@ -175,12 +175,14 @@ InstructionCost AddTiming::getInstructionCost(const Instruction *I) const {
   case Instruction::Select: {
     const SelectInst *SI = cast<SelectInst>(I);
     Type *CondTy = SI->getCondition()->getType();
-    return TTI->getCmpSelInstrCost(I->getOpcode(), I->getType(), CondTy);
+    return TTI->getCmpSelInstrCost(I->getOpcode(), I->getType(), CondTy,
+                                   CmpInst::BAD_ICMP_PREDICATE);
   }
   case Instruction::ICmp:
   case Instruction::FCmp: {
     Type *ValTy = I->getOperand(0)->getType();
-    return TTI->getCmpSelInstrCost(I->getOpcode(), ValTy);
+    return TTI->getCmpSelInstrCost(I->getOpcode(), ValTy, nullptr,
+                                   CmpInst::BAD_ICMP_PREDICATE);
   }
   case Instruction::Store: {
     const StoreInst *SI = cast<StoreInst>(I);
@@ -224,7 +226,7 @@ InstructionCost AddTiming::getInstructionCost(const Instruction *I) const {
   case Instruction::Call: {
     if (const IntrinsicInst *II = dyn_cast<IntrinsicInst>(I)) {
       SmallVector<Type *, 4> Tys;
-      for (unsigned J = 0, JE = II->getNumArgOperands(); J != JE; ++J)
+      for (unsigned J = 0, JE = II->arg_size(); J != JE; ++J)
         Tys.push_back(II->getArgOperand(J)->getType());
 
       FastMathFlags FMF;

lib/smack/AnnotateLoopExits.cpp

@@ -8,7 +8,6 @@
 // to reach the loop exit.
 //
 
-#define DEBUG_TYPE "smack-loop-unroll"
 #include "smack/AnnotateLoopExits.h"
 #include "smack/Debug.h"
 #include "smack/Naming.h"
@@ -27,6 +26,8 @@
 
 #include "llvm/Support/raw_ostream.h"
 
+#define DEBUG_TYPE "smack-loop-unroll"
+
 namespace smack {
 
 using namespace llvm;

lib/smack/CodifyStaticInits.cpp

@@ -52,7 +52,10 @@ bool CodifyStaticInits::runOnModule(Module &M) {
     if (V->getType()->isIntegerTy() || V->getType()->isPointerTy() ||
         V->getType()->isFloatingPointTy() || V->getType()->isVectorTy())
 
-      IRB.CreateStore(V, IRB.CreateGEP(P, ArrayRef<Value *>(I)));
+      IRB.CreateStore(
+          V,
+          IRB.CreateGEP(P->getType()->getScalarType()->getPointerElementType(),
+                        P, ArrayRef<Value *>(I)));
 
     else if (ArrayType *AT = dyn_cast<ArrayType>(V->getType()))
       for (unsigned i = AT->getNumElements(); i-- > 0;) {

lib/smack/ExtractContracts.cpp

@@ -2,8 +2,6 @@
 // This file is distributed under the MIT License. See LICENSE for details.
 //
 
-#define DEBUG_TYPE "contracts"
-
 #include "smack/ExtractContracts.h"
 #include "smack/Debug.h"
 #include "smack/Naming.h"
@@ -15,6 +13,8 @@
 #include "llvm/Transforms/Utils/Cloning.h"
 #include "llvm/Transforms/Utils/CodeExtractor.h"
 
+#define DEBUG_TYPE "contracts"
+
 #include <map>
 #include <set>
 #include <stack>
@@ -247,7 +247,7 @@ bool ExtractContracts::runOnModule(Module &M) {
         // function
         for (auto Fs : getContractExprs(*newF)) {
           std::vector<Value *> Args;
-          for (auto &A : I->arg_operands())
+          for (auto &A : I->args())
             Args.push_back(A);
           auto *E = Builder.CreateCall(std::get<1>(Fs), Args);
           Builder.CreateCall(std::get<0>(Fs), {E});
@@ -276,7 +276,7 @@ bool ExtractContracts::runOnModule(Module &M) {
         // insert one invariant invocation per invocation in the original loop
         for (auto Fs : getContractExprs(*newF)) {
           std::vector<Value *> Args;
-          for (auto &A : I->arg_operands())
+          for (auto &A : I->args())
             Args.push_back(A);
           auto *E = Builder.CreateCall(std::get<1>(Fs), Args);
           Builder.CreateCall(std::get<0>(Fs), {E});