Misc: bug fixes, additional WASM operations, and support heuristic profiling

benchmarks/wasm/call_indirect_test.1.wat

@@ -0,0 +1,38 @@
+(module
+  (type (;0;) (func (param i32) (result i32)))
+  (type (;1;) (func (param i32 i32) (result i32)))
+  (type (;2;) (func (result i32)))
+  (func (;0;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 1
+    i32.add)
+  (func (;1;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 2
+    i32.mul)
+  (func (;2;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 3
+    i32.sub)
+  (func (;3;) (type 1) (param i32 i32) (result i32)
+    local.get 1
+    local.get 0
+    call_indirect (type 0))
+  (func (;4;) (type 2) (result i32)
+    ;; (1 + 10) + (2 * 10) + (10 - 3) = 38
+    i32.const 1000
+    i32.const 10
+    call 3
+    i32.const 1001
+    i32.const 10
+    call 3
+    i32.add
+    i32.const 1002
+    i32.const 10
+    call 3
+    i32.add)
+  (table (;0;) 4 funcref)
+  (export "run" (func 4))
+  (export "dispatch" (func 3))
+  (elem (;0;) (i32.const 1000) func 0 1 2)
+  (start 4))

benchmarks/wasm/call_indirect_test.wat

@@ -3,26 +3,36 @@
   (type (;1;) (func (param i32 i32) (result i32)))
   (type (;2;) (func (result i32)))
   (func (;0;) (type 0) (param i32) (result i32)
-    (local i32 i32 i32 i32 i32)
-    local.get 3
-    drop
     local.get 0
     i32.const 1
     i32.add)
   (func (;1;) (type 0) (param i32) (result i32)
     local.get 0
     i32.const 2
     i32.mul)
-  (func (;2;) (type 1) (param i32 i32) (result i32)
+  (func (;2;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 3
+    i32.sub)
+  (func (;3;) (type 1) (param i32 i32) (result i32)
     local.get 1
     local.get 0
     call_indirect (type 0))
-  (func (;3;) (type 2) (result i32)
+  (func (;4;) (type 2) (result i32)
+    ;; (1 + 10) + (2 * 10) + (10 - 3) = 38
     i32.const 0
-    i32.const 41
-    call 2)
-  (table (;0;) 2 funcref)
-  (export "run" (func 3))
-  (export "dispatch" (func 2))
-  (elem (;0;) (i32.const 0) func 0 1)
-  (start 3))
+    i32.const 10
+    call 3
+    i32.const 1
+    i32.const 10
+    call 3
+    i32.add
+    i32.const 2
+    i32.const 10
+    call 3
+    i32.add)
+  (table (;0;) 3 funcref)
+  (export "run" (func 4))
+  (export "dispatch" (func 3))
+  (elem (;0;) (i32.const 0) func 0 1 2)
+  (start 4))

benchmarks/wasm/fp_ops.wat

@@ -15,6 +15,16 @@
     f64.const 0x1p-1 (;=0.5;)
     local.set 3
     local.get 0
+    f32.abs
+    f32.const 0x1.cp+1 (;=3.5;)
+    f32.eq
+    call 0
+    local.get 2
+    f64.abs
+    f64.const 0x1.48p+3 (;=10.25;)
+    f64.eq
+    call 0
+    local.get 0
     local.get 1
     f32.add
     f32.const 0x1.6p+2 (;=5.5;)
@@ -139,6 +149,18 @@
     f64.convert_i64_s
     f64.const -1.0
     f64.eq
+    call 0
+
+    f32.const 3.75
+    i32.trunc_f32_s
+    i32.const 3
+    i32.eq
+    call 0
+
+    f32.const 3.75
+    i32.trunc_f32_u
+    i32.const 3
+    i32.eq
     call 0)
 
   ;; symbolic branch guard for f32

headers/wasm/concolic_driver.hpp

@@ -86,6 +86,7 @@ class DefaultPathPicker : public PathPicker {
       : PathPicker(unexplored_paths, visited) {}
 
   std::optional<PathFrontier> pick_path() override {
+    ManagedTimer timer(TimeProfileKind::SOLVER_TOTAL);
     NodeBox *node = unexplored_paths.back();
     unexplored_paths.pop_back();
 
@@ -102,7 +103,6 @@ class DefaultPathPicker : public PathPicker {
 
     std::optional<QueryResult> result;
     {
-      ManagedTimer timer(TimeProfileKind::SOLVER_TOTAL);
       auto cond = node->collect_path_conds();
       result = solver.solve_path_conds(cond, true);
     }
@@ -196,7 +196,15 @@ inline void ConcolicDriver::main_exploration_loop() {
       GENSYM_INFO("Now execute the program with symbolic environment: ");
       GENSYM_INFO(SymEnv.to_string());
       auto snapshot = dynamic_cast<SnapshotNode *>(node->node.get());
+      if (snapshot && PROFILE_SNAPSHOT) {
+        auto resume_cost = snapshot->cost_of_snapshot_resume();
+        auto restart_cost = snapshot->cost_of_restart();
+        Profile.record_snapshot_history(resume_cost, restart_cost);
+      }
       if (REUSE_SNAPSHOT && snapshot && snapshot->worth_to_reuse()) {
+        // If we enabled snapshot reuse and the current snapshot is worth to
+        // reuse, resume the execution from the snapshot with the model we got
+        // from SMT solver.
         assert(REUSE_SNAPSHOT);
         Profile.incr_fromsnapshot_count();
         auto snap = snapshot->get_snapshot();
@@ -223,6 +231,7 @@ inline void ConcolicDriver::main_exploration_loop() {
       GENSYM_INFO("Caught runtime error during execution");
       switch (EXPLORE_MODE) {
       case ExploreMode::EarlyExit:
+        GENSYM_INFO("Exiting exploration due to error...");
         return;
       case ExploreMode::ExitByCoverage:
         if (ExploreTree.all_branch_covered()) {
@@ -274,4 +283,4 @@ static void start_concolic_execution_with(
   std::quick_exit(0);
 }
 
-#endif // CONCOLIC_DRIVER_HPP
+#endif // CONCOLIC_DRIVER_HPP

headers/wasm/concrete_num.hpp

@@ -640,6 +640,48 @@ struct Num {
     return Num(static_cast<int32_t>(r_bits));
   }
 
+  inline Num trunc_f32_to_i32_s() const {
+    uint32_t bits = toUInt();
+    float value = f32_from_bits(bits);
+
+    if (std::isnan(value)) {
+      throw std::runtime_error("i32.trunc_f32_s: NaN");
+    }
+    if (std::isinf(value)) {
+      throw std::runtime_error("i32.trunc_f32_s: Infinity");
+    }
+    if (value < -2147483648.0f || value >= 2147483648.0f) {
+      throw std::runtime_error("i32.trunc_f32_s: Out of range");
+    }
+
+    float truncated = std::trunc(value);
+    int32_t result = static_cast<int32_t>(truncated);
+    Num res(result);
+    debug_print("i32.trunc_f32_s", *this, *this, res);
+    return res;
+  }
+
+  inline Num trunc_f32_to_i32_u() const {
+    uint32_t bits = toUInt();
+    float value = f32_from_bits(bits);
+
+    if (std::isnan(value)) {
+      throw std::runtime_error("i32.trunc_f32_u: NaN");
+    }
+    if (std::isinf(value)) {
+      throw std::runtime_error("i32.trunc_f32_u: Infinity");
+    }
+    if (value < 0.0f || value >= 4294967296.0f) {
+      throw std::runtime_error("i32.trunc_f32_u: Out of range");
+    }
+
+    float truncated = std::trunc(value);
+    uint32_t result = static_cast<uint32_t>(truncated);
+    Num res(static_cast<int32_t>(result));
+    debug_print("i32.trunc_f32_u", *this, *this, res);
+    return res;
+  }
+
   // f32.min / f32.max: follow wasm-ish semantics: if either is NaN, return NaN
   // (propagate)
   inline Num f32_min(const Num &other) const {

headers/wasm/concrete_rt.hpp

@@ -11,6 +11,7 @@
 #include <cstdio>
 #include <iostream>
 #include <memory>
+#include <optional>
 #include <ostream>
 #include <string>
 #include <unistd.h>
@@ -50,7 +51,10 @@ class Stack_t {
 
   Num pop() {
     Profile.step(StepProfileKind::POP);
-    assert(count > 0 && "Stack underflow");
+    if (count <= 0) {
+      assert(false);
+      throw std::runtime_error("Stack underflow");
+    }
 #ifdef DEBUG
     printf("[Debug] popping a value %ld from stack, size of concrete stack is: "
            "%d\n",
@@ -261,11 +265,15 @@ struct Memory_t {
     reset();
   }
 
+  void assert_valid_range(int32_t addr, size_t width) const {
+    assert(addr >= 0);
+    assert(static_cast<size_t>(addr) + width <= memory.size());
+    GENSYM_ASSERT_ADDR_ALLOCATED(addr, width);
+  }
+
   int32_t loadInt(int32_t base, int32_t offset) {
     int32_t addr = base + offset;
-    if (!(addr + 3 < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 4);
     int32_t result = 0;
     // Little-endian: lowest byte at lowest address
     for (int i = 0; i < 4; ++i) {
@@ -282,9 +290,7 @@ struct Memory_t {
 
   uint8_t loadByte(int32_t base, int32_t offset) {
     int32_t addr = base + offset;
-    if (!(addr < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 1);
     return memory[addr];
   }
 
@@ -343,15 +349,14 @@ struct Memory_t {
     uint64_t b1 = static_cast<uint64_t>(loadByte(base, offset + 1));
     uint64_t b2 = static_cast<uint64_t>(loadByte(base, offset + 2));
     uint64_t b3 = static_cast<uint64_t>(loadByte(base, offset + 3));
-    uint32_t raw = static_cast<uint32_t>(b0 | (b1 << 8) | (b2 << 16) | (b3 << 24));
+    uint32_t raw =
+        static_cast<uint32_t>(b0 | (b1 << 8) | (b2 << 16) | (b3 << 24));
     return static_cast<int32_t>(raw);
   }
 
   int64_t loadLong(int32_t base, int32_t offset) {
     int32_t addr = base + offset;
-    if (!(addr + 7 < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 8);
     int64_t result = 0;
     for (int i = 0; i < 8; ++i) {
       result |= static_cast<int64_t>(memory[addr + i]) << (8 * i);
@@ -361,10 +366,7 @@ struct Memory_t {
 
   std::monostate storeInt(int32_t base, int32_t offset, int32_t value) {
     int32_t addr = base + offset;
-    // Ensure we don't write out of bounds
-    if (!(addr + 3 < memory.size())) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 4);
     for (int i = 0; i < 4; ++i) {
       memory[addr + i] = static_cast<uint8_t>((value >> (8 * i)) & 0xFF);
     }
@@ -377,11 +379,10 @@ struct Memory_t {
 
   std::monostate storeLong(int32_t base, int32_t offset, int64_t value) {
     int32_t addr = base + offset;
-    if (!(addr + 7 < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 8);
     for (int i = 0; i < 8; ++i) {
-      memory[addr + i] = static_cast<uint8_t>((static_cast<uint64_t>(value) >> (8 * i)) & 0xFF);
+      memory[addr + i] = static_cast<uint8_t>(
+          (static_cast<uint64_t>(value) >> (8 * i)) & 0xFF);
     }
     return std::monostate{};
   }
@@ -419,7 +420,7 @@ struct Memory_t {
     std::cout << "[Debug] storing byte " << std::to_string(value)
               << " to memory at address " << addr << std::endl;
 #endif
-    assert(addr < memory.size());
+    assert_valid_range(addr, 1);
     memory[addr] = value;
     return std::monostate{};
   }
@@ -470,26 +471,44 @@ struct FuncTable_t {
   std::vector<Func_t> table;
 
   Func_t read(int32_t index) {
-    if (index < 0 || index >= table.size()) {
+    auto offset = index - start_index.value();
+    if (offset < 0 || offset >= table.size()) {
       throw std::runtime_error("Function table read out of bounds: " +
                                std::to_string(index));
     }
-    if (!table[index]) {
-      assert(false);
+    if (!table[offset]) {
+      std::cout << "Function table entry at index " << index
+                << " is empty or invalid" << std::endl;
+      assert(false && "Function table entry is empty or invalid");
       throw std::runtime_error("Function table entry at index " +
                                std::to_string(index) + " is empty or invalid");
     }
-    return table[index];
+    return table[offset];
   }
 
   std::monostate set(Num offset, int32_t index, Func_t func) {
+    if (start_index.has_value()) {
+      assert(offset.toInt() == start_index &&
+             "Currently only supporting one function table per module.");
+    } else {
+      start_index = offset.toInt();
+    }
     if (index < 0 || index >= table.size()) {
       throw std::runtime_error("Function table set out of bounds: " +
                                std::to_string(index));
     }
-    table[offset.toInt() + index] = func;
+    table[index] = func;
     return std::monostate{};
   }
+
+  std::monostate setStart(int32_t index) {
+    // set start index to be the function at index 0
+    start_index = index;
+    return std::monostate{};
+  }
+
+private:
+  std::optional<int32_t> start_index;
 };
 
 static FuncTable_t FuncTable;