Skip to content

Commit cb4a318

Browse files
mamaria-kladisgin
mamaria-k
authored and
ladisgin
committed
Add annotations json parser
1 parent 8999685 commit cb4a318

File tree

12 files changed

+486
-8
lines changed

12 files changed

+486
-8
lines changed

‎include/klee/Core/Interpreter.h‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
#define KLEE_INTERPRETER_H
1111

1212
#include "TerminationTypes.h"
13+
#include "klee/Module/Annotation.h"
1314

1415
#include "klee/Module/SarifReport.h"
1516

@@ -157,7 +158,8 @@ class Interpreter {
157158
const std::unordered_set<std::string> &mainModuleFunctions,
158159
const std::unordered_set<std::string> &mainModuleGlobals,
159160
std::unique_ptr<InstructionInfoTable> origInfos,
160-
const std::set<std::string> &ignoredExternals) = 0;
161+
const std::set<std::string> &ignoredExternals,
162+
const Annotations &annotations) = 0;
161163

162164
virtual std::map<std::string, llvm::Type *>
163165
getAllExternals(const std::set<std::string> &ignoredExternals) = 0;

‎include/klee/Core/MockBuilder.h‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#ifndef KLEE_MOCKBUILDER_H
22
#define KLEE_MOCKBUILDER_H
33

4+
#include "klee/Module/Annotation.h"
5+
46
#include "llvm/IR/IRBuilder.h"
57
#include "llvm/IR/Module.h"
68

@@ -15,6 +17,7 @@ class MockBuilder {
1517
std::unique_ptr<llvm::Module> mockModule;
1618
std::unique_ptr<llvm::IRBuilder<>> builder;
1719
std::map<std::string, llvm::Type *> externals;
20+
Annotations annotations;
1821

1922
const std::string mockEntrypoint, userEntrypoint;
2023

@@ -25,11 +28,16 @@ class MockBuilder {
2528
void buildCallKleeMakeSymbol(const std::string &klee_function_name,
2629
llvm::Value *source, llvm::Type *type,
2730
const std::string &symbol_name);
31+
void buildAnnotationForExternalFunctionParams(llvm::Function *func,
32+
Annotation &annotation);
33+
llvm::Value *goByOffset(llvm::Value *value,
34+
const std::vector<std::string> &offset);
2835

2936
public:
3037
MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
3138
std::string userEntrypoint,
32-
std::map<std::string, llvm::Type *> externals);
39+
std::map<std::string, llvm::Type *> externals,
40+
Annotations annotations);
3341

3442
std::unique_ptr<llvm::Module> build();
3543
};

‎include/klee/Module/Annotation.h‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
#ifndef KLEE_ANNOTATION_H
2+
#define KLEE_ANNOTATION_H
3+
4+
#include "map"
5+
#include "set"
6+
#include "string"
7+
#include "vector"
8+
9+
#include "nlohmann/json.hpp"
10+
#include "nonstd/optional.hpp"
11+
12+
using nonstd::nullopt;
13+
using nonstd::optional;
14+
using json = nlohmann::json;
15+
16+
namespace klee {
17+
18+
// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
19+
struct Annotation {
20+
enum class StatementKind {
21+
Unknown,
22+
23+
Deref,
24+
InitNull,
25+
};
26+
27+
enum class Property {
28+
Unknown,
29+
30+
Determ,
31+
Noreturn,
32+
};
33+
34+
struct StatementUnknown {
35+
explicit StatementUnknown(const std::string &str);
36+
virtual ~StatementUnknown();
37+
38+
virtual Annotation::StatementKind getStatementName() const;
39+
virtual bool operator==(const StatementUnknown &other) const;
40+
41+
std::string statementStr;
42+
std::vector<std::string> offset;
43+
44+
protected:
45+
void parseOffset(const std::string &offsetStr);
46+
void parseOnlyOffset(const std::string &str);
47+
};
48+
49+
struct StatementDeref final : public StatementUnknown {
50+
explicit StatementDeref(const std::string &str);
51+
52+
Annotation::StatementKind getStatementName() const override;
53+
};
54+
55+
struct StatementInitNull final : public StatementUnknown {
56+
explicit StatementInitNull(const std::string &str);
57+
58+
Annotation::StatementKind getStatementName() const override;
59+
};
60+
61+
using StatementPtr = std::shared_ptr<StatementUnknown>;
62+
using StatementPtrs = std::vector<StatementPtr>;
63+
64+
bool operator==(const Annotation &other) const;
65+
66+
std::string functionName;
67+
std::vector<StatementPtrs> statements;
68+
std::set<Property> properties;
69+
};
70+
71+
using Annotations = std::map<std::string, Annotation>;
72+
73+
const std::map<std::string, Annotation::Property> toProperties{
74+
{"determ", Annotation::Property::Determ},
75+
{"noreturn", Annotation::Property::Noreturn},
76+
};
77+
78+
Annotations parseAnnotationsFile(const json &annotationsJson);
79+
Annotations parseAnnotationsFile(const std::string &path);
80+
81+
bool operator==(const Annotation::StatementPtr &first,
82+
const Annotation::StatementPtr &second);
83+
84+
} // namespace klee
85+
86+
#endif // KLEE_ANNOTATION_H

