Working first version of loop exit pass

Added code to AnnotateLoopEnds which inserts
a boogie 'assert false' at any exit of a loop.

The assertions are inserted at the beginning
of the "loop exit" basic block, that is the
immediate node outside of the loop.
In order to prevent a random failure, the pass
now requires the LoopSimplify pass to run first,
which guarentees that each loop exit block is
dominated only by the loop.

include/smack/AnnotateLoopEnds.h

@@ -11,12 +11,12 @@
 
 namespace smack {
 
-class AnnotateLoopEnds : public llvm::FunctionPass {
+class AnnotateLoopEnds : public llvm::ModulePass {
 public:
   static char ID; // Pass identification, replacement for typeid
-  AnnotateLoopEnds() : llvm::FunctionPass(ID) {}
+  AnnotateLoopEnds() : llvm::ModulePass(ID) {}
   virtual llvm::StringRef getPassName() const override;
-  virtual bool runOnFunction(llvm::Function &F) override;
+  virtual bool runOnModule(llvm::Module &m) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
 } // namespace smack

lib/smack/AnnotateLoopEnds.cpp

@@ -11,6 +11,7 @@
 #include "smack/AnnotateLoopEnds.h"
 #include "smack/Naming.h"
 #include "llvm/Analysis/LoopInfo.h"
+#include "llvm/Transforms/Utils.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/Dominators.h"
 #include "llvm/IR/IRBuilder.h"
@@ -29,27 +30,34 @@ using namespace llvm;
 
 // Register LoopInfo
 void AnnotateLoopEnds::getAnalysisUsage(AnalysisUsage &AU) const {
+  AU.addRequiredID(LoopSimplifyID);
   AU.addRequired<LoopInfoWrapperPass>();
 }
 
-void processExitingBlock(BasicBlock *block) {
+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";
 
+  Instruction& front = block->front();
+  insertLoopEndAssertion(le,&front);
 }
 
-void annotateLoopEnd(Loop *loop) {
+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.
-  SmallVector<BasicBlock *, 5> exitingBlocks; 
+  SmallVector<BasicBlock *, 5> exitBlocks; 
 
-  loop->getExitingBlocks(exitingBlocks);
+  loop->getExitBlocks(exitBlocks);
 
-  for (BasicBlock *b : exitingBlocks) {
-    processExitingBlock(b);
+  for (BasicBlock *b : exitBlocks) {
+    processExitBlock(b,le);
   } 
 
   // Handle subloops
@@ -58,16 +66,26 @@ void annotateLoopEnd(Loop *loop) {
   //}
 }
 
-bool AnnotateLoopEnds::runOnFunction(Function &F) {
-  if (F.isIntrinsic() || F.empty()) {
-    return false;
-  }
-  errs() << "Hello " << F.getName() << "\n";
-  LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>().getLoopInfo();
-  for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
-       LI != LIEnd; ++LI) {
-    errs() << "  Loop Found in " << F.getName() << "\n";
-    annotateLoopEnd(*LI);
+bool AnnotateLoopEnds::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";
+      annotateLoopEnd(*LI, le);
+    }
   }
 
   return true;

share/smack/lib/smack.c

@@ -1409,6 +1409,10 @@ void __SMACK_check_overflow(int flag) {
   __SMACK_code("assert {:overflow} @ == $0;", flag);
 }
 
+void __SMACK_loop_end(void) {
+  __SMACK_code("assert {:loopexit} false;");
+}
+
 char __VERIFIER_nondet_char(void) {
   char x = __SMACK_nondet_char();
   __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX);