Skip to content

Commit a1aa217

Browse files
ladisginladisgin
committed
Add annotation implementation and tests
1 parent cb4a318 commit a1aa217

39 files changed

+1724
-498
lines changed

‎.github/workflows/build.yaml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,6 @@ jobs:
139139
runs-on: macos-latest
140140
env:
141141
BASE: /tmp
142-
LLVM_VERSION: 11
143142
SOLVERS: STP
144143
UCLIBC_VERSION: 0
145144
USE_TCMALLOC: 0

‎.gitmodules‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
[submodule "json"]
2-
path = json
2+
path = submodules/json
33
url = https://github.com/nlohmann/json.git
44
[submodule "optional"]
5-
path = optional
5+
path = submodules/optional
66
url = https://github.com/martinmoene/optional-lite.git
7+
[submodule "submodules/pugixml"]
8+
path = submodules/pugixml
9+
url = https://github.com/zeux/pugixml.git

‎CMakeLists.txt‎

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -657,8 +657,21 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
657657
################################################################################
658658
include_directories("${CMAKE_BINARY_DIR}/include")
659659
include_directories("${CMAKE_SOURCE_DIR}/include")
660-
include_directories("${CMAKE_SOURCE_DIR}/json/include")
661-
include_directories("${CMAKE_SOURCE_DIR}/optional/include")
660+
include_directories("${CMAKE_SOURCE_DIR}/submodules/json/include")
661+
include_directories("${CMAKE_SOURCE_DIR}/submodules/optional/include")
662+
663+
664+
option(ENABLE_XML_ANNOTATION "Enable XML annotation" ON)
665+
666+
if (ENABLE_XML_ANNOTATION)
667+
message(STATUS "XML annotation is enabled")
668+
file(COPY "${CMAKE_SOURCE_DIR}/submodules/pugiconfig.hpp"
669+
DESTINATION "${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
670+
include_directories("${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
671+
else()
672+
message(STATUS "XML annotation is disabled")
673+
set(ENABLE_XML_ANNOTATION 0)
674+
endif()
662675
# set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
663676

664677
################################################################################

‎include/klee/Config/config.h.cmin‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -119,4 +119,7 @@ macro for that. That would simplify the C++ code. */
119119
/* Install directory for KLEE runtime */
120120
#define KLEE_INSTALL_RUNTIME_DIR "@KLEE_INSTALL_RUNTIME_DIR@"
121121

122+
/* Enable XML annotation parser */
123+
#define ENABLE_XML_ANNOTATION "@ENABLE_XML_ANNOTATION@"
124+
122125
#endif /* KLEE_CONFIG_H */

‎include/klee/Core/Interpreter.h‎

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -88,25 +88,31 @@ class Interpreter {
8888
std::string OptSuffix;
8989
std::string MainCurrentName;
9090
std::string MainNameAfterMock;
91+
std::string AnnotationsFile;
9192
bool Optimize;
9293
bool Simplify;
9394
bool CheckDivZero;
9495
bool CheckOvershift;
96+
bool AnnotateOnlyExternal;
9597
bool WithFPRuntime;
9698
bool WithPOSIXRuntime;
9799

98100
ModuleOptions(const std::string &_LibraryDir,
99101
const std::string &_EntryPoint, const std::string &_OptSuffix,
100102
const std::string &_MainCurrentName,
101-
const std::string &_MainNameAfterMock, bool _Optimize,
103+
const std::string &_MainNameAfterMock,
104+
const std::string &_AnnotationsFile, bool _Optimize,
102105
bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
103-
bool _WithFPRuntime, bool _WithPOSIXRuntime)
106+
bool _AnnotateOnlyExternal, bool _WithFPRuntime,
107+
bool _WithPOSIXRuntime)
104108
: LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
105109
OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
106-
MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize),
110+
MainNameAfterMock(_MainNameAfterMock),
111+
AnnotationsFile(_AnnotationsFile), Optimize(_Optimize),
107112
Simplify(_Simplify), CheckDivZero(_CheckDivZero),
108-
CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime),
109-
WithPOSIXRuntime(_WithPOSIXRuntime) {}
113+
CheckOvershift(_CheckOvershift),
114+
AnnotateOnlyExternal(_AnnotateOnlyExternal),
115+
WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
110116
};
111117

112118
enum LogType {
@@ -159,10 +165,7 @@ class Interpreter {
159165
const std::unordered_set<std::string> &mainModuleGlobals,
160166
std::unique_ptr<InstructionInfoTable> origInfos,
161167
const std::set<std::string> &ignoredExternals,
162-
const Annotations &annotations) = 0;
163-
164-
virtual std::map<std::string, llvm::Type *>
165-
getAllExternals(const std::set<std::string> &ignoredExternals) = 0;
168+
std::vector<std::pair<std::string, std::string>> redefinitions) = 0;
166169

