/
stuck.go
127 lines (119 loc) · 4.61 KB
/
stuck.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
// File generated by the K Framework Go backend. Timestamp: 2019-08-13 18:16:45.638
package ieletestinginterpreter
import (
m "github.com/ElrondNetwork/elrond-vm/iele/original/node/iele-testing-kompiled/ieletestingmodel"
)
func (i *Interpreter) makeStuck(c m.KReference, config m.KReference) (m.KReference, error) {
var v [makeStuckFuncNrVars]KReference
var bv [makeStuckFuncNrBoolVars]bool
matched := false
// all rules: -1
if c&kapplyMatchMask == kapplyMatchLblXltgeneratedTopXgt9 { // `<generatedTop>`(_0,`<s>`(DotVar1),_1,_2,_3,_4,_5,_6,_7)
v[0] = i.Model.KApplyArg(c, 0)
v[1 /*_0*/] = v[0] // lhs KVariable _0
v[2] = i.Model.KApplyArg(c, 1)
if v[2]&kapplyMatchMask == kapplyMatchLblXltsXgt1 { // `<s>`(DotVar1)
v[3] = i.Model.KApplyArg(v[2], 0)
// KSequence, size 1:DotVar1
v[4 /*DotVar1*/] = v[3] // lhs KVariable DotVar1
v[5] = i.Model.KApplyArg(c, 2)
v[6 /*_1*/] = v[5] // lhs KVariable _1
v[7] = i.Model.KApplyArg(c, 3)
v[8 /*_2*/] = v[7] // lhs KVariable _2
v[9] = i.Model.KApplyArg(c, 4)
v[10 /*_3*/] = v[9] // lhs KVariable _3
v[11] = i.Model.KApplyArg(c, 5)
v[12 /*_4*/] = v[11] // lhs KVariable _4
v[13] = i.Model.KApplyArg(c, 6)
v[14 /*_5*/] = v[13] // lhs KVariable _5
v[15] = i.Model.KApplyArg(c, 7)
v[16 /*_6*/] = v[15] // lhs KVariable _6
v[17] = i.Model.KApplyArg(c, 8)
v[18 /*_7*/] = v[17] // lhs KVariable _7
// rule #-1
// source: ? @?
// {| rule `<generatedTop>`(_0,`<s>`(``.K=>#STUCK(.KList)``~>DotVar1),_1,_2,_3,_4,_5,_6,_7) requires #token("true","Bool") ensures #token("true","Bool") [] |}
if !matched {
// RHS
i.traceRuleApply("STEP", -1, "{| rule `<generatedTop>`(_0,`<s>`(``.K=>#STUCK(.KList)``~>DotVar1),_1,_2,_3,_4,_5,_6,_7) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [] |}")
return i.Model.NewKApply(m.LblXltgeneratedTopXgt, // as-is <generatedTop>
v[1 /*_0*/],
i.Model.NewKApply(m.LblXltsXgt, // as-is <s>
i.Model.AssembleKSequence(
i.Model.NewKApply(m.LblXhashSTUCK, // as-is #STUCK
),
v[4 /*DotVar1*/],
),
),
v[6 /*_1*/],
v[8 /*_2*/],
v[10 /*_3*/],
v[12 /*_4*/],
v[14 /*_5*/],
v[16 /*_6*/],
v[18 /*_7*/],
), nil
}
}
}
doNothingWithVars(len(v), len(bv))
return c, nil
}
func (i *Interpreter) makeUnstuck(c m.KReference, config m.KReference) (m.KReference, error) {
var v [makeStuckFuncNrVars]KReference
var bv [makeStuckFuncNrBoolVars]bool
matched := false
// all rules: -1
if c&kapplyMatchMask == kapplyMatchLblXltgeneratedTopXgt9 { // `<generatedTop>`(_0,`<s>`(#STUCK(.KList)~>DotVar1),_1,_2,_3,_4,_5,_6,_7)
v[0] = i.Model.KApplyArg(c, 0)
v[1 /*_0*/] = v[0] // lhs KVariable _0
v[2] = i.Model.KApplyArg(c, 1)
if v[2]&kapplyMatchMask == kapplyMatchLblXltsXgt1 { // `<s>`(#STUCK(.KList)~>DotVar1)
v[3] = i.Model.KApplyArg(v[2], 0)
if v[3]>>refTypeShift != refEmptyKseqTypeAsUint { // #STUCK(.KList)~>DotVar1
_, v[4], v[5] = i.Model.KSequenceSplitHeadTail(v[3]) // #STUCK(.KList) ~> ...
if v[4]&kapplyMatchMask == kapplyMatchLblXhashSTUCK0 { // #STUCK(.KList)
v[6 /*DotVar1*/] = v[5] // lhs KVariable DotVar1
v[7] = i.Model.KApplyArg(c, 2)
v[8 /*_1*/] = v[7] // lhs KVariable _1
v[9] = i.Model.KApplyArg(c, 3)
v[10 /*_2*/] = v[9] // lhs KVariable _2
v[11] = i.Model.KApplyArg(c, 4)
v[12 /*_3*/] = v[11] // lhs KVariable _3
v[13] = i.Model.KApplyArg(c, 5)
v[14 /*_4*/] = v[13] // lhs KVariable _4
v[15] = i.Model.KApplyArg(c, 6)
v[16 /*_5*/] = v[15] // lhs KVariable _5
v[17] = i.Model.KApplyArg(c, 7)
v[18 /*_6*/] = v[17] // lhs KVariable _6
v[19] = i.Model.KApplyArg(c, 8)
v[20 /*_7*/] = v[19] // lhs KVariable _7
// rule #-1
// source: ? @?
// {| rule `<generatedTop>`(_0,`<s>`(``#STUCK(.KList)=>.K``~>DotVar1),_1,_2,_3,_4,_5,_6,_7) requires #token("true","Bool") ensures #token("true","Bool") [] |}
if !matched {
// RHS
i.traceRuleApply("STEP", -1, "{| rule `<generatedTop>`(_0,`<s>`(``#STUCK(.KList)=>.K``~>DotVar1),_1,_2,_3,_4,_5,_6,_7) requires #token(\"true\",\"Bool\") ensures #token(\"true\",\"Bool\") [] |}")
return i.Model.NewKApply(m.LblXltgeneratedTopXgt, // as-is <generatedTop>
v[1 /*_0*/],
i.Model.NewKApply(m.LblXltsXgt, // as-is <s>/* rhs KSequence size=1 */
v[6 /*DotVar1*/],
),
v[8 /*_1*/],
v[10 /*_2*/],
v[12 /*_3*/],
v[14 /*_4*/],
v[16 /*_5*/],
v[18 /*_6*/],
v[20 /*_7*/],
), nil
}
}
}
}
}
doNothingWithVars(len(v), len(bv))
return c, nil
}
const makeStuckFuncNrVars = 21
const makeStuckFuncNrBoolVars = 0