Improve WASM Memory Ergonomics

manticore/platforms/wasm.py

@@ -86,6 +86,8 @@ def __setstate__(self, state):
         self.forward_events_from(self.stack)
         self.forward_events_from(self.instance)
         self.forward_events_from(self.instance.executor)
+        for mem in self.store.mems:
+            self.forward_events_from(mem)
         super().__setstate__(state)
 
     @property
@@ -254,7 +256,9 @@ def get_module_imports(self, module, exec_start, stub_missing) -> typing.List[Ex
                             partial(stub, len(func_type.result_types)),  # type: ignore
                         )
                     )
-                    imports.append(FuncAddr(len(self.store.funcs) - 1))
+                    addr = FuncAddr(len(self.store.funcs) - 1)
+                    imports.append(addr)
+                    self.instance.function_names[addr] = f"{i.module}.{i.name}"
 
                 elif isinstance(i.desc, TableType):
                     self.store.tables.append(
@@ -311,6 +315,8 @@ def instantiate(
         for k in supplemental_env:
             self.set_env(supplemental_env[k], k)
         self.import_module(self.default_module, exec_start, stub_missing)
+        for mem in self.store.mems:
+            self.forward_events_from(mem)
 
     def invoke(self, name="main", argv=[], module=None):
         """

manticore/wasm/executor.py

@@ -41,14 +41,7 @@ class Executor(Eventful):
     https://www.w3.org/TR/wasm-core-1/#a7-index-of-instructions
     """
 
-    _published_events = {
-        "write_memory",
-        "read_memory",
-        "set_global",
-        "read_global",
-        "set_local",
-        "read_local",
-    }
+    _published_events = {"set_global", "get_global", "set_local", "get_local"}
 
     def __init__(self, constraints, *args, **kwargs):
 
@@ -346,7 +339,7 @@ def set_global(self, store, stack, imm: GlobalVarXsImm):
         a = f.module.globaladdrs[imm.global_index]
         assert a in range(len(store.globals))
         stack.has_type_on_top(Value_t, 1)
-        self._publish("did_set_global", imm.global_index, stack.peek())
+        self._publish("will_set_global", imm.global_index, stack.peek())
         store.globals[a].value = stack.pop()
         self._publish("did_set_global", imm.global_index, store.globals[a].value)
 
@@ -363,12 +356,10 @@ def i32_load(self, store, stack, imm: MemoryImm):
                 -1, I32, "Concretizing memory read", i
             )  # TODO - Implement a symbolic memory model
         ea = i + imm.offset
-        if (ea + 4) not in range(len(mem.data) + 1):
+        if (ea + 4) - 1 not in mem:
             raise OutOfBoundsMemoryTrap(ea + 4)
-        self._publish("will_read_memory", ea, ea + 4)
-        c = Operators.CONCAT(32, *map(Operators.ORD, reversed(mem.data[ea : ea + 4])))
+        c = mem.read_int(ea, 32)
         stack.push(I32.cast(c))
-        self._publish("did_read_memory", ea, stack.peek())
 
     def i64_load(self, store, stack, imm: MemoryImm):
         f = stack.get_frame().frame
@@ -383,12 +374,10 @@ def i64_load(self, store, stack, imm: MemoryImm):
                 -1, I32, "Concretizing memory read", i
             )  # TODO - Implement a symbolic memory model
         ea = i + imm.offset
-        if (ea + 8) not in range(len(mem.data) + 1):
+        if (ea + 8) - 1 not in mem:
             raise OutOfBoundsMemoryTrap(ea + 8)
-        self._publish("will_read_memory", ea, ea + 8)
-        c = Operators.CONCAT(64, *map(Operators.ORD, reversed(mem.data[ea : ea + 8])))
+        c = mem.read_int(ea, 64)
         stack.push(I64.cast(c))
-        self._publish("did_read_memory", ea, stack.peek())
 
     def int_load(self, store, stack, imm: MemoryImm, ty: type, size: int, signed: bool):
         assert ty in {I32, I64}, f"{type(ty)} is not an I32 or I64"
@@ -404,20 +393,18 @@ def int_load(self, store, stack, imm: MemoryImm, ty: type, size: int, signed: bo
                 -1, I32, "Concretizing memory read", i
             )  # TODO - Implement a symbolic memory model
         ea = i + imm.offset
-        if ea not in range(len(mem.data)):
+        if ea not in mem:
             raise OutOfBoundsMemoryTrap(ea)