167170
// supply a tree stream writer which the interpreter will use
168171
// to record the concrete path (as a stream of '0' and '1' bytes).

‎include/klee/Core/MockBuilder.h‎

Lines changed: 37 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
#ifndef KLEE_MOCKBUILDER_H
22
#define KLEE_MOCKBUILDER_H
33

4+
#include "klee/Core/Interpreter.h"
45
#include "klee/Module/Annotation.h"
56

67
#include "llvm/IR/IRBuilder.h"
@@ -16,30 +17,52 @@ class MockBuilder {
1617
const llvm::Module *userModule;
1718
std::unique_ptr<llvm::Module> mockModule;
1819
std::unique_ptr<llvm::IRBuilder<>> builder;
19-
std::map<std::string, llvm::Type *> externals;
20-
Annotations annotations;
2120

22-
const std::string mockEntrypoint, userEntrypoint;
21+
const Interpreter::ModuleOptions &opts;
22+
23+
std::set<std::string> ignoredExternals;
24+
std::vector<std::pair<std::string, std::string>> redefinitions;
25+
26+
InterpreterHandler *interpreterHandler;
27+
28+
AnnotationsMap annotations;
2329

2430
void initMockModule();
2531
void buildMockMain();
2632
void buildExternalGlobalsDefinitions();
2733
void buildExternalFunctionsDefinitions();
28-
void buildCallKleeMakeSymbol(const std::string &klee_function_name,
29-
llvm::Value *source, llvm::Type *type,
30-
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);
34+
void
35+
buildCallKleeMakeSymbolic(const std::string &kleeMakeSymbolicFunctionName,
36+
llvm::Value *source, llvm::Type *type,
37+
const std::string &symbolicName);
38+
39+
void buildAnnotationForExternalFunctionArgs(
40+
llvm::Function *func,
41+
const std::vector<std::vector<Statement::Ptr>> &statementsNotAllign);
42+
void buildAnnotationForExternalFunctionReturn(
43+
llvm::Function *func, const std::vector<Statement::Ptr> &statements);
44+
void buildAnnotationForExternalFunctionProperties(
45+
llvm::Function *func, const std::set<Statement::Property> &properties);
46+
47+
std::map<std::string, llvm::FunctionType *> getExternalFunctions();
48+
std::map<std::string, llvm::Type *> getExternalGlobals();
49+
50+
std::pair<llvm::Value *, llvm::Value *>
51+
goByOffset(llvm::Value *value, const std::vector<std::string> &offset);
3552

3653
public:
37-
MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
38-
std::string userEntrypoint,
39-
std::map<std::string, llvm::Type *> externals,
40-
Annotations annotations);
54+
MockBuilder(const llvm::Module *initModule,
55+
const Interpreter::ModuleOptions &opts,
56+
const std::set<std::string> &ignoredExternals,
57+
std::vector<std::pair<std::string, std::string>> &redefinitions,
58+
InterpreterHandler *interpreterHandler);
4159

4260
std::unique_ptr<llvm::Module> build();
61+
void buildAllocSource(llvm::Value *prev, llvm::Type *elemType,
62+
const Statement::AllocSource *allocSourcePtr);
63+
void processingValue(llvm::Value *prev, llvm::Type *elemType,
64+
const Statement::AllocSource *allocSourcePtr,
65+
const Statement::InitNull *initNullPtr);
4366
};
4467

4568
} // namespace klee

‎include/klee/Module/Annotation.h‎

Lines changed: 65 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -9,78 +9,98 @@
99
#include "nlohmann/json.hpp"
1010
#include "nonstd/optional.hpp"
1111

12+
#include "klee/Config/config.h"
13+
14+
#include "llvm/IR/Module.h"
15+
1216
using nonstd::nullopt;
1317
using nonstd::optional;
1418
using json = nlohmann::json;
1519

1620
namespace klee {
1721

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

23-
Deref,
24-
InitNull,
25-
};
26+
Deref,
27+
InitNull,
28+
AllocSource,
29+
};
2630

27-
enum class Property {
28-
Unknown,
31+
enum class Property {
32+
Unknown,
2933

30-
Determ,
31-
Noreturn,
32-
};
34+
Deterministic,
35+
Noreturn,
36+
};
3337

