fixed a bug, zero initialize local variables

Author: butterunderflow

headers/wasm/concolic_driver.hpp

@@ -3,11 +3,11 @@
 
 #include "concrete_rt.hpp"
 #include "config.hpp"
+#include "output_report.hpp"
 #include "profile.hpp"
 #include "smt_solver.hpp"
 #include "symbolic_rt.hpp"
 #include "utils.hpp"
-#include "output_report.hpp"
 #include <cassert>
 #include <chrono>
 #include <functional>
@@ -103,13 +103,26 @@ inline void ConcolicDriver::main_exploration_loop() {
     try {
       GENSYM_INFO("Now execute the program with symbolic environment: ");
       GENSYM_INFO(SymEnv.to_string());
-      { node->reach_here(entrypoint); }
+      if (REUSE_SNAPSHOT) {
+        node->reach_here(entrypoint);
+      } else {
+        auto timer = ManagedTimer(TimeProfileKind::INSTR);
+        ExploreTree.reset_cursor();
+        reset_stacks();
+        entrypoint();
+      }
 
       GENSYM_INFO("Execution finished successfully with symbolic environment:");
       GENSYM_INFO(SymEnv.to_string());
     } catch (std::runtime_error &e) {
       std::cout << "Caught runtime error: " << e.what() << std::endl;
       ExploreTree.fillFailedNode();
+
+      if (std::string(e.what()) == "Symbolic assertion failed") {
+        GENSYM_INFO("Symbolic assertion failed, continuing to next path...");
+        continue;
+      }
+
       GENSYM_INFO("Caught runtime error with symbolic environment:");
       GENSYM_INFO(SymEnv.to_string());
       switch (EXPLORE_MODE) {

headers/wasm/concrete_rt.hpp

@@ -21,75 +21,115 @@ struct Num {
   int32_t toInt() const { return static_cast<int32_t>(value); }
   uint32_t toUInt() const { return static_cast<uint32_t>(value); }
 
+  // debug printer: enabled only when -DDEBUG
+  static inline void debug_print(const char *op, const Num &a, const Num &b,
+                                 const Num &res) {
+#ifdef DEBUG_OP
+    std::cout << "[Debug] " << op << ": lhs=" << static_cast<int32_t>(a.value)
+              << " rhs=" << static_cast<int32_t>(b.value)
+              << " -> res=" << static_cast<int32_t>(res.value) << std::endl;
+#endif
+  }
+
   // Helper to create a Wasm Boolean result (1 or 0 as Num)
-  Num WasmBool(bool condition) const { return Num(condition ? 1 : 0); }
+  Num WasmBool(bool condition) const {
+    Num res(condition ? 1 : 0);
+    debug_print("WasmBool", *this, *this, res);
+    return res;
+  }
   // TODO: support different bit width operations, for now we just assume all
   // oprands are i32
   // i32.eq (Equals): *this == other
   inline Num i32_eq(const Num &other) const {
-    return WasmBool(this->toUInt() == other.toUInt());
+    Num res = WasmBool(this->toUInt() == other.toUInt());
+    debug_print("i32.eq", *this, other, res);
+    return res;
   }
 
   // i32.ne (Not Equals): *this != other
   inline Num i32_ne(const Num &other) const {
-    return WasmBool(this->toUInt() != other.toUInt());
+    Num res = WasmBool(this->toUInt() != other.toUInt());
+    debug_print("i32.ne", *this, other, res);
+    return res;
   }
 
   // i32.lt_s (Signed Less Than): *this < other
   inline Num i32_lt_s(const Num &other) const {
-    return WasmBool(this->toInt() < other.toInt());
+    Num res = WasmBool(this->toInt() < other.toInt());
+    debug_print("i32.lt_s", *this, other, res);
+    return res;
   }
 
   // i32.lt_u (Unsigned Less Than): *this < other (unsigned)
   inline Num i32_lt_u(const Num &other) const {
-    return WasmBool(this->toUInt() < other.toUInt());
+    Num res = WasmBool(this->toUInt() < other.toUInt());
+    debug_print("i32.lt_u", *this, other, res);
+    return res;
   }
 
   // i32.le_s (Signed Less Than or Equal): *this <= other
   inline Num i32_le_s(const Num &other) const {
-    return WasmBool(this->toInt() <= other.toInt());
+    Num res = WasmBool(this->toInt() <= other.toInt());
+    debug_print("i32.le_s", *this, other, res);
+    return res;
   }
   // i32.le_u (Unsigned Less Than or Equal): *this <= other (unsigned)
   inline Num i32_le_u(const Num &other) const {
-    return WasmBool(this->toUInt() <= other.toUInt());
+    Num res = WasmBool(this->toUInt() <= other.toUInt());
+    debug_print("i32.le_u", *this, other, res);
+    return res;
   }
 
   // i32.gt_s (Signed Greater Than): *this > other
   inline Num i32_gt_s(const Num &other) const {
-    return WasmBool(this->toInt() > other.toInt());
+    Num res = WasmBool(this->toInt() > other.toInt());
+    debug_print("i32.gt_s", *this, other, res);
+    return res;
   }
 
   // i32.gt_u (Unsigned Greater Than): *this > other (unsigned)
   inline Num i32_gt_u(const Num &other) const {
-    return WasmBool(this->toUInt() > other.toUInt());
+    Num res = WasmBool(this->toUInt() > other.toUInt());
+    debug_print("i32.gt_u", *this, other, res);
+    return res;
   }
 
   // i32.ge_s (Signed Greater Than or Equal): *this >= other
   inline Num i32_ge_s(const Num &other) const {
-    return WasmBool(this->toInt() >= other.toInt());
+    Num res = WasmBool(this->toInt() >= other.toInt());
+    debug_print("i32.ge_s", *this, other, res);
+    return res;
   }
 
   // i32.ge_u (Unsigned Greater Than or Equal): *this >= other (unsigned)
   inline Num i32_ge_u(const Num &other) const {
-    return WasmBool(this->toUInt() >= other.toUInt());
+    Num res = WasmBool(this->toUInt() >= other.toUInt());
+    debug_print("i32.ge_u", *this, other, res);
+    return res;
   }
 
   // i32.add (Wrapping addition)
   inline Num i32_add(const Num &other) const {
     uint32_t result_u = this->toUInt() + other.toUInt();
-    return Num(static_cast<int32_t>(result_u));
+    Num res(static_cast<int32_t>(result_u));
+    debug_print("i32.add", *this, other, res);
+    return res;
   }
 
   // i32.sub (Wrapping subtraction)
   inline Num i32_sub(const Num &other) const {
     uint32_t result_u = this->toUInt() - other.toUInt();
-    return Num(static_cast<int32_t>(result_u));
+    Num res(static_cast<int32_t>(result_u));
+    debug_print("i32.sub", *this, other, res);
+    return res;
   }
 
   // i32.mul (Wrapping multiplication)
   inline Num i32_mul(const Num &other) const {
     uint32_t result_u = this->toUInt() * other.toUInt();
-    return Num(static_cast<int32_t>(result_u));
+    Num res(static_cast<int32_t>(result_u));
+    debug_print("i32.mul", *this, other, res);
+    return res;
   }
 
   // i32.div_s (Signed division with traps)
@@ -101,36 +141,46 @@ struct Num {
       throw std::runtime_error("i32.div_s: Division by zero");
     }
 
-    return Num(dividend / divisor);
+    Num res(dividend / divisor);
+    debug_print("i32.div_s", *this, other, res);
+    return res;
   }
 
   // i32.shl (Shift Left): *this << other (shift count masked by 31)
   inline Num i32_shl(const Num &other) const {
     uint32_t shift_amount = other.toUInt() & 0x1F;
     uint32_t result_u = toUInt() << shift_amount;
-    return Num(static_cast<int32_t>(result_u));
+    Num res(static_cast<int32_t>(result_u));
+    debug_print("i32.shl", *this, other, res);
+    return res;
   }
 
   // i32.shr_s (Signed Shift Right): *this >> other (Arithmetic shift)
   inline Num i32_shr_s(const Num &other) const {
     // Wasm masks the shift amount by 31 (0x1F)
     uint32_t shift_amount = other.toUInt() & 0x1F;
     int32_t result_s = toInt() >> shift_amount;
-    return Num(result_s);
+    Num res(result_s);
+    debug_print("i32.shr_s", *this, other, res);
+    return res;
   }
 
   // i32.shr_u (Unsigned Shift Right): *this >>> other (Logical shift)
   inline Num i32_shr_u(const Num &other) const {
     // Wasm masks the shift amount by 31 (0x1F)
     uint32_t shift_amount = other.toUInt() & 0x1F;
     uint32_t result_u = toUInt() >> shift_amount;
-    return Num(static_cast<int32_t>(result_u));
+    Num res(static_cast<int32_t>(result_u));
+    debug_print("i32.shr_u", *this, other, res);
+    return res;
   }
 
   // i32.and (Bitwise AND)
   inline Num i32_and(const Num &other) const {
     uint32_t result_u = this->toUInt() & other.toUInt();
-    return Num(static_cast<int32_t>(result_u));
+    Num res(static_cast<int32_t>(result_u));
+    debug_print("i32.and", *this, other, res);
+    return res;
   }
 };
 
@@ -272,6 +322,10 @@ class Frames_t {
   void pushFrame(std::int32_t size) {
     assert(size >= 0);
     count += size;
+    // Zero-initialize the new stack frames.
+    for (std::int32_t i = 0; i < size; ++i) {
+      stack_ptr[count - 1 - i] = Num(0);
+    }
   }
 
   void reset() { count = 0; }

headers/wasm/symbolic_rt.hpp

@@ -777,7 +777,12 @@ inline bool NodeBox::fillIfElseNode(SymVal cond, int id) {
   } else if (dynamic_cast<UnExploredNode *>(node.get())) {
     node = std::make_unique<IfElseNode>(cond, this, id);
     return true;
+  } else if (dynamic_cast<NotToExploreNode *>(node.get()) != nullptr) {
+    assert(false &&
+           "Unexpected traversal: arrived at a node marked 'NotToExplore'.");
+    return false;
   }
+
   assert(
       dynamic_cast<IfElseNode *>(node.get()) != nullptr &&
       "Current node is not an Unexplored nor an IfElseNode, cannot fill it!");