made disjoint checker smarter; fixes regressions

3 files changed, 43 insertions, 14 deletions

diff --git a/compiler/ast.nim b/compiler/ast.nim
index 08a991468..4001e896e 100644
--- a/compiler/ast.nim
+++ b/compiler/ast.nim
@@ -1588,6 +1588,14 @@ proc makeStmtList*(n: PNode): PNode =
     result = newNodeI(nkStmtList, n.info)
     result.add n
 
+proc skipStmtList*(n: PNode): PNode =
+  if n.kind in {nkStmtList, nkStmtListExpr}:
+    for i in 0 .. n.len-2:
+      if n[i].kind notin {nkEmpty, nkCommentStmt}: return n
+    result = n.lastSon
+  else:
+    result = n
+
 proc createMagic*(name: string, m: TMagic): PSym =
   result = newSym(skProc, getIdent(name), nil, unknownLineInfo())
   result.magic = m
diff --git a/compiler/guards.nim b/compiler/guards.nim
index bc802ae33..eeadcb6c7 100644
--- a/compiler/guards.nim
+++ b/compiler/guards.nim
@@ -37,6 +37,7 @@ const
   someMod = {mModI}
   someMax = {mMaxI, mMaxF64}
   someMin = {mMinI, mMinF64}
+  someBinaryOp = someAdd+someSub+someMul+someDiv+someMod+someMax+someMin
 
 proc isValue(n: PNode): bool = n.kind in {nkCharLit..nkNilLit}
 proc isLocation(n: PNode): bool = not n.isValue
@@ -721,6 +722,7 @@ proc ple(m: TModel; a, b: PNode): TImplication =
     if a.intVal <= 0: return impYes
 
   #   x <= y+c  if 0 <= c and x <= y
+  #   x <= y+(-c)  if c <= 0  and y >= x
   if b.getMagic in someAdd and zero() <=? b[2] and a <=? b[1]: return impYes
 
   #   x+c <= y  if c <= 0 and x <= y
@@ -730,6 +732,10 @@ proc ple(m: TModel; a, b: PNode): TImplication =
   if b.getMagic in someMul:
     if a <=? b[1] and one() <=? b[2] and zero() <=? b[1]: return impYes
 
+  #  x+c <= x+d  if c <= d. Same for *, div etc.
+  if a.getMagic in someBinaryOp and a.getMagic == b.getMagic:
+    if sameTree(a[1], b[1]) and a[2] <=? b[2]: return impYes
+
   #   x div c <= y   if   1 <= c  and  0 <= y  and x <= y:
   if a.getMagic in someDiv:
     if one() <=? a[2] and zero() <=? b and a[1] <=? b: return impYes
@@ -769,11 +775,19 @@ proc pleViaModelRec(m: var TModel; a, b: PNode): TImplication =
   for i in 0..m.high:
     let fact = m[i]
     if fact != nil and fact.getMagic in someLe:
-      # x <= y implies a <= b  if  a <= x and y <= b
-      let x = fact[1]
-      let y = fact[2]
       # mark as used:
       m[i] = nil
+      # i <= len-100
+      # i <=? len-1
+      # --> true  if  (len-100) <= (len-1)
+      let x = fact[1]
+      let y = fact[2]
+      if sameTree(x, a) and y.getMagic in someAdd and b.getMagic in someAdd and
+         sameTree(y[1], b[1]):
+        if ple(m, b[2], y[2]) == impYes:
+          return impYes
+
+      # x <= y implies a <= b  if  a <= x and y <= b
       if ple(m, a, x) == impYes:
         if ple(m, y, b) == impYes:
           return impYes
diff --git a/compiler/semparallel.nim b/compiler/semparallel.nim
index 36c63d038..c1609a169 100644
--- a/compiler/semparallel.nim
+++ b/compiler/semparallel.nim
@@ -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)