Skip to content

Commit 9f57b55

Browse files
rv-jenkinsrv-auditorjberthold
authored
Update dependency: deps/stable-mir-json_release (#639)
Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
1 parent 51d8d8d commit 9f57b55

51 files changed

Lines changed: 12043 additions & 960 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎deps/stable-mir-json‎

Submodule stable-mir-json updated 40 files

‎deps/stable-mir-json_release‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
89a011e5a590635892fffae9ffd16885106c14e3
1+
9610a3fcb6e8f07fb72622ffa7e5b69122eef89f

‎kmir/src/kmir/kdist/mir-semantics/alloc.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@ syntax GlobalAllocKind ::= globalAllocFunction(Instance)
3030
| Memory(Allocation)
3131
[group(mir-enum), symbol(GlobalAllocKind::Memory)]
3232
33-
syntax GlobalAlloc ::= globalAllocEntry(MIRInt, GlobalAllocKind)
34-
[symbol(globalAllocEntry), group(mir)]
33+
syntax GlobalAlloc ::= globalAllocEntry(MIRInt, Ty, GlobalAllocKind)
34+
[symbol(globalAllocEntry), group(mir---alloc-id--ty--global-alloc)]
3535
3636
syntax GlobalAllocs ::= List {GlobalAlloc, ""}
3737
[symbol(GlobalAllocs::append), terminator-symbol(GlobalAllocs::empty), group(mir-list)]

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

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,10 @@
22
"name": "arithmetic_unchecked_runs",
33
"crate_id": 13794361957699792544,
44
"allocs": [
5-
[
6-
2,
7-
{
5+
{
6+
"alloc_id": 2,
7+
"ty": 24,
8+
"global_alloc": {
89
"Memory": {
910
"bytes": [
1011
117,
@@ -81,10 +82,11 @@
8182
"mutability": "Not"
8283
}
8384
}
84-
],
85-
[
86-
3,
87-
{
85+
},
86+
{
87+
"alloc_id": 3,
88+
"ty": 24,
89+
"global_alloc": {
8890
"Memory": {
8991
"bytes": [
9092
117,
@@ -161,7 +163,7 @@
161163
"mutability": "Not"
162164
}
163165
}
164-
]
166+
}
165167
],
166168
"functions": [
167169
[
@@ -237,7 +239,7 @@
237239
}
238240
],
239241
[
240-
38,
242+
40,
241243
{
242244
"NoOpSym": ""
243245
}
@@ -3642,7 +3644,7 @@
36423644
5,
36433645
{
36443646
"RefType": {
3645-
"pointee_type": 39,
3647+
"pointee_type": 38,
36463648
"layout": {
36473649
"fields": {
36483650
"Arbitrary": {
@@ -3707,7 +3709,7 @@
37073709
8,
37083710
{
37093711
"PtrType": {
3710-
"pointee_type": 40,
3712+
"pointee_type": 39,
37113713
"layout": {
37123714
"fields": "Primitive",
37133715
"variants": {
@@ -3749,7 +3751,7 @@
37493751
{
37503752
"EnumType": {
37513753
"name": "std::result::Result<isize, !>",
3752-
"adt_def": 22,
3754+
"adt_def": 23,
37533755
"discriminants": [
37543756
0,
37553757
1
@@ -3839,7 +3841,7 @@
38393841
{
38403842
"StructType": {
38413843
"name": "std::sys::pal::unix::process::process_common::ExitCode",
3842-
"adt_def": 13,
3844+
"adt_def": 14,
38433845
"fields": [
38443846
9
38453847
],
@@ -4320,7 +4322,7 @@
43204322
}
43214323
],
43224324
[
4323-
40,
4325+
39,
43244326
{
43254327
"PtrType": {
43264328
"pointee_type": 9,

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -71,13 +71,13 @@
7171
<types>
7272
ty ( 1 ) |-> typeInfoTupleType ( .Tys )
7373
ty ( 2 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI8 ) )
74-
ty ( 5 ) |-> typeInfoRefType ( ty ( 39 ) )
74+
ty ( 5 ) |-> typeInfoRefType ( ty ( 38 ) )
7575
ty ( 6 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyIsize ) )
76-
ty ( 8 ) |-> typeInfoPtrType ( ty ( 40 ) )
76+
ty ( 8 ) |-> typeInfoPtrType ( ty ( 39 ) )
7777
ty ( 9 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU8 ) )
78-
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 22 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
78+
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 23 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
7979
ty ( 11 ) |-> typeInfoRefType ( ty ( 12 ) )
80-
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 13 ) , ty ( 9 ) .Tys )
80+
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 14 ) , ty ( 9 ) .Tys )
8181
ty ( 16 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI32 ) )
8282
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 12 ) , ty ( 15 ) .Tys )
8383
ty ( 18 ) |-> typeInfoRefType ( ty ( 15 ) )
@@ -91,11 +91,11 @@
9191
ty ( 35 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI16 ) )
9292
ty ( 36 ) |-> typeInfoTupleType ( ty ( 35 ) ty ( 21 ) .Tys )
9393
ty ( 37 ) |-> typeInfoPrimitiveType ( primTypeStr )
94-
ty ( 40 ) |-> typeInfoPtrType ( ty ( 9 ) )
94+
ty ( 39 ) |-> typeInfoPtrType ( ty ( 9 ) )
9595
</types>
9696
<adt-to-ty>
9797
adtDef ( 12 ) |-> ty ( 17 )
98-
adtDef ( 13 ) |-> ty ( 15 )
99-
adtDef ( 22 ) |-> ty ( 10 )
98+
adtDef ( 14 ) |-> ty ( 15 )
99+
adtDef ( 23 ) |-> ty ( 10 )
100100
</adt-to-ty>
101101
</kmir>

‎kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.smir.json‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@
4646
}
4747
],
4848
[
49-
30,
49+
33,
5050
{
5151
"NoOpSym": ""
5252
}
@@ -2757,7 +2757,7 @@
27572757
5,
27582758
{
27592759
"RefType": {
2760-
"pointee_type": 31,
2760+
"pointee_type": 30,
27612761
"layout": {
27622762
"fields": {
27632763
"Arbitrary": {
@@ -2822,7 +2822,7 @@
28222822
8,
28232823
{
28242824
"PtrType": {
2825-
"pointee_type": 32,
2825+
"pointee_type": 31,
28262826
"layout": {
28272827
"fields": "Primitive",
28282828
"variants": {
@@ -2864,7 +2864,7 @@
28642864
{
28652865
"EnumType": {
28662866
"name": "std::result::Result<isize, !>",
2867-
"adt_def": 16,
2867+
"adt_def": 13,
28682868
"discriminants": [
28692869
0,
28702870
1
@@ -2874,7 +2874,7 @@
28742874
6
28752875
],
28762876
[
2877-
33
2877+
32
28782878
]
28792879
],
28802880
"layout": {
@@ -2954,7 +2954,7 @@
29542954
{
29552955
"StructType": {
29562956
"name": "std::sys::pal::unix::process::process_common::ExitCode",
2957-
"adt_def": 10,
2957+
"adt_def": 18,
29582958
"fields": [
29592959
9
29602960
],
@@ -3010,7 +3010,7 @@
30103010
{
30113011
"StructType": {
30123012
"name": "std::process::ExitCode",
3013-
"adt_def": 9,
3013+
"adt_def": 16,
30143014
"fields": [
30153015
15
30163016
],
@@ -3365,7 +3365,7 @@
33653365
}
33663366
],
33673367
[
3368-
32,
3368+
31,
33693369
{
33703370
"PtrType": {
33713371
"pointee_type": 9,
@@ -3398,7 +3398,7 @@
33983398
}
33993399
],
34003400
[
3401-
33,
3401+
32,
34023402
"VoidType"
34033403
]
34043404
],

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -80,15 +80,15 @@
8080
<types>
8181
ty ( 1 ) |-> typeInfoTupleType ( .Tys )
8282
ty ( 2 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI8 ) )
83-
ty ( 5 ) |-> typeInfoRefType ( ty ( 31 ) )
83+
ty ( 5 ) |-> typeInfoRefType ( ty ( 30 ) )
8484
ty ( 6 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyIsize ) )
85-
ty ( 8 ) |-> typeInfoPtrType ( ty ( 32 ) )
85+
ty ( 8 ) |-> typeInfoPtrType ( ty ( 31 ) )
8686
ty ( 9 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU8 ) )
87-
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 16 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
87+
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 13 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
8888
ty ( 11 ) |-> typeInfoRefType ( ty ( 12 ) )
89-
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 10 ) , ty ( 9 ) .Tys )
89+
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 18 ) , ty ( 9 ) .Tys )
9090
ty ( 16 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI32 ) )
91-
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 9 ) , ty ( 15 ) .Tys )
91+
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 16 ) , ty ( 15 ) .Tys )
9292
ty ( 18 ) |-> typeInfoRefType ( ty ( 15 ) )
9393
ty ( 22 ) |-> typeInfoPtrType ( ty ( 12 ) )
9494
ty ( 24 ) |-> typeInfoRefType ( ty ( 12 ) )
@@ -97,12 +97,12 @@
9797
ty ( 27 ) |-> typeInfoTupleType ( ty ( 9 ) ty ( 25 ) .Tys )
9898
ty ( 28 ) |-> typeInfoTupleType ( ty ( 2 ) ty ( 25 ) .Tys )
9999
ty ( 29 ) |-> typeInfoTupleType ( ty ( 26 ) ty ( 25 ) .Tys )
100-
ty ( 32 ) |-> typeInfoPtrType ( ty ( 9 ) )
101-
ty ( 33 ) |-> typeInfoVoidType
100+
ty ( 31 ) |-> typeInfoPtrType ( ty ( 9 ) )
101+
ty ( 32 ) |-> typeInfoVoidType
102102
</types>
103103
<adt-to-ty>
104-
adtDef ( 9 ) |-> ty ( 17 )
105-
adtDef ( 10 ) |-> ty ( 15 )
106-
adtDef ( 16 ) |-> ty ( 10 )
104+
adtDef ( 13 ) |-> ty ( 10 )
105+
adtDef ( 16 ) |-> ty ( 17 )
106+
adtDef ( 18 ) |-> ty ( 15 )
107107
</adt-to-ty>
108108
</kmir>

‎kmir/src/tests/integration/data/exec-smir/arithmetic/unary.smir.json‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2038,7 +2038,7 @@
20382038
{
20392039
"EnumType": {
20402040
"name": "std::result::Result<isize, !>",
2041-
"adt_def": 16,
2041+
"adt_def": 12,
20422042
"discriminants": [
20432043
0,
20442044
1
@@ -2128,7 +2128,7 @@
21282128
{
21292129
"StructType": {
21302130
"name": "std::sys::pal::unix::process::process_common::ExitCode",
2131-
"adt_def": 10,
2131+
"adt_def": 18,
21322132
"fields": [
21332133
9
21342134
],
@@ -2184,7 +2184,7 @@
21842184
{
21852185
"StructType": {
21862186
"name": "std::process::ExitCode",
2187-
"adt_def": 9,
2187+
"adt_def": 16,
21882188
"fields": [
21892189
15
21902190
],

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -58,11 +58,11 @@
5858
ty ( 6 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyIsize ) )
5959
ty ( 8 ) |-> typeInfoPtrType ( ty ( 28 ) )
6060
ty ( 9 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU8 ) )
61-
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 16 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
61+
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 12 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
6262
ty ( 11 ) |-> typeInfoRefType ( ty ( 12 ) )
63-
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 10 ) , ty ( 9 ) .Tys )
63+
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 18 ) , ty ( 9 ) .Tys )
6464
ty ( 16 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI32 ) )
65-
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 9 ) , ty ( 15 ) .Tys )
65+
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 16 ) , ty ( 15 ) .Tys )
6666
ty ( 18 ) |-> typeInfoRefType ( ty ( 15 ) )
6767
ty ( 22 ) |-> typeInfoPtrType ( ty ( 12 ) )
6868
ty ( 24 ) |-> typeInfoRefType ( ty ( 12 ) )
@@ -72,8 +72,8 @@
7272
ty ( 29 ) |-> typeInfoVoidType
7373
</types>
7474
<adt-to-ty>
75-
adtDef ( 9 ) |-> ty ( 17 )
76-
adtDef ( 10 ) |-> ty ( 15 )
77-
adtDef ( 16 ) |-> ty ( 10 )
75+
adtDef ( 12 ) |-> ty ( 10 )
76+
adtDef ( 16 ) |-> ty ( 17 )
77+
adtDef ( 18 ) |-> ty ( 15 )
7878
</adt-to-ty>
7979
</kmir>

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

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,10 @@
22
"name": "array_indexing",
33
"crate_id": 11673844854779303684,
44
"allocs": [
5-
[
6-
1,
7-
{
5+
{
6+
"alloc_id": 1,
7+
"ty": 28,
8+
"global_alloc": {
89
"Memory": {
910
"bytes": [
1011
97,
@@ -39,7 +40,7 @@
3940
"mutability": "Not"
4041
}
4142
}
42-
]
43+
}
4344
],
4445
"functions": [
4546
[
@@ -2221,7 +2222,7 @@
22212222
{
22222223
"EnumType": {
22232224
"name": "std::result::Result<isize, !>",
2224-
"adt_def": 17,
2225+
"adt_def": 22,
22252226
"discriminants": [
22262227
0,
22272228
1
@@ -2311,7 +2312,7 @@
23112312
{
23122313
"StructType": {
23132314
"name": "std::sys::pal::unix::process::process_common::ExitCode",
2314-
"adt_def": 11,
2315+
"adt_def": 9,
23152316
"fields": [
23162317
9
23172318
],
@@ -2367,7 +2368,7 @@
23672368
{
23682369
"StructType": {
23692370
"name": "std::process::ExitCode",
2370-
"adt_def": 10,
2371+
"adt_def": 7,
23712372
"fields": [
23722373
15
23732374
],
@@ -2696,7 +2697,7 @@
26962697
{
26972698
"StructType": {
26982699
"name": "std::panic::Location<'_>",
2699-
"adt_def": 8,
2700+
"adt_def": 13,
27002701
"fields": [
27012702
28,
27022703
35,

0 commit comments

Comments
 (0)