Unbundle drnim

- Removes main drnim directory along with all the hacks added into `sem*`
  implementation - special keywords for
  `ensures/requires/assume/invariant`, more logic built into sempass and so
  on. Sem reports that were added in the main compilation.
- External tooling for code analysis should better be implemented via
  completely external modifications, instead of clobbering the main
  compiler codebase with logic for barely functioning tooling. With DOD
  refactor this task becomes much easier, since extra metadata can be
  attached to any symbol.
- We definitely want to move in the direction of automatic code correctness
  and static analysis, but right now this is not a priority, and
  considering dubious implementation of the tool, it would be easier to
  remove it for now and come up with a proper implementation later on, or
  when can turn all hacks back into sem.
- drnim itself not tested as a part of CI so right now it can't even be
  built, due to file reorganization
  nim-works#177.
- Adds reports for `--staticBounds:on|off` that were mistakenly assumed to
  be drnim-only during earlier refactor
  nim-works#94 for structured reports.

Closes nim-works#130 as this pull removes
`drnim` as well, and the author of that PR is no longer responsive. Due to
multiple merge conflicts it is highly unlikely the old PR will be revived.

compiler/ast/ast_types.nim

@@ -389,11 +389,9 @@ const
   nkEffectList* = nkArgList
   # hacks ahead: an nkEffectList is a node with 4 children:
   exceptionEffects* = 0 ## exceptions at position 0
-  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
+  tagEffects* = 1       ## user defined tag ('gc', 'time' etc.)
+  pragmasEffects* = 2   ## not an effect, but a slot for pragmas in proc type
+  effectListLen* = 3    ## list of effects list
   nkLastBlockStmts* = {nkRaiseStmt, nkReturnStmt, nkBreakStmt, nkContinueStmt}
                         ## these must be last statements in a block
 
@@ -719,7 +717,6 @@ type
     mCStrToStr,
     mStrToStr, mEnumToStr,
     mAnd, mOr,
-    mImplies, mIff, mExists, mForall, mOld,
     mEqStr, mLeStr, mLtStr,
     mEqSet, mLeSet, mLtSet, mMulSet, mPlusSet, mMinusSet,
     mConStrStr, mSlice,

compiler/ast/reports.nim

@@ -336,6 +336,8 @@ type
     rsemCantComputeOffsetof
     rsemStaticOutOfBounds ## Error generated when semfold or static bound
     ## checking sees and out-of-bounds index error.
+    rsemStaticIndexLeqUnprovable
+    rsemStaticIndexGeProvable
     rsemStaticFieldNotFound # TODO DOC generated in `semfold.nim`, need
     # better documentation, right now I don't know what exactly this error
     # means and how to reproduce it in the example code.
@@ -773,10 +775,6 @@ type
     rsemUnguardedAccess
     rsemInvalidGuardField
 
-    rsemDrNimRequiresUsesMissingResult
-    rsemDrnimCannotProveLeq
-    rsemDrnimCannotPorveGe
-
     rsemErrGcUnsafeListing
     rsemBorrowPragmaNonDot
     rsemInvalidExtern
@@ -1259,8 +1257,9 @@ type
       of rsemWrongIdent:
         expectedIdents*: seq[string]
 
-      of rsemDrnimCannotProveLeq, rsemDrnimCannotPorveGe:
-        drnimExpressions*: tuple[a, b: PNode]
+
+      of rsemStaticIndexLeqUnprovable, rsemStaticIndexGeProvable:
+        rangeExpression*: tuple[a, b: PNode]
 
       of rsemExprHasNoAddress:
         isUnsafeAddr*: bool

compiler/ast/trees.nim

@@ -160,12 +160,6 @@ 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)

compiler/ast/wordrecg.nim

@@ -70,8 +70,7 @@ type
     wSinkInference = "sinkInference", wWarnings = "warnings",
     wHints = "hints", wOptimization = "optimization", wRaises = "raises",
     wWrites = "writes", wReads = "reads", wSize = "size", wEffects = "effects", wTags = "tags",
-    wRequires = "requires", wEnsures = "ensures", wInvariant = "invariant",
-    wAssume = "assume", wAssert = "assert",
+    wAssert = "assert",
     wDeadCodeElimUnused = "deadCodeElim",  # deprecated, dead code elim always happens
     wSafecode = "safecode", wPackage = "package", wNoForward = "noforward", wReorder = "reorder",
     wNoRewrite = "norewrite", wNoDestroy = "nodestroy", wPragma = "pragma",

compiler/front/cli_reporter.nim

@@ -2163,14 +2163,13 @@ proc reportBody*(conf: ConfigRef, r: SemReport): string =
     of rsemErrGcUnsafe:
       result = r.ast.render & " is not GC safe"
 
-    of rsemDrnimCannotPorveGe:
-      assert false, "TODO"
+    of rsemStaticIndexLeqUnprovable:
+      let (a, b) = r.rangeExpression
+      result = "cannot prove: " & $a & " <= " & $b
 
-    of rsemDrnimCannotProveLeq:
-      assert false, "TODO"
-
-    of rsemDrNimRequiresUsesMissingResult:
-      assert false, "TODO"
+    of rsemStaticIndexGeProvable:
+      let (a, b) = r.rangeExpression
+      result = "can prove: " & $a & " > " & $b
 
     of rsemInvalidGuardField:
       result = "invalid guard field: " & r.symstr

compiler/modules/modulegraphs.nim

@@ -449,9 +449,8 @@ proc registerModule*(g: ModuleGraph; m: PSym) =
 proc registerModuleById*(g: ModuleGraph; m: FileIndex) =
   registerModule(g, g.packed[int m].module)
 
-proc initOperators*(g: ModuleGraph): Operators =
+proc initOperators(g: ModuleGraph): Operators =
   # These are safe for IC.
-  # Public because it's used by DrNim.
   result.opLe = createMagic(g, "<=", mLeI)
   result.opLt = createMagic(g, "<", mLtI)
   result.opAnd = createMagic(g, "and", mAnd)

compiler/sem/guards.nim

@@ -474,30 +474,6 @@ proc hasSubTree(n, x: PNode): bool =
       for i in 0..<n.len:
         if hasSubTree(n[i], x): return true
 
-proc invalidateFacts*(s: var seq[PNode], n: PNode) =
-  # We are able to guard local vars (as opposed to 'let' variables)!
-  # 'while p != nil: f(p); p = p.next'
-  # This is actually quite easy to do:
-  # Re-assignments (incl. pass to a 'var' param) trigger an invalidation
-  # of every fact that contains 'v'.
-  #
-  #   if x < 4:
-  #     if y < 5
-  #       x = unknown()
-  #       # we invalidate 'x' here but it's known that x >= 4
-  #       # for the else anyway
-  #   else:
-  #     echo x
-  #
-  # The same mechanism could be used for more complex data stored on the heap;
-  # procs that 'write: []' cannot invalidate 'n.kind' for instance. In fact, we
-  # could CSE these expressions then and help C's optimizer.
-  for i in 0..high(s):
-    if s[i] != nil and s[i].hasSubTree(n): s[i] = nil
-
-proc invalidateFacts*(m: var TModel, n: PNode) =
-  invalidateFacts(m.s, n)
-
 proc valuesUnequal(a, b: PNode): bool =
   if a.isValue and b.isValue:
     result = not sameValue(a, b)

compiler/sem/pragmas.nim

@@ -67,7 +67,7 @@ const
     wAsmNoStackFrame, wDiscardable, wNoInit, wCodegenDecl,
     wGensym, wInject, wRaises, wEffectsOf, wTags, wLocks, wDelegator, wGcSafe,
     wConstructor, wLiftLocals, wStackTrace, wLineTrace, wNoDestroy,
-    wRequires, wEnsures, wEnforceNoRaises}
+    wEnforceNoRaises}
   converterPragmas* = procPragmas
   methodPragmas* = procPragmas+{wBase}-{wImportCpp}
   templatePragmas* = {wDeprecated, wError, wGensym, wInject, wDirty,
@@ -78,7 +78,7 @@ const
   iteratorPragmas* = declPragmas + {FirstCallConv..LastCallConv, wNoSideEffect, wSideEffect,
     wMagic, wBorrow,
     wDiscardable, wGensym, wInject, wRaises, wEffectsOf,
-    wTags, wLocks, wGcSafe, wRequires, wEnsures}
+    wTags, wLocks, wGcSafe}
   exprPragmas* = {wLine, wLocks, wNoRewrite, wGcSafe, wNoSideEffect}
   stmtPragmas* = {wChecks, wObjChecks, wFieldChecks, wRangeChecks,
     wBoundChecks, wOverflowChecks, wNilChecks, wStaticBoundchecks,
@@ -91,11 +91,11 @@ const
     wDeprecated,
     wFloatChecks, wInfChecks, wNanChecks, wPragma, wEmit, wUnroll,
     wLinearScanEnd, wPatterns, wTrMacros, wEffects, wNoForward, wReorder, wComputedGoto,
-    wExperimental, wThis, wUsed, wInvariant, wAssume, wAssert}
+    wExperimental, wThis, wUsed, wAssert}
   lambdaPragmas* = {FirstCallConv..LastCallConv,
     wNoSideEffect, wSideEffect, wNoreturn, wNosinks, wDynlib, wHeader,
     wThread, wAsmNoStackFrame,
-    wRaises, wLocks, wTags, wRequires, wEnsures, wEffectsOf,
+    wRaises, wLocks, wTags, wEffectsOf,
     wGcSafe, wCodegenDecl, wNoInit, wCompileTime}
   typePragmas* = declPragmas + {wMagic, wAcyclic,
     wPure, wHeader, wCompilerProc, wCore, wFinal, wSize, wShallow,
@@ -115,8 +115,7 @@ const
   paramPragmas* = {wNoalias, wInject, wGensym}
   letPragmas* = varPragmas
   procTypePragmas* = {FirstCallConv..LastCallConv, wVarargs, wNoSideEffect,
-                      wThread, wRaises, wEffectsOf, wLocks, wTags, wGcSafe,
-                      wRequires, wEnsures}
+                      wThread, wRaises, wEffectsOf, wLocks, wTags, wGcSafe}
   forVarPragmas* = {wInject, wGensym}
   allRoutinePragmas* = methodPragmas + iteratorPragmas + lambdaPragmas
   enumFieldPragmas* = {wDeprecated}
@@ -158,45 +157,6 @@ proc newIllegalCustomPragmaNode*(c: PContext; n: PNode, s: PSym): PNode =
     n.info
   )
 
