Conversion and load i64

benchmarks/wasm/fp_ops.wat

@@ -115,6 +115,30 @@
     local.get 3
     f64.le
     i32.eqz
+    call 0
+
+    i32.const -1
+    f32.convert_i32_s
+    f32.const -1.0
+    f32.eq
+    call 0
+
+    i32.const -1
+    f32.convert_i32_u
+    f32.const 0x1p+32 (;=4294967296;)
+    f32.eq
+    call 0
+
+    i32.const -1
+    f64.convert_i32_u
+    f64.const 4294967295.0
+    f64.eq
+    call 0
+
+    i64.const -1
+    f64.convert_i64_s
+    f64.const -1.0
+    f64.eq
     call 0)
 
   ;; symbolic branch guard for f32

benchmarks/wasm/mem-sym.wat

@@ -12,24 +12,48 @@
     i32.load
     i32.const 25
     i32.eq
-    if (result i32)  ;; if x == 25
-      i32.const 0 
+    if  ;; if x == 25
+      i32.const 0
       call 0 ;; assert false
-      i32.const 1 ;; to satisfy the type checker, this line will never be reached
-    else
-      i32.const 1
-      i32.load
-      i32.const 1
-      i32.eq
-      if (result i32) ;; if x >> 8 == 1
-        i32.const 0
-        call 0 ;; assert false
-        i32.const 1 ;; to satisfy the type checker, this line will never be reached
-      else
-        i32.const 1
-      end
-      i32.const 1
     end
+    i32.const 1
+    i32.load
+    i32.const 1
+    i32.eq
+    if ;; if x >> 8 == 1
+      i32.const 0
+      call 0 ;; assert false
+    end
+    i32.const 4
+    i64.load
+    i64.eqz
+    i32.eqz
+    if
+      i32.const 0
+      call 0 ;; assert false
+    end
+    i32.const 0
+    i64.load
+    i64.const 32
+    i64.shr_u
+    i64.eqz
+    i32.eqz
+    if
+      i32.const 0
+      call 0 ;; assert false
+    end
+    i32.const 8
+    i64.const 0x0102030405060708
+    i64.store
+    i32.const 8
+    i64.load
+    i64.const 0x0102030405060708
+    i64.ne
+    if
+      i32.const 0
+      call 0 ;; assert false
+    end
+    i32.const 1
   )
   (func (;2;) (type 1)
     i32.const 0
@@ -40,4 +64,4 @@
   (memory (;0;) 2)
   (export "main" (func 1))
   (global (;0;) (mut i32) (i32.const 42))
-)
+)

headers/wasm/concrete_num.hpp

@@ -236,10 +236,18 @@ struct Num {
   }
 
   // i64.extend_i32_s: sign-extend low 32 bits to i64
-  inline Num i32_extend_to_i64() const {
+  inline Num i32_extend_to_i64_s() const {
     int64_t result_s = static_cast<int64_t>(this->toInt());
     Num res(result_s);
-    debug_print("i32.extend_to_i64", *this, *this, res);
+    debug_print("i32.extend_to_i64_s", *this, *this, res);
+    return res;
+  }
+
+  // i64.extend_i32_u: zero-extend low 32 bits to i64
+  inline Num i32_extend_to_i64_u() const {
+    uint64_t result_u = static_cast<uint64_t>(this->toUInt());
+    Num res(static_cast<int64_t>(result_u));
+    debug_print("i32.extend_to_i64_u", *this, *this, res);
     return res;
   }
 
@@ -611,6 +619,26 @@ struct Num {
     return res;
   }
 
+  inline Num convert_i32_to_f32_s() const {
+    uint32_t r_bits = f32_to_bits(static_cast<float>(toInt()));
+    return Num(static_cast<int32_t>(r_bits));
+  }
+
+  inline Num convert_i32_to_f32_u() const {
+    uint32_t r_bits = f32_to_bits(static_cast<float>(toUInt()));
+    return Num(static_cast<int32_t>(r_bits));
+  }
+
+  inline Num convert_i64_to_f32_s() const {
+    uint32_t r_bits = f32_to_bits(static_cast<float>(toInt64()));
+    return Num(static_cast<int32_t>(r_bits));
+  }
+
+  inline Num convert_i64_to_f32_u() const {
+    uint32_t r_bits = f32_to_bits(static_cast<float>(toUInt64()));
+    return Num(static_cast<int32_t>(r_bits));
+  }
+
   // f32.min / f32.max: follow wasm-ish semantics: if either is NaN, return NaN
   // (propagate)
   inline Num f32_min(const Num &other) const {
@@ -829,6 +857,26 @@ struct Num {
     return res;
   }
 
+  inline Num convert_i32_to_f64_s() const {
+    uint64_t r_bits = f64_to_bits(static_cast<double>(toInt()));
+    return Num(static_cast<int64_t>(r_bits));
+  }
+
+  inline Num convert_i32_to_f64_u() const {
+    uint64_t r_bits = f64_to_bits(static_cast<double>(toUInt()));
+    return Num(static_cast<int64_t>(r_bits));
+  }
+
+  inline Num convert_i64_to_f64_s() const {
+    uint64_t r_bits = f64_to_bits(static_cast<double>(toInt64()));
+    return Num(static_cast<int64_t>(r_bits));
+  }
+
+  inline Num convert_i64_to_f64_u() const {
+    uint64_t r_bits = f64_to_bits(static_cast<double>(toUInt64()));
+    return Num(static_cast<int64_t>(r_bits));
+  }
+
   // 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/concrete_rt.hpp

@@ -280,6 +280,18 @@ struct Memory_t {
     return result;
   }
 
+  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));
+    }
+    int64_t result = 0;
+    for (int i = 0; i < 8; ++i) {
+      result |= static_cast<int64_t>(memory[addr + i]) << (8 * i);
+    }
+    return result;
+  }
+
   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
