next steps for guarded data flow analysis

1 files changed, 220 insertions, 35 deletions

diff --git a/compiler/guards.nim b/compiler/guards.nim
index 6d0bf6bc6..e9c9f9ac1 100644
--- a/compiler/guards.nim
+++ b/compiler/guards.nim
@@ -27,23 +27,53 @@ const
 
 proc isValue(n: PNode): bool = n.kind in {nkCharLit..nkNilLit}
 proc isLocation(n: PNode): bool = not n.isValue
-#n.kind in {nkSym, nkBracketExpr, nkDerefExpr, nkHiddenDeref, nkDotExpr}
 
 proc isLet(n: PNode): bool =
   if n.kind == nkSym:
-    # XXX allow skResult, skVar here if not re-bound
     if n.sym.kind in {skLet, skTemp, skForVar}:
       result = true
     elif n.sym.kind == skParam and skipTypes(n.sym.typ, 
                                              abstractInst).kind != tyVar:
       result = true
 
-proc isLetLocation(m: PNode): bool =
+proc isVar(n: PNode): bool =
+  n.kind == nkSym and n.sym.kind in {skResult, skVar} and
+      sfGlobal notin n.sym.flags
+
+proc isLetLocation(m: PNode, isApprox: bool): bool =
+  # consider: 'n[].kind' --> we really need to support 1 deref op even if this
+  # is technically wrong due to aliasing :-( We could introduce "soft" facts
+  # for this; this would still be very useful for warnings and also nicely
+  # solves the 'var' problems. For now we fix this by requiring much more
+  # restrictive expressions for the 'not nil' checking.
   var n = m
+  var derefs = 0
   while true:
     case n.kind
     of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv:
       n = n.sons[0]
+    of nkDerefExpr, nkHiddenDeref:
+      n = n.sons[0]
+      inc derefs
+    of nkBracketExpr:
+      if isConstExpr(n.sons[1]) or isLet(n.sons[1]):
+        n = n.sons[0]
+      else: return
+    of nkHiddenStdConv, nkHiddenSubConv, nkConv:
+      n = n.sons[1]
+    else:
+      break
+  result = n.isLet and derefs <= ord(isApprox)
+  if not result and isApprox:
+    result = isVar(n)
+
+proc interestingCaseExpr*(m: PNode): bool = 
+  var n = m
+  while true:
+    case n.kind
+    of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv, 
+       nkDerefExpr, nkHiddenDeref:
+      n = n.sons[0]
     of nkBracketExpr:
       if isConstExpr(n.sons[1]) or isLet(n.sons[1]):
         n = n.sons[0]
@@ -62,14 +92,30 @@ proc neg(n: PNode): PNode =
     result.sons[0] = newSymNode(getSysMagic("not", mNot))
     result.sons[1] = n
 
+proc buildIsNil(arg: PNode): PNode =
+  result = newNodeI(nkCall, arg.info, 2)
+  result.sons[0] = newSymNode(getSysMagic("isNil", mIsNil))
+  result.sons[1] = arg
+
 proc usefulFact(n: PNode): PNode =
   case n.getMagic
-  of someEq+someLe+someLt:
-    if isLetLocation(n.sons[1]) or n.len == 3 and isLetLocation(n.sons[2]):
+  of someEq:
+    if skipConv(n.sons[2]).kind == nkNilLit and (
+        isLetLocation(n.sons[1], false) or isVar(n.sons[1])):
+      result = buildIsNil(n.sons[1])
+    else:
+      if isLetLocation(n.sons[1], true) or isLetLocation(n.sons[2], true):
+        # XXX algebraic simplifications!  'i-1 < a.len' --> 'i < a.len+1'
+        result = n
+  of someLe+someLt:
+    if isLetLocation(n.sons[1], true) or isLetLocation(n.sons[2], true):
       # XXX algebraic simplifications!  'i-1 < a.len' --> 'i < a.len+1'
       result = n
-  of someIn, mIsNil:
-    if isLetLocation(n.sons[1]):
+  of mIsNil:
+    if isLetLocation(n.sons[1], false) or isVar(n.sons[1]):
+      result = n
+  of someIn:
+    if isLetLocation(n.sons[1], true):
       result = n
   of mAnd:
     let
@@ -102,7 +148,9 @@ proc usefulFact(n: PNode): PNode =
         result.sons[2] = b.neg
     else:
       let a = usefulFact(n.sons[1])
-      if a != nil: result = n
+      if a != nil:
+        result = copyTree(n)
+        result.sons[1] = a
   of mOr:
     # 'or' sucks! (p.isNil or q.isNil) --> hard to do anything
     # with that knowledge...
@@ -157,10 +205,44 @@ proc sameTree(a, b: PNode): bool =
           if not sameTree(a.sons[i], b.sons[i]): return
         result = true
 
