Refactor AnnotateLoopEnds and remove extra prints

Rename AnnotateLoopEnds to AnnotateLoopExits Remove some extrateous pringing in AnnotateLoopExits, and put the remaining print statements into the smack debug printing macro.
TerrisGO · Sep 13, 2021 · 9dd9f15 · 9dd9f15
1 parent 9cc59b3
commit 9dd9f15
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 25 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -120,7 +120,7 @@ add_library(smackTranslator STATIC
   include/smack/RewriteBitwiseOps.h
   include/smack/NormalizeLoops.h
   include/smack/RustFixes.h
-  include/smack/AnnotateLoopEnds.h
+  include/smack/AnnotateLoopExits.h
   include/smack/SplitAggregateValue.h
   include/smack/Prelude.h
   include/smack/SmackWarnings.h
@@ -147,7 +147,7 @@ add_library(smackTranslator STATIC
   lib/smack/RewriteBitwiseOps.cpp
   lib/smack/NormalizeLoops.cpp
   lib/smack/RustFixes.cpp
-  lib/smack/AnnotateLoopEnds.cpp
+  lib/smack/AnnotateLoopExits.cpp
   lib/smack/SplitAggregateValue.cpp
   lib/smack/Prelude.cpp
   lib/smack/SmackWarnings.cpp

diff --git a/include/smack/AnnotateLoopEnds.h → include/smack/AnnotateLoopExits.h b/include/smack/AnnotateLoopEnds.h → include/smack/AnnotateLoopExits.h
@@ -1,8 +1,8 @@
 //
 // This file is distributed under the MIT License. See LICENSE for details.
 //
-#ifndef ANNOTATELOOPENDS_H
-#define ANNOTATELOOPENDS_H
+#ifndef ANNOTATELOOPEXITS_H
+#define ANNOTATELOOPEXITS_H
 
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
@@ -11,14 +11,14 @@
 
 namespace smack {
 
-class AnnotateLoopEnds : public llvm::ModulePass {
+class AnnotateLoopExits : public llvm::ModulePass {
 public:
   static char ID; // Pass identification, replacement for typeid
-  AnnotateLoopEnds() : llvm::ModulePass(ID) {}
+  AnnotateLoopExits() : llvm::ModulePass(ID) {}
   virtual llvm::StringRef getPassName() const override;
   virtual bool runOnModule(llvm::Module &m) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
 } // namespace smack
 
-#endif // ANNOTATELOOPENDS_H
+#endif // ANNOTATELOOPEXITS_H
diff --git a/lib/smack/AnnotateLoopEnds.cpp → lib/smack/AnnotateLoopExits.cpp b/lib/smack/AnnotateLoopEnds.cpp → lib/smack/AnnotateLoopExits.cpp
@@ -8,8 +8,10 @@
 // is added between a branching block and the loop header.
 //
 
-#include "smack/AnnotateLoopEnds.h"
+#define DEBUG_TYPE "smack-loop-unroll"
+#include "smack/AnnotateLoopExits.h"
 #include "smack/Naming.h"
+#include "smack/Debug.h"
 #include "llvm/Analysis/LoopInfo.h"
 #include "llvm/Transforms/Utils.h"
 #include "llvm/IR/Constants.h"
@@ -29,19 +31,20 @@ namespace smack {
 using namespace llvm;
 
 // Register LoopInfo
-void AnnotateLoopEnds::getAnalysisUsage(AnalysisUsage &AU) const {
+void AnnotateLoopExits::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequiredID(LoopSimplifyID);
   AU.addRequired<LoopInfoWrapperPass>();
 }
 
+// This method is for clarity and self-documentingness
 void insertLoopEndAssertion(Function *le, Instruction *insertBefore) {
   CallInst::Create(le, "", insertBefore);
 }
 
 void processExitBlock(BasicBlock *block, Function *le) {
   // print exit block found!!
 
-  errs() << "    Exit block found! \n";
+  SDEBUG(errs() << "Processing an Exit Block\n");
 
   Instruction& front = block->front();
   insertLoopEndAssertion(le,&front);
@@ -51,39 +54,32 @@ void annotateLoopEnd(Loop *loop, Function *le) {
   //BasicBlock *headerBlock = loop->getHeader();
 
   // I imagine that it is very uncommon for a loop to have
-  //   more than 5 exit points.
+  //   more than 5 exit points. This is a complete guess
+  //   and we could probably have a better heuristic
   SmallVector<BasicBlock *, 5> exitBlocks; 
 
   loop->getExitBlocks(exitBlocks);
 
   for (BasicBlock *b : exitBlocks) {
     processExitBlock(b,le);
   } 
-
-  // Handle subloops
-  //for (Loop *subloop : loop->getSubLoops()) {
-  //  processLoop(subloop);
-  //}
 }
 
-bool AnnotateLoopEnds::runOnModule(Module &m) {
+bool AnnotateLoopExits::runOnModule(Module &m) {
 
   Function *le = m.getFunction("__SMACK_loop_end");
   assert(le != NULL && "Function __SMACK_loop_end shoudl be present.");
 
-  errs() << "Module Start\n";
   for (auto F = m.begin(), FEnd = m.end(); F != FEnd; ++F) {
     if (F->isIntrinsic() || F->empty()) {
       continue;
     }
 
-    errs() << "Hello " << F->getName() << "\n";
-
     LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>(*F).getLoopInfo();
     for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
          LI != LIEnd; ++LI) {
 
-      errs() << "  Loop Found in " << F->getName() << "\n";
+      SDEBUG(errs() << "Processing Loop in " << F->getName() << "\n");
       annotateLoopEnd(*LI, le);
     }
   }
@@ -92,7 +88,7 @@ bool AnnotateLoopEnds::runOnModule(Module &m) {
 }
 
 // Pass ID variable
-char AnnotateLoopEnds::ID = 0;
+char AnnotateLoopExits::ID = 0;
 
-StringRef AnnotateLoopEnds::getPassName() const { return "Annotate Loop Ends with assert(false)"; }
+StringRef AnnotateLoopExits::getPassName() const { return "Annotate Loop Ends with assert(false)"; }
 } // namespace smack
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
@@ -36,7 +36,7 @@
 #include "smack/MemorySafetyChecker.h"
 #include "smack/Naming.h"
 #include "smack/NormalizeLoops.h"
-#include "smack/AnnotateLoopEnds.h"
+#include "smack/AnnotateLoopExits.h"
 #include "smack/RemoveDeadDefs.h"
 #include "smack/RewriteBitwiseOps.h"
 #include "smack/RustFixes.h"
@@ -197,7 +197,7 @@ int main(int argc, char **argv) {
 
   // pass_manager.add(new llvm::StructRet());
   pass_manager.add(new smack::NormalizeLoops());
-  pass_manager.add(new smack::AnnotateLoopEnds());
+  pass_manager.add(new smack::AnnotateLoopExits());
   pass_manager.add(new llvm::SimplifyEV());
   pass_manager.add(new llvm::SimplifyIV());
   pass_manager.add(new smack::ExtractContracts());