Upgrade SMACK to support LLVM 13

bin/versions

@@ -5,6 +5,6 @@ BOOGIE_VERSION="2.9.6"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
-LLVM_SHORT_VERSION="12"
-LLVM_FULL_VERSION="12.0.1"
-RUST_VERSION="nightly-2021-03-01"
+LLVM_SHORT_VERSION="13"
+LLVM_FULL_VERSION="13.0.1"
+RUST_VERSION="nightly-2022-01-01"

examples/rust-cargo/Cargo.toml

@@ -2,7 +2,7 @@
 name = "rust-cargo"
 version = "0.1.0"
 authors = ["Shaobo He <[email protected]>"]
-edition = "2018"
+edition = "2021"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 

include/smack/AddTiming.h

@@ -6,6 +6,7 @@
 
 #include "llvm/IR/Instructions.h"
 #include "llvm/Pass.h"
+#include "llvm/Support/InstructionCost.h"
 
 namespace llvm {
 class TargetTransformInfo;
@@ -16,7 +17,6 @@ using namespace llvm;
 
 class AddTiming : public FunctionPass {
 
-  enum Flags { NO_TIMING_INFO = -1 };
   static const std::string INT_TIMING_COST_METADATA;
   static const std::string INSTRUCTION_NAME_METADATA;
 
@@ -25,10 +25,10 @@ class AddTiming : public FunctionPass {
   AddTiming() : FunctionPass(ID), F(nullptr), TTI(nullptr) {}
 
   /// Returns the expected cost of the instruction.
-  /// Returns -1 if the cost is unknown.
+  /// Returns invalid `InstructionCost` if the cost is unknown.
   /// Note, this method does not cache the cost calculation and it
   /// can be expensive in some cases.
-  unsigned getInstructionCost(const Instruction *I) const;
+  InstructionCost getInstructionCost(const Instruction *I) const;
 
 private:
   void addMetadata(Instruction *Inst, const std::string &name,

include/smack/IntegerOverflowChecker.h

@@ -21,8 +21,8 @@ class IntegerOverflowChecker : public llvm::ModulePass {
 private:
   static const std::map<std::string, llvm::Instruction::BinaryOps>
       INSTRUCTION_TABLE;
-  std::string getMax(unsigned bits, bool isSigned);
-  std::string getMin(unsigned bits, bool isSigned);
+  llvm::APInt getMax(unsigned bits, bool isSigned);
+  llvm::APInt getMin(unsigned bits, bool isSigned);
   llvm::Value *extendBitWidth(llvm::Value *v, int bits, bool isSigned,
                               llvm::Instruction *i);
   llvm::BinaryOperator *createFlag(llvm::Value *v, int bits, bool isSigned,

include/smack/SmackRep.h

@@ -4,6 +4,7 @@
 #ifndef SMACKREP_H
 #define SMACKREP_H
 
+#include "llvm/ADT/SmallString.h"
 #include "llvm/IR/DataLayout.h"
 #include "llvm/IR/GetElementPtrTypeIterator.h"
 #include "llvm/IR/InstVisitor.h"

lib/smack/AddTiming.cpp

@@ -91,9 +91,9 @@ bool AddTiming::runOnFunction(Function &F) {
 }
 
 void AddTiming::addTimingMetadata(Instruction *Inst) const {
-  unsigned Cost = getInstructionCost(Inst);
-  if (Cost != (unsigned)NO_TIMING_INFO) {
-    addMetadata(Inst, "smack.InstTimingCost.Int64", Cost);
+  auto Cost = getInstructionCost(Inst);
+  if (Cost.isValid()) {
+    addMetadata(Inst, "smack.InstTimingCost.Int64", *Cost.getValue());
   }
 }
 
@@ -118,9 +118,9 @@ static TargetTransformInfo::OperandValueKind getOperandInfo(Value *V) {
   return OpInfo;
 }
 
-unsigned AddTiming::getInstructionCost(const Instruction *I) const {
+InstructionCost AddTiming::getInstructionCost(const Instruction *I) const {
   if (!TTI)
-    return NO_TIMING_INFO;
+    return InstructionCost::getInvalid();
 
   // When an assume statement appears in the C code
   // llvm turns it into a series of IR instructions
@@ -132,7 +132,7 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
   // return 0
 
   if (VerifierCodeMetadata::isMarked(*I)) {
-    return 0;
+    return InstructionCost(0);
   }
 
   switch (I->getOpcode()) {
@@ -216,14 +216,10 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
     return TTI->getCastInstrCost(I->getOpcode(), I->getType(), SrcTy,
                                  TTI->getCastContextHint(I));
   }
-  case Instruction::ExtractElement: {
-    return NO_TIMING_INFO;
-  }
-  case Instruction::InsertElement: {
-    return NO_TIMING_INFO;
-  }
+  case Instruction::ExtractElement:
+  case Instruction::InsertElement:
   case Instruction::ShuffleVector: {
-    return NO_TIMING_INFO;
+    return InstructionCost::getInvalid();
   }
   case Instruction::Call: {
     if (const IntrinsicInst *II = dyn_cast<IntrinsicInst>(I)) {
@@ -241,11 +237,11 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
           TargetTransformInfo::TargetCostKind::TCK_Latency);
     }
 
-    return NO_TIMING_INFO;
+    return InstructionCost::getInvalid();
   }
   default:
     // We don't have any information on this instruction.
-    return NO_TIMING_INFO;
+    return InstructionCost::getInvalid();
   }
 }
 
@@ -271,8 +267,8 @@ void AddTiming::print(raw_ostream &OS, const Module *) const {
   for (Function::iterator B = F->begin(), BE = F->end(); B != BE; ++B) {
     for (BasicBlock::iterator it = B->begin(), e = B->end(); it != e; ++it) {
       Instruction *Inst = &*it;
-      unsigned Cost = getInstructionCost(Inst);
-      if (Cost != (unsigned)NO_TIMING_INFO) {
+      auto Cost = getInstructionCost(Inst);
+      if (Cost.isValid()) {
         OS << "Cost Model: Found an estimated cost of " << Cost;
       } else {
         OS << "Cost Model: Unknown cost";

lib/smack/ExtractContracts.cpp

@@ -188,7 +188,8 @@ Function *getContractExpr(Function *F, CallInst *I) {
     DestA->setName(A.getName());
     VMap[&A] = &*DestA++;
   }
-  CloneFunctionInto(NewF, F, VMap, false, Returns);
+  CloneFunctionInto(NewF, F, VMap, CloneFunctionChangeType::LocalChangesOnly,
+                    Returns);
   setReturnToArgumentValue(NewF, dyn_cast<CallInst>(VMap[I]));
   return NewF;
 }

lib/smack/IntegerOverflowChecker.cpp

@@ -32,18 +32,14 @@ const std::map<std::string, Instruction::BinaryOps>
                                               {"sub", Instruction::Sub},
                                               {"mul", Instruction::Mul}};
 
-std::string IntegerOverflowChecker::getMax(unsigned bits, bool isSigned) {
-  if (isSigned)
-    return APInt::getSignedMaxValue(bits).toString(10, true);
-  else
-    return APInt::getMaxValue(bits).toString(10, false);
+APInt IntegerOverflowChecker::getMax(unsigned bits, bool isSigned) {
+  return isSigned ? APInt::getSignedMaxValue(bits).sext(bits * 2)
+                  : APInt::getMaxValue(bits).zext(bits * 2);
 }
 
-std::string IntegerOverflowChecker::getMin(unsigned bits, bool isSigned) {
-  if (isSigned)
-    return APInt::getSignedMinValue(bits).toString(10, true);
-  else
-    return APInt::getMinValue(bits).toString(10, false);
+APInt IntegerOverflowChecker::getMin(unsigned bits, bool isSigned) {
+  return isSigned ? APInt::getSignedMinValue(bits).sext(bits * 2)
+                  : APInt::getMinValue(bits).zext(bits * 2);
 }
 
 /*
@@ -67,12 +63,12 @@ Value *IntegerOverflowChecker::extendBitWidth(Value *v, int bits, bool isSigned,
 BinaryOperator *IntegerOverflowChecker::createFlag(Value *v, int bits,
                                                    bool isSigned,
                                                    Instruction *i) {
-  ConstantInt *max = ConstantInt::get(
+  auto *max = ConstantInt::get(
       IntegerType::get(i->getFunction()->getContext(), bits * 2),
-      getMax(bits, isSigned), 10);
-  ConstantInt *min = ConstantInt::get(
+      getMax(bits, isSigned));
+  auto *min = ConstantInt::get(
       IntegerType::get(i->getFunction()->getContext(), bits * 2),
-      getMin(bits, isSigned), 10);
+      getMin(bits, isSigned));
   CmpInst::Predicate maxCmpPred =
       (isSigned ? CmpInst::ICMP_SGT : CmpInst::ICMP_UGT);
   CmpInst::Predicate minCmpPred =

lib/smack/Prelude.cpp

@@ -169,7 +169,9 @@ FuncDecl *builtinOp(std::string baseName, const Attr *attr,
 std::string getIntLimit(unsigned size) {
   auto n = APInt(size + 1, 0);
   n.setBit(size);
-  return n.toString(10, false);
+  SmallString<32> rstr;
+  n.toStringUnsigned(rstr, 10);
+  return std::string(rstr);
 }
 
 const std::vector<unsigned> IntOpGen::INTEGER_SIZES{

lib/smack/SmackInstGenerator.cpp

@@ -1218,7 +1218,10 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
   auto it = stmtMap.find(ii.getIntrinsicID());
   if (it != stmtMap.end())
     it->second(&ii);
-  else {
+  else if (ii.getIntrinsicID() ==
+           llvm::Intrinsic::experimental_noalias_scope_decl) {
+    // Ignore this function as we cannot handle arguments of metadata type.
+  } else {
     SmackWarnings::warnApproximate(ii.getCalledFunction()->getName().str(),
                                    currBlock, &ii);
     emit(rep->call(ii.getCalledFunction(), ii));

lib/smack/SmackRep.cpp

@@ -640,9 +640,11 @@ const Expr *SmackRep::lit(const llvm::Value *v, bool isUnsigned,
     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);
+    SmallString<32> str;
+    (neg ? API.abs() : API).toString(str, 10, false);
+    const Expr *e = SmackOptions::BitPrecise
+                        ? Expr::lit(std::string(str), width)
+                        : Expr::lit(std::string(str), 0);
     std::stringstream op;
     op << "$sub." << (SmackOptions::BitPrecise ? "bv" : "i") << width;
     return neg ? Expr::fn(op.str(), integerLit(0ULL, width), e) : e;
@@ -706,10 +708,14 @@ const Expr *SmackRep::lit(const llvm::Value *v, bool isUnsigned,
 
       sig.setBit(sig.getBitWidth() - 1);
 
-      std::string hexSig = sig.toString(16, false).substr(1);
+      SmallString<32> sigStr;
+      sig.toString(sigStr, 16, false);
+      std::string hexSig = sigStr.substr(1).str();
       hexSig.insert(leftSize / 4, ".");
 
-      return Expr::lit(API.isNegative(), hexSig, finalExp.toString(10, true),
+      SmallString<32> finalExpStr;
+      finalExp.toString(finalExpStr, 10, true);
+      return Expr::lit(API.isNegative(), hexSig, std::string(finalExpStr),
                        sigSize, expSize);
     } else {
       const APFloat APF = CFP->getValueAPF();

lib/smack/VectorOperations.cpp

@@ -55,7 +55,8 @@ const Expr *VectorOperations::constant(const ConstantDataVector *C) {
 const Expr *VectorOperations::constant(const ConstantAggregateZero *C) {
   auto T = C->getType();
   std::list<const Expr *> args;
-  for (unsigned i = 0; i < C->getNumElements(); i++)
+  auto elemCount = C->getElementCount().getFixedValue();
+  for (unsigned i = 0; i < elemCount; i++)
     args.push_back(rep->expr(C->getElementValue(i)));
   return Expr::fn(constructor(T), args);
 }

share/smack/frontend.py

@@ -2,7 +2,7 @@
 import sys
 import re
 import json
-from .utils import temporary_file, try_command, temporary_directory,\
+from .utils import temporary_file, try_command, temporary_directory, \
     llvm_exact_bin, smack_headers, smack_lib
 from .versions import RUST_VERSION
 

share/smack/lib/smack/Cargo.toml

@@ -2,7 +2,7 @@
 name = "smack"
 version = "0.1.0"
 authors = ["Shaobo He <[email protected]>"]
-edition = "2018"
+edition = "2021"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 

share/smack/top.py

@@ -11,7 +11,7 @@
 import yaml
 from enum import Flag, auto
 from .svcomp.utils import verify_bpl_svcomp
-from .utils import temporary_file, try_command, remove_temp_files,\
+from .utils import temporary_file, try_command, remove_temp_files, \
     llvm_exact_bin, smack_portfolio_path
 from .replay import replay_error_trace
 from .frontend import link_bc_files, frontends, languages, extra_libs

test/c/failing/floppy_false.i.cil.c

@@ -2291,8 +2291,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject,
           disketteExtension->TargetObject =
               IoAttachDeviceToDeviceStack(deviceObject, PhysicalDeviceObject);
         }
-        {}
-        {
+        {} {
           /*       KeInitializeSemaphore(& disketteExtension->RequestSemaphore,
            * 0L, 2147483647); */ /* INLINED */
           disketteExtension->PowerDownMutex.Count = 1;
@@ -2615,11 +2614,9 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     } else {
     }
     {
-      /*   ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED
-                                                                        */
-    }
-    {}
-    {
+        /*   ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED
+                                                                          */
+    } {} {
       /*   ExAcquireFastMutex(& DisketteExtension->ThreadReferenceMutex); */ /* INLINED */
       DisketteExtension->ThreadReferenceCount += 1L;
     }
@@ -3221,8 +3218,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                     goto switch_16_break;
                                   } else {
                                   }
-                                  {}
-                                  {
+                                  {} {
                                     ntStatus = FlQueueIrpToThread(
                                         Irp, disketteExtension);
                                   }
@@ -4172,9 +4168,7 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     _L___0 : /* CIL Label */
     {}
     }
-    {}
-    {}
-    { IofCompleteRequest(Irp, 1); }
+    {} {} { IofCompleteRequest(Irp, 1); }
     return;
   }
 }
@@ -4775,8 +4769,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                                 .__annonCompField16.CurrentStackLocation -= 1;
                             ntStatus = FlReadWrite(DisketteExtension, irp, 1);
                           }
-                          {}
-                          {
+                          {} {
                             /*                     MmUnlockPages(irp->MdlAddress);
                              */ /* INLINED */
                             /*                     IoFreeMdl(irp->MdlAddress);
@@ -5059,10 +5052,11 @@ void FloppyThread(PVOID Context) {
               }
             } else {
             }
-            { /*         ExReleaseFastMutex(PagingMutex); */ /* INLINED */
+            {
+                /*         ExReleaseFastMutex(PagingMutex); */ /* INLINED */
+            } {} {
+              PsTerminateSystemThread(0L);
             }
-            {}
-            { PsTerminateSystemThread(0L); }
           } else {
           }
           {
@@ -5666,8 +5660,7 @@ void FlConsolidateMediaTypeWithBootSector(PDISKETTE_EXTENSION DisketteExtension,
       }
     } else {
     }
-    {}
-    {}
+    {} {}
     if ((int)bpbMediaType == (int)DisketteExtension->MediaType) {
       changeToBpbMedia = 0;
       {}