From 5bc24191f97125a35a7e3168c0f5c3db7c6e625c Mon Sep 17 00:00:00 2001 From: Juan Carlos Date: Mon, 27 Dec 2021 19:47:21 -0800 Subject: [PATCH] this is just stupid --- compiler/sempass2.nim | 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 - lib/std/logic.nim | 10 - tests/effects/tstrict_funcs_imports.nim | 1 - 10 files changed, 1487 deletions(-) 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 delete mode 100644 lib/std/logic.nim diff --git a/compiler/sempass2.nim b/compiler/sempass2.nim index e834b2d5d6d..5e6bfcf8af6 100644 --- a/compiler/sempass2.nim +++ b/compiler/sempass2.nim @@ -756,8 +756,6 @@ proc patchResult(c: PEffects; n: PNode) = 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: - localError(c.config, n.info, "routine has no return type, but .requires contains 'result'") else: for i in 0.. (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/lib/std/logic.nim b/lib/std/logic.nim deleted file mode 100644 index 84640d3807f..00000000000 --- a/lib/std/logic.nim +++ /dev/null @@ -1,10 +0,0 @@ -## This module provides further logic operators like 'forall' and 'exists' -## They are only supported in `.ensures` etc pragmas. - -proc `->`*(a, b: bool): bool {.magic: "Implies".} -proc `<->`*(a, b: bool): bool {.magic: "Iff".} - -proc forall*(args: varargs[untyped]): bool {.magic: "Forall".} -proc exists*(args: varargs[untyped]): bool {.magic: "Exists".} - -proc old*[T](x: T): T {.magic: "Old".} diff --git a/tests/effects/tstrict_funcs_imports.nim b/tests/effects/tstrict_funcs_imports.nim index 29cc707283b..7e42733fedf 100644 --- a/tests/effects/tstrict_funcs_imports.nim +++ b/tests/effects/tstrict_funcs_imports.nim @@ -139,7 +139,6 @@ import std/[ exitprocs, isolation, jsonutils, - logic, monotimes, packedsets, setutils,