-        if ea + (size // 8) not in range(len(mem.data) + 1):
+        if ea + (size // 8) - 1 not in mem:
             raise OutOfBoundsMemoryTrap(ea + (size // 8))
-        self._publish("will_read_memory", ea, ea + size // 8)
-        c = Operators.CONCAT(size, *map(Operators.ORD, reversed(mem.data[ea : ea + (size // 8)])))
+        c = mem.read_int(ea, size)
         width = 32 if ty is I32 else 64
         if signed:
             c = Operators.SEXTEND(c, size, width)
         else:
             c = Operators.ZEXTEND(c, width)
         # Mypy can't figure out that that ty will definitely have a cast method, so we ignore the type
         stack.push(ty.cast(c))  # type: ignore
-        self._publish("did_read_memory", ea, stack.peek())
 
     def i32_load8_s(self, store, stack, imm: MemoryImm):
         self.int_load(store, stack, imm, I32, 8, True)
@@ -466,9 +453,9 @@ def int_store(self, store, stack, imm: MemoryImm, ty: type, n=None):
             )  # TODO - Implement a symbolic memory model
         ea = i + imm.offset
         N = n if n else (32 if ty is I32 else 64)
-        if ea not in range(len(mem.data)):
+        if ea not in mem:
             raise OutOfBoundsMemoryTrap(ea)
-        if (ea + (N // 8)) not in range(len(mem.data) + 1):
+        if (ea + (N // 8)) - 1 not in mem:
             raise OutOfBoundsMemoryTrap(ea + (N // 8))
         if n:
             b = [
@@ -477,10 +464,7 @@ def int_store(self, store, stack, imm: MemoryImm, ty: type, n=None):
         else:
             b = [Operators.CHR(Operators.EXTRACT(c, offset, 8)) for offset in range(0, N, 8)]
 
-        self._publish("will_write_memory", ea, ea + len(b), b)
-        for idx, v in enumerate(b):
-            mem.data[ea + idx] = v
-        self._publish("did_write_memory", ea, b)
+        mem.write_bytes(ea, b)
 
     def i32_store(self, store, stack, imm: MemoryImm):
         self.int_store(store, stack, imm, I32)
@@ -509,15 +493,15 @@ def current_memory(self, store, stack, imm: CurGrowMemImm):
         a = f.module.memaddrs[0]
         assert a in range(len(store.mems))
         mem = store.mems[a]
-        stack.push(I32(len(mem.data) // 65536))
+        stack.push(I32(mem.npages))
 
     def grow_memory(self, store, stack, imm: CurGrowMemImm):
         f = stack.get_frame().frame
         assert f.module.memaddrs
         a = f.module.memaddrs[0]
         assert a in range(len(store.mems))
         mem = store.mems[a]
-        sz = len(mem.data) // 65536
+        sz = mem.npages
         stack.has_type_on_top(I32, 1)
         if issymbolic(stack.peek()):
             raise ConcretizeStack(-1, I32, "Concretizing memory grow operand", stack.peek())
@@ -1228,16 +1212,14 @@ def float_load(self, store, stack, imm: MemoryImm, ty: type):
                 -1, I32, "Concretizing float memory read", i
             )  # TODO - Implement a symbolic memory model
         ea = i + imm.offset
-        if ea not in range(len(mem.data)):
+        if ea not in mem:
             raise OutOfBoundsMemoryTrap(ea)
-        if (ea + (size // 8)) not in range(len(mem.data) + 1):
+        if (ea + (size // 8)) - 1 not in mem:
             raise OutOfBoundsMemoryTrap(ea + (size // 8))
-        self._publish("will_read_memory", ea, ea + (size // 8))
-        c = Operators.CONCAT(size, *map(Operators.ORD, reversed(mem.data[ea : ea + (size // 8)])))
+        c = mem.read_int(ea, size)
         # Mypy can't figure out that that ty will definitely have a cast method, so we ignore the type
         ret = ty.cast(c)  # type: ignore
         stack.push(ret)
-        self._publish("did_read_memory", ea, stack.peek())
 
     def f32_load(self, store, stack, imm: MemoryImm):
         return self.float_load(store, stack, imm, F32)
@@ -1258,19 +1240,16 @@ def float_store(self, store, stack, imm: MemoryImm, ty: type, n=None):
             size = 32
         else:
             size = 64
-        if ea not in range(len(mem.data)):
+        if ea not in mem:
             raise OutOfBoundsMemoryTrap(ea)
-        if (ea + (size // 8)) not in range(len(mem.data) + 1):
+        if (ea + (size // 8)) - 1 not in mem:
             raise OutOfBoundsMemoryTrap(ea + (size // 8))
         if not issymbolic(c):
             c = struct.unpack(
                 "i" if size == 32 else "q", struct.pack("f" if size == 32 else "d", c)
             )[0]
         b = [Operators.CHR(Operators.EXTRACT(c, offset, 8)) for offset in range(0, size, 8)]
-        self._publish("will_write_memory", ea, ea + len(b), b)
-        for idx, v in enumerate(b):
-            mem.data[ea + idx] = v
-        self._publish("did_write_memory", ea, b)
+        mem.write_bytes(ea, b)
 
     def float_push_compare_return(self, stack, v, rettype=I32):
         if issymbolic(v):

manticore/wasm/manticore.py

@@ -212,7 +212,7 @@ def generate_testcase(self, state, message="test", name="test"):
             stackf.write(str(state.stack.data))
 
         with testcase.open_stream("memory") as memoryf:
-            memoryf.write(str(state.mem.data))
+            memoryf.write(str(state.mem.dump()))
 
         term = getattr(state, "_terminated_by", None)
         if term: