Skip to content

Commit d401761

Browse files
tothtamas28tothtamas28
authored
Decode strings (#731)
1 parent 8fba85a commit d401761

22 files changed

Lines changed: 82 additions & 30 deletions

‎kmir/src/kmir/decoding.py‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
from pyk.kast.prelude.string import stringToken
88

99
from .alloc import Allocation, AllocInfo, Memory, ProvenanceEntry, ProvenanceMap
10-
from .ty import ArrayT, Bool, EnumT, Int, IntTy, PtrT, RefT, Uint
10+
from .ty import ArrayT, Bool, EnumT, Int, IntTy, PtrT, RefT, Str, Uint
1111
from .value import (
1212
NO_METADATA,
1313
AggregateValue,
@@ -17,6 +17,7 @@
1717
IntValue,
1818
RangeValue,
1919
StaticSize,
20+
StrValue,
2021
Value,
2122
)
2223

@@ -127,6 +128,8 @@ def decode_value(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMe
127128
match type_info:
128129
case Bool():
129130
return _decode_bool(data)
131+
case Str():
132+
return _decode_str(data)
130133
case Uint(int_ty) | Int(int_ty):
131134
return _decode_int(data, int_ty)
132135
case ArrayT(elem_ty, length):
@@ -147,6 +150,10 @@ def _decode_bool(data: bytes) -> Value:
147150
raise ValueError(f'Cannot decode as Bool: {data!r}')
148151

149152

153+
def _decode_str(data: bytes) -> Value:
154+
return StrValue(data.decode('utf-8'))
155+
156+
150157
def _decode_int(data: bytes, int_ty: IntTy | UintTy) -> Value:
151158
nbytes = int_ty.value
152159
if len(data) != nbytes:

‎kmir/src/kmir/kdist/mir-semantics/rt/value.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ The special `Moved` value represents values that have been used and should not b
2929
// value, bit-width, signedness for un/signed int
3030
| BoolVal( Bool ) [symbol(Value::BoolVal)]
3131
// boolean
32+
| StringVal( String ) [symbol(Value::StringVal)]
33+
// UTF-8 encoded Unicode string
3234
| Aggregate( VariantIdx , List ) [symbol(Value::Aggregate)]
3335
// heterogenous value list for tuples and structs (standard, tuple, or anonymous)
3436
| Float( Float, Int ) [symbol(Value::Float)]

‎kmir/src/kmir/value.py‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
from pyk.kast.prelude.collections import list_of
99
from pyk.kast.prelude.kbool import boolToken
1010
from pyk.kast.prelude.kint import intToken
11+
from pyk.kast.prelude.string import stringToken
1112

1213
if TYPE_CHECKING:
1314
from collections.abc import Iterable
@@ -46,6 +47,17 @@ def to_kast(self) -> KInner:
4647
)
4748

4849

50+
@dataclass
51+
class StrValue(Value):
52+
value: str
53+
54+
def to_kast(self) -> KInner:
55+
return KApply(
56+
'Value::StringVal',
57+
stringToken(self.value),
58+
)
59+
60+
4961
@dataclass
5062
class RangeValue(Value):
5163
elems: tuple[Value, ...]

‎kmir/src/tests/integration/data/decode-value/str.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
StringVal ( "Hello, World! \xf0\x9f\x8c\x8f" )

‎kmir/src/tests/integration/data/decode-value/str.json‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
{
2+
"bytes": [
3+
72,
4+
101,
5+
108,
6+
108,
7+
111,
8+
44,
9+
32,
10+
87,
11+
111,
12+
114,
13+
108,
14+
100,
15+
33,
16+
32,
17+
240,
18+
159,
19+
140,
20+
143
21+
],
22+
"types": [],
23+
"typeInfo": {
24+
"PrimitiveType": "Str"
25+
}
26+
}

‎kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@
5959
allocId ( 3 ) |-> Range ( ListItem ( Integer ( 100 , 16 , false ) )
6060
ListItem ( Integer ( 200 , 16 , false ) )
6161
ListItem ( Integer ( 300 , 16 , false ) ) )
62-
allocId ( 4 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: compare_to_stored(U16_ARRAY)', of type: Str(): Unsupported type: Str()" )
62+
allocId ( 4 ) |-> StringVal ( "assertion failed: compare_to_stored(U16_ARRAY)" )
6363
</memory>
6464
<functions>
6565
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )

‎kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,8 +84,8 @@
8484
ListItem ( Range ( ListItem ( Integer ( 100 , 16 , false ) )
8585
ListItem ( Integer ( 200 , 16 , false ) )
8686
ListItem ( Integer ( 300 , 16 , false ) ) ) ) )
87-
allocId ( 5 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: compare_to_stored(U16_ARRAY)', of type: Str(): Unsupported type: Str()" )
88-
allocId ( 6 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: compare_to_stored(NESTED[0])', of type: Str(): Unsupported type: Str()" )
87+
allocId ( 5 ) |-> StringVal ( "assertion failed: compare_to_stored(U16_ARRAY)" )
88+
allocId ( 6 ) |-> StringVal ( "assertion failed: compare_to_stored(NESTED[0])" )
8989
</memory>
9090
<functions>
9191
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )

‎kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,8 @@
8282
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])" )
8383
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])" )
8484
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)" )
85-
allocId ( 8 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'Thing', of type: Str(): Unsupported type: Str()" )
86-
allocId ( 9 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'Another', of type: Str(): Unsupported type: Str()" )
85+
allocId ( 8 ) |-> StringVal ( "Thing" )
86+
allocId ( 9 ) |-> StringVal ( "Another" )
8787
allocId ( 10 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
8888
allocId ( 11 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
8989
allocId ( 12 ) |-> UnableToDecodePy (... msg: "Unknown type: 0" )
@@ -92,7 +92,7 @@
9292
allocId ( 15 ) |-> Integer ( 2 , 32 , false )
9393
allocId ( 16 ) |-> Integer ( 1 , 32 , true )
9494
allocId ( 17 ) |-> Integer ( 2 , 32 , false )
95-
allocId ( 18 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'All assertions passed\\n', of type: Str(): Unsupported type: Str()" )
95+
allocId ( 18 ) |-> StringVal ( "All assertions passed\n" )
9696
</memory>
9797
<functions>
9898
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )

‎kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,8 @@
5555
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
5656
</stack>
5757
<memory>
58-
allocId ( 2 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'unsafe precondition(s) violated: u8::unchecked_add cannot overflow', of type: Str(): Unsupported type: Str()" )
59-
allocId ( 3 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'unsafe precondition(s) violated: i8::unchecked_sub cannot overflow', of type: Str(): Unsupported type: Str()" )
58+
allocId ( 2 ) |-> StringVal ( "unsafe precondition(s) violated: u8::unchecked_add cannot overflow" )
59+
allocId ( 3 ) |-> StringVal ( "unsafe precondition(s) violated: i8::unchecked_sub cannot overflow" )
6060
</memory>
6161
<functions>
6262
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )

‎kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@
5050
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
5151
</stack>
5252
<memory>
53-
allocId ( 1 ) |-> UnableToDecodePy (... msg: "Unable to decode value: b'assertion failed: b == c', of type: Str(): Unsupported type: Str()" )
53+
allocId ( 1 ) |-> StringVal ( "assertion failed: b == c" )
5454
</memory>
5555
<functions>
5656
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )

0 commit comments

Comments
 (0)