Add a more consistent and sophisticated warning system

CMakeLists.txt

@@ -180,6 +180,7 @@ add_library(smackTranslator STATIC
   include/smack/NormalizeLoops.h
   include/smack/SplitAggregateValue.h
   include/smack/Prelude.h
+  include/smack/SmackWarnings.h
   lib/smack/AddTiming.cpp
   lib/smack/BoogieAst.cpp
   lib/smack/BplFilePrinter.cpp
@@ -203,6 +204,7 @@ add_library(smackTranslator STATIC
   lib/smack/NormalizeLoops.cpp
   lib/smack/SplitAggregateValue.cpp
   lib/smack/Prelude.cpp
+  lib/smack/SmackWarnings.cpp
 )
 
 add_executable(llvm2bpl

include/smack/SmackOptions.h

@@ -7,12 +7,15 @@
 
 #include "llvm/Support/CommandLine.h"
 
+#include "smack/SmackWarnings.h"
+
 namespace smack {
 class SmackOptions {
 public:
   static const llvm::cl::list<std::string> EntryPoints;
 
-  static const llvm::cl::opt<bool> Warnings;
+  static const llvm::cl::opt<SmackWarnings::WarningLevel> WarningLevel;
+  static const llvm::cl::opt<bool> ColoredWarnings;
 
   static const llvm::cl::opt<bool> MemoryModelDebug;
   static const llvm::cl::opt<bool> MemoryModelImpls;

include/smack/SmackRep.h

@@ -80,6 +80,7 @@ class SmackRep {
   const Stmt* store(unsigned R, const llvm::Type* T, const Expr* P, const Expr* V);
 
   const Expr* cast(unsigned opcode, const llvm::Value* v, const llvm::Type* t);
+  bool isFpArithOp(unsigned opcode);
   const Expr* bop(unsigned opcode, const llvm::Value* lhs, const llvm::Value* rhs, const llvm::Type* t);
   const Expr* cmp(unsigned predicate, const llvm::Value* lhs, const llvm::Value* rhs, bool isUnsigned);
 
@@ -127,6 +128,9 @@ class SmackRep {
   const Expr* cast(const llvm::Instruction* I);
   const Expr* cast(const llvm::ConstantExpr* CE);
 
+  bool isBitwiseOp(llvm::Instruction* I);
+  bool isFpArithOp(llvm::Instruction* I);
+
   const Expr* bop(const llvm::BinaryOperator* BO);
   const Expr* bop(const llvm::ConstantExpr* CE);
 

include/smack/SmackWarnings.h

@@ -0,0 +1,46 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+
+#ifndef SMACKWARNINGS_H
+#define SMACKWARNINGS_H
+
+#include "llvm/Support/CommandLine.h"
+#include "llvm/IR/Instruction.h"
+#include "smack/BoogieAst.h"
+
+#include <list>
+#include <initializer_list>
+
+namespace smack {
+
+class SmackWarnings {
+  typedef const llvm::cl::opt<bool> FlagT;
+  typedef std::initializer_list<const FlagT*> RequiredFlagsT;
+  typedef std::list<const FlagT*> UnsetFlagsT;
+
+public:
+  enum class WarningLevel: unsigned {
+    Silent=0,
+    Unsound=10, // Unhandled intrinsics, asm, etc
+    Info=20 // Memory length, etc.
+  };
+
+  static UnsetFlagsT getUnsetFlags(RequiredFlagsT flags);
+
+  // generate warnings about unsoundness
+  static void warnUnsound(std::string unmodeledOpName, Block* currBlock, const llvm::Instruction* i, bool ignore=false);
+  static void warnUnsound(std::string name, UnsetFlagsT unsetFlags, Block* currBlock, const llvm::Instruction* i, bool ignore=false);
+  static void warnIfUnsound(std::string name, RequiredFlagsT requiredFlags, Block* currBlock, const llvm::Instruction* i, bool ignore=false);
+  static void warnIfUnsound(std::string name, FlagT& requiredFlag, Block* currBlock, const llvm::Instruction* i);
+  static void warnIfUnsound(std::string name, FlagT& requiredFlag1, FlagT& requiredFlag2, Block* currBlock, const llvm::Instruction* i);
+
+  // generate warnings about memcpy/memset length/DSA
+  static void warnInfo(std::string info);
+private:
+  static bool isSufficientWarningLevel(WarningLevel level);
+  static std::string getFlagStr(UnsetFlagsT flags);
+};
+}
+
+#endif // SMACKWARNINGS_H

lib/DSA/DSMonitor.cpp

@@ -2,7 +2,8 @@
 #include "dsa/DSMonitor.h"
 #include "dsa/DSGraph.h"
 #include "llvm/IR/DebugInfo.h"
-#include "smack/SmackOptions.h"
+#include "llvm/Support/raw_ostream.h"
+#include "smack/SmackWarnings.h"
 
 #include <deque>
 
@@ -156,40 +157,42 @@ void DSMonitor::watch(DSNodeHandle N, std::vector<Value*> VS, std::string M) {
 }
 
 void DSMonitor::warn() {
-  if (!smack::SmackOptions::Warnings)
-    return;
+  std::string msg;
+  raw_string_ostream ss(msg);
 
   if (location != "")
-    errs() << location << ": ";
+    ss << location << ": ";
 
-  errs() << "warning: collapsing DSA node\n";
+  ss << "warning: collapsing DSA node\n";
 
   if (message != "")
-    errs() << message << "\n";
+    ss << message << "\n";
 
   if (VS.empty()) {
-    errs() << "(unknown value)" << "\n";
+    ss << "(unknown value)" << "\n";
 
   } else {
     if (Instruction *I = getInstruction(VS[0])) {
       if (BasicBlock *B = I->getParent()) {
         if (Function *F = B->getParent()) {
           if (F->hasName())
-            errs() << "in function:\n  " << F->getName() << "\n";
+            ss << "in function:\n  " << F->getName() << "\n";
         }
         if (B->hasName())
-          errs() << "in block:\n  " << I->getParent()->getName() << "\n";
+          ss << "in block:\n  " << I->getParent()->getName() << "\n";
       }
-      errs() << "at instruction:\n" << *I << "\n";
+      ss << "at instruction:\n" << *I << "\n";
     }
 
     for (auto V : VS)
-      errs() << "at value:\n" << *V << "\n";
+      ss << "at value:\n" << *V << "\n";
 
     if (caption != "")
-      errs() << "node:\n  " << caption << "\n";
+      ss << "node:\n  " << caption << "\n";
   }
-  errs() << "\n";
+  ss << "\n";
+
+  smack::SmackWarnings::warnInfo(ss.str());
 }
 
 void DSMonitor::witness(DSNodeHandle N, std::vector<Value*> VS, std::string M) {