@@ -164,7 +164,8 @@ type factsTable struct {
164
164
// order is a couple of partial order sets that record information
165
165
// about relations between SSA values in the signed and unsigned
166
166
// domain.
167
- order [2 ]* poset
167
+ orderS * poset
168
+ orderU * poset
168
169
169
170
// known lower and upper bounds on individual values.
170
171
limits map [ID ]limit
@@ -187,10 +188,10 @@ var checkpointBound = limitFact{}
187
188
188
189
func newFactsTable (f * Func ) * factsTable {
189
190
ft := & factsTable {}
190
- ft .order [ 0 ] = f .newPoset () // signed
191
- ft .order [ 1 ] = f .newPoset () // unsigned
192
- ft .order [ 0 ] .SetUnsigned (false )
193
- ft .order [ 1 ] .SetUnsigned (true )
191
+ ft .orderS = f .newPoset ()
192
+ ft .orderU = f .newPoset ()
193
+ ft .orderS .SetUnsigned (false )
194
+ ft .orderU .SetUnsigned (true )
194
195
ft .facts = make (map [pair ]relation )
195
196
ft .stack = make ([]fact , 4 )
196
197
ft .limits = make (map [ID ]limit )
@@ -221,23 +222,23 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
221
222
222
223
if d == signed || d == unsigned {
223
224
var ok bool
224
- idx := 0
225
+ order := ft . orderS
225
226
if d == unsigned {
226
- idx = 1
227
+ order = ft . orderU
227
228
}
228
229
switch r {
229
230
case lt :
230
- ok = ft . order [ idx ] .SetOrder (v , w )
231
+ ok = order .SetOrder (v , w )
231
232
case gt :
232
- ok = ft . order [ idx ] .SetOrder (w , v )
233
+ ok = order .SetOrder (w , v )
233
234
case lt | eq :
234
- ok = ft . order [ idx ] .SetOrderOrEqual (v , w )
235
+ ok = order .SetOrderOrEqual (v , w )
235
236
case gt | eq :
236
- ok = ft . order [ idx ] .SetOrderOrEqual (w , v )
237
+ ok = order .SetOrderOrEqual (w , v )
237
238
case eq :
238
- ok = ft . order [ idx ] .SetEqual (v , w )
239
+ ok = order .SetEqual (v , w )
239
240
case lt | gt :
240
- ok = ft . order [ idx ] .SetNonEqual (v , w )
241
+ ok = order .SetNonEqual (v , w )
241
242
default :
242
243
panic ("unknown relation" )
243
244
}
@@ -588,6 +589,7 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
588
589
}
589
590
590
591
// Check if the recorded limits can prove that the value is positive
592
+
591
593
if l , has := ft .limits [v .ID ]; has && (l .min >= 0 || l .umax <= uint64 (max )) {
592
594
return true
593
595
}
@@ -610,7 +612,7 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
610
612
}
611
613
612
614
// Check if the signed poset can prove that the value is >= 0
613
- return ft .order [ 0 ] .OrderedOrEqual (ft .zero , v )
615
+ return ft .orderS .OrderedOrEqual (ft .zero , v )
614
616
}
615
617
616
618
// checkpoint saves the current state of known relations.
@@ -621,8 +623,8 @@ func (ft *factsTable) checkpoint() {
621
623
}
622
624
ft .stack = append (ft .stack , checkpointFact )
623
625
ft .limitStack = append (ft .limitStack , checkpointBound )
624
- ft .order [ 0 ] .Checkpoint ()
625
- ft .order [ 1 ] .Checkpoint ()
626
+ ft .orderS .Checkpoint ()
627
+ ft .orderU .Checkpoint ()
626
628
}
627
629
628
630
// restore restores known relation to the state just
@@ -658,8 +660,8 @@ func (ft *factsTable) restore() {
658
660
ft .limits [old .vid ] = old .limit
659
661
}
660
662
}
661
- ft .order [ 0 ] .Undo ()
662
- ft .order [ 1 ] .Undo ()
663
+ ft .orderS .Undo ()
664
+ ft .orderU .Undo ()
663
665
}
664
666
665
667
func lessByID (v , w * Value ) bool {
@@ -922,7 +924,7 @@ func prove(f *Func) {
922
924
ft .restore ()
923
925
924
926
// Return the posets to the free list
925
- for _ , po := range ft .order {
927
+ for _ , po := range [] * poset { ft .orderS , ft . orderU } {
926
928
// Make sure it's empty as it should be. A non-empty poset
927
929
// might cause errors and miscompilations if reused.
928
930
if checkEnabled {
0 commit comments