DrNim (Nim compiler with Z3 integration) (#13743)

* code cleanups and feature additions * added basic test and koch/CI integration * make it build on Unix * DrNim: now buildable on Unix, only takes 10 minutes, enjoy * added basic documentation for DrNim which can also be seen as the RFC we're following * drnim: change the build setup so that drnim.exe ends up in bin/ * makes simple floating point ranges work * added basic float range check * drnim: teach Z3 about Nim's range types plus code refactoring * drnim: make unsigned numbers work * added and fixed index checking under setLen * first implementation of .ensures, .invariant and .assume (.requires still missing and so is proc type compatibility checking * drnim: .requires checking implemented * drnim: implemented .ensures properly * more impressive test involving min() * drnim: check for proc type compatibility and base method compatibility wrt .requires and .ensures * testament: support for 'pattern <directory> * koch: uses new <directory> feature of testament * drnim: added tiny musings about 'old' * Make testament work with old SSL versions * koch: add support for 'koch drnim -d:release' * drnim: preparations for the param.old notation
2025-12-28 17:04:41 +00:00 · 2020-03-31 22:54:48 +02:00
parent dd44701728
commit 9ffec79300
25 changed files with 1242 additions and 35 deletions
--- a/compiler/ast.nim
+++ b/compiler/ast.nim
@@ -335,8 +335,8 @@ const
  nkEffectList* = nkArgList
  # hacks ahead: an nkEffectList is a node with 4 children:
  exceptionEffects* = 0 # exceptions at position 0
-  usesEffects* = 1      # read effects at position 1
-  writeEffects* = 2     # write effects at position 2
+  requiresEffects* = 1      # 'requires' annotation
+  ensuresEffects* = 2     # 'ensures' annotation
  tagEffects* = 3       # user defined tag ('gc', 'time' etc.)
  pragmasEffects* = 4    # not an effect, but a slot for pragmas in proc type
  effectListLen* = 5    # list of effects list
@@ -633,6 +633,7 @@ type
    mCharToStr, mBoolToStr, mIntToStr, mInt64ToStr, mFloatToStr, mCStrToStr,
    mStrToStr, mEnumToStr,
    mAnd, mOr,
+    mImplies, mIff, mExists, mForall, mOld,
    mEqStr, mLeStr, mLtStr,
    mEqSet, mLeSet, mLtSet, mMulSet, mPlusSet, mMinusSet,
    mConStrStr, mSlice,
--- a/compiler/condsyms.nim
+++ b/compiler/condsyms.nim
@@ -114,4 +114,5 @@ proc initDefines*(symbols: StringTableRef) =

  defineSymbol("nimHasSinkInference")
  defineSymbol("nimNewIntegerOps")
+  defineSymbol("nimHasInvariant")
  defineSymbol("nimHasStacktraceMsgs")
--- a/compiler/guards.nim
+++ b/compiler/guards.nim
@@ -249,6 +249,9 @@ 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 =
  if n.safeLen >= 1:
    result = shallowCopy(n)
--- a/compiler/modulegraphs.nim
+++ b/compiler/modulegraphs.nim
@@ -72,6 +72,10 @@ type
    onDefinitionResolveForward*: proc (graph: ModuleGraph; s: PSym; info: TLineInfo) {.nimcall.}
    onUsage*: proc (graph: ModuleGraph; s: PSym; info: TLineInfo) {.nimcall.}
    globalDestructors*: seq[PNode]
+    proofEngine*: proc (graph: ModuleGraph; assumptions: seq[PNode]; toProve: PNode): (bool, string) {.nimcall.}
+    requirementsCheck*: proc (graph: ModuleGraph; assumptions: seq[PNode];
+                             call, requirement: PNode): (bool, string) {.nimcall.}
+    compatibleProps*: proc (graph: ModuleGraph; formal, actual: PType): bool {.nimcall.}

  TPassContext* = object of RootObj # the pass's context
  PPassContext* = ref TPassContext
--- a/compiler/pragmas.nim
+++ b/compiler/pragmas.nim
@@ -28,7 +28,8 @@ const
    wBorrow, wImportCompilerProc, wThread,
    wAsmNoStackFrame, wDiscardable, wNoInit, wCodegenDecl,
    wGensym, wInject, wRaises, wTags, wLocks, wDelegator, wGcSafe,
-    wConstructor, wLiftLocals, wStackTrace, wLineTrace, wNoDestroy}
+    wConstructor, wLiftLocals, wStackTrace, wLineTrace, wNoDestroy,
+    wRequires, wEnsures}
  converterPragmas* = procPragmas
  methodPragmas* = procPragmas+{wBase}-{wImportCpp}
  templatePragmas* = {wDeprecated, wError, wGensym, wInject, wDirty,
@@ -39,7 +40,7 @@ const
  iteratorPragmas* = declPragmas + {FirstCallConv..LastCallConv, wNoSideEffect, wSideEffect,
    wMagic, wBorrow,
    wDiscardable, wGensym, wInject, wRaises,
-    wTags, wLocks, wGcSafe}
+    wTags, wLocks, wGcSafe, wRequires, wEnsures}
  exprPragmas* = {wLine, wLocks, wNoRewrite, wGcSafe, wNoSideEffect}
  stmtPragmas* = {wChecks, wObjChecks, wFieldChecks, wRangeChecks,
    wBoundChecks, wOverflowChecks, wNilChecks, wStaticBoundchecks,
@@ -52,11 +53,12 @@ const
    wDeprecated,
    wFloatChecks, wInfChecks, wNanChecks, wPragma, wEmit, wUnroll,
    wLinearScanEnd, wPatterns, wTrMacros, wEffects, wNoForward, wReorder, wComputedGoto,
-    wInjectStmt, wExperimental, wThis, wUsed}
+    wInjectStmt, wExperimental, wThis, wUsed, wInvariant, wAssume}
  lambdaPragmas* = declPragmas + {FirstCallConv..LastCallConv,
    wNoSideEffect, wSideEffect, wNoreturn, wNosinks, wDynlib, wHeader,
    wThread, wAsmNoStackFrame,
-    wRaises, wLocks, wTags, wGcSafe, wCodegenDecl} - {wExportNims, wError, wUsed}  # why exclude these?
+    wRaises, wLocks, wTags, wRequires, wEnsures,
+    wGcSafe, wCodegenDecl} - {wExportNims, wError, wUsed}  # why exclude these?
  typePragmas* = declPragmas + {wMagic, wAcyclic,
    wPure, wHeader, wCompilerProc, wCore, wFinal, wSize, wShallow,
    wIncompleteStruct, wByCopy, wByRef,
@@ -73,7 +75,8 @@ const
    wIntDefine, wStrDefine, wBoolDefine, wCompilerProc, wCore}
  letPragmas* = varPragmas
  procTypePragmas* = {FirstCallConv..LastCallConv, wVarargs, wNoSideEffect,
-                      wThread, wRaises, wLocks, wTags, wGcSafe}
+                      wThread, wRaises, wLocks, wTags, wGcSafe,
+                      wRequires, wEnsures}
  forVarPragmas* = {wInject, wGensym}
  allRoutinePragmas* = methodPragmas + iteratorPragmas + lambdaPragmas
  enumFieldPragmas* = {wDeprecated}
@@ -105,6 +108,26 @@ proc invalidPragma*(c: PContext; n: PNode) =
 proc illegalCustomPragma*(c: PContext, n: PNode, s: PSym) =
  localError(c.config, n.info, "cannot attach a custom pragma to '" & s.name.s & "'")

+proc pragmaProposition(c: PContext, n: PNode) =
+  if n.kind notin nkPragmaCallKinds or n.len != 2:
+    localError(c.config, n.info, "proposition expected")
+  else:
+    n[1] = c.semExpr(c, n[1])
+
+proc pragmaEnsures(c: PContext, n: PNode) =
+  if n.kind notin nkPragmaCallKinds or n.len != 2:
+    localError(c.config, n.info, "proposition expected")
+  else:
+    openScope(c)
+    let o = getCurrOwner(c)
+    if o.kind in routineKinds and o.typ != nil and o.typ.sons[0] != nil:
+      var s = newSym(skResult, getIdent(c.cache, "result"), o, n.info)
+      s.typ = o.typ.sons[0]
+      incl(s.flags, sfUsed)
+      addDecl(c, s)
+    n[1] = c.semExpr(c, n[1])
+    closeScope(c)
+
 proc pragmaAsm*(c: PContext, n: PNode): char =
  result = '\0'
  if n != nil:
