drnim: phi nodes for 'if' statements (#13990)

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..<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])
+  #[ 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
+
+  However, this loses some information. The formula that doesn't
+  lose information is::
+
+    (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
-  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..<n.len:
+  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)

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.}