# # # The Nim Compiler # (c) Copyright 2015 Andreas Rumpf # # See the file "copying.txt", included in this # distribution, for details about the copyright. # ## This module implements the 'implies' relation for guards. import ast, astalgo, msgs, magicsys, nimsets, trees, types, renderer, idents, saturate, modulegraphs, options, lineinfos const someEq = {mEqI, mEqF64, mEqEnum, mEqCh, mEqB, mEqRef, mEqProc, mEqUntracedRef, mEqStr, mEqSet, mEqCString} # set excluded here as the semantics are vastly different: someLe = {mLeI, mLeF64, mLeU, mLeU64, mLeEnum, mLeCh, mLeB, mLePtr, mLeStr} someLt = {mLtI, mLtF64, mLtU, mLtU64, mLtEnum, mLtCh, mLtB, mLtPtr, mLtStr} someLen = {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq, mXLenStr, mXLenSeq} someIn = {mInRange, mInSet} someHigh = {mHigh} # we don't list unsigned here because wrap around semantics suck for # proving anything: someAdd = {mAddI, mAddF64, mSucc} someSub = {mSubI, mSubF64, mPred} someMul = {mMulI, mMulF64} someDiv = {mDivI, mDivF64} someMod = {mModI} someMax = {mMaxI, mMaxF64} someMin = {mMinI, mMinF64} someBinaryOp = someAdd+someSub+someMul+someMax+someMin proc isValue(n: PNode): bool = n.kind in {nkCharLit..nkNilLit} proc isLocation(n: PNode): bool = not n.isValue 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 proc isVar(n: PNode): bool = n.kind == nkSym and n.sym.kind in {skResult, skVar} and {sfAddrTaken} * n.sym.flags == {} proc isLetLocation(m: PNode, isApprox: bool): bool = # consider: 'n[].kind' --> we really need to support 1 deref op even if this # is technically wrong due to aliasing :-( We could introduce "soft" facts # for this; this would still be very useful for warnings and also nicely # solves the 'var' problems. For now we fix this by requiring much more # restrictive expressions for the 'not nil' checking. var n = m var derefs = 0 while true: case n.kind of nkDotExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv: n = n.sons[0] of nkDerefExpr, nkHiddenDeref: n = n.sons[0] inc derefs of nkBracketExpr: if isConstExpr(n.sons[1]) or isLet(n.sons[1]) or isConstExpr(n.sons[1].skipConv): n = n.sons[0] else: return of nkHiddenStdConv, nkHiddenSubConv, nkConv: n = n.sons[1] else: break result = n.isLet and derefs <= ord(isApprox) if not result and isApprox: result = isVar(n) proc interestingCaseExpr*(m: PNode): bool = isLetLocation(m, true) type Operators* = object opNot, opContains, opLe, opLt, opAnd, opOr, opIsNil, opEq: PSym opAdd, opSub, opMul, opDiv, opLen: PSym proc initOperators*(g: ModuleGraph): Operators = result.opLe = createMagic(g, "<=", mLeI) result.opLt = createMagic(g, "<", mLtI) result.opAnd = createMagic(g, "and", mAnd) result.opOr = createMagic(g, "or", mOr) result.opIsNil = createMagic(g, "isnil", mIsNil) result.opEq = createMagic(g, "==", mEqI) result.opAdd = createMagic(g, "+", mAddI) result.opSub = createMagic(g, "-", mSubI) result.opMul = createMagic(g, "*", mMulI) result.opDiv = createMagic(g, "div", mDivI) result.opLen = createMagic(g, "len", mLengthSeq) result.opNot = createMagic(g, "not", mNot) result.opContains = createMagic(g, "contains", mInSet) proc swapArgs(fact: PNode, newOp: PSym): PNode = result = newNodeI(nkCall, fact.info, 3) result.sons[0] = newSymNode(newOp) result.sons[1] = fact.sons[2] result.sons[2] = fact.sons[1] proc neg(n: PNode; o: Operators): PNode = if n == nil: return nil case n.getMagic of mNot: result = n.sons[1] of someLt: # not (a < b) == a >= b == b <= a result = swapArgs(n, o.opLe) of someLe: result = swapArgs(n, o.opLt) of mInSet: if n.sons[1].kind != nkCurly: return nil let t = n.sons[2].typ.skipTypes(abstractInst) result = newNodeI(nkCall, n.info, 3) result.sons[0] = n.sons[0] result.sons[2] = n.sons[2] if t.kind == tyEnum: var s = newNodeIT(nkCurly, n.info, n.sons[1].typ) for e in t.n: let eAsNode = newIntNode(nkIntLit, e.sym.position) if not inSet(n.sons[1], eAsNode): s.add eAsNode result.sons[1] = s #elif t.kind notin {tyString, tySequence} and lengthOrd(t) < 1000: # result.sons[1] = complement(n.sons[1]) else: # not ({2, 3, 4}.contains(x)) x != 2 and x != 3 and x != 4 # XXX todo result = nil of mOr: # not (a or b) --> not a and not b let a = n.sons[1].neg(o) b = n.sons[2].neg(o) if a != nil and b != nil: result = newNodeI(nkCall, n.info, 3) result.sons[0] = newSymNode(o.opAnd) result.sons[1] = a result.sons[2] = b elif a != nil: result = a elif b != nil: result = b else: # leave not (a == 4) as it is result = newNodeI(nkCall, n.info, 2) result.sons[0] = newSymNode(o.opNot) result.sons[1] = n proc buildCall(op: PSym; a: PNode): PNode = result = newNodeI(nkCall, a.info, 2) result.sons[0] = newSymNode(op) result.sons[1] = a proc buildCall(op: PSym; a, b: PNode): PNode = result = newNodeI(nkInfix, a.info, 3) result.sons[0] = newSymNode(op) result.sons[1] = a result.sons[2] = b proc `|+|`(a, b: PNode): PNode = result = copyNode(a) if a.kind in {nkCharLit..nkUInt64Lit}: result.intVal = a.intVal |+| b.intVal else: result.floatVal = a.floatVal + b.floatVal proc `|-|`(a, b: PNode): PNode = result = copyNode(a) if a.kind in {nkCharLit..nkUInt64Lit}: result.intVal = a.intVal |-| b.intVal else: result.floatVal = a.floatVal - b.floatVal proc `|*|`(a, b: PNode): PNode = result = copyNode(a) if a.kind in {nkCharLit..nkUInt64Lit}: result.intVal = a.intVal |*| b.intVal else: result.floatVal = a.floatVal * b.floatVal proc `|div|`(a, b: PNode): PNode = result = copyNode(a) if a.kind in {nkCharLit..nkUInt64Lit}: result.intVal = a.intVal div b.intVal else: result.floatVal = a.floatVal / b.floatVal proc negate(a, b, res: PNode; o: Operators): PNode = if b.kind in {nkCharLit..nkUInt64Lit} and b.intVal != low(BiggestInt): var b = copyNode(b) b.intVal = -b.intVal if a.kind in {nkCharLit..nkUInt64Lit}: b.intVal = b.intVal |+| a.intVal result = b else: result = buildCall(o.opAdd, a, b) elif b.kind in {nkFloatLit..nkFloat64Lit}: var b = copyNode(b) b.floatVal = -b.floatVal result = buildCall(o.opAdd, a, b) else: result = res proc zero(): PNode = nkIntLit.newIntNode(0) proc one(): PNode = nkIntLit.newIntNode(1) proc minusOne(): PNode = nkIntLit.newIntNode(-1) proc lowBound*(conf: ConfigRef; x: PNode): PNode = result = nkIntLit.newIntNode(firstOrd(conf, x.typ)) result.info = x.info proc highBound*(conf: ConfigRef; x: PNode; o: Operators): PNode = let typ = x.typ.skipTypes(abstractInst) result = if typ.kind == tyArray: nkIntLit.newIntNode(lastOrd(conf, typ)) elif typ.kind == tySequence and x.kind == nkSym and x.sym.kind == skConst: nkIntLit.newIntNode(x.sym.ast.len-1) else: o.o
#
#
#           The Nim Compiler
#        (c) Copyright 2012 Andreas Rumpf
#
#    See the file "copying.txt", included in this
#    distribution, for details about the copyright.
#

