@@ -688,6 +688,7 @@ bool push_symbolic_int(Module *m, const std::string &primitive_origin,
688688}
689689
690690void 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
@@ -818,12 +821,7 @@ void run_concolic(const std::vector<std::string>& snapshot_messages, int max_ins
818821 m->create_symbolic_state ();
819822 success = wac->interpreter ->interpret (m);
820823 } else {
821- // wac->instantiate_module(m);
822- // 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 );
824+ m->warduino ->reset_module (m);
827825 m->warduino ->program_state = WARDUINOrun;
828826 success = wac->run_module (m);
829827 }
0 commit comments