‎lib/Core/Executor.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -537,7 +537,8 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
537537
const std::unordered_set<std::string> &mainModuleFunctions,
538538
const std::unordered_set<std::string> &mainModuleGlobals,
539539
std::unique_ptr<InstructionInfoTable> origInfos,
540-
const std::set<std::string> &ignoredExternals) {
540+
const std::set<std::string> &ignoredExternals,
541+
const Annotations &annotations) {
541542
assert(!kmodule && !userModules.empty() &&
542543
"can only register one module"); // XXX gross
543544

@@ -582,7 +583,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
582583
std::map<std::string, llvm::Type *> externals =
583584
getAllExternals(ignoredExternals);
584585
MockBuilder builder(kmodule->module.get(), opts.MainCurrentName,
585-
opts.MainNameAfterMock, externals);
586+
opts.MainNameAfterMock, externals, annotations);
586587
std::unique_ptr<llvm::Module> mockModule = builder.build();
587588
if (!mockModule) {
588589
klee_error("Unable to generate mocks");

‎lib/Core/Executor.h‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -733,7 +733,8 @@ class Executor : public Interpreter {
733733
const std::unordered_set<std::string> &mainModuleFunctions,
734734
const std::unordered_set<std::string> &mainModuleGlobals,
735735
std::unique_ptr<InstructionInfoTable> origInfos,
736-
const std::set<std::string> &ignoredExternals) override;
736+
const std::set<std::string> &ignoredExternals,
737+
const Annotations &annotations) override;
737738

738739
std::map<std::string, llvm::Type *>
739740
getAllExternals(const std::set<std::string> &ignoredExternals) override;

‎lib/Core/MockBuilder.cpp‎

Lines changed: 73 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,21 @@
11
#include "klee/Core/MockBuilder.h"
22

3+
#include "klee/Module/Annotation.h"
34
#include "klee/Support/ErrorHandling.h"
45
#include "llvm/IR/IRBuilder.h"
56
#include "llvm/IR/Module.h"
67

78
#include <memory>
9+
#include <utility>
810

911
namespace klee {
1012

1113
MockBuilder::MockBuilder(const llvm::Module *initModule,
1214
std::string mockEntrypoint, std::string userEntrypoint,
13-
std::map<std::string, llvm::Type *> externals)
15+
std::map<std::string, llvm::Type *> externals,
16+
Annotations annotations)
1417
: userModule(initModule), externals(std::move(externals)),
18+
annotations(std::move(annotations)),
1519
mockEntrypoint(std::move(mockEntrypoint)),
1620
userEntrypoint(std::move(userEntrypoint)) {}
1721

@@ -115,6 +119,11 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
115119
continue;
116120
}
117121

122+
const auto annotation = annotations.find(extName);
123+
if (annotation != annotations.end()) {
124+
buildAnnotationForExternalFunctionParams(func, annotation->second);
125+
}
126+
118127
auto *mockReturnValue =
119128
builder->CreateAlloca(func->getReturnType(), nullptr);
120129
buildCallKleeMakeSymbol("klee_make_mock", mockReturnValue,
@@ -149,4 +158,67 @@ void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name,
149158
gep});
150159
}
151160

161+
// TODO: add method for return value of external functions.
162+
void MockBuilder::buildAnnotationForExternalFunctionParams(
163+
llvm::Function *func, Annotation &annotation) {
164+
for (size_t i = 1; i < annotation.statements.size(); i++) {
165+
const auto arg = func->getArg(i - 1);
166+
for (const auto &statement : annotation.statements[i]) {
167+
llvm::Value *elem = goByOffset(arg, statement->offset);
168+
switch (statement->getStatementName()) {
169+
case Annotation::StatementKind::Deref: {
170+
if (!elem->getType()->isPointerTy()) {
171+
klee_error("Incorrect annotation offset.");
172+
}
173+
builder->CreateLoad(elem);
174+
break;
175+
}
176+
case Annotation::StatementKind::InitNull: {
177+
// TODO
178+
}
179+
case Annotation::StatementKind::Unknown:
180+
default:
181+
__builtin_unreachable();
182+
}
183+
}
184+
}
185+
186+
for (const auto &property : annotation.properties) {
187+
switch (property) {
188+
case Annotation::Property::Determ: {
189+
// TODO
190+
}
191+
case Annotation::Property::Noreturn: {
192+
// TODO
193+
}
194+
case Annotation::Property::Unknown:
195+
default:
196+
__builtin_unreachable();
197+
}
198+
}
199+
}
200+
201+
llvm::Value *MockBuilder::goByOffset(llvm::Value *value,
202+
const std::vector<std::string> &offset) {
203+
llvm::Value *current = value;
204+
for (const auto &inst : offset) {
205+
if (inst == "*") {
206+
if (!current->getType()->isPointerTy()) {
207+
klee_error("Incorrect annotation offset.");
208+
}
209+
current = builder->CreateLoad(current);
210+
} else if (inst == "&") {
211+
auto addr = builder->CreateAlloca(current->getType());
212+
current = builder->CreateStore(current, addr);
213+
} else {
214+
const size_t index = std::stol(inst);
215+
if (!(current->getType()->isPointerTy() || current->getType()->isArrayTy())) {
216+
klee_error("Incorrect annotation offset.");
217+
}
218+
current = builder->CreateConstInBoundsGEP1_64(current, index);
219+
}
220+
}
221+
return current;
222+
}
223+
152224
} // namespace klee

0 commit comments

Comments
 (0)