@@ -1146,6 +1169,10 @@ proc singlePragma(c: PContext, sym: PSym, n: PNode, i: var int,
        if sym == nil: invalidPragma(c, it)
        else: sym.flags.incl sfUsed
      of wLiftLocals: discard
+      of wRequires, wInvariant, wAssume:
+        pragmaProposition(c, it)
+      of wEnsures:
+        pragmaEnsures(c, it)
      else: invalidPragma(c, it)
    elif comesFromPush and whichKeyword(ident) != wInvalid:
      discard "ignore the .push pragma; it doesn't apply"
--- a/compiler/semcall.nim
+++ b/compiler/semcall.nim
@@ -128,7 +128,7 @@ proc pickBestCandidate(c: PContext, headSymbol: PNode,
    else:
      break

-proc effectProblem(f, a: PType; result: var string) =
+proc effectProblem(f, a: PType; result: var string; c: PContext) =
  if f.kind == tyProc and a.kind == tyProc:
    if tfThread in f.flags and tfThread notin a.flags:
      result.add "\n  This expression is not GC-safe. Annotate the " &
@@ -152,7 +152,9 @@ proc effectProblem(f, a: PType; result: var string) =
      of efLockLevelsDiffer:
        result.add "\n  The `.locks` requirements differ. Annotate the " &
            "proc with {.locks: 0.} to get extended error information."
-
+      when defined(drnim):
+        if not c.graph.compatibleProps(c.graph, f, a):
+          result.add "\n  The `.requires` or `.ensures` properties are incompatible."

 proc renderNotLValue(n: PNode): string =
  result = $n
@@ -238,7 +240,7 @@ proc presentFailedCandidates(c: PContext, n: PNode, errors: CandidateErrors):
          var got = nArg.typ
          candidates.add typeToString(got)
          doAssert wanted != nil
-          if got != nil: effectProblem(wanted, got, candidates)
+          if got != nil: effectProblem(wanted, got, candidates, c)
      of kUnknown: discard "do not break 'nim check'"
      candidates.add "\n"
      if err.firstMismatch.arg == 1 and nArg.kind == nkTupleConstr and
--- a/compiler/semmagic.nim
+++ b/compiler/semmagic.nim
@@ -428,6 +428,27 @@ proc turnFinalizerIntoDestructor(c: PContext; orig: PSym; info: TLineInfo): PSym
  result.typ = newProcType(result.info, result)
  result.typ.addParam newParam

+proc semQuantifier(c: PContext; n: PNode): PNode =
+  checkMinSonsLen(n, 2, c.config)
+  openScope(c)
+  for i in 0..n.len-2:
+    let v = newSymS(skForVar, n[i], c)
+    styleCheckDef(c.config, v)
+    onDef(n.info, v)
+    n[i] = newSymNode(v)
+    addDecl(c, v)
+  n[^1] = forceBool(c, semExprWithType(c, n[^1]))
+  closeScope(c)
+
+proc semOld(c: PContext; n: PNode): PNode =
+  if n[1].kind == nkHiddenDeref:
+    n[1] = n[1][0]
+  if n[1].kind != nkSym or n[1].sym.kind != skParam:
+    localError(c.config, n[1].info, "'old' takes a parameter name")
+  elif n[1].sym.owner != getCurrOwner(c):
+    localError(c.config, n[1].info, n[1].sym.name.s & " does not belong to " & getCurrOwner(c).name.s)
+  result = n
+
 proc magicsAfterOverloadResolution(c: PContext, n: PNode,
                                   flags: TExprFlags): PNode =
  ## This is the preferred code point to implement magics.
@@ -505,4 +526,8 @@ proc magicsAfterOverloadResolution(c: PContext, n: PNode,
      result[0] = newSymNode(t.destructor)
  of mUnown:
    result = semUnown(c, n)
+  of mExists, mForall:
+    result = semQuantifier(c, n)
+  of mOld:
+    result = semOld(c, n)
  else: result = n
--- a/compiler/sempass2.nim
+++ b/compiler/sempass2.nim
@@ -565,6 +565,7 @@ proc trackOperand(tracked: PEffects, n: PNode, paramType: PType; caller: PNode)
      elif tfNoSideEffect notin op.flags:
        markSideEffect(tracked, a)
  if paramType != nil and paramType.kind == tyVar:
+    invalidateFacts(tracked.guards, n)
    if n.kind == nkSym and isLocalVar(tracked, n.sym):
      makeVolatile(tracked, n.sym)
  if paramType != nil and paramType.kind == tyProc and tfGcSafe in paramType.flags:
@@ -675,28 +676,75 @@ proc cstringCheck(tracked: PEffects; n: PNode) =
      a.typ.kind == tyString and a.kind notin {nkStrLit..nkTripleStrLit}):
    message(tracked.config, n.info, warnUnsafeCode, renderTree(n))

+proc prove(c: PEffects; prop: PNode): bool =
+  if c.graph.proofEngine != nil:
+    let (success, m) = c.graph.proofEngine(c.graph, c.guards.s,
+      canon(prop, c.guards.o))
+    if not success:
+      message(c.config, prop.info, warnStaticIndexCheck, "cannot prove: " & $prop & m)
+    result = success
+
+proc patchResult(c: PEffects; n: PNode) =
+  if n.kind == nkSym and n.sym.kind == skResult:
+    let fn = c.owner
+    if fn != nil and fn.kind in routineKinds and fn.ast != nil and resultPos < fn.ast.len:
+      n.sym = fn.ast[resultPos].sym
+    else:
+      localError(c.config, n.info, "routine has no return type, but .requires contains 'result'")
+  else:
+    for i in 0..<safeLen(n):
+      patchResult(c, n[i])
+
+when defined(drnim):
+  proc requiresCheck(c: PEffects; call: PNode; op: PType) =
+    assert op.n[0].kind == nkEffectList
+    if requiresEffects < op.n[0].len:
+      let requires = op.n[0][requiresEffects]
+      if requires != nil and requires.kind != nkEmpty:
+        # we need to map the call arguments to the formal parameters used inside
+        # 'requires':
+        let (success, m) = c.graph.requirementsCheck(c.graph, c.guards.s, call, canon(requires, c.guards.o))
+        if not success:
+          message(c.config, call.info, warnStaticIndexCheck, "cannot prove: " & $requires & m)
+
+else:
+  template requiresCheck(c, n, op) = discard
+
 proc checkLe(c: PEffects; a, b: PNode) =
-  case proveLe(c.guards, a, b)
-  of impUnknown:
-    #for g in c.guards.s:
-    #  if g != nil: echo "I Know ", g
-    message(c.config, a.info, warnStaticIndexCheck,
-      "cannot prove: " & $a & " <= " & $b)
-  of impYes:
-    discard
-  of impNo:
-    message(c.config, a.info, warnStaticIndexCheck,
-      "can prove: " & $a & " > " & $b)
+  if c.graph.proofEngine != nil:
+    var cmpOp = mLeI
+    if a.typ != nil:
+      case a.typ.skipTypes(abstractInst).kind
+      of tyFloat..tyFloat128: cmpOp = mLeF64
+      of tyChar, tyUInt..tyUInt64: cmpOp = mLeU
+      else: discard
+
+    let cmp = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), a, b)
+    cmp.info = a.info
+    discard prove(c, cmp)
+  else:
+    case proveLe(c.guards, a, b)
+    of impUnknown:
+      #for g in c.guards.s:
+      #  if g != nil: echo "I Know ", g
+      message(c.config, a.info, warnStaticIndexCheck,
+        "cannot prove: " & $a & " <= " & $b)
+    of impYes:
+      discard
+    of impNo:
+      message(c.config, a.info, warnStaticIndexCheck,
+        "can prove: " & $a & " > " & $b)

 proc checkBounds(c: PEffects; arr, idx: PNode) =
  checkLe(c, lowBound(c.config, arr), idx)
  checkLe(c, idx, highBound(c.config, arr, c.guards.o))

 proc checkRange(c: PEffects; value: PNode; typ: PType) =
-  if typ.skipTypes(abstractInst - {tyRange}).kind == tyRange:
-    let lowBound = nkIntLit.newIntNode(firstOrd(c.config, typ))
+  let t = typ.skipTypes(abstractInst - {tyRange})
+  if t.kind == tyRange:
+    let lowBound = copyTree(t.n[0])
    lowBound.info = value.info
-    let highBound = nkIntLit.newIntNode(lastOrd(c.config, typ))
+    let highBound = copyTree(t.n[1])
    highBound.info = value.info
    checkLe(c, lowBound, value)
    checkLe(c, value, highBound)
@@ -783,6 +831,7 @@ proc track(tracked: PEffects, n: PNode) =
        mergeEffects(tracked, effectList[exceptionEffects], n)
        mergeTags(tracked, effectList[tagEffects], n)
        gcsafeAndSideeffectCheck()
+      requiresCheck(tracked, n, op)
    if a.kind != nkSym or a.sym.magic != mNBindSym:
      for i in 1..<n.len: trackOperand(tracked, n[i], paramType(op, i), a)
    if a.kind == nkSym and a.sym.magic in {mNew, mNewFinalize, mNewSeq}:
@@ -976,6 +1025,13 @@ proc track(tracked: PEffects, n: PNode) =
        enforcedGcSafety = true
      elif pragma == wNoSideEffect:
        enforceNoSideEffects = true
+      when defined(drnim):
+        if pragma == wAssume:
+          addFact(tracked.guards, pragmaList[i][1])
+        elif pragma == wInvariant:
+          if prove(tracked, pragmaList[i][1]):
+            addFact(tracked.guards, pragmaList[i][1])
+
    if enforcedGcSafety: tracked.inEnforcedGcSafe = true
    if enforceNoSideEffects: tracked.inEnforcedNoSideEffects = true
    track(tracked, n.lastSon)
@@ -1065,6 +1121,11 @@ proc checkMethodEffects*(g: ModuleGraph; disp, branch: PSym) =
  if sfThread in disp.flags and notGcSafe(branch.typ):
    localError(g.config, branch.info, "base method is GC-safe, but '$1' is not" %
                                branch.name.s)
+  when defined(drnim):
+    if not g.compatibleProps(g, disp.typ, branch.typ):
+      localError(g.config, branch.info, "for method '" & branch.name.s &
+        "' the `.requires` or `.ensures` properties are incompatible.")
+
  if branch.typ.lockLevel > disp.typ.lockLevel:
    when true:
      message(g.config, branch.info, warnLockLevel,
@@ -1088,14 +1149,22 @@ proc setEffectsForProcType*(g: ModuleGraph; t: PType, n: PNode) =
    let tagsSpec = effectSpec(n, wTags)
    if not isNil(tagsSpec):
      effects[tagEffects] = tagsSpec
+
+    let requiresSpec = propSpec(n, wRequires)
+    if not isNil(requiresSpec):
+      effects[requiresEffects] = requiresSpec
+    let ensuresSpec = propSpec(n, wEnsures)
+    if not isNil(ensuresSpec):
+      effects[ensuresEffects] = ensuresSpec
+
    effects[pragmasEffects] = n

 proc initEffects(g: ModuleGraph; effects: PNode; s: PSym; t: var TEffects; c: PContext) =
  newSeq(effects.sons, effectListLen)
  effects[exceptionEffects] = newNodeI(nkArgList, s.info)
  effects[tagEffects] = newNodeI(nkArgList, s.info)
-  effects[usesEffects] = g.emptyNode
-  effects[writeEffects] = g.emptyNode
+  effects[requiresEffects] = g.emptyNode
+  effects[ensuresEffects] = g.emptyNode
  effects[pragmasEffects] = g.emptyNode

  t.exc = effects[exceptionEffects]
@@ -1155,6 +1224,15 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) =
    # after the check, use the formal spec:
    effects[tagEffects] = tagsSpec

+  let requiresSpec = propSpec(p, wRequires)
+  if not isNil(requiresSpec):
+    effects[requiresEffects] = requiresSpec
+  let ensuresSpec = propSpec(p, wEnsures)
+  if not isNil(ensuresSpec):
+    patchResult(t, ensuresSpec)
+    effects[ensuresEffects] = ensuresSpec
+    discard prove(t, ensuresSpec)
+
  if sfThread in s.flags and t.gcUnsafe:
    if optThreads in g.config.globalOptions and optThreadAnalysis in g.config.globalOptions:
      #localError(s.info, "'$1' is not GC-safe" % s.name.s)
