From 92c1d97f9f2b224e2d4aad0f61bd8c66e726a5fa Mon Sep 17 00:00:00 2001 From: Vladislav Kalugin Date: Mon, 4 Sep 2023 12:31:17 +0300 Subject: [PATCH] Add annotation free --- include/klee/Core/MockBuilder.h | 1 + include/klee/Module/Annotation.h | 19 +++++++++++++ lib/Core/MockBuilder.cpp | 30 +++++++++++++++++++-- lib/Module/Annotation.cpp | 19 ++++++++++++- test/Feature/Annotation/Free.c | 45 +++++++++++++++++++++++++++++++ test/Feature/Annotation/Free.json | 31 +++++++++++++++++++++ 6 files changed, 142 insertions(+), 3 deletions(-) create mode 100644 test/Feature/Annotation/Free.c create mode 100644 test/Feature/Annotation/Free.json diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h index 7c788b705ad..72ddfed0014 100644 --- a/include/klee/Core/MockBuilder.h +++ b/include/klee/Core/MockBuilder.h @@ -60,6 +60,7 @@ class MockBuilder { std::unique_ptr 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); diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h index 448c74f913c..17a6b5fa9c3 100644 --- a/include/klee/Module/Annotation.h +++ b/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; bool operator==(const Ptr &first, const Ptr &second); } // namespace Statement diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 421231f482e..cb0ef96a19d 100644 --- a/lib/Core/MockBuilder.cpp +++ b/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,6 +436,15 @@ 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", @@ -442,7 +452,9 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs( 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 &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; } diff --git a/lib/Module/Annotation.cpp b/lib/Module/Annotation.cpp index 8063e0284f8..01ea95e54f4 100644 --- a/lib/Module/Annotation.cpp +++ b/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(std::stoi(rawValue)); + } +} + +Kind Free::getKind() const { return Kind::Free; } + const std::map 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(str); case Statement::Kind::AllocSource: return std::make_shared(str); + case Statement::Kind::Free: + return std::make_shared(str); } } diff --git a/test/Feature/Annotation/Free.c b/test/Feature/Annotation/Free.c new file mode 100644 index 00000000000..fb364a82644 --- /dev/null +++ b/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 + +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; +} diff --git a/test/Feature/Annotation/Free.json b/test/Feature/Annotation/Free.json new file mode 100644 index 00000000000..d8a9becf9d3 --- /dev/null +++ b/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": [] + } +}