Support fp load & fix memory initialize & symbolic store and load

headers/wasm/concrete_num.hpp

@@ -2,6 +2,7 @@
 #define WASM_CONCRETE_NUM_HPP
 #include "wasm/profile.hpp"
 #include "wasm/utils.hpp"
+#include <cmath>
 #include <cstdint>
 
 struct Num {
@@ -877,6 +878,27 @@ struct Num {
     return Num(static_cast<int64_t>(r_bits));
   }
 
+  inline Num trunc_f64_to_i32_u() const {
+    uint64_t bits = toUInt64();
+    double value = f64_from_bits(bits);
+
+    if (std::isnan(value)) {
+      throw std::runtime_error("i32.trunc_f64_u: NaN");
+    }
+    if (std::isinf(value)) {
+      throw std::runtime_error("i32.trunc_f64_u: Infinity");
+    }
+    if (value < 0.0 || value >= 4294967296.0) {
+      throw std::runtime_error("i32.trunc_f64_u: Out of range");
+    }
+
+    double truncated = std::trunc(value);
+    uint32_t result = static_cast<uint32_t>(truncated);
+    Num res(static_cast<int32_t>(result));
+    debug_print("i32.trunc_f64_u", *this, *this, res);
+    return res;
+  }
+
   // f64.min / f64.max: follow wasm-ish semantics: if either is NaN, return
   // NaN (propagate)
   inline Num f64_min(const Num &other) const {

headers/wasm/sym_rt.hpp

@@ -354,7 +354,39 @@ class SymMemory_t {
     SymVal s7 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
 #endif
 
-    return s7.concat(s6).concat(s5).concat(s4).concat(s3).concat(s2).concat(s1).concat(s0);
+    return s7.concat(s6)
+        .concat(s5)
+        .concat(s4)
+        .concat(s3)
+        .concat(s2)
+        .concat(s1)
+        .concat(s0);
+  }
+
+  SymVal loadSymFloat(int32_t base, int32_t offset) {
+    // For simplicity, we treat float as concrete value for now
+    auto symbv = loadSym(base, offset);
+    assert(symbv.is_concrete() && "Currently only support concrete symbolic "
+                                  "value for float-point values");
+    if (auto concrete = dynamic_cast<SymConcrete *>(symbv.symptr.get())) {
+      auto value = concrete->value;
+      return SVFactory::make_concrete_fp(value, 32);
+    } else {
+      assert(false && "unreachable");
+    }
+  }
+
+  SymVal loadSymDouble(int32_t base, int32_t offset) {
+    // For simplicity, we treat double as concrete value for now
+    auto symbv = loadSymLong(base, offset);
+    assert(symbv.is_concrete() && "Currently only support concrete symbolic "
+                                  "value for float-point values");
+    if (auto concrete = dynamic_cast<SymConcrete *>(symbv.symptr.get())) {
+      auto value = concrete->value;
+      return SVFactory::make_concrete_fp(value, 64);
+    } else {
+      assert(false && "unreachable");
+    }
   }
 
   // when loading a symval, we need to concat 4 symbolic values
@@ -396,6 +428,18 @@ class SymMemory_t {
     return std::monostate{};
   }
 
+  std::monostate storeSymFloat(int32_t base, int32_t offset, SymVal value) {
+    assert(value.is_concrete() && "Currently only support concrete symbolic "
+                                  "value for float-point values");
+    return storeSym(base, offset, value);
+  }
+
+  std::monostate storeSymDouble(int32_t base, int32_t offset, SymVal value) {
+    assert(value.is_concrete() && "Currently only support concrete symbolic "
+                                  "value for float-point values");
+    return storeSymLong(base, offset, value);
+  }
+
   std::monostate storeSymByte(int32_t addr, SymVal value) {
     // assume the input value is 8-bit symbolic value
     bool exists;

headers/wasm/symbolic_decl.hpp

@@ -10,17 +10,20 @@ enum BinOperation {
   SUB,     // Subtraction
   MUL,     // Multiplication
   DIV,     // Division
+  DIV_U,   // Unsigned division
   AND,     // Logical AND
   OR,      // Logical OR
   EQ_BOOL, // Equal (return a boolean) TODO: remove bv version of comparison ops
   NEQ_BOOL, // Not equal (return a boolean)
   LT_BOOL,  // Less than (return a boolean)
   LTU_BOOL, // Unsigned less than (return a boolean)
   LEQ_BOOL, // Less than or equal (return a boolean)
+  LEU_BOOL, // Unsigned less than or equal (return a boolean)
   GT_BOOL,  // Greater than (return a boolean)
   GTU_BOOL, // Unsigned greater than (return a boolean)
   GEQ_BOOL, // Greater than or equal (return a boolean)
   GEU_BOOL, // Unsigned greater than or equal (return a boolean)
+  SHL,      // Shift left
   SHR_U,    // Shift right unsigned
   SHR_S,    // Shift right signed
   REM_U,    // Unsigned remainder
@@ -33,7 +36,7 @@ enum BinOperation {
 enum UnaryOperation {
   NOT,     // bool not
   BOOL2BV, // bool to bitvector,
-  EXTEND,   // bitvector extension, extend i32 to i64
+  EXTEND,  // bitvector extension, extend i32 to i64
 };
 
 enum ValueKind { KindBV, KindBool, KindFP };
@@ -145,6 +148,8 @@ struct SymBinary : public Symbolic {
     case SUB:
     case MUL:
     case DIV:
+    case DIV_U:
+    case SHL:
     case SHR_U:
     case SHR_S:
     case REM_U:
@@ -166,6 +171,7 @@ struct SymBinary : public Symbolic {
     case LT_BOOL:
     case LTU_BOOL:
     case LEQ_BOOL:
+    case LEU_BOOL:
     case GT_BOOL:
     case GTU_BOOL:
     case GEQ_BOOL:

headers/wasm/symbolic_impl.hpp

@@ -76,6 +76,9 @@ inline z3::expr Symbolic::build_z3_expr_aux() {
     case LEQ_BOOL: {
       return left <= right;
     }
+    case LEU_BOOL: {
+      return z3::ule(left, right);
+    }
     case GT_BOOL: {
       return left > right;
     }
@@ -85,6 +88,18 @@ inline z3::expr Symbolic::build_z3_expr_aux() {
     case GEU_BOOL: {
       return z3::uge(left, right);
     }
+    case SHL: {
+      if (bit_width == 32) {
+        z3::expr shift_mask = global_z3_ctx().bv_val(0x1F, bit_width);
+        return z3::shl(left, right & shift_mask);
+      } else if (bit_width == 64) {
+        z3::expr shift_mask = global_z3_ctx().bv_val(0x3F, bit_width);
+        return z3::shl(left, right & shift_mask);
+      } else {
+        throw std::runtime_error("Unsupported bit width for SHL: " +
+                                 std::to_string(bit_width));
+      }
+    }
     case SHR_U: {
       return z3::lshr(left, right);
     }
@@ -109,6 +124,9 @@ inline z3::expr Symbolic::build_z3_expr_aux() {
     case DIV: {
       return left / right;
     }
+    case DIV_U: {
+      return z3::udiv(left, right);
+    }
     case B_AND: {
       return left & right;
     }

headers/wasm/symval_decl.hpp

@@ -28,6 +28,7 @@ struct SymVal {
   SymVal minus(const SymVal &other) const;
   SymVal mul(const SymVal &other) const;
   SymVal div(const SymVal &other) const;
+  SymVal div_u(const SymVal &other) const;
   SymVal eq_bool(const SymVal &other) const;
   SymVal neq_bool(const SymVal &other) const;
   SymVal land(const SymVal &other) const;
@@ -37,10 +38,12 @@ struct SymVal {
   SymVal lt(const SymVal &other) const;
   SymVal ltu(const SymVal &other) const;
   SymVal le(const SymVal &other) const;
+  SymVal leu(const SymVal &other) const;
   SymVal gt(const SymVal &other) const;
   SymVal gtu(const SymVal &other) const;
   SymVal ge(const SymVal &other) const;
   SymVal geu(const SymVal &other) const;
+  SymVal shl(const SymVal &other) const;
   SymVal shr_u(const SymVal &other) const;
   SymVal shr_s(const SymVal &other) const;
   SymVal bv_negate() const;
@@ -83,4 +86,10 @@ template <typename... Args> inline bool allConcrete(const Args &...args) {
 
 inline SymVal Concrete(Num num, int width);
 
+[[noreturn]] inline SymVal debug_unreachable(const char* msg) {
+    std::cerr << "unreachable: " << msg << '\n';
+    assert(false && "unreachable reached");
+    std::abort();
+}
+
 #endif // WASM_SYMVAL_HPP

headers/wasm/symval_factory.hpp

@@ -365,6 +365,12 @@ inline SymVal make_binary(BinOperation op, const SymVal &lhs,
         if (lhs_width == 64 && rhs_width == 64)
           return make_eval_bool(lhs_value.i64_lt_u(rhs_value));
         break;
+      case LEU_BOOL:
+        if (lhs_width == 32 && rhs_width == 32)
+          return make_eval_bool(lhs_value.i32_le_u(rhs_value));
+        if (lhs_width == 64 && rhs_width == 64)
+          return make_eval_bool(lhs_value.i64_le_u(rhs_value));
+        break;
       case GTU_BOOL:
         if (lhs_width == 32 && rhs_width == 32)
           return make_eval_bool(lhs_value.i32_gt_u(rhs_value));

headers/wasm/symval_impl.hpp

@@ -21,6 +21,10 @@ inline SymVal SymVal::div(const SymVal &other) const {
   return SVFactory::make_binary(DIV, *this, other);
 }
 
+inline SymVal SymVal::div_u(const SymVal &other) const {
+  return SVFactory::make_binary(DIV_U, *this, other);
+}
+
 inline SymVal SymVal::land(const SymVal &other) const {
   return SVFactory::make_binary(AND, *this, other);
 }
@@ -70,6 +74,10 @@ inline SymVal SymVal::le(const SymVal &other) const {
   return SVFactory::make_binary(LEQ_BOOL, *this, other);
 }
 
+inline SymVal SymVal::leu(const SymVal &other) const {
+  return SVFactory::make_binary(LEU_BOOL, *this, other);
+}
+
 inline SymVal SymVal::gt(const SymVal &other) const {
   return SVFactory::make_binary(GT_BOOL, *this, other);
 }
@@ -86,6 +94,10 @@ inline SymVal SymVal::geu(const SymVal &other) const {
   return SVFactory::make_binary(GEU_BOOL, *this, other);
 }
 
+inline SymVal SymVal::shl(const SymVal &other) const {
+  return SVFactory::make_binary(SHL, *this, other);
+}
+
 inline SymVal SymVal::shr_u(const SymVal &other) const {
   return SVFactory::make_binary(SHR_U, *this, other);
 }