diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ccgtypes.nim | 18 | ||||
| -rw-r--r-- | compiler/cgen.nim | 2 | ||||
| -rw-r--r-- | compiler/guards.nim | 346 |
3 files changed, 356 insertions, 10 deletions
diff --git a/compiler/ccgtypes.nim b/compiler/ccgtypes.nim index 427b0ec86..88e7e264d 100644 --- a/compiler/ccgtypes.nim +++ b/compiler/ccgtypes.nim @@ -674,7 +674,7 @@ proc genProcHeader(m: BModule, prc: PSym): PRope = # ------------------ type info generation ------------------------------------- -proc genTypeInfo(m: BModule, typ: PType): PRope +proc genTypeInfo(m: BModule, t: PType): PRope proc getNimNode(m: BModule): PRope = result = ropef("$1[$2]", [m.typeNodesName, toRope(m.typeNodes)]) inc(m.typeNodes) @@ -692,7 +692,7 @@ proc isObjLackingTypeField(typ: PType): bool {.inline.} = result = (typ.kind == tyObject) and ((tfFinal in typ.flags) and (typ.sons[0] == nil) or isPureObject(typ)) -proc genTypeInfoAuxBase(m: BModule, typ: PType, name, base: PRope) = +proc genTypeInfoAuxBase(m: BModule, typ: PType, name, base: PRope) = var nimtypeKind: int #allocMemTI(m, typ, name) if isObjLackingTypeField(typ): @@ -901,21 +901,21 @@ type include ccgtrav -proc genTypeInfo(m: BModule, typ: PType): PRope = - var t = getUniqueType(typ) +proc genTypeInfo(m: BModule, t: PType): PRope = + var t = getUniqueType(t) result = ropef("NTI$1", [toRope(t.id)]) - let owner = typ.skipTypes(typedescPtrs).owner.getModule + if ContainsOrIncl(m.typeInfoMarker, t.id): + return con("(&".toRope, result, ")".toRope) + let owner = t.skipTypes(typedescPtrs).owner.getModule if owner != m.module: # make sure the type info is created in the owner module - discard genTypeInfo(owner.bmod, typ) - # refenrece the type info as extern here + discard genTypeInfo(owner.bmod, t) + # reference the type info as extern here discard cgsym(m, "TNimType") discard cgsym(m, "TNimNode") appf(m.s[cfsVars], "extern TNimType $1; /* $2 */$n", [result, toRope(typeToString(t))]) return con("(&".toRope, result, ")".toRope) - if ContainsOrIncl(m.typeInfoMarker, t.id): - return con("(&".toRope, result, ")".toRope) case t.kind of tyEmpty: result = toRope"0" of tyPointer, tyBool, tyChar, tyCString, tyString, tyInt..tyUInt64, tyVar: diff --git a/compiler/cgen.nim b/compiler/cgen.nim index 7e782fc12..45fb9f878 100644 --- a/compiler/cgen.nim +++ b/compiler/cgen.nim @@ -1031,7 +1031,7 @@ proc genInitCode(m: BModule) = var procname = CStringLit(m.initProc, prc, m.module.name.s) app(prc, initFrame(m.initProc, procname, m.module.info.quotedFilename)) else: - app(prc, ~"\tvolatile TFrame F; F.len = 0;$N") + app(prc, ~"\tTFrame F; F.len = 0;$N") app(prc, genSectionStart(cpsInit)) app(prc, m.preInitProc.s(cpsInit)) diff --git a/compiler/guards.nim b/compiler/guards.nim new file mode 100644 index 000000000..6d0bf6bc6 --- /dev/null +++ b/compiler/guards.nim @@ -0,0 +1,346 @@ +# +# +# The Nimrod Compiler +# (c) Copyright 2013 Andreas Rumpf +# +# See the file "copying.txt", included in this +# distribution, for details about the copyright. +# + +## This module implements the 'implies' relation for guards. + +import ast, astalgo, msgs, magicsys, nimsets, trees, types, renderer + +const + someEq = {mEqI, mEqI64, mEqF64, mEqEnum, mEqCh, mEqB, mEqRef, mEqProc, + mEqUntracedRef, mEqStr, mEqSet, mEqCString} + + # set excluded here as the semantics are vastly different: + someLe = {mLeI, mLeI64, mLeF64, mLeU, mLeU64, mLeEnum, + mLeCh, mLeB, mLePtr, mLeStr} + someLt = {mLtI, mLtI64, mLtF64, mLtU, mLtU64, mLtEnum, + mLtCh, mLtB, mLtPtr, mLtStr} + + someLen = {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq} + + someIn = {mInRange, mInSet} + +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 = + var n = m + while true: + case n.kind + of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv: + n = n.sons[0] + 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 + +proc neg(n: PNode): PNode = + if n.getMagic == mNot: + result = n.sons[1] + else: + result = newNodeI(nkCall, n.info, 2) + result.sons[0] = newSymNode(getSysMagic("not", mNot)) + result.sons[1] = n + +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]): + # XXX algebraic simplifications! 'i-1 < a.len' --> 'i < a.len+1' + result = n + of someIn, mIsNil: + if isLetLocation(n.sons[1]): + result = n + of mAnd: + let + a = usefulFact(n.sons[1]) + b = usefulFact(n.sons[2]) + if a != nil and b != nil: + result = newNodeI(nkCall, n.info, 3) + result.sons[0] = newSymNode(getSysMagic("and", mAnd)) + result.sons[1] = a + result.sons[2] = b + elif a != nil: + result = a + elif b != nil: + result = b + of mNot: + case n.sons[1].getMagic + of mNot: + # normalize 'not (not a)' into 'a': + result = usefulFact(n.sons[1].sons[1]) + of mOr: + # not (a or b) --> not a and not b + let n = n.sons[1] + let + a = usefulFact(n.sons[1]) + b = usefulFact(n.sons[2]) + if a != nil and b != nil: + result = newNodeI(nkCall, n.info, 3) + result.sons[0] = newSymNode(getSysMagic("and", mAnd)) + result.sons[1] = a.neg + result.sons[2] = b.neg + else: + let a = usefulFact(n.sons[1]) + if a != nil: result = n + of mOr: + # 'or' sucks! (p.isNil or q.isNil) --> hard to do anything + # with that knowledge... + # DeMorgan helps a little though: + # not a or not b --> not (a and b) + # (x == 3) or (y == 2) ---> not ( not (x==3) and not (y == 2)) + # not (x != 3 and y != 2) + let + a = usefulFact(n.sons[1]) + b = usefulFact(n.sons[2]) + if a != nil and b != nil: + result = newNodeI(nkCall, n.info, 3) + result.sons[0] = newSymNode(getSysMagic("and", mAnd)) + result.sons[1] = a.neg + result.sons[2] = b.neg + result = result.neg + elif n.kind == nkSym and n.sym.kind == skLet: + # consider: + # let a = 2 < x + # if a: + # ... + # We make can easily replace 'a' by '2 < x' here: + result = usefulFact(n.sym.ast) + elif n.kind == nkStmtListExpr: + result = usefulFact(n.lastSon) + +type + TModel* = seq[PNode] # the "knowledge base" + +proc addFact*(m: var TModel, n: PNode) = + let n = usefulFact(n) + if n != nil: m.add n + +proc addFactNeg*(m: var TModel, n: PNode) = addFact(m, n.neg) + +proc sameTree(a, b: PNode): bool = + result = false + if a == b: + result = true + elif (a != nil) and (b != nil) and (a.kind == b.kind): + case a.kind + of nkSym: result = a.sym == b.sym + of nkIdent: result = a.ident.id == b.ident.id + of nkCharLit..nkInt64Lit: result = a.intVal == b.intVal + of nkFloatLit..nkFloat64Lit: result = a.floatVal == b.floatVal + of nkStrLit..nkTripleStrLit: result = a.strVal == b.strVal + of nkType: result = a.typ == b.typ + of nkEmpty, nkNilLit: result = true + else: + if sonsLen(a) == sonsLen(b): + for i in countup(0, sonsLen(a) - 1): + if not sameTree(a.sons[i], b.sons[i]): return + result = true + +proc valuesUnequal(a, b: PNode): bool = + if a.isValue and b.isValue: + result = not SameValue(a, b) + +type + TImplication* = enum + impUnknown, impNo, impYes + +proc impliesEq(fact, eq: PNode): TImplication = + let (loc, val) = if isLocation(eq.sons[1]): (1, 2) else: (2, 1) + + case fact.sons[0].sym.magic + of someEq: + if sameTree(fact.sons[1], eq.sons[loc]): + # this is not correct; consider: a == b; a == 1 --> unknown! + if sameTree(fact.sons[2], eq.sons[val]): result = impYes + elif valuesUnequal(fact.sons[2], eq.sons[val]): result = impNo + elif sameTree(fact.sons[2], eq.sons[loc]): + 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 + 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 + +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 + +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) + case fact.sons[0].sym.magic + of someEq: + if sameTree(fact.sons[1], x): + if isValue(fact.sons[2]) and isValue(c): + # fact: x = 4; question x >= 56? --> true iff 4 >= 56 + if leValue(c, fact.sons[2]): result = impYes + else: result = impNo + elif sameTree(fact.sons[2], x): + if isValue(fact.sons[1]) and isValue(c): + if leValue(c, fact.sons[1]): result = impYes + else: result = impNo + of someLt: + if sameTree(fact.sons[1], x): + if isValue(fact.sons[2]) and isValue(c): + # fact: x < 4; question N <= x? --> false iff N <= 4 + if leValue(fact.sons[2], c): result = impNo + # fact: x < 4; question 2 <= x? --> we don't know + elif sameTree(fact.sons[2], x): + # fact: 3 < x; question: N-1 < x ? --> true iff N-1 <= 3 + if isValue(fact.sons[1]) and isValue(c): + if leValue(c.pred, fact.sons[1]): result = impYes + of someLe: + if sameTree(fact.sons[1], x): + if isValue(fact.sons[2]) and isValue(c): + # fact: x <= 4; question x >= 56? --> false iff 4 <= 56 + if leValue(fact.sons[2], c): result = impNo + # fact: x <= 4; question x >= 2? --> we don't know + elif sameTree(fact.sons[2], x): + # fact: 3 <= x; question: x >= 2 ? --> true iff 2 <= 3 + 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 + +proc impliesLe(fact, x, c: PNode): TImplication = + if not isLocation(x): + return impliesGe(fact, c, x) + case fact.sons[0].sym.magic + of someEq: + if sameTree(fact.sons[1], x): + if isValue(fact.sons[2]) and isValue(c): + # fact: x = 4; question x <= 56? --> true iff 4 <= 56 + if leValue(fact.sons[2], c): result = impYes + else: result = impNo + elif sameTree(fact.sons[2], x): + if isValue(fact.sons[1]) and isValue(c): + if leValue(fact.sons[1], c): result = impYes + else: result = impNo + of someLt: + if sameTree(fact.sons[1], x): + if isValue(fact.sons[2]) and isValue(c): + # fact: x < 4; question x <= N? --> true iff N-1 <= 4 + if leValue(fact.sons[2], c.pred): result = impYes + # fact: x < 4; question x <= 2? --> we don't know + elif sameTree(fact.sons[2], x): + # fact: 3 < x; question: x <= 1 ? --> false iff 1 <= 3 + if isValue(fact.sons[1]) and isValue(c): + if leValue(c, fact.sons[1]): result = impNo + + of someLe: + if sameTree(fact.sons[1], x): + if isValue(fact.sons[2]) and isValue(c): + # fact: x <= 4; question x <= 56? --> true iff 4 <= 56 + if leValue(fact.sons[2], c): result = impYes + # fact: x <= 4; question x <= 2? --> we don't know + + elif sameTree(fact.sons[2], x): + # fact: 3 <= x; question: x <= 2 ? --> false iff 2 < 3 + if isValue(fact.sons[1]) and isValue(c): + if leValue(c, fact.sons[1].pred): result = impNo + + of mNot, mOr, mAnd: internalError(x.info, "impliesLe") + else: nil + +proc impliesLt(fact, x, c: PNode): TImplication = + # x < 3 same as x <= 2: + let p = c.pred + if p != c: + result = impliesLe(fact, x, p) + else: + # 4 < x same as 3 <= x + let q = x.pred + if q != x: + result = impliesLe(fact, q, c) + +proc factImplies(fact, prop: PNode, isNegation: bool): TImplication = + case fact.getMagic + of mNot: + case factImplies(fact.sons[1], prop, not isNegation) + of impUnknown: return impUnknown + of impNo: return impYes + of impYes: return impNo + of mAnd: + if not isNegation: + result = factImplies(fact.sons[1], prop, isNegation) + if result != impUnknown: return result + return factImplies(fact.sons[2], prop, isNegation) + else: + # careful! not (a and b) means not a or not b: + # a or b --> both need to imply 'prop' + let a = factImplies(fact.sons[1], prop, isNegation) + let b = factImplies(fact.sons[2], prop, isNegation) + if a == b: return a + return impUnknown + else: discard + + case prop.sons[0].sym.magic + of mNot: + case fact.factImplies(prop.sons[1], isNegation) + of impUnknown: result = impUnknown + of impNo: result = impYes + of impYes: result = impNo + of mIsNil: + result = impliesIsNil(fact, prop) + of someEq: + result = impliesEq(fact, prop) + of someLe: + result = impliesLe(fact, prop.sons[1], prop.sons[2]) + of someLt: + result = impliesLt(fact, prop.sons[1], prop.sons[2]) + 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 + +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) |