made disjoint checker smarter; fixes regressions
This commit is contained in:
parent
ac3cc140f5
commit
90d1ad4231
3 changed files with 43 additions and 14 deletions
|
|
@ -156,19 +156,23 @@ proc addSlice(c: var AnalysisCtx; n: PNode; x, le, ri: PNode) =
|
|||
|
||||
proc overlap(m: TModel; x,y,c,d: PNode) =
|
||||
# X..Y and C..D overlap iff (X <= D and C <= Y)
|
||||
case proveLe(m, x, d)
|
||||
case proveLe(m, c, y)
|
||||
of impUnknown:
|
||||
localError(x.info,
|
||||
"cannot prove: $# > $#; required for ($#)..($#) disjoint from ($#)..($#)" %
|
||||
[?x, ?d, ?x, ?y, ?c, ?d])
|
||||
case proveLe(m, x, d)
|
||||
of impNo: discard
|
||||
of impUnknown, impYes:
|
||||
localError(x.info,
|
||||
"cannot prove: $# > $#; required for ($#)..($#) disjoint from ($#)..($#)" %
|
||||
[?c, ?y, ?x, ?y, ?c, ?d])
|
||||
of impYes:
|
||||
case proveLe(m, c, y)
|
||||
case proveLe(m, x, d)
|
||||
of impUnknown:
|
||||
localError(x.info,
|
||||
"cannot prove: $# > $#; required for ($#)..($#) disjoint from ($#)..($#)" %
|
||||
[?c, ?y, ?x, ?y, ?c, ?d])
|
||||
[?x, ?d, ?x, ?y, ?c, ?d])
|
||||
of impYes:
|
||||
localError(x.info, "($#)..($#) not disjoint from ($#)..($#)" % [?x, ?y, ?c, ?d])
|
||||
localError(x.info, "($#)..($#) not disjoint from ($#)..($#)" %
|
||||
[?c, ?y, ?x, ?y, ?c, ?d])
|
||||
of impNo: discard
|
||||
of impNo: discard
|
||||
|
||||
|
|
@ -278,10 +282,12 @@ proc analyseCall(c: var AnalysisCtx; n: PNode; op: PSym) =
|
|||
slot.stride = min(slot.stride, incr)
|
||||
analyseSons(c, n)
|
||||
elif op.name.s == "[]" and op.fromSystem:
|
||||
c.addSlice(n, n[1], n[2][1], n[2][2])
|
||||
let slice = n[2].skipStmtList
|
||||
c.addSlice(n, n[1], slice[1], slice[2])
|
||||
analyseSons(c, n)
|
||||
elif op.name.s == "[]=" and op.fromSystem:
|
||||
c.addSlice(n, n[1], n[2][1], n[2][2])
|
||||
let slice = n[2].skipStmtList
|
||||
c.addSlice(n, n[1], slice[1], slice[2])
|
||||
analyseSons(c, n)
|
||||
else:
|
||||
analyseSons(c, n)
|
||||
|
|
@ -395,8 +401,9 @@ proc transformSlices(n: PNode): PNode =
|
|||
result = copyNode(n)
|
||||
result.add opSlice.newSymNode
|
||||
result.add n[1]
|
||||
result.add n[2][1]
|
||||
result.add n[2][2]
|
||||
let slice = n[2].skipStmtList
|
||||
result.add slice[1]
|
||||
result.add slice[2]
|
||||
return result
|
||||
if n.safeLen > 0:
|
||||
result = shallowCopy(n)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue