From a8f030fea21894e51c188a5804b0bbf787335f4d Mon Sep 17 00:00:00 2001 From: Andreas Rumpf Date: Sun, 19 Apr 2020 02:41:16 +0200 Subject: [PATCH] drnim: phi nodes for 'if' statements (#13990) --- drnim/drnim.nim | 164 +++++++++++++++++++++++++++++++++++++++---- drnim/tests/tphi.nim | 23 ++++++ 2 files changed, 172 insertions(+), 15 deletions(-) create mode 100644 drnim/tests/tphi.nim diff --git a/drnim/drnim.nim b/drnim/drnim.nim index 7c79add263..6c08bed426 100644 --- a/drnim/drnim.nim +++ b/drnim/drnim.nim @@ -65,11 +65,13 @@ type graph: ModuleGraph facts: seq[(PNode, VersionScope)] varVersions: seq[int] # this maps variable IDs to their current version. + varSyms: seq[PSym] # mirrors 'varVersions' o: Operators hasUnstructedCf: int currOptions: TOptions owner: PSym mangler: seq[PSym] + opImplies: PSym DrCon = object graph: ModuleGraph @@ -126,8 +128,17 @@ proc isLoc(m: PNode; assumeUniqueness: bool): bool = else: discard -proc varVersion(c: DrnimContext; s: PSym; begin: VersionScope): int = +proc currentVarVersion(c: DrnimContext; s: PSym; begin: VersionScope): int = + # we need to take into account both en- and disabled var bindings here, + # hence the 'abs' call: result = 0 + for i in countdown(int(begin)-1, 0): + if abs(c.varVersions[i]) == s.id: inc result + +proc previousVarVersion(c: DrnimContext; s: PSym; begin: VersionScope): int = + # we need to ignore currently disabled var bindings here, + # hence no 'abs' call here. + result = -1 for i in countdown(int(begin)-1, 0): if c.varVersions[i] == s.id: inc result @@ -156,15 +167,30 @@ proc stableName(result: var string; c: DrnimContext; n: PNode; version: VersionS if d != 0: result.add "`scope=" result.addInt d - let v = c.varVersion(n.sym, version) - ord(isOld) - assert v >= 0 + let v = if isOld: c.previousVarVersion(n.sym, version) + else: c.currentVarVersion(n.sym, version) if v > 0: result.add '`' result.addInt v else: result.add "`magic=" result.addInt ord(n.sym.magic) - + of nkBindStmt: + # we use 'bind x 3' to use the 3rd version of variable 'x'. This + # is easier than using 'old' which is position relative. + assert n.len == 2 + assert n[0].kind == nkSym + assert n[1].kind == nkIntLit + let s = n[0].sym + let v = int(n[1].intVal) + result.add s.name.s + let d = disamb(c, s) + if d != 0: + result.add "`scope=" + result.addInt d + if v > 0: + result.add '`' + result.addInt v of nkCharLit..nkUInt64Lit: result.addInt n.intVal of nkFloatLit..nkFloat64Lit: @@ -700,7 +726,8 @@ proc compatibleProps(graph: ModuleGraph; formal, actual: PType): bool {.nimcall. c.graph = graph c.canonParameterNames = true try: - c.up = DrnimContext(z3: setupZ3(), o: initOperators(graph), graph: graph, owner: nil) + c.up = DrnimContext(z3: setupZ3(), o: initOperators(graph), graph: graph, owner: nil, + opImplies: createMagic(graph, "->", mImplies)) template zero: untyped = VersionScope(0) if not frequires.isEmpty: result = not arequires.isEmpty and proofEngineAux(c, @[(frequires, zero)], (arequires, zero))[0] @@ -721,14 +748,22 @@ template config(c: typed): untyped = c.graph.config proc addFact(c: DrnimContext; n: PNode) = let v = c.currentScope if n[0].kind == nkSym and n[0].sym.magic in {mOr, mAnd}: - c.facts.add((n[1], v)) + c.addFact(n[1]) c.facts.add((n, v)) +proc neg(c: DrnimContext; n: PNode): PNode = + result = newNodeI(nkCall, n.info, 2) + result[0] = newSymNode(c.o.opNot) + result[1] = n + proc addFactNeg(c: DrnimContext; n: PNode) = - var neg = newNodeI(nkCall, n.info, 2) - neg[0] = newSymNode(c.o.opNot) - neg[1] = n - addFact(c, neg) + addFact(c, neg(c, n)) + +proc combineFacts(c: DrnimContext; a, b: PNode): PNode = + if a == nil: + result = b + else: + result = buildCall(c.o.opAnd, a, b) proc prove(c: DrnimContext; prop: PNode): bool = let (success, m) = proofEngine(c, c.facts, (prop, c.currentScope)) @@ -745,6 +780,8 @@ proc traversePragmaStmt(c: DrnimContext, n: PNode) = elif pragma == wInvariant or pragma == wAssert: if prove(c, it[1]): addFact(c, it[1]) + else: + echoFacts(c) proc requiresCheck(c: DrnimContext, call: PNode; op: PType) = assert op.n[0].kind == nkEffectList @@ -761,6 +798,7 @@ proc freshVersion(c: DrnimContext; arg: PNode) = let v = getRoot(arg) if v != nil: c.varVersions.add v.id + c.varSyms.add v proc translateEnsuresFromCall(c: DrnimContext, e, call: PNode): PNode = if e.kind in nkCallKinds and e[0].kind == nkSym and e[0].sym.magic == mOld: @@ -837,23 +875,118 @@ proc traverseCase(c: DrnimContext; n: PNode) = # XXX make this as smart as 'if elif' setLen(c.facts, oldFacts) +proc disableVarVersions(c: DrnimContext; until: int) = + for i in until.. (x'3 == x'1)) and + ((not a and b) -> (x'3 == x'2)) and + ((not a and not b) -> (x'3 == x'0)) + + (Where ``->`` is the logical implication.) + + In addition to the Phi information we also know the 'facts' + computed by the branches, for example:: + + if a: + factA + elif b: + factB + else: + factC + + (a -> factA) and + ((not a and b) -> factB) and + ((not a and not b) -> factC) + + We can combine these two aspects by producing the following facts + after each branch:: + + var x = y # x'0 + if a: + inc x # x'1 == x'0 + 1 + # also: x'1 == x'final + elif b: + inc x, 2 # x'2 == x'0 + 2 + # also: x'2 == x'final + else: + # also: x'0 == x'final + + ]# let oldFacts = c.facts.len - addFact(c, n[0][0]) + let oldVars = c.varVersions.len + var newFacts: seq[PNode] + var branches = newSeq[(PNode, int)](n.len) # (cond, newVars) pairs + template condVersion(): untyped = VersionScope(oldVars) - traverse(c, n[0][1]) - - for i in 1.. 1: addFact(c, branch[0]) + cond = combineFacts(c, cond, branch[0]) + for i in 0..", mImplies) try: traverse(c, n) ensuresCheck(c, owner) diff --git a/drnim/tests/tphi.nim b/drnim/tests/tphi.nim new file mode 100644 index 0000000000..7ff49f4dc5 --- /dev/null +++ b/drnim/tests/tphi.nim @@ -0,0 +1,23 @@ +discard """ + nimout: '''tphi.nim(9, 10) Warning: BEGIN [User] +tphi.nim(22, 10) Warning: END [User]''' + cmd: "drnim $file" + action: "compile" +""" +import std/logic +{.push staticBoundChecks: defined(nimDrNim).} +{.warning: "BEGIN".} + +proc testAsgn(y: int) = + var a = y + if a > 0: + if a > 3: + a = a + 2 + else: + a = a + 1 + {.assert: a > 1.} + +testAsgn(3) + +{.warning: "END".} +{.pop.}