diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index 1aa3bd6b0..6cbf23a92 100644
--- a/kmir/src/kmir/__main__.py
+++ b/kmir/src/kmir/__main__.py
@@ -16,7 +16,7 @@
from .build import HASKELL_DEF_DIR, LLVM_DEF_DIR, LLVM_LIB_DIR
from .cargo import CargoProject
-from .kmir import KMIR, DecodeMode, KMIRAPRNodePrinter
+from .kmir import KMIR, KMIRAPRNodePrinter
from .linker import link
from .options import (
GenSpecOpts,
@@ -352,13 +352,6 @@ def _arg_parser() -> ArgumentParser:
prove_rs_parser.add_argument(
'--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
)
- prove_rs_parser.add_argument(
- '--decode-mode',
- type=DecodeMode,
- metavar='DECODE_MODE',
- default=DecodeMode.NONE,
- help='Allocation decoding mode: NONE (default), PARTIAL, or FULL',
- )
link_parser = command_parser.add_parser(
'link', help='Link together 2 or more SMIR JSON files', parents=[kcli_args.logging_args]
@@ -435,7 +428,6 @@ def _parse_args(ns: Namespace) -> KMirOpts:
save_smir=ns.save_smir,
smir=ns.smir,
start_symbol=ns.start_symbol,
- decode_mode=ns.decode_mode,
)
case 'link':
return LinkOpts(
diff --git a/kmir/src/kmir/alloc.py b/kmir/src/kmir/alloc.py
index 0d2010994..c2ce0b6bc 100644
--- a/kmir/src/kmir/alloc.py
+++ b/kmir/src/kmir/alloc.py
@@ -79,7 +79,7 @@ def from_dict(dct: dict[str, Any]) -> ProvenanceMap:
ptrs=[
ProvenanceEntry(
offset=int(size),
- prov=AllocId(prov),
+ alloc_id=AllocId(prov),
)
for size, prov in dct['ptrs']
],
@@ -88,4 +88,4 @@ def from_dict(dct: dict[str, Any]) -> ProvenanceMap:
class ProvenanceEntry(NamedTuple):
offset: int
- prov: AllocId
+ alloc_id: AllocId
diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py
index 5b8d6bade..c6effb3e3 100644
--- a/kmir/src/kmir/decoding.py
+++ b/kmir/src/kmir/decoding.py
@@ -4,8 +4,7 @@
from typing import TYPE_CHECKING
from pyk.kast.inner import KApply
-from pyk.kast.prelude.bytes import bytesToken
-from pyk.kast.prelude.kint import intToken
+from pyk.kast.prelude.string import stringToken
from .alloc import Allocation, AllocInfo, Memory, ProvenanceEntry, ProvenanceMap
from .ty import ArrayT, Bool, EnumT, Int, IntTy, PtrT, RefT, Uint
@@ -32,28 +31,12 @@
@dataclass
class UnableToDecodeValue(Value):
- data: bytes
- type_info: TypeMetadata
+ msg: str
def to_kast(self) -> KInner:
return KApply(
- 'Evaluation::UnableToDecodeValue',
- bytesToken(self.data),
- KApply('TypeInfo::VoidType'), # TODO: TypeInfo -> KAST transformation
- )
-
-
-@dataclass
-class UnableToDecodeAlloc(Value):
- data: bytes
- ty: Ty
-
- def to_kast(self) -> KInner:
- return KApply(
- 'Evaluation::UnableToDecodeAlloc',
- bytesToken(self.data),
- KApply('ty', intToken(self.ty)),
- KApply('ProvenanceMapEntries::empty'), # TODO
+ 'Evaluation::UnableToDecodePy',
+ stringToken(self.msg),
)
@@ -71,34 +54,50 @@ def decode_alloc_or_unable(alloc_info: AllocInfo, types: Mapping[Ty, TypeMetadat
),
):
data = bytes(n or 0 for n in bytez)
- type_info = types[ty]
-
- match ptrs:
- case []:
- return decode_value_or_unable(data=data, type_info=type_info, types=types)
-
- case [ProvenanceEntry(0, alloc_id)]:
- if (pointee_ty := _pointee_ty(type_info)) is not None: # ensures this is a reference type
- pointee_type_info = types[pointee_ty]
- metadata = _metadata(pointee_type_info)
-
- if len(data) == 8:
- # single slim pointer (assumes usize == u64)
- return AllocRefValue(alloc_id=alloc_id, metadata=metadata)
-
- if len(data) == 16 and metadata == DynamicSize(1):
- # sufficient data to decode dynamic size (assumes usize == u64)
- # expect fat pointer
- return AllocRefValue(
- alloc_id=alloc_id,
- metadata=DynamicSize(int.from_bytes(data[8:16], byteorder='little', signed=False)),
- )
-
- return UnableToDecodeAlloc(data=data, ty=ty)
+ return _decode_memory_alloc_or_unable(data=data, ptrs=ptrs, ty=ty, types=types)
case _:
raise AssertionError('Unhandled case')
+def _decode_memory_alloc_or_unable(
+ data: bytes,
+ ptrs: list[ProvenanceEntry],
+ ty: Ty,
+ types: Mapping[Ty, TypeMetadata],
+) -> Value:
+ try:
+ type_info = types[ty]
+ except KeyError:
+ return UnableToDecodeValue(f'Unknown type: {ty}')
+
+ match ptrs:
+ case []:
+ return decode_value_or_unable(data=data, type_info=type_info, types=types)
+
+ case [ProvenanceEntry(0, alloc_id)]:
+ if (pointee_ty := _pointee_ty(type_info)) is not None: # ensures this is a reference type
+ try:
+ pointee_type_info = types[pointee_ty]
+ except KeyError:
+ return UnableToDecodeValue(f'Unknown pointee type: {pointee_ty}')
+
+ metadata = _metadata(pointee_type_info)
+
+ if len(data) == 8:
+ # single slim pointer (assumes usize == u64)
+ return AllocRefValue(alloc_id=alloc_id, metadata=metadata)
+
+ if len(data) == 16 and metadata == DynamicSize(1):
+ # sufficient data to decode dynamic size (assumes usize == u64)
+ # expect fat pointer
+ return AllocRefValue(
+ alloc_id=alloc_id,
+ metadata=DynamicSize(int.from_bytes(data[8:16], byteorder='little', signed=False)),
+ )
+
+ return UnableToDecodeValue(f'Unable to decode alloc: {data!r}, of type: {type_info}')
+
+
def _pointee_ty(type_info: TypeMetadata) -> Ty | None:
match type_info:
case PtrT(ty) | RefT(ty):
@@ -120,8 +119,8 @@ def _metadata(type_info: TypeMetadata) -> Metadata:
def decode_value_or_unable(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMetadata]) -> Value:
try:
return decode_value(data=data, type_info=type_info, types=types)
- except ValueError:
- return UnableToDecodeValue(data=data, type_info=type_info)
+ except ValueError as err:
+ return UnableToDecodeValue(f'Unable to decode value: {data!r}, of type: {type_info}: {err}')
def decode_value(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMetadata]) -> Value:
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
index c4a30a549..62960e83b 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
@@ -14,14 +14,12 @@ from raw bytes to typed `Value` objects according to Rust's memory layout rules.
requires "../ty.md"
requires "value.md"
requires "numbers.md"
-requires "../alloc.md"
module RT-DECODING
imports BOOL
imports MAP
imports TYPES
- imports ALLOC
imports RT-VALUE-SYNTAX
imports RT-NUMBERS
imports RT-TYPES
@@ -37,9 +35,9 @@ and arrays (where layout is trivial).
### Decoding `PrimitiveType`s
```k
- syntax Evaluation ::= #decodeValue ( Bytes , TypeInfo , Map ) [function, total, symbol(decodeValue)]
- | UnableToDecodeValue( Bytes , TypeInfo ) [symbol(Evaluation::UnableToDecodeValue)]
- | UnableToDecodeAlloc( Bytes , Ty , ProvenanceMapEntries ) [symbol(Evaluation::UnableToDecodeAlloc)]
+ syntax Evaluation ::= #decodeValue ( Bytes , TypeInfo , Map ) [function, total, symbol(decodeValue)]
+ | UnableToDecode ( Bytes , TypeInfo ) [symbol(Evaluation::UnableToDecode)]
+ | UnableToDecodePy ( msg: String ) [symbol(Evaluation::UnableToDecodePy)]
// Boolean: should be one byte with value one or zero
rule #decodeValue(BYTES, typeInfoPrimitiveType(primTypeBool), _TYPEMAP) => BoolVal(false)
@@ -83,7 +81,7 @@ rule #decodeValue(BYTES, typeInfoArrayType(ELEMTY, noTyConst), TYPEMAP)
All unimplemented cases will become thunks by way of this default rule:
```k
- rule #decodeValue(BYTES, TYPEINFO, _TYPEMAP) => UnableToDecodeValue(BYTES, TYPEINFO) [owise]
+ rule #decodeValue(BYTES, TYPEINFO, _TYPEMAP) => UnableToDecode(BYTES, TYPEINFO) [owise]
```
## Helper function to determine the expected byte length for a type
@@ -283,100 +281,6 @@ by the element size, then uses the same element-by-element decoding approach as
[preserves-definedness]
```
-# Decoding the allocated constants into a memory map
-
-When the program starts, all allocated constants are stored in the `` cell in the configuration,
-as a mapping of `AllocId -> Value`, decoding the allocations to values using the above functions.
-
-Besides actual byte allocations, we often find allocations with provenance,
-as slim or fat pointers pointing to other static allocations.
-One example of this is allocated error strings, whose length is stored in a fat pointer that is itself an allocated constant.
-
-
-The basic decoding function is very similar to `#decodeConstant` but returns its result as a singleton `Map` instead of a mere value.
-
-```k
- syntax Map ::= #decodeAlloc ( AllocId , Ty , Allocation , Map ) [function] // returns AllocId |-> Value
- // ----------------------------------------------------------
- rule #decodeAlloc(ID, TY, allocation(BYTES, provenanceMap(.ProvenanceMapEntries), _ALIGN, _MUT), TYPEMAP)
- => ID |-> #decodeValue(BYTES, {TYPEMAP[TY]}:>TypeInfo, TYPEMAP)
- requires TY in_keys(TYPEMAP)
- andBool isTypeInfo(TYPEMAP[TY])
-```
-
-If there are entries in the provenance map, then the decoder must create references to other allocations.
-Each entry replaces a pointer starting at a certain offset in the bytes.
-The pointee of the respective pointer is determined by type _layout_ of the type to decode.
-
-Simple cases of offset 0 and reference types can be implemented here without consideration of layout.
-The reference metadata is either determined statically by type, or filled in from the bytes for fat pointers.
-
-```k
- // if length(BYTES) ==Int 16 decode BYTES[9..16] as dynamic size.
- rule #decodeAlloc(
- ID,
- TY,
- allocation(BYTES, provenanceMap(provenanceMapEntry(0, REF_ID) ), _ALIGN, _MUT),
- TYPEMAP
- )
- => ID |-> AllocRef(REF_ID, .ProjectionElems, dynamicSize(Bytes2Int(substrBytes(BYTES, 8, 16), LE, Unsigned)))
- requires TY in_keys(TYPEMAP)
- andBool isTypeInfo(TYPEMAP[TY])
- andBool isTy(pointeeTy({TYPEMAP[TY]}:>TypeInfo)) // ensures this is a reference type
- andBool lengthBytes(BYTES) ==Int 16 // sufficient data to decode dynamic size (assumes usize == u64)
- andBool dynamicSize(1) ==K #metadata(pointeeTy({TYPEMAP[TY]}:>TypeInfo), TYPEMAP) // expect fat pointer
- [preserves-definedness] // valid type lookup ensured
-
- // Otherwise query type information for static size and insert it.
- rule #decodeAlloc(
- ID,
- TY,
- allocation(BYTES, provenanceMap(provenanceMapEntry(0, REF_ID) ), _ALIGN, _MUT),
- TYPEMAP
- )
- => ID |-> AllocRef(REF_ID, .ProjectionElems, #metadata(pointeeTy({TYPEMAP[TY]}:>TypeInfo), TYPEMAP))
- requires TY in_keys(TYPEMAP)
- andBool isTypeInfo(TYPEMAP[TY])
- andBool isTy(pointeeTy({TYPEMAP[TY]}:>TypeInfo)) // ensures this is a reference type
- andBool lengthBytes(BYTES) ==Int 8 // single slim pointer (assumes usize == u64)
- [priority(60), preserves-definedness] // valid type lookup ensured
-```
-
-Allocations with more than one provenance map entry or witn non-reference types remain undecoded.
-
-```k
- rule #decodeAlloc(ID, TY, allocation(BYTES, provenanceMap(ENTRIES), _ALIGN, _MUT), _TYPEMAP)
- => ID |-> UnableToDecodeAlloc(BYTES, TY, ENTRIES)
- [owise]
-```
-
-The entire set of `GlobalAllocs` is decoded by iterating over the list.
-It is assumed that the given `Ty -> TypeInfo` map contains all types required.
-
-```k
- syntax Map ::= #decodeAllocs ( GlobalAllocs , Map ) [function, total, symbol("decodeAllocs") ] // AllocId |-> Thing
- | #decodeAllocsAux ( Map , GlobalAllocs , Map ) [function, total, symbol("decodeAllocsAux")] // accumulating version
- // -----------------------------------------------------------------------------------------------
- rule #decodeAllocs(ALLOCS, TYPEMAP) => #decodeAllocsAux(.Map, ALLOCS, TYPEMAP)
-
- rule #decodeAllocsAux(ACCUM, .GlobalAllocs, _TYPEMAP) => ACCUM
- rule #decodeAllocsAux(ACCUM, globalAllocEntry(ID, TY, Memory(ALLOC)) ALLOCS, TYPEMAP)
- => #decodeAllocsAux(ACCUM #decodeAlloc(ID, TY, ALLOC, TYPEMAP), ALLOCS, TYPEMAP)
- requires TY in_keys(TYPEMAP)
- [preserves-definedness]
-```
-
-If the type of an alloc cannot be found, or for non-`Memory` allocs, the raw data is stored in a super-sort of `Value`.
-This ensures that the function is total (anyway lookups require constraining the sort).
-
-```k
- syntax AllocData ::= Value | AllocData ( Ty , GlobalAllocKind )
-
- rule #decodeAllocsAux(ACCUM, globalAllocEntry(ID, TY, OTHER) ALLOCS, TYPEMAP)
- => #decodeAllocsAux(ACCUM ID |-> AllocData(TY, OTHER), ALLOCS, TYPEMAP)
- [owise]
-```
-
```k
endmodule
```
diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py
index 64abe4075..00d947cde 100644
--- a/kmir/src/kmir/kmir.py
+++ b/kmir/src/kmir/kmir.py
@@ -2,9 +2,8 @@
import logging
from contextlib import contextmanager
-from enum import Enum
from functools import cached_property
-from typing import TYPE_CHECKING, NamedTuple
+from typing import TYPE_CHECKING
from pyk.cli.utils import bug_report_arg
from pyk.cterm import CTerm, cterm_symbolic
@@ -43,24 +42,6 @@
_LOGGER: Final = logging.getLogger(__name__)
-class DecodeMode(Enum):
- FULL = 'full'
- PARTIAL = 'partial'
- NONE = 'none'
-
-
-class Decoded(NamedTuple):
- alloc_id: KInner
- value: KInner
-
-
-class Undecoded(NamedTuple):
- alloc: KInner
-
-
-DecodeRes = Decoded | Undecoded
-
-
class KMIR(KProve, KRun, KParse):
llvm_library_dir: Path | None
bug_report: BugReport | None
@@ -127,7 +108,6 @@ def make_call_config(
start_symbol: str = 'main',
sort: str = 'GeneratedTopCell',
init: bool = False,
- decode_mode: DecodeMode = DecodeMode.NONE,
) -> tuple[KInner, list[KInner]]:
if not start_symbol in smir_info.function_tys:
raise KeyError(f'{start_symbol} not found in program')
@@ -141,7 +121,7 @@ def make_call_config(
'STARTSYMBOL_CELL': KApply('symbol(_)_LIB_Symbol_String', (token(start_symbol),)),
'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack
'LOCALS_CELL': list_of(locals),
- 'MEMORY_CELL': self._make_memory_term(smir_info, types, decode_mode=decode_mode),
+ 'MEMORY_CELL': self._make_memory_map(smir_info, types),
'FUNCTIONS_CELL': self._make_function_map(smir_info),
'TYPES_CELL': types,
}
@@ -160,71 +140,31 @@ def make_call_config(
config = self.definition.empty_config(KSort(sort))
return (subst.apply(config), constraints)
- def _make_memory_term(self, smir_info: SMIRInfo, types: KInner, *, decode_mode: DecodeMode) -> KInner:
- done, rest = self._process_allocs(smir_info, decode_mode=decode_mode)
- return KApply('decodeAllocsAux', done, rest, types)
+ def _make_memory_map(self, smir_info: SMIRInfo, types: KInner) -> KInner:
+ raw_allocs = smir_info._smir['allocs']
+ return map_of(
+ self._decode_alloc(
+ smir_info=smir_info,
+ raw_alloc=raw_alloc,
+ )
+ for raw_alloc in raw_allocs
+ )
- def _process_allocs(self, smir_info: SMIRInfo, *, decode_mode: DecodeMode) -> tuple[KInner, KInner]:
- def global_allocs(allocs: list[KInner]) -> KInner:
- from pyk.kast.inner import build_cons
+ def _decode_alloc(self, smir_info: SMIRInfo, raw_alloc: Any) -> tuple[KInner, KInner]:
+ from .decoding import UnableToDecodeValue, decode_alloc_or_unable
- return build_cons(
- unit=KApply('GlobalAllocs::empty'),
- label='GlobalAllocs::append',
- terms=allocs,
- )
+ alloc_id = raw_alloc['alloc_id']
+ alloc_info = smir_info.allocs[alloc_id]
+ value = decode_alloc_or_unable(alloc_info=alloc_info, types=smir_info.types)
- done: list[tuple[KInner, KInner]] = []
- rest: list[KInner] = []
+ match value:
+ case UnableToDecodeValue(msg):
+ _LOGGER.debug(f'Decoding failed: {msg}')
+ case _:
+ pass
- for raw_alloc in smir_info._smir['allocs']:
- processed = self._process_alloc(
- smir_info=smir_info,
- raw_alloc=raw_alloc,
- decode_mode=decode_mode,
- )
- match processed:
- case Decoded():
- done.append(processed)
- case Undecoded(alloc):
- rest.append(alloc)
- case _:
- raise AssertionError('Unhandled case')
-
- _LOGGER.info(f'Allocations processed: {len(done)} decoded, {len(rest)} undecoded')
- return map_of(dict(done)), global_allocs(rest)
-
- def _process_alloc(self, smir_info: SMIRInfo, raw_alloc: Any, decode_mode: DecodeMode) -> DecodeRes:
- from .decoding import UnableToDecodeAlloc, UnableToDecodeValue, decode_alloc_or_unable
-
- if decode_mode in [DecodeMode.PARTIAL, DecodeMode.FULL]:
- alloc_id = raw_alloc['alloc_id']
- alloc_info = smir_info.allocs[alloc_id]
- value = decode_alloc_or_unable(alloc_info=alloc_info, types=smir_info.types)
-
- success: bool
- match value:
- case UnableToDecodeValue(data, type_info):
- _LOGGER.debug(f'Unable to decode value: {data!r}; of type: {type_info}')
- success = False
- case UnableToDecodeAlloc():
- _LOGGER.debug(f'Unable to decode allocation: {alloc_info}')
- success = False
- case _:
- success = True
-
- if success or decode_mode is DecodeMode.FULL:
- alloc_id_term = KApply('allocId', intToken(alloc_id))
- return Decoded(alloc_id=alloc_id_term, value=value.to_kast())
-
- alloc_term = self._parse_alloc(raw_alloc=raw_alloc)
- return Undecoded(alloc=alloc_term)
-
- def _parse_alloc(self, raw_alloc: Any) -> KInner:
- parse_res = self.parser.parse_mir_json(raw_alloc, 'GlobalAlloc')
- assert parse_res is not None
- res, _ = parse_res
- return res
+ alloc_id_term = KApply('allocId', intToken(alloc_id))
+ return alloc_id_term, value.to_kast()
def _make_function_map(self, smir_info: SMIRInfo) -> KInner:
parsed_terms: dict[KInner, KInner] = {}
@@ -261,8 +201,6 @@ def apr_proof_from_smir(
start_symbol: str = 'main',
sort: str = 'GeneratedTopCell',
proof_dir: Path | None = None,
- *,
- decode_mode: DecodeMode = DecodeMode.NONE,
) -> APRProof:
lhs_config, constraints = self.make_call_config(smir_info, start_symbol=start_symbol, sort=sort)
lhs = CTerm(lhs_config, constraints)
diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py
index a8adfcec5..f9e65808f 100644
--- a/kmir/src/kmir/options.py
+++ b/kmir/src/kmir/options.py
@@ -7,8 +7,6 @@
from pyk.cli.args import LoggingOptions
-from .kmir import DecodeMode
-
if TYPE_CHECKING:
from typing import Final
@@ -79,7 +77,6 @@ class ProveRSOpts(ProveOpts):
save_smir: bool
smir: bool
start_symbol: str
- decode_mode: DecodeMode
def __init__(
self,
@@ -92,7 +89,6 @@ def __init__(
save_smir: bool = False,
smir: bool = False,
start_symbol: str = 'main',
- decode_mode: DecodeMode = DecodeMode.NONE,
) -> None:
self.rs_file = rs_file
self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
@@ -103,7 +99,6 @@ def __init__(
self.save_smir = save_smir
self.smir = smir
self.start_symbol = start_symbol
- self.decode_mode = decode_mode
@dataclass
diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state
index c99ce67e3..572566d6e 100644
--- a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state
+++ b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state
@@ -59,7 +59,7 @@
allocId ( 3 ) |-> Range ( ListItem ( Integer ( 100 , 16 , false ) )
ListItem ( Integer ( 200 , 16 , false ) )
ListItem ( Integer ( 300 , 16 , false ) ) )
- allocId ( 4 ) |-> UnableToDecodeValue ( b"assertion failed: compare_to_stored(U16_ARRAY)" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 4 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: compare_to_stored(U16_ARRAY)', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state
index f8e825d62..2378cc197 100644
--- a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state
+++ b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state
@@ -84,8 +84,8 @@
ListItem ( Range ( ListItem ( Integer ( 100 , 16 , false ) )
ListItem ( Integer ( 200 , 16 , false ) )
ListItem ( Integer ( 300 , 16 , false ) ) ) ) )
- allocId ( 5 ) |-> UnableToDecodeValue ( b"assertion failed: compare_to_stored(U16_ARRAY)" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 6 ) |-> UnableToDecodeValue ( b"assertion failed: compare_to_stored(NESTED[0])" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 5 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: compare_to_stored(U16_ARRAY)', of type: Str(): Unsupported type: Str()" )
+ allocId ( 6 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: compare_to_stored(NESTED[0])', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state
index cecbee982..af7f14219 100644
--- a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state
+++ b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state
@@ -76,23 +76,23 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 0 ) |-> Range ( .List )
- allocId ( 1 ) |-> UnableToDecodeAlloc ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ty ( 99 ) , provenanceMapEntry (... offset: 0 , allocId: allocId ( 10 ) ) provenanceMapEntry (... offset: 8 , allocId: allocId ( 11 ) ) .ProvenanceMapEntries )
- allocId ( 2 ) |-> UnableToDecodeAlloc ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ty ( 99 ) , provenanceMapEntry (... offset: 0 , allocId: allocId ( 12 ) ) provenanceMapEntry (... offset: 8 , allocId: allocId ( 13 ) ) .ProvenanceMapEntries )
- allocId ( 3 ) |-> UnableToDecodeAlloc ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ty ( 108 ) , provenanceMapEntry (... offset: 0 , allocId: allocId ( 14 ) ) provenanceMapEntry (... offset: 8 , allocId: allocId ( 15 ) ) .ProvenanceMapEntries )
- allocId ( 4 ) |-> UnableToDecodeAlloc ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ty ( 108 ) , provenanceMapEntry (... offset: 0 , allocId: allocId ( 16 ) ) provenanceMapEntry (... offset: 8 , allocId: allocId ( 17 ) ) .ProvenanceMapEntries )
- allocId ( 5 ) |-> UnableToDecodeAlloc ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x00\x00\x00\x00\x00\x00" , ty ( 126 ) , provenanceMapEntry (... offset: 0 , allocId: allocId ( 18 ) ) .ProvenanceMapEntries )
- allocId ( 8 ) |-> UnableToDecodeValue ( b"Thing" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 9 ) |-> UnableToDecodeValue ( b"Another" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 10 ) |-> AllocData ( ty ( 0 ) , Memory ( allocation (... bytes: b"\x01\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityNot ) ) )
- allocId ( 11 ) |-> AllocData ( ty ( 0 ) , Memory ( allocation (... bytes: b"\x02\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityNot ) ) )
- allocId ( 12 ) |-> AllocData ( ty ( 0 ) , Memory ( allocation (... bytes: b"\x01\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityNot ) ) )
- allocId ( 13 ) |-> AllocData ( ty ( 0 ) , Memory ( allocation (... bytes: b"\x02\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityNot ) ) )
+ allocId ( 0 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'', of type: ArrayT(element_type=113, length=0): Method nbytes() is unsupported for type: StructT(name=\"core::fmt::rt::Argument<'_>\", adt_def=51, fields=[114])" )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode alloc: b'\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00', of type: EnumT(name=\"Thing<'_>\", adt_def=25, discriminants=[0], fields=[[37, 45]])" )
+ allocId ( 2 ) |-> UnableToDecodePy (... msg: "Unable to decode alloc: b'\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00', of type: EnumT(name=\"Thing<'_>\", adt_def=25, discriminants=[0], fields=[[37, 45]])" )
+ allocId ( 3 ) |-> UnableToDecodePy (... msg: "Unable to decode alloc: b'\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00', of type: StructT(name=\"Another<'_>\", adt_def=44, fields=[28, 42])" )
+ allocId ( 4 ) |-> UnableToDecodePy (... msg: "Unable to decode alloc: b'\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00', of type: StructT(name=\"Another<'_>\", adt_def=44, fields=[28, 42])" )
+ allocId ( 5 ) |-> UnableToDecodePy (... msg: "Unable to decode alloc: b'\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x00\\x16\\x00\\x00\\x00\\x00\\x00\\x00\\x00', of type: ArrayT(element_type=96, length=1)" )
+ allocId ( 8 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'Thing', of type: Str(): Unsupported type: Str()" )
+ allocId ( 9 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'Another', of type: Str(): Unsupported type: Str()" )
+ allocId ( 10 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
+ allocId ( 11 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
+ allocId ( 12 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
+ allocId ( 13 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
allocId ( 14 ) |-> Integer ( 1 , 32 , true )
allocId ( 15 ) |-> Integer ( 2 , 32 , false )
allocId ( 16 ) |-> Integer ( 1 , 32 , true )
allocId ( 17 ) |-> Integer ( 2 , 32 , false )
- allocId ( 18 ) |-> UnableToDecodeValue ( b"All assertions passed\n" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 18 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'All assertions passed\\n', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
index dfd97fc35..b70daeffa 100644
--- a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
+++ b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
@@ -55,8 +55,8 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 2 ) |-> UnableToDecodeValue ( b"unsafe precondition(s) violated: u8::unchecked_add cannot overflow" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 3 ) |-> UnableToDecodeValue ( b"unsafe precondition(s) violated: i8::unchecked_sub cannot overflow" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 2 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'unsafe precondition(s) violated: u8::unchecked_add cannot overflow', of type: Str(): Unsupported type: Str()" )
+ allocId ( 3 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'unsafe precondition(s) violated: i8::unchecked_sub cannot overflow', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
index fab3efbef..0eefe46ff 100644
--- a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
+++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
@@ -50,7 +50,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: b == c" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: b == c', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
index a96fc4825..8a4e5edac 100644
--- a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
+++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
@@ -59,7 +59,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: a[0] == a[1]" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: a[0] == a[1]', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state b/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state
index 9e478e825..78145c098 100644
--- a/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state
+++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state
@@ -41,7 +41,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: result" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: result', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state
index f2d2235fb..8bd3bc5aa 100644
--- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state
+++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state
@@ -87,10 +87,10 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 4 ) |-> UnableToDecodeValue ( b"assertion failed: arr.len() >= 4" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 5 ) |-> UnableToDecodeValue ( b"assertion failed: arr4.len() == 4" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 6 ) |-> UnableToDecodeValue ( b"assertion failed: l4 == 4" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 7 ) |-> UnableToDecodeValue ( b"assertion failed: arr9.len() == 9" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 4 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: arr.len() >= 4', of type: Str(): Unsupported type: Str()" )
+ allocId ( 5 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: arr4.len() == 4', of type: Str(): Unsupported type: Str()" )
+ allocId ( 6 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: l4 == 4', of type: Str(): Unsupported type: Str()" )
+ allocId ( 7 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: arr9.len() == 9', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state b/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state
index 594bc146b..4cdceffc2 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state
@@ -46,7 +46,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: *x == 0" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: *x == 0', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state
index 547a320a7..8de719016 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state
@@ -50,8 +50,8 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 2 ) |-> UnableToDecodeValue ( b"assertion failed: **z == x" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 3 ) |-> UnableToDecodeValue ( b"assertion failed: z == &&x" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 2 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: **z == x', of type: Str(): Unsupported type: Str()" )
+ allocId ( 3 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: z == &&x', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state
index 5e9bea5c1..8a99ac9d0 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state
@@ -45,8 +45,8 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 2 ) |-> UnableToDecodeValue ( b"assertion failed: x == 32" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 3 ) |-> UnableToDecodeValue ( b"assertion failed: x == 22" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 2 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: x == 32', of type: Str(): Unsupported type: Str()" )
+ allocId ( 3 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: x == 22', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state
index 620b57f93..da5ac298e 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state
@@ -40,7 +40,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: z == x" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: z == x', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state
index c935e2842..81f6e5870 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state
@@ -40,7 +40,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: z == x" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: z == x', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state
index 45e1209e3..ad14caad0 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state
@@ -41,7 +41,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: z == x" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: z == x', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/simple.state b/kmir/src/tests/integration/data/exec-smir/references/simple.state
index 367744d7e..199aed48b 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/simple.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/simple.state
@@ -39,7 +39,7 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 1 ) |-> UnableToDecodeValue ( b"assertion failed: z == x" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: z == x', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state
index 8410119d8..fd7efe8fd 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state
@@ -68,11 +68,11 @@
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
- allocId ( 5 ) |-> UnableToDecodeValue ( b"assertion failed: a.a_value == 42" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 6 ) |-> UnableToDecodeValue ( b"assertion failed: a.a_value == 43" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 7 ) |-> UnableToDecodeValue ( b"assertion failed: vv == 43" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 8 ) |-> UnableToDecodeValue ( b"assertion failed: a.another" , typeInfoPrimitiveType ( primTypeStr ) )
- allocId ( 9 ) |-> UnableToDecodeValue ( b"assertion failed: a.a_third == 43" , typeInfoPrimitiveType ( primTypeStr ) )
+ allocId ( 5 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: a.a_value == 42', of type: Str(): Unsupported type: Str()" )
+ allocId ( 6 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: a.a_value == 43', of type: Str(): Unsupported type: Str()" )
+ allocId ( 7 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: vv == 43', of type: Str(): Unsupported type: Str()" )
+ allocId ( 8 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: a.another', of type: Str(): Unsupported type: Str()" )
+ allocId ( 9 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: a.a_third == 43', of type: Str(): Unsupported type: Str()" )
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state
index 182a85ae4..4dd00c908 100644
--- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state
+++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/struct_field_update.state
@@ -28,7 +28,7 @@
ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 32 , true ) )
ListItem ( BoolVal ( true ) )
- ListItem ( thunk ( UnableToDecodeValue ( b"33333sE@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) )
+ ListItem ( thunk ( UnableToDecode ( b"33333sE@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) )
ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 32 , true ) )
ListItem ( Integer ( 10 , 32 , true ) ) ) ) ) , ty ( 28 ) , mutabilityMut ) )
ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state
index fdf922fb2..ddfc6ca7a 100644
--- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state
+++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state
@@ -28,17 +28,17 @@
ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( 10 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
ListItem ( typedValue ( BoolVal ( false ) , ty ( 26 ) , mutabilityNot ) )
- ListItem ( typedValue ( thunk ( UnableToDecodeValue ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) , ty ( 27 ) , mutabilityNot ) )
+ ListItem ( typedValue ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) , ty ( 27 ) , mutabilityNot ) )
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 32 , true ) )
ListItem ( BoolVal ( false ) )
- ListItem ( thunk ( UnableToDecodeValue ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 28 ) , mutabilityNot ) )
+ ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 28 ) , mutabilityNot ) )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 32 , true ) )
ListItem ( BoolVal ( true ) )
- ListItem ( thunk ( UnableToDecodeValue ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 29 ) , mutabilityNot ) )
+ ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) ) , ty ( 29 ) , mutabilityNot ) )
ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) )
ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) )
ListItem ( typedValue ( Moved , ty ( 16 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
index 1bb59e468..d387d0c29 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
@@ -5,7 +5,7 @@
│
│ (159 steps)
└─ 3 (stuck, leaf)
- #traverseProjection ( toStack ( 3 , local ( 1 ) ) , thunk ( UnableToDecodeValue
+ #traverseProjection ( toStack ( 3 , local ( 1 ) ) , thunk ( UnableToDecode ( b"\
span: 86