Skip to content

Commit

Permalink
Split InitNull to InitNull and MaybeInitNull
Browse files Browse the repository at this point in the history
  • Loading branch information
@ladisgin
ladisgin committed Nov 28, 2023
1 parent 6bc15d7 commit d898c1a
Show file tree
Hide file tree
Showing 8 changed files with 76 additions and 64 deletions.
2 changes: 1 addition & 1 deletion include/klee/Core/MockBuilder.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
15 changes: 8 additions & 7 deletions include/klee/Module/Annotation.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ enum class Kind {

Deref,
InitNull,
MaybeInitNull,
// TODO: rename to alloc
AllocSource,
Free
Expand Down Expand Up @@ -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;
};
Expand Down Expand Up @@ -127,7 +128,7 @@ struct Annotation {
using AnnotationsMap = std::map<std::string, Annotation>;

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
30 changes: 18 additions & 12 deletions lib/Core/MockBuilder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ MockBuilder::MockBuilder(
interpreterHandler(interpreterHandler),
mainModuleFunctions(mainModuleFunctions),
mainModuleGlobals(mainModuleGlobals) {
annotations = parseAnnotations(opts.AnnotationsFile, userModule);
annotations = parseAnnotations(opts.AnnotationsFile);
}

std::unique_ptr<llvm::Module> MockBuilder::build() {
Expand Down Expand Up @@ -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<Statement::InitNull>()});
func, {std::make_shared<Statement::MaybeInitNull>()});
}
}
}
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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()) {
Expand All @@ -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: {
Expand All @@ -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 =
Expand Down
35 changes: 20 additions & 15 deletions lib/Module/Annotation.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,22 +91,14 @@ Deref::Deref(const std::string &str) : Unknown(str) {}

Kind Deref::getKind() const { return Kind::Deref; }

const std::map<std::string, InitNull::Type> 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());
Expand All @@ -132,6 +124,7 @@ Kind Free::getKind() const { return Kind::Free; }
const std::map<std::string, Statement::Kind> 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}};
Expand All @@ -153,6 +146,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::MaybeInitNull:
return std::make_shared<MaybeInitNull>(str);
case Statement::Kind::AllocSource:
return std::make_shared<Alloc>(str);
case Statement::Kind::Free:
Expand Down Expand Up @@ -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<Statement::Ptr> &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<std::vector<Statement::Ptr>>(tmp.begin() + 1, tmp.end());
}
Expand All @@ -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 {};
}
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/Annotation/General.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
"name": "ptrRet",
"annotation": [
[
"InitNull",
"MaybeInitNull",
"AllocSource::1"
]
],
Expand Down
30 changes: 15 additions & 15 deletions test/Feature/Annotation/InitNull.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 <assert.h>

#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
Expand Down
22 changes: 11 additions & 11 deletions test/Feature/Annotation/InitNull.json
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"maybeInitNull1": {
"mustInitNull1": {
"name": "maybeInitNull1",
"annotation": [
[],
Expand All @@ -9,7 +9,7 @@
],
"properties": []
},
"maybeInitNull2": {
"mustInitNull2": {
"name": "maybeInitNull2",
"annotation": [
[],
Expand All @@ -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": []
Expand Down
4 changes: 2 additions & 2 deletions unittests/Annotations/AnnotationsTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
Expand Down

0 comments on commit d898c1a

Please sign in to comment.