[WIP] Add annotation free

include/klee/Core/MockBuilder.h

@@ -60,6 +60,7 @@ class MockBuilder {
   std::unique_ptr<llvm::Module> build();
   void buildAllocSource(llvm::Value *prev, llvm::Type *elemType,
                         const Statement::AllocSource *allocSourcePtr);
+  void buildFree(llvm::Value *elem, const Statement::Free *freePtr);
   void processingValue(llvm::Value *prev, llvm::Type *elemType,
                        const Statement::AllocSource *allocSourcePtr,
                        const Statement::InitNull *initNullPtr);

include/klee/Module/Annotation.h

@@ -25,7 +25,9 @@ enum class Kind {
 
   Deref,
   InitNull,
+  // TODO: rename to alloc
   AllocSource,
+  Free
 };
 
 enum class Property {
@@ -83,6 +85,23 @@ struct AllocSource final : public Unknown {
   [[nodiscard]] Kind getKind() const override;
 };
 
+struct Free final : public Unknown {
+public:
+  enum Type {
+    Free_ = 1,           // Kind of free function
+    Delete = 2,         // operator delete
+    DeleteBrackets = 3, // operator delete[]
+    CloseFile = 4,      // close file
+    MutexUnlock = 5     // mutex unlock (pthread_mutex_unlock)
+  };
+
+  Type value;
+
+  explicit Free(const std::string &str = "FreeSource::1");
+
+  [[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

@@ -381,6 +381,7 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
       auto [prev, elem] = goByOffset(arg, offset);
 
       Statement::AllocSource *allocSourcePtr = nullptr;
+      Statement::Free *freePtr = nullptr;
       Statement::InitNull *initNullPtr = nullptr;
 
       for (const auto &statement : statementsOffset) {
@@ -435,14 +436,25 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
           }
           break;
         }
+        case Statement::Kind::Free: {
+          if (elem->getType()->isPointerTy()) {
+            freePtr = (Statement::Free *)statement.get();
+          } else {
+            klee_message("Annotation: not valid annotation %s",
+                         statement->toString().c_str());
+          }
+          break;
+        }
         case Statement::Kind::Unknown:
         default:
           klee_message("Annotation not implemented %s",
                        statement->toString().c_str());
           break;
         }
       }
-
+      if (freePtr) {
+        buildFree(elem, freePtr);
+      }
       processingValue(prev, elem->getType(), allocSourcePtr, initNullPtr);
     }
   }
@@ -509,6 +521,15 @@ void MockBuilder::buildAllocSource(
   builder->CreateStore(mallocValue, prev);
 }
 
+void MockBuilder::buildFree(llvm::Value *elem, const Statement::Free *freePtr) {
+  if (freePtr->value != Statement::Free::Free_) {
+    klee_warning("Annotation: AllocSource \"%d\" not implemented use free",
+                 freePtr->value);
+  }
+  auto freeInstr = llvm::CallInst::CreateFree(elem, builder->GetInsertBlock());
+  builder->Insert(freeInstr);
+}
+
 void MockBuilder::buildAnnotationForExternalFunctionReturn(
     llvm::Function *func, const std::vector<Statement::Ptr> &statements) {
   auto returnType = func->getReturnType();
@@ -517,6 +538,7 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
     return;
   }
 
+  // TODO: change to set
   Statement::AllocSource *allocSourcePtr = nullptr;
   Statement::InitNull *initNullPtr = nullptr;
 
@@ -538,9 +560,13 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
                         : nullptr;
       break;
     }
+    case Statement::Kind::Free: {
+      klee_warning("Annotation: unused \"Free\" for return");
+      break;
+    }
     case Statement::Kind::Unknown:
     default:
-      klee_message("Annotation not implemented %s",
+      klee_message("Annotation: not implemented %s",
                    statement->toString().c_str());
       break;
     }

lib/Module/Annotation.cpp