+proc hasSubTree(n, x: PNode): bool =
+  if n.sameTree(x): result = true
+  else:
+    for i in 0..safeLen(n)-1:
+      if hasSubTree(n.sons[i], x): return true
+
+proc invalidateFacts*(m: var TModel, n: PNode) =
+  # We are able to guard local vars (as opposed to 'let' variables)!
+  # 'while p != nil: f(p); p = p.next'
+  # This is actually quite easy to do:
+  # Re-assignments (incl. pass to a 'var' param) trigger an invalidation
+  # of every fact that contains 'v'. 
+  # 
+  #   if x < 4:
+  #     if y < 5
+  #       x = unknown()
+  #       # we invalidate 'x' here but it's known that x >= 4
+  #       # for the else anyway
+  #   else:
+  #     echo x
+  #
+  # The same mechanism could be used for more complex data stored on the heap;
+  # procs that 'write: []' cannot invalidate 'n.kind' for instance. In fact, we
+  # could CSE these expressions then and help C's optimizer.
+  for i in 0..high(m):
+    if m[i] != nil and m[i].hasSubTree(n): m[i] = nil
+
 proc valuesUnequal(a, b: PNode): bool =
   if a.isValue and b.isValue:
     result = not SameValue(a, b)
 
+proc pred(n: PNode): PNode =
+  if n.kind in {nkCharLit..nkUInt64Lit} and n.intVal != low(biggestInt):
+    result = copyNode(n)
+    dec result.intVal
+  else:
+    result = n
+
 type
   TImplication* = enum
     impUnknown, impNo, impYes  
@@ -178,35 +260,85 @@ proc impliesEq(fact, eq: PNode): TImplication =
       if sameTree(fact.sons[1], eq.sons[val]): result = impYes
       elif valuesUnequal(fact.sons[1], eq.sons[val]): result = impNo
   of mInSet:
-    if sameTree(fact.sons[1], eq.sons[loc]) and isValue(eq.sons[val]):
-      if inSet(fact.sons[2], eq.sons[val]): result = impYes
+    # remember: mInSet is 'contains' so the set comes first!
+    if sameTree(fact.sons[2], eq.sons[loc]) and isValue(eq.sons[val]):
+      if inSet(fact.sons[1], eq.sons[val]): result = impYes
       else: result = impNo
-  of mIsNil:
-    if sameTree(fact.sons[1], eq.sons[loc]):
-      if eq.sons[val].kind == nkNilLit:
-        result = impYes
   of mNot, mOr, mAnd: internalError(eq.info, "impliesEq")
-  else: nil
+  else: discard
   
-proc impliesIsNil(fact, eq: PNode): TImplication =
+proc leImpliesIn(x, c, aSet: PNode): TImplication =
+  if c.kind in {nkCharLit..nkUInt64Lit}:
+    # fact:  x <= 4;  question x in {56}?
+    # --> true iff every value <= 4 is in the set {56}
+    #   
+    var value = newIntNode(c.kind, firstOrd(x.typ))
+    # don't iterate too often:
+    if c.intVal - value.intVal < 1000:
+      var i, pos, neg: int
+      while value.intVal <= c.intVal:
+        if inSet(aSet, value): inc pos
+        else: inc neg
+        inc i; inc value.intVal
+      if pos == i: result = impYes
+      elif neg == i: result = impNo
+      #echo "result ", result, " ", i, " ", neg, " ", pos
+      # XXX wrong for the impNo case
+
+proc geImpliesIn(x, c, aSet: PNode): TImplication =
+  if c.kind in {nkCharLit..nkUInt64Lit}:
+    # fact:  x >= 4;  question x in {56}?
+    # --> true iff every value >= 4 is in the set {56}
+    #   
+    var value = newIntNode(c.kind, c.intVal)
+    let max = lastOrd(x.typ)
+    # don't iterate too often:
+    if max - value.intVal < 1000:
+      var i, pos, neg: int
+      while value.intVal <= max:
+        if inSet(aSet, value): inc pos
+        else: inc neg
+        inc i; inc value.intVal
+      if pos == i: result = impYes
+      elif neg == i: result = impNo
+
+proc compareSets(a, b: PNode): TImplication =
+  if equalSets(a, b): result = impYes
+  elif intersectSets(a, b).len == 0: result = impNo
+
+proc impliesIn(fact, loc, aSet: PNode): TImplication =
   case fact.sons[0].sym.magic
   of someEq:
-    if sameTree(fact.sons[1], eq.sons[1]):
-      if fact.sons[2].kind == nkNilLit: result = impYes
-    elif sameTree(fact.sons[2], eq.sons[1]):
-      if fact.sons[1].kind == nkNilLit: result = impYes
+    if sameTree(fact.sons[1], loc):
+      if inSet(aSet, fact.sons[2]): result = impYes
+      else: result = impNo
+    elif sameTree(fact.sons[2], loc):
+      if inSet(aSet, fact.sons[1]): result = impYes
+      else: result = impNo
+  of mInSet:
+    if sameTree(fact.sons[2], loc):
+      result = compareSets(fact.sons[1], aSet)
+  of someLe:
+    if sameTree(fact.sons[1], loc):
+      result = leImpliesIn(fact.sons[1], fact.sons[2], aSet)
+    elif sameTree(fact.sons[2], loc):
+      result = geImpliesIn(fact.sons[2], fact.sons[1], aSet)
+  of someLt:
+    if sameTree(fact.sons[1], loc):
+      result = leImpliesIn(fact.sons[1], fact.sons[2].pred, aSet)
+    elif sameTree(fact.sons[2], loc):
+      # 4 < x  -->  3 <= x
+      result = geImpliesIn(fact.sons[2], fact.sons[1].pred, aSet)
+  of mNot, mOr, mAnd: internalError(loc.info, "impliesIn")
+  else: discard
+  
+proc impliesIsNil(fact, eq: PNode): TImplication =
+  case fact.sons[0].sym.magic
   of mIsNil:
     if sameTree(fact.sons[1], eq.sons[1]):
       result = impYes
   of mNot, mOr, mAnd: internalError(eq.info, "impliesIsNil")
