Skip to content

Commit

Permalink
.forbids pragma: defining forbidden tags (nim-lang#20050)
Browse files Browse the repository at this point in the history
* .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 <[email protected]>

* updated changelog

* corrected typo

Co-authored-by: ringabout <[email protected]>
  • Loading branch information
2 people authored and capocasa committed Mar 31, 2023
1 parent 13b8ec3 commit fc29a04
Show file tree
Hide file tree
Showing 24 changed files with 405 additions and 71 deletions.
2 changes: 2 additions & 0 deletions changelog.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
which 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).
Expand Down
3 changes: 2 additions & 1 deletion compiler/ast.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 3 additions & 1 deletion compiler/docgen.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
12 changes: 6 additions & 6 deletions compiler/pragmas.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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,
Expand All @@ -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,
Expand All @@ -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
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 3 additions & 1 deletion compiler/semcall.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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."
Expand Down Expand Up @@ -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
56 changes: 51 additions & 5 deletions compiler/sempass2.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand All @@ -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)

Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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}:
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 = @[]
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion compiler/semstmts.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 18 additions & 0 deletions compiler/types.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -1381,6 +1388,7 @@ type
efTagsUnknown
efLockLevelsDiffer
efEffectsDelayed
efTagsIllegal

proc compatibleEffects*(formal, actual: PType): EffectsCompat =
# for proc type compatibility checking:
Expand Down Expand Up @@ -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:

Expand Down Expand Up @@ -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 =
Expand Down
2 changes: 2 additions & 0 deletions compiler/vmops.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions compiler/wordrecg.nim
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -145,4 +145,4 @@ else:
for i in a..b:
if cmpIgnoreStyle($i, s) == 0:
return i
result = default
result = default
Loading

0 comments on commit fc29a04

Please sign in to comment.