contracts: fixes and tests assignments (#833)

* fixes and tests assignments
* contracts: proper IR traversals

Author: Araq

src/nimony/contracts.nim

@@ -32,7 +32,8 @@ type
     indegree, touched: int
     indegreeFacts: Facts
   Context = object
-    cf, dest: TokenBuf
+    cf, dest, toplevelStmts: TokenBuf
+    routines: seq[Cursor]
     typeCache: TypeCache
     facts: Facts
     writesTo: seq[SymId]
@@ -123,9 +124,11 @@ proc compileCmp(c: var Context; paramMap: Table[SymId, int]; req, call: Cursor):
     b = mapSymbol(c, paramMap, call, r.symId)
     inc r
   elif r.kind == IntLit:
+    b = VarId(0)
     cnst = createXint(pool.integers[r.intId])
     inc r
   elif r.kind == UIntLit:
+    b = VarId(0)
     cnst = createXint(pool.uintegers[r.uintId])
     inc r
   elif (let op = r.exprKind; op in {AddX, SubX}):
@@ -300,10 +303,12 @@ proc rightHandSide(c: var Context; pc: var Cursor; fact: var LeXplusC): bool =
     result = true
     inc pc
   elif pc.kind == IntLit:
+    fact.b = VarId(0)
     fact.c = fact.c + createXint(pool.integers[pc.intId])
     result = true
     inc pc
   elif pc.kind == UIntLit:
+    fact.b = VarId(0)
     fact.c = fact.c + createXint(pool.uintegers[pc.uintId])
     result = true
     inc pc
@@ -537,7 +542,7 @@ proc decAndTest(x: var int): bool {.inline.} =
   result = x == 0
 
 proc takeFacts(c: var Context; bb: var BasicBlock; conditionalFacts: int; negate: bool) =
-  let start = bb.indegreeFacts.len
+  #let start = bb.indegreeFacts.len
   if bb.touched == 0:
     for i in 1 ..< c.facts.len - conditionalFacts:
       bb.indegreeFacts.add c.facts[i]
@@ -557,10 +562,20 @@ proc pushFacts(c: var Context; bb: var BasicBlock) =
   for i in 0 ..< bb.indegreeFacts.len:
     c.facts.add bb.indegreeFacts[i]
 
-proc checkContracts(c: var Context) =
-  var bbs = computeBasicBlocks(c.cf)
+proc checkContracts(c: var Context; n: Cursor) =
+  c.cf = toControlflow(n)
+  c.facts = createFacts()
+  freeze c.cf
+  #echo "CF IS ", codeListing(c.cf)
+
   c.startInstr = readonlyCursorAt(c.cf, 0)
-  var current = BasicBlockIdx(0)
+  var body = c.startInstr
+  if body.stmtKind in {ProcS, FuncS, IteratorS, ConverterS, MethodS, MacroS}:
+    inc body
+    for i in 0 ..< BodyPos: skip body
+
+  var current = BasicBlockIdx(cursorToPosition(c.cf, body))
+  var bbs = computeBasicBlocks(c.cf, current.int)
   var nextIter = true
   var candidates = newSeq[BasicBlockIdx]()
   while nextIter or candidates.len > 0:
@@ -588,17 +603,68 @@ proc checkContracts(c: var Context) =
         else:
           candidates.add cont.elsePart
 
+proc traverseProc(c: var Context; n: var Cursor) =
+  let orig = n
+  let r = takeRoutine(n, SkipExclBody)
+  skip n # effects
+  if not isGeneric(r):
+    c.routines.add orig
+    var nested = 0
+    while true:
+      # don't forget about inner procs:
+      let sk = n.stmtKind
+      if sk in {ProcS, FuncS, IteratorS, ConverterS, MethodS}:
+        traverseProc(c, n)
+      elif sk in {MacroS, TemplateS, TypeS, CommentS, PragmasS}:
+        skip n
+      elif n.kind == ParLe:
+        inc nested
+        inc n
+      elif n.kind == ParRi:
+        dec nested
+        inc n
+        if nested == 0: break
+      else:
+        inc n
+    skipParRi n
+  else:
+    skip n # body
+    skipParRi n
+
+proc traverseToplevel(c: var Context; n: var Cursor) =
+  case n.stmtKind
+  of StmtsS:
+    c.toplevelStmts.add n
+    inc n
+    while n.kind != ParRi:
+      traverseToplevel(c, n)
+    c.toplevelStmts.add n
+    skipParRi n
+  of ProcS, FuncS, IteratorS, ConverterS, MethodS:
+    traverseProc(c, n)
+  of MacroS, TemplateS, TypeS, CommentS, PragmasS,
+     ImportasS, ExportexceptS, BindS, MixinS, UsingS,
+     ExportS,
+     IncludeS, ImportS, FromimportS, ImportExceptS:
+    skip n
+  of IfS, WhenS, WhileS, ForS, CaseS, TryS, YldS, RaiseS,
+     UnpackDeclS, StaticstmtS, AsmS, DeferS,
+     CallS, CmdS, GvarS, TvarS, VarS, ConstS, ResultS,
+     GletS, TletS, LetS, CursorS, BlockS, EmitS, AsgnS, ScopeS,
+     BreakS, ContinueS, RetS, InclS, ExclS, DiscardS, AssumeS, AssertS, NoStmt:
+    c.toplevelStmts.takeTree n
+
 proc analyzeContracts*(input: var TokenBuf): TokenBuf =
   let oldInfos = prepare(input)
   var c = Context(typeCache: createTypeCache(),
-    dest: createTokenBuf(500),
-    cf: toControlflow(beginRead input),
-    facts: createFacts())
-  freeze c.cf
-  #echo "CF IS ", codeListing(c.cf)
+    dest: createTokenBuf(500))
   c.typeCache.openScope()
-
-  checkContracts(c)
+  var n = beginRead(input)
+  traverseToplevel c, n
+  for r in c.routines:
+    checkContracts(c, r)
+  var nt = beginRead c.toplevelStmts
+  checkContracts(c, nt)
 
   endRead input
   restore(input, oldInfos)

src/nimony/controlflow.nim

@@ -810,15 +810,19 @@ proc trExpr(c: var ControlFlow; n: var Cursor) =
 
 proc toControlflow*(n: Cursor): TokenBuf =
   var c = ControlFlow(typeCache: createTypeCache())
-  assert n.stmtKind == StmtsS
   c.typeCache.openScope()
+  let sk = n.stmtKind
   var n = n
-  c.dest.add n
-  inc n
-  while n.kind != ParRi:
-    trStmt c, n
-  c.dest.addParPair RetS, NoLineInfo
-  c.dest.addParRi()
+  if sk in {ProcS, FuncS, IteratorS, ConverterS, MethodS, MacroS}:
+    trProc c, n
+  else:
+    assert sk == StmtsS
+    c.dest.add n
+    inc n
+    while n.kind != ParRi:
+      trStmt c, n
+    c.dest.addParPair RetS, NoLineInfo
+    c.dest.addParRi()
   c.typeCache.closeScope()
   result = ensureMove c.dest
   #echo "result: ", codeListing(result)

src/nimony/inferle.nim

@@ -185,7 +185,7 @@ proc implies*(facts: Facts; v: LeXplusC): bool =
 
 proc merge*(x: Facts; xstart: int; y: Facts; negate: bool): Facts =
   # computes thing we know on a joint point.
-  # we know that `a <= b + c` and `a <= b + d` then we know
+  # we know that `a <= b + c` or `a <= b + d` then we know
   # that `a <= b + max(c, d)`
   result = Facts()
   for i in 0 ..< xstart:

tests/contracts/tasgn.msgs

@@ -0,0 +1 @@
+OK 0 <= v3 + -0

tests/contracts/tasgn.nif

@@ -0,0 +1,14 @@
+(stmts
+  (proc :my.proc . . . (params (param :cond.0 . . (bool) .)) . . . (stmts
+    (var :x.0 . . (i +32) .)
+    (if
+      (elif (cond.0) (stmts
+        (asgn x.0 +12)
+      ))
+      (else (stmts
+        (asgn x.0 +14)
+      ))
+    )
+    (assert (out) (le . +0 x.0))
+  ))
+)