Skip to content

Commit 3340a08

Browse files
Lana243misonijnik
authored andcommitted
Add mocks:
- Generation in two modes: naive and determinitic - Mocks are reproducible - Special mocks for allocators: malloc, calloc, realloc
1 parent 7f6fd2d commit 3340a08

32 files changed

Lines changed: 957 additions & 45 deletions

.github/workflows/build.yaml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,7 @@ jobs:
146146
runs-on: macos-latest
147147
env:
148148
BASE: /tmp
149+
LLVM_VERSION: 11
149150
SOLVERS: STP
150151
UCLIBC_VERSION: 0
151152
USE_TCMALLOC: 0

include/klee/Core/Interpreter.h

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ class BasicBlock;
2929
class Function;
3030
class LLVMContext;
3131
class Module;
32+
class Type;
3233
class raw_ostream;
3334
class raw_fd_ostream;
3435
} // namespace llvm
@@ -63,6 +64,13 @@ using FLCtoOpcode = std::unordered_map<
6364
std::unordered_map<
6465
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
6566

67+
enum class MockStrategy {
68+
None, // No mocks are generated
69+
Naive, // For each function call new symbolic value is generated
70+
Deterministic, // Each function is treated as uninterpreted function in SMT.
71+
// Compatible with Z3 solver only
72+
};
73+
6674
class Interpreter {
6775
public:
6876
enum class GuidanceKind {
@@ -79,6 +87,8 @@ class Interpreter {
7987
std::string LibraryDir;
8088
std::string EntryPoint;
8189
std::string OptSuffix;
90+
std::string MainCurrentName;
91+
std::string MainNameAfterMock;
8292
bool Optimize;
8393
bool Simplify;
8494
bool CheckDivZero;
@@ -88,13 +98,16 @@ class Interpreter {
8898

8999
ModuleOptions(const std::string &_LibraryDir,
90100
const std::string &_EntryPoint, const std::string &_OptSuffix,
91-
bool _Optimize, bool _Simplify, bool _CheckDivZero,
92-
bool _CheckOvershift, bool _WithFPRuntime,
93-
bool _WithPOSIXRuntime)
101+
const std::string &_MainCurrentName,
102+
const std::string &_MainNameAfterMock, bool _Optimize,
103+
bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
104+
bool _WithFPRuntime, bool _WithPOSIXRuntime)
94105
: LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
95-
OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify),
96-
CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift),
97-
WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
106+
OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
107+
MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize),
108+
Simplify(_Simplify), CheckDivZero(_CheckDivZero),
109+
CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime),
110+
WithPOSIXRuntime(_WithPOSIXRuntime) {}
98111
};
99112

100113
enum LogType {
@@ -112,10 +125,11 @@ class Interpreter {
112125
unsigned MakeConcreteSymbolic;
113126
GuidanceKind Guidance;
114127
std::optional<SarifReport> Paths;
128+
enum MockStrategy MockStrategy;
115129

116130
InterpreterOptions(std::optional<SarifReport> Paths)
117131
: MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
118-
Paths(std::move(Paths)) {}
132+
Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {}
119133
};
120134

121135
protected:
@@ -144,7 +158,11 @@ class Interpreter {
144158
const ModuleOptions &opts,
145159
std::set<std::string> &&mainModuleFunctions,
146160
std::set<std::string> &&mainModuleGlobals,
147-
FLCtoOpcode &&origInstructions) = 0;
161+
FLCtoOpcode &&origInstructions,
162+
const std::set<std::string> &ignoredExternals) = 0;
163+
164+
virtual std::map<std::string, llvm::Type *>
165+
getAllExternals(const std::set<std::string> &ignoredExternals) = 0;
148166

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

include/klee/Core/MockBuilder.h

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
#ifndef KLEE_MOCKBUILDER_H
2+
#define KLEE_MOCKBUILDER_H
3+
4+
#include "llvm/IR/IRBuilder.h"
5+
#include "llvm/IR/Module.h"
6+
7+
#include <set>
8+
#include <string>
9+
10+
namespace klee {
11+
12+
class MockBuilder {
13+
private:
14+
const llvm::Module *userModule;
15+
std::unique_ptr<llvm::Module> mockModule;
16+
std::unique_ptr<llvm::IRBuilder<>> builder;
17+
std::map<std::string, llvm::Type *> externals;
18+
19+
const std::string mockEntrypoint, userEntrypoint;
20+
21+
void initMockModule();
22+
void buildMockMain();
23+
void buildExternalGlobalsDefinitions();
24+
void buildExternalFunctionsDefinitions();
25+
void buildCallKleeMakeSymbol(const std::string &klee_function_name,
26+
llvm::Value *source, llvm::Type *type,
27+
const std::string &symbol_name);
28+
29+
public:
30+
MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
31+
std::string userEntrypoint,
32+
std::map<std::string, llvm::Type *> externals);
33+
34+
std::unique_ptr<llvm::Module> build();
35+
};
36+
37+
} // namespace klee
38+
39+
#endif // KLEE_MOCKBUILDER_H