34-
struct StatementUnknown {
35-
explicit StatementUnknown(const std::string &str);
36-
virtual ~StatementUnknown();
38+
struct Unknown {
39+
protected:
40+
std::string rawAnnotation;
41+
std::string rawOffset;
42+
std::string rawValue;
3743

38-
virtual Annotation::StatementKind getStatementName() const;
39-
virtual bool operator==(const StatementUnknown &other) const;
44+
public:
45+
std::vector<std::string> offset;
4046

41-
std::string statementStr;
42-
std::vector<std::string> offset;
47+
explicit Unknown(const std::string &str = "Unknown");
48+
virtual ~Unknown();
4349

44-
protected:
45-
void parseOffset(const std::string &offsetStr);
46-
void parseOnlyOffset(const std::string &str);
47-
};
50+
virtual bool operator==(const Unknown &other) const;
51+
[[nodiscard]] virtual Kind getKind() const;
4852

49-
struct StatementDeref final : public StatementUnknown {
50-
explicit StatementDeref(const std::string &str);
53+
[[nodiscard]] const std::vector<std::string> &getOffset() const;
54+
[[nodiscard]] std::string toString() const;
55+
};
5156

52-
Annotation::StatementKind getStatementName() const override;
53-
};
57+
struct Deref final : public Unknown {
58+
explicit Deref(const std::string &str = "Deref");
5459

55-
struct StatementInitNull final : public StatementUnknown {
56-
explicit StatementInitNull(const std::string &str);
60+
[[nodiscard]] Kind getKind() const override;
61+
};
5762

58-
Annotation::StatementKind getStatementName() const override;
63+
struct InitNull final : public Unknown {
64+
explicit InitNull(const std::string &str = "InitNull");
65+
66+
[[nodiscard]] Kind getKind() const override;
67+
};
68+
69+
struct AllocSource final : public Unknown {
70+
public:
71+
enum Type {
72+
Alloc = 1, // malloc, calloc, realloc
73+
New = 2, // operator new
74+
NewBrackets = 3, // operator new[]
75+
OpenFile = 4, // open file (fopen, open)
76+
MutexLock = 5 // mutex lock (pthread_mutex_lock)
5977
};
6078

61-
using StatementPtr = std::shared_ptr<StatementUnknown>;
62-
using StatementPtrs = std::vector<StatementPtr>;
79+
Type value;
6380

64-
bool operator==(const Annotation &other) const;
81+
explicit AllocSource(const std::string &str = "AllocSource::1");
6582

66-
std::string functionName;
67-
std::vector<StatementPtrs> statements;
68-
std::set<Property> properties;
83+
[[nodiscard]] Kind getKind() const override;
6984
};
7085

71-
using Annotations = std::map<std::string, Annotation>;
86+
using Ptr = std::shared_ptr<Unknown>;
87+
bool operator==(const Ptr &first, const Ptr &second);
88+
} // namespace Statement
7289

73-
const std::map<std::string, Annotation::Property> toProperties{
74-
{"determ", Annotation::Property::Determ},
75-
{"noreturn", Annotation::Property::Noreturn},
76-
};
90+
// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
91+
struct Annotation {
92+
std::string functionName;
93+
std::vector<Statement::Ptr> returnStatements;
94+
std::vector<std::vector<Statement::Ptr>> argsStatements;
95+
std::set<Statement::Property> properties;
7796

78-
Annotations parseAnnotationsFile(const json &annotationsJson);
79-
Annotations parseAnnotationsFile(const std::string &path);
97+
bool operator==(const Annotation &other) const;
98+
};
8099

81-
bool operator==(const Annotation::StatementPtr &first,
82-
const Annotation::StatementPtr &second);
100+
using AnnotationsMap = std::map<std::string, Annotation>;
83101

102+
AnnotationsMap parseAnnotationsJson(const json &annotationsJson);
103+
AnnotationsMap parseAnnotations(const std::string &path, const llvm::Module *m);
84104
} // namespace klee
85105

86106
#endif // KLEE_ANNOTATION_H

‎lib/Core/ExecutionState.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,10 @@
2323
#include "klee/Support/CompilerWarning.h"
2424
DISABLE_WARNING_PUSH
2525
DISABLE_WARNING_DEPRECATED_DECLARATIONS
26+
#include "klee/Support/ErrorHandling.h"
2627
#include "llvm/IR/Function.h"
2728
#include "llvm/Support/CommandLine.h"
2829
#include "llvm/Support/raw_ostream.h"
29-
#include "klee/Support/ErrorHandling.h"
3030
DISABLE_WARNING_POP
3131

3232
#include <cassert>

0 commit comments

Comments
 (0)