--- a/compiler/semstmts.nim
+++ b/compiler/semstmts.nim
@@ -1930,7 +1930,7 @@ proc semProcAux(c: PContext, n: PNode, kind: TSymKind,
    if n[pragmasPos].kind != nkEmpty:
      pragma(c, s, n[pragmasPos], validPragmas)
      # To ease macro generation that produce forwarded .async procs we now
-      # allow a bit redudancy in the pragma declarations. The rule is
+      # allow a bit redundancy in the pragma declarations. The rule is
      # a prototype's pragma list must be a superset of the current pragma
      # list.
      # XXX This needs more checks eventually, for example that external
--- a/compiler/sigmatch.nim
+++ b/compiler/sigmatch.nim
@@ -646,6 +646,8 @@ proc procTypeRel(c: var TCandidate, f, a: PType): TTypeRelation =
        return isNone
    when useEffectSystem:
      if compatibleEffects(f, a) != efCompat: return isNone
+    when defined(drnim):
+      if not c.c.graph.compatibleProps(c.c.graph, f, a): return isNone

  of tyNil:
    result = f.allowsNil
--- a/compiler/trees.nim
+++ b/compiler/trees.nim
@@ -148,6 +148,12 @@ proc effectSpec*(n: PNode, effectType: TSpecialWord): PNode =
        result.add(it[1])
      return

+proc propSpec*(n: PNode, effectType: TSpecialWord): PNode =
+  for i in 0..<n.len:
+    var it = n[i]
+    if it.kind == nkExprColonExpr and whichPragma(it) == effectType:
+      return it[1]
+
 proc unnestStmts(n, result: PNode) =
  if n.kind == nkStmtList:
    for x in items(n): unnestStmts(x, result)
--- a/compiler/wordrecg.nim
+++ b/compiler/wordrecg.nim
@@ -54,6 +54,7 @@ type
    wNonReloadable, wExecuteOnReload,
    wAssertions, wPatterns, wTrMacros, wSinkInference, wWarnings,
    wHints, wOptimization, wRaises, wWrites, wReads, wSize, wEffects, wTags,
+    wRequires, wEnsures, wInvariant, wAssume,
    wDeadCodeElimUnused,  # deprecated, dead code elim always happens
    wSafecode, wPackage, wNoForward, wReorder, wNoRewrite, wNoDestroy,
    wPragma,
@@ -142,6 +143,7 @@ const

    "assertions", "patterns", "trmacros", "sinkinference", "warnings", "hints",
    "optimization", "raises", "writes", "reads", "size", "effects", "tags",
+    "requires", "ensures", "invariant", "assume",
    "deadcodeelim",  # deprecated, dead code elim always happens
    "safecode", "package", "noforward", "reorder", "norewrite", "nodestroy",
    "pragma",
--- a/doc/drnim.rst
+++ b/doc/drnim.rst
@@ -0,0 +1,203 @@
+===================================
+   DrNim User Guide
+===================================
+
+:Author: Andreas Rumpf
+:Version: |nimversion|
+
+.. contents::
+
+
+Introduction
+============
+
+This document describes the usage of the *DrNim* tool. DrNim combines
+the Nim frontend with the `Z3 <https://github.com/Z3Prover/z3>`_ proof
+engine in order to allow verify / validate software written in Nim.
+DrNim's command line options are the same as the Nim compiler's.
+
+
+DrNim currently only checks the sections of your code that are marked
+via ``staticBoundChecks: on``:
+
+.. code-block:: nim
+
+  {.push staticBoundChecks: on.}
+  # <--- code section here ---->
+  {.pop.}
+
+DrNim currently only tries to prove array indexing or subrange checks,
+overflow errors are *not* prevented. Overflows will be checked for in
+the future.
+
+Later versions of the **Nim compiler** will **assume** that the checks inside
+the ``staticBoundChecks: on`` environment have been proven correct and so
+it will **omit** the runtime checks. If you do not want this behavior, use
+instead ``{.push staticBoundChecks: defined(nimDrNim).}``. This way the
+Nim compiler remains unaware of the performed proofs but DrNim will prove
+your code.
+
+
+Installation
+============
+
+Run ``koch drnim``, the executable will afterwards be in ``$nim/bin/drnim``.
+
+
+Motivating Example
+==================
+
+The follow example highlights what DrNim can easily do, even
+without additional annotations:
+
+.. code-block:: nim
+
+  {.push staticBoundChecks: on.}
+
+  proc sum(a: openArray[int]): int =
+    for i in 0..a.len:
+      result += a[i]
+
+  {.pop.}
+
+  echo sum([1, 2, 3])
+
+This program contains a famous "index out of bounds" bug. DrNim
+detects it and produces the following error message::
+
+  cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
+
+In other words for ``i == 0`` and ``a.len == 0`` (for example!) there would be
+an index out of bounds error.
+
+
+Pre-, postconditions and invariants
+===================================
+
+DrNim adds 4 additional annotations (pragmas) to Nim:
+
+- `requires`:idx:
+- `ensures`:idx:
+- `invariant`:idx:
+- `assume`:idx:
+
+These pragmas are ignored by the Nim compiler so that they don't have to
+be disabled via ``when defined(nimDrNim)``.
+
+
+Invariant
+---------
+
+An ``invariant`` is a proposition that must be true after every loop
+iteration, it's tied to the loop body it's part of.
+
+
+Requires
+--------
+
+A ``requires`` annotation describes what the function expects to be true
+before it's called so that it can perform its operation. A ``requires``
+annotation is also called a `precondition`:idx:.
+
+
+Ensures
+-------
+
+An ``ensures`` annotation describes what will be true after the function
+call. An ``ensures`` annotation is also called a `postcondition`:idx:.
+
+
+Assume
+------
+
+An ``assume`` annotation describes what DrNim should **assume** to be true
+in this section of the program. It is an unsafe escape mechanism comparable
+to Nim's ``cast`` statement. Use it only when you really know better
+than DrNim. You should add a comment to a paper that proves the proposition
+you assume.
+
+
+Example: insertionSort
+======================
+
+**Note**: This example does not yet work with DrNim. ``forall`` and ``exists``
+are not implemented.
+
+.. code-block:: nim
+
+  import std / logic
+
+  proc insertionSort(a: var openArray[int]) {.
+      ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
+
+    for k in 1 ..< a.len:
+      {.invariant: 1 <= k and k <= a.len.}
+      {.invariant: forall(j in 1..<k, i in 0..<j, a[i] <= a[j]).}
+      var t = k
+      while t > 0 and a[t-1] > a[t]:
+        {.invariant: k < a.len.}
+        {.invariant: 0 <= t and t <= k.}
+        {.invariant: forall(j in 1..k, i in 0..<j, j == t or a[i] <= a[j]).}
+        swap a[t], a[t-1]
+        dec t
+
+Unfortunately the invariants required to prove this code correct take more
+code than the imperative instructions. However this effort can be compensated
+by the fact that the result needs very little testing. Be aware though that
+DrNim only proves that after ``insertionSort`` this condition holds::
+
+  forall(i in 1..<a.len, a[i-1] <= a[i])
+
+
+This is required, but not sufficient to describe that a ``sort`` operation
+was performed. For example, the same postcondition is true for this proc
+which doesn't sort at all:
+
+.. code-block:: nim
+
+  import std / logic
+
+  proc insertionSort(a: var openArray[int]) {.
+      ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
+    # does not sort, overwrites `a`'s contents!
+    for i in 0..<a.len: a[i] = i
+
+
+
+Syntax of propositions
+======================
+
+The basic syntax is ``ensures|requires|invariant: <prop>``.
+A ``prop`` is either a comparison or a compound::
+
+  prop = nim_bool_expression
+       | prop 'and' prop
+       | prop 'or' prop
+       | prop '->' prop # implication
+       | prop '<->' prop
+       | 'not' prop
+       | '(' prop ')' # you can group props via ()
+       | forallProp
+       | existsProp
+
+  forallProp = 'forall' '(' quantifierList ',' prop ')'
+  existsProp = 'exists' '(' quantifierList ',' prop ')'
+
+  quantifierList = quantifier (',' quantifier)*
+  quantifier = <new identifier> 'in' nim_iteration_expression
+
+
+``nim_iteration_expression`` here is an ordinary expression of Nim code
+that describes an iteration space, for example ``1..4`` or ``1..<a.len``.
+
+``nim_bool_expression`` here is an ordinary expression of Nim code of
+type ``bool`` like ``a == 3`` or ``23 > a.len``.
+
+The supported subset of Nim code that can be used in these expressions
+is currently underspecified but ``let`` variables, function parameters
+and ``result`` (which represents the function's final result) are amenable
+for verification. The expressions must not have any side-effects and must
+terminate.
+
+The operators ``forall``, ``exists``, ``->``, ``<->`` have to imported
+from ``std / logic``.
--- a/drnim/drnim.nim
+++ b/drnim/drnim.nim
@@ -0,0 +1,675 @@
+#
+#
+#            Doctor Nim
+#        (c) Copyright 2020 Andreas Rumpf
+#
+#    See the file "copying.txt", included in this
+#    distribution, for details about the copyright.
+#
+
+#[
+
+- Most important bug:
+
+  while i < x.len and use(s[i]): inc i # is safe
+
+- We need to map arrays to Z3 and test for something like 'forall(i, (i in 3..4) -> (a[i] > 3))'
+- forall/exists need syntactic sugar as the manual
+- We need teach DrNim what 'inc', 'dec' and 'swap' mean, for example
+  'x in n..m; inc x' implies 'x in n+1..m+1'
+
+- We need an ``old`` annotation:
+
+proc f(x: var int; y: var int) {.ensures: x == old(x)+1 and y == old(y)+1 .} =
+  inc x
+  inc y
+
+var x = 3
+var y: range[N..M]
+f(x, y)
+{.assume: y in N+1 .. M+1.}
+# --> y in N+1..M+1
+
+proc myinc(x: var int) {.ensures: x-1 == old(x).} =
+  inc x
+
+facts(x) # x < 3
+myinc x
+facts(x+1)
+
+We handle state transitions in this way:
+
+  for every f in facts:
+    replace 'x' by 'old(x)'
+  facts.add ensuresClause
+
+  # then we know: old(x) < 3; x-1 == old(x)
+  # we can conclude:  x-1 < 3 but leave this task to Z3
+
+]#
+
+import std / [
+  parseopt, strutils, os, tables, times
+]
+
+import ".." / compiler / [
+  ast, types, renderer,
+  commands, options, msgs,
+  platform,
+  idents, lineinfos, cmdlinehelper, modulegraphs, condsyms,
+  pathutils, passes, passaux, sem, modules
+]
+
+import z3 / z3_api
+
+when not defined(windows):
+  # on UNIX we use static linking because UNIX's lib*.so system is broken
+  # beyond repair and the neckbeards don't understand software development.
+  {.passL: "dist/z3/build/libz3.a".}
+
+const
+  HelpMessage = "DrNim Version $1 [$2: $3]\n" &
+      "Compiled at $4\n" &
+      "Copyright (c) 2006-" & copyrightYear & " by Andreas Rumpf\n"
+
+const
+  Usage = """
+drnim [options] [projectfile]
+
+Options: Same options that the Nim compiler supports.
+"""
+
+proc getCommandLineDesc(conf: ConfigRef): string =
+  result = (HelpMessage % [system.NimVersion, platform.OS[conf.target.hostOS].name,
+                           CPU[conf.target.hostCPU].name, CompileDate]) &
+                           Usage
+
+proc helpOnError(conf: ConfigRef) =
+  msgWriteln(conf, getCommandLineDesc(conf), {msgStdout})
+  msgQuit(0)
+
+type
+  CannotMapToZ3Error = object of ValueError
+  Z3Exception = object of ValueError
+
+  DrCon = object
+    z3: Z3_context
+    graph: ModuleGraph
+    mapping: Table[string, Z3_ast]
+    canonParameterNames: bool
+
+proc stableName(result: var string; n: PNode) =
+  # we can map full Nim expressions like 'f(a, b, c)' to Z3 variables.
+  # We must be carefult to select a unique, stable name for these expressions
+  # based on structural equality. 'stableName' helps us with this problem.
+  case n.kind
+  of nkEmpty, nkNilLit, nkType: discard
+  of nkIdent:
+    result.add n.ident.s
+  of nkSym:
+    result.add n.sym.name.s
+    result.add '_'
+    result.addInt n.sym.id
+  of nkCharLit..nkUInt64Lit:
+    result.addInt n.intVal
+  of nkFloatLit..nkFloat64Lit:
+    result.addFloat n.floatVal
+  of nkStrLit..nkTripleStrLit:
+    result.add strutils.escape n.strVal
+  else:
+    result.add $n.kind
+    result.add '('
+    for i in 0..<n.len:
+      if i > 0: result.add ", "
+      stableName(result, n[i])
+    result.add ')'
+
+proc stableName(n: PNode): string = stableName(result, n)
+
+proc notImplemented(msg: string) {.noinline.} =
+  raise newException(CannotMapToZ3Error, "; cannot map to Z3: " & msg)
+
+proc translateEnsures(e, x: PNode): PNode =
+  if e.kind == nkSym and e.sym.kind == skResult:
+    result = x
+  else:
+    result = shallowCopy(e)
+    for i in 0 ..< safeLen(e):
+      result[i] = translateEnsures(e[i], x)
+
+proc typeToZ3(c: DrCon; t: PType): Z3_sort =
+  template ctx: untyped = c.z3
+  case t.skipTypes(abstractInst+{tyVar}).kind
+  of tyEnum, tyInt..tyInt64:
+    result = Z3_mk_int_sort(ctx)
+  of tyBool:
+    result = Z3_mk_bool_sort(ctx)
+  of tyFloat..tyFloat128:
+    result = Z3_mk_fpa_sort_double(ctx)
+  of tyChar, tyUInt..tyUInt64:
+    result = Z3_mk_bv_sort(ctx, 64)
+    #cuint(getSize(c.graph.config, t) * 8))
+  else:
+    notImplemented(typeToString(t))
+
+template binary(op, a, b): untyped =
+  var arr = [a, b]
+  op(ctx, cuint(2), addr(arr[0]))
+
+proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast
+
+template quantorToZ3(fn) {.dirty.} =
+  template ctx: untyped = c.z3
+
+  var bound = newSeq[Z3_app](n.len-1)
+  for i in 0..n.len-2:
+    doAssert n[i].kind == nkSym
+    let v = n[i].sym
+    let name = Z3_mk_string_symbol(ctx, v.name.s)
+    let vz3 = Z3_mk_const(ctx, name, typeToZ3(c, v.typ))
+    c.mapping[stableName(n[i])] = vz3
+    bound[i] = Z3_to_app(ctx, vz3)
+
+  var dummy: seq[PNode]
+  let x = nodeToZ3(c, n[^1], dummy)
+  result = fn(ctx, 0, bound.len.cuint, addr(bound[0]), 0, nil, x)
+
+proc forallToZ3(c: var DrCon; n: PNode): Z3_ast = quantorToZ3(Z3_mk_forall_const)
+proc existsToZ3(c: var DrCon; n: PNode): Z3_ast = quantorToZ3(Z3_mk_exists_const)
+
+proc paramName(n: PNode): string =
+  case n.sym.kind
+  of skParam: result = "arg" & $n.sym.position
+  of skResult: result = "result"
+  else: result = stableName(n)
+
+proc nodeToZ3(c: var DrCon; n: PNode; vars: var seq[PNode]): Z3_ast =
+  template ctx: untyped = c.z3
+  template rec(n): untyped = nodeToZ3(c, n, vars)
+  case n.kind
+  of nkSym:
+    let key = if c.canonParameterNames: paramName(n) else: stableName(n)
+    result = c.mapping.getOrDefault(key)
+    if pointer(result) == nil:
+      let name = Z3_mk_string_symbol(ctx, n.sym.name.s)
+      result = Z3_mk_const(ctx, name, typeToZ3(c, n.sym.typ))
+      c.mapping[key] = result
+      vars.add n
+  of nkCharLit..nkUInt64Lit:
+    if n.typ != nil and n.typ.skipTypes(abstractInst).kind in {tyInt..tyInt64}:
+      # optimized for the common case
+      result = Z3_mk_int64(ctx, clonglong(n.intval), Z3_mk_int_sort(ctx))
+    elif n.typ != nil and n.typ.kind == tyBool:
+      result = if n.intval != 0: Z3_mk_true(ctx) else: Z3_mk_false(ctx)
+    elif n.typ != nil and isUnsigned(n.typ):
+      result = Z3_mk_unsigned_int64(ctx, cast[uint64](n.intVal), typeToZ3(c, n.typ))
+    else:
+      let zt = if n.typ == nil: Z3_mk_int_sort(ctx) else: typeToZ3(c, n.typ)
+      result = Z3_mk_numeral(ctx, $getOrdValue(n), zt)
+  of nkFloatLit..nkFloat64Lit:
+    result = Z3_mk_fpa_numeral_double(ctx, n.floatVal, Z3_mk_fpa_sort_double(ctx))
+  of nkCallKinds:
+    assert n.len > 0
+    assert n[0].kind == nkSym
+    let operator = n[0].sym.magic
+    case operator
+    of mEqI, mEqF64, mEqEnum, mEqCh, mEqB, mEqRef, mEqProc,
+        mEqStr, mEqSet, mEqCString:
+      result = Z3_mk_eq(ctx, rec n[1], rec n[2])
+    of mLeI, mLeEnum, mLeCh, mLeB, mLePtr, mLeStr:
+      result = Z3_mk_le(ctx, rec n[1], rec n[2])
+    of mLtI, mLtEnum, mLtCh, mLtB, mLtPtr, mLtStr:
+      result = Z3_mk_lt(ctx, rec n[1], rec n[2])
+    of mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq:
+      # len(x) needs the same logic as 'x' itself
+      if n[1].kind == nkSym:
+        let key = stableName(n)
+        let sym = n[1].sym
+        result = c.mapping.getOrDefault(key)
+        if pointer(result) == nil:
+          let name = Z3_mk_string_symbol(ctx, sym.name.s & ".len")
+          result = Z3_mk_const(ctx, name, Z3_mk_int_sort(ctx))
+          c.mapping[key] = result
+          vars.add n
+      else:
+        notImplemented(renderTree(n))
+    of mAddI, mSucc:
+      result = binary(Z3_mk_add, rec n[1], rec n[2])
+    of mSubI, mPred:
+      result = binary(Z3_mk_sub, rec n[1], rec n[2])
+    of mMulI:
+      result = binary(Z3_mk_mul, rec n[1], rec n[2])
+    of mDivI:
+      result = Z3_mk_div(ctx, rec n[1], rec n[2])
+    of mModI:
+      result = Z3_mk_mod(ctx, rec n[1], rec n[2])
+    of mMaxI:
+      # max(a, b) <=> ite(a < b, b, a)
+      result = Z3_mk_ite(ctx, Z3_mk_lt(ctx, rec n[1], rec n[2]),
+        rec n[2], rec n[1])
+    of mMinI:
+      # min(a, b) <=> ite(a < b, a, b)
+      result = Z3_mk_ite(ctx, Z3_mk_lt(ctx, rec n[1], rec n[2]),
+        rec n[1], rec n[2])
+    of mLeU:
+      result = Z3_mk_bvule(ctx, rec n[1], rec n[2])
+    of mLtU:
+      result = Z3_mk_bvult(ctx, rec n[1], rec n[2])
+    of mAnd:
+      result = binary(Z3_mk_and, rec n[1], rec n[2])
+    of mOr:
+      result = binary(Z3_mk_or, rec n[1], rec n[2])
+    of mXor:
+      result = Z3_mk_xor(ctx, rec n[1], rec n[2])
+    of mNot:
+      result = Z3_mk_not(ctx, rec n[1])
+    of mImplies:
+      result = Z3_mk_implies(ctx, rec n[1], rec n[2])
+    of mIff:
+      result = Z3_mk_iff(ctx, rec n[1], rec n[2])
+    of mForall:
+      result = forallToZ3(c, n)
+    of mExists:
+      result = existsToZ3(c, n)
+    of mLeF64:
+      result = Z3_mk_fpa_leq(ctx, rec n[1], rec n[2])
+    of mLtF64:
+      result = Z3_mk_fpa_lt(ctx, rec n[1], rec n[2])
+    of mAddF64:
+      result = Z3_mk_fpa_add(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2])
+    of mSubF64:
+      result = Z3_mk_fpa_sub(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2])
+    of mMulF64:
+      result = Z3_mk_fpa_mul(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2])
+    of mDivF64:
+      result = Z3_mk_fpa_div(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2])
+    of mShrI:
+      # XXX handle conversions from int to uint here somehow
+      result = Z3_mk_bvlshr(ctx, rec n[1], rec n[2])
+    of mAshrI:
+      result = Z3_mk_bvashr(ctx, rec n[1], rec n[2])
+    of mShlI:
+      result = Z3_mk_bvshl(ctx, rec n[1], rec n[2])
+    of mBitandI:
+      result = Z3_mk_bvand(ctx, rec n[1], rec n[2])
+    of mBitorI:
+      result = Z3_mk_bvor(ctx, rec n[1], rec n[2])
+    of mBitxorI:
+      result = Z3_mk_bvxor(ctx, rec n[1], rec n[2])
+    of mOrd, mChr:
+      result = rec n[1]
+    of mOld:
+      let key = (if c.canonParameterNames: paramName(n[1]) else: stableName(n[1])) & ".old"
+      result = c.mapping.getOrDefault(key)
+      if pointer(result) == nil:
+        let name = Z3_mk_string_symbol(ctx, $n)
+        result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ))
+        c.mapping[key] = result
+        # XXX change the logic in `addRangeInfo` for this
+        #vars.add n
+
+    else:
+      # sempass2 adds some 'fact' like 'x = f(a, b)' (see addAsgnFact)
+      # 'f(a, b)' can have an .ensures annotation and we need to make use
+      # of this information.
+      # we need to map 'f(a, b)' to a Z3 variable of this name
+      let op = n[0].typ
+      if op != nil and op.n != nil and op.n.len > 0 and op.n[0].kind == nkEffectList and
+          ensuresEffects < op.n[0].len:
+        let ensures = op.n[0][ensuresEffects]
+        if ensures != nil and ensures.kind != nkEmpty:
+          let key = stableName(n)
+          result = c.mapping.getOrDefault(key)
+          if pointer(result) == nil:
+            let name = Z3_mk_string_symbol(ctx, $n)
+            result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ))
+            c.mapping[key] = result
+            vars.add n
+
+      if pointer(result) == nil:
+        notImplemented(renderTree(n))
+  of nkStmtListExpr, nkPar:
+    var isTrivial = true
+    for i in 0..n.len-2:
+      isTrivial = isTrivial and n[i].kind in {nkEmpty, nkCommentStmt}
+    if isTrivial:
+      result = nodeToZ3(c, n[^1], vars)
+    else:
+      notImplemented(renderTree(n))
+  of nkHiddenDeref:
+    result = rec n[0]
+  else:
+    notImplemented(renderTree(n))
+
+proc addRangeInfo(c: var DrCon, n: PNode, res: var seq[Z3_ast]) =
+  var cmpOp = mLeI
+  if n.typ != nil:
+    cmpOp =
+      case n.typ.skipTypes(abstractInst).kind
+      of tyFloat..tyFloat128: mLeF64
+      of tyChar, tyUInt..tyUInt64: mLeU
+      else: mLeI
+
+  var lowBound, highBound: PNode
+  if n.kind == nkSym:
+    let v = n.sym
+    let t = v.typ.skipTypes(abstractInst - {tyRange})
+
+    case t.kind
+    of tyRange:
+      lowBound = t.n[0]
+      highBound = t.n[1]
+    of tyFloat..tyFloat128:
+      # no range information for non-range'd floats
+      return
+    of tyUInt..tyUInt64, tyChar:
+      lowBound = newIntNode(nkUInt64Lit, firstOrd(nil, v.typ))
+      lowBound.typ = v.typ
+      highBound = newIntNode(nkUInt64Lit, lastOrd(nil, v.typ))
+      highBound.typ = v.typ
+    of tyInt..tyInt64, tyEnum:
+      lowBound = newIntNode(nkInt64Lit, firstOrd(nil, v.typ))
+      highBound = newIntNode(nkInt64Lit, lastOrd(nil, v.typ))
+    else:
+      # no range information available:
+      return
+  elif n.kind in nkCallKinds and n.len == 2 and n[0].kind == nkSym and
+      n[0].sym.magic in {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq}:
+    # we know it's a 'len(x)' expression and we seek to teach
+    # Z3 that the result is >= 0 and <= high(int).
+    doAssert n.kind in nkCallKinds
+    doAssert n[0].kind == nkSym
+    doAssert n.len == 2
+
+    lowBound = newIntNode(nkInt64Lit, 0)
+    if n.typ != nil:
+      highBound = newIntNode(nkInt64Lit, lastOrd(nil, n.typ))
+    else:
+      highBound = newIntNode(nkInt64Lit, high(int64))
+  else:
+    let op = n[0].typ
+    if op != nil and op.n != nil and op.n.len > 0 and op.n[0].kind == nkEffectList and
+        ensuresEffects < op.n[0].len:
+      let ensures = op.n[0][ensuresEffects]
+      if ensures != nil and ensures.kind != nkEmpty:
+        var dummy: seq[PNode]
+        res.add nodeToZ3(c, translateEnsures(ensures, n), dummy)
+    return
+
+  let x = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), lowBound, n)
+  let y = newTree(nkInfix, newSymNode createMagic(c.graph, "<=", cmpOp), n, highBound)
+
+  var dummy: seq[PNode]
+  res.add nodeToZ3(c, x, dummy)
+  res.add nodeToZ3(c, y, dummy)
+
+proc on_err(ctx: Z3_context, e: Z3_error_code) {.nimcall.} =
+  #writeStackTrace()
+  let msg = $Z3_get_error_msg(ctx, e)
+  raise newException(Z3Exception, msg)
+
+proc forall(ctx: Z3_context; vars: seq[Z3_ast]; assumption, body: Z3_ast): Z3_ast =
+  let x = Z3_mk_implies(ctx, assumption, body)
+  if vars.len > 0:
+    var bound: seq[Z3_app]
+    for v in vars: bound.add Z3_to_app(ctx, v)
+    result = Z3_mk_forall_const(ctx, 0, bound.len.cuint, addr(bound[0]), 0, nil, x)
+  else:
+    result = x
+
+proc conj(ctx: Z3_context; conds: seq[Z3_ast]): Z3_ast =
+  if conds.len > 0:
+    result = Z3_mk_and(ctx, cuint(conds.len), unsafeAddr conds[0])
+  else:
+    result = Z3_mk_true(ctx)
+
+proc proofEngineAux(c: var DrCon; assumptions: seq[PNode]; toProve: PNode): (bool, string) =
+  c.mapping = initTable[string, Z3_ast]()
+  let cfg = Z3_mk_config()
+  Z3_set_param_value(cfg, "model", "true");
+  let ctx = Z3_mk_context(cfg)
+  c.z3 = ctx
+  Z3_del_config(cfg)
+  Z3_set_error_handler(ctx, on_err)
+
+  when false:
+    Z3_set_param_value(cfg, "timeout", "1000")
+
+  try:
+
+    #[
+    For example, let's have these facts:
+
+      i < 10
+      i > 0
+
+    Question:
+
+      i + 3 < 13
+
+    What we need to produce:
+
+    forall(i, (i < 10) & (i > 0) -> (i + 3 < 13))
+
+    ]#
+
+    var collectedVars: seq[PNode]
+
+    let solver = Z3_mk_solver(ctx)
+    var lhs: seq[Z3_ast]
+    for assumption in assumptions:
+      if assumption != nil:
+        try:
+          let za = nodeToZ3(c, assumption, collectedVars)
+          #Z3_solver_assert ctx, solver, za
+          lhs.add za
+        except CannotMapToZ3Error:
+          discard "ignore a fact we cannot map to Z3"
+
+    let z3toProve = nodeToZ3(c, toProve, collectedVars)
+    for v in collectedVars:
+      addRangeInfo(c, v, lhs)
+
+    # to make Z3 produce nice counterexamples, we try to prove the
+    # negation of our conjecture and see if it's Z3_L_FALSE
+    let fa = Z3_mk_not(ctx, Z3_mk_implies(ctx, conj(ctx, lhs), z3toProve))
+
+    #Z3_mk_not(ctx, forall(ctx, collectedVars, conj(ctx, lhs), z3toProve))
+
+    #echo "toProve: ", Z3_ast_to_string(ctx, fa), " ", c.graph.config $ toProve.info
+    Z3_solver_assert ctx, solver, fa
+
+    let z3res = Z3_solver_check(ctx, solver)
+    result[0] = z3res == Z3_L_FALSE
+    result[1] = ""
+    if not result[0]:
+      let counterex = strip($Z3_model_to_string(ctx, Z3_solver_get_model(ctx, solver)))
+      if counterex.len > 0:
+        result[1].add "; counter example: " & counterex
+  except ValueError:
+    result[0] = false
+    result[1] = getCurrentExceptionMsg()
+  finally:
+    Z3_del_context(ctx)
+
+proc proofEngine(graph: ModuleGraph; assumptions: seq[PNode]; toProve: PNode): (bool, string) =
+  var c: DrCon
+  c.graph = graph
+  result = proofEngineAux(c, assumptions, toProve)
+
+proc translateReq(r, call: PNode): PNode =
+  if r.kind == nkSym and r.sym.kind == skParam:
+    if r.sym.position+1 < call.len:
+      result = call[r.sym.position+1]
+    else:
+      notImplemented("no argument given for formal parameter: " & r.sym.name.s)
+  else:
+    result = shallowCopy(r)
+    for i in 0 ..< safeLen(r):
+      result[i] = translateReq(r[i], call)
+
+proc requirementsCheck(graph: ModuleGraph; assumptions: seq[PNode];
+                      call, requirement: PNode): (bool, string) {.nimcall.} =
+  try:
+    let r = translateReq(requirement, call)
+    result = proofEngine(graph, assumptions, r)
+  except ValueError:
+    result[0] = false
+    result[1] = getCurrentExceptionMsg()
+
+proc compatibleProps(graph: ModuleGraph; formal, actual: PType): bool {.nimcall.} =
+  #[
+  Thoughts on subtyping rules for 'proc' types:
+
+    proc a(y: int) {.requires: y > 0.}  # a is 'weaker' than F
+    # 'requires' must be weaker (or equal)
+    # 'ensures'  must be stronger (or equal)
+
+    # a 'is weaker than' b iff  b -> a
+    # a 'is stronger than' b iff a -> b
+    # --> We can use Z3 to compute whether 'var x: T = q' is valid
+
+    type
+      F = proc (y: int) {.requires: y > 5.}
+
+    var
+      x: F = a # valid?
+  ]#
+  proc isEmpty(n: PNode): bool {.inline.} = n == nil or n.safeLen == 0
+
+  result = true
+  if formal.n != nil and formal.n.len > 0 and formal.n[0].kind == nkEffectList and
+      ensuresEffects < formal.n[0].len:
+
+    let frequires = formal.n[0][requiresEffects]
+    let fensures = formal.n[0][ensuresEffects]
+
+    if actual.n != nil and actual.n.len > 0 and actual.n[0].kind == nkEffectList and
+        ensuresEffects < actual.n[0].len:
+      let arequires = actual.n[0][requiresEffects]
+      let aensures = actual.n[0][ensuresEffects]
+
+      var c: DrCon
+      c.graph = graph
+      c.canonParameterNames = true
+      if not frequires.isEmpty:
+        result = not arequires.isEmpty and proofEngineAux(c, @[frequires], arequires)[0]
+
+      if result:
+        if not fensures.isEmpty:
+          result = not aensures.isEmpty and proofEngineAux(c, @[aensures], fensures)[0]
+    else:
+      # formal has requirements but 'actual' has none, so make it
+      # incompatible. XXX What if the requirement only mentions that
+      # we already know from the type system?
+      result = frequires.isEmpty and fensures.isEmpty
+
+proc mainCommand(graph: ModuleGraph) =
+  let conf = graph.config
+  conf.lastCmdTime = epochTime()
+
+  graph.proofEngine = proofEngine
+  graph.requirementsCheck = requirementsCheck
+  graph.compatibleProps = compatibleProps
+
+  graph.config.errorMax = high(int)  # do not stop after first error
+  defineSymbol(graph.config.symbols, "nimcheck")
+  defineSymbol(graph.config.symbols, "nimDrNim")
+
+  registerPass graph, verbosePass
+  registerPass graph, semPass
+  compileProject(graph)
+  if conf.errorCounter == 0:
+    let mem =
+      when declared(system.getMaxMem): formatSize(getMaxMem()) & " peakmem"
+      else: formatSize(getTotalMem()) & " totmem"
+    let loc = $conf.linesCompiled
+    let build = if isDefined(conf, "danger"): "Dangerous Release"
+                elif isDefined(conf, "release"): "Release"
+                else: "Debug"
+    let sec = formatFloat(epochTime() - conf.lastCmdTime, ffDecimal, 3)
+    let project = if optListFullPaths in conf.globalOptions: $conf.projectFull else: $conf.projectName
+    var output = $conf.absOutFile
+    if optListFullPaths notin conf.globalOptions: output = output.AbsoluteFile.extractFilename
+    rawMessage(conf, hintSuccessX, [
+      "loc", loc,
+      "sec", sec,
+      "mem", mem,
+      "build", build,
+      "project", project,
+      "output", output,
+      ])
+
+proc prependCurDir(f: AbsoluteFile): AbsoluteFile =
+  when defined(unix):
+    if os.isAbsolute(f.string): result = f
+    else: result = AbsoluteFile("./" & f.string)
+  else:
+    result = f
+
+proc addCmdPrefix(result: var string, kind: CmdLineKind) =
+  # consider moving this to std/parseopt
+  case kind
+  of cmdLongOption: result.add "--"
+  of cmdShortOption: result.add "-"
+  of cmdArgument, cmdEnd: discard
+
+proc processCmdLine(pass: TCmdLinePass, cmd: string; config: ConfigRef) =
+  var p = parseopt.initOptParser(cmd)
+  var argsCount = 1
+
+  config.commandLine.setLen 0
+  config.command = "check"
+  config.cmd = cmdCheck
+
+  while true:
+    parseopt.next(p)
+    case p.kind
+    of cmdEnd: break
+    of cmdLongOption, cmdShortOption:
+      config.commandLine.add " "
+      config.commandLine.addCmdPrefix p.kind
+      config.commandLine.add p.key.quoteShell # quoteShell to be future proof
+      if p.val.len > 0:
+        config.commandLine.add ':'
+        config.commandLine.add p.val.quoteShell
+
+      if p.key == " ":
+        p.key = "-"
+        if processArgument(pass, p, argsCount, config): break
+      else:
+        processSwitch(pass, p, config)
+    of cmdArgument:
+      config.commandLine.add " "
+      config.commandLine.add p.key.quoteShell
+      if processArgument(pass, p, argsCount, config): break
+  if pass == passCmd2:
+    if {optRun, optWasNimscript} * config.globalOptions == {} and
+        config.arguments.len > 0 and config.command.normalize notin ["run", "e"]:
+      rawMessage(config, errGenerated, errArgsNeedRunOption)
+
+proc handleCmdLine(cache: IdentCache; conf: ConfigRef) =
+  let self = NimProg(
+    supportsStdinFile: true,
+    processCmdLine: processCmdLine,
+    mainCommand: mainCommand
+  )
+  self.initDefinesProg(conf, "drnim")
+  if paramCount() == 0:
+    helpOnError(conf)
+    return
+
+  self.processCmdLineAndProjectPath(conf)
+  if not self.loadConfigsAndRunMainCommand(cache, conf): return
+  if conf.hasHint(hintGCStats): echo(GC_getStatistics())
+
+when compileOption("gc", "v2") or compileOption("gc", "refc"):
+  # the new correct mark&sweep collector is too slow :-/
+  GC_disableMarkAndSweep()
+
+when not defined(selftest):
+  let conf = newConfigRef()
+  handleCmdLine(newIdentCache(), conf)
+  when declared(GC_setMaxPause):
+    echo GC_getStatistics()
+  msgQuit(int8(conf.errorCounter > 0))
--- a/drnim/nim.cfg
+++ b/drnim/nim.cfg
@@ -0,0 +1,18 @@
+# Special configuration file for the Nim project
+
+hint[XDeclaredButNotUsed]:off
+
+define:booting
+define:nimcore
+define:drnim
+
+@if windows:
+  cincludes: "$lib/wrappers/libffi/common"
+@end
+
+define:useStdoutAsStdmsg
+
+--path: "../../nimz3/src"
+--path: "../dist/nimz3/src"
+
+#define:useNodeIds
--- a/drnim/tests/config.nims
+++ b/drnim/tests/config.nims
@@ -0,0 +1,7 @@
+switch("path", "$nim/testament/lib") # so we can `import stdtest/foo` in this dir
+
+## prevent common user config settings to interfere with testament expectations
+## Indifidual tests can override this if needed to test for these options.
+switch("colors", "off")
+switch("listFullPaths", "off")
+switch("excessiveStackTrace", "off")
--- a/drnim/tests/tbasic_array_index.nim
+++ b/drnim/tests/tbasic_array_index.nim
@@ -0,0 +1,43 @@
+discard """
+  nimout: '''tbasic_array_index.nim(26, 17) Warning: cannot prove: 0 <= len(a) - 4; counter example: a.len -> 0 [IndexCheck]
+tbasic_array_index.nim(32, 5) Warning: cannot prove: 4.0 <= 1.0 [IndexCheck]
+tbasic_array_index.nim(38, 36) Warning: cannot prove: a <= 10'u32; counter example: a -> #x000000000000000b
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+
+proc takeNat(n: Natural) =
+  discard
+
+proc p(a, b: openArray[int]) =
+  if a.len > 0:
+    echo a[0]
+
+  for i in 0..a.len-8:
+    #{.invariant: i < a.len.}
+    echo a[i]
+
+  for i in 0..min(a.len, b.len)-1:
+    echo a[i], " ", b[i]
+
+  takeNat(a.len - 4)
+
+proc r(x: range[0.0..1.0]) = echo x
+
+proc sum() =
+  r 1.0
+  r 4.0
+
+proc ru(x: range[1u32..10u32]) = echo x
+
+proc xu(a: uint) =
+  if a >= 4u:
+    let chunk = range[1u32..10u32](a)
+    ru chunk
+
+{.pop.}
+
+p([1, 2, 3], [4, 5])
--- a/drnim/tests/tensures.nim
+++ b/drnim/tests/tensures.nim
@@ -0,0 +1,31 @@
+discard """
+  nimout: '''tensures.nim(11, 10) Warning: BEGIN [User]
+tensures.nim(20, 5) Warning: cannot prove:
+0 < n [IndexCheck]
+tensures.nim(30, 10) Warning: END [User]'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+{.warning: "BEGIN".}
+
+proc fac(n: int) {.requires: n > 0.} =
+  discard
+
+proc g(): int {.ensures: result > 0.} =
+  result = 10
+
+fac 7 # fine
+fac -45 # wrong
+
+fac g() # fine
+
+proc main =
+  var x = g()
+  fac x
+
+main()
+
+{.warning: "END".}
+{.pop.}
--- a/drnim/tests/tsetlen_invalidates.nim
+++ b/drnim/tests/tsetlen_invalidates.nim
@@ -0,0 +1,22 @@
+discard """
+  nimout: '''
+tsetlen_invalidates.nim(15, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a.len -> 0 [IndexCheck]
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+
+proc p() =
+  var a = newSeq[int](3)
+  if a.len > 0:
+    a.setLen 0
+    echo a[0]
+
+  if a.len > 0:
+    echo a[0]
+
+{.pop.}
+
+p()
--- a/koch.nim
+++ b/koch.nim
@@ -12,6 +12,10 @@
 const
  NimbleStableCommit = "4007b2a778429a978e12307bf13a038029b4c4d9" # master

+when not defined(windows):
+  const
+    Z3StableCommit = "65de3f748a6812eecd7db7c478d5fc54424d368b" # the version of Z3 that DrNim uses
+
 when defined(gcc) and defined(windows):
  when defined(x86):
    {.link: "icons/koch.res".}
@@ -473,6 +477,29 @@ proc xtemp(cmd: string) =
  finally:
    copyExe(d / "bin" / "nim_backup".exe, d / "bin" / "nim".exe)

+proc buildDrNim(args: string) =
+  if not dirExists("dist/nimz3"):
+    exec("git clone https://github.com/zevv/nimz3.git dist/nimz3")
+  when defined(windows):
+    if not dirExists("dist/dlls"):
+      exec("git clone -q https://github.com/nim-lang/dlls.git dist/dlls")
+    copyExe("dist/dlls/libz3.dll", "bin/libz3.dll")
+    execFold("build drnim", "nim c -o:$1 $2 drnim/drnim" % ["bin/drnim".exe, args])
+  else:
+    if not dirExists("dist/z3"):
+      exec("git clone -q https://github.com/Z3Prover/z3.git dist/z3")
+      withDir("dist/z3"):
+        exec("git fetch")
+        exec("git checkout " & Z3StableCommit)
+        createDir("build")
+        withDir("build"):
+          exec("""cmake -DZ3_BUILD_LIBZ3_SHARED=FALSE -G "Unix Makefiles" ../""")
+          exec("make -j4")
+    execFold("build drnim", "nim cpp --dynlibOverride=libz3 -o:$1 $2 drnim/drnim" % ["bin/drnim".exe, args])
+  # always run the tests for now:
+  exec("testament/testament".exe & " --nim:" & "drnim".exe & " pat drnim/tests")
+
+
 proc hostInfo(): string =
  "hostOS: $1, hostCPU: $2, int: $3, float: $4, cpuEndian: $5, cwd: $6" %
    [hostOS, hostCPU, $int.sizeof, $float.sizeof, $cpuEndian, getCurrentDir()]
@@ -636,6 +663,7 @@ when isMainModule:
      of "pushcsource", "pushcsources": pushCsources()
      of "valgrind": valgrind(op.cmdLineRest)
      of "c2nim": bundleC2nim(op.cmdLineRest)
+      of "drnim": buildDrNim(op.cmdLineRest)
      else: showHelp()
      break
    of cmdEnd: break
--- a/lib/std/logic.nim
+++ b/lib/std/logic.nim
@@ -0,0 +1,10 @@
+## This module provides further logic operators like 'forall' and 'exists'
+## They are only supported in ``.ensures`` etc pragmas.
+
+proc `->`*(a, b: bool): bool {.magic: "Implies".}
+proc `<->`*(a, b: bool): bool {.magic: "Iff".}
+
+proc forall*(args: varargs[untyped]): bool {.magic: "Forall".}
+proc exists*(args: varargs[untyped]): bool {.magic: "Exists".}
+
+proc old*[T](x: T): T {.magic: "Old".}
--- a/lib/system/strmantle.nim
+++ b/lib/system/strmantle.nim
@@ -115,6 +115,9 @@ const
              1e10, 1e11, 1e12, 1e13, 1e14, 1e15, 1e16, 1e17, 1e18, 1e19,
              1e20, 1e21, 1e22]

