[inprogress] free annotation

include/klee/Core/MockBuilder.h

@@ -60,9 +60,11 @@ 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);
+                       const Statement::InitNull *initNullPtr,
+                       const Statement::Free *freePtr);
 };
 
 } // namespace klee

include/klee/Module/Annotation.h

@@ -25,7 +25,9 @@ enum class Kind {
 
   Deref,
   InitNull,
+  // Maybe 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) {
@@ -418,6 +419,7 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
           break;
         }
         case Statement::Kind::AllocSource: {
+          // TODO:copy-paste can be replaced by template function
           if (prev != nullptr) {
             allocSourcePtr = (Statement::AllocSource *)statement.get();
           } else {
@@ -435,22 +437,35 @@ 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;
         }
       }
-
-      processingValue(prev, elem->getType(), allocSourcePtr, initNullPtr);
+      if (freePtr) {
+        buildFree(elem, freePtr);
+      }
+      processingValue(prev, elem->getType(), allocSourcePtr, initNullPtr,
+                      freePtr);
     }
   }
 }
 
 void MockBuilder::processingValue(llvm::Value *prev, llvm::Type *elemType,
                                   const Statement::AllocSource *allocSourcePtr,
-                                  const Statement::InitNull *initNullPtr) {
+                                  const Statement::InitNull *initNullPtr,
+                                  const Statement::Free *freePtr) {
   if (initNullPtr) {
     auto intType = llvm::IntegerType::get(mockModule->getContext(), 1);
     auto *allocCond = builder->CreateAlloca(intType, nullptr);
@@ -509,6 +524,28 @@ void MockBuilder::buildAllocSource(
   builder->CreateStore(mallocValue, prev);
 }
 
+// TODO copy-paste from buildAllocSource
+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 valueType = elemType->getPointerElementType();
+  //  auto sizeValue = llvm::ConstantInt::get(
+  //      mockModule->getContext(),
+  //      llvm::APInt(64,
+  //      mockModule->getDataLayout().getTypeStoreSize(valueType),
+  //                  false));
+  //  auto int8PtrTy = llvm::IntegerType::getInt64Ty(mockModule->getContext());
+  //  auto mallocInstr =
+  //      llvm::CallInst::CreateMalloc(builder->GetInsertBlock(), int8PtrTy,
+  //                                   valueType, sizeValue, nullptr, nullptr);
+  auto freeInstr = llvm::CallInst::CreateFree(elem, builder->GetInsertBlock());
+  //  auto mallocValue = builder->Insert(mallocInstr,
+  //  llvm::Twine("MallocValue")); builder->CreateStore(mallocValue, prev);
+  builder->Insert(freeInstr);
+}
+
 void MockBuilder::buildAnnotationForExternalFunctionReturn(
     llvm::Function *func, const std::vector<Statement::Ptr> &statements) {
   auto returnType = func->getReturnType();
@@ -517,6 +554,7 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
     return;
   }
 
+  // TODO change to set
   Statement::AllocSource *allocSourcePtr = nullptr;
   Statement::InitNull *initNullPtr = nullptr;
 
@@ -538,9 +576,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;
     }
@@ -571,7 +613,8 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
       builder->CreateCall(kleeAssumeFunc, {cmpResult64});
     }
   } else {
-    processingValue(retValuePtr, returnType, allocSourcePtr, initNullPtr);
+    processingValue(retValuePtr, returnType, allocSourcePtr, initNullPtr,
+                    nullptr);
   }
   llvm::Value *retValue = builder->CreateLoad(returnType, retValuePtr, retName);
   builder->CreateRet(retValue);

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,9 @@ 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,22 @@
+// 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
+
+
+// CHECK-FREE1: memory error: invalid pointer: free
+// CHECK-FREE1: KLEE: done: partially completed paths = 1
+// CHECK-FREE1: KLEE: done: generated tests = 2
+
+#include <assert.h>
+
+void maybeFree1(int *a);
+
+
+
+int main() {
+  int *a = malloc(sizeof(int));
+  maybeFree1(a);
+  maybeFree1(a);
+  return 0;
+}

test/Feature/Annotation/Free.json

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