-  else: nil
-
-proc pred(n: PNode): PNode =
-  if n.kind in {nkCharLit..nkUInt64Lit} and n.intVal != low(biggestInt):
-    result = copyNode(n)
-    dec result.intVal
-  else:
-    result = n
+  else: discard
 
 proc impliesGe(fact, x, c: PNode): TImplication =
   InternalAssert isLocation(x)
@@ -242,7 +374,7 @@ proc impliesGe(fact, x, c: PNode): TImplication =
       if isValue(fact.sons[1]) and isValue(c):
         if leValue(c, fact.sons[1]): result = impYes
   of mNot, mOr, mAnd: internalError(x.info, "impliesGe")
-  else: nil
+  else: discard
 
 proc impliesLe(fact, x, c: PNode): TImplication =
   if not isLocation(x):
@@ -330,17 +462,70 @@ proc factImplies(fact, prop: PNode, isNegation: bool): TImplication =
     result = impliesLe(fact, prop.sons[1], prop.sons[2])
   of someLt:
     result = impliesLt(fact, prop.sons[1], prop.sons[2])
+  of mInSet:
+    result = impliesIn(fact, prop.sons[2], prop.sons[1])
   else:
     internalError(prop.info, "invalid proposition")
 
 proc doesImply*(facts: TModel, prop: PNode): TImplication =
   assert prop.kind in nkCallKinds
   for f in facts:
-    result = f.factImplies(prop, false)
-    if result != impUnknown: return
+    # facts can be invalidated, in which case they are 'nil':
+    if not f.isNil:
+      result = f.factImplies(prop, false)
+      if result != impUnknown: return
 
 proc impliesNotNil*(facts: TModel, arg: PNode): TImplication =
-  var x = newNodeI(nkCall, arg.info, 2)
-  x.sons[0] = newSymNode(getSysMagic("isNil", mIsNil))
-  x.sons[1] = arg
-  result = doesImply(facts, x.neg)
+  result = doesImply(facts, buildIsNil(arg).neg)
+
+proc settype(n: PNode): PType =
+  result = newType(tySet, n.typ.owner)
+  addSonSkipIntLit(result, n.typ)
+
+proc buildOf(it, loc: PNode): PNode =
+  var s = newNodeI(nkCurly, it.info, it.len-1)
+  s.typ = settype(loc)
+  for i in 0..it.len-2: s.sons[i] = it.sons[i]
+  result = newNodeI(nkCall, it.info, 3)
+  result.sons[0] = newSymNode(getSysMagic("contains", mInSet))
+  result.sons[1] = s
+  result.sons[2] = loc
+
+proc buildElse(n: PNode): PNode =
+  var s = newNodeIT(nkCurly, n.info, settype(n.sons[0]))
+  for i in 1..n.len-2:
+    let branch = n.sons[i]
+    assert branch.kind == nkOfBranch
+    for j in 0..branch.len-2:
+      s.add(branch.sons[j])
+  result = newNodeI(nkCall, n.info, 3)
+  result.sons[0] = newSymNode(getSysMagic("contains", mInSet))
+  result.sons[1] = s
+  result.sons[2] = n.sons[0]
+
+proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) =
+  let branch = n.sons[i]
+  if branch.kind == nkOfBranch:
+    m.add buildOf(branch, n.sons[0])
+  else:
+    m.add n.buildElse.neg
+
+proc buildProperFieldCheck(access, check: PNode): PNode =
+  if check.sons[1].kind == nkCurly:
+    result = copyTree(check)
+    if access.kind == nkDotExpr:
+      var a = copyTree(access)
+      a.sons[1] = check.sons[2]
+      result.sons[2] = a
+      # 'access.kind != nkDotExpr' can happen for object constructors
+      # which we don't check yet
+  else:
+    # it is some 'not'
+    assert check.getMagic == mNot
+    result = buildProperFieldCheck(access, check.sons[1]).neg
+
+proc checkFieldAccess*(m: TModel, n: PNode) =
+  for i in 1..n.len-1:
+    let check = buildProperFieldCheck(n.sons[0], n.sons[i])
+    if m.doesImply(check) != impYes:
+      Message(n.info, warnProveField, renderTree(n.sons[0])); break