@@ -116,10 +116,25 @@ AllocSource::AllocSource(const std::string &str) : Unknown(str) {
 
 Kind AllocSource::getKind() const { return Kind::AllocSource; }
 
+Free::Free(const std::string &str) : Unknown(str) {
+  if (!std::all_of(rawValue.begin(), rawValue.end(), isdigit)) {
+    klee_error("Annotation: Incorrect value format \"%s\"", rawValue.c_str());
+  }
+  if (rawValue.empty()) {
+    value = Free::Type::Free_;
+  } else {
+    value = static_cast<Type>(std::stoi(rawValue));
+  }
+}
+
+Kind Free::getKind() const { return Kind::Free; }
+
 const std::map<std::string, Statement::Kind> StringToKindMap = {
     {"deref", Statement::Kind::Deref},
     {"initnull", Statement::Kind::InitNull},
-    {"allocsource", Statement::Kind::AllocSource}};
+    {"allocsource", Statement::Kind::AllocSource},
+    {"freesource", Statement::Kind::Free},
+    {"freesink", Statement::Kind::Free}};
 
 inline Statement::Kind stringToKind(const std::string &str) {
   auto it = StringToKindMap.find(toLower(str));
@@ -140,6 +155,8 @@ Ptr stringToKindPtr(const std::string &str) {
     return std::make_shared<InitNull>(str);
   case Statement::Kind::AllocSource:
     return std::make_shared<AllocSource>(str);
+  case Statement::Kind::Free:
+    return std::make_shared<Free>(str);
   }
 }
 

test/Feature/Annotation/Free.c

@@ -0,0 +1,45 @@
+// REQUIRES: z3
+// RUN: %clang -DFree1 %s -g -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t1.klee-out-1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE1
+
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t1.klee-out-1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE2
+
+// RUN: %clang -DFree3 %s -g -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t1.klee-out-1
+// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE3
+
+#include <assert.h>
+
+int *maybeAllocSource1();
+void maybeFree1(int *a);
+
+int main() {
+  int *a;
+#ifdef Free1
+  // CHECK-FREE1: memory error: invalid pointer: free
+  // CHECK-FREE1: KLEE: done: completed paths = 1
+  // CHECK-FREE1: KLEE: done: partially completed paths = 1
+  // CHECK-FREE1: KLEE: done: generated tests = 2
+  a = malloc(sizeof(int));
+  maybeFree1(a);
+  maybeFree1(a);
+#endif
+
+  a = maybeAllocSource1();
+  maybeFree1(a);
+  // CHECK-NOT-FREE2: memory error: invalid pointer: free
+  // CHECK-FREE2: KLEE: done: completed paths = 1
+  // CHECK-FREE2: KLEE: done: partially completed paths = 0
+  // CHECK-FREE2: KLEE: done: generated tests = 1
+#ifdef Free3
+  // CHECK-FREE3: memory error: invalid pointer: free
+  // CHECK-FREE3: KLEE: done: completed paths = 0
+  // CHECK-FREE3: KLEE: done: partially completed paths = 1
+  // CHECK-FREE3: KLEE: done: generated tests = 1
+  maybeFree1(a);
+#endif
+  return 0;
+}

test/Feature/Annotation/Free.json

@@ -0,0 +1,31 @@
+{
+  "maybeFree1": {
+    "name": "maybeFree1",
+    "annotation": [
+      [],
+      [
+        "FreeSink::1"
+      ]
+    ],
+    "properties": []
+  },
+  "maybeFree2": {
+    "name": "maybeFree2",
+    "annotation": [
+      [],
+      [
+        "FreeSink:*:1"
+      ]
+    ],
+    "properties": []
+  },
+  "maybeAllocSource1": {
+    "name": "maybeAllocSource1",
+    "annotation": [
+      [
+        "AllocSource::1"
+      ]
+    ],
+    "properties": []
+  }
+}