[wip] AllocSource annotation support

Author: Columpio

include/klee/Module/Annotation.h

@@ -25,6 +25,15 @@ enum class Kind {
 
   Deref,
   InitNull,
+  AllocSource,
+};
+
+enum class AllocSourceKind {
+  MCREalloc = 1,    // malloc, calloc, realloc
+  New = 2,          // operator new
+  NewBrackets = 3,  // operator new[]
+  OpenFile = 4,     // open file (fopen, open)
+  MutexLock = 5     // mutex lock (pthread_mutex_lock)
 };
 
 enum class Property {
@@ -60,6 +69,12 @@ struct InitNull final : public Unknown {
   [[nodiscard]] Kind getKind() const override;
 };
 
+struct AllocSource final : public Unknown {
+  explicit AllocSource(std::string str);
+
+  [[nodiscard]] Kind getKind() const override;
+};
+
 using Ptr = std::shared_ptr<Unknown>;
 bool operator==(const Ptr &first, const Ptr &second);
 } // namespace Statement

lib/Core/MockBuilder.cpp

@@ -304,6 +304,8 @@ inline bool isCorrectStatements(const std::vector<Statement::Ptr> &statements,
                        case Statement::Kind::Deref:
                        case Statement::Kind::InitNull:
                          return argType->isPointerTy();
+                       case Statement::Kind::AllocSource:
+                        assert(false);
                        case Statement::Kind::Unknown:
                        default:
                          return true;
@@ -395,6 +397,8 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
 
         break;
       }
+      case Statement::Kind::AllocSource:
+        assert(false);
       case Statement::Kind::InitNull:
       case Statement::Kind::Unknown:
       default:

lib/Module/Annotation.cpp

@@ -86,8 +86,15 @@ InitNull::InitNull(std::string str) : Unknown(std::move(str)) {}
 
 Kind InitNull::getKind() const { return Kind::InitNull; }
 
+AllocSource::AllocSource(std::string str) : Unknown(std::move(str)) {}
+
+Kind AllocSource::getKind() const { return Kind::AllocSource; }
+
 const std::map<std::string, Statement::Kind> StringToKindMap = {
-    {"deref", Statement::Kind::Deref}, {"initnull", Statement::Kind::InitNull}};
+    {"deref", Statement::Kind::Deref},
+    {"initnull", Statement::Kind::InitNull},
+    {"allocsource", Statement::Kind::AllocSource}
+};
 
 inline Statement::Kind stringToKind(const std::string &str) {
   auto it = StringToKindMap.find(toLower(str));
@@ -106,6 +113,8 @@ Ptr stringToKindPtr(const std::string &str) {
     return std::make_shared<Deref>(str);
   case Statement::Kind::InitNull:
     return std::make_shared<InitNull>(str);
+  case Statement::Kind::AllocSource:
+    return std::make_shared<AllocSource>(str);
   }
 }
 
@@ -268,6 +277,9 @@ AnnotationsMap parseAnnotationsXml(const pugi::xml_document &annotationsXml,
           }
           break;
         }
+        case Statement::Kind::AllocSource: {
+          assert(false);
+        }
         case Statement::Kind::Unknown:
           break;
         }