Skip to content

Commit bddcfc0

Browse files
committed
Fix bugs, change annotation config and calc AnnotationData for Executor
1 parent c4b8b10 commit bddcfc0

13 files changed

Lines changed: 919 additions & 12593 deletions

configs/annotations.json

Lines changed: 837 additions & 12544 deletions
Large diffs are not rendered by default.

include/klee/Core/Interpreter.h

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@
1010
#define KLEE_INTERPRETER_H
1111

1212
#include "TerminationTypes.h"
13-
#include "klee/Module/Annotation.h"
1413

14+
#include "klee/Module/AnnotationsData.h"
1515
#include "klee/Module/SarifReport.h"
1616

1717
#include <cstdint>
@@ -122,17 +122,13 @@ class Interpreter {
122122
ModuleOptions(const std::string &_LibraryDir,
123123
const std::string &_EntryPoint, const std::string &_OptSuffix,
124124
const std::string &_MainCurrentName,
125-
const std::string &_MainNameAfterMock,
126-
const std::string &_AnnotationsFile,
127-
const std::string &_TaintAnnotationsFile, bool _Optimize,
125+
const std::string &_MainNameAfterMock, bool _Optimize,
128126
bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
129127
bool _AnnotateOnlyExternal, bool _WithFPRuntime,
130128
bool _WithPOSIXRuntime)
131129
: LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
132130
OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
133-
MainNameAfterMock(_MainNameAfterMock),
134-
AnnotationsFile(_AnnotationsFile),
135-
TaintAnnotationsFile(_TaintAnnotationsFile), Optimize(_Optimize),
131+
MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize),
136132
Simplify(_Simplify), CheckDivZero(_CheckDivZero),
137133
CheckOvershift(_CheckOvershift),
138134
AnnotateOnlyExternal(_AnnotateOnlyExternal),
@@ -157,6 +153,8 @@ class Interpreter {
157153
MockPolicy Mock;
158154
MockStrategyKind MockStrategy;
159155
MockMutableGlobalsPolicy MockMutableGlobals;
156+
std::string AnnotationsFile;
157+
std::string TaintAnnotationsFile;
160158

161159
InterpreterOptions(std::optional<SarifReport> Paths)
162160
: MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),

include/klee/Core/MockBuilder.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ class MockBuilder {
3838
std::set<std::string> &mainModuleFunctions;
3939
std::set<std::string> &mainModuleGlobals;
4040

41-
AnnotationsData annotationsData;
41+
const AnnotationsData &annotationsData;
4242

4343
void initMockModule();
4444
void buildMockMain();
@@ -86,7 +86,8 @@ class MockBuilder {
8686
std::vector<std::pair<std::string, std::string>> &redefinitions,
8787
InterpreterHandler *interpreterHandler,
8888
std::set<std::string> &mainModuleFunctions,
89-
std::set<std::string> &mainModuleGlobals);
89+
std::set<std::string> &mainModuleGlobals,
90+
const AnnotationsData &annotationsData);
9091

