diff options
| -rw-r--r-- | drnim/drnim.nim | 164 | ||||
| -rw-r--r-- | drnim/tests/tphi.nim | 23 |
2 files changed, 172 insertions, 15 deletions
diff --git a/drnim/drnim.nim b/drnim/drnim.nim index 7c79add26..6c08bed42 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,9 +128,18 @@ 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 proc disamb(c: DrnimContext; s: PSym): int = @@ -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..<c.varVersions.len: + c.varVersions[i] = - abs(c.varVersions[i]) + +proc varOfVersion(c: DrnimContext; x: PSym; scope: int): PNode = + let version = currentVarVersion(c, x, VersionScope(scope)) + result = newTree(nkBindStmt, newSymNode(x), newIntNode(nkIntLit, version)) + proc traverseIf(c: DrnimContext; n: PNode) = - traverse(c, n[0][0]) - let oldFacts = c.facts.len - addFact(c, n[0][0]) + #[ Consider this example:: + + var x = y # x'0 + if a: + inc x # x'1 == x'0 + 1 + elif b: + inc x, 2 # x'2 == x'0 + 2 + + afterwards we know this is fact:: + + x'3 = Phi(x'0, x'1, x'2) + + So a Phi node from SSA representation is an 'or' formula like:: + + x'3 == x'1 or x'3 == x'2 or x'3 == x'0 - traverse(c, n[0][1]) + However, this loses some information. The formula that doesn't + lose information is:: - for i in 1..<n.len: + (a -> (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 + let oldVars = c.varVersions.len + var newFacts: seq[PNode] + var branches = newSeq[(PNode, int)](n.len) # (cond, newVars) pairs + template condVersion(): untyped = VersionScope(oldVars) + + for i in 0..<n.len: let branch = n[i] setLen(c.facts, oldFacts) + + var cond = PNode(nil) for j in 0..i-1: addFactNeg(c, n[j][0]) + cond = combineFacts(c, cond, neg(c, n[j][0])) if branch.len > 1: addFact(c, branch[0]) + cond = combineFacts(c, cond, branch[0]) + for i in 0..<branch.len: traverse(c, branch[i]) + + assert cond != nil + branches[i] = (cond, c.varVersions.len) + + var newInfo = PNode(nil) + for f in oldFacts..<c.facts.len: + newInfo = combineFacts(c, newInfo, c.facts[f][0]) + if newInfo != nil: + newFacts.add buildCall(c.opImplies, cond, newInfo) + + disableVarVersions(c, oldVars) + setLen(c.facts, oldFacts) + for f in newFacts: c.facts.add((f, condVersion)) + # build the 'Phi' information: + let varsWithoutFinals = c.varVersions.len + var mutatedVars = initIntSet() + for i in oldVars ..< varsWithoutFinals: + let vv = c.varVersions[i] + if not mutatedVars.containsOrIncl(vv): + c.varVersions.add vv + c.varSyms.add c.varSyms[i] + + var prevIdx = oldVars + for i in 0 ..< branches.len: + for v in prevIdx .. branches[i][1] - 1: + c.facts.add((buildCall(c.opImplies, branches[i][0], + buildCall(c.o.opEq, varOfVersion(c, c.varSyms[v], branches[i][1]), newSymNode(c.varSyms[v]))), + condVersion)) + prevIdx = branches[i][1] proc traverseBlock(c: DrnimContext; n: PNode) = traverse(c, n) @@ -1028,6 +1161,7 @@ proc strongSemCheck(graph: ModuleGraph; owner: PSym; n: PNode) = c.o = initOperators(graph) c.graph = graph c.owner = owner + c.opImplies = createMagic(c.graph, "->", 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 000000000..7ff49f4dc --- /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.} |