Upgrade SMACK to support LLVM 13

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "sea-dsa"]
   path = sea-dsa
-  url = https://github.com/seahorn/sea-dsa.git
+  url = https://github.com/shaobo-he/sea-dsa.git

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"

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/BoogieAst.h

@@ -4,6 +4,7 @@
 #ifndef BOOGIEAST_H
 #define BOOGIEAST_H
 
+#include "llvm/ADT/StringRef.h"
 #include <list>
 #include <sstream>
 #include <string>
@@ -33,11 +34,13 @@ class Expr {
   static const Expr *id(std::string x);
   static const Expr *impl(const Expr *l, const Expr *r);
   static const Expr *lit(bool b);
+  static const Expr *lit(llvm::StringRef s);
   static const Expr *lit(std::string v);
   static const Expr *lit(unsigned v) { return lit((unsigned long long)v); }
   static const Expr *lit(unsigned long long v);
   static const Expr *lit(long long v);
   static const Expr *lit(std::string v, unsigned w);
+  static const Expr *lit(llvm::StringRef v, unsigned w);
   static const Expr *lit(unsigned long long v, unsigned w);
   static const Expr *lit(bool n, std::string s, std::string e, unsigned ss,
                          unsigned es);

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/BoogieAst.cpp

@@ -72,12 +72,16 @@ const Expr *Expr::impl(const Expr *l, const Expr *r) {
 
 const Expr *Expr::lit(bool b) { return new BoolLit(b); }
 
+const Expr *Expr::lit(llvm::StringRef s) { return lit(s.str()); }
+
 const Expr *Expr::lit(std::string v) { return new StringLit(v); }
 
 const Expr *Expr::lit(unsigned long long v) { return new IntLit(v); }
 
 const Expr *Expr::lit(long long v) { return new IntLit(v); }
 
+const Expr *Expr::lit(llvm::StringRef v, unsigned w) { return lit(v.str(), w); }
+
 const Expr *Expr::lit(std::string v, unsigned w) {
   return w ? (const Expr *)new BvLit(v, w) : (const Expr *)new IntLit(v);
 }

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

@@ -33,17 +33,21 @@ const std::map<std::string, Instruction::BinaryOps>
                                               {"mul", Instruction::Mul}};
 
 std::string IntegerOverflowChecker::getMax(unsigned bits, bool isSigned) {
+  SmallString<32> ret;
   if (isSigned)
-    return APInt::getSignedMaxValue(bits).toString(10, true);
+    APInt::getSignedMaxValue(bits).toString(ret, 10, true);
   else
-    return APInt::getMaxValue(bits).toString(10, false);
+    APInt::getMaxValue(bits).toString(ret, 10, false);
+  return ret.str().str();
 }
 
 std::string IntegerOverflowChecker::getMin(unsigned bits, bool isSigned) {
+  SmallString<32> ret;
   if (isSigned)
-    return APInt::getSignedMinValue(bits).toString(10, true);
+    APInt::getSignedMinValue(bits).toString(ret, 10, true);
   else
-    return APInt::getMinValue(bits).toString(10, false);
+    APInt::getMinValue(bits).toString(ret, 10, false);
+  return ret.str().str();
 }
 
 /*

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/SmackRep.cpp

@@ -640,7 +640,8 @@ 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);
+    SmallString<32> str;
+    (neg ? API.abs() : API).toString(str, 10, false);
     const Expr *e =
         SmackOptions::BitPrecise ? Expr::lit(str, width) : Expr::lit(str, 0);
     std::stringstream op;
@@ -706,10 +707,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, finalExpStr.str().str(),
                        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);
 }

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;
       {}