From 7c700fd43b8474cac23e015c84954153229b6dde Mon Sep 17 00:00:00 2001 From: Juan Carlos Date: Wed, 22 Dec 2021 14:18:41 -0800 Subject: [PATCH] Remove DrNim --- compiler/modulegraphs.nim | 4 +- compiler/pragmas.nim | 78 ++++----------- compiler/semcall.nim | 4 +- compiler/sempass2.nim | 29 +----- compiler/sigmatch.nim | 4 +- compiler/wordrecg.nim | 2 - doc/drnim.rst | 205 -------------------------------------- doc/rstcommon.rst | 2 +- tools/koch/koch.nim | 26 ----- 9 files changed, 24 insertions(+), 330 deletions(-) delete mode 100644 doc/drnim.rst diff --git a/compiler/modulegraphs.nim b/compiler/modulegraphs.nim index de34e739ef4..f63110c5227 100644 --- a/compiler/modulegraphs.nim +++ b/compiler/modulegraphs.nim @@ -419,7 +419,7 @@ proc registerModule*(g: ModuleGraph; m: PSym) = g.ifaces[m.position] = Iface(module: m, converters: @[], patterns: @[], uniqueName: rope(uniqueModuleName(g.config, FileIndex(m.position)))) - + initStrTables(g, m) proc registerModuleById*(g: ModuleGraph; m: FileIndex) = @@ -427,7 +427,7 @@ proc registerModuleById*(g: ModuleGraph; m: FileIndex) = 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) diff --git a/compiler/pragmas.nim b/compiler/pragmas.nim index 8cc684071b7..5e3d87b0b31 100644 --- a/compiler/pragmas.nim +++ b/compiler/pragmas.nim @@ -31,7 +31,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, @@ -42,7 +42,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, @@ -55,11 +55,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} 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, @@ -79,8 +79,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} @@ -118,45 +117,6 @@ proc newIllegalCustomPragmaNode*(c: PContext; n: PNode, s: PSym): PNode = ## create an error node (`nkError`) for an illegal custom pragma error newError(n, IllegalCustomPragma, newSymNode(s)) -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 = newError(n, "proposition expected") - 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 = newError(n, "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"), 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: @@ -277,7 +237,7 @@ proc getStrLitNode(c: PContext, n: PNode): PNode = # for pragmas prior to changing, but we're meant to return n[1], yet # on error we return a wrapped `n`, that's the wrong level of AST. newError(n, StringLiteralExpected) - + proc strLitToStrOrErr(c: PContext, n: PNode): (string, PNode) = ## extracts the string from an string literal, or errors if it's not a string @@ -288,7 +248,7 @@ proc strLitToStrOrErr(c: PContext, n: PNode): (string, PNode) = (r.strVal, nil) of nkError: ("", r) - else: + else: ("", newError(n, errStringLiteralExpected)) proc intLitToIntOrErr(c: PContext, n: PNode): (int, PNode) = @@ -355,7 +315,7 @@ proc isTurnedOn(c: PContext, n: PNode): (bool, PNode) = (x.intVal != 0, nil) else: (false, newError(n, "'on' or 'off' expected")) - else: + else: (false, newError(n, "'on' or 'off' expected")) proc onOff(c: PContext, n: PNode, op: TOptions, resOptions: var TOptions): PNode = @@ -474,7 +434,7 @@ proc processNote(c: PContext, n: PNode): PNode = if x.kind == nkIntLit and x.intVal != 0: incl(notes, nk) else: excl(notes, nk) n - + let validPragma = n.kind in nkPragmaCallKinds and n.len == 2 exp = @@ -485,7 +445,7 @@ proc processNote(c: PContext, n: PNode): PNode = bracketExpr = if useExp: exp else: newInvalidPragmaNode(c, n) - + result = if isBracketExpr: var nk: TNoteKind @@ -694,7 +654,7 @@ proc relativeFile(c: PContext; name: string, info: TLineInfo; proc processCompile(c: PContext, n: PNode): PNode = ## compile pragma ## produces (mutates) `n`, which must be a callable, analysing its arg, or returning - ## `n` wrapped in an error. + ## `n` wrapped in an error. result = n proc docompile(c: PContext; it: PNode; src, dest: AbsoluteFile; customArgs: string) = var cf = Cfile(nimname: splitFile(src).name, @@ -1109,7 +1069,7 @@ proc prepareSinglePragma( ): PNode = ## given a `sym`bol with pragmas `n`, check and prepare `i`'th pragma, if ## it's a single valid pragma, where valid is a kind within `validPragmas`. - ## + ## ## With special handling for: ## * comes from a push ## * whether it's `isStatement` @@ -1185,7 +1145,7 @@ proc prepareSinglePragma( if extLit.kind == nkError: result = it else: - let ext = extLit.strVal + let ext = extLit.strVal case makeExternExport(c, sym, ext) of ExternNameSet: if k == wExportCpp: @@ -1410,7 +1370,7 @@ proc prepareSinglePragma( incl(sym.flags, sfGeneratedOp) of wNosinks: result = noVal(c, it) - incl(sym.flags, sfWasForwarded) + incl(sym.flags, sfWasForwarded) of wDynlib: result = processDynLib(c, it, sym) of wCompilerProc, wCore: @@ -1497,7 +1457,7 @@ proc prepareSinglePragma( if sym.kind != skType: incl(sym.flags, sfThread) if sym.typ != nil: incl(sym.typ.flags, tfGcSafe) - else: + else: result = newInvalidPragmaNode(c, it) else: discard "no checking if used as a code block" @@ -1562,7 +1522,7 @@ proc prepareSinglePragma( result = if err.isNil: extccomp.addLinkOption(c.config, s) - recordPragma(c, it, "passl", s) + recordPragma(c, it, "passl", s) it else: err @@ -1777,13 +1737,9 @@ 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: + else: result = newInvalidPragmaNode(c, it) elif comesFromPush and whichKeyword(ident) != wInvalid: discard "ignore the .push pragma; it doesn't apply" diff --git a/compiler/semcall.nim b/compiler/semcall.nim index 27306b8b5e4..260396d70d3 100644 --- a/compiler/semcall.nim +++ b/compiler/semcall.nim @@ -159,9 +159,7 @@ 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." - 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 diff --git a/compiler/sempass2.nim b/compiler/sempass2.nim index 0086b53767c..e834b2d5d6d 100644 --- a/compiler/sempass2.nim +++ b/compiler/sempass2.nim @@ -1310,10 +1310,6 @@ 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: @@ -1344,13 +1340,6 @@ 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 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 if s != nil and s.magic != mNone: if s.magic != mEcho: @@ -1374,10 +1363,7 @@ proc initEffects(g: ModuleGraph; effects: PNode; s: PSym; t: var TEffects; c: PC t.init = @[] t.guards.s = @[] t.guards.g = g - when defined(drnim): - t.currOptions = g.config.options + s.options - {optStaticBoundsCheck} - else: - t.currOptions = g.config.options + s.options + t.currOptions = g.config.options + s.options t.guards.beSmart = optStaticBoundsCheck in t.currOptions t.locked = @[] t.graph = g @@ -1443,14 +1429,6 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) = else: effects[tagEffects] = t.tags - 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 - var mutationInfo = MutationInfo() var hasMutationSideEffect = false if {strictFuncs, views} * c.features != {}: @@ -1494,8 +1472,7 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) = message(g.config, s.info, warnLockLevel, "declared lock level is $1, but real lock level is $2" % [$s.typ.lockLevel, $t.maxLockLevel]) - when defined(drnim): - if c.graph.strongSemCheck != nil: c.graph.strongSemCheck(c.graph, s, body) + when defined(useDfa): if s.name.s == "testp": dataflowAnalysis(s, body) @@ -1514,5 +1491,3 @@ proc trackStmt*(c: PContext; module: PSym; n: PNode, isTopLevel: bool) = initEffects(g, effects, module, t, c) t.isTopLevel = isTopLevel track(t, n) - when defined(drnim): - if c.graph.strongSemCheck != nil: c.graph.strongSemCheck(c.graph, module, n) diff --git a/compiler/sigmatch.nim b/compiler/sigmatch.nim index 125e076b1ec..f4cd43f2abd 100644 --- a/compiler/sigmatch.nim +++ b/compiler/sigmatch.nim @@ -28,7 +28,7 @@ type TCandidateState* = enum csEmpty, csMatch, csNoMatch - + CandidateDiagnostic* = PNode ## PNode is only ever an `nkError` kind, often converted to a string for ## display purpopses @@ -638,8 +638,6 @@ proc procTypeRel(c: var TCandidate, f, a: PType): TTypeRelation = 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 diff --git a/compiler/wordrecg.nim b/compiler/wordrecg.nim index 22f6cc71dee..dee659111a1 100644 --- a/compiler/wordrecg.nim +++ b/compiler/wordrecg.nim @@ -71,8 +71,6 @@ 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", wDeadCodeElimUnused = "deadCodeElim", # deprecated, dead code elim always happens wSafecode = "safecode", wPackage = "package", wNoForward = "noforward", wReorder = "reorder", wNoRewrite = "norewrite", wNoDestroy = "nodestroy", wPragma = "pragma", diff --git a/doc/drnim.rst b/doc/drnim.rst deleted file mode 100644 index 070cd17871f..00000000000 --- a/doc/drnim.rst +++ /dev/null @@ -1,205 +0,0 @@ -=================================== - DrNim User Guide -=================================== - -:Author: Andreas Rumpf -:Version: |nimversion| - -.. default-role:: code -.. include:: rstcommon.rst -.. contents:: - - -Introduction -============ - -This document describes the usage of the *DrNim* tool. DrNim combines -the Nim frontend with the `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`:cmd:, 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. - -.. code-block:: nim - - import std / logic - - proc insertionSort(a: var openArray[int]) {. - ensures: forall(i in 1.. 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..`. -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 = '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`. - -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`. diff --git a/doc/rstcommon.rst b/doc/rstcommon.rst index 7f37f3fed0f..3ebd7f540f2 100644 --- a/doc/rstcommon.rst +++ b/doc/rstcommon.rst @@ -32,7 +32,7 @@ .. |nim| replace:: nim .. |nimskull| replace:: nimskull .. |nimsuggest| replace:: nimsuggest -.. |drnim| replace:: drnim + .. define language roles explicitly (for compatibility with rst2html.py): diff --git a/tools/koch/koch.nim b/tools/koch/koch.nim index c1abc1abfd8..6970ec54d23 100644 --- a/tools/koch/koch.nim +++ b/tools/koch/koch.nim @@ -9,9 +9,6 @@ # See doc/koch.txt for documentation. # -when not defined(windows): - const - Z3StableCommit = "65de3f748a6812eecd7db7c478d5fc54424d368b" # the version of Z3 that DrNim uses when defined(gcc) and defined(windows): when defined(x86): @@ -553,28 +550,6 @@ proc icTest(args: string) = exec(cmd) inc i -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") - nimexecFold("build drnim", "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") - nimexecFold("build drnim", "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" % @@ -718,7 +693,6 @@ when isMainModule: quit "use this instead: https://github.com/nim-lang/csources_v1/blob/master/push_c_code.nim" of "valgrind": valgrind(op.cmdLineRest) of "c2nim": bundleC2nim(op.cmdLineRest) - of "drnim": buildDrNim(op.cmdLineRest) of "ic": icTest(op.cmdLineRest) of "branchdone": branchDone() else: showHelp(success = false)