diff options
| -rw-r--r-- | compiler/guards.nim | 255 | ||||
| -rw-r--r-- | compiler/msgs.nim | 23 | ||||
| -rw-r--r-- | compiler/semexprs.nim | 4 | ||||
| -rw-r--r-- | compiler/sempass2.nim | 34 | ||||
| -rw-r--r-- | tests/reject/tcheckedfield1.nim | 60 | ||||
| -rw-r--r-- | tests/reject/tnotnil1.nim | 5 | ||||
| -rw-r--r-- | todo.txt | 7 |
7 files changed, 330 insertions, 58 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 diff --git a/compiler/msgs.nim b/compiler/msgs.nim index 302a7cfd8..e57c41f71 100644 --- a/compiler/msgs.nim +++ b/compiler/msgs.nim @@ -106,11 +106,13 @@ type warnUnknownSubstitutionX, warnLanguageXNotSupported, warnCommentXIgnored, warnNilStatement, warnAnalysisLoophole, warnDifferentHeaps, warnWriteToForeignHeap, warnImplicitClosure, - warnEachIdentIsTuple, warnShadowIdent, warnProveInit, warnUninit, warnUser, - hintSuccess, hintSuccessX, - hintLineTooLong, hintXDeclaredButNotUsed, hintConvToBaseNotNeeded, - hintConvFromXtoItselfNotNeeded, hintExprAlwaysX, hintQuitCalled, - hintProcessing, hintCodeBegin, hintCodeEnd, hintConf, hintPath, + warnEachIdentIsTuple, warnShadowIdent, + warnProveInit, warnProveField, warnProveIndex, + warnUninit, warnUser, + hintSuccess, hintSuccessX, + hintLineTooLong, hintXDeclaredButNotUsed, hintConvToBaseNotNeeded, + hintConvFromXtoItselfNotNeeded, hintExprAlwaysX, hintQuitCalled, + hintProcessing, hintCodeBegin, hintCodeEnd, hintConf, hintPath, hintConditionAlwaysTrue, hintPattern, hintUser @@ -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", - "User"] + "ImplicitClosure", "EachIdentIsTuple", "ShadowIdent", + "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 diff --git a/compiler/semexprs.nim b/compiler/semexprs.nim index cdab9b535..d418cd1e7 100644 --- a/compiler/semexprs.nim +++ b/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 diff --git a/compiler/sempass2.nim b/compiler/sempass2.nim index 151cb9cbc..f5b70ff18 100644 --- a/compiler/sempass2.nim +++ b/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 - op != nil and tfNotNil notin op.flags: - case impliesNotNil(tracked.guards, n) - of impUnknown: - Message(n.info, errGenerated, - "cannot prove '$1' is not nil" % n.renderTree) - of impNo: - Message(n.info, errGenerated, "'$1' is provably nil" % n.renderTree) - of impYes: discard + if paramType != nil: + if tfNotNil in paramType.flags and op != nil and tfNotNil notin op.flags: + case impliesNotNil(tracked.guards, n) + of impUnknown: + Message(n.info, errGenerated, + "cannot prove '$1' is not nil" % n.renderTree) + of impNo: + Message(n.info, errGenerated, "'$1' is provably nil" % n.renderTree) + 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 diff --git a/tests/reject/tcheckedfield1.nim b/tests/reject/tcheckedfield1.nim new file mode 100644 index 000000000..f74a8b76d --- /dev/null +++ b/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() diff --git a/tests/reject/tnotnil1.nim b/tests/reject/tnotnil1.nim index 3535bbd63..222c77376 100644 --- a/tests/reject/tnotnil1.nim +++ b/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) diff --git a/todo.txt b/todo.txt index 5b9f36dcd..f0e01c6c6 100644 --- a/todo.txt +++ b/todo.txt @@ -1,9 +1,10 @@ version 0.9.4 ============= -- make 'bind' default for templates and introduce 'mixin'; -- test 'not nil' checking more -- prove field accesses; prove array accesses +- make 'bind' default for templates and introduce 'mixin' +- fix tcheckedfield1 +- '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' |