Symbolic memory

benchmarks/wasm/Makefile

@@ -0,0 +1,7 @@
+.PHONY: clean
+
+clean:
+	find . -type f -name '*.cpp' -delete
+	find . -type f -name '*.cpp.exe' -delete
+	find . -type d -name '*.dSYM' -exec rm -rf {} +
+	find . -type f -name '*.dot' -delete

benchmarks/wasm/load-offset.wat

@@ -0,0 +1,19 @@
+(module
+  (type (;0;) (func (result i32)))
+  (type (;1;) (func))
+  (func (;0;) (type 0) (result i32)
+    i32.const 0
+    i32.const 256
+    i32.store 
+    i32.const 0
+    i32.load offset=1
+  )
+  (func (;1;) (type 1)
+    call 0
+    ;; should be 1
+    ;; drop
+  )
+  (start 1)
+  (memory (;0;) 2)
+  (export "main" (func 1))
+)

benchmarks/wasm/load-overflow1.wat

@@ -0,0 +1,19 @@
+(module
+  (type (;0;) (func (result i32)))
+  (type (;1;) (func))
+  (func (;0;) (type 0) (result i32)
+    i32.const 0
+    i32.const 256
+    i32.store 
+    i32.const 1
+    i32.load
+  )
+  (func (;1;) (type 1)
+    call 0
+    ;; should be 1
+    ;; drop
+  )
+  (start 1)
+  (memory (;0;) 2)
+  (export "main" (func 1))
+)

benchmarks/wasm/load-overflow2.wat

@@ -0,0 +1,19 @@
+(module
+  (type (;0;) (func (result i32)))
+  (type (;1;) (func))
+  (func (;0;) (type 0) (result i32)
+    i32.const 0
+    i32.const 65536
+    i32.store 
+    i32.const 2
+    i32.load
+  )
+  (func (;1;) (type 1)
+    call 0
+    ;; should be 1
+    ;; drop
+  )
+  (start 1)
+  (memory (;0;) 2)
+  (export "main" (func 1))
+)

benchmarks/wasm/load.wat

@@ -10,7 +10,7 @@
   )
   (func (;1;) (type 1)
     call 0
-    ;; should be 65536
+    ;; should be 1
     ;; drop
     )
   (start 1)

benchmarks/wasm/mem-sym-extract.wat

@@ -0,0 +1,32 @@
+(module
+  (type (;0;) (func (result i32)))
+  (type (;1;) (func))
+  (type (;2;) (func (param i32) (result i32)))
+  (type (;3;) (func (param i32)))
+  (import "console" "assert" (func (type 3)))
+  (func (;1;) (type 2) (param i32) (result i32)
+    i32.const 0
+    local.get 0
+    i32.store
+    i32.const 0
+    i32.load
+    i32.const 1
+    i32.eq
+    if (result i32)  ;; if x == 256
+      i32.const 1 ;; return 1
+    else
+      i32.const 0 
+      call 0 ;; assert false
+      i32.const 1 ;; to satisfy the type checker, this line will never be reached
+    end
+  )
+  (func (;2;) (type 1)
+    i32.const 0
+    i32.symbolic ;; call it x
+    call 1
+  )
+  (start 2)
+  (memory (;0;) 2)
+  (export "main" (func 1))
+  (global (;0;) (mut i32) (i32.const 42))
+)

benchmarks/wasm/mem-sym.wat

@@ -0,0 +1,32 @@
+(module
+  (type (;0;) (func (result i32)))
+  (type (;1;) (func))
+  (type (;2;) (func (param i32) (result i32)))
+  (type (;3;) (func (param i32)))
+  (import "console" "assert" (func (type 3)))
+  (func (;1;) (type 2) (param i32) (result i32)
+    i32.const 0
+    local.get 0
+    i32.store
+    i32.const 0
+    i32.load
+    i32.const 25
+    i32.eq
+    if (result i32)  ;; if x == 25
+      i32.const 1 ;; return 1
+    else
+      i32.const 0 
+      call 0 ;; assert false
+      i32.const 1 ;; to satisfy the type checker, this line will never be reached
+    end
+  )
+  (func (;2;) (type 1)
+    i32.const 0
+    i32.symbolic ;; call it x
+    call 1
+  )
+  (start 2)
+  (memory (;0;) 2)
+  (export "main" (func 1))
+  (global (;0;) (mut i32) (i32.const 42))
+)