include/klee/Expr/SourceBuilder.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33

44
#include "klee/Expr/SymbolicSource.h"
55

6+
#include "llvm/IR/Function.h"
7+
68
namespace klee {
79

810
class KInstruction;
@@ -39,6 +41,12 @@ class SourceBuilder {
3941
static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
4042
KModule *km);
4143
static ref<SymbolicSource> irreproducible(const std::string &name);
44+
static ref<SymbolicSource> mockNaive(const KModule *kModule,
45+
const llvm::Function &kFunction,
46+
unsigned version);
47+
static ref<SymbolicSource>
48+
mockDeterministic(const KModule *kModule, const llvm::Function &kFunction,
49+
const std::vector<ref<Expr>> &args);
4250
static ref<SymbolicSource> alpha(int _index);
4351
};
4452

include/klee/Expr/SymbolicSource.h

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,13 @@ DISABLE_WARNING_POP
2020

2121
namespace klee {
2222

23+
class Expr;
2324
class Array;
2425
class Expr;
2526
class ConstantExpr;
2627
struct KGlobalVariable;
2728
class KModule;
29+
struct KFunction;
2830
struct KValue;
2931
struct KInstruction;
3032

@@ -48,6 +50,8 @@ class SymbolicSource {
4850
Instruction,
4951
Argument,
5052
Irreproducible,
53+
MockNaive,
54+
MockDeterministic,
5155
Alpha
5256
};
5357

@@ -383,6 +387,58 @@ class AlphaSource : public SymbolicSource {
383387
}
384388
};
385389

390+
class MockSource : public SymbolicSource {
391+
public:
392+
const KModule *km;
393+
const llvm::Function &function;
394+
MockSource(const KModule *_km, const llvm::Function &_function)
395+
: km(_km), function(_function) {}
396+
397+
static bool classof(const SymbolicSource *S) {
398+
return S->getKind() == Kind::MockNaive ||
399+
S->getKind() == Kind::MockDeterministic;
400+
}
401+
};
402+
403+
class MockNaiveSource : public MockSource {
404+
public:
405+
const unsigned version;
406+
407+
MockNaiveSource(const KModule *km, const llvm::Function &function,
408+
unsigned _version)
409+
: MockSource(km, function), version(_version) {}
410+
411+
Kind getKind() const override { return Kind::MockNaive; }
412+
std::string getName() const override { return "mockNaive"; }
413+
414+
static bool classof(const SymbolicSource *S) {
415+
return S->getKind() == Kind::MockNaive;
416+
}
417+
418+
unsigned computeHash() override;
419+
420+
int internalCompare(const SymbolicSource &b) const override;
421+
};
422+
423+
class MockDeterministicSource : public MockSource {
424+
public:
425+
const std::vector<ref<Expr>> args;
426+
427+
MockDeterministicSource(const KModule *_km, const llvm::Function &_function,
428+
const std::vector<ref<Expr>> &_args);
429+
430+
Kind getKind() const override { return Kind::MockDeterministic; }
431+
std::string getName() const override { return "mockDeterministic"; }
432+
433+
static bool classof(const SymbolicSource *S) {
434+
return S->getKind() == Kind::MockDeterministic;
435+
}
436+
437+
unsigned computeHash() override;
438+
439+
int internalCompare(const SymbolicSource &b) const override;
440+
};
441+
386442
} // namespace klee
387443

388444
#endif /* KLEE_SYMBOLICSOURCE_H */

include/klee/klee.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -201,5 +201,6 @@ long double klee_rintl(long double d);
201201
// stdin/stdout
202202
void klee_init_env(int *argcPtr, char ***argvPtr);
203203
void check_stdin_read();
204+
void *__klee_wrapped_malloc(size_t size);
204205

205206
#endif /* KLEE_H */

lib/Core/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ add_library(kleeCore
2222
Memory.cpp
2323
MemoryManager.cpp
2424
PForest.cpp
25+
MockBuilder.cpp
2526
PTree.cpp
2627
Searcher.cpp
2728
SeedInfo.cpp

lib/Core/ExecutionState.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
2525
#include "llvm/IR/Function.h"
2626
#include "llvm/Support/CommandLine.h"
2727
#include "llvm/Support/raw_ostream.h"
28+
#include "klee/Support/ErrorHandling.h"
2829
DISABLE_WARNING_POP
2930

3031
#include <cassert>

0 commit comments

Comments
 (0)