diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h index 73ff27fbc0..34ddb081d7 100644 --- a/include/klee/Core/MockBuilder.h +++ b/include/klee/Core/MockBuilder.h @@ -70,7 +70,7 @@ class MockBuilder { void buildFree(llvm::Value *elem, const Statement::Free *freePtr); void processingValue(llvm::Value *prev, llvm::Type *elemType, const Statement::Alloc *allocSourcePtr, - const Statement::InitNull *initNullPtr); + bool initNullPtr); }; } // namespace klee diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h index c51c0172ff..96b60949b2 100644 --- a/include/klee/Module/Annotation.h +++ b/include/klee/Module/Annotation.h @@ -25,6 +25,7 @@ enum class Kind { Deref, InitNull, + MaybeInitNull, // TODO: rename to alloc AllocSource, Free @@ -64,14 +65,14 @@ struct Deref final : public Unknown { struct InitNull final : public Unknown { public: - enum Type { - MAYBE, // Return value which maybe Null - MUST // Create two branch one with Null second nonNull valu - }; + explicit InitNull(const std::string &str = "InitNull"); - Type value = InitNull::Type::MAYBE; + [[nodiscard]] Kind getKind() const override; +}; - explicit InitNull(const std::string &str = "InitNull"); +struct MaybeInitNull final : public Unknown { +public: + explicit MaybeInitNull(const std::string &str = "MaybeInitNull"); [[nodiscard]] Kind getKind() const override; }; @@ -127,7 +128,7 @@ struct Annotation { using AnnotationsMap = std::map; AnnotationsMap parseAnnotationsJson(const json &annotationsJson); -AnnotationsMap parseAnnotations(const std::string &path, const llvm::Module *m); +AnnotationsMap parseAnnotations(const std::string &path); } // namespace klee #endif // KLEE_ANNOTATION_H diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index e923097c52..b2b4d37531 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -70,7 +70,7 @@ MockBuilder::MockBuilder( interpreterHandler(interpreterHandler), mainModuleFunctions(mainModuleFunctions), mainModuleGlobals(mainModuleGlobals) { - annotations = parseAnnotations(opts.AnnotationsFile, userModule); + annotations = parseAnnotations(opts.AnnotationsFile); } std::unique_ptr MockBuilder::build() { @@ -227,7 +227,7 @@ void MockBuilder::buildExternalFunctionsDefinitions() { klee_message("Mocking external function %s", extName.c_str()); // Default annotation for externals return buildAnnotationForExternalFunctionReturn( - func, {std::make_shared()}); + func, {std::make_shared()}); } } } @@ -476,7 +476,7 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs( void MockBuilder::processingValue(llvm::Value *prev, llvm::Type *elemType, const Statement::Alloc *allocSourcePtr, - const Statement::InitNull *initNullPtr) { + bool initNullPtr) { if (initNullPtr) { auto intType = llvm::IntegerType::get(mockModule->getContext(), 1); auto *allocCond = builder->CreateAlloca(intType, nullptr); @@ -552,7 +552,8 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn( } Statement::Alloc *allocSourcePtr = nullptr; - Statement::InitNull *initNullPtr = nullptr; + Statement::InitNull *mustInitNull = nullptr; + Statement::MaybeInitNull *maybeInitNull = nullptr; for (const auto &statement : statements) { switch (statement->getKind()) { @@ -567,9 +568,15 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn( break; } case Statement::Kind::InitNull: { - initNullPtr = returnType->isPointerTy() - ? (Statement::InitNull *)statement.get() - : nullptr; + mustInitNull = returnType->isPointerTy() + ? (Statement::InitNull *)statement.get() + : nullptr; + break; + } + case Statement::Kind::MaybeInitNull: { + maybeInitNull = returnType->isPointerTy() + ? (Statement::MaybeInitNull *)statement.get() + : nullptr; break; } case Statement::Kind::Free: { @@ -586,14 +593,13 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn( std::string retName = "ret_" + func->getName().str(); llvm::Value *retValuePtr = builder->CreateAlloca(returnType, nullptr); - bool mustBeNull = - initNullPtr && initNullPtr->value == Statement::InitNull::Type::MUST; - if (returnType->isPointerTy() && (allocSourcePtr || mustBeNull)) { - processingValue(retValuePtr, returnType, allocSourcePtr, initNullPtr); + if (returnType->isPointerTy() && (allocSourcePtr || mustInitNull)) { + processingValue(retValuePtr, returnType, allocSourcePtr, + mustInitNull || maybeInitNull); } else { buildCallKleeMakeSymbolic("klee_make_mock", retValuePtr, returnType, func->getName().str()); - if (returnType->isPointerTy() && !initNullPtr) { + if (returnType->isPointerTy() && !maybeInitNull) { llvm::Value *retValue = builder->CreateLoad(returnType, retValuePtr, retName); auto cmpResult = diff --git a/lib/Module/Annotation.cpp b/lib/Module/Annotation.cpp index 26b46ed8d4..defd65b5c1 100644 --- a/lib/Module/Annotation.cpp +++ b/lib/Module/Annotation.cpp @@ -91,22 +91,14 @@ Deref::Deref(const std::string &str) : Unknown(str) {} Kind Deref::getKind() const { return Kind::Deref; } -const std::map initNullTypeMap = { - {"maybe", InitNull::Type::MAYBE}, {"must", InitNull::Type::MUST}}; - -InitNull::InitNull(const std::string &str) : Unknown(str) { - if (!rawValue.empty()) { - auto val = initNullTypeMap.find(toLower(rawValue)); - if (val != initNullTypeMap.end()) { - value = val->second; - } else { - klee_error("Annotation: Incorrect value \"%s\"", rawValue.c_str()); - } - } -} +InitNull::InitNull(const std::string &str) : Unknown(str) {} Kind InitNull::getKind() const { return Kind::InitNull; } +MaybeInitNull::MaybeInitNull(const std::string &str) : Unknown(str) {} + +Kind MaybeInitNull::getKind() const { return Kind::MaybeInitNull; } + Alloc::Alloc(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()); @@ -132,6 +124,7 @@ Kind Free::getKind() const { return Kind::Free; } const std::map StringToKindMap = { {"deref", Statement::Kind::Deref}, {"initnull", Statement::Kind::InitNull}, + {"maybeinitnull", Statement::Kind::MaybeInitNull}, {"allocsource", Statement::Kind::AllocSource}, {"freesource", Statement::Kind::Free}, {"freesink", Statement::Kind::Free}}; @@ -153,6 +146,8 @@ Ptr stringToKindPtr(const std::string &str) { return std::make_shared(str); case Statement::Kind::InitNull: return std::make_shared(str); + case Statement::Kind::MaybeInitNull: + return std::make_shared(str); case Statement::Kind::AllocSource: return std::make_shared(str); case Statement::Kind::Free: @@ -230,6 +225,17 @@ AnnotationsMap parseAnnotationsJson(const json &annotationsJson) { annotation.functionName.c_str()); } annotation.returnStatements = tmp[0]; + if (std::any_of(tmp.begin() + 1, tmp.end(), + [](const std::vector &statements) { + return std::any_of( + statements.begin() + 1, statements.end(), + [](const Statement::Ptr &statement) { + return statement->getKind() == + Statement::Kind::MaybeInitNull; + }); + })) { + klee_error("Annotation: MaybeInitNull can annotate only return value"); + } annotation.argsStatements = std::vector>(tmp.begin() + 1, tmp.end()); } @@ -241,8 +247,7 @@ AnnotationsMap parseAnnotationsJson(const json &annotationsJson) { return annotations; } -AnnotationsMap parseAnnotations(const std::string &path, - const llvm::Module *m) { +AnnotationsMap parseAnnotations(const std::string &path) { if (path.empty()) { return {}; } diff --git a/test/Feature/Annotation/General.json b/test/Feature/Annotation/General.json index 606550656f..65cffd2fbf 100644 --- a/test/Feature/Annotation/General.json +++ b/test/Feature/Annotation/General.json @@ -15,7 +15,7 @@ "name": "ptrRet", "annotation": [ [ - "InitNull", + "MaybeInitNull", "AllocSource::1" ] ], diff --git a/test/Feature/Annotation/InitNull.c b/test/Feature/Annotation/InitNull.c index cf9ab35a88..ccf34ec2da 100644 --- a/test/Feature/Annotation/InitNull.c +++ b/test/Feature/Annotation/InitNull.c @@ -22,56 +22,56 @@ // CHECK-EMPTY: ASSERTION FAIL: a != 0 && "A is Null" // CHECK-EMPTY: partially completed paths = 2 -// RUN: %clang -DMustInitNull %s -g -emit-llvm %O0opt -c -o %t6.bc +// RUN: %clang -DMustInitNull5 %s -g -emit-llvm %O0opt -c -o %t6.bc // RUN: rm -rf %t6.klee-out-1 -// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-MUSTINITNULL +// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL5 #include #ifdef InitNull1 -void maybeInitNull1(int *a); +void mustInitNull1(int *a); #endif -void maybeInitNull2(int **a); -int *maybeInitNull3(); -int **maybeInitNull4(); +void mustInitNull2(int **a); +int *maybeInitNull1(); +int **maybeInitNull2(); -int *mustInitNull(); +int *mustInitNull3(); int main() { int c = 42; int *a = &c; #ifdef InitNull1 // CHECK-INITNULL1: not valid annotation - maybeInitNull1(a); + mustInitNull1(a); // CHECK-INITNULL1-NOT: A is Null // CHECK-INITNULL1: partially completed paths = 0 // CHECK-INITNULL1: generated tests = 1 #endif #ifdef InitNull2 - maybeInitNull2(&a); + mustInitNull2(&a); // CHECK-INITNULL2: ASSERTION FAIL: a != 0 && "A is Null" // CHECK-INITNULL2: partially completed paths = 1 // CHECK-INITNULL2: generated tests = 2 #endif #ifdef InitNull3 - a = maybeInitNull3(); + a = maybeInitNull1(); // CHECK-INITNULL3: ASSERTION FAIL: a != 0 && "A is Null" // CHECK-INITNULL3: partially completed paths = 1 // CHECK-INITNULL3: generated tests = 2 #endif #ifdef InitNull4 - a = *maybeInitNull4(); + a = *maybeInitNull2(); // CHECK-INITNULL4: ASSERTION FAIL: a != 0 && "A is Null" // CHECK-INITNULL4: partially completed paths = 3 #endif -#ifdef MustInitNull - a = mustInitNull(); - // CHECK-MUSTINITNULL: partially completed paths = 0 - // CHECK-MUSTINITNULL: generated tests = 2 +#ifdef MustInitNull5 + a = mustInitNull3(); + // CHECK-INITNULL5: partially completed paths = 0 + // CHECK-INITNULL5: generated tests = 2 #else assert(a != 0 && "A is Null"); #endif diff --git a/test/Feature/Annotation/InitNull.json b/test/Feature/Annotation/InitNull.json index 963524347a..270c7f01d1 100644 --- a/test/Feature/Annotation/InitNull.json +++ b/test/Feature/Annotation/InitNull.json @@ -1,5 +1,5 @@ { - "maybeInitNull1": { + "mustInitNull1": { "name": "maybeInitNull1", "annotation": [ [], @@ -9,7 +9,7 @@ ], "properties": [] }, - "maybeInitNull2": { + "mustInitNull2": { "name": "maybeInitNull2", "annotation": [ [], @@ -19,29 +19,29 @@ ], "properties": [] }, - "maybeInitNull3": { - "name": "maybeInitNull3", + "maybeInitNull1": { + "name": "maybeInitNull1", "annotation": [ [ - "InitNull" + "MaybeInitNull" ] ], "properties": [] }, - "maybeInitNull4": { - "name": "maybeInitNull4", + "maybeInitNull2": { + "name": "maybeInitNull2", "annotation": [ [ - "InitNull:*" + "MaybeInitNull:*" ] ], "properties": [] }, - "mustInitNull": { - "name": "mustInitNull", + "mustInitNull3": { + "name": "mustInitNull3", "annotation": [ [ - "InitNull::Must" + "InitNull" ] ], "properties": [] diff --git a/unittests/Annotations/AnnotationsTest.cpp b/unittests/Annotations/AnnotationsTest.cpp index b48bcf7004..4fbe599dab 100644 --- a/unittests/Annotations/AnnotationsTest.cpp +++ b/unittests/Annotations/AnnotationsTest.cpp @@ -86,14 +86,14 @@ TEST(AnnotationsTest, KnownAnnotations) { const json j = json::parse(R"( { "foo" : { - "annotation" : [["InitNull"], ["Deref", "InitNull"]], + "annotation" : [["MaybeInitNull"], ["Deref", "InitNull"]], "properties" : [] } } )"); const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(actual.at("foo").returnStatements[0]->getKind(), - Statement::Kind::InitNull); + Statement::Kind::MaybeInitNull); ASSERT_EQ(actual.at("foo").argsStatements[0][0]->getKind(), Statement::Kind::Deref); ASSERT_EQ(actual.at("foo").argsStatements[0][1]->getKind(),