SymbolicMemoryView is always writable — memoryview readonly not modeled

[pschanely]

Summary

SymbolicMemoryView never models a read-only memoryview. register_type(memoryview, lambda p: SymbolicMemoryView(p(bytearray))) always backs the view with a mutable SymbolicByteArray, and SymbolicMemoryView.__init__ sets self.readonly = isinstance(obj, bytes) — which is therefore always False. So a symbolic memoryview is always writable, whereas a concrete memoryview(b"...") is read-only.

Impact

Write-through operations diverge from CPython:

• Concrete: memoryview(b"ab")[0] = 1 → TypeError: cannot modify read-only memory
• Symbolic: succeeds (mutates the backing bytearray)

This can produce false divergences in the single-operation differential (fuzz_core_test / tools/measure_support) for memoryview write ops, and generally under-models read-only views.

Where

• crosshair/libimpl/builtinslib.py — SymbolicMemoryView.__init__: self.readonly = isinstance(obj, bytes)
• crosshair/libimpl/builtinslib.py — register_type(memoryview, lambda p: SymbolicMemoryView(p(bytearray)))

The __setitem__ guard already raises TypeError when self.readonly — the flag is just never True.

Related

SymbolicMemoryView intentionally has no _smt_for_unification (a view's equality is only over the viewed bytes, no clean full SMT form), so memoryview inputs currently can't be pinned in the differential and are skipped. Modeling readonly is likely a prerequisite to meaningfully enabling memoryview coverage there.

Possible directions

• Have proxy_for_type(memoryview) sometimes choose a bytes (read-only) backing and set readonly accordingly.
• Ensure write ops honor readonly.

Found while adding the differential support-measurement (branch demo-support-measurement).