Skip to content

Commit ab2cd9d

Browse files
committed
[wip] Uninitialized Memory
1 parent b9794c2 commit ab2cd9d

40 files changed

+811
-489
lines changed

include/klee/ADT/Ref.h

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,13 @@ template <class T> class ref {
205205

206206
// assumes non-null arguments
207207
bool equals(const ref &rhs) const {
208-
assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");
208+
if (isNull() && rhs.isNull()) {
209+
return true;
210+
}
211+
if (isNull() || rhs.isNull()) {
212+
return false;
213+
}
214+
// assert(!isNull() && !rhs.isNull() && "Invalid call to compare()");
209215
return get()->equals(*rhs.get());
210216
}
211217

include/klee/ADT/SparseStorage.h

Lines changed: 51 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#ifndef KLEE_SPARSESTORAGE_H
22
#define KLEE_SPARSESTORAGE_H
33

4+
#include "klee/ADT/Ref.h"
5+
#include <algorithm>
46
#include <cassert>
57
#include <cstddef>
68
#include <iterator>
@@ -12,31 +14,47 @@ namespace llvm {
1214
class raw_ostream;
1315
};
1416

17+
1518
namespace klee {
1619

20+
enum class Density {
21+
Sparse,
22+
Dense,
23+
};
24+
1725
template <typename ValueType> class SparseStorage {
1826
private:
1927
std::unordered_map<size_t, ValueType> internalStorage;
2028
ValueType defaultValue;
21-
size_t rangeSize = 0;
2229

2330
bool contains(size_t key) const { return internalStorage.count(key) != 0; }
2431

2532
public:
2633
SparseStorage(const ValueType &defaultValue = ValueType())
2734
: defaultValue(defaultValue) {}
2835

36+
SparseStorage(const std::unordered_map<size_t, ValueType> &internalStorage,
37+
const ValueType &defaultValue)
38+
: defaultValue(defaultValue) {
39+
for (auto &[index, value] : internalStorage) {
40+
store(index, value);
41+
}
42+
}
43+
2944
SparseStorage(const std::vector<ValueType> &values,
3045
const ValueType &defaultValue = ValueType())
3146
: defaultValue(defaultValue) {
3247
for (size_t idx = 0; idx < values.size(); ++idx) {
33-
internalStorage[idx] = values[idx];
48+
store(idx, values[idx]);
3449
}
3550
}
3651

3752
void store(size_t idx, const ValueType &value) {
53+
if (value == defaultValue) {
54+
internalStorage.erase(idx);
55+
} else {
3856
internalStorage[idx] = value;
39-
rangeSize = std::max(rangeSize, idx + 1);
57+
}
4058
}
4159

4260
template <typename InputIterator>
@@ -52,12 +70,15 @@ template <typename ValueType> class SparseStorage {
5270
}
5371

5472
size_t sizeOfSetRange() const {
55-
return rangeSize;
73+
size_t sizeOfRange = 0;
74+
for (auto i : internalStorage) {
75+
sizeOfRange = std::max(i.first, sizeOfRange);
76+
}
77+
return sizeOfRange;
5678
}
5779

5880
bool operator==(const SparseStorage<ValueType> &another) const {
59-
return defaultValue == another.defaultValue &&
60-
compare(another) == 0;
81+
return defaultValue == another.defaultValue && compare(another) == 0;
6182
}
6283

6384
bool operator!=(const SparseStorage<ValueType> &another) const {
@@ -73,46 +94,56 @@ template <typename ValueType> class SparseStorage {
7394
}
7495

7596
int compare(const SparseStorage<ValueType> &other) const {
76-
std::map<size_t, ValueType> thisMap;
77-
std::map<size_t, ValueType> otherMap;
78-
for (auto i : internalStorage) {
79-
thisMap.insert(i);
80-
}
81-
for (auto i : other.internalStorage) {
82-
otherMap.insert(i);
83-
}
84-
if (thisMap == otherMap) {
97+
auto ordered = calculateOrderedStorage();
98+
auto otherOrdered = other.calculateOrderedStorage();
99+
100+
if (ordered == otherOrdered) {
85101
return 0;
86102
} else {
87-
return thisMap < otherMap ? -1 : 1;
103+
return ordered < otherOrdered ? -1 : 1;
88104
}
89105
}
90106

107+
std::map<size_t, ValueType> calculateOrderedStorage() const {
108+
std::map<size_t, ValueType> ordered;
109+
for (const auto &i : internalStorage) {
110+
ordered.insert(i);
111+
}
112+
return ordered;
113+
}
114+
115+
std::vector<ValueType> getFirstNIndexes(size_t n) const {
116+
std::vector<ValueType> vectorized(n);
117+
for (size_t i = 0; i < n; i++) {
118+
vectorized[i] = load(i);
119+
}
120+
return vectorized;
121+
}
122+
91123
const std::unordered_map<size_t, ValueType> &storage() const {
92124
return internalStorage;
93125
};
126+
94127
const ValueType &defaultV() const { return defaultValue; };
95128

96129
void reset() {
97130
internalStorage.clear();
98-
rangeSize = 0;
99131
}
100132

101133
void reset(ValueType newDefault) {
102134
defaultValue = newDefault;
103135
internalStorage.clear();
104-
rangeSize = 0;
105136
}
106137

107138
// Specialized for unsigned char in .cpp
108-
void print(llvm::raw_ostream &os) const;
139+
void print(llvm::raw_ostream &os, Density) const;
109140
};
110141

111142
template <typename U>
112143
SparseStorage<unsigned char> sparseBytesFromValue(const U &value) {
113144
const unsigned char *valueUnsignedCharIterator =
114145
reinterpret_cast<const unsigned char *>(&value);
115-
SparseStorage<unsigned char> result(sizeof(value));
146+
SparseStorage<unsigned char> result;
116147
result.store(0, valueUnsignedCharIterator,
117148
valueUnsignedCharIterator + sizeof(value));
118149
return result;

include/klee/Expr/Expr.h

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -629,10 +629,7 @@ class Array {
629629

630630
public:
631631
bool isSymbolicArray() const { return !isConstantArray(); }
632-
bool isConstantArray() const {
633-
return isa<ConstantSource>(source) ||
634-
isa<SymbolicSizeConstantSource>(source);
635-
}
632+
bool isConstantArray() const;
636633

637634
const std::string getName() const { return source->toString(); }
638635
const std::string getIdentifier() const {

include/klee/Expr/Parser/Lexer.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ struct Token {
3232
KWFalse, ///< 'false'
3333
KWQuery, ///< 'query'
3434
KWPath, ///< 'path'
35+
KWDV, ///< 'DV'
36+
KWNull, ///< 'null'
3537
KWReserved, ///< fp[0-9]+([.].*)?, i[0-9]+
3638
KWSymbolic, ///< 'symbolic'
3739
KWTrue, ///< 'true'

include/klee/Expr/SourceBuilder.h

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
#define KLEE_SOURCEBUILDER_H
33

44
#include "klee/ADT/Ref.h"
5+
#include "klee/ADT/SparseStorage.h"
56
#include "klee/Expr/SymbolicSource.h"
67
#include "klee/Module/KModule.h"
78

@@ -12,10 +13,14 @@ class SourceBuilder {
1213
SourceBuilder() = delete;
1314

1415
static ref<SymbolicSource>
15-
constant(const std::vector<ref<ConstantExpr>> &constantValues);
16-
static ref<SymbolicSource> symbolicSizeConstant(unsigned defaultValue);
17-
static ref<SymbolicSource> symbolicSizeConstantAddress(unsigned defaultValue,
18-
unsigned version);
16+
constant(SparseStorage<ref<ConstantExpr>> constantValues);
17+
18+
static ref<SymbolicSource> uninitialized(unsigned version,
19+
const KInstruction *allocSite);
20+
static ref<SymbolicSource>
21+
symbolicSizeConstantAddress(unsigned version,
22+
const KInstruction *allocSite,
23+
ref<Expr> size);
1924
static ref<SymbolicSource> makeSymbolic(const std::string &name,
2025
unsigned version);
2126
static ref<SymbolicSource> lazyInitializationAddress(ref<Expr> pointer);
@@ -27,6 +32,7 @@ class SourceBuilder {
2732
int _index, KModule *km);
2833
static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
2934
KModule *km);
35+
static ref<SymbolicSource> global(const llvm::GlobalVariable &name);
3036
static ref<SymbolicSource> irreproducible(const std::string &name);
3137
};
3238

0 commit comments

Comments
 (0)