From b492d9047f52d9aea6fbf6a49577ffc33f631278 Mon Sep 17 00:00:00 2001 From: haxscramper Date: Thu, 27 Jan 2022 14:19:53 +0300 Subject: [PATCH] Unbundle drnim - Removes main drnim directory along with all the hacks added into `sem*` implementation - special keywords for `ensures/requires/assume/invariant`, more logic built into sempass and so on. Sem reports that were added in the main compilation. - External tooling for code analysis should better be implemented via completely external modifications, instead of clobbering the main compiler codebase with logic for barely functioning tooling. With dod refactor this task becomes much easier, since extra metada can be attached to any symbol. - We definitely want to move in the direction of automatic code correctness and static analysis, but right now this is not a priority, and considering dubious implementation of the tool it would be easier to remove it for now and come up with a proper implementation later on, or wen can turn all hacks back into sem. - Not testsed as a part of CI so right now it can't even be built, due to file reorganization https://github.com/nim-works/nimskull/pull/177. - Adds reports for `--staticBounds:on|off` that were mistakenly assumed to be drnim-only during earlier refactor https://github.com/nim-works/nimskull/pull/94 for structured reports. Closes https://github.com/nim-works/nimskull/pull/130 as this pull removes `drnim` as well, and the author of that PR is no longer responsive. Due to multiple merge conflicts it is highly unlikely the old PR will be revived. --- compiler/ast/ast_types.nim | 9 +- compiler/ast/reports.nim | 11 +- compiler/ast/trees.nim | 6 - compiler/ast/wordrecg.nim | 3 +- compiler/front/cli_reporter.nim | 13 +- compiler/modules/modulegraphs.nim | 3 +- compiler/sem/guards.nim | 24 - compiler/sem/pragmas.nim | 54 +- compiler/sem/semmagic.nim | 43 - compiler/sem/semparallel.nim | 1 - compiler/sem/sempass2.nim | 63 +- compiler/sem/sigmatch.nim | 5 +- doc/drnim.rst | 205 ----- doc/rstcommon.rst | 2 - drnim/drnim.nim | 1272 --------------------------- drnim/nim.cfg | 18 - drnim/tests/config.nims | 10 - drnim/tests/tbasic_array_index.nim | 51 -- drnim/tests/tensures.nim | 74 -- drnim/tests/tphi.nim | 23 - drnim/tests/tsetlen_invalidates.nim | 26 - tools/koch/koch.nim | 28 - 22 files changed, 30 insertions(+), 1914 deletions(-) delete mode 100644 doc/drnim.rst delete mode 100644 drnim/drnim.nim delete mode 100644 drnim/nim.cfg delete mode 100644 drnim/tests/config.nims delete mode 100644 drnim/tests/tbasic_array_index.nim delete mode 100644 drnim/tests/tensures.nim delete mode 100644 drnim/tests/tphi.nim delete mode 100644 drnim/tests/tsetlen_invalidates.nim 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":