Added a pass that warns about loops

CMakeLists.txt

@@ -124,6 +124,7 @@ add_library(smackTranslator STATIC
   include/smack/SplitAggregateValue.h
   include/smack/Prelude.h
   include/smack/SmackWarnings.h
+  include/smack/LoopInfo.h
   lib/smack/AddTiming.cpp
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
@@ -151,6 +152,7 @@ add_library(smackTranslator STATIC
   lib/smack/SplitAggregateValue.cpp
   lib/smack/Prelude.cpp
   lib/smack/SmackWarnings.cpp
+  lib/smack/LoopInfo.cpp
 )
 
 add_executable(llvm2bpl

include/smack/LoopInfo.h

@@ -0,0 +1,21 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef LOOPINFO_H
+#define LOOPINFO_H
+
+#include "llvm/Pass.h"
+
+namespace smack {
+
+class LoopInfo : public llvm::FunctionPass {
+public:
+  static char ID; // Pass identification, replacement for typeid
+  LoopInfo() : llvm::FunctionPass(ID) {}
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnFunction(llvm::Function &F) override;
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
+};
+} // namespace smack
+
+#endif // LOOPINFO_H

include/smack/SmackWarnings.h

@@ -34,6 +34,8 @@ class SmackWarnings {
   static void warnApproximate(std::string name, Block *currBlock,
                               const llvm::Instruction *i);
 
+  static void warnLoop(std::string description);
+
   static void warnOverApproximate(std::string name, UnsetFlagsT unsetFlags,
                                   Block *currBlock, const llvm::Instruction *i,
                                   FlagRelation rel);

lib/smack/LoopInfo.cpp

@@ -0,0 +1,54 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+
+#define DEBUG_TYPE "smack-loop-info"
+#include "smack/LoopInfo.h"
+#include "smack/Debug.h"
+#include "smack/SmackWarnings.h"
+#include "llvm/Analysis/LoopInfo.h"
+#include "llvm/Analysis/ScalarEvolution.h"
+#include "llvm/Analysis/ScalarEvolutionExpressions.h"
+#include "llvm/Support/raw_ostream.h"
+
+namespace smack {
+
+using namespace llvm;
+
+void LoopInfo::getAnalysisUsage(AnalysisUsage &AU) const {
+  AU.setPreservesAll();
+  AU.addRequired<LoopInfoWrapperPass>();
+  AU.addRequired<ScalarEvolutionWrapperPass>();
+}
+
+bool LoopInfo::runOnFunction(Function &F) {
+  auto &loopInfo = getAnalysis<LoopInfoWrapperPass>().getLoopInfo();
+  auto &SE = getAnalysis<ScalarEvolutionWrapperPass>().getSE();
+  for (auto LI = loopInfo.begin(), LIEnd = loopInfo.end(); LI != LIEnd; ++LI) {
+    auto L = *LI;
+    auto lr = L->getLocRange();
+    auto sl = lr.getStart();
+    auto el = lr.getEnd();
+    std::string description;
+    raw_string_ostream o(description);
+    o << "found loop from line " << sl.getLine() << " to line " << el.getLine()
+      << " in function " << F.getName() << " with ";
+    // TODO: figure out why induction variable won't work
+    // auto bs = L->getInductionVariable(SE);
+    if (auto C =
+            dyn_cast<SCEVConstant>(SE.getConstantMaxBackedgeTakenCount(L))) {
+      auto CI = C->getValue()->getValue().getZExtValue();
+      o << "known loop bound " << CI;
+    } else
+      o << "unknown loop bound";
+    SmackWarnings::warnLoop(o.str());
+  }
+  return false;
+}
+
+char LoopInfo::ID = 0;
+
+StringRef LoopInfo::getPassName() const {
+  return "Get Loop Information for the purpose of sound analysis";
+}
+} // namespace smack

lib/smack/SmackWarnings.cpp

@@ -54,6 +54,12 @@ std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) {
   return ret + "}";
 }
 
+void SmackWarnings::warnLoop(std::string description) {
+  processApproximate(description + "; please check loop unrolling bound "
+                                   "otherwise there may be missed bugs",
+                     {}, nullptr, nullptr, FlagRelation::And);
+}
+
 void SmackWarnings::warnApproximate(std::string name, Block *currBlock,
                                     const Instruction *i) {
   processApproximate(

tools/llvm2bpl/llvm2bpl.cpp

@@ -34,6 +34,7 @@
 #include "smack/ExtractContracts.h"
 #include "smack/InitializePasses.h"
 #include "smack/IntegerOverflowChecker.h"
+#include "smack/LoopInfo.h"
 #include "smack/MemorySafetyChecker.h"
 #include "smack/Naming.h"
 #include "smack/NormalizeLoops.h"
@@ -213,6 +214,8 @@ int main(int argc, char **argv) {
   // pass_manager.add(new smack::SimplifyLibCalls());
   pass_manager.add(new llvm::Devirtualize());
   pass_manager.add(new smack::SplitAggregateValue());
+  pass_manager.add(llvm::createLoopSimplifyPass());
+  pass_manager.add(new smack::LoopInfo());
 
   if (smack::SmackOptions::MemorySafety) {
     pass_manager.add(new smack::MemorySafetyChecker());