Skip to content

Commit e4ac385

Browse files
add an option to use immutable data structure
1 parent f63f682 commit e4ac385

File tree

3 files changed

+103
-7
lines changed

3 files changed

+103
-7
lines changed

headers/wasm/config.hpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,4 +33,12 @@ static const bool REUSE_SNAPSHOT = false;
3333
static const bool REUSE_SNAPSHOT = true;
3434
#endif
3535

36+
// If we use immutable data structures for symbolic states to reduce the cost of
37+
// copying.
38+
#ifdef USE_IMM
39+
static const bool IMMUTABLE_SYMS = true;
40+
#else
41+
static const bool IMMUTABLE_SYMS = false;
42+
#endif
43+
3644
#endif // CONFIG_HPP

headers/wasm/profile.hpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
#ifndef PROFILE_HPP
22
#define PROFILE_HPP
33

4-
#include "utils.hpp"
54
#include "config.hpp"
5+
#include "utils.hpp"
66
#include <array>
77
#include <chrono>
88
#include <iomanip>

headers/wasm/symbolic_rt.hpp

Lines changed: 94 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@
55
#include "config.hpp"
66
#include "controls.hpp"
77
#include "heap_mem_bookkeeper.hpp"
8+
#include "immer/map.hpp"
9+
#include "immer/map_transient.hpp"
10+
#include "immer/vector_transient.hpp"
811
#include "profile.hpp"
912
#include "utils.hpp"
1013
#include <cassert>
@@ -238,47 +241,81 @@ class SymStack_t {
238241
printf("[Debug] poping from stack, size of symbolic stack is: %zu\n",
239242
stack.size());
240243
#endif
244+
#ifdef USE_IMM
245+
auto ret = *(stack.end() - 1);
246+
stack.take(stack.size() - 1);
247+
return ret;
248+
#else
241249
auto ret = stack.back();
242250
stack.pop_back();
243251
return ret;
252+
#endif
244253
}
245254

246-
SymVal peek() { return stack.back(); }
255+
SymVal peek() { return *(stack.end() - 1); }
247256

248257
std::monostate shift(int32_t offset, int32_t size) {
249258
auto n = stack.size();
250259
for (size_t i = n - size; i < n; ++i) {
251260
assert(i - offset >= 0);
261+
#ifdef USE_IMM
262+
stack.set(i - offset, stack[i]);
263+
#else
252264
stack[i - offset] = stack[i];
265+
#endif
253266
}
267+
#ifdef USE_IMM
268+
stack.take(n - offset);
269+
#else
254270
stack.resize(n - offset);
271+
#endif
255272
return std::monostate();
256273
}
257274

258275
void reset() {
259-
// Reset the symbolic stack
276+
// Reset the symbolic stack
277+
#ifdef USE_IMM
278+
stack = immer::vector_transient<SymVal>();
279+
#else
260280
stack.clear();
281+
#endif
261282
}
262283

263284
size_t size() const { return stack.size(); }
264285

265286
SymVal operator[](size_t index) const { return stack[index]; }
266287

267288
private:
289+
#ifdef USE_IMM
290+
immer::vector_transient<SymVal> stack;
291+
#else
268292
std::vector<SymVal> stack;
293+
#endif
269294
};
270295

271296
static SymStack_t SymStack;
272297