-proc pragmaProposition(c: PContext, n: PNode): PNode =
-  ## drnim - `ensures` pragma,  must be a callable with single arg predicate,
-  ## producing either:
-  ## 1. mutated `n` with the the proposition (2nd child) semantically checked
-  ##    analysed
-  ## 2. nkError node over `n`, when a callable unary proposition isn't provided
-  if n.kind notin nkPragmaCallKinds or n.len != 2:
-    result = c.config.newError(n, SemReport(kind: rsemPropositionExpected))
-  else:
-    n[1] = c.semExpr(c, n[1])
-
-proc pragmaEnsures(c: PContext, n: PNode): PNode =
-  ## drnim - `ensures` pragma, must be a callable with single arg predicate,
-  ## producing either:
-  ## 1. mutated `n` with the the proposition (2nd child) semantically checked
-  ##    analysed, and if the current owner is a routineKind adds a `result`
-  ##    symbol.
-  ## 2. nkError node over `n`, when a callable unary proposition isn't provided
-  ##
-  ## xxx: 1. the implementation is unclear, we create a `result` symbol for
-  ##      routines, adding it to the a sub-scope with the routine as owner, but
-  ##      won't that potentially create a duplicate `result` symbol? or does
-  ##      that get resolved later?
-  ##      2. `routineKinds` includes template, so is that potentially an issue
-  ##      as well?
-  result = n
-  if n.kind notin nkPragmaCallKinds or n.len != 2:
-    result = c.config.newError(n, SemReport(kind: rsemPropositionExpected))
-  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"), nextSymId(c.idgen), 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:
@@ -1879,10 +1839,6 @@ proc prepareSinglePragma(
           sym.flags.incl sfUsed
       of wLiftLocals:
         result = it
-      of wRequires, wInvariant, wAssume, wAssert:
-        result = pragmaProposition(c, it)
-      of wEnsures:
-        result = pragmaEnsures(c, it)
       of wEnforceNoRaises:
         sym.flags.incl sfNeverRaises
       else:

compiler/sem/semmagic.nim

@@ -431,45 +431,6 @@ proc turnFinalizerIntoDestructor(c: PContext; orig: PSym; info: TLineInfo): PSym
   result.typ = newProcType(result.info, nextTypeId c.idgen, result)
   result.typ.addParam newParam
 
-proc semQuantifier(c: PContext; n: PNode): PNode =
-  checkSonsLen(n, 2, c.config)
-  openScope(c)
-  result = newNodeIT(n.kind, n.info, n.typ)
-  result.add n[0]
-  let args = n[1]
-  assert args.kind == nkArgList
-  for i in 0..args.len-2:
-    let it = args[i]
-    var valid = false
-    if it.kind == nkInfix:
-      let op = considerQuotedIdent(c, it[0])
-      if op.id == ord(wIn):
-        let v = newSymS(skForVar, it[1], c)
-        styleCheckDef(c.config, v)
-        onDef(it[1].info, v)
-        let domain = semExprWithType(c, it[2], {efWantIterator})
-        v.typ = domain.typ
-        valid = true
-        addDecl(c, v)
-        result.add newTree(nkInfix, it[0], newSymNode(v), domain)
-    if not valid:
-      localReport(c.config, n, reportSem rsemQuantifierInRangeExpected)
-  result.add forceBool(c, semExprWithType(c, args[^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:
-    localReport(c.config, n[1], reportSem rsemOldTakesParameterName)
-
-  elif n[1].sym.owner != getCurrOwner(c):
-    localReport(c.config, n[1].info, reportAst(
-      rsemOldDoesNotBelongTo, n[1], sym = getCurrOwner(c)))
-
-  result = n
-
 proc semPrivateAccess(c: PContext, n: PNode): PNode =
   let t = n[1].typ[0].toObjectFromRefPtrGeneric
   c.currentScope.allowPrivateAccess.add t.sym
@@ -574,10 +535,6 @@ proc magicsAfterOverloadResolution(c: PContext, n: PNode,
       result[0] = newSymNode(op)
   of mUnown:
     result = semUnown(c, n)
-  of mExists, mForall:
-    result = semQuantifier(c, n)
-  of mOld:
-    result = semOld(c, n)
   of mSetLengthSeq:
     result = n
     let seqType = result[1].typ.skipTypes({tyPtr, tyRef, # in case we had auto-dereferencing

compiler/sem/semparallel.nim

@@ -373,7 +373,6 @@ proc analyse(c: var AnalysisCtx; n: PNode) =
       # prevent direct assignments to the monotonic variable:
       let slot = c.getSlot(n[0].sym)
       slot.blacklisted = true
-    invalidateFacts(c.guards, n[0])
     let value = n[1]
     if getMagic(value) == mSpawn:
       pushSpawnId(c):