Skip to content

Commit c268b2f

Browse files
committed
Reset module after installing concolic primitives
This will trigger the module to resolve it's primitives again so they are not stuck using the old primitives if a snapshot is loaded.
1 parent 3b77ffa commit c268b2f

2 files changed

Lines changed: 5 additions & 4 deletions

File tree

platforms/CLI-Emulator/main.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -688,6 +688,7 @@ bool push_symbolic_int(Module *m, const std::string &primitive_origin,
688688
}
689689

690690
void install_concolic_primitives(Interpreter *interpreter) {
691+
dbg_info("INSTALLING CONCOLIC PRIMITIVES\n");
691692
// Make the following primitives not print anything in concolic mode.
692693
interpreter->register_primitive(
693694
"chip_pin_mode",
@@ -787,6 +788,8 @@ void run_concolic(const std::vector<std::string>& snapshot_messages, int max_ins
787788
const auto start{std::chrono::steady_clock::now()};
788789
wac->setInterpreter(new ConcolicInterpreter());
789790
install_concolic_primitives(wac->interpreter);
791+
// This will trigger the module to resolve all primitives again.
792+
m->warduino->reset_module(m);
790793

791794
// Has a big impact on performance, for example if you have a simple program
792795
// with a loop that contains an if statement and, you run the loop 30 times
@@ -820,10 +823,7 @@ void run_concolic(const std::vector<std::string>& snapshot_messages, int max_ins
820823
} else {
821824
//wac->instantiate_module(m);
822825
//wac->instantiate_module(m, m->bytes, m->byte_count);
823-
// TODO: Introduce a reset module function
824-
auto wasm = (uint8_t *)malloc(sizeof(uint8_t) * m->byte_count);
825-
memcpy(wasm, m->bytes, m->byte_count);
826-
m->warduino->update_module(m, wasm, m->byte_count);
826+
m->warduino->reset_module(m);
827827
m->warduino->program_state = WARDUINOrun;
828828
success = wac->run_module(m);
829829
}

src/Interpreter/interpreter.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ class Interpreter {
7979
}
8080

8181
void register_primitive(const PrimitiveEntry &entry) {
82+
dbg_info("installing primitive %s\n", entry.name);
8283
primitives[entry.name] = entry;
8384
}
8485

0 commit comments

Comments
 (0)