@@ -296,6 +308,17 @@ struct Memory_t {
     return std::monostate{};
   }
 
+  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));
+    }
+    for (int i = 0; i < 8; ++i) {
+      memory[addr + i] = static_cast<uint8_t>((static_cast<uint64_t>(value) >> (8 * i)) & 0xFF);
+    }
+    return std::monostate{};
+  }
+
   std::monostate store_byte(int32_t addr, uint8_t value) {
 #ifdef DEBUG
     std::cout << "[Debug] storing byte " << std::to_string(value)

headers/wasm/sym_rt.hpp

@@ -315,6 +315,48 @@ class SymMemory_t {
 #endif
   }
 
+  SymVal loadSymLong(int32_t base, int32_t offset) {
+#ifdef USE_IMM
+    int32_t addr = base + offset;
+    auto it = memory.find(addr);
+    SymVal s0 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 1);
+    SymVal s1 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 2);
+    SymVal s2 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 3);
+    SymVal s3 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 4);
+    SymVal s4 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 5);
+    SymVal s5 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 6);
+    SymVal s6 = it ? *it : SVFactory::ZeroByte;
+    it = memory.find(addr + 7);
+    SymVal s7 = it ? *it : SVFactory::ZeroByte;
+#else
+    int32_t addr = base + offset;
+    auto it = memory.find(addr);
+    SymVal s0 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 1);
+    SymVal s1 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 2);
+    SymVal s2 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 3);
+    SymVal s3 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 4);
+    SymVal s4 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 5);
+    SymVal s5 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 6);
+    SymVal s6 = (it != memory.end()) ? it->second : SVFactory::ZeroByte;
+    it = memory.find(addr + 7);
+    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);
+  }
+
   // when loading a symval, we need to concat 4 symbolic values
   // This sounds terribly bad for SMT...
   // Load a 4-byte symbolic value from memory
@@ -333,6 +375,27 @@ class SymMemory_t {
     return std::monostate{};
   }
 
