next steps for guarded data flow analysis

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:
+  of someEq:
-    if isLetLocation(n.sons[1]) or n.len == 3 and isLetLocation(n.sons[2]):
+    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:
+  of mIsNil:
-    if isLetLocation(n.sons[1]):
+    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]):
+    # remember: mInSet is 'contains' so the set comes first!
-      if inSet(fact.sons[2], eq.sons[val]): result = impYes
+    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 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], 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 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
   of mIsNil:
     if sameTree(fact.sons[1], eq.sons[1]):
       result = impYes
   of mNot, mOr, mAnd: internalError(eq.info, "impliesIsNil")
-  else: nil
+  else: discard
-
-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
 
 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)
+    # facts can be invalidated, in which case they are 'nil':
-    if result != impUnknown: return
+    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)
+  result = doesImply(facts, buildIsNil(arg).neg)
-  x.sons[0] = newSymNode(getSysMagic("isNil", mIsNil))
+
-  x.sons[1] = arg
+proc settype(n: PNode): PType =
-  result = doesImply(facts, x.neg)
+  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

compiler/msgs.nim

@@ -106,7 +106,9 @@ type
     warnUnknownSubstitutionX, warnLanguageXNotSupported, warnCommentXIgnored, 
     warnNilStatement, warnAnalysisLoophole,
     warnDifferentHeaps, warnWriteToForeignHeap, warnImplicitClosure,
-    warnEachIdentIsTuple, warnShadowIdent, warnProveInit, warnUninit, warnUser,
+    warnEachIdentIsTuple, warnShadowIdent, 
+    warnProveInit, warnProveField, warnProveIndex,
+    warnUninit, warnUser,
     hintSuccess, hintSuccessX,
     hintLineTooLong, hintXDeclaredButNotUsed, hintConvToBaseNotNeeded,
     hintConvFromXtoItselfNotNeeded, hintExprAlwaysX, hintQuitCalled,
@@ -356,6 +358,8 @@ const
     warnEachIdentIsTuple: "each identifier is a tuple [EachIdentIsTuple]",
     warnShadowIdent: "shadowed identifier: '$1' [ShadowIdent]",
     warnProveInit: "Cannot prove that '$1' is initialized. This will become a compile time error in the future. [ProveInit]",
+    warnProveField: "cannot prove that field '$1' is accessible [ProveField]",
+    warnProveIndex: "cannot prove index '$1' is valid [ProveIndex]",
     warnUninit: "'$1' might not have been initialized [Uninit]",
     warnUser: "$1 [User]", 
     hintSuccess: "operation successful [Success]", 
@@ -376,15 +380,15 @@ const
     hintUser: "$1 [User]"]
 
 const
