.forbids pragma: defining forbidden tags

changelog.md

@@ -67,6 +67,8 @@ becomes an alias for `addr`.
 
 ## Language changes
 
+- [Tag tracking](manual.html#tag-tracking) supports the definition of forbidden tags by the `.forbids` pragma
+  it can be used to disable certain effects in proc types
 - [Case statement macros](manual.html#macros-case-statement-macros) are no longer experimental,
   meaning you no longer need to enable the experimental switch `caseStmtMacros` to use them.
 - Templates now accept [macro pragmas](https://nim-lang.github.io/Nim/manual.html#userminusdefined-pragmas-macro-pragmas).

compiler/ast.nim

@@ -347,7 +347,8 @@ const
   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
+  forbiddenEffects* = 5    # list of illegal effects
+  effectListLen* = 6    # list of effects list
   nkLastBlockStmts* = {nkRaiseStmt, nkReturnStmt, nkBreakStmt, nkContinueStmt}
                         # these must be last statements in a block
 

compiler/docgen.nim

@@ -1212,15 +1212,17 @@ proc documentRaises*(cache: IdentCache; n: PNode) =
   let p3 = documentWriteEffect(cache, n, sfWrittenTo, "writes")
   let p4 = documentNewEffect(cache, n)
   let p5 = documentWriteEffect(cache, n, sfEscapes, "escapes")
+  let p6 = documentEffect(cache, n, pragmas, wForbids, forbiddenEffects)
 
-  if p1 != nil or p2 != nil or p3 != nil or p4 != nil or p5 != nil:
+  if p1 != nil or p2 != nil or p3 != nil or p4 != nil or p5 != nil or p6 != nil:
     if pragmas.kind == nkEmpty:
       n[pragmasPos] = newNodeI(nkPragma, n.info)
     if p1 != nil: n[pragmasPos].add p1
     if p2 != nil: n[pragmasPos].add p2
     if p3 != nil: n[pragmasPos].add p3
     if p4 != nil: n[pragmasPos].add p4
     if p5 != nil: n[pragmasPos].add p5
+    if p6 != nil: n[pragmasPos].add p6
 
 proc generateDoc*(d: PDoc, n, orig: PNode, docFlags: DocFlags = kDefault) =
   ## Goes through nim nodes recursively and collects doc comments.

compiler/pragmas.nim

@@ -32,7 +32,7 @@ const
     wCompilerProc, wNonReloadable, wCore, wProcVar, wVarargs, wCompileTime, wMerge,
     wBorrow, wImportCompilerProc, wThread,
     wAsmNoStackFrame, wDiscardable, wNoInit, wCodegenDecl,
-    wGensym, wInject, wRaises, wEffectsOf, wTags, wLocks, wDelegator, wGcSafe,
+    wGensym, wInject, wRaises, wEffectsOf, wTags, wForbids, wLocks, wDelegator, wGcSafe,
     wConstructor, wLiftLocals, wStackTrace, wLineTrace, wNoDestroy,
     wRequires, wEnsures, wEnforceNoRaises}
   converterPragmas* = procPragmas
@@ -45,7 +45,7 @@ const
   iteratorPragmas* = declPragmas + {FirstCallConv..LastCallConv, wNoSideEffect, wSideEffect,
     wMagic, wBorrow,
     wDiscardable, wGensym, wInject, wRaises, wEffectsOf,
-    wTags, wLocks, wGcSafe, wRequires, wEnsures}
+    wTags, wForbids, wLocks, wGcSafe, wRequires, wEnsures}
   exprPragmas* = {wLine, wLocks, wNoRewrite, wGcSafe, wNoSideEffect}
   stmtPragmas* = {
     wHint, wWarning, wError,
@@ -65,7 +65,7 @@ const
   lambdaPragmas* = {FirstCallConv..LastCallConv,
     wNoSideEffect, wSideEffect, wNoreturn, wNosinks, wDynlib, wHeader,
     wThread, wAsmNoStackFrame,
-    wRaises, wLocks, wTags, wRequires, wEnsures, wEffectsOf,
+    wRaises, wLocks, wTags, wForbids, wRequires, wEnsures, wEffectsOf,
     wGcSafe, wCodegenDecl, wNoInit, wCompileTime}
   typePragmas* = declPragmas + {wMagic, wAcyclic,
     wPure, wHeader, wCompilerProc, wCore, wFinal, wSize, wShallow,
@@ -85,7 +85,7 @@ const
   paramPragmas* = {wNoalias, wInject, wGensym}
   letPragmas* = varPragmas
   procTypePragmas* = {FirstCallConv..LastCallConv, wVarargs, wNoSideEffect,
-                      wThread, wRaises, wEffectsOf, wLocks, wTags, wGcSafe,
+                      wThread, wRaises, wEffectsOf, wLocks, wTags, wForbids, wGcSafe,
                       wRequires, wEnsures}
   forVarPragmas* = {wInject, wGensym}
   allRoutinePragmas* = methodPragmas + iteratorPragmas + lambdaPragmas
@@ -820,7 +820,7 @@ proc singlePragma(c: PContext, sym: PSym, n: PNode, i: var int,
     elif not isStatement:
       localError(c.config, n.info, "'cast' pragma only allowed in a statement context")
     case whichPragma(key[1])
-    of wRaises, wTags: pragmaRaisesOrTags(c, key[1])
+    of wRaises, wTags, wForbids: pragmaRaisesOrTags(c, key[1])
     else: discard
     return
   elif key.kind notin nkIdentKinds:
@@ -1184,7 +1184,7 @@ proc singlePragma(c: PContext, sym: PSym, n: PNode, i: var int,
         noVal(c, it)
         if sym == nil: invalidPragma(c, it)
       of wLine: pragmaLine(c, it)
-      of wRaises, wTags: pragmaRaisesOrTags(c, it)
+      of wRaises, wTags, wForbids: pragmaRaisesOrTags(c, it)
       of wLocks:
         if sym == nil: pragmaLockStmt(c, it)
         elif sym.typ == nil: invalidPragma(c, it)

compiler/semcall.nim

@@ -154,6 +154,8 @@ proc effectProblem(f, a: PType; result: var string; c: PContext) =
             "proc with {.locks: 0.} to get extended error information."
       of efEffectsDelayed:
         result.add "\n  The `.effectsOf` annotations differ."
+      of efTagsIllegal:
+        result.add "\n  The `.forbids` requirements catched an illegal tag."
       when defined(drnim):
         if not c.graph.compatibleProps(c.graph, f, a):
           result.add "\n  The `.requires` or `.ensures` properties are incompatible."
@@ -730,4 +732,4 @@ proc searchForBorrowProc(c: PContext, startScope: PScope, fn: PSym): PSym =
         result = nil
       elif result.magic in {mArrPut, mArrGet}:
         # cannot borrow these magics for now
-        result = nil
+        result = nil

compiler/sempass2.nim

@@ -66,6 +66,7 @@ type
   TEffects = object
     exc: PNode  # stack of exceptions
     tags: PNode # list of tags
+    forbids: PNode # list of tags
     bottom, inTryStmt, inExceptOrFinallyStmt, leftPartOfAsgn: int
     owner: PSym
     ownerModule: PSym
@@ -388,6 +389,12 @@ proc addTag(a: PEffects, e, comesFrom: PNode) =
     if sameType(aa[i].typ.skipTypes(skipPtrs), e.typ.skipTypes(skipPtrs)): return
   throws(a.tags, e, comesFrom)
 
+proc addNotTag(a: PEffects, e, comesFrom: PNode) =
+  var aa = a.forbids
+  for i in 0..<aa.len:
+    if sameType(aa[i].typ.skipTypes(skipPtrs), e.typ.skipTypes(skipPtrs)): return
+  throws(a.forbids, e, comesFrom)
+
 proc mergeRaises(a: PEffects, b, comesFrom: PNode) =
   if b.isNil:
     addRaiseEffect(a, createRaise(a.graph, comesFrom), comesFrom)
@@ -403,6 +410,7 @@ proc mergeTags(a: PEffects, b, comesFrom: PNode) =
 proc listEffects(a: PEffects) =
   for e in items(a.exc):  message(a.config, e.info, hintUser, typeToString(e.typ))
   for e in items(a.tags): message(a.config, e.info, hintUser, typeToString(e.typ))
+  for e in items(a.forbids): message(a.config, e.info, hintUser, typeToString(e.typ))
   #if a.maxLockLevel != 0:
   #  message(e.info, hintUser, "lockLevel: " & a.maxLockLevel)
 
@@ -604,7 +612,7 @@ proc isOwnedProcVar(tracked: PEffects; n: PNode): bool =
 
 proc isNoEffectList(n: PNode): bool {.inline.} =
   assert n.kind == nkEffectList
-  n.len == 0 or (n[tagEffects] == nil and n[exceptionEffects] == nil)
+  n.len == 0 or (n[tagEffects] == nil and n[exceptionEffects] == nil and n[forbiddenEffects] == nil)
 
 proc isTrival(caller: PNode): bool {.inline.} =
   result = caller.kind == nkSym and caller.sym.magic in {mEqProc, mIsNil, mMove, mWasMoved, mSwap}
@@ -924,14 +932,17 @@ type
     oldLocked: int
     oldLockLevel: TLockLevel
     enforcedGcSafety, enforceNoSideEffects: bool
-    oldExc, oldTags: int
-    exc, tags: PNode
+    oldExc, oldTags, oldForbids: int
+    exc, tags, forbids: PNode
 
 proc createBlockContext(tracked: PEffects): PragmaBlockContext =
+  var oldForbidsLen = 0
+  if tracked.forbids != nil: oldForbidsLen = tracked.forbids.len
   result = PragmaBlockContext(oldLocked: tracked.locked.len,
     oldLockLevel: tracked.currLockLevel,
     enforcedGcSafety: false, enforceNoSideEffects: false,
-    oldExc: tracked.exc.len, oldTags: tracked.tags.len)
+    oldExc: tracked.exc.len, oldTags: tracked.tags.len,
+    oldForbids: oldForbidsLen)
 
 proc applyBlockContext(tracked: PEffects, bc: PragmaBlockContext) =
   if bc.enforcedGcSafety: tracked.inEnforcedGcSafe = true
@@ -952,6 +963,10 @@ proc unapplyBlockContext(tracked: PEffects; bc: PragmaBlockContext) =
     setLen(tracked.tags.sons, bc.oldTags)
     for t in bc.tags:
       addTag(tracked, t, t)
+  if bc.forbids != nil:
+    setLen(tracked.forbids.sons, bc.oldForbids)
+    for t in bc.forbids:
+      addNotTag(tracked, t, t)
 
 proc castBlock(tracked: PEffects, pragma: PNode, bc: var PragmaBlockContext) =
   case whichPragma(pragma)
@@ -966,6 +981,13 @@ proc castBlock(tracked: PEffects, pragma: PNode, bc: var PragmaBlockContext) =
     else:
       bc.tags = newNodeI(nkArgList, pragma.info)
       bc.tags.add n
+  of wForbids:
+    let n = pragma[1]
+    if n.kind in {nkCurly, nkBracket}:
+      bc.forbids = n
+    else:
+      bc.forbids = newNodeI(nkArgList, pragma.info)
+      bc.forbids.add n
   of wRaises:
     let n = pragma[1]
     if n.kind in {nkCurly, nkBracket}:
@@ -1274,16 +1296,19 @@ proc subtypeRelation(g: ModuleGraph; spec, real: PNode): bool =
 
 proc checkRaisesSpec(g: ModuleGraph; emitWarnings: bool; spec, real: PNode, msg: string, hints: bool;
                      effectPredicate: proc (g: ModuleGraph; a, b: PNode): bool {.nimcall.};
-                     hintsArg: PNode = nil) =
+                     hintsArg: PNode = nil; isForbids: bool = false) =
   # check that any real exception is listed in 'spec'; mark those as used;
   # report any unused exception
   var used = initIntSet()
   for r in items(real):
     block search:
       for s in 0..<spec.len:
         if effectPredicate(g, spec[s], r):
+          if isForbids: break
           used.incl(s)
           break search
+        if isForbids:
+          break search
       # XXX call graph analysis would be nice here!
       pushInfoContext(g.config, spec.info)
       var rr = if r.kind == nkRaiseStmt: r[0] else: r
@@ -1312,6 +1337,10 @@ proc checkMethodEffects*(g: ModuleGraph; disp, branch: PSym) =
   if not isNil(tagsSpec):
     checkRaisesSpec(g, false, tagsSpec, actual[tagEffects],
       "can have an unlisted effect: ", hints=off, subtypeRelation)
+  let forbidsSpec = effectSpec(p, wForbids)
+  if not isNil(forbidsSpec):
+    checkRaisesSpec(g, false, forbidsSpec, actual[tagEffects],
+      "has an illegal effect: ", hints=off, subtypeRelation, isForbids=true)
   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)
@@ -1349,6 +1378,12 @@ proc setEffectsForProcType*(g: ModuleGraph; t: PType, n: PNode; s: PSym = nil) =
     elif s != nil and (s.magic != mNone or {sfImportc, sfExportc} * s.flags == {sfImportc}):
       effects[tagEffects] = newNodeI(nkArgList, effects.info)
 
+    let forbidsSpec = effectSpec(n, wForbids)
+    if not isNil(forbidsSpec):
+      effects[forbiddenEffects] = forbidsSpec
+    elif s != nil and (s.magic != mNone or {sfImportc, sfExportc} * s.flags == {sfImportc}):
+      effects[forbiddenEffects] = newNodeI(nkArgList, effects.info)
+
     let requiresSpec = propSpec(n, wRequires)
     if not isNil(requiresSpec):
       effects[requiresEffects] = requiresSpec
@@ -1365,6 +1400,7 @@ proc rawInitEffects(g: ModuleGraph; effects: PNode) =
   newSeq(effects.sons, effectListLen)
   effects[exceptionEffects] = newNodeI(nkArgList, effects.info)
   effects[tagEffects] = newNodeI(nkArgList, effects.info)
+  effects[forbiddenEffects] = newNodeI(nkArgList, effects.info)
   effects[requiresEffects] = g.emptyNode
   effects[ensuresEffects] = g.emptyNode
   effects[pragmasEffects] = g.emptyNode
@@ -1374,6 +1410,7 @@ proc initEffects(g: ModuleGraph; effects: PNode; s: PSym; t: var TEffects; c: PC
 
   t.exc = effects[exceptionEffects]
   t.tags = effects[tagEffects]
+  t.forbids = effects[forbiddenEffects]
   t.owner = s
   t.ownerModule = s.getModule
   t.init = @[]
@@ -1448,6 +1485,15 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) =
   else:
     effects[tagEffects] = t.tags
 
+  let forbidsSpec = effectSpec(p, wForbids)
+  if not isNil(forbidsSpec):
+    checkRaisesSpec(g, false, forbidsSpec, t.tags, "has an illegal effect: ",
+                    hints=off, subtypeRelation, isForbids=true)
+    # after the check, use the formal spec:
+    effects[forbiddenEffects] = forbidsSpec
+  else:
+    effects[forbiddenEffects] = t.forbids
+
   let requiresSpec = propSpec(p, wRequires)
   if not isNil(requiresSpec):
     effects[requiresEffects] = requiresSpec

compiler/semstmts.nim

@@ -2300,7 +2300,7 @@ proc semPragmaBlock(c: PContext, n: PNode): PNode =
   for p in pragmaList:
     if whichPragma(p) == wCast:
       case whichPragma(p[1])
-      of wGcSafe, wNoSideEffect, wTags, wRaises:
+      of wGcSafe, wNoSideEffect, wTags, wForbids, wRaises:
         discard "handled in sempass2"
       of wUncheckedAssign:
         inUncheckedAssignSection = 1

compiler/types.nim

@@ -1372,6 +1372,13 @@ proc compatibleEffectsAux(se, re: PNode): bool =
       return false
   result = true
 
+proc hasIncompatibleEffect(se, re: PNode): bool =
+  if re.isNil: return false
+  for r in items(re):
+    for s in items(se):
+      if safeInheritanceDiff(r.typ, s.typ) != high(int):
+        return true
+
 type
   EffectsCompat* = enum
     efCompat
@@ -1381,6 +1388,7 @@ type
     efTagsUnknown
     efLockLevelsDiffer
     efEffectsDelayed
+    efTagsIllegal
 
 proc compatibleEffects*(formal, actual: PType): EffectsCompat =
   # for proc type compatibility checking:
@@ -1414,6 +1422,13 @@ proc compatibleEffects*(formal, actual: PType): EffectsCompat =
       if not res:
         #if tfEffectSystemWorkaround notin actual.flags:
         return efTagsDiffer
+
+    let sn = spec[forbiddenEffects]
+    if not isNil(sn) and sn.kind != nkArgList:
+      if hasIncompatibleEffect(sn, real[tagEffects]):
+        writeFile("/tmp/x.log", $formal & "\n" & $real[tagEffects])
+        return efTagsIllegal
+
   if formal.lockLevel.ord < 0 or
       actual.lockLevel.ord <= formal.lockLevel.ord:
 
@@ -1627,6 +1642,8 @@ proc typeMismatch*(conf: ConfigRef; info: TLineInfo, formal, actual: PType, n: P
         msg.add "\nlock levels differ"
       of efEffectsDelayed:
         msg.add "\n.effectsOf annotations differ"
+      of efTagsIllegal:
+        msg.add "\n.notTag catched an illegal effect"
     localError(conf, info, msg)
 
 proc isTupleRecursive(t: PType, cycleDetector: var IntSet): bool =

compiler/vmops.nim

@@ -324,6 +324,8 @@ proc registerAdditionalOps*(c: PCtx) =
     getEffectList(c, a, exceptionEffects)
   registerCallback c, "stdlib.effecttraits.getTagsListImpl", proc (a: VmArgs) =
     getEffectList(c, a, tagEffects)
+  registerCallback c, "stdlib.effecttraits.getForbidsListImpl", proc (a: VmArgs) =
+    getEffectList(c, a, forbiddenEffects)
 
   registerCallback c, "stdlib.effecttraits.isGcSafeImpl", proc (a: VmArgs) =
     let fn = getNode(a, 0)

compiler/wordrecg.nim

@@ -71,7 +71,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",
+    wForbids = "forbids", wRequires = "requires", wEnsures = "ensures", wInvariant = "invariant",
     wAssume = "assume", wAssert = "assert",
     wDeadCodeElimUnused = "deadCodeElim",  # deprecated, dead code elim always happens
     wSafecode = "safecode", wPackage = "package", wNoForward = "noforward", wReorder = "reorder",
@@ -145,4 +145,4 @@ else:
     for i in a..b:
       if cmpIgnoreStyle($i, s) == 0:
         return i
-    result = default
+    result = default

doc/manual.md

@@ -4945,7 +4945,7 @@ means to *tag* a routine and to perform checks against this tag:
   type IO = object ## input/output effect
   proc readLine(): string {.tags: [IO].} = discard
 
-  proc no_IO_please() {.tags: [].} =
+  proc no_effects_please() {.tags: [].} =
     # the compiler prevents this:
     let x = readLine()
 
@@ -4955,6 +4955,33 @@ also be attached to a proc type. This affects type compatibility.
 The inference for tag tracking is analogous to the inference for
 exception tracking.
 
+There is also a way which can be used to forbid certain effects:
+
+.. code-block:: nim
+    :test: "nim c --warningAsError:Effect:on $1"
+    :status: 1
+
+  type IO = object ## input/output effect
+  proc readLine(): string {.tags: [IO].} = discard
+  proc echoLine(): void = discard
+
+  proc no_IO_please() {.forbids: [IO].} =
+    # this is OK because it didn't define any tag:
+    echoLine()
+    # the compiler prevents this:
+    let y = readLine()
+
+The `forbids` pragma defines a list if illegal effects - proc types not using that effect are all valid use cases.
+
+In the example below, the `ProcType1` procedure type is a subtype of `ProcType1`:
+
+.. code-block:: nim
+  type MyEffect = object
+  type ProcType1 = proc (i: int) {.forbids: [MyEffect].}
+  type ProcType2 = proc (i: int)
+
+Calling `ProcType2` in place of `ProcType1` is valid because `ProcType2` doesn't support any tag, and thus it doesn't allow `MyEffect` either.
+
 
 Side effects
 ------------