Skip to content

Commit cd62c3a

Browse files
ladisginladisgin
committed
temp
1 parent dc27b24 commit cd62c3a

5 files changed

Lines changed: 187 additions & 189 deletions

File tree

‎include/klee/Core/MockBuilder.h‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -27,17 +27,16 @@ class MockBuilder {
2727
void buildExternalFunctionsDefinitions();
2828
void
2929
buildCallKleeMakeSymbolic(const std::string &kleeMakeSymbolicFunctionName,
30-
llvm::Value *source, llvm::Type *type,
31-
const std::string &symbolicName);
30+
llvm::Value *source, llvm::Type *type,
31+
const std::string &symbolicName);
3232

3333
void buildAnnotationForExternalFunctionArgs(
3434
llvm::Function *func,
35-
const std::vector<std::vector<Annotation::StatementPtr>> &statementsNotAllign);
35+
const std::vector<std::vector<Statement::Ptr>> &statementsNotAllign);
3636
void buildAnnotationForExternalFunctionReturn(
37-
llvm::Function *func, const std::vector<Annotation::StatementPtr> &statements);
37+
llvm::Function *func, const std::vector<Statement::Ptr> &statements);
3838
void buildAnnotationForExternalFunctionProperties(
39-
llvm::Function *func,
40-
const std::set<Annotation::PropertyKind> &properties);
39+
llvm::Function *func, const std::set<Statement::Property> &properties);
4140

4241
llvm::Value *goByOffset(llvm::Value *value,
4342
const std::vector<std::string> &offset);

‎include/klee/Module/Annotation.h‎

Lines changed: 41 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -15,56 +15,63 @@ using json = nlohmann::json;
1515