-  WarningsToStr*: array[0..21, string] = ["CannotOpenFile", "OctalEscape", 
+  WarningsToStr*: array[0..23, string] = ["CannotOpenFile", "OctalEscape", 
     "XIsNeverRead", "XmightNotBeenInit",
     "Deprecated", "ConfigDeprecated",
     "SmallLshouldNotBeUsed", "UnknownMagic", 
     "RedefinitionOfLabel", "UnknownSubstitutionX", "LanguageXNotSupported", 
     "CommentXIgnored", "NilStmt",
     "AnalysisLoophole", "DifferentHeaps", "WriteToForeignHeap",
-    "ImplicitClosure", "EachIdentIsTuple", "ShadowIdent", "ProveInit", "Uninit",
+    "ImplicitClosure", "EachIdentIsTuple", "ShadowIdent", 
-    "User"]
+    "ProveInit", "ProveField", "ProveIndex", "Uninit", "User"]
 
   HintsToStr*: array[0..15, string] = ["Success", "SuccessX", "LineTooLong", 
     "XDeclaredButNotUsed", "ConvToBaseNotNeeded", "ConvFromXtoItselfNotNeeded", 
@@ -516,7 +520,8 @@ proc sourceLine*(i: TLineInfo): PRope
 
 var
   gNotes*: TNoteKinds = {low(TNoteKind)..high(TNoteKind)} - 
-                        {warnShadowIdent, warnUninit}
+                        {warnShadowIdent, warnUninit,
+                         warnProveField, warnProveIndex}
   gErrorCounter*: int = 0     # counts the number of errors
   gHintCounter*: int = 0
   gWarnCounter*: int = 0

compiler/semexprs.nim

@@ -1657,7 +1657,9 @@ proc semObjConstr(c: PContext, n: PNode, flags: TExprFlags): PNode =
       e = fitNode(c, f.typ, e)
       # small hack here in a nkObjConstr the ``nkExprColonExpr`` node can have
       # 3 childen the last being the field check
-      if check != nil: it.add(check)
+      if check != nil:
+        check.sons[0] = it.sons[0]
+        it.add(check)
     else:
       localError(it.info, errUndeclaredFieldX, id.s)
     it.sons[1] = e

compiler/sempass2.nim

@@ -315,15 +315,17 @@ proc trackOperand(tracked: PEffects, n: PNode, paramType: PType) =
     else:
       mergeEffects(tracked, effectList.sons[exceptionEffects], n)
       mergeTags(tracked, effectList.sons[tagEffects], n)
-  if paramType != nil and tfNotNil in paramType.flags and
+  if paramType != nil:
-      op != nil and tfNotNil notin op.flags:
+    if tfNotNil in paramType.flags and op != nil and tfNotNil notin op.flags:
-    case impliesNotNil(tracked.guards, n)
+      case impliesNotNil(tracked.guards, n)
-    of impUnknown:
+      of impUnknown:
-      Message(n.info, errGenerated, 
+        Message(n.info, errGenerated, 
-              "cannot prove '$1' is not nil" % n.renderTree)
+                "cannot prove '$1' is not nil" % n.renderTree)
-    of impNo:
+      of impNo:
-      Message(n.info, errGenerated, "'$1' is provably nil" % n.renderTree)
+        Message(n.info, errGenerated, "'$1' is provably nil" % n.renderTree)
-    of impYes: discard
+      of impYes: discard
+    if skipTypes(paramType, abstractInst).kind == tyVar:
+      invalidateFacts(tracked.guards, n)
 
 proc breaksBlock(n: PNode): bool =
   case n.kind
@@ -341,16 +343,22 @@ proc breaksBlock(n: PNode): bool =
 proc trackCase(tracked: PEffects, n: PNode) =
   track(tracked, n.sons[0])
   let oldState = tracked.init.len
+  let oldFacts = tracked.guards.len
+  let interesting = interestingCaseExpr(n.sons[0]) and warnProveField in gNotes
   var inter: TIntersection = @[]
   var toCover = 0
   for i in 1.. <n.len:
     let branch = n.sons[i]
     setLen(tracked.init, oldState)
+    if interesting:
+      setLen(tracked.guards, oldFacts)
+      addCaseBranchFacts(tracked.guards, n, i)
     for i in 0 .. <branch.len:
       track(tracked, branch.sons[i])
     if not breaksBlock(branch.lastSon): inc toCover
     for i in oldState.. <tracked.init.len:
       addToIntersection(inter, tracked.init[i])
+    
   let exh = case skipTypes(n.sons[0].Typ, abstractVarRange-{tyTypeDesc}).Kind
             of tyFloat..tyFloat128, tyString:
               lastSon(n).kind == nkElse
@@ -361,6 +369,7 @@ proc trackCase(tracked: PEffects, n: PNode) =
     for id, count in items(inter):
       if count >= toCover: tracked.init.add id
     # else we can't merge
+  setLen(tracked.guards, oldFacts)
 
 proc trackIf(tracked: PEffects, n: PNode) =
   track(tracked, n.sons[0].sons[0])
@@ -453,12 +462,16 @@ proc track(tracked: PEffects, n: PNode) =
       # XXX new(objWithNotNil) is not initialized properly!
     for i in 0 .. <safeLen(n):
       track(tracked, n.sons[i])
+  of nkCheckedFieldExpr:
+    track(tracked, n.sons[0])
+    if warnProveField in gNotes: checkFieldAccess(tracked.guards, n)
   of nkTryStmt: trackTryStmt(tracked, n)
   of nkPragma: trackPragmaStmt(tracked, n)
   of nkMacroDef, nkTemplateDef: discard
   of nkAsgn, nkFastAsgn:
     track(tracked, n.sons[1])
     initVar(tracked, n.sons[0])
+    invalidateFacts(tracked.guards, n.sons[0])
     track(tracked, n.sons[0])
   of nkVarSection:
     for child in n:
@@ -476,8 +489,11 @@ proc track(tracked: PEffects, n: PNode) =
     else:
       # loop may never execute:
       let oldState = tracked.init.len
+      let oldFacts = tracked.guards.len
+      addFact(tracked.guards, n.sons[0])
       track(tracked, n.sons[1])
       setLen(tracked.init, oldState)
+      setLen(tracked.guards, oldFacts)
   of nkForStmt, nkParForStmt:
     # we are very conservative here and assume the loop is never executed:
     let oldState = tracked.init.len

tests/reject/tcheckedfield1.nim

@@ -0,0 +1,60 @@
+discard """
+  errormsg: "cannot prove that field 's' is accessible"
+  line:54
+"""
+
+import strutils
+
+{.warning[ProveField]: on.}
+
+type
+  TNodeKind = enum
+    nkBinary, nkTernary, nkStr
+  PNode = ref TNode not nil
+  TNode = object
+    case k: TNodeKind
+    of nkBinary, nkTernary: a, b: PNode
+    of nkStr: s: string
+    
+  PList = ref object
+    data: string
+    next: PList
+
+proc getData(x: PList not nil) =
+  echo x.data
+
+var head: PList
+
+proc processList() =
+  var it = head
+  while it != nil:
+    getData(it)
+    it = it.next
+
+proc toString2(x: PNode): string =
+  if x.k < nkStr:
+    toString2(x.a) & " " & toString2(x.b)
+  else:
+    x.s
+
+proc toString(x: PNode): string =
+  case x.k
+  of nkTernary, nkBinary:
+    toString(x.a) & " " & toString(x.b)
+  of nkStr:
+    x.s
+
+proc toString3(x: PNode): string =
+  if x.k <= nkBinary:
+    toString3(x.a) & " " & toString3(x.b)
+  else:
+    x.s # x.k in {nkStr}  --> fact:  not (x.k <= nkBinary)
+
+proc p() =
+  var x: PNode = PNode(k: nkStr, s: "abc")
+  
+  let y = x
+  if not y.isNil:
+    echo toString(y), " ", toString2(y)
+
+p()

tests/reject/tnotnil1.nim

@@ -1,6 +1,6 @@
 discard """
   errormsg: "'y' is provably nil"
-  line:22
+  line:25
 """
 
 import strutils
@@ -15,6 +15,9 @@ proc q(x: pointer not nil) =
 
 proc p() =
   var x: pointer
+  if not x.isNil:
+    q(x)
+  
   let y = x
   if not y.isNil:
     q(y)

todo.txt

@@ -1,9 +1,10 @@
 version 0.9.4
 =============
 
-- make 'bind' default for templates and introduce 'mixin';
+- make 'bind' default for templates and introduce 'mixin'
-- test 'not nil' checking more
+- fix tcheckedfield1
-- prove field accesses; prove array accesses
+- 'not nil' checking for globals
+- prove array accesses
 - special rule for ``[]=``
 - ``=`` should be overloadable; requires specialization for ``=``; general
   lift mechanism in the compiler is already implemented for 'fields'