fixes #481
This commit is contained in:
parent
2464da5b26
commit
ff1d68c50b
3 changed files with 41 additions and 2 deletions
|
|
@ -345,12 +345,22 @@ proc impliesIn(fact, loc, aSet: PNode): TImplication =
|
||||||
result = geImpliesIn(fact.sons[2], fact.sons[1].pred, aSet)
|
result = geImpliesIn(fact.sons[2], fact.sons[1].pred, aSet)
|
||||||
of mNot, mOr, mAnd: internalError(loc.info, "impliesIn")
|
of mNot, mOr, mAnd: internalError(loc.info, "impliesIn")
|
||||||
else: discard
|
else: discard
|
||||||
|
|
||||||
|
proc valueIsNil(n: PNode): TImplication =
|
||||||
|
if n.kind == nkNilLit: impYes
|
||||||
|
elif n.kind in {nkStrLit..nkTripleStrLit, nkBracket, nkObjConstr}: impNo
|
||||||
|
else: impUnknown
|
||||||
|
|
||||||
proc impliesIsNil(fact, eq: PNode): TImplication =
|
proc impliesIsNil(fact, eq: PNode): TImplication =
|
||||||
case fact.sons[0].sym.magic
|
case fact.sons[0].sym.magic
|
||||||
of mIsNil:
|
of mIsNil:
|
||||||
if sameTree(fact.sons[1], eq.sons[1]):
|
if sameTree(fact.sons[1], eq.sons[1]):
|
||||||
result = impYes
|
result = impYes
|
||||||
|
of someEq:
|
||||||
|
if sameTree(fact.sons[1], eq.sons[1]):
|
||||||
|
result = valueIsNil(fact.sons[2].skipConv)
|
||||||
|
elif sameTree(fact.sons[2], eq.sons[1]):
|
||||||
|
result = valueIsNil(fact.sons[1].skipConv)
|
||||||
of mNot, mOr, mAnd: internalError(eq.info, "impliesIsNil")
|
of mNot, mOr, mAnd: internalError(eq.info, "impliesIsNil")
|
||||||
else: discard
|
else: discard
|
||||||
|
|
||||||
|
|
@ -539,6 +549,13 @@ proc addDiscriminantFact*(m: var TModel, n: PNode) =
|
||||||
fact.sons[2] = n.sons[1]
|
fact.sons[2] = n.sons[1]
|
||||||
m.add fact
|
m.add fact
|
||||||
|
|
||||||
|
proc addAsgnFact*(m: var TModel, key, value: PNode) =
|
||||||
|
var fact = newNodeI(nkCall, key.info, 3)
|
||||||
|
fact.sons[0] = newSymNode(getSysMagic("==", mEqI))
|
||||||
|
fact.sons[1] = key
|
||||||
|
fact.sons[2] = value
|
||||||
|
m.add fact
|
||||||
|
|
||||||
proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) =
|
proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) =
|
||||||
let branch = n.sons[i]
|
let branch = n.sons[i]
|
||||||
if branch.kind == nkOfBranch:
|
if branch.kind == nkOfBranch:
|
||||||
|
|
|
||||||
|
|
@ -309,6 +309,12 @@ proc notNilCheck(tracked: PEffects, n: PNode, paramType: PType) =
|
||||||
let n = n.skipConv
|
let n = n.skipConv
|
||||||
if paramType != nil and tfNotNil in paramType.flags and
|
if paramType != nil and tfNotNil in paramType.flags and
|
||||||
n.typ != nil and tfNotNil notin n.typ.flags:
|
n.typ != nil and tfNotNil notin n.typ.flags:
|
||||||
|
if n.kind == nkAddr:
|
||||||
|
# addr(x[]) can't be proven, but addr(x) can:
|
||||||
|
if not containsNode(n, {nkDerefExpr, nkHiddenDeref}): return
|
||||||
|
elif n.kind == nkSym and n.sym.kind in RoutineKinds:
|
||||||
|
# 'p' is not nil obviously:
|
||||||
|
return
|
||||||
case impliesNotNil(tracked.guards, n)
|
case impliesNotNil(tracked.guards, n)
|
||||||
of impUnknown:
|
of impUnknown:
|
||||||
Message(n.info, errGenerated,
|
Message(n.info, errGenerated,
|
||||||
|
|
@ -481,6 +487,7 @@ proc track(tracked: PEffects, n: PNode) =
|
||||||
initVar(tracked, n.sons[0])
|
initVar(tracked, n.sons[0])
|
||||||
invalidateFacts(tracked.guards, n.sons[0])
|
invalidateFacts(tracked.guards, n.sons[0])
|
||||||
track(tracked, n.sons[0])
|
track(tracked, n.sons[0])
|
||||||
|
addAsgnFact(tracked.guards, n.sons[0], n.sons[1])
|
||||||
notNilCheck(tracked, n.sons[1], n.sons[0].typ)
|
notNilCheck(tracked, n.sons[1], n.sons[0].typ)
|
||||||
of nkVarSection:
|
of nkVarSection:
|
||||||
for child in n:
|
for child in n:
|
||||||
|
|
@ -489,6 +496,7 @@ proc track(tracked: PEffects, n: PNode) =
|
||||||
track(tracked, last)
|
track(tracked, last)
|
||||||
for i in 0 .. child.len-3:
|
for i in 0 .. child.len-3:
|
||||||
initVar(tracked, child.sons[i])
|
initVar(tracked, child.sons[i])
|
||||||
|
addAsgnFact(tracked.guards, child.sons[i], last)
|
||||||
notNilCheck(tracked, last, child.sons[i].typ)
|
notNilCheck(tracked, last, child.sons[i].typ)
|
||||||
# since 'var (a, b): T = ()' is not even allowed, there is always type
|
# since 'var (a, b): T = ()' is not even allowed, there is always type
|
||||||
# inference for (a, b) and thus no nil checking is necessary.
|
# inference for (a, b) and thus no nil checking is necessary.
|
||||||
|
|
@ -523,6 +531,7 @@ proc track(tracked: PEffects, n: PNode) =
|
||||||
if sfDiscriminant in x.sons[0].sym.flags:
|
if sfDiscriminant in x.sons[0].sym.flags:
|
||||||
addDiscriminantFact(tracked.guards, x)
|
addDiscriminantFact(tracked.guards, x)
|
||||||
setLen(tracked.guards, oldFacts)
|
setLen(tracked.guards, oldFacts)
|
||||||
|
of nkTypeSection: discard
|
||||||
else:
|
else:
|
||||||
for i in 0 .. <safeLen(n): track(tracked, n.sons[i])
|
for i in 0 .. <safeLen(n): track(tracked, n.sons[i])
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
discard """
|
discard """
|
||||||
errormsg: "'y' is provably nil"
|
errormsg: "'y' is provably nil"
|
||||||
line:25
|
line:38
|
||||||
"""
|
"""
|
||||||
|
|
||||||
import strutils
|
import strutils
|
||||||
|
|
@ -10,6 +10,19 @@ type
|
||||||
TObj = object
|
TObj = object
|
||||||
x, y: int
|
x, y: int
|
||||||
|
|
||||||
|
type
|
||||||
|
superstring = string not nil
|
||||||
|
|
||||||
|
|
||||||
|
proc q(s: superstring) =
|
||||||
|
echo s
|
||||||
|
|
||||||
|
proc p2() =
|
||||||
|
var a: string = "I am not nil"
|
||||||
|
q(a) # but this should and does not
|
||||||
|
|
||||||
|
p2()
|
||||||
|
|
||||||
proc q(x: pointer not nil) =
|
proc q(x: pointer not nil) =
|
||||||
nil
|
nil
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue