diff --git a/compiler/ast/ast_types.nim b/compiler/ast/ast_types.nim index 79f0ad97800..8704c693bf3 100644 --- a/compiler/ast/ast_types.nim +++ b/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, diff --git a/compiler/ast/reports.nim b/compiler/ast/reports.nim index 8a32d1472e4..c87731d0782 100644 --- a/compiler/ast/reports.nim +++ b/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 diff --git a/compiler/ast/trees.nim b/compiler/ast/trees.nim index baf6460d54b..8bd212e78fc 100644 --- a/compiler/ast/trees.nim +++ b/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.. " & $b of rsemInvalidGuardField: result = "invalid guard field: " & r.symstr diff --git a/compiler/modules/modulegraphs.nim b/compiler/modules/modulegraphs.nim index eb092035fd0..f5a21429ad4 100644 --- a/compiler/modules/modulegraphs.nim +++ b/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) diff --git a/compiler/sem/guards.nim b/compiler/sem/guards.nim index 645231e653f..dba7791f7df 100644 --- a/compiler/sem/guards.nim +++ b/compiler/sem/guards.nim @@ -474,30 +474,6 @@ proc hasSubTree(n, x: PNode): bool = for i in 0..= 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) diff --git a/compiler/sem/pragmas.nim b/compiler/sem/pragmas.nim index 291c8d85e11..6bdb1a2967b 100644 --- a/compiler/sem/pragmas.nim +++ 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: diff --git a/compiler/sem/semmagic.nim b/compiler/sem/semmagic.nim index 50071d55c61..486931b1d81 100644 --- a/compiler/sem/semmagic.nim +++ b/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 diff --git a/compiler/sem/semparallel.nim b/compiler/sem/semparallel.nim index ddccf20ea8c..674e8336056 100644 --- a/compiler/sem/semparallel.nim +++ b/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): diff --git a/compiler/sem/sempass2.nim b/compiler/sem/sempass2.nim index 1b6f12ac31a..d8a555fc0cc 100644 --- a/compiler/sem/sempass2.nim +++ b/compiler/sem/sempass2.nim @@ -741,7 +741,6 @@ proc trackOperandForIndirectCall(tracked: PEffects, n: PNode, formals: PType; ar markSideEffect(tracked, a, n.info) let paramType = if formals != nil and argIndex < formals.len: formals[argIndex] else: nil if paramType != nil and paramType.kind in {tyVar}: - invalidateFacts(tracked.guards, n) if n.kind == nkSym and isLocalVar(tracked, n.sym): makeVolatile(tracked, n.sym) if paramType != nil and paramType.kind == tyProc and tfGcSafe in paramType.flags: @@ -845,36 +844,18 @@ proc cstringCheck(tracked: PEffects; n: PNode) = a.typ.kind == tyString and a.kind notin {nkStrLit..nkTripleStrLit}): localReport(tracked.config, n.info, reportAst(rsemWarnUnsafeCode, n)) -proc patchResult(c: PEffects; n: PNode) = - if n.kind == nkSym and n.sym.kind == skResult: - let fn = c.owner - if fn != nil and fn.kind in routineKinds and fn.ast != nil and resultPos < fn.ast.len: - n.sym = fn.ast[resultPos].sym - else: - localReport(c.config, n.info, reportSem(rsemDrNimRequiresUsesMissingResult)) - else: - for i in 0.. disp.typ.lockLevel: when true: localReport(g.config, branch.info, reportSymbols( @@ -1453,13 +1428,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: @@ -1469,8 +1437,6 @@ proc rawInitEffects(g: ModuleGraph; effects: PNode) = newSeq(effects.sons, effectListLen) effects[exceptionEffects] = newNodeI(nkArgList, effects.info) effects[tagEffects] = newNodeI(nkArgList, effects.info) - effects[requiresEffects] = g.emptyNode - effects[ensuresEffects] = g.emptyNode effects[pragmasEffects] = g.emptyNode proc initEffects(g: ModuleGraph; effects: PNode; s: PSym; t: var TEffects; c: PContext) = @@ -1483,10 +1449,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 @@ -1553,14 +1516,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 != {}: @@ -1620,8 +1575,6 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) = kind: rsemLockLevelMismatch, lockMismatch: ($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) @@ -1648,5 +1601,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/sem/sigmatch.nim b/compiler/sem/sigmatch.nim index fc73181425e..ac3d625aa93 100644 --- a/compiler/sem/sigmatch.nim +++ b/compiler/sem/sigmatch.nim @@ -624,9 +624,8 @@ proc procTypeRel(c: var TCandidate, f, a: PType): TTypeRelation = result = getProcConvMismatch(c.c.config, f, a, result)[1] 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 + if compatibleEffects(f, a) != efCompat: + return isNone of tyNil: result = f.allowsNil 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..93379dd9452 100644 --- a/doc/rstcommon.rst +++ b/doc/rstcommon.rst @@ -32,7 +32,6 @@ .. |nim| replace:: nim .. |nimskull| replace:: nimskull .. |nimsuggest| replace:: nimsuggest -.. |drnim| replace:: drnim .. define language roles explicitly (for compatibility with rst2html.py): @@ -64,4 +63,3 @@ .. role:: program(code) .. role:: option(code) - diff --git a/drnim/drnim.nim b/drnim/drnim.nim deleted file mode 100644 index eb0d89aa287..00000000000 --- a/drnim/drnim.nim +++ /dev/null @@ -1,1272 +0,0 @@ -# -# -# Doctor Nim -# (c) Copyright 2020 Andreas Rumpf -# -# See the file "copying.txt", included in this -# distribution, for details about the copyright. -# - -#[ - -- introduce Phi nodes to complete the SSA representation -- the analysis has to take 'break', 'continue' and 'raises' into account -- We need to map arrays to Z3 and test for something like 'forall(i, (i in 3..4) -> (a[i] > 3))' -- We need teach DrNim what 'inc', 'dec' and 'swap' mean, for example - 'x in n..m; inc x' implies 'x in n+1..m+1' - -]# - -import std / [ - parseopt, strutils, os, tables, times, intsets, hashes -] - -import ".." / compiler / [ - ast, astalgo, types, renderer, - commands, options, msgs, - platform, trees, wordrecg, guards, - idents, lineinfos, cmdlinehelper, modulegraphs, condsyms, - pathutils, passes, passaux, sem, modules -] - -import z3 / z3_api - -when not defined(windows): - # on UNIX we use static linking because UNIX's lib*.so system is broken - # beyond repair and the neckbeards don't understand software development. - {.passL: "dist/z3/build/libz3.a".} - -const - HelpMessage = "DrNim Version $1 [$2: $3]\n" & - "Compiled at $4\n" & - "Copyright (c) 2006-" & copyrightYear & " by Andreas Rumpf\n" - -const - Usage = """ -drnim [options] [projectfile] - -Options: Same options that the Nim compiler supports. Plus: - ---assumeUnique Assume unique `ref` pointers. This makes the analysis unsound - but more useful for wild Nim code such as the Nim compiler - itself. -""" - -proc getCommandLineDesc(conf: ConfigRef): string = - result = (HelpMessage % [system.NimVersion, platform.OS[conf.target.hostOS].name, - CPU[conf.target.hostCPU].name, CompileDate]) & - Usage - -proc helpOnError(conf: ConfigRef) = - msgWriteln(conf, getCommandLineDesc(conf), {msgStdout}) - msgQuit(0) - -type - CannotMapToZ3Error = object of ValueError - Z3Exception = object of ValueError - VersionScope = distinct int - DrnimContext = ref object - z3: Z3_context - graph: ModuleGraph - idgen: IdGenerator - facts: seq[(PNode, VersionScope)] - varVersions: seq[int] # this maps variable IDs to their current version. - varSyms: seq[PSym] # mirrors 'varVersions' - o: Operators - hasUnstructedCf: int - currOptions: TOptions - owner: PSym - mangler: seq[PSym] - opImplies: PSym - - DrCon = object - graph: ModuleGraph - idgen: IdGenerator - mapping: Table[string, Z3_ast] - canonParameterNames: bool - assumeUniqueness: bool - up: DrnimContext - -var - assumeUniqueness: bool - -proc echoFacts(c: DrnimContext) = - echo "FACTS:" - for i in 0 ..< c.facts.len: - let f = c.facts[i] - echo f[0], " version ", int(f[1]) - -proc isLoc(m: PNode; assumeUniqueness: bool): bool = - # We can reason about "locations" and map them to Z3 constants. - # For code that is full of "ref" (e.g. the Nim compiler itself) that - # is too limiting - proc isLet(n: PNode): bool = - if n.kind == nkSym: - if n.sym.kind in {skLet, skTemp, skForVar}: - result = true - elif n.sym.kind == skParam and skipTypes(n.sym.typ, - abstractInst).kind != tyVar: - result = true - - var n = m - while true: - case n.kind - of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv, nkHiddenDeref: - n = n[0] - of nkDerefExpr: - n = n[0] - if not assumeUniqueness: return false - of nkBracketExpr: - if isConstExpr(n[1]) or isLet(n[1]) or isConstExpr(n[1].skipConv): - n = n[0] - else: return - of nkHiddenStdConv, nkHiddenSubConv, nkConv: - n = n[1] - else: - break - if n.kind == nkSym: - case n.sym.kind - of skLet, skTemp, skForVar, skParam: - result = true - #of skParam: - # result = skipTypes(n.sym.typ, abstractInst).kind != tyVar - of skResult, skVar: - result = {sfAddrTaken} * n.sym.flags == {} - else: - discard - -proc currentVarVersion(c: DrnimContext; s: PSym; begin: VersionScope): int = - # we need to take into account both en- and disabled var bindings here, - # hence the 'abs' call: - result = 0 - for i in countdown(int(begin)-1, 0): - if abs(c.varVersions[i]) == s.id: inc result - -proc previousVarVersion(c: DrnimContext; s: PSym; begin: VersionScope): int = - # we need to ignore currently disabled var bindings here, - # hence no 'abs' call here. - result = -1 - for i in countdown(int(begin)-1, 0): - if c.varVersions[i] == s.id: inc result - -proc disamb(c: DrnimContext; s: PSym): int = - # we group by 's.name.s' to compute the stable name ID. - result = 0 - for i in 0 ..< c.mangler.len: - if s == c.mangler[i]: return result - if s.name.s == c.mangler[i].name.s: inc result - c.mangler.add s - -proc stableName(result: var string; c: DrnimContext; n: PNode; version: VersionScope; - isOld: bool) = - # we can map full Nim expressions like 'f(a, b, c)' to Z3 variables. - # We must be careful to select a unique, stable name for these expressions - # based on structural equality. 'stableName' helps us with this problem. - # In the future we will also use this string for the caching mechanism. - case n.kind - of nkEmpty, nkNilLit, nkType: discard - of nkIdent: - result.add n.ident.s - of nkSym: - result.add n.sym.name.s - if n.sym.magic == mNone: - let d = disamb(c, n.sym) - if d != 0: - result.add "`scope=" - result.addInt d - let v = if isOld: c.previousVarVersion(n.sym, version) - else: c.currentVarVersion(n.sym, version) - if v > 0: - result.add '`' - result.addInt v - else: - result.add "`magic=" - result.addInt ord(n.sym.magic) - of nkBindStmt: - # we use 'bind x 3' to use the 3rd version of variable 'x'. This - # is easier than using 'old' which is position relative. - assert n.len == 2 - assert n[0].kind == nkSym - assert n[1].kind == nkIntLit - let s = n[0].sym - let v = int(n[1].intVal) - result.add s.name.s - let d = disamb(c, s) - if d != 0: - result.add "`scope=" - result.addInt d - if v > 0: - result.add '`' - result.addInt v - of nkCharLit..nkUInt64Lit: - result.addInt n.intVal - of nkFloatLit..nkFloat64Lit: - result.addFloat n.floatVal - of nkStrLit..nkTripleStrLit: - result.add strutils.escape n.strVal - of nkDotExpr: - stableName(result, c, n[0], version, isOld) - result.add '.' - stableName(result, c, n[1], version, isOld) - of nkBracketExpr: - stableName(result, c, n[0], version, isOld) - result.add '[' - stableName(result, c, n[1], version, isOld) - result.add ']' - of nkCallKinds: - if n.len == 2: - stableName(result, c, n[1], version, isOld) - result.add '.' - case getMagic(n) - of mLengthArray, mLengthOpenArray, mLengthSeq, mLengthStr: - result.add "len" - of mHigh: - result.add "high" - of mLow: - result.add "low" - else: - stableName(result, c, n[0], version, isOld) - elif n.kind == nkInfix and n.len == 3: - result.add '(' - stableName(result, c, n[1], version, isOld) - result.add ' ' - stableName(result, c, n[0], version, isOld) - result.add ' ' - stableName(result, c, n[2], version, isOld) - result.add ')' - else: - stableName(result, c, n[0], version, isOld) - result.add '(' - for i in 1.. 1: result.add ", " - stableName(result, c, n[i], version, isOld) - result.add ')' - else: - result.add $n.kind - result.add '(' - for i in 0.. 0: result.add ", " - stableName(result, c, n[i], version, isOld) - result.add ')' - -proc stableName(c: DrnimContext; n: PNode; version: VersionScope; - isOld = false): string = - stableName(result, c, n, version, isOld) - -template allScopes(c): untyped = VersionScope(c.varVersions.len) -template currentScope(c): untyped = VersionScope(c.varVersions.len) - -proc notImplemented(msg: string) {.noinline.} = - when defined(debug): - writeStackTrace() - echo msg - raise newException(CannotMapToZ3Error, "; cannot map to Z3: " & msg) - -proc notImplemented(n: PNode) {.noinline.} = - when defined(debug): - writeStackTrace() - raise newException(CannotMapToZ3Error, "; cannot map to Z3: " & $n) - -proc notImplemented(t: PType) {.noinline.} = - when defined(debug): - writeStackTrace() - raise newException(CannotMapToZ3Error, "; cannot map to Z3: " & typeToString t) - -proc translateEnsures(e, x: PNode): PNode = - if e.kind == nkSym and e.sym.kind == skResult: - result = x - else: - result = shallowCopy(e) - for i in 0 ..< safeLen(e): - result[i] = translateEnsures(e[i], x) - -proc typeToZ3(c: DrCon; t: PType): Z3_sort = - template ctx: untyped = c.up.z3 - case t.skipTypes(abstractInst+{tyVar}).kind - of tyEnum, tyInt..tyInt64: - result = Z3_mk_int_sort(ctx) - of tyBool: - result = Z3_mk_bool_sort(ctx) - of tyFloat..tyFloat128: - result = Z3_mk_fpa_sort_double(ctx) - of tyChar, tyUInt..tyUInt64: - result = Z3_mk_bv_sort(ctx, 64) - #cuint(getSize(c.graph.config, t) * 8)) - else: - notImplemented(t) - -template binary(op, a, b): untyped = - var arr = [a, b] - op(ctx, cuint(2), addr(arr[0])) - -proc nodeToZ3(c: var DrCon; n: PNode; scope: VersionScope; vars: var seq[PNode]): Z3_ast - -proc nodeToDomain(c: var DrCon; n, q: PNode; opAnd: PSym): PNode = - assert n.kind == nkInfix - let opLe = createMagic(c.graph, c.idgen, "<=", mLeI) - case $n[0] - of "..": - result = buildCall(opAnd, buildCall(opLe, n[1], q), buildCall(opLe, q, n[2])) - of "..<": - let opLt = createMagic(c.graph, c.idgen, "<", mLtI) - result = buildCall(opAnd, buildCall(opLe, n[1], q), buildCall(opLt, q, n[2])) - else: - notImplemented(n) - -template quantorToZ3(fn) {.dirty.} = - template ctx: untyped = c.up.z3 - - var bound = newSeq[Z3_app](n.len-2) - let opAnd = createMagic(c.graph, c.idgen, "and", mAnd) - var known: PNode - for i in 1..n.len-2: - let it = n[i] - doAssert it.kind == nkInfix - let v = it[1].sym - let name = Z3_mk_string_symbol(ctx, v.name.s) - let vz3 = Z3_mk_const(ctx, name, typeToZ3(c, v.typ)) - c.mapping[stableName(c.up, it[1], allScopes(c.up))] = vz3 - bound[i-1] = Z3_to_app(ctx, vz3) - let domain = nodeToDomain(c, it[2], it[1], opAnd) - if known == nil: - known = domain - else: - known = buildCall(opAnd, known, domain) - - var dummy: seq[PNode] - assert known != nil - let x = nodeToZ3(c, buildCall(createMagic(c.graph, c.idgen, "->", mImplies), - known, n[^1]), scope, dummy) - result = fn(ctx, 0, bound.len.cuint, addr(bound[0]), 0, nil, x) - -proc forallToZ3(c: var DrCon; n: PNode; scope: VersionScope): Z3_ast = quantorToZ3(Z3_mk_forall_const) -proc existsToZ3(c: var DrCon; n: PNode; scope: VersionScope): Z3_ast = quantorToZ3(Z3_mk_exists_const) - -proc paramName(c: DrnimContext; n: PNode): string = - case n.sym.kind - of skParam: result = "arg" & $n.sym.position - of skResult: result = "result" - else: result = stableName(c, n, allScopes(c)) - -proc nodeToZ3(c: var DrCon; n: PNode; scope: VersionScope; vars: var seq[PNode]): Z3_ast = - template ctx: untyped = c.up.z3 - template rec(n): untyped = nodeToZ3(c, n, scope, vars) - case n.kind - of nkSym: - let key = if c.canonParameterNames: paramName(c.up, n) else: stableName(c.up, n, scope) - result = c.mapping.getOrDefault(key) - if pointer(result) == nil: - let name = Z3_mk_string_symbol(ctx, key) - result = Z3_mk_const(ctx, name, typeToZ3(c, n.sym.typ)) - c.mapping[key] = result - vars.add n - of nkCharLit..nkUInt64Lit: - if n.typ != nil and n.typ.skipTypes(abstractInst).kind in {tyInt..tyInt64}: - # optimized for the common case - result = Z3_mk_int64(ctx, clonglong(n.intval), Z3_mk_int_sort(ctx)) - elif n.typ != nil and n.typ.kind == tyBool: - result = if n.intval != 0: Z3_mk_true(ctx) else: Z3_mk_false(ctx) - elif n.typ != nil and isUnsigned(n.typ): - result = Z3_mk_unsigned_int64(ctx, cast[uint64](n.intVal), typeToZ3(c, n.typ)) - else: - let zt = if n.typ == nil: Z3_mk_int_sort(ctx) else: typeToZ3(c, n.typ) - result = Z3_mk_numeral(ctx, $getOrdValue(n), zt) - of nkFloatLit..nkFloat64Lit: - result = Z3_mk_fpa_numeral_double(ctx, n.floatVal, Z3_mk_fpa_sort_double(ctx)) - of nkCallKinds: - assert n.len > 0 - let operator = getMagic(n) - case operator - of mEqI, mEqF64, mEqEnum, mEqCh, mEqB, mEqRef, mEqProc, - mEqStr, mEqSet, mEqCString: - result = Z3_mk_eq(ctx, rec n[1], rec n[2]) - of mLeI, mLeEnum, mLeCh, mLeB, mLePtr, mLeStr: - result = Z3_mk_le(ctx, rec n[1], rec n[2]) - of mLtI, mLtEnum, mLtCh, mLtB, mLtPtr, mLtStr: - result = Z3_mk_lt(ctx, rec n[1], rec n[2]) - of mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq: - # len(x) needs the same logic as 'x' itself - if isLoc(n[1], c.assumeUniqueness): - let key = stableName(c.up, n, scope) - result = c.mapping.getOrDefault(key) - if pointer(result) == nil: - let name = Z3_mk_string_symbol(ctx, key) - result = Z3_mk_const(ctx, name, Z3_mk_int_sort(ctx)) - c.mapping[key] = result - vars.add n - else: - notImplemented(n) - of mHigh: - let addOpr = createMagic(c.graph, c.idgen, "+", mAddI) - let lenOpr = createMagic(c.graph, c.idgen, "len", mLengthOpenArray) - let asLenExpr = addOpr.buildCall(lenOpr.buildCall(n[1]), nkIntLit.newIntNode(-1)) - result = rec asLenExpr - of mLow: - result = rec lowBound(c.graph.config, n[1]) - of mAddI, mSucc: - result = binary(Z3_mk_add, rec n[1], rec n[2]) - of mSubI, mPred: - result = binary(Z3_mk_sub, rec n[1], rec n[2]) - of mMulI: - result = binary(Z3_mk_mul, rec n[1], rec n[2]) - of mDivI: - result = Z3_mk_div(ctx, rec n[1], rec n[2]) - of mModI: - result = Z3_mk_mod(ctx, rec n[1], rec n[2]) - of mMaxI: - # max(a, b) <=> ite(a < b, b, a) - result = Z3_mk_ite(ctx, Z3_mk_lt(ctx, rec n[1], rec n[2]), - rec n[2], rec n[1]) - of mMinI: - # min(a, b) <=> ite(a < b, a, b) - result = Z3_mk_ite(ctx, Z3_mk_lt(ctx, rec n[1], rec n[2]), - rec n[1], rec n[2]) - of mLeU: - result = Z3_mk_bvule(ctx, rec n[1], rec n[2]) - of mLtU: - result = Z3_mk_bvult(ctx, rec n[1], rec n[2]) - of mAnd: - # 'a and b' <=> ite(a, b, false) - result = Z3_mk_ite(ctx, rec n[1], rec n[2], Z3_mk_false(ctx)) - #result = binary(Z3_mk_and, rec n[1], rec n[2]) - of mOr: - result = Z3_mk_ite(ctx, rec n[1], Z3_mk_true(ctx), rec n[2]) - #result = binary(Z3_mk_or, rec n[1], rec n[2]) - of mXor: - result = Z3_mk_xor(ctx, rec n[1], rec n[2]) - of mNot: - result = Z3_mk_not(ctx, rec n[1]) - of mImplies: - result = Z3_mk_implies(ctx, rec n[1], rec n[2]) - of mIff: - result = Z3_mk_iff(ctx, rec n[1], rec n[2]) - of mForall: - result = forallToZ3(c, n, scope) - of mExists: - result = existsToZ3(c, n, scope) - of mLeF64: - result = Z3_mk_fpa_leq(ctx, rec n[1], rec n[2]) - of mLtF64: - result = Z3_mk_fpa_lt(ctx, rec n[1], rec n[2]) - of mAddF64: - result = Z3_mk_fpa_add(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2]) - of mSubF64: - result = Z3_mk_fpa_sub(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2]) - of mMulF64: - result = Z3_mk_fpa_mul(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2]) - of mDivF64: - result = Z3_mk_fpa_div(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx), rec n[1], rec n[2]) - of mShrI: - # XXX handle conversions from int to uint here somehow - result = Z3_mk_bvlshr(ctx, rec n[1], rec n[2]) - of mAshrI: - result = Z3_mk_bvashr(ctx, rec n[1], rec n[2]) - of mShlI: - result = Z3_mk_bvshl(ctx, rec n[1], rec n[2]) - of mBitandI: - result = Z3_mk_bvand(ctx, rec n[1], rec n[2]) - of mBitorI: - result = Z3_mk_bvor(ctx, rec n[1], rec n[2]) - of mBitxorI: - result = Z3_mk_bvxor(ctx, rec n[1], rec n[2]) - of mOrd, mChr: - result = rec n[1] - of mOld: - let key = if c.canonParameterNames: (paramName(c.up, n[1]) & ".old") - else: stableName(c.up, n[1], scope, isOld = true) - result = c.mapping.getOrDefault(key) - if pointer(result) == nil: - let name = Z3_mk_string_symbol(ctx, key) - result = Z3_mk_const(ctx, name, typeToZ3(c, n[1].typ)) - c.mapping[key] = result - # XXX change the logic in `addRangeInfo` for this - #vars.add n - - else: - # sempass2 adds some 'fact' like 'x = f(a, b)' (see addAsgnFact) - # 'f(a, b)' can have an .ensures annotation and we need to make use - # of this information. - # we need to map 'f(a, b)' to a Z3 variable of this name - let op = n[0].typ - if op != nil and op.n != nil and op.n.len > 0 and op.n[0].kind == nkEffectList and - ensuresEffects < op.n[0].len: - let ensures = op.n[0][ensuresEffects] - if ensures != nil and ensures.kind != nkEmpty: - let key = stableName(c.up, n, scope) - result = c.mapping.getOrDefault(key) - if pointer(result) == nil: - let name = Z3_mk_string_symbol(ctx, key) - result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ)) - c.mapping[key] = result - vars.add n - - if pointer(result) == nil: - notImplemented(n) - of nkStmtListExpr, nkPar: - var isTrivial = true - for i in 0..n.len-2: - isTrivial = isTrivial and n[i].kind in {nkEmpty, nkCommentStmt} - if isTrivial: - result = rec n[^1] - else: - notImplemented(n) - of nkHiddenDeref: - result = rec n[0] - else: - if isLoc(n, c.assumeUniqueness): - let key = stableName(c.up, n, scope) - result = c.mapping.getOrDefault(key) - if pointer(result) == nil: - let name = Z3_mk_string_symbol(ctx, key) - result = Z3_mk_const(ctx, name, typeToZ3(c, n.typ)) - c.mapping[key] = result - vars.add n - else: - notImplemented(n) - -proc addRangeInfo(c: var DrCon, n: PNode; scope: VersionScope, res: var seq[Z3_ast]) = - var cmpOp = mLeI - if n.typ != nil: - cmpOp = - case n.typ.skipTypes(abstractInst).kind - of tyFloat..tyFloat128: mLeF64 - of tyChar, tyUInt..tyUInt64: mLeU - else: mLeI - - var lowBound, highBound: PNode - if n.kind == nkSym: - let v = n.sym - let t = v.typ.skipTypes(abstractInst - {tyRange}) - - case t.kind - of tyRange: - lowBound = t.n[0] - highBound = t.n[1] - of tyFloat..tyFloat128: - # no range information for non-range'd floats - return - of tyUInt..tyUInt64, tyChar: - lowBound = newIntNode(nkUInt64Lit, firstOrd(nil, v.typ)) - lowBound.typ = v.typ - highBound = newIntNode(nkUInt64Lit, lastOrd(nil, v.typ)) - highBound.typ = v.typ - of tyInt..tyInt64, tyEnum: - lowBound = newIntNode(nkInt64Lit, firstOrd(nil, v.typ)) - highBound = newIntNode(nkInt64Lit, lastOrd(nil, v.typ)) - else: - # no range information available: - return - elif n.kind in nkCallKinds and n.len == 2 and n[0].kind == nkSym and - n[0].sym.magic in {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq}: - # we know it's a 'len(x)' expression and we seek to teach - # Z3 that the result is >= 0 and <= high(int). - doAssert n.kind in nkCallKinds - doAssert n[0].kind == nkSym - doAssert n.len == 2 - - lowBound = newIntNode(nkInt64Lit, 0) - if n.typ != nil: - highBound = newIntNode(nkInt64Lit, lastOrd(nil, n.typ)) - else: - highBound = newIntNode(nkInt64Lit, high(int64)) - else: - let op = n[0].typ - if op != nil and op.n != nil and op.n.len > 0 and op.n[0].kind == nkEffectList and - ensuresEffects < op.n[0].len: - let ensures = op.n[0][ensuresEffects] - if ensures != nil and ensures.kind != nkEmpty: - var dummy: seq[PNode] - res.add nodeToZ3(c, translateEnsures(ensures, n), scope, dummy) - return - - let x = newTree(nkInfix, newSymNode createMagic(c.graph, c.idgen, "<=", cmpOp), lowBound, n) - let y = newTree(nkInfix, newSymNode createMagic(c.graph, c.idgen, "<=", cmpOp), n, highBound) - - var dummy: seq[PNode] - res.add nodeToZ3(c, x, scope, dummy) - res.add nodeToZ3(c, y, scope, dummy) - -proc on_err(ctx: Z3_context, e: Z3_error_code) {.nimcall.} = - #writeStackTrace() - let msg = $Z3_get_error_msg(ctx, e) - raise newException(Z3Exception, msg) - -proc forall(ctx: Z3_context; vars: seq[Z3_ast]; assumption, body: Z3_ast): Z3_ast = - let x = Z3_mk_implies(ctx, assumption, body) - if vars.len > 0: - var bound: seq[Z3_app] - for v in vars: bound.add Z3_to_app(ctx, v) - result = Z3_mk_forall_const(ctx, 0, bound.len.cuint, addr(bound[0]), 0, nil, x) - else: - result = x - -proc conj(ctx: Z3_context; conds: seq[Z3_ast]): Z3_ast = - if conds.len > 0: - result = Z3_mk_and(ctx, cuint(conds.len), unsafeAddr conds[0]) - else: - result = Z3_mk_true(ctx) - -proc setupZ3(): Z3_context = - let cfg = Z3_mk_config() - when false: - Z3_set_param_value(cfg, "timeout", "1000") - Z3_set_param_value(cfg, "model", "true") - result = Z3_mk_context(cfg) - Z3_del_config(cfg) - Z3_set_error_handler(result, on_err) - -proc proofEngineAux(c: var DrCon; assumptions: seq[(PNode, VersionScope)]; - toProve: (PNode, VersionScope)): (bool, string) = - c.mapping = initTable[string, Z3_ast]() - try: - - #[ - For example, let's have these facts: - - i < 10 - i > 0 - - Question: - - i + 3 < 13 - - What we need to produce: - - forall(i, (i < 10) & (i > 0) -> (i + 3 < 13)) - - ]# - - var collectedVars: seq[PNode] - - template ctx(): untyped = c.up.z3 - - let solver = Z3_mk_solver(ctx) - var lhs: seq[Z3_ast] - for assumption in items(assumptions): - try: - let za = nodeToZ3(c, assumption[0], assumption[1], collectedVars) - #Z3_solver_assert ctx, solver, za - lhs.add za - except CannotMapToZ3Error: - discard "ignore a fact we cannot map to Z3" - - let z3toProve = nodeToZ3(c, toProve[0], toProve[1], collectedVars) - for v in collectedVars: - addRangeInfo(c, v, toProve[1], lhs) - - # to make Z3 produce nice counterexamples, we try to prove the - # negation of our conjecture and see if it's Z3_L_FALSE - let fa = Z3_mk_not(ctx, Z3_mk_implies(ctx, conj(ctx, lhs), z3toProve)) - - #Z3_mk_not(ctx, forall(ctx, collectedVars, conj(ctx, lhs), z3toProve)) - - when defined(dz3): - echo "toProve: ", Z3_ast_to_string(ctx, fa), " ", c.graph.config $ toProve[0].info, " ", int(toProve[1]) - Z3_solver_assert ctx, solver, fa - - let z3res = Z3_solver_check(ctx, solver) - result[0] = z3res == Z3_L_FALSE - result[1] = "" - if not result[0]: - let counterex = strip($Z3_model_to_string(ctx, Z3_solver_get_model(ctx, solver))) - if counterex.len > 0: - result[1].add "; counter example: " & counterex - except ValueError: - result[0] = false - result[1] = getCurrentExceptionMsg() - -proc proofEngine(ctx: DrnimContext; assumptions: seq[(PNode, VersionScope)]; - toProve: (PNode, VersionScope)): (bool, string) = - var c: DrCon - c.graph = ctx.graph - c.idgen = ctx.idgen - c.assumeUniqueness = assumeUniqueness - c.up = ctx - result = proofEngineAux(c, assumptions, toProve) - -proc skipAddr(n: PNode): PNode {.inline.} = - (if n.kind == nkHiddenAddr: n[0] else: n) - -proc translateReq(r, call: PNode): PNode = - if r.kind == nkSym and r.sym.kind == skParam: - if r.sym.position+1 < call.len: - result = call[r.sym.position+1].skipAddr - else: - notImplemented("no argument given for formal parameter: " & r.sym.name.s) - else: - result = shallowCopy(r) - for i in 0 ..< safeLen(r): - result[i] = translateReq(r[i], call) - -proc requirementsCheck(ctx: DrnimContext; assumptions: seq[(PNode, VersionScope)]; - call, requirement: PNode): (bool, string) = - try: - let r = translateReq(requirement, call) - result = proofEngine(ctx, assumptions, (r, ctx.currentScope)) - except ValueError: - result[0] = false - result[1] = getCurrentExceptionMsg() - -proc compatibleProps(graph: ModuleGraph; formal, actual: PType): bool {.nimcall.} = - #[ - Thoughts on subtyping rules for 'proc' types: - - proc a(y: int) {.requires: y > 0.} # a is 'weaker' than F - # 'requires' must be weaker (or equal) - # 'ensures' must be stronger (or equal) - - # a 'is weaker than' b iff b -> a - # a 'is stronger than' b iff a -> b - # --> We can use Z3 to compute whether 'var x: T = q' is valid - - type - F = proc (y: int) {.requires: y > 5.} - - var - x: F = a # valid? - ]# - proc isEmpty(n: PNode): bool {.inline.} = n == nil or n.safeLen == 0 - - result = true - if formal.n != nil and formal.n.len > 0 and formal.n[0].kind == nkEffectList and - ensuresEffects < formal.n[0].len: - - let frequires = formal.n[0][requiresEffects] - let fensures = formal.n[0][ensuresEffects] - - if actual.n != nil and actual.n.len > 0 and actual.n[0].kind == nkEffectList and - ensuresEffects < actual.n[0].len: - let arequires = actual.n[0][requiresEffects] - let aensures = actual.n[0][ensuresEffects] - - var c: DrCon - c.graph = graph - c.idgen = graph.idgen - c.canonParameterNames = true - try: - c.up = DrnimContext(z3: setupZ3(), o: initOperators(graph), graph: graph, owner: nil, - opImplies: createMagic(graph, c.idgen, "->", mImplies)) - template zero: untyped = VersionScope(0) - if not frequires.isEmpty: - result = not arequires.isEmpty and proofEngineAux(c, @[(frequires, zero)], (arequires, zero))[0] - - if result: - if not fensures.isEmpty: - result = not aensures.isEmpty and proofEngineAux(c, @[(aensures, zero)], (fensures, zero))[0] - finally: - Z3_del_context(c.up.z3) - else: - # formal has requirements but 'actual' has none, so make it - # incompatible. XXX What if the requirement only mentions that - # we already know from the type system? - result = frequires.isEmpty and fensures.isEmpty - -template config(c: typed): untyped = c.graph.config - -proc addFact(c: DrnimContext; n: PNode) = - let v = c.currentScope - if n.kind in nkCallKinds and n[0].kind == nkSym and n[0].sym.magic in {mOr, mAnd}: - c.addFact(n[1]) - c.facts.add((n, v)) - -proc neg(c: DrnimContext; n: PNode): PNode = - result = newNodeI(nkCall, n.info, 2) - result[0] = newSymNode(c.o.opNot) - result[1] = n - -proc addFactNeg(c: DrnimContext; n: PNode) = - addFact(c, neg(c, n)) - -proc combineFacts(c: DrnimContext; a, b: PNode): PNode = - if a == nil: - result = b - else: - result = buildCall(c.o.opAnd, a, b) - -proc prove(c: DrnimContext; prop: PNode): bool = - let (success, m) = proofEngine(c, c.facts, (prop, c.currentScope)) - if not success: - message(c.config, prop.info, warnStaticIndexCheck, "cannot prove: " & $prop & m) - result = success - -proc traversePragmaStmt(c: DrnimContext, n: PNode) = - for it in n: - if it.kind == nkExprColonExpr: - let pragma = whichPragma(it) - if pragma == wAssume: - addFact(c, it[1]) - elif pragma == wInvariant or pragma == wAssert: - if prove(c, it[1]): - addFact(c, it[1]) - else: - echoFacts(c) - -proc requiresCheck(c: DrnimContext, call: PNode; op: PType) = - assert op.n[0].kind == nkEffectList - if requiresEffects < op.n[0].len: - let requires = op.n[0][requiresEffects] - if requires != nil and requires.kind != nkEmpty: - # we need to map the call arguments to the formal parameters used inside - # 'requires': - let (success, m) = requirementsCheck(c, c.facts, call, requires) - if not success: - message(c.config, call.info, warnStaticIndexCheck, "cannot prove: " & $requires & m) - -proc freshVersion(c: DrnimContext; arg: PNode) = - let v = getRoot(arg) - if v != nil: - c.varVersions.add v.id - c.varSyms.add v - -proc translateEnsuresFromCall(c: DrnimContext, e, call: PNode): PNode = - if e.kind in nkCallKinds and e[0].kind == nkSym and e[0].sym.magic == mOld: - assert e[1].kind == nkSym and e[1].sym.kind == skParam - let param = e[1].sym - let arg = call[param.position+1].skipAddr - result = buildCall(e[0].sym, arg) - elif e.kind == nkSym and e.sym.kind == skParam: - let param = e.sym - let arg = call[param.position+1].skipAddr - result = arg - else: - result = shallowCopy(e) - for i in 0 ..< safeLen(e): result[i] = translateEnsuresFromCall(c, e[i], call) - -proc collectEnsuredFacts(c: DrnimContext, call: PNode; op: PType) = - assert op.n[0].kind == nkEffectList - for i in 1 ..< min(call.len, op.len): - if op[i].kind == tyVar: - freshVersion(c, call[i].skipAddr) - - if ensuresEffects < op.n[0].len: - let ensures = op.n[0][ensuresEffects] - if ensures != nil and ensures.kind != nkEmpty: - addFact(c, translateEnsuresFromCall(c, ensures, call)) - -proc checkLe(c: DrnimContext, a, b: PNode) = - var cmpOp = mLeI - if a.typ != nil: - case a.typ.skipTypes(abstractInst).kind - of tyFloat..tyFloat128: cmpOp = mLeF64 - of tyChar, tyUInt..tyUInt64: cmpOp = mLeU - else: discard - - let cmp = newTree(nkInfix, newSymNode createMagic(c.graph, c.idgen, "<=", cmpOp), a, b) - cmp.info = a.info - discard prove(c, cmp) - -proc checkBounds(c: DrnimContext; arr, idx: PNode) = - checkLe(c, lowBound(c.config, arr), idx) - checkLe(c, idx, highBound(c.config, arr, c.o)) - -proc checkRange(c: DrnimContext; value: PNode; typ: PType) = - let t = typ.skipTypes(abstractInst - {tyRange}) - if t.kind == tyRange: - let lowBound = copyTree(t.n[0]) - lowBound.info = value.info - let highBound = copyTree(t.n[1]) - highBound.info = value.info - checkLe(c, lowBound, value) - checkLe(c, value, highBound) - -proc addAsgnFact*(c: DrnimContext, key, value: PNode) = - var fact = newNodeI(nkCall, key.info, 3) - fact[0] = newSymNode(c.o.opEq) - fact[1] = key - fact[2] = value - c.facts.add((fact, c.currentScope)) - -proc traverse(c: DrnimContext; n: PNode) - -proc traverseTryStmt(c: DrnimContext; n: PNode) = - traverse(c, n[0]) - let oldFacts = c.facts.len - for i in 1 ..< n.len: - traverse(c, n[i].lastSon) - setLen(c.facts, oldFacts) - -proc traverseCase(c: DrnimContext; n: PNode) = - traverse(c, n[0]) - let oldFacts = c.facts.len - for i in 1 ..< n.len: - traverse(c, n[i].lastSon) - # XXX make this as smart as 'if elif' - setLen(c.facts, oldFacts) - -proc disableVarVersions(c: DrnimContext; until: int) = - for i in until.. (x'3 == x'1)) and - ((not a and b) -> (x'3 == x'2)) and - ((not a and not b) -> (x'3 == x'0)) - - (Where ``->`` is the logical implication.) - - In addition to the Phi information we also know the 'facts' - computed by the branches, for example:: - - if a: - factA - elif b: - factB - else: - factC - - (a -> factA) and - ((not a and b) -> factB) and - ((not a and not b) -> factC) - - We can combine these two aspects by producing the following facts - after each branch:: - - var x = y # x'0 - if a: - inc x # x'1 == x'0 + 1 - # also: x'1 == x'final - elif b: - inc x, 2 # x'2 == x'0 + 2 - # also: x'2 == x'final - else: - # also: x'0 == x'final - - ]# - let oldFacts = c.facts.len - let oldVars = c.varVersions.len - var newFacts: seq[PNode] - var branches = newSeq[(PNode, int)](n.len) # (cond, newVars) pairs - template condVersion(): untyped = VersionScope(oldVars) - - for i in 0.. 1: - addFact(c, branch[0]) - cond = combineFacts(c, cond, branch[0]) - - for i in 0.. 0 and n[0].kind == nkEffectList and ensuresEffects < n[0].len: - let ensures = n[0][ensuresEffects] - if ensures != nil and ensures.kind != nkEmpty: - discard prove(c, ensures) - -proc traverseAsgn(c: DrnimContext; n: PNode) = - traverse(c, n[0]) - traverse(c, n[1]) - - proc replaceByOldParams(fact, le: PNode): PNode = - if guards.sameTree(fact, le): - result = newNodeIT(nkCall, fact.info, fact.typ) - result.add newSymNode createMagic(c.graph, c.idgen, "old", mOld) - result.add fact - else: - result = shallowCopy(fact) - for i in 0 ..< safeLen(fact): - result[i] = replaceByOldParams(fact[i], le) - - freshVersion(c, n[0]) - addAsgnFact(c, n[0], replaceByOldParams(n[1], n[0])) - when defined(debug): - echoFacts(c) - -proc traverse(c: DrnimContext; n: PNode) = - case n.kind - of nkEmpty..nkNilLit: - discard "nothing to do" - of nkRaiseStmt, nkBreakStmt, nkContinueStmt: - inc c.hasUnstructedCf - for i in 0..", mImplies) - try: - traverse(c, n) - ensuresCheck(c, owner) - finally: - Z3_del_context(c.z3) - - -proc mainCommand(graph: ModuleGraph) = - let conf = graph.config - conf.lastCmdTime = epochTime() - - graph.strongSemCheck = strongSemCheck - graph.compatibleProps = compatibleProps - - graph.config.setErrorMaxHighMaybe - defineSymbol(graph.config.symbols, "nimcheck") - defineSymbol(graph.config.symbols, "nimDrNim") - - registerPass graph, verbosePass - registerPass graph, semPass - compileProject(graph) - if conf.errorCounter == 0: - genSuccessX(graph.config) - -proc processCmdLine(pass: TCmdLinePass, cmd: string; config: ConfigRef) = - var p = parseopt.initOptParser(cmd) - var argsCount = 1 - - config.commandLine.setLen 0 - config.setCmd cmdCheck - while true: - parseopt.next(p) - case p.kind - of cmdEnd: break - of cmdLongOption, cmdShortOption: - config.commandLine.add " " - config.commandLine.addCmdPrefix p.kind - config.commandLine.add p.key.quoteShell # quoteShell to be future proof - if p.val.len > 0: - config.commandLine.add ':' - config.commandLine.add p.val.quoteShell - - if p.key == " ": - p.key = "-" - if processArgument(pass, p, argsCount, config): break - else: - case p.key.normalize - of "assumeunique": - assumeUniqueness = true - else: - processSwitch(pass, p, config) - of cmdArgument: - config.commandLine.add " " - config.commandLine.add p.key.quoteShell - if processArgument(pass, p, argsCount, config): break - if pass == passCmd2: - if {optRun, optWasNimscript} * config.globalOptions == {} and - config.arguments.len > 0 and config.cmd notin {cmdTcc, cmdNimscript}: - rawMessage(config, errGenerated, errArgsNeedRunOption) - -proc handleCmdLine(cache: IdentCache; conf: ConfigRef) = - incl conf.options, optStaticBoundsCheck - let self = NimProg( - supportsStdinFile: true, - processCmdLine: processCmdLine - ) - self.initDefinesProg(conf, "drnim") - if paramCount() == 0: - helpOnError(conf) - return - - self.processCmdLineAndProjectPath(conf) - var graph = newModuleGraph(cache, conf) - if not self.loadConfigsAndProcessCmdLine(cache, conf, graph): return - mainCommand(graph) - if conf.hasHint(hintGCStats): echo(GC_getStatistics()) - -when compileOption("gc", "refc"): - # the new correct mark&sweep collector is too slow :-/ - GC_disableMarkAndSweep() - -when not defined(selftest): - let conf = newConfigRef() - handleCmdLine(newIdentCache(), conf) - when declared(GC_setMaxPause): - echo GC_getStatistics() - msgQuit(int8(conf.errorCounter > 0)) diff --git a/drnim/nim.cfg b/drnim/nim.cfg deleted file mode 100644 index 58c1725d981..00000000000 --- a/drnim/nim.cfg +++ /dev/null @@ -1,18 +0,0 @@ -# Special configuration file for the Nim project - -hint[XDeclaredButNotUsed]:off - -define:booting -define:nimcore -define:drnim - -@if windows: - cincludes: "$lib/wrappers/libffi/common" -@end - -define:useStdoutAsStdmsg - ---path: "../../nimz3/src" ---path: "../dist/nimz3/src" - -#define:useNodeIds diff --git a/drnim/tests/config.nims b/drnim/tests/config.nims deleted file mode 100644 index 346b0b4e668..00000000000 --- a/drnim/tests/config.nims +++ /dev/null @@ -1,10 +0,0 @@ -switch("path", "$nim/testament/lib") # so we can `import stdtest/foo` in this dir - -## prevent common user config settings to interfere with testament expectations -## Indifidual tests can override this if needed to test for these options. -switch("colors", "off") -switch("filenames", "canonical") -switch("excessiveStackTrace", "off") - -# we only want to check the marked parts in the tests: -switch("staticBoundChecks", "off") diff --git a/drnim/tests/tbasic_array_index.nim b/drnim/tests/tbasic_array_index.nim deleted file mode 100644 index 8ae019e7895..00000000000 --- a/drnim/tests/tbasic_array_index.nim +++ /dev/null @@ -1,51 +0,0 @@ -discard """ - nimout: '''tbasic_array_index.nim(26, 17) Warning: cannot prove: 0 <= len(a) - 4; counter example: a.len -> 0 [IndexCheck] -tbasic_array_index.nim(32, 5) Warning: cannot prove: 4.0 <= 1.0 [IndexCheck] -tbasic_array_index.nim(38, 36) Warning: cannot prove: a <= 10'u32; counter example: a -> #x000000000000000b -''' - cmd: "drnim $file" - action: "compile" -""" - -{.push staticBoundChecks: defined(nimDrNim).} - -proc takeNat(n: Natural) = - discard - -proc p(a, b: openArray[int]) = - if a.len > 0: - echo a[0] - - for i in 0..a.len-8: - #{.invariant: i < a.len.} - echo a[i] - - for i in 0..min(a.len, b.len)-1: - echo a[i], " ", b[i] - - takeNat(a.len - 4) - -proc r(x: range[0.0..1.0]) = echo x - -proc sum() = - r 1.0 - r 4.0 - -proc ru(x: range[1u32..10u32]) = echo x - -proc xu(a: uint) = - if a >= 4u: - let chunk = range[1u32..10u32](a) - ru chunk - -proc parse(s: string) = - var i = 0 - - while i < s.len and s[i] != 'a': - inc i - -parse("abc") - -{.pop.} - -p([1, 2, 3], [4, 5]) diff --git a/drnim/tests/tensures.nim b/drnim/tests/tensures.nim deleted file mode 100644 index f4e8f84e62c..00000000000 --- a/drnim/tests/tensures.nim +++ /dev/null @@ -1,74 +0,0 @@ -discard """ - nimout: '''tensures.nim(18, 10) Warning: BEGIN [User] -tensures.nim(27, 5) Warning: cannot prove: -0 < n [IndexCheck] -tensures.nim(47, 17) Warning: cannot prove: a < 4; counter example: y -> 2 -a`2 -> 4 -a`1 -> 3 -a -> 2 [IndexCheck] -tensures.nim(69, 17) Warning: cannot prove: a < 4; counter example: y -> 2 -a`1 -> 4 -a -> 2 [IndexCheck] -tensures.nim(73, 10) Warning: END [User]''' - cmd: "drnim $file" - action: "compile" -""" -import std/logic -{.push staticBoundChecks: defined(nimDrNim).} -{.warning: "BEGIN".} - -proc fac(n: int) {.requires: n > 0.} = - discard - -proc g(): int {.ensures: result > 0.} = - result = 10 - -fac 7 # fine -fac -45 # wrong - -fac g() # fine - -proc main = - var x = g() - fac x - -main() - -proc myinc(x: var int) {.ensures: x == old(x)+1.} = - inc x - {.assume: old(x)+1 == x.} - -proc mainB(y: int) = - var a = y - if a < 3: - myinc a - {.assert: a < 4.} - myinc a - {.assert: a < 4.} # now this is wrong! - -mainB(3) - -proc a(yy, z: int) {.requires: (yy - z) > 6.} = discard -# 'requires' must be weaker (or equal) -# 'ensures' must be stronger (or equal) - -# a 'is weaker than' b iff b -> a -# a 'is stronger than' b iff a -> b -# --> We can use Z3 to compute whether 'var x: T = q' is valid - -type - F = proc (yy, z3: int) {.requires: z3 < 5 and z3 > -5 and yy > 10.} - -var - x: F = a # valid? - -proc testAsgn(y: int) = - var a = y - if a < 3: - a = a + 2 - {.assert: a < 4.} - -testAsgn(3) - -{.warning: "END".} -{.pop.} diff --git a/drnim/tests/tphi.nim b/drnim/tests/tphi.nim deleted file mode 100644 index 7ff49f4dc50..00000000000 --- a/drnim/tests/tphi.nim +++ /dev/null @@ -1,23 +0,0 @@ -discard """ - nimout: '''tphi.nim(9, 10) Warning: BEGIN [User] -tphi.nim(22, 10) Warning: END [User]''' - cmd: "drnim $file" - action: "compile" -""" -import std/logic -{.push staticBoundChecks: defined(nimDrNim).} -{.warning: "BEGIN".} - -proc testAsgn(y: int) = - var a = y - if a > 0: - if a > 3: - a = a + 2 - else: - a = a + 1 - {.assert: a > 1.} - -testAsgn(3) - -{.warning: "END".} -{.pop.} diff --git a/drnim/tests/tsetlen_invalidates.nim b/drnim/tests/tsetlen_invalidates.nim deleted file mode 100644 index f3e59574461..00000000000 --- a/drnim/tests/tsetlen_invalidates.nim +++ /dev/null @@ -1,26 +0,0 @@ -discard """ - nimout: '''tsetlen_invalidates.nim(12, 10) Warning: BEGIN [User] -tsetlen_invalidates.nim(18, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a`1.len -> 0 -a.len -> 1 [IndexCheck] -tsetlen_invalidates.nim(26, 10) Warning: END [User] -''' - cmd: "drnim $file" - action: "compile" -""" - -{.push staticBoundChecks: defined(nimDrNim).} -{.warning: "BEGIN".} - -proc p() = - var a = newSeq[int](3) - if a.len > 0: - a.setLen 0 - echo a[0] - - if a.len > 0: - echo a[0] - -{.pop.} - -p() -{.warning: "END".} diff --git a/tools/koch/koch.nim b/tools/koch/koch.nim index d4664363b1b..fefaaa0c2d4 100644 --- a/tools/koch/koch.nim +++ b/tools/koch/koch.nim @@ -9,10 +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): {.link: "icons/koch.res".} @@ -515,29 +511,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" % [hostOS, hostCPU, $int.sizeof, $float.sizeof, $cpuEndian, getCurrentDir()] @@ -680,7 +653,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() of "fetch-bootstrap":