+when defined(nimHasInvariant):
+  {.push staticBoundChecks: off.}
+
 proc nimParseBiggestFloat(s: string, number: var BiggestFloat,
                          start = 0): int {.compilerproc.} =
  # This routine attempt to parse float that can parsed quickly.
@@ -236,7 +239,7 @@ proc nimParseBiggestFloat(s: string, number: var BiggestFloat,
    # if exponent is greater try to fit extra exponent above 22 by multiplying
    # integer part is there is space left.
    let slop = 15 - kdigits - fdigits
-    if  absExponent <= 22 + slop and not expNegative:
+    if absExponent <= 22 + slop and not expNegative:
      number = sign * integer.float * powtens[slop] * powtens[absExponent-slop]
      return i - start

@@ -274,6 +277,9 @@ proc nimParseBiggestFloat(s: string, number: var BiggestFloat,
  else:
    number = c_strtod(t, nil)

+when defined(nimHasInvariant):
+  {.pop.} # staticBoundChecks
+
 proc nimInt64ToStr(x: int64): string {.compilerRtl.} =
  result = newStringOfCap(sizeof(x)*4)
  result.addInt x
--- a/testament/categories.nim
+++ b/testament/categories.nim
@@ -728,12 +728,22 @@ proc processCategory(r: var TResults, cat: Category,

 proc processPattern(r: var TResults, pattern, options: string; simulate: bool) =
  var testsRun = 0
-  for name in walkPattern(pattern):
-    if simulate:
-      echo "Detected test: ", name
-    else:
-      var test = makeTest(name, options, Category"pattern")
-      testSpec r, test
-    inc testsRun
+  if dirExists(pattern):
+    for k, name in walkDir(pattern):
+      if k in {pcFile, pcLinkToFile} and name.endsWith(".nim"):
+        if simulate:
+          echo "Detected test: ", name
+        else:
+          var test = makeTest(name, options, Category"pattern")
+          testSpec r, test
+        inc testsRun
+  else:
+    for name in walkPattern(pattern):
+      if simulate:
+        echo "Detected test: ", name
+      else:
+        var test = makeTest(name, options, Category"pattern")
+        testSpec r, test
+      inc testsRun
  if testsRun == 0:
    echo "no tests were found for pattern: ", pattern
--- a/testament/testament.nim.cfg
+++ b/testament/testament.nim.cfg
@@ -1,2 +1,4 @@
 path = "$nim" # For compiler/nodejs
 -d:ssl # For azure
+# my SSL doesn't have this feature and I don't care:
+-d:nimDisableCertificateValidation
--- a/tools/kochdocs.nim
+++ b/tools/kochdocs.nim
@@ -110,6 +110,7 @@ doc/tut2.rst
 doc/tut3.rst
 doc/nimc.rst
 doc/hcr.rst
+doc/drnim.rst
 doc/overview.rst
 doc/filters.rst
 doc/tools.rst