Some bug fix (#100)

* bug fix: remove recalculation of symbolic size

* a debug utility

* fix: symbol name for combined z3 model

* compute composed model by z3::model directly

* remove a test case for i64.rotr, which is not use in benchmarks

* more debuggiing infos

Author: butterunderflow

benchmarks/wasm/i64_ops.wat

@@ -87,13 +87,13 @@
     i64.eq
     call 0
 
-    local.get 0
-    local.get 2
-    i64.extend_i32_u
-    i64.rotr
-    i64.const 4611686018427387909
-    i64.eq
-    call 0
+    ;; local.get 0
+    ;; local.get 2
+    ;; i64.extend_i32_u
+    ;; i64.rotr
+    ;; i64.const 4611686018427387909
+    ;; i64.eq
+    ;; call 0
 
     ;; comparisons
     local.get 0

headers/wasm/smt_solver.hpp

@@ -36,6 +36,7 @@ static QueryResult
 compose_query_results(const std::vector<QueryResult> &results) {
   ManagedTimer timer(TimeProfileKind::SPLIT_CONDITIONS);
   NumMap combined_map;
+  z3::model combined_model(global_z3_ctx());
   for (const auto &res : results) {
     auto num_map = res.map_box;
     for (const auto &[id, num] : *num_map) {
@@ -44,19 +45,21 @@ compose_query_results(const std::vector<QueryResult> &results) {
           "Conflicting symbolic environment ids when composing query results");
       combined_map[id] = num;
     }
+    const z3::model &model = res.model;
+    for (unsigned i = 0; i < model.num_consts(); ++i) {
+      z3::func_decl decl = model.get_const_decl(i);
+      std::string name = decl.name().str();
+      assert((starts_with(name, "s_int") || starts_with(name, "s_f32") ||
+              starts_with(name, "s_f64")) &&
+             "Unexpected declaration in query result model");
+      assert(!combined_model.has_interp(decl) &&
+             "Internal Error: Conflicting constant declarations when composing query results");
+      z3::expr value = model.get_const_interp(decl);
+      combined_model.add_const_interp(decl, value);
+    }
   }
   ImmNumMapBox combined_map_box(combined_map);
-
-  z3::solver solver(global_z3_ctx());
-
-  // build a combined z3 model
-  for (const auto &[id, num] : combined_map) {
-    solver.add(
-        global_z3_ctx().bv_const(("s_" + std::to_string(id)).c_str(), 32) ==
-        global_z3_ctx().bv_val(num.value, 32));
-  }
-  solver.check();
-  return QueryResult{combined_map_box, solver.get_model()};
+  return QueryResult{combined_map_box, combined_model};
 }
 
 // VectorGroupResult groups a vector. key is the vector index, and value is the

headers/wasm/sym_rt.hpp

@@ -42,7 +42,6 @@ class SymStack_t {
   void push(SymVal val) {
     // Push a symbolic value to the stack
     stack.push_back(val);
-    symbolic_size += val->size();
   }
 
   SymVal pop() {
@@ -54,12 +53,10 @@ class SymStack_t {
 #ifdef USE_IMM
     auto ret = *(stack.end() - 1);
     stack.take(stack.size() - 1);
-    symbolic_size -= ret->size();
     return ret;
 #else
     auto ret = stack.back();
     stack.pop_back();
-    symbolic_size -= ret->size();
     return ret;
 #endif
   }
@@ -71,7 +68,6 @@ class SymStack_t {
     for (size_t i = n - size; i < n; ++i) {
       assert(i - offset >= 0);
 #ifdef USE_IMM
-      symbolic_size -= stack[i - offset]->size();
       stack.set(i - offset, stack[i]);
 #else
       stack[i - offset] = stack[i];
@@ -149,10 +145,6 @@ class SymFrames_t {
     auto frame_base = current_frame_base();
     assert(frame_base + size == stack.size());
 
-    for (int i = 0; i < size; ++i) {
-      symbolic_size -= stack[stack.size() - 1 - i]->size();
-    }
-
 #ifdef USE_IMM
     stack.take(stack.size() - size);
 #else
@@ -173,10 +165,6 @@ class SymFrames_t {
     assert(size >= 0);
     assert(static_cast<size_t>(size) <= stack.size());
 
-    for (int i = 0; i < size; ++i) {
-      symbolic_size -= stack[stack.size() - 1 - i]->size();
-    }
-
 #ifdef USE_IMM
     stack.take(stack.size() - size);
 #else
@@ -203,7 +191,6 @@ class SymFrames_t {
     auto frame_base = current_frame_base();
     assert(index >= 0 &&
            static_cast<size_t>(frame_base + index) < stack.size());
-    symbolic_size += val->size() - stack[frame_base + index]->size();
 #ifdef USE_IMM
     stack.set(frame_base + index, val);
 #else
@@ -451,11 +438,6 @@ class SymMemory_t {
     exists = (it != memory.end());
 #endif
     auto old_value = loadSymByte(addr);
-    if (exists) {
-      // We are overwriting an existing symbolic value
-      symbolic_size -= old_value->size();
-    }
-    symbolic_size += value->size();
 #ifdef USE_IMM
     memory.set(addr, value);
 #else

headers/wasm/symbolic_decl.hpp

@@ -314,7 +314,7 @@ inline std::tuple<int, bool> count_dag_size_aux(Symbolic &val,
   } else if (auto witness = dynamic_cast<Witness *>(&val)) {
     assert(false && "Witness should not appear during instruction execution");
   } else {
-    throw std::runtime_error("Unknown symbolic type in dag size counting");
+    assert(false && "Unknown symbolic type in dag size counting");
   }
 }
 

headers/wasm/utils.hpp

@@ -52,18 +52,36 @@ inline bool starts_with(const std::string &str, const std::string &prefix) {
 }
 #endif
 
-inline std::monostate info() {
-#ifdef DEBUG
+inline std::monostate print_infos() {
   std::cout << std::endl;
-#endif
+  return std::monostate{};
+}
+
+template <typename T, typename... Args>
+std::monostate print_infos(const T &first, const Args &...args) {
+  std::cout << first << " ";
+  print_infos(args...);
   return std::monostate{};
 }
 
 template <typename T, typename... Args>
 std::monostate info(const T &first, const Args &...args) {
 #ifdef DEBUG
-  std::cout << first << " ";
-  info(args...);
+  print_infos(first, args...);
+#endif
+  return std::monostate{};
+}
+
+constexpr const char *DEBUG_OPTS_ENV_VAR = "GENSYM_DEBUG";
+
+template <typename... Args>
+std::monostate infoWhen(const char *dbg_option, const Args &...args) {
+#ifdef DEBUGWHEN
+  const char *env_value = std::getenv(DEBUG_OPTS_ENV_VAR);
+  if (env_value && std::string(env_value).find(std::string(dbg_option)) !=
+                       std::string::npos) {
+    print_infos(args...);
+  }
 #endif
   return std::monostate{};
 }

src/main/scala/wasm/StagedConcolicMiniWasm.scala

@@ -1112,6 +1112,10 @@ trait DebugInfo extends SAIOps {
   def info(xs: Rep[_]*): Rep[Unit] = {
     "info".reflectCtrlWith[Unit](xs: _*)
   }
+
+  def infoWhen(envVar: Rep[String], xs: Rep[_]*): Rep[Unit] = {
+    "infoWhen".reflectCtrlWith[Unit](envVar :: xs.toList: _*)
+  }
 }
 
 @virtualize
@@ -1575,7 +1579,7 @@ trait StagedWasmEvaluator extends SAIOps
           }
           tailCall(thnK, ())
         } else {
-          info(s"Continue")
+          info(s"Continue rest of the block")
           withBlock {
             val control = makeControl(thnK, currentMCont)
             ExploreTree.moveCursor(false, control)
@@ -1671,7 +1675,7 @@ trait StagedWasmEvaluator extends SAIOps
     })
     val newMKont: Rep[MCont[Unit]] = currentMCont.prependCont(restK)
     updateCurrentMCont(newMKont)
-    info(s"Calling function at index ", index.toInt, " with call_indirect, stackSize =", Stack.size)
+    infoWhen("CALL", s"Calling function at index ", index.toInt, " with call_indirect, stackSize =", Stack.size)
     val argsC = Stack.takeC(functy.inps)
     val argsS = Stack.takeS(functy.inps)
     Frames.pushFrameCallerC(functy.inps)
@@ -1686,7 +1690,7 @@ trait StagedWasmEvaluator extends SAIOps
       compileCache(funcIndex)
     } else {
       def retK(ctx: Context): Rep[Cont[Unit]] = topFun((_: Rep[Unit]) => {
-        info(s"Return from the function at $funcIndex, stackSize =", Stack.size)
+        infoWhen("CALL", s"Exiting the function at $funcIndex, stackSize =", Stack.size)
         Frames.popFrameCalleeC(locals.size)
         Frames.popFrameCalleeS(locals.size)
         val offset = ctx.stackTypes.size - ty.out.size
@@ -1696,7 +1700,7 @@ trait StagedWasmEvaluator extends SAIOps
       })
 
       val func = topFun((_: Rep[Unit]) => {
-        info(s"Entered the function at $funcIndex, stackSize =", Stack.size)
+        infoWhen("CALL", s"Entered the function at $funcIndex, stackSize =", Stack.size)
         Frames.pushFrameCalleeC(locals.size)
         Frames.pushFrameCalleeS(locals)
         // the return instruction is also stack polymorphic
@@ -1718,14 +1722,14 @@ trait StagedWasmEvaluator extends SAIOps
         val callee = evalFunc(ty, body, funcIndex, ty.inps, bodyLocals)
         // Predef.println(s"[DEBUG] locals size: ${locals.size}")
         withBlock {
-          info("Taking arguments from stack to call function at ", funcIndex)
+          infoWhen("CALL", s"Taking arguments from stack to call function at ", funcIndex)
           val newCtx = ctx.take(ty.inps.size)
           val argsC = Stack.takeC(ty.inps)
           val argsS = Stack.takeS(ty.inps)
           // We make a new trail by `restK`, since function creates a new block to escape
           // (more or less like `return`)
           val restK: Rep[Cont[Unit]] = topFun((_: Rep[Unit]) => {
-            info(s"Exiting the function at $funcIndex, stackSize =", Stack.size)
+            infoWhen("CALL", s"Returning from the function at $funcIndex, stackSize =", Stack.size)
             Frames.popFrameCallerC(ty.inps.size)
             Frames.popFrameCallerS(ty.inps.size)
             eval(rest, kont, trail)(newCtx.copy(stackTypes = ty.out.reverse ++ ctx.stackTypes.drop(ty.inps.size)))