Skip to content

Commit 713f4a7

Browse files
ladisginladisgin
committed
[wip] remove instructionInfo
1 parent 915e90a commit 713f4a7

25 files changed

+803
-659
lines changed

‎include/klee/Core/Interpreter.h

+14-7
Original file line numberDiff line numberDiff line change
@@ -11,17 +11,18 @@
1111

1212
#include "TerminationTypes.h"
1313
#include "klee/Module/Annotation.h"
14-
1514
#include "klee/Module/SarifReport.h"
1615

1716
#include <cstdint>
18-
#include <map>
1917
#include <memory>
18+
#include <map>
2019
#include <set>
21-
#include <string>
20+
#include <unordered_set>
2221
#include <unordered_map>
22+
#include <string>
2323
#include <vector>
2424

25+
#include "llvm/ADT/StringRef.h"
2526
#include <nonstd/optional.hpp>
2627

2728
using nonstd::optional;
@@ -63,6 +64,12 @@ class InterpreterHandler {
6364
const char *suffix, bool isError = false) = 0;
6465
};
6566

67+
// TODO remove
68+
using FInstructions = std::unordered_map<
69+
std::string,
70+
std::unordered_map<
71+
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
72+
6673
enum class MockStrategy {
6774
None, // No mocks are generated
6875
Naive, // For each function call new symbolic value is generated
@@ -161,9 +168,9 @@ class Interpreter {
161168
setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
162169
std::vector<std::unique_ptr<llvm::Module>> &libsModules,
163170
const ModuleOptions &opts,
164-
const std::unordered_set<std::string> &mainModuleFunctions,
165-
const std::unordered_set<std::string> &mainModuleGlobals,
166-
std::unique_ptr<InstructionInfoTable> origInfos,
171+
std::set<llvm::StringRef> &mainModuleFunctions,
172+
std::set<llvm::StringRef> &mainModuleGlobals,
173+
FInstructions &&origInstructions,
167174
const std::set<std::string> &ignoredExternals,
168175
std::vector<std::pair<std::string, std::string>> redefinitions) = 0;
169176

@@ -217,7 +224,7 @@ class Interpreter {
217224

218225
virtual void
219226
getCoveredLines(const ExecutionState &state,
220-
std::map<const std::string *, std::set<unsigned>> &res) = 0;
227+
std::map<std::string, std::set<size_t>> &res) = 0;
221228

222229
virtual void getBlockPath(const ExecutionState &state,
223230
std::string &blockPath) = 0;

‎include/klee/Module/InstructionInfoTable.h

+79-80
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
//===-- InstructionInfoTable.h ----------------------------------*- C++ -*-===//
2-
//
3-
// The KLEE Symbolic Virtual Machine
4-
//
5-
// This file is distributed under the University of Illinois Open Source
6-
// License. See LICENSE.TXT for details.
7-
//
8-
//===----------------------------------------------------------------------===//
1+
////===-- InstructionInfoTable.h ----------------------------------*- C++ -*-===//
2+
////
3+
//// The KLEE Symbolic Virtual Machine
4+
////
5+
//// This file is distributed under the University of Illinois Open Source
6+
//// License. See LICENSE.TXT for details.
7+
////
8+
////===----------------------------------------------------------------------===//
99

1010
#ifndef KLEE_INSTRUCTIONINFOTABLE_H
1111
#define KLEE_INSTRUCTIONINFOTABLE_H
@@ -31,82 +31,81 @@ class Module;
3131

3232
namespace klee {
3333

34-
/// @brief InstructionInfo stores debug information for a KInstruction.
35-
struct InstructionInfo {
36-
/// @brief The instruction id.
37-
unsigned id;
38-
/// @brief Line number in source file.
39-
unsigned line;
40-
/// @brief Column number in source file.
41-
unsigned column;
42-
/// @brief Line number in generated assembly.ll.
43-
llvm::Optional<uint64_t> assemblyLine;
44-
/// @brief Source file name.
45-
const std::string &file;
46-
47-
public:
48-
InstructionInfo(unsigned id, const std::string &file, unsigned line,
49-
unsigned column, llvm::Optional<uint64_t> assemblyLine)
50-
: id{id}, line{line}, column{column},
51-
assemblyLine{assemblyLine}, file{file} {}
52-
};
53-
54-
/// @brief FunctionInfo stores debug information for a KFunction.
55-
struct FunctionInfo {
56-
/// @brief The function id.
57-
unsigned id;
58-
/// @brief Line number in source file.
59-
unsigned line;
60-
/// @brief Line number in generated assembly.ll.
61-
llvm::Optional<uint64_t> assemblyLine;
62-
/// @brief Source file name.
63-
const std::string &file;
64-
65-
public:
66-
FunctionInfo(unsigned id, const std::string &file, unsigned line,
67-
llvm::Optional<uint64_t> assemblyLine)
68-
: id{id}, line{line}, assemblyLine{assemblyLine}, file{file} {}
69-
70-
FunctionInfo(const FunctionInfo &) = delete;
71-
FunctionInfo &operator=(FunctionInfo const &) = delete;
72-
73-
FunctionInfo(FunctionInfo &&) = default;
34+
//// TODO move to methods of kInstruction
35+
///// @brief InstructionInfo stores debug information for a KInstruction.
36+
//struct InstructionInfo {
37+
// /// @brief The instruction id.
38+
//// unsigned id; // TODO move to kInstruction
39+
// /// @brief Line number in source file.
40+
// // unsigned line;
41+
// /// @brief Column number in source file.
42+
// // unsigned column;
43+
// /// @brief Line number in generated assembly.ll.
44+
//// llvm::Optional<uint64_t> assemblyLine;
45+
// /// @brief Source file name.
46+
//// const std::string &file;
47+
//
48+
//public:
49+
// InstructionInfo(unsigned id) {}
50+
//};
51+
//
52+
///// @brief FunctionInfo stores debug information for a KFunction.
53+
//struct FunctionInfo { // TODO clear this too
54+
// /// @brief The function id.
55+
//// unsigned id; // TODO move to kFunction
56+
// /// @brief Line number in source file.
57+
//// unsigned line;
58+
// /// @brief Line number in generated assembly.ll.
59+
//// llvm::Optional<uint64_t> assemblyLine;
60+
// /// @brief Source file name.
61+
//// const std::string &file;
62+
//
63+
//public:
64+
// FunctionInfo(unsigned id) {}
65+
//
66+
// FunctionInfo(const FunctionInfo &) = delete;
67+
// FunctionInfo &operator=(FunctionInfo const &) = delete;
68+
//
69+
// FunctionInfo(FunctionInfo &&) = default;
70+
//};
71+
//
72+
//class InstructionInfoTable {
73+
//public:
74+
// using LocationToFunctionsMap =
75+
// std::unordered_map<std::string,
76+
// std::unordered_set<const llvm::Function *>>;
77+
//
78+
//private:
79+
// std::unordered_map<const llvm::Instruction *,
80+
// std::unique_ptr<InstructionInfo>> infos;
81+
// std::unordered_map<const llvm::Function *, std::unique_ptr<FunctionInfo>>
82+
// functionInfos;
83+
// LocationToFunctionsMap fileNameToFunctions; // TODO remove
84+
//// Instructions insts; // TODO remove when move prepare target to main
85+
//
86+
//public:
87+
// explicit InstructionInfoTable(
88+
// const llvm::Module &m);
89+
//
90+
//// unsigned getMaxID() const;
91+
// const InstructionInfo &getInfo(const llvm::Instruction &) const;
92+
// const FunctionInfo &getFunctionInfo(const llvm::Function &) const;
93+
// const LocationToFunctionsMap &getFileNameToFunctions() const;
94+
//// Instructions getInstructions();
95+
//};
96+
97+
struct LocationInfo {
98+
std::string file;
99+
size_t line;
100+
size_t column;
74101
};
75102

76-
class InstructionInfoTable {
77-
public:
78-
using Instructions = std::unordered_map<
79-
std::string,
80-
std::unordered_map<
81-
unsigned int,
82-
std::unordered_map<unsigned int, std::unordered_set<unsigned int>>>>;
83-
using LocationToFunctionsMap =
84-
std::unordered_map<std::string,
85-
std::unordered_set<const llvm::Function *>>;
86103

87-
private:
88-
std::unordered_map<const llvm::Instruction *,
89-
std::unique_ptr<InstructionInfo>>
90-
infos;
91-
std::unordered_map<const llvm::Function *, std::unique_ptr<FunctionInfo>>
92-
functionInfos;
93-
LocationToFunctionsMap fileNameToFunctions;
94-
std::vector<std::unique_ptr<std::string>> internedStrings;
95-
std::unordered_set<std::string> filesNames;
96-
Instructions insts;
104+
// TODO need unify with kFunction
105+
LocationInfo getLocationInfo(const llvm::Function *func);
97106

98-
public:
99-
explicit InstructionInfoTable(
100-
const llvm::Module &m, std::unique_ptr<llvm::raw_fd_ostream> assemblyFS,
101-
bool withInstructions = false);
102-
103-
unsigned getMaxID() const;
104-
const InstructionInfo &getInfo(const llvm::Instruction &) const;
105-
const FunctionInfo &getFunctionInfo(const llvm::Function &) const;
106-
const LocationToFunctionsMap &getFileNameToFunctions() const;
107-
const std::unordered_set<std::string> &getFilesNames() const;
108-
Instructions getInstructions();
109-
};
107+
// TODO need unify with kInstruction
108+
LocationInfo getLocationInfo(const llvm::Instruction *inst);
110109

111110
} // namespace klee
112111

‎include/klee/Module/KInstruction.h

+41-13
Original file line numberDiff line numberDiff line change
@@ -11,15 +11,14 @@
1111
#define KLEE_KINSTRUCTION_H
1212

1313
#include "klee/Config/Version.h"
14-
#include "klee/Module/InstructionInfoTable.h"
15-
1614
#include "klee/Support/CompilerWarning.h"
1715
DISABLE_WARNING_PUSH
1816
DISABLE_WARNING_DEPRECATED_DECLARATIONS
1917
#include "llvm/Support/DataTypes.h"
2018
#include "llvm/Support/raw_ostream.h"
2119
DISABLE_WARNING_POP
2220

21+
#include <optional>
2322
#include <vector>
2423

2524
namespace llvm {
@@ -28,34 +27,57 @@ class Instruction;
2827

2928
namespace klee {
3029
class Executor;
31-
struct InstructionInfo;
3230
class KModule;
31+
struct KFunction;
3332
struct KBlock;
3433

3534
/// KInstruction - Intermediate instruction representation used
3635
/// during execution.
3736
struct KInstruction {
3837
llvm::Instruction *inst;
39-
const InstructionInfo *info;
38+
// const InstructionInfo *info; // TODO remove it
4039

4140
/// Value numbers for each operand. -1 is an invalid value,
4241
/// otherwise negative numbers are indices (negated and offset by
4342
/// 2) into the module constant table and positive numbers are
4443
/// register indices.
4544
int *operands;
46-
/// Destination register index.
47-
unsigned dest;
4845
KBlock *parent;
4946

47+
private:
5048
// Instruction index in the basic block
51-
unsigned index;
49+
const unsigned globalIndex;
5250

51+
/// Destination register index.
52+
// unsigned dest;
5353
public:
54-
KInstruction() = default;
55-
explicit KInstruction(const KInstruction &ki);
54+
/// Unique index for KFunction and KInstruction inside KModule
55+
/// from 0 to [KFunction + KInstruction]
56+
[[nodiscard]] unsigned getGlobalIndex() const;
57+
/// Instruction index in the basic block
58+
[[nodiscard]] unsigned getIndex() const;
59+
/// Destination register index.
60+
[[nodiscard]] unsigned getDest() const;
61+
62+
KInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
63+
&_instructionToRegisterMap,
64+
llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
65+
unsigned &_globalIndexInc);
66+
67+
KInstruction() = delete; // TODO remove default constructor
68+
explicit KInstruction(const KInstruction &ki) = delete;
5669
virtual ~KInstruction();
57-
std::string getSourceLocation() const;
58-
std::string toString() const;
70+
71+
[[nodiscard]] size_t getLine() const;
72+
[[nodiscard]] size_t getColumn() const;
73+
[[nodiscard]] std::string getSourceFilepath() const;
74+
75+
[[nodiscard]] std::string getSourceLocationString() const;
76+
[[nodiscard]] std::string toString() const;
77+
78+
[[nodiscard]] KBlock *getKBlock() const;
79+
[[nodiscard]] KFunction *getKFunction() const;
80+
[[nodiscard]] KModule *getKModule() const;
5981
};
6082

6183
struct KGEPInstruction : KInstruction {
@@ -70,8 +92,14 @@ struct KGEPInstruction : KInstruction {
7092
uint64_t offset;
7193

7294
public:
73-
KGEPInstruction() = default;
74-
explicit KGEPInstruction(const KGEPInstruction &ki);
95+
KGEPInstruction(const std::unordered_map<llvm::Instruction *, unsigned>
96+
&_instructionToRegisterMap,
97+
llvm::Instruction *_inst, KModule *_km, KBlock *_kb,
98+
unsigned &_globalIndexInc)
99+
: KInstruction(_instructionToRegisterMap, _inst, _km, _kb,
100+
_globalIndexInc) {}
101+
KGEPInstruction() = delete;
102+
explicit KGEPInstruction(const KGEPInstruction &ki) = delete;
75103
};
76104
} // namespace klee
77105

0 commit comments

Comments
 (0)