1616
namespace klee {
1717

18-
// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
19-
struct Annotation {
20-
enum class StatementKind {
21-
Unknown,
18+
namespace Statement {
19+
enum class Kind {
20+
Unknown,
2221

23-
Deref,
24-
InitNull,
25-
};
22+
Deref,
23+
InitNull,
24+
};
2625

27-
enum class PropertyKind {
28-
Unknown,
26+
enum class Property {
27+
Unknown,
2928

30-
Determ,
31-
Noreturn,
32-
};
29+
Deterministic,
30+
Noreturn,
31+
};
3332

34-
struct StatementUnknown {
35-
explicit StatementUnknown(const std::string &str);
36-
virtual ~StatementUnknown();
33+
struct Unknown {
34+
explicit Unknown(const std::string &str = "Unknown");
35+
virtual ~Unknown();
3736

38-
virtual Annotation::StatementKind getStatementKind() const;
39-
virtual bool operator==(const StatementUnknown &other) const;
37+
virtual bool operator==(const Unknown &other) const;
38+
[[nodiscard]] virtual Kind getKind() const;
4039

41-
std::string statementStr;
42-
std::vector<std::string> offset;
40+
std::string statementStr;
41+
std::vector<std::string> offset;
4342

44-
private:
45-
void parseOffset(const std::string &str);
46-
};
43+
private:
44+
void parseOffset(const std::string &str);
45+
};
4746

48-
struct StatementDeref final : public StatementUnknown {
49-
explicit StatementDeref(const std::string &str);
47+
struct Deref final : public Unknown {
48+
explicit Deref(const std::string &str = "Deref");
5049

51-
Annotation::StatementKind getStatementKind() const override;
52-
};
50+
[[nodiscard]] Kind getKind() const override;
51+
};
5352

54-
struct StatementInitNull final : public StatementUnknown {
55-
explicit StatementInitNull(const std::string &str);
53+
struct InitNull final : public Unknown {
54+
explicit InitNull(const std::string &str = "InitNull");
5655

57-
Annotation::StatementKind getStatementKind() const override;
58-
};
56+
[[nodiscard]] Kind getKind() const override;
57+
};
5958

60-
using StatementPtr = std::shared_ptr<StatementUnknown>;
59+
using Ptr = std::shared_ptr<Unknown>;
60+
bool operator==(const Ptr &first, const Ptr &second);
61+
} // namespace Statement
62+
63+
// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
64+
struct Annotation {
6165

6266
bool operator==(const Annotation &other) const;
6367

6468
std::string functionName;
65-
std::vector<StatementPtr> returnStatements;
66-
std::vector<std::vector<StatementPtr>> argsStatements;
67-
std::set<PropertyKind> properties;
69+
std::vector<Statement::Ptr> returnStatements;
70+
std::vector<std::vector<Statement::Ptr>> argsStatements;
71+
std::set<Statement::Property> properties;
72+
73+
static void printWarrning(const std::string &message,
74+
const std::string &functionName);
6875
};
6976

7077
using AnnotationsMap = std::map<std::string, Annotation>;

‎lib/Core/MockBuilder.cpp‎

Lines changed: 57 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,7 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
124124
if (nameToAnnotations != annotations.end()) {
125125
const auto &annotation = nameToAnnotations->second;
126126

127-
buildAnnotationForExternalFunctionArgs(func,
128-
annotation.argsStatements);
127+
buildAnnotationForExternalFunctionArgs(func, annotation.argsStatements);
129128
buildAnnotationForExternalFunctionReturn(func,
130129
annotation.returnStatements);
131130
buildAnnotationForExternalFunctionProperties(func, annotation.properties);
@@ -208,28 +207,26 @@ inline llvm::Type *getTypeByOffset(llvm::Type *value,
208207
return current;
209208
}
210209

211-
inline bool
212-
isCorrectStatements(const std::vector<Annotation::StatementPtr> &statements,
213-
const llvm::Argument *arg) {
210+
inline bool isCorrectStatements(const std::vector<Statement::Ptr> &statements,
211+
const llvm::Argument *arg) {
214212
return std::any_of(statements.begin(), statements.end(),
215-
[arg](const Annotation::StatementPtr &statement) {
213+
[arg](const Statement::Ptr &statement) {
216214
auto argType =
217215
getTypeByOffset(arg->getType(), statement->offset);
218-
switch (statement->getStatementKind()) {
219-
case Annotation::StatementKind::Deref:
220-
case Annotation::StatementKind::InitNull:
216+
switch (statement->getKind()) {
217+
case Statement::Kind::Deref:
218+
case Statement::Kind::InitNull:
221219
return argType->isPointerTy();
222-
case Annotation::StatementKind::Unknown:
220+
case Statement::Kind::Unknown:
223221
default:
224222
return true;
225223
}
226224
});
227225
}
228226

229-
bool tryAllign(
230-
llvm::Function *func,
231-
const std::vector<std::vector<Annotation::StatementPtr>> &statements,
232-
std::vector<std::vector<Annotation::StatementPtr>> &res) {
227+
bool tryAlign(llvm::Function *func,
228+
const std::vector<std::vector<Statement::Ptr>> &statements,
229+
std::vector<std::vector<Statement::Ptr>> &res) {
233230
if (func->arg_size() == statements.size()) {
234231
return true;
235232
}
@@ -254,10 +251,9 @@ bool tryAllign(
254251

255252
void MockBuilder::buildAnnotationForExternalFunctionArgs(
256253
llvm::Function *func,
257-
const std::vector<std::vector<Annotation::StatementPtr>>
258-
&statementsNotAllign) {
259-
std::vector<std::vector<Annotation::StatementPtr>> statements;
260-
bool flag = tryAllign(func, statementsNotAllign, statements);
254+
const std::vector<std::vector<Statement::Ptr>> &statementsNotAlign) {
255+
std::vector<std::vector<Statement::Ptr>> statements;
256+
bool flag = tryAlign(func, statementsNotAlign, statements);
261257
if (!flag) {
262258
klee_warning("Annotation: incorrect arguments count function %s ",
263259
func->getName().str().c_str());
@@ -267,8 +263,8 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
267263
const auto arg = func->getArg(i);
268264
for (const auto &statement : statements[i]) {
269265
llvm::Value *elem = goByOffset(arg, statement->offset);
270-
switch (statement->getStatementKind()) {
271-
case Annotation::StatementKind::Deref: {
266+
switch (statement->getKind()) {
267+
case Statement::Kind::Deref: {
272268
if (!elem->getType()->isPointerTy()) {
273269
klee_error("Annotation: deref arg not pointer");
274270
}
@@ -299,8 +295,8 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
299295

300296
break;
301297
}
302-
case Annotation::StatementKind::InitNull:
303-
case Annotation::StatementKind::Unknown:
298+
case Statement::Kind::InitNull:
299+
case Statement::Kind::Unknown:
304300
default:
305301
klee_message("Annotation not implemented");
306302
break;
@@ -310,8 +306,7 @@ void MockBuilder::buildAnnotationForExternalFunctionArgs(
310306
}
311307

312308
void MockBuilder::buildAnnotationForExternalFunctionReturn(
313-
llvm::Function *func,
314-
const std::vector<Annotation::StatementPtr> &statements) {
309+
llvm::Function *func, const std::vector<Statement::Ptr> &statements) {
315310
auto returnType = func->getReturnType();
316311
std::string retName = "ret_" + func->getName().str();
317312

@@ -321,58 +316,56 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
321316
auto *loadInst =
322317
builder->CreateLoad(func->getReturnType(), mockReturnValue, retName);
323318

324-
if (!statements.empty()) {
325-
bool initNull = false;
319+
bool initNull = false;
326320

327-
for (const auto &statement : statements) {
328-
switch (statement->getStatementKind()) {
329-
case Annotation::StatementKind::Deref:
330-
klee_warning("unused annotation Deref for return");
331-
break;
332-
case Annotation::StatementKind::InitNull: {
333-
if (!returnType->isPointerTy()) {
334-
klee_error("incorrect type for InitNull");
335-
}
336-
initNull = true;
337-
break;
338-
}
339-
case Annotation::StatementKind::Unknown:
340-
default:
341-
klee_message("Annotation not implemented");
342-
break;
321+
for (const auto &statement : statements) {
322+
switch (statement->getKind()) {
323+
case Statement::Kind::Deref:
324+
klee_warning("Annotation: unused Deref for return function \"%s\"",
325+
func->getName());
326+
break;
327+
case Statement::Kind::InitNull: {
328+
if (!returnType->isPointerTy()) {
329+
klee_error("incorrect type for InitNull");
343330
}
331+
initNull = true;
332+
break;
344333
}
345-
346-
if (!initNull) {
347-
auto cmpResult = builder->CreateICmpNE(
348-
loadInst,
349-
llvm::ConstantPointerNull::get(
350-
llvm::cast<llvm::PointerType>(loadInst->getType())),
351-
"condition_init_null" + retName);
352-
353-
auto *kleeAssumeType = llvm::FunctionType::get(
354-
llvm::Type::getVoidTy(mockModule->getContext()),
355-
{llvm::Type::getInt64Ty(mockModule->getContext())}, false);
356-
357-
auto kleeAssumeFunc =
358-
mockModule->getOrInsertFunction("klee_assume", kleeAssumeType);
359-
auto cmpResult64 = builder->CreateZExt(
360-
cmpResult, llvm::Type::getInt64Ty(mockModule->getContext()));
361-
builder->CreateCall(kleeAssumeFunc, {cmpResult64});
334+
case Statement::Kind::Unknown:
335+
default:
336+
klee_message("Annotation not implemented");
337+
break;
362338
}
363339
}
364340

341+
if (!initNull) {
342+
auto cmpResult = builder->CreateICmpNE(
343+
loadInst,
344+
llvm::ConstantPointerNull::get(
345+
llvm::cast<llvm::PointerType>(loadInst->getType())),
346+
"condition_init_null" + retName);
347+
348+
auto *kleeAssumeType = llvm::FunctionType::get(
349+
llvm::Type::getVoidTy(mockModule->getContext()),
350+
{llvm::Type::getInt64Ty(mockModule->getContext())}, false);
351+
352+
auto kleeAssumeFunc =
353+
mockModule->getOrInsertFunction("klee_assume", kleeAssumeType);
354+
auto cmpResult64 = builder->CreateZExt(
355+
cmpResult, llvm::Type::getInt64Ty(mockModule->getContext()));
356+
builder->CreateCall(kleeAssumeFunc, {cmpResult64});
357+
}
358+
365359
builder->CreateRet(loadInst);
366360
}
367361

368362
void MockBuilder::buildAnnotationForExternalFunctionProperties(
369-
llvm::Function *func,
370-
const std::set<Annotation::PropertyKind> &properties) {
363+
llvm::Function *func, const std::set<Statement::Property> &properties) {
371364
for (const auto &property : properties) {
372365
switch (property) {
373-
case Annotation::PropertyKind::Determ:
374-
case Annotation::PropertyKind::Noreturn:
375-
case Annotation::PropertyKind::Unknown:
366+
case Statement::Property::Deterministic:
367+
case Statement::Property::Noreturn:
368+
case Statement::Property::Unknown:
376369
default:
377370
klee_message("Annotation not implemented");
378371
break;

0 commit comments

Comments
 (0)