273298
class SymFrames_t {
299+
274300
public:
275301
void pushFrame(int size) {
276302
// Push a new frame with the given size
303+
#ifdef USE_IMM
304+
for (int i = 0; i < size; ++i) {
305+
stack.push_back(SymVal());
306+
}
307+
#else
277308
stack.resize(size + stack.size());
309+
#endif
278310
}
279311
std::monostate popFrame(int size) {
280312
// Pop the frame of the given size
313+
314+
#ifdef USE_IMM
315+
stack.take(stack.size() - size);
316+
#else
281317
stack.resize(stack.size() - size);
318+
#endif
282319
return std::monostate();
283320
}
284321

@@ -291,40 +328,79 @@ class SymFrames_t {
291328
void set(int index, SymVal val) {
292329
// Set the symbolic value at the given index
293330
assert(val.symptr != nullptr);
331+
#ifdef USE_IMM
332+
stack.set(stack.size() - 1 - index, val);
333+
#else
294334
stack[stack.size() - 1 - index] = val;
335+
#endif
295336
}
296337

297338
void reset() {
298339
// Reset the symbolic frames
340+
341+
#ifdef USE_IMM
342+
stack = immer::vector_transient<SymVal>();
343+
#else
299344
stack.clear();
345+
#endif
300346
}
301347

302348
size_t size() const { return stack.size(); }
303349

304350
SymVal operator[](size_t index) const { return stack[index]; }
305351

306352
private:
353+
#ifdef USE_IMM
354+
immer::vector_transient<SymVal> stack;
355+
#else
307356
std::vector<SymVal> stack;
357+
#endif
308358
};
309359

310360
struct NodeBox;
311361
struct SymEnv_t;
312362

313363
class SymMemory_t {
314364
public:
365+
#ifdef USE_IMM
366+
immer::map_transient<int, SymVal> memory;
367+
#else
315368
std::unordered_map<int, SymVal> memory;
369+
#endif
316370

317371
SymVal loadSymByte(int32_t addr) {
318-
// if the address is not in the memory, it must be a zero-initialized memory
372+
// if the address is not in the memory, it must be a zero-initialized memory
373+
#ifdef USE_IMM
319374
auto it = memory.find(addr);
320-
SymVal s = (it != memory.end())
321-
? it->second
322-
: SymVal(SymBookKeeper.allocate<SmallBV>(8, 0));
375+
if (it != nullptr) {
376+
return *it;
377+
} else {
378+
auto s = SymVal(ZeroByte);
379+
return s;
380+
}
381+
#else
382+
auto it = memory.find(addr);
383+
SymVal s = (it != memory.end()) ? it->second : SymVal(ZeroByte);
323384
return s;
385+
#endif
324386
}
325387

326388
SymVal loadSym(int32_t base, int32_t offset) {
327389
// calculate the real address
390+
391+
#ifdef USE_IMM
392+
int32_t addr = base + offset;
393+
auto it = memory.find(addr);
394+
SymVal s0 = it ? *it : SymVal(ZeroByte);
395+
it = memory.find(addr + 1);
396+
SymVal s1 = it ? *it : SymVal(ZeroByte);
397+
it = memory.find(addr + 2);
398+
SymVal s2 = it ? *it : SymVal(ZeroByte);
399+
it = memory.find(addr + 3);
400+
SymVal s3 = it ? *it : SymVal(ZeroByte);
401+
402+
return s3.concat(s2).concat(s1).concat(s0);
403+
#else
328404
int32_t addr = base + offset;
329405
auto it = memory.find(addr);
330406
SymVal s0 = (it != memory.end()) ? it->second : SymVal(ZeroByte);
@@ -336,6 +412,7 @@ class SymMemory_t {
336412
SymVal s3 = (it != memory.end()) ? it->second : SymVal(ZeroByte);
337413

338414
return s3.concat(s2).concat(s1).concat(s0);
415+
#endif
339416
}
340417

341418
// when loading a symval, we need to concat 4 symbolic values
@@ -349,15 +426,26 @@ class SymMemory_t {
349426
SymVal s1 = value.extract(2, 2);
350427
SymVal s2 = value.extract(3, 3);
351428
SymVal s3 = value.extract(4, 4);
429+
#ifdef USE_IMM
430+
memory.set(addr, s0);
431+
memory.set(addr + 1, s1);
432+
memory.set(addr + 2, s2);
433+
memory.set(addr + 3, s3);
434+
#else
352435
memory[addr] = s0;
353436
memory[addr + 1] = s1;
354437
memory[addr + 2] = s2;
355438
memory[addr + 3] = s3;
439+
#endif
356440
return std::monostate{};
357441
}
358442

359443
std::monostate reset() {
444+
#ifdef USE_IMM
445+
memory = immer::map_transient<int, SymVal>();
446+
#else
360447
memory.clear();
448+
#endif
361449
return std::monostate{};
362450
}
363451
};

0 commit comments

Comments
 (0)