9192
std::unique_ptr<llvm::Module> build();
9293
void buildAllocSource(llvm::Value *prev, llvm::Type *elemType,

include/klee/Core/TerminationTypes.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,8 @@ enum class StateTerminationClass : std::uint8_t {
7575
TTMARK(EARLYALGORITHM, 72U) \
7676
TTYPE(SilentExit, 80U, "") \
7777
TTMARK(EARLYUSER, 80U) \
78-
TTMARK(END, 80U)
78+
TTMARK(END, 80U) \
79+
TTYPE(Taint, 90U, "taint.err")
7980

8081
///@brief Reason an ExecutionState got terminated.
8182
enum class StateTerminationType : std::uint8_t {

include/klee/Module/AnnotationsData.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,9 @@ struct AnnotationsData final {
1010
AnnotationsMap annotations;
1111
TaintAnnotation taintAnnotation;
1212

13-
explicit AnnotationsData(const std::string &annotationsFile,
14-
const std::string &taintAnnotationsFile);
13+
explicit AnnotationsData(
14+
const std::string &annotationsFile = std::string(),
15+
const std::string &taintAnnotationsFile = std::string());
1516
virtual ~AnnotationsData();
1617
};
1718

include/klee/Module/TaintAnnotation.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,16 +13,17 @@ using json = nlohmann::json;
1313

1414
namespace klee {
1515

16+
// TODO: set<size_t> to set<pair<size_t, size)t>>, where pair is sink and target
1617
using TaintSinksSourcesMap = std::map<size_t, std::set<size_t>>;
1718

1819
class TaintAnnotation final {
1920
public:
2021
TaintSinksSourcesMap sinksToSources;
2122
std::map<std::string, size_t> sinks;
2223
std::map<std::string, size_t> sources;
24+
// TODO: add map from size_t target to string
2325

24-
explicit TaintAnnotation();
25-
explicit TaintAnnotation(const std::string &taintAnnotationsFile);
26+
explicit TaintAnnotation(const std::string &path);
2627
virtual ~TaintAnnotation();
2728
};
2829

lib/Core/Executor.cpp

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -505,7 +505,9 @@ const std::unordered_set<Intrinsic::ID> Executor::modelledFPIntrinsics = {
505505

506506
Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
507507
InterpreterHandler *ih)
508-
: Interpreter(opts), interpreterHandler(ih), searcher(nullptr),
508+
: Interpreter(opts),
509+
annotationsData(opts.AnnotationsFile, opts.TaintAnnotationsFile),
510+
interpreterHandler(ih), searcher(nullptr),
509511
externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
510512
pathWriter(0), symPathWriter(0),
511513
specialFunctionHandler(0), timers{time::Span(TimerInterval)},
@@ -636,7 +638,8 @@ llvm::Module *Executor::setModule(
636638
!opts.AnnotationsFile.empty()) {
637639
MockBuilder mockBuilder(kmodule->module.get(), opts, interpreterOpts,
638640
ignoredExternals, redefinitions, interpreterHandler,
639-
mainModuleFunctions, mainModuleGlobals);
641+
mainModuleFunctions, mainModuleGlobals,
642+
annotationsData);
640643
std::unique_ptr<llvm::Module> mockModule = mockBuilder.build();
641644

642645
std::vector<std::unique_ptr<llvm::Module>> mockModules;
@@ -5022,6 +5025,22 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
50225025
state, new ErrorEvent(locationOf(state), terminationType, messaget));
50235026
}
50245027

5028+
// TODO: add taint target errors to taint-annotations.json and change function
5029+
void Executor::terminateStateOnTaintError(ExecutionState &state, size_t sink) {
5030+
// reportStateOnTargetError(state, error);
5031+
5032+
const auto &sinks = annotationsData.taintAnnotation.sinks;
5033+
auto taintSink = std::find_if(sinks.begin(), sinks.end(),
5034+
[&](const std::pair<std::string, size_t> &i) {
5035+
return i.second == sink;
5036+
});
5037+
if (taintSink == std::end(sinks)) {
5038+
klee_error("Unknown sink index");
5039+
}
5040+
terminateStateOnProgramError(state, taintSink->first + " taint error",
5041+
StateTerminationType::Taint);
5042+
}
5043+
50255044
void Executor::terminateStateOnError(ExecutionState &state,
50265045
const llvm::Twine &messaget,
50275046
StateTerminationType terminationType,

lib/Core/Executor.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
#include "klee/Expr/Constraints.h"
3232
#include "klee/Expr/SourceBuilder.h"
3333
#include "klee/Expr/SymbolicSource.h"
34+
#include "klee/Module/AnnotationsData.h"
3435
#include "klee/Module/Cell.h"
3536
#include "klee/Module/KInstruction.h"
3637
#include "klee/Module/KModule.h"
@@ -127,6 +128,8 @@ class Executor : public Interpreter {
127128
RNG theRNG;
128129

129130
private:
131+
AnnotationsData annotationsData;
132+
130133
int *errno_addr;
131134

132135
size_t maxNewWriteableOSSize = 0;
@@ -631,6 +634,8 @@ class Executor : public Interpreter {
631634
/// Then just call `terminateStateOnError`
632635
void terminateStateOnTargetError(ExecutionState &state, ReachWithError error);
633636

637+
void terminateStateOnTaintError(ExecutionState &state, size_t sink);
638+
634639
/// Call error handler and terminate state in case of program errors
635640
/// (e.g. free()ing globals, out-of-bound accesses)
636641
void terminateStateOnProgramError(ExecutionState &state,

lib/Core/MockBuilder.cpp

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -89,14 +89,14 @@ MockBuilder::MockBuilder(
8989
std::vector<std::pair<std::string, std::string>> &redefinitions,
9090
InterpreterHandler *interpreterHandler,
9191
std::set<std::string> &mainModuleFunctions,
92-
std::set<std::string> &mainModuleGlobals)
92+
std::set<std::string> &mainModuleGlobals,
93+
const AnnotationsData &annotationsData)
9394
: userModule(initModule), ctx(initModule->getContext()), opts(opts),
9495
interpreterOptions(interpreterOptions),
9596
ignoredExternals(ignoredExternals), redefinitions(redefinitions),
9697
interpreterHandler(interpreterHandler),
9798
mainModuleFunctions(mainModuleFunctions),
98-
mainModuleGlobals(mainModuleGlobals),
99-
annotationsData(opts.AnnotationsFile, opts.TaintAnnotationsFile) {}
99+
mainModuleGlobals(mainModuleGlobals), annotationsData(annotationsData) {}
100100

101101
std::unique_ptr<llvm::Module> MockBuilder::build() {
102102
initMockModule();
@@ -535,7 +535,7 @@ MockBuilder::buildCallKleeTaintFunction(const std::string &functionName,
535535
{llvm::Type::getInt8PtrTy(mockModule->getContext()),
536536
llvm::Type::getInt64Ty(mockModule->getContext())},
537537
false);
538-
auto kleeAddTaintCallee =
538+
auto kleeTaintFunctionCallee =
539539
mockModule->getOrInsertFunction(functionName, kleeTaintFunctionType);
540540

541541
// //TODO: that's not all:
@@ -579,13 +579,15 @@ MockBuilder::buildCallKleeTaintFunction(const std::string &functionName,
579579
if (!source->getType()->isPointerTy() && !source->getType()->isArrayTy()) {
580580
beginPtr = builder->CreateAlloca(source->getType());
581581
builder->CreateStore(source, beginPtr);
582+
beginPtr = builder->CreateBitCast(
583+
beginPtr, llvm::Type::getInt8PtrTy(mockModule->getContext()));
582584
} else {
583585
beginPtr = builder->CreateBitCast(
584586
source, llvm::Type::getInt8PtrTy(mockModule->getContext()));
585587
}
586588

587589
return builder->CreateCall(
588-
kleeAddTaintCallee,
590+
kleeTaintFunctionCallee,
589591
{beginPtr, llvm::ConstantInt::get(mockModule->getContext(),
590592
llvm::APInt(64, taint, false))});
591593
}
@@ -847,6 +849,14 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
847849
std::string retName = "ret_" + func->getName().str();
848850
llvm::Value *retValuePtr = builder->CreateAlloca(returnType, nullptr);
849851

852+
// TODO: fix strange type ("fopen" mock, store instruction)
853+
// if (func->getName() == "fopen") {
854+
// buildCallKleeMakeSymbolic("klee_make_mock", retValuePtr, returnType,
855+
// func->getName().str());
856+
// llvm::Value *retValue = builder->CreateLoad(returnType, retValuePtr,
857+
// retName); builder->CreateRet(retValue); return;
858+
// }
859+
850860
if (returnType->isPointerTy() && (allocSourcePtr || mustInitNull)) {
851861
processingValue(retValuePtr, returnType, allocSourcePtr,
852862
mustInitNull || maybeInitNull);

lib/Core/SpecialFunctionHandler.cpp

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
135135
add("klee_check_taint_source", handleCheckTaintSource, true),
136136
add("klee_check_taint_sink", handleCheckTaintSink, true),
137137
add("klee_taint_sink_hit", handleTaintSinkHit, false),
138+
138139
#ifdef SUPPORT_KLEE_EH_CXX
139140
add("_klee_eh_Unwind_RaiseException_impl", handleEhUnwindRaiseExceptionImpl,
140141
false),
@@ -1220,8 +1221,6 @@ void SpecialFunctionHandler::handleFAbs(ExecutionState &state,
12201221
executor.bindLocal(target, state, result);
12211222
}
12221223

1223-
// TODO: update definitions after adding taint memory
1224-
12251224
void SpecialFunctionHandler::handleAddTaint(klee::ExecutionState &state,
12261225
klee::KInstruction *target,
12271226
std::vector<ref<Expr>> &arguments) {
@@ -1231,8 +1230,6 @@ void SpecialFunctionHandler::handleAddTaint(klee::ExecutionState &state,
12311230
"klee_add_taint(void*, size_t)");
12321231
return;
12331232
}
1234-
1235-
// executor.executeMemoryOperation(state, true)
12361233
}
12371234

12381235
void SpecialFunctionHandler::handleClearTaint(
@@ -1244,8 +1241,6 @@ void SpecialFunctionHandler::handleClearTaint(
12441241
"klee_clear_taint(void*, size_t)");
12451242
return;
12461243
}
1247-
1248-
// executor.executeMemoryOperation(state, true)
12491244
}
12501245

12511246
void SpecialFunctionHandler::handleCheckTaintSource(
@@ -1257,9 +1252,6 @@ void SpecialFunctionHandler::handleCheckTaintSource(
12571252
"klee_check_taint_source(void*, size_t)");
12581253
return;
12591254
}
1260-
1261-
// ref<Expr> result = ConstantExpr::create(true, Expr::Bool);
1262-
// executor.bindLocal(target, state, result);
12631255
}
12641256

12651257
void SpecialFunctionHandler::handleCheckTaintSink(
@@ -1285,6 +1277,12 @@ void SpecialFunctionHandler::handleTaintSinkHit(
12851277
return;
12861278
}
12871279

1288-
// executor.terminateStateOnError(state, "FormatString",
1289-
// StateTerminationType::User);
1280+
char *end = nullptr;
1281+
size_t sink = strtoul(arguments[0]->toString().c_str(), &end, 10);
1282+
if (*end != '\0' || errno == ERANGE) {
1283+
executor.terminateStateOnUserError(
1284+
state, "Incorrect argument 0 to klee_taint_sink_hit(size_t)");
1285+
}
1286+
1287+
executor.terminateStateOnTaintError(state, sink);
12901288
}

0 commit comments

Comments
 (0)