## Serialization utilities for the compiler.
import strutils

proc c_sprintf(buf, frmt: cstring) {.importc: "sprintf", header: "<stdio.h>", nodecl, varargs.}

proc toStrMaxPrecision*(f: BiggestFloat): string =
  if f != f:
    result = "NAN"
  elif f == 0.0:
    result = "0.0"
  elif f == 0.5 * f:
    if f > 0.0: result = "INF"
    else: result = "-INF"
  else:
    var buf: array[0..80, char]
    c_sprintf(buf, "%#.16e", f)
    result = $buf

proc encodeStr*(s: string, result: var string) =
  for i in countup(0, len(s) - 1):
    case s[i]
    of 'a'..'z', 'A'..'Z', '0'..'9', '_': add(result, s[i])
    else: add(result, '\\' & toHex(ord(s[i]), 2))

proc hexChar(c: char, xi: var int) =
  case c
  of '0'..'9': xi = (xi shl 4) or (ord(c) - ord('0'))
  of 'a'..'f': xi = (xi shl 4) or (ord(c) - ord('a') + 10)
  of 'A'..'F': xi = (xi shl 4) or (ord(c) - ord('A') + 10)
  else: discard

proc decodeStr*(s: cstring, pos: var int): string =
  var i = pos
  result = ""
  while true:
    case s[i]
    of '\\':
      inc(i, 3)
      var xi = 0
      hexChar(s[i-2], xi)
      hexChar(s[i-1], xi)
      add(result, chr(xi))
    of 'a'..'z', 'A'..'Z', '0'..'9', '_':
      add(result, s[i])
      inc(i)
    else: break
  pos = i

const
  chars = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"

# since negative numbers require a leading '-' they use up 1 byte. Thus we
# subtract/add `vintDelta` here to save space for small negative numbers
# which are common in ROD files:
const
  vintDelta = 5

template encodeIntImpl(self: expr) =
  var d: char
  var v = x
  var rem = v mod 190
  if rem < 0:
    add(result, '-')
    v = - (v div 190)
    rem = - rem
  else:
    v = v div 190
  var idx = int(rem)
  if idx < 62: d = chars[idx]
  else: d = chr(idx - 62 + 128)
  if v != 0: self(v, result)
  add(result, d)

proc encodeVBiggestIntAux(x: BiggestInt, result: var string) =
  ## encode a biggest int as a variable length base 190 int.
  encodeIntImpl(encodeVBiggestIntAux)

proc encodeVBiggestInt*(x: BiggestInt, result: var string) =
  ## encode a biggest int as a variable length base 190 int.
  encodeVBiggestIntAux(x +% vintDelta, result)
  #  encodeIntImpl(encodeVBiggestInt)

proc encodeVIntAux(x: int, result: var string) =
  ## encode an int as a variable length base 190 int.
  encodeIntImpl(encodeVIntAux)

proc encodeVInt*(x: int, result: var string) =
  ## encode an int as a variable length base 190 int.
  encodeVIntAux(x +% vintDelta, result)

template decodeIntImpl() =
  var i = pos
  var sign = - 1
  assert(s[i] in {'a'..'z'