headers/wasm/concrete_rt.hpp

@@ -74,6 +74,7 @@ class Stack_t {
   Num pop() {
 #ifdef DEBUG
     assert(count > 0 && "Stack underflow");
+    printf("[Debug] poping from stack, size of concrete stack is: %d\n", count);
 #endif
     Num num = stack_ptr[count - 1];
     count--;
@@ -99,9 +100,13 @@ class Stack_t {
     if (size < 0) {
       throw std::out_of_range("Invalid size: " + std::to_string(size));
     }
+    std::cout << "Shifting stack by offset " << offset << " and size " << size
+              << std::endl;
+    std::cout << "Current stack size: " << count << std::endl;
 #endif
     // shift last `size` of numbers forward of `offset`
     for (int32_t i = count - size; i < count; ++i) {
+      assert(i - offset >= 0);
       stack_ptr[i - offset] = stack_ptr[i];
     }
     count -= offset;
@@ -195,39 +200,4 @@ static std::monostate unreachable() {
 static int32_t pagesize = 65536;
 static int32_t page_count = 0;
 
-struct Memory_t {
-  std::vector<uint8_t> memory;
-  Memory_t(int32_t init_page_count) : memory(init_page_count * pagesize) {}
-
-  int32_t loadInt(int32_t base, int32_t offset) {
-    return *reinterpret_cast<int32_t *>(static_cast<uint8_t *>(memory.data()) +
-                                        base + offset);
-  }
-
-  std::monostate storeInt(int32_t base, int32_t offset, int32_t value) {
-    *reinterpret_cast<int32_t *>(static_cast<uint8_t *>(memory.data()) + base +
-                                 offset) = value;
-    return std::monostate{};
-  }
-
-  // grow memory by delta bytes when bytes > 0. return -1 if failed, return old
-  // size when success
-  int32_t grow(int32_t delta) {
-    if (delta <= 0) {
-      return memory.size();
-    }
-
-    try {
-      memory.resize(memory.size() + delta * pagesize);
-      auto old_page_count = page_count;
-      page_count += delta;
-      return memory.size();
-    } catch (const std::bad_alloc &e) {
-      return -1;
-    }
-  }
-};
-
-static Memory_t Memory(1); // 1 page memory
-
 #endif // WASM_CONCRETE_RT_HPP

headers/wasm/smt_solver.hpp

@@ -71,6 +71,9 @@ inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) {
   } else if (auto concrete =
                  std::dynamic_pointer_cast<SymConcrete>(sym_val.symptr)) {
     return z3_ctx.bv_val(concrete->value.value, 32);
+  } else if (auto smallbv =
+                 std::dynamic_pointer_cast<SmallBV>(sym_val.symptr)) {
+    return z3_ctx.bv_val(smallbv->get_value(), smallbv->get_size());
   } else if (auto binary =
                  std::dynamic_pointer_cast<SymBinary>(sym_val.symptr)) {
     auto bit_width = 32;
@@ -119,7 +122,23 @@ inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) {
     case DIV: {
       return left / right;
     }
+    case B_AND: {
+      return left & right;
     }
+    case CONCAT: {
+      return z3::concat(left, right);
+    }
+    default:
+      throw std::runtime_error("Operation not supported: " +
+                               std::to_string(binary->op));
+    }
+  } else if (auto extract = dynamic_cast<SymExtract *>(sym_val.symptr.get())) {
+    assert(extract);
+    int high = extract->high * 8 - 1;
+    int low = extract->low * 8 - 8;
+    auto s = build_z3_expr(extract->value);
+    auto res = s.extract(high, low);
+    return res;
   }
   throw std::runtime_error("Unsupported symbolic value type");
 }