+  std::monostate storeSymLong(int32_t base, int32_t offset, SymVal value) {
+    int32_t addr = base + offset;
+    SymVal s0 = value.extract(1, 1);
+    SymVal s1 = value.extract(2, 2);
+    SymVal s2 = value.extract(3, 3);
+    SymVal s3 = value.extract(4, 4);
+    SymVal s4 = value.extract(5, 5);
+    SymVal s5 = value.extract(6, 6);
+    SymVal s6 = value.extract(7, 7);
+    SymVal s7 = value.extract(8, 8);
+    storeSymByte(addr, s0);
+    storeSymByte(addr + 1, s1);
+    storeSymByte(addr + 2, s2);
+    storeSymByte(addr + 3, s3);
+    storeSymByte(addr + 4, s4);
+    storeSymByte(addr + 5, s5);
+    storeSymByte(addr + 6, s6);
+    storeSymByte(addr + 7, s7);
+    return std::monostate{};
+  }
+
   std::monostate storeSymByte(int32_t addr, SymVal value) {
     // assume the input value is 8-bit symbolic value
     bool exists;

headers/wasm/symval_factory.hpp

@@ -2,8 +2,8 @@
 #define WASM_SYMVAL_FACTORY_HPP
 
 #include "heap_mem_bookkeeper.hpp"
-#include "symval_decl.hpp"
 #include "symbolic_decl.hpp"
+#include "symval_decl.hpp"
 
 namespace SVFactory {
 
@@ -116,7 +116,7 @@ struct UnaryOpKeyHash {
 
 // Caches.
 static std::unordered_map<int, SymVal> SymbolStore;
-static std::unordered_map<int64_t, SymVal> concrete_pool;
+static std::unordered_map<int64_t, SymVal> FPStore;
 static std::unordered_map<SmallBVKey, SymVal, SmallBVKeyHash> SmallBVStore;
 static std::unordered_map<ExtractKey, SymVal, ExtractKeyHash>
     ExtractOperationStore;
@@ -126,26 +126,27 @@ static std::unordered_map<UnaryOpKey, SymVal, UnaryOpKeyHash>
 
 // Factory implementations.
 inline SymVal make_concrete_bv(Num num, int width) {
-  auto it = concrete_pool.find(num.toInt());
-  if (it != concrete_pool.end()) {
+  auto key = SmallBVKey(width, num.toInt64());
+  auto it = SmallBVStore.find(key);
+  if (it != SmallBVStore.end()) {
     return it->second;
   }
 
   auto new_val =
       SymVal(SymBookKeeper.allocate<SymConcrete>(num, KindBV, width));
-  concrete_pool.insert({num.toInt(), new_val});
+  SmallBVStore.insert({key, new_val});
   return new_val;
 }
 
 inline SymVal make_concrete_fp(Num num, int width) {
-  auto it = concrete_pool.find(num.toInt());
-  if (it != concrete_pool.end()) {
+  auto it = FPStore.find(num.toInt64());
+  if (it != FPStore.end()) {
     return it->second;
   }
 
   auto new_val =
       SymVal(SymBookKeeper.allocate<SymConcrete>(num, KindFP, width));
-  concrete_pool.insert({num.toInt(), new_val});
+  FPStore.insert({num.toInt64(), new_val});
   return new_val;
 }
 
@@ -205,7 +206,8 @@ inline SymVal make_extract(const SymVal &value, int high, int low) {
 
   if (auto concrete = std::dynamic_pointer_cast<SymConcrete>(value.symptr)) {
     if (concrete->kind != KindBV) {
-      throw std::runtime_error("Extract only supports bitvector concrete values");
+      throw std::runtime_error(
+          "Extract only supports bitvector concrete values");
     }
     // extract from concrete bitvector value
     int64_t val = concrete->value.value;
@@ -520,7 +522,8 @@ inline SymVal make_binary(BinOperation op, const SymVal &lhs,
     }
   }
 
-  auto result = SymVal(SVFactory::SymBookKeeper.allocate<SymBinary>(op, lhs, rhs));
+  auto result =
+      SymVal(SVFactory::SymBookKeeper.allocate<SymBinary>(op, lhs, rhs));
   BinaryOperationStore.insert({key, result});
   return result;
 }
@@ -594,8 +597,8 @@ inline SymVal make_unary(UnaryOperation op, const SymVal &value) {
         break;
       }
       if (negated_op != inner_binary->op) {
-        auto result =
-            SVFactory::make_binary(negated_op, inner_binary->lhs, inner_binary->rhs);
+        auto result = SVFactory::make_binary(negated_op, inner_binary->lhs,
+                                             inner_binary->rhs);
         UnaryOperationStore.insert({key, result});
         return result;
       }
@@ -609,7 +612,8 @@ inline SymVal make_unary(UnaryOperation op, const SymVal &value) {
 
 inline SymVal make_concat(const SymVal &lhs, const SymVal &rhs) {
   if (auto lhs_concrete = std::dynamic_pointer_cast<SymConcrete>(lhs.symptr)) {
-    if (auto rhs_concrete = std::dynamic_pointer_cast<SymConcrete>(rhs.symptr)) {
+    if (auto rhs_concrete =
+            std::dynamic_pointer_cast<SymConcrete>(rhs.symptr)) {
       if (lhs_concrete->kind == KindBV && rhs_concrete->kind == KindBV) {
         int new_width = lhs_concrete->width() + rhs_concrete->width();
         int64_t new_value =