Previously, if any variable in scope had unusable BK, the usage checker would fail -- even if that variable was not needed in the check (because all BK was processed fully before the later lookup). So now it is done lazily -- BK is stored with possible errors, which are then ignored unless that BK is looked up and used.
This is two changes. The first drills down through the BK, adding everything relevant (this helps deal with abbreviations of replicators). The second is that checkPlainVarUsage now only checks non-array variables, and leaves all the array variables to checkArrayUsage, to prevent false alarms where array accesses with an abbreviation of a replicator were being handled by checkPlainVarUsage instead of checkArrayUsage. The only downside of all the changes is that multidimensional array accesses (they only worked with all constants before) are now no longer handled.
Previously, it was taking one lot of BK at a time, then checking to see if i and i' could overlap (i.e. i and i' were the array indexes to check), which of course they never could. It now takes a list of BK to pair up against each other, and asks if 0 can overlap with 0, which it can as long as there is a solution to the replicators.
This allows us to check situations like this:
PAR i = 0 FOR 10
IF
i = 0
a[10] := 3
TRUE
a[i] := 3
Previously this would have been flagged unsafe (because 10 can overlap with 10 between the replicated branches).
But with this change, the equations on the replicators (including: i'>=i+1, i = 0, i' = 0) are included alongside 10=10, so there is no solution over all because the replicator equations prevent a solution (i.e. the 10 can't be used twice in parallel).
Previously, constraints on a replicator from BK (such as i >= 3) were not being mirrored to the other copy of the replicator (so the constraint i' >= 3 was not added, which was causing problems)
This expansion was causing a big blow-up in the code, as things like:
VAL [2][1]INT as IS [[0,1]]
were getting transformed into:
VAL [2]INT n0 IS [0,1]:
VAL [2]INT n1 IS [0,1]:
VAL [2]INT n2 IS [n0[0], n1[1]]:
VAL [2][1]INT as IS [n2]:
Or something similar -- the inner arrays were pulled up into multiple definitions that were then subscripted, because the first pull-up did this:
VAL [2]INT n2 IS [[0,1][0], [0,1][1]]:
and then the inner arrays got pulled up again, separately. The change hasn't immediately broken anything, but I haven't fully tested it yet
