.forbids pragma: defining forbidden tags (#20050)

* .forbids pragma: defining illegal effects for proc types

This patch intends to define the opposite of the .tags pragma: a way to define effects which are not allowed in a proc.

* updated documentation and changelogs for the forbids pragma

* renamed notTagEffects to forbiddenEffects

* corrected issues of forbids pragma

the forbids pragma didn't handle simple restrictions properly and it also had issues with subtyping

* removed incorrect character from changelog

* added test to cover the interaction of methods and the forbids pragma

* covering the interaction of the tags and forbids pragmas

* updated manual about the forbids pragma

* removed useless statement

* corrected the subtyping of proc types using the forbids pragma

* updated manual for the forbids pragma

* updated documentations for forbids pragma

* updated nim docs

* updated docs with rsttester.nim

* regenerated documentation

* updated rst docs

* Update changelog.md

Co-authored-by: ringabout <43030857+ringabout@users.noreply.github.com>

* updated changelog

* corrected typo

Co-authored-by: ringabout <43030857+ringabout@users.noreply.github.com>
This commit is contained in:
Lancer11211 2022-07-26 07:40:49 +02:00 • committed by GitHub
commit efd5c571bf
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
24 changed files with 405 additions and 71 deletions

View file

@ -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

View file

@ -1212,8 +1212,9 @@ 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
@ -1221,6 +1222,7 @@ proc documentRaises*(cache: IdentCache; n: PNode) =
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.

View file

@ -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)

View file

@ -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 caught 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

View file

@ -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,7 +1296,7 @@ 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()
@ -1282,8 +1304,11 @@ proc checkRaisesSpec(g: ModuleGraph; emitWarnings: bool; spec, real: PNode, msg:
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

View file

@ -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

View file

@ -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,14 @@ 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 0 == real.len:
return efTagsUnknown
elif hasIncompatibleEffect(sn, real[tagEffects]):
return efTagsIllegal
if formal.lockLevel.ord < 0 or
actual.lockLevel.ord <= formal.lockLevel.ord:
@ -1627,6 +1643,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 =

View file

@ -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)

View file

@ -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