test(kmir): refresh proof and execution snapshots

Author: Stevengre

kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state

@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #setArgFromStack ( 1 , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) ) ~> #setArgsFromStack ( 2 , operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x0b\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) )  .Operands ) ~> #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K
+    #setLocalValue ( place (... local: local ( 1 ) , projection: .ProjectionElems ) , Integer ( 10 , 64 , false ) ) ~> #setArgsFromStack ( 2 , operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x0b\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 2 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) )  .Operands ) ~> #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K
   </k>
   <retVal>
     noReturn

kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state

@@ -1,8 +1,6 @@
 <kmir>
   <k>
-    #traverseProjection ( toSlot ( 1 ) , thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 32 , true ) )
-    ListItem ( BoolVal ( false ) )
-    ListItem ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) ) , 2 , ty ( 27 ) )  .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 25 ) , id: mirConstId ( 9 ) ) ) ) , args: operandMove ( place (... local: local ( 5 ) , projection: .ProjectionElems ) )  operandMove ( place (... local: local ( 6 ) , projection: .ProjectionElems ) )  operandMove ( place (... local: local ( 7 ) , projection: .ProjectionElems ) )  .Operands , destination: place (... local: local ( 4 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 51 ) ) ) ~> .K
+    #execTerminatorCall ( ty ( 25 ) , monoItemFn (... name: symbol ( "foo" ) , id: defId ( 8 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 74 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 16 ) , span: span ( 75 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 26 ) , span: span ( 76 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 27 ) , span: span ( 77 ) , mut: mutabilityNot )  .LocalDecls , argCount: 3 , varDebugInfo: varDebugInfo (... name: symbol ( "_i" ) , sourceInfo: sourceInfo (... span: span ( 75 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "_b" ) , sourceInfo: sourceInfo (... span: span ( 76 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 2 ) )  varDebugInfo (... name: symbol ( "_f" ) , sourceInfo: sourceInfo (... span: span ( 77 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 3 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 78 ) ) ) ) , operandMove ( place (... local: local ( 5 ) , projection: .ProjectionElems ) )  operandMove ( place (... local: local ( 6 ) , projection: .ProjectionElems ) )  operandMove ( place (... local: local ( 7 ) , projection: .ProjectionElems ) )  .Operands , place (... local: local ( 4 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , span ( 51 ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -58,7 +56,7 @@
     4 |-> newLocal ( ty ( 1 ) , mutabilityNot )
     5 |-> typedValue ( Integer ( 10 , 32 , true ) , ty ( 16 ) , mutabilityMut )
     6 |-> typedValue ( BoolVal ( false ) , ty ( 26 ) , mutabilityMut )
-    7 |-> newLocal ( ty ( 27 ) , mutabilityMut )
+    7 |-> typedValue ( thunk ( UnableToDecode ( b"\x00\x00\x00\x00\x00\x00$@" , typeInfoPrimitiveType ( primTypeFloat ( floatTyF64 ) ) ) ) , ty ( 27 ) , mutabilityMut )
     8 |-> newLocal ( ty ( 1 ) , mutabilityNot )
     9 |-> newLocal ( ty ( 16 ) , mutabilityMut )
     10 |-> newLocal ( ty ( 26 ) , mutabilityMut )

kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (148 steps)
+│  (163 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (61 steps)
+│  (67 steps)
 └─ 3 (stuck, leaf)
     #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
     span: 32

kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (837 steps)
+│  (928 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (73 steps)
+│  (107 steps)
 ├─ 3
 │   #cast ( Integer ( 4 , 64 , false ) , castKindTransmute , ty ( 29 ) , ty ( 50 ) )
 │   span: 186

kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected

@@ -3,8 +3,104 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (1045 steps)
-└─ 3 (stuck, leaf)
+│  (50 steps)
+├─ 3
+│   rvalueAggregate ( aggregateKindAdt ( adtDef ( 17 ) , variantIdx ( 0 ) , genericA
+│   span: 32
+│
+│  (50 steps)
+├─ 4
+│   Aggregate ( variantIdx ( 0 ) , ListItem ( Aggregate ( variantIdx ( 0 ) , ListIte
+│   span: 263
+│
+│  (50 steps)
+├─ 5
+│   #reserveSlots ( localDecl ( ... ty: ty ( 47 ) , span: span ( 68 ) , mut: mutabil
+│   span: 68
+│
+│  (50 steps)
+├─ 6
+│   #traverseProjection ( toSlot ( 29 ) , Reference ( slotPlace ( 2 , projectionElem
+│   span: 159
+│
+│  (50 steps)
+├─ 7
+│   #cast ( PtrLocal ( slotPlace ( 2 , projectionElemField ( fieldIdx ( 0 ) , ty ( 6
+│   span: 86
+│
+│  (50 steps)
+├─ 8
+│   #setLocalValue ( place ( ... local: local ( 16 ) , projection: .ProjectionElems
+│   span: 102
+│
+│  (50 steps)
+├─ 9
+│   #decodeConstant ( constantKindAllocated ( allocation ( ... bytes: b"\xff\xff\xff
+│   span: 100
+│
+│  (50 steps)
+├─ 10
+│   #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l
+│   span: 168
+│
+│  (50 steps)
+├─ 11
+│   #execStmts ( statement ( ... kind: statementKindStorageDead ( local ( 7 ) ) , sp
+│   span: 171
+│
+│  (50 steps)
+├─ 12
+│   #execStmt ( statement ( ... kind: statementKindStorageDead ( local ( 22 ) ) , sp
+│   span: 172
+│
+│  (50 steps)
+├─ 13
+│   #execTerminator ( terminator ( ... kind: terminatorKindReturn , span: span ( 160
+│   span: 160
+│
+│  (50 steps)
+├─ 14
+│   rvalueRef ( region ( ... kind: regionKindReErased ) , borrowKindMut ( ... kind:
+│   span: 271
+│
+│  (50 steps)
+├─ 15
+│   #execStmt ( statement ( ... kind: statementKindStorageLive ( local ( 5 ) ) , spa
+│   span: 237
+│
+│  (50 steps)
+├─ 16
+│   #execStmts ( statement ( ... kind: statementKindAssign ( ... place: place ( ...
+│   span: 272
+│
+│  (50 steps)
+├─ 17
+│   #execStmts ( .Statements )
+~> #execTerminator ( terminator ( ... kind: terminato
+│   span: 274
+│
+│  (50 steps)
+├─ 18
+│   #reserveSlots ( localDecl ( ... ty: ty ( 46 ) , span: span ( 76 ) , mut: mutabil
+│   span: 76
+│
+│  (50 steps)
+├─ 19
+│   rvalueRef ( region ( ... kind: regionKindReErased ) , borrowKindShared , place (
+│   span: 159
+│
+│  (50 steps)
+├─ 20
+│   PtrLocal ( slotPlace ( 2 , projectionElemField ( fieldIdx ( 0 ) , ty ( 68 ) )  p
+│   span: 86
+│
+│  (50 steps)
+├─ 21
+│   #execTerminator ( terminator ( ... kind: terminatorKindGoto ( ... target: basicB
+│   span: 162
+│
+│  (37 steps)
+└─ 22 (stuck, leaf)
     #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core4cell22panic_already
     span: 32
 

kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected

@@ -3,8 +3,226 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (2330 steps)
-├─ 3 (terminal)
+│  (50 steps)
+├─ 3
+│   rvalueAggregate ( aggregateKindArray ( ty ( 31 ) ) , operandMove ( place ( ... l
+│   function: main
+│   span: 199
+│
+│  (50 steps)
+├─ 4
+│   #setLocalValue ( place ( ... local: local ( 7 ) , projection: .ProjectionElems )
+│   function: main
+│   span: 190
+│
+│  (50 steps)
+├─ 5
+│   #setLocalValue ( place ( ... local: local ( 4 ) , projection: .ProjectionElems )
+│   span: 176
+│
+│  (50 steps)
+├─ 6
+│   rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p
+│   span: 55
+│
+│  (50 steps)
+├─ 7
+│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
+│
+│  (50 steps)
+├─ 8
+│   #execStmts ( .Statements )
+~> #execTerminator ( terminator ( ... kind: terminato
+│   span: 60
+│
+│  (50 steps)
+├─ 9
+│   #dropSlots ( ListItem ( 25 ) ListItem ( 26 ) )
+~> #execBlockIdx ( basicBlockIdx
+│
+│  (50 steps)
+├─ 10
+│   #mkRef ( toSlot ( 15 ) , .ProjectionElems , mutabilityMut , metadata ( noMetadat
+│   span: 179
+│
+│  (50 steps)
+├─ 11
+│   #execBlockIdx ( basicBlockIdx ( 2 ) ) ~> .K
+│
+│  (50 steps)
+├─ 12
+│   #traverseProjection ( toSlot ( 41 ) , Reference ( slotPlace ( 15 , .ProjectionEl
+│   span: 110
+│
+│  (50 steps)
+├─ 13
+│   #traverseProjection ( toSlot ( 45 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+│   span: 115
+│
+│  (50 steps)
+├─ 14
+│   #setLocalValue ( place ( ... local: local ( 15 ) , projection: .ProjectionElems
+│   span: 119
+│
+│  (50 steps)
+├─ 15
+│   #execStmts ( statement ( ... kind: statementKindAssign ( ... place: place ( ...
+│   span: 144
+│
+│  (50 steps)
+├─ 16
+│   #traverseProjection ( toSlot ( 64 ) , PtrLocal ( slotPlace ( 2 , projectionElemF
+│   span: 149
+│
+│  (50 steps)
+├─ 17
+│   #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l
+│   span: 113
+│
+│  (50 steps)
+├─ 18
+│   Aggregate ( variantIdx ( 1 ) , ListItem ( Reference ( slotPlace ( 2 , projection
+│   span: 117
+│
+│  (50 steps)
+├─ 19
+│   rvalueUse ( operandConstant ( constOperand ( ... span: span ( 183 ) , userTy: no
+│   span: 183
+│
+│  (50 steps)
+├─ 20
+│   Integer ( 1 , 8 , false )
+~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Eva
+│   span: 185
+│
+│  (50 steps)
+├─ 21
+│   #reserveSlots ( localDecl ( ... ty: ty ( 30 ) , span: span ( 145 ) , mut: mutabi
+│   span: 145
+│
+│  (50 steps)
+├─ 22
+│   #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l
+│   span: 107
+│
+│  (50 steps)
+├─ 23
+│   #traverseProjection ( toSlot ( 15 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+│   span: 113
+│
+│  (50 steps)
+├─ 24
+│   #execStmts ( .Statements )
+~> #execTerminator ( terminator ( ... kind: terminato
+│   span: 97
+│
+│  (50 steps)
+├─ 25
+│   PtrLocal ( slotPlace ( 15 , projectionElemField ( fieldIdx ( 1 ) , ty ( 30 ) )
+│   span: 134
+│
+│  (50 steps)
+├─ 26
+│   #traverseProjection ( toSlot ( 93 ) , PtrLocal ( slotPlace ( 2 , projectionElemF
+│   span: 32
+│
+│  (50 steps)
+├─ 27
+│   #execStmts ( .Statements )
+~> #execTerminator ( terminator ( ... kind: terminato
+│   span: 132
+│
+│  (50 steps)
+├─ 28
+│   Reference ( slotPlace ( 2 , projectionElemField ( fieldIdx ( 1 ) , ty ( 48 ) )
+│   span: 126
+│
+│  (50 steps)
+├─ 29
+│   #setSlotValue ( 18 , Moved )
+~> Integer ( 1 , 0 , false )
+~> #freezer#selectBloc
+│
+│  (50 steps)
+├─ 30
+│   operandMove ( place ( ... local: local ( 14 ) , projection: .ProjectionElems ) )
+│
+│  (50 steps)
+├─ 31
+│   #reserveSlots ( localDecl ( ... ty: ty ( 35 ) , span: span ( 156 ) , mut: mutabi
+│   span: 156
+│
+│  (50 steps)
+├─ 32
+│   #traverseProjection ( toSlot ( 15 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+│   span: 105
+│
+│  (50 steps)
+├─ 33
+│   rvalueRef ( region ( ... kind: regionKindReErased ) , borrowKindShared , place (
+│   span: 111
+│
+│  (50 steps)
+├─ 34
+│   #applyBinOp ( binOpEq , PtrLocal ( slotPlace ( 2 , projectionElemField ( fieldId
+│   span: 111
+│
+│  (50 steps)
+├─ 35
+│   operandConstant ( constOperand ( ... span: span ( 119 ) , userTy: noUserTypeAnno
+│   span: 119
+│
+│  (50 steps)
+├─ 36
+│   #execStmt ( statement ( ... kind: statementKindStorageLive ( local ( 24 ) ) , sp
+│   span: 145
+│
+│  (50 steps)
+├─ 37
+│   #execStmts ( statement ( ... kind: statementKindAssign ( ... place: place ( ...
+│   span: 151
+│
+│  (50 steps)
+├─ 38
+│   #cast ( operandCopy ( place ( ... local: local ( 27 ) , projection: .ProjectionE
+│   span: 128
+│
+│  (50 steps)
+├─ 39
+│   #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
+│
+│  (50 steps)
+├─ 40
+│   #setLocalValue ( place ( ... local: local ( 13 ) , projection: .ProjectionElems
+│   span: 181
+│
+│  (50 steps)
+├─ 41
+│   #execBlockIdx ( basicBlockIdx ( 3 ) ) ~> .K
+│
+│  (50 steps)
+├─ 42
+│   #execStmts ( .Statements )
+~> #execTerminator ( terminator ( ... kind: terminato
+│   span: 96
+│
+│  (50 steps)
+├─ 43
+│   #execStmt ( statement ( ... kind: statementKindStorageDead ( local ( 6 ) ) , spa
+│   span: 108
+│
+│  (50 steps)
+├─ 44
+│   #execStmts ( statement ( ... kind: statementKindStorageDead ( local ( 11 ) ) , s
+│   span: 114
+│
+│  (50 steps)
+├─ 45
+│   #execStmts ( statement ( ... kind: statementKindAssign ( ... place: place ( ...
+│   span: 32
+│
+│  (49 steps)
+├─ 46 (terminal)
 │   #EndProgram ~> .K
 │   function: main
 │