diff options
Diffstat (limited to 'compiler/guards.nim')
| -rw-r--r-- | compiler/guards.nim | 324 |
1 files changed, 231 insertions, 93 deletions
diff --git a/compiler/guards.nim b/compiler/guards.nim index a2cbdbda2..bbb239867 100644 --- a/compiler/guards.nim +++ b/compiler/guards.nim @@ -12,20 +12,22 @@ import ast, astalgo, msgs, magicsys, nimsets, trees, types, renderer, idents, saturate, modulegraphs, options, lineinfos, int128 +when defined(nimPreviewSlimSystem): + import std/assertions + const someEq = {mEqI, mEqF64, mEqEnum, mEqCh, mEqB, mEqRef, mEqProc, - mEqUntracedRef, mEqStr, mEqSet, mEqCString} + mEqStr, mEqSet, mEqCString} # set excluded here as the semantics are vastly different: - someLe = {mLeI, mLeF64, mLeU, mLeU64, mLeEnum, + someLe = {mLeI, mLeF64, mLeU, mLeEnum, mLeCh, mLeB, mLePtr, mLeStr} - someLt = {mLtI, mLtF64, mLtU, mLtU64, mLtEnum, + someLt = {mLtI, mLtF64, mLtU, mLtEnum, mLtCh, mLtB, mLtPtr, mLtStr} - someLen = {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq, - mXLenStr, mXLenSeq} + someLen = {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq} - someIn = {mInRange, mInSet} + someIn = {mInSet} someHigh = {mHigh} # we don't list unsigned here because wrap around semantics suck for @@ -47,8 +49,12 @@ proc isLet(n: PNode): bool = if n.sym.kind in {skLet, skTemp, skForVar}: result = true elif n.sym.kind == skParam and skipTypes(n.sym.typ, - abstractInst).kind != tyVar: + abstractInst).kind notin {tyVar}: result = true + else: + result = false + else: + result = false proc isVar(n: PNode): bool = n.kind == nkSym and n.sym.kind in {skResult, skVar} and @@ -66,9 +72,12 @@ proc isLetLocation(m: PNode, isApprox: bool): bool = case n.kind of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv: n = n[0] - of nkDerefExpr, nkHiddenDeref: + of nkDerefExpr: n = n[0] inc derefs + of nkHiddenDeref: + n = n[0] + if not isApprox: inc derefs of nkBracketExpr: if isConstExpr(n[1]) or isLet(n[1]) or isConstExpr(n[1].skipConv): n = n[0] @@ -83,26 +92,6 @@ proc isLetLocation(m: PNode, isApprox: bool): bool = proc interestingCaseExpr*(m: PNode): bool = isLetLocation(m, true) -type - Operators* = object - opNot, opContains, opLe, opLt, opAnd, opOr, opIsNil, opEq: PSym - opAdd, opSub, opMul, opDiv, opLen: PSym - -proc initOperators*(g: ModuleGraph): Operators = - result.opLe = createMagic(g, "<=", mLeI) - result.opLt = createMagic(g, "<", mLtI) - result.opAnd = createMagic(g, "and", mAnd) - result.opOr = createMagic(g, "or", mOr) - result.opIsNil = createMagic(g, "isnil", mIsNil) - result.opEq = createMagic(g, "==", mEqI) - result.opAdd = createMagic(g, "+", mAddI) - result.opSub = createMagic(g, "-", mSubI) - result.opMul = createMagic(g, "*", mMulI) - result.opDiv = createMagic(g, "div", mDivI) - result.opLen = createMagic(g, "len", mLengthSeq) - result.opNot = createMagic(g, "not", mNot) - result.opContains = createMagic(g, "contains", mInSet) - proc swapArgs(fact: PNode, newOp: PSym): PNode = result = newNodeI(nkCall, fact.info, 3) result[0] = newSymNode(newOp) @@ -151,18 +140,20 @@ proc neg(n: PNode; o: Operators): PNode = result = a elif b != nil: result = b + else: + result = nil else: # leave not (a == 4) as it is result = newNodeI(nkCall, n.info, 2) result[0] = newSymNode(o.opNot) result[1] = n -proc buildCall(op: PSym; a: PNode): PNode = +proc buildCall*(op: PSym; a: PNode): PNode = result = newNodeI(nkCall, a.info, 2) result[0] = newSymNode(op) result[1] = a -proc buildCall(op: PSym; a, b: PNode): PNode = +proc buildCall*(op: PSym; a, b: PNode): PNode = result = newNodeI(nkInfix, a.info, 3) result[0] = newSymNode(op) result[1] = a @@ -218,7 +209,7 @@ proc highBound*(conf: ConfigRef; x: PNode; o: Operators): PNode = nkIntLit.newIntNode(lastOrd(conf, typ)) elif typ.kind == tySequence and x.kind == nkSym and x.sym.kind == skConst: - nkIntLit.newIntNode(x.sym.ast.len-1) + nkIntLit.newIntNode(x.sym.astdef.len-1) else: o.opAdd.buildCall(o.opLen.buildCall(x), minusOne()) result.info = x.info @@ -250,15 +241,17 @@ proc pred(n: PNode): PNode = else: result = n +proc buildLe*(o: Operators; a, b: PNode): PNode = + result = o.opLe.buildCall(a, b) + proc canon*(n: PNode; o: Operators): PNode = - # XXX for now only the new code in 'semparallel' uses this if n.safeLen >= 1: result = shallowCopy(n) for i in 0..<n.len: result[i] = canon(n[i], o) elif n.kind == nkSym and n.sym.kind == skLet and n.sym.astdef.getMagic in (someEq + someAdd + someMul + someMin + - someMax + someHigh + {mUnaryLt} + someSub + someLen + someDiv): + someMax + someHigh + someSub + someLen + someDiv): result = n.sym.astdef.copyTree else: result = n @@ -271,14 +264,12 @@ proc canon*(n: PNode; o: Operators): PNode = of someHigh: # high == len+(-1) result = o.opAdd.buildCall(o.opLen.buildCall(result[1]), minusOne()) - of mUnaryLt: - result = buildCall(o.opAdd, result[1], minusOne()) of someSub: # x - 4 --> x + (-4) result = negate(result[1], result[2], result, o) of someLen: result[0] = o.opLen.newSymNode - of someLt: + of someLt - {mLtF64}: # x < y same as x <= y-1: let y = n[2].canon(o) let p = pred(y) @@ -318,12 +309,12 @@ proc canon*(n: PNode; o: Operators): PNode = if plus != nil and not isLetLocation(x, true): result = buildCall(result[0].sym, plus, y[1]) else: discard - elif x.isValue and y.getMagic in someAdd and y[2].isValue: + elif x.isValue and y.getMagic in someAdd and y[2].kind == x.kind: # 0 <= a.len + 3 # -3 <= a.len result[1] = x |-| y[2] result[2] = y[1] - elif x.isValue and y.getMagic in someSub and y[2].isValue: + elif x.isValue and y.getMagic in someSub and y[2].kind == x.kind: # 0 <= a.len - 3 # 3 <= a.len result[1] = x |+| y[2] @@ -343,6 +334,10 @@ proc usefulFact(n: PNode; o: Operators): PNode = if isLetLocation(n[1], true) or isLetLocation(n[2], true): # XXX algebraic simplifications! 'i-1 < a.len' --> 'i < a.len+1' result = n + elif n[1].getMagic in someLen or n[2].getMagic in someLen: + result = n + else: + result = nil of someLe+someLt: if isLetLocation(n[1], true) or isLetLocation(n[2], true): # XXX algebraic simplifications! 'i-1 < a.len' --> 'i < a.len+1' @@ -350,12 +345,18 @@ proc usefulFact(n: PNode; o: Operators): PNode = elif n[1].getMagic in someLen or n[2].getMagic in someLen: # XXX Rethink this whole idea of 'usefulFact' for semparallel result = n + else: + result = nil of mIsNil: if isLetLocation(n[1], false) or isVar(n[1]): result = n + else: + result = nil of someIn: if isLetLocation(n[1], true): result = n + else: + result = nil of mAnd: let a = usefulFact(n[1], o) @@ -369,10 +370,14 @@ proc usefulFact(n: PNode; o: Operators): PNode = result = a elif b != nil: result = b + else: + result = nil of mNot: let a = usefulFact(n[1], o) if a != nil: result = a.neg(o) + else: + result = nil of mOr: # 'or' sucks! (p.isNil or q.isNil) --> hard to do anything # with that knowledge... @@ -389,6 +394,8 @@ proc usefulFact(n: PNode; o: Operators): PNode = result[1] = a result[2] = b result = result.neg(o) + else: + result = nil elif n.kind == nkSym and n.sym.kind == skLet: # consider: # let a = 2 < x @@ -397,20 +404,34 @@ proc usefulFact(n: PNode; o: Operators): PNode = # We make can easily replace 'a' by '2 < x' here: if n.sym.astdef != nil: result = usefulFact(n.sym.astdef, o) + else: + result = nil elif n.kind == nkStmtListExpr: result = usefulFact(n.lastSon, o) + else: + result = nil type TModel* = object s*: seq[PNode] # the "knowledge base" - o*: Operators + g*: ModuleGraph + beSmart*: bool proc addFact*(m: var TModel, nn: PNode) = - let n = usefulFact(nn, m.o) - if n != nil: m.s.add n + let n = usefulFact(nn, m.g.operators) + if n != nil: + if not m.beSmart: + m.s.add n + else: + let c = canon(n, m.g.operators) + if c.getMagic == mAnd: + addFact(m, c[1]) + addFact(m, c[2]) + else: + m.s.add c proc addFactNeg*(m: var TModel, n: PNode) = - let n = n.neg(m.o) + let n = n.neg(m.g.operators) if n != nil: addFact(m, n) proc sameOpr(a, b: PSym): bool = @@ -450,10 +471,17 @@ proc sameTree*(a, b: PNode): bool = proc hasSubTree(n, x: PNode): bool = if n.sameTree(x): result = true else: - for i in 0..n.safeLen-1: - if hasSubTree(n[i], x): return true + case n.kind + of nkEmpty..nkNilLit: + result = n.sameTree(x) + of nkFormalParams: + result = false + else: + result = false + for i in 0..<n.len: + if hasSubTree(n[i], x): return true -proc invalidateFacts*(m: var TModel, n: PNode) = +proc invalidateFacts*(s: var seq[PNode], 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: @@ -471,12 +499,17 @@ proc invalidateFacts*(m: var TModel, n: PNode) = # 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.s): - if m.s[i] != nil and m.s[i].hasSubTree(n): m.s[i] = nil + for i in 0..high(s): + if s[i] != nil and s[i].hasSubTree(n): s[i] = nil + +proc invalidateFacts*(m: var TModel, n: PNode) = + invalidateFacts(m.s, n) proc valuesUnequal(a, b: PNode): bool = if a.isValue and b.isValue: result = not sameValue(a, b) + else: + result = false proc impliesEq(fact, eq: PNode): TImplication = let (loc, val) = if isLocation(eq[1]): (1, 2) else: (2, 1) @@ -487,16 +520,26 @@ proc impliesEq(fact, eq: PNode): TImplication = # this is not correct; consider: a == b; a == 1 --> unknown! if sameTree(fact[2], eq[val]): result = impYes elif valuesUnequal(fact[2], eq[val]): result = impNo + else: + result = impUnknown elif sameTree(fact[2], eq[loc]): if sameTree(fact[1], eq[val]): result = impYes elif valuesUnequal(fact[1], eq[val]): result = impNo + else: + result = impUnknown + else: + result = impUnknown of mInSet: # remember: mInSet is 'contains' so the set comes first! if sameTree(fact[2], eq[loc]) and isValue(eq[val]): if inSet(fact[1], eq[val]): result = impYes else: result = impNo - of mNot, mOr, mAnd: assert(false, "impliesEq") - else: discard + else: + result = impUnknown + of mNot, mOr, mAnd: + result = impUnknown + assert(false, "impliesEq") + else: result = impUnknown proc leImpliesIn(x, c, aSet: PNode): TImplication = if c.kind in {nkCharLit..nkUInt64Lit}: @@ -506,13 +549,19 @@ proc leImpliesIn(x, c, aSet: PNode): TImplication = var value = newIntNode(c.kind, firstOrd(nil, x.typ)) # don't iterate too often: if c.intVal - value.intVal < 1000: - var i, pos, neg: int + var i, pos, neg: int = 0 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 + else: + result = impUnknown + else: + result = impUnknown + else: + result = impUnknown proc geImpliesIn(x, c, aSet: PNode): TImplication = if c.kind in {nkCharLit..nkUInt64Lit}: @@ -523,17 +572,23 @@ proc geImpliesIn(x, c, aSet: PNode): TImplication = let max = lastOrd(nil, x.typ) # don't iterate too often: if max - getInt(value) < toInt128(1000): - var i, pos, neg: int + var i, pos, neg: int = 0 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 + else: result = impUnknown + else: + result = impUnknown + else: + result = impUnknown proc compareSets(a, b: PNode): TImplication = if equalSets(nil, a, b): result = impYes elif intersectSets(nil, a, b).len == 0: result = impNo + else: result = impUnknown proc impliesIn(fact, loc, aSet: PNode): TImplication = case fact[0].sym.magic @@ -544,22 +599,32 @@ proc impliesIn(fact, loc, aSet: PNode): TImplication = elif sameTree(fact[2], loc): if inSet(aSet, fact[1]): result = impYes else: result = impNo + else: + result = impUnknown of mInSet: if sameTree(fact[2], loc): result = compareSets(fact[1], aSet) + else: + result = impUnknown of someLe: if sameTree(fact[1], loc): result = leImpliesIn(fact[1], fact[2], aSet) elif sameTree(fact[2], loc): result = geImpliesIn(fact[2], fact[1], aSet) + else: + result = impUnknown of someLt: if sameTree(fact[1], loc): result = leImpliesIn(fact[1], fact[2].pred, aSet) elif sameTree(fact[2], loc): # 4 < x --> 3 <= x result = geImpliesIn(fact[2], fact[1].pred, aSet) - of mNot, mOr, mAnd: assert(false, "impliesIn") - else: discard + else: + result = impUnknown + of mNot, mOr, mAnd: + result = impUnknown + assert(false, "impliesIn") + else: result = impUnknown proc valueIsNil(n: PNode): TImplication = if n.kind == nkNilLit: impYes @@ -571,13 +636,19 @@ proc impliesIsNil(fact, eq: PNode): TImplication = of mIsNil: if sameTree(fact[1], eq[1]): result = impYes + else: + result = impUnknown of someEq: if sameTree(fact[1], eq[1]): result = valueIsNil(fact[2].skipConv) elif sameTree(fact[2], eq[1]): result = valueIsNil(fact[1].skipConv) - of mNot, mOr, mAnd: assert(false, "impliesIsNil") - else: discard + else: + result = impUnknown + of mNot, mOr, mAnd: + result = impUnknown + assert(false, "impliesIsNil") + else: result = impUnknown proc impliesGe(fact, x, c: PNode): TImplication = assert isLocation(x) @@ -588,35 +659,63 @@ proc impliesGe(fact, x, c: PNode): TImplication = # fact: x = 4; question x >= 56? --> true iff 4 >= 56 if leValue(c, fact[2]): result = impYes else: result = impNo + else: + result = impUnknown elif sameTree(fact[2], x): if isValue(fact[1]) and isValue(c): if leValue(c, fact[1]): result = impYes else: result = impNo + else: + result = impUnknown + else: + result = impUnknown of someLt: if sameTree(fact[1], x): if isValue(fact[2]) and isValue(c): # fact: x < 4; question N <= x? --> false iff N <= 4 if leValue(fact[2], c): result = impNo + else: result = impUnknown # fact: x < 4; question 2 <= x? --> we don't know + else: + result = impUnknown elif sameTree(fact[2], x): # fact: 3 < x; question: N-1 < x ? --> true iff N-1 <= 3 if isValue(fact[1]) and isValue(c): if leValue(c.pred, fact[1]): result = impYes + else: result = impUnknown + else: + result = impUnknown + else: + result = impUnknown of someLe: if sameTree(fact[1], x): if isValue(fact[2]) and isValue(c): # fact: x <= 4; question x >= 56? --> false iff 4 <= 56 if leValue(fact[2], c): result = impNo # fact: x <= 4; question x >= 2? --> we don't know + else: + result = impUnknown + else: + result = impUnknown elif sameTree(fact[2], x): # fact: 3 <= x; question: x >= 2 ? --> true iff 2 <= 3 if isValue(fact[1]) and isValue(c): if leValue(c, fact[1]): result = impYes - of mNot, mOr, mAnd: assert(false, "impliesGe") - else: discard + else: result = impUnknown + else: + result = impUnknown + else: + result = impUnknown + of mNot, mOr, mAnd: + result = impUnknown + assert(false, "impliesGe") + else: result = impUnknown proc impliesLe(fact, x, c: PNode): TImplication = if not isLocation(x): + if c.isValue: + if leValue(x, x): return impYes + else: return impNo return impliesGe(fact, c, x) case fact[0].sym.magic of someEq: @@ -625,35 +724,59 @@ proc impliesLe(fact, x, c: PNode): TImplication = # fact: x = 4; question x <= 56? --> true iff 4 <= 56 if leValue(fact[2], c): result = impYes else: result = impNo + else: + result = impUnknown elif sameTree(fact[2], x): if isValue(fact[1]) and isValue(c): if leValue(fact[1], c): result = impYes else: result = impNo + else: + result = impUnknown + else: + result = impUnknown of someLt: if sameTree(fact[1], x): if isValue(fact[2]) and isValue(c): # fact: x < 4; question x <= N? --> true iff N-1 <= 4 if leValue(fact[2], c.pred): result = impYes + else: + result = impUnknown # fact: x < 4; question x <= 2? --> we don't know + else: + result = impUnknown elif sameTree(fact[2], x): # fact: 3 < x; question: x <= 1 ? --> false iff 1 <= 3 if isValue(fact[1]) and isValue(c): if leValue(c, fact[1]): result = impNo - + else: result = impUnknown + else: + result = impUnknown + else: + result = impUnknown of someLe: if sameTree(fact[1], x): if isValue(fact[2]) and isValue(c): # fact: x <= 4; question x <= 56? --> true iff 4 <= 56 if leValue(fact[2], c): result = impYes + else: result = impUnknown # fact: x <= 4; question x <= 2? --> we don't know + else: + result = impUnknown elif sameTree(fact[2], x): # fact: 3 <= x; question: x <= 2 ? --> false iff 2 < 3 if isValue(fact[1]) and isValue(c): if leValue(c, fact[1].pred): result = impNo + else:result = impUnknown + else: + result = impUnknown + else: + result = impUnknown - of mNot, mOr, mAnd: assert(false, "impliesLe") - else: discard + of mNot, mOr, mAnd: + result = impUnknown + assert(false, "impliesLe") + else: result = impUnknown proc impliesLt(fact, x, c: PNode): TImplication = # x < 3 same as x <= 2: @@ -665,6 +788,8 @@ proc impliesLt(fact, x, c: PNode): TImplication = let q = x.pred if q != x: result = impliesLe(fact, q, c) + else: + result = impUnknown proc `~`(x: TImplication): TImplication = case x @@ -716,6 +841,7 @@ proc factImplies(fact, prop: PNode): TImplication = proc doesImply*(facts: TModel, prop: PNode): TImplication = assert prop.kind in nkCallKinds + result = impUnknown for f in facts.s: # facts can be invalidated, in which case they are 'nil': if not f.isNil: @@ -723,7 +849,7 @@ proc doesImply*(facts: TModel, prop: PNode): TImplication = if result != impUnknown: return proc impliesNotNil*(m: TModel, arg: PNode): TImplication = - result = doesImply(m, m.o.opIsNil.buildCall(arg).neg(m.o)) + result = doesImply(m, m.g.operators.opIsNil.buildCall(arg).neg(m.g.operators)) proc simpleSlice*(a, b: PNode): BiggestInt = # returns 'c' if a..b matches (i+c)..(i+c), -1 otherwise. (i)..(i) is matched @@ -744,7 +870,7 @@ template isSub(x): untyped = x.getMagic in someSub template isVal(x): untyped = x.kind in {nkCharLit..nkUInt64Lit} template isIntVal(x, y): untyped = x.intVal == y -import macros +import std/macros macro `=~`(x: PNode, pat: untyped): bool = proc m(x, pat, conds: NimNode) = @@ -777,12 +903,7 @@ macro `=~`(x: PNode, pat: untyped): bool = var conds = newTree(nnkBracket) m(x, pat, conds) - when compiles(nestList(ident"and", conds)): - result = nestList(ident"and", conds) - #elif declared(macros.toNimIdent): - # result = nestList(toNimIdent"and", conds) - else: - result = nestList(!"and", conds) + result = nestList(ident"and", conds) proc isMinusOne(n: PNode): bool = n.kind in {nkCharLit..nkUInt64Lit} and n.intVal == -1 @@ -802,7 +923,7 @@ proc ple(m: TModel; a, b: PNode): TImplication = if lastOrd(nil, a.typ) <= b.intVal: return impYes # 3 <= x iff low(x) <= 3 if a.isValue and b.typ != nil and b.typ.isOrdinalType: - if firstOrd(nil, b.typ) <= a.intVal: return impYes + if a.intVal <= firstOrd(nil, b.typ): return impYes # x <= x if sameTree(a, b): return impYes @@ -813,7 +934,11 @@ proc ple(m: TModel; a, b: PNode): TImplication = # x <= y+c if 0 <= c and x <= y # x <= y+(-c) if c <= 0 and y >= x - if b.getMagic in someAdd and zero() <=? b[2] and a <=? b[1]: return impYes + if b.getMagic in someAdd: + if zero() <=? b[2] and a <=? b[1]: return impYes + # x <= y-c if x+c <= y + if b[2] <=? zero() and (canon(m.g.operators.opSub.buildCall(a, b[2]), m.g.operators) <=? b[1]): + return impYes # x+c <= y if c <= 0 and x <= y if a.getMagic in someAdd and a[2] <=? zero() and a[1] <=? b: return impYes @@ -826,20 +951,20 @@ proc ple(m: TModel; a, b: PNode): TImplication = if a.getMagic in someMul and a[2].isValue and a[1].getMagic in someDiv and a[1][2].isValue: # simplify (x div 4) * 2 <= y to x div (c div d) <= y - if ple(m, buildCall(m.o.opDiv, a[1][1], `|div|`(a[1][2], a[2])), b) == impYes: + if ple(m, buildCall(m.g.operators.opDiv, a[1][1], `|div|`(a[1][2], a[2])), b) == impYes: return impYes # x*3 + x == x*4. It follows that: # x*3 + y <= x*4 if y <= x and 3 <= 4 if a =~ x*dc + y and b =~ x2*ec: if sameTree(x, x2): - let ec1 = m.o.opAdd.buildCall(ec, minusOne()) + let ec1 = m.g.operators.opAdd.buildCall(ec, minusOne()) if x >=? 1 and ec >=? 1 and dc >=? 1 and dc <=? ec1 and y <=? x: return impYes elif a =~ x*dc and b =~ x2*ec + y: #echo "BUG cam ehrer e ", a, " <=? ", b if sameTree(x, x2): - let ec1 = m.o.opAdd.buildCall(ec, minusOne()) + let ec1 = m.g.operators.opAdd.buildCall(ec, minusOne()) if x >=? 1 and ec >=? 1 and dc >=? 1 and dc <=? ec1 and y <=? zero(): return impYes @@ -892,6 +1017,7 @@ proc applyReplacements(n: PNode; rep: TReplacements): PNode = proc pleViaModelRec(m: var TModel; a, b: PNode): TImplication = # now check for inferrable facts: a <= b and b <= c implies a <= c + result = impUnknown for i in 0..m.s.high: let fact = m.s[i] if fact != nil and fact.getMagic in someLe: @@ -902,10 +1028,13 @@ proc pleViaModelRec(m: var TModel; a, b: PNode): TImplication = # --> true if (len-100) <= (len-1) let x = fact[1] let y = fact[2] - if sameTree(x, a) and y.getMagic in someAdd and b.getMagic in someAdd and - sameTree(y[1], b[1]): - if ple(m, b[2], y[2]) == impYes: - return impYes + # x <= y. + # Question: x <= b? True iff y <= b. + if sameTree(x, a): + if ple(m, y, b) == impYes: return impYes + if y.getMagic in someAdd and b.getMagic in someAdd and sameTree(y[1], b[1]): + if ple(m, b[2], y[2]) == impYes: + return impYes # x <= y implies a <= b if a <= x and y <= b if ple(m, a, x) == impYes: @@ -934,17 +1063,17 @@ proc pleViaModel(model: TModel; aa, bb: PNode): TImplication = let b = fact[2] if a.kind == nkSym: replacements.add((a,b)) else: replacements.add((b,a)) - var m: TModel + var m = TModel() var a = aa var b = bb if replacements.len > 0: m.s = @[] - m.o = model.o + m.g = model.g # make the other facts consistent: for fact in model.s: if fact != nil and fact.getMagic notin someEq: # XXX 'canon' should not be necessary here, but it is - m.s.add applyReplacements(fact, replacements).canon(m.o) + m.s.add applyReplacements(fact, replacements).canon(m.g.operators) a = applyReplacements(aa, replacements) b = applyReplacements(bb, replacements) else: @@ -953,20 +1082,25 @@ proc pleViaModel(model: TModel; aa, bb: PNode): TImplication = result = pleViaModelRec(m, a, b) proc proveLe*(m: TModel; a, b: PNode): TImplication = - let x = canon(m.o.opLe.buildCall(a, b), m.o) + let x = canon(m.g.operators.opLe.buildCall(a, b), m.g.operators) #echo "ROOT ", renderTree(x[1]), " <=? ", renderTree(x[2]) result = ple(m, x[1], x[2]) if result == impUnknown: # try an alternative: a <= b iff not (b < a) iff not (b+1 <= a): - let y = canon(m.o.opLe.buildCall(m.o.opAdd.buildCall(b, one()), a), m.o) + let y = canon(m.g.operators.opLe.buildCall(m.g.operators.opAdd.buildCall(b, one()), a), m.g.operators) result = ~ple(m, y[1], y[2]) proc addFactLe*(m: var TModel; a, b: PNode) = - m.s.add canon(m.o.opLe.buildCall(a, b), m.o) + m.s.add canon(m.g.operators.opLe.buildCall(a, b), m.g.operators) + +proc addFactLt*(m: var TModel; a, b: PNode) = + let bb = m.g.operators.opAdd.buildCall(b, minusOne()) + addFactLe(m, a, bb) proc settype(n: PNode): PType = - result = newType(tySet, n.typ.owner) - addSonSkipIntLit(result, n.typ) + var idgen = idGeneratorForPackage(-1'i32) + result = newType(tySet, idgen, n.typ.owner) + addSonSkipIntLit(result, n.typ, idgen) proc buildOf(it, loc: PNode; o: Operators): PNode = var s = newNodeI(nkCurly, it.info, it.len-1) @@ -992,14 +1126,14 @@ proc buildElse(n: PNode; o: Operators): PNode = proc addDiscriminantFact*(m: var TModel, n: PNode) = var fact = newNodeI(nkCall, n.info, 3) - fact[0] = newSymNode(m.o.opEq) + fact[0] = newSymNode(m.g.operators.opEq) fact[1] = n[0] fact[2] = n[1] m.s.add fact proc addAsgnFact*(m: var TModel, key, value: PNode) = var fact = newNodeI(nkCall, key.info, 3) - fact[0] = newSymNode(m.o.opEq) + fact[0] = newSymNode(m.g.operators.opEq) fact[1] = key fact[2] = value m.s.add fact @@ -1015,7 +1149,7 @@ proc sameSubexprs*(m: TModel; a, b: PNode): bool = # However, nil checking requires exactly the same mechanism! But for now # we simply use sameTree and live with the unsoundness of the analysis. var check = newNodeI(nkCall, a.info, 3) - check[0] = newSymNode(m.o.opEq) + check[0] = newSymNode(m.g.operators.opEq) check[1] = a check[2] = b result = m.doesImply(check) == impYes @@ -1023,9 +1157,9 @@ proc sameSubexprs*(m: TModel; a, b: PNode): bool = proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) = let branch = n[i] if branch.kind == nkOfBranch: - m.s.add buildOf(branch, n[0], m.o) + m.s.add buildOf(branch, n[0], m.g.operators) else: - m.s.add n.buildElse(m.o).neg(m.o) + m.s.add n.buildElse(m.g.operators).neg(m.g.operators) proc buildProperFieldCheck(access, check: PNode; o: Operators): PNode = if check[1].kind == nkCurly: @@ -1041,8 +1175,12 @@ proc buildProperFieldCheck(access, check: PNode; o: Operators): PNode = assert check.getMagic == mNot result = buildProperFieldCheck(access, check[1], o).neg(o) -proc checkFieldAccess*(m: TModel, n: PNode; conf: ConfigRef) = +proc checkFieldAccess*(m: TModel, n: PNode; conf: ConfigRef; produceError: bool) = for i in 1..<n.len: - let check = buildProperFieldCheck(n[0], n[i], m.o) + let check = buildProperFieldCheck(n[0], n[i], m.g.operators) if check != nil and m.doesImply(check) != impYes: - message(conf, n.info, warnProveField, renderTree(n[0])); break + if produceError: + localError(conf, n.info, "field access outside of valid case branch: " & renderTree(n[0])) + else: + message(conf, n.info, warnProveField, renderTree(n[0])) + break |