summary refs log blame commit diff stats
path: root/compiler/pluginsupport.nim
blob: f67942c97926dcc9e4bc40cac69328553d29fa09 (plain) (tree) 
4be0d1652 ^









b8fce9c58 ^



4be0d1652 ^











5de900b45 ^


50e83d643 ^

4be0d1652 ^

5de900b45 ^


4be0d1652 ^


5de900b45 ^


4be0d1652 ^














1
2
3
4
5
6
7
8
9

10
11
12

13
14
15
16
17
18
19
20
21
22
23

24
25

26

27

28
29

30
31

32
33

34
35
36
37
38
39
40
41
42
43
44
45
46
47









                                                   


                                                          










                                                                   

                          
                                 
                                                

                                    

                                                   

                                      













                                                                      
#
#
#           The Nim Compiler
#        (c) Copyright 2015 Andreas Rumpf
#
#    See the file "copying.txt", included in this
#    distribution, for details about the copyright.
#

## Plugin support for the Nim compiler. Right now plugins
## need to be built with the compiler only: plugins using 
## DLLs or the FFI will not work.

import ast, semdata, idents

type
  Transformation* = proc (c: PContext; n: PNode): PNode {.nimcall.}
  Plugin = ref object
    fn, module, package: PIdent
    t: Transformation
    next: Plugin

proc pluginMatches(p: Plugin; s: PSym): bool =
  if s.name.id != p.fn.id:
    return false
  let module = s.skipGenericOwner
  if module == nil or module.kind != skModule or
      module.name.id != p.module.id:
    return false
  let package = module.owner
  if package == nil or package.kind != skPackage or
      package.name.id != p.package.id:
    return false
  return true

var head: Plugin

proc getPlugin*(fn: PSym): Transformation =
  var it = head
  while it != nil:
    if pluginMatches(it, fn): return it.t
    it = it.next

proc registerPlugin*(package, module, fn: string; t: Transformation) =
  let oldHead = head
  head = Plugin(fn: getIdent(fn), module: getIdent(module),
                 package: getIdent(package), t: t, next: oldHead)
generated by cgit-pink 1.4.1-2-gfad0 (git 2.36.2.497.gbbea4dcf42) at 2025-01-29 02:42:30 +0000
id='n699' href='#n699'>699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 
#
#
#           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, int128

when defined(nimPreviewSlimSystem):
  import std/assertions

const
  someEq = {mEqI, mEqF64, mEqEnum, mEqCh, mEqB, mEqRef, mEqProc,
    mEqStr, mEqSet, mEqCString}

  # set excluded here as the semantics are vastly different:
  someLe = {mLeI, mLeF64, mLeU, mLeEnum,
            mLeCh, mLeB, mLePtr, mLeStr}
  someLt = {mLtI, mLtF64, mLtU, mLtEnum,
            mLtCh, mLtB, mLtPtr, mLtStr}

  someLen = {mLengthOpenArray, mLengthStr, mLengthArray, mLengthSeq}

  someIn = {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}
  someMin = {mMinI}
  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 notin {tyVar}:
      result = true
    else:
      result = false
  else:
    result = false

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[0]
    of nkDerefExpr:
      n = n[0]
      inc derefs
    of nkHiddenDeref:
      n = n[0]
      if not isApprox: inc derefs
    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
  result = n.isLet and derefs <= ord(isApprox)
  if not result and isApprox:
    result = isVar(n)

proc interestingCaseExpr*(m: PNode): bool = isLetLocation(m, true)

proc swapArgs(fact: PNode, newOp: PSym): PNode =
  result = newNodeI(nkCall, fact.info, 3)
  result[0] = newSymNode(newOp)
  result[1] = fact[2]
  result[2] = fact[1]

proc neg(n: PNode; o: Operators): PNode =
  if n == nil: return nil
  case n.getMagic
  of mNot:
    result = n[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[1].kind != nkCurly: return nil
    let t = n[2].typ.skipTypes(abstractInst)
    result = newNodeI(nkCall, n.info, 3)
    result[0] = n[0]
    result[2] = n[2]
    if t.kind == tyEnum:
      var s = newNodeIT(nkCurly, n.info, n[1].typ)
      for e in t.n:
        let eAsNode = newIntNode(nkIntLit, e.sym.position)
        if not inSet(n[1], eAsNode): s.add eAsNode
      result[1] = s
    #elif t.kind notin {tyString, tySequence} and lengthOrd(t) < 1000:
    #  result[1] = complement(n[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[1].neg(o)
      b = n[2].neg(o)
    if a != nil and b != nil:
      result = newNodeI(nkCall, n.info, 3)
      result[0] = newSymNode(o.opAnd)
      result[1] = a
      result[2] = b
    elif a != nil:
      result = a
    elif b != nil:
      result = b
    else:
      result = nil
  else:
    # leave  not (a == 4)  as it is
    result = newNodeI(nkCall, n.info, 2)
    result[0] = newSymNode(o.opNot)
    result[1] = n

proc buildCall*(op: PSym; a: PNode): PNode =
  result = newNodeI(nkCall, a.info, 2)
  result[0] = newSymNode(op)
  result[1] = a

proc buildCall*(op: PSym; a, b: PNode): PNode =
  result = newNodeI(nkInfix, a.info, 3)
  result[0] = newSymNode(op)
  result[1] = a
  result[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.astdef.len-1)
           else:
             o.opAdd.buildCall(o.opLen.buildCall(x), minusOne())
  result.info = x.info

proc reassociation(n: PNode; o: Operators): PNode =
  result = n
  # (foo+5)+5 --> foo+10;  same for '*'
  case result.getMagic
  of someAdd:
    if result[2].isValue and
        result[1].getMagic in someAdd and result[1][2].isValue:
      result = o.opAdd.buildCall(result[1][1], result[1][2] |+| result[2])
      if result[2].intVal == 0:
        result = result[1]
  of someMul:
    if result[2].isValue and
        result[1].getMagic in someMul and result[1][2].isValue:
      result = o.opMul.buildCall(result[1][1], result[1][2] |*| result[2])
      if result[2].intVal == 1:
        result = result[1]
      elif result[2].intVal == 0:
        result = zero()
  else: discard

proc pred(n: PNode): PNode =
  if n.kind in {nkCharLit..nkUInt64Lit} and n.intVal != low(BiggestInt):
    result = copyNode(n)
    dec result.intVal
  else:
    result = n

proc buildLe*(o: Operators; a, b: PNode): PNode =
  result = o.opLe.buildCall(a, b)

proc canon*(n: PNode; o: Operators): PNode =
  if n.safeLen >= 1:
    result = shallowCopy(n)
    for i in 0..<n.len:
      result[i] = canon(n[i], o)
  elif n.kind == nkSym and n.sym.kind == skLet and
      n.sym.astdef.getMagic in (someEq + someAdd + someMul + someMin +
      someMax + someHigh + someSub + someLen + someDiv):
    result = n.sym.astdef.copyTree
  else:
    result = n
  case result.getMagic
  of someEq, someAdd, someMul, someMin, someMax:
    # these are symmetric; put value as last:
    if result[1].isValue and not result[2].isValue:
      result = swapArgs(result, result[0].sym)
      # (4 + foo) + 2 --> (foo + 4) + 2
  of someHigh:
    # high == len+(-1)
    result = o.opAdd.buildCall(o.opLen.buildCall(result[1]), minusOne())
  of someSub:
    # x - 4  -->  x + (-4)
    result = negate(result[1], result[2], result, o)
  of someLen:
    result[0] = o.opLen.newSymNode
  of someLt - {mLtF64}:
    # x < y  same as x <= y-1:
    let y = n[2].canon(o)
    let p = pred(y)
    let minus = if p != y: p else: o.opAdd.buildCall(y, minusOne()).canon(o)
    result = o.opLe.buildCall(n[1].canon(o), minus)
  else: discard

  result = skipConv(result)
  result = reassociation(result, o)
  # most important rule: (x-4) <= a.len -->  x <= a.len+4
  case result.getMagic
  of someLe:
    let x = result[1]
    let y = result[2]
    if x.kind in nkCallKinds and x.len == 3 and x[2].isValue and
        isLetLocation(x[1], true):
      case x.getMagic
      of someSub:
        result = buildCall(result[0].sym, x[1],
                           reassociation(o.opAdd.buildCall(y, x[2]), o))
      of someAdd:
        # Rule A:
        let plus = negate(y, x[2], nil, o).reassociation(o)
        if plus != nil: result = buildCall(result[0].sym, x[1], plus)
      else: discard
    elif y.kind in nkCallKinds and y.len == 3 and y[2].isValue and
        isLetLocation(y[1], true):
      # a.len < x-3
      case y.getMagic
      of someSub:
        result = buildCall(result[0].sym, y[1],
                           reassociation(o.opAdd.buildCall(x, y[2]), o))
      of someAdd:
        let plus = negate(x, y[2], nil, o).reassociation(o)
        # ensure that Rule A will not trigger afterwards with the
        # additional 'not isLetLocation' constraint:
        if plus != nil and not isLetLocation(x, true):
          result = buildCall(result[0].sym, plus, y[1])
      else: discard
    elif x.isValue and y.getMagic in someAdd and y[2].kind == x.kind:
      # 0 <= a.len + 3
      # -3 <= a.len
      result[1] = x |-| y[2]
      result[2] = y[1]
    elif x.isValue and y.getMagic in someSub and y[2].kind == x.kind:
      # 0 <= a.len - 3
      # 3 <= a.len
      result[1] = x |+| y[2]
      result[2] = y[1]
  else: discard

proc buildAdd*(a: PNode; b: BiggestInt; o: Operators): PNode =
  canon(if b != 0: o.opAdd.buildCall(a, nkIntLit.newIntNode(b)) else: a, o)

proc usefulFact(n: PNode; o: Operators): PNode =
  case n.getMagic
  of someEq:
    if skipConv(n[2]).kind == nkNilLit and (
        isLetLocation(n[1], false) or isVar(n[1])):
      result = o.opIsNil.buildCall(n[1])
    else:
      if isLetLocation(n[1], true) or isLetLocation(n[2], true):
        # XXX algebraic simplifications!  'i-1 < a.len' --> 'i < a.len+1'
        result = n
      elif n[1].getMagic in someLen or n[2].getMagic in someLen:
        result = n
      else:
        result = nil
  of someLe+someLt:
    if isLetLocation(n[1], true) or isLetLocation(n[2], true):
      # XXX algebraic simplifications!  'i-1 < a.len' --> 'i < a.len+1'
      result = n
    elif n[1].getMagic in someLen or n[2].getMagic in someLen:
      # XXX Rethink this whole idea of 'usefulFact' for semparallel
      result = n
    else:
      result = nil
  of mIsNil:
    if isLetLocation(n[1], false) or isVar(n[1]):
      result = n
    else:
      result = nil
  of someIn:
    if isLetLocation(n[1], true):
      result = n
    else:
      result = nil
  of mAnd:
    let
      a = usefulFact(n[1], o)
      b = usefulFact(n[2], o)
    if a != nil and b != nil:
      result = newNodeI(nkCall, n.info, 3)
      result[0] = newSymNode(o.opAnd)
      result[1] = a
      result[2] = b
    elif a != nil:
      result = a
    elif b != nil:
      result = b
    else:
      result = nil
  of mNot:
    let a = usefulFact(n[1], o)
    if a != nil:
      result = a.neg(o)
    else:
      result = nil
  of mOr:
    # 'or' sucks! (p.isNil or q.isNil) --> hard to do anything
    # with that knowledge...
    # DeMorgan helps a little though:
    #   not a or not b --> not (a and b)
    #  (x == 3) or (y == 2)  ---> not ( not (x==3) and not (y == 2))
    #  not (x != 3 and y != 2)
    let
      a = usefulFact(n[1], o).neg(o)
      b = usefulFact(n[2], o).neg(o)
    if a != nil and b != nil:
      result = newNodeI(nkCall, n.info, 3)
      result[0] = newSymNode(o.opAnd)
      result[1] = a
      result[2] = b
      result = result.neg(o)
    else:
      result = nil
  elif n.kind == nkSym and n.sym.kind == skLet:
    # consider:
    #   let a = 2 < x
    #   if a:
    #     ...
    # We make can easily replace 'a' by '2 < x' here:
    if n.sym.astdef != nil:
      result = usefulFact(n.sym.astdef, o)
    else:
      result = nil
  elif n.kind == nkStmtListExpr:
    result = usefulFact(n.lastSon, o)
  else:
    result = nil

type
  TModel* = object
    s*: seq[PNode] # the "knowledge base"
    g*: ModuleGraph
    beSmart*: bool

proc addFact*(m: var TModel, nn: PNode) =
  let n = usefulFact(nn, m.g.operators)
  if n != nil:
    if not m.beSmart:
      m.s.add n
    else:
      let c = canon(n, m.g.operators)
      if c.getMagic == mAnd:
        addFact(m, c[1])
        addFact(m, c[2])
      else:
        m.s.add c

proc addFactNeg*(m: var TModel, n: PNode) =
  let n = n.neg(m.g.operators)
  if n != nil: addFact(m, n)

proc sameOpr(a, b: PSym): bool =
  case a.magic
  of someEq: result = b.magic in someEq
  of someLe: result = b.magic in someLe
  of someLt: result = b.magic in someLt
  of someLen: result = b.magic in someLen
  of someAdd: result = b.magic in someAdd
  of someSub: result = b.magic in someSub
  of someMul: result = b.magic in someMul
  of someDiv: result = b.magic in someDiv
  else: result = a == b

proc sameTree*(a, b: PNode): bool =
  result = false
  if a == b:
    result = true
  elif a != nil and b != nil and a.kind == b.kind:
    case a.kind
    of nkSym:
      result = a.sym == b.sym
      if not result and a.sym.magic != mNone:
        result = a.sym.magic == b.sym.magic or sameOpr(a.sym, b.sym)
    of nkIdent: result = a.ident.id == b.ident.id
    of nkCharLit..nkUInt64Lit: result = a.intVal == b.intVal
    of nkFloatLit..nkFloat64Lit: result = a.floatVal == b.floatVal
    of nkStrLit..nkTripleStrLit: result = a.strVal == b.strVal
    of nkType: result = a.typ == b.typ
    of nkEmpty, nkNilLit: result = true
    else:
      if a.len == b.len:
        for i in 0..<a.len:
          if not sameTree(a[i], b[i]): return
        result = true

proc hasSubTree(n, x: PNode): bool =
  if n.sameTree(x): result = true
  else:
    case n.kind
    of nkEmpty..nkNilLit:
      result = n.sameTree(x)
    of nkFormalParams:
      result = false
    else:
      result = false
      for i in 0..<n.len:
        if hasSubTree(n[i], x): return true

proc invalidateFacts*(s: var seq[PNode], n: PNode) =
  # We are able to guard local vars (as opposed to 'let' variables)!
  # 'while p != nil: f(p); p = p.next'
  # This is actually quite easy to do:
  # Re-assignments (incl. pass to a 'var' param) trigger an invalidation
  # of every fact that contains 'v'.
  #
  #   if x < 4:
  #     if y < 5
  #       x = unknown()
  #       # we invalidate 'x' here but it's known that x >= 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)
  else:
    result = false

proc impliesEq(fact, eq: PNode): TImplication =
  let (loc, val) = if isLocation(eq[1]): (1, 2) else: (2, 1)

  case fact[0].sym.magic
  of someEq:
    if sameTree(fact[1], eq[loc]):
      # this is not correct; consider:  a == b;  a == 1 --> unknown!
      if sameTree(fact[2], eq[val]): result = impYes
      elif valuesUnequal(fact[2], eq[val]): result = impNo
      else:
        result = impUnknown
    elif sameTree(fact[2], eq[loc]):
      if sameTree(fact[1], eq[val]): result = impYes
      elif valuesUnequal(fact[1], eq[val]): result = impNo
      else:
        result = impUnknown
    else:
      result = impUnknown
  of mInSet:
    # remember: mInSet is 'contains' so the set comes first!
    if sameTree(fact[2], eq[loc]) and isValue(eq[val]):
      if inSet(fact[1], eq[val]): result = impYes
      else: result = impNo
    else:
      result = impUnknown
  of mNot, mOr, mAnd:
    result = impUnknown
    assert(false, "impliesEq")
  else: result = impUnknown

proc leImpliesIn(x, c, aSet: PNode): TImplication =
  if c.kind in {nkCharLit..nkUInt64Lit}:
    # fact:  x <= 4;  question x in {56}?
    # --> true if every value <= 4 is in the set {56}
    #
    var value = newIntNode(c.kind, firstOrd(nil, x.typ))
    # don't iterate too often:
    if c.intVal - value.intVal < 1000:
      var i, pos, neg: int = 0
      while value.intVal <= c.intVal:
        if inSet(aSet, value): inc pos
        else: inc neg
        inc i; inc value.intVal
      if pos == i: result = impYes
      elif neg == i: result = impNo
      else:
        result = impUnknown
    else:
      result = impUnknown
  else:
    result = impUnknown

proc geImpliesIn(x, c, aSet: PNode): TImplication =
  if c.kind in {nkCharLit..nkUInt64Lit}:
    # fact:  x >= 4;  question x in {56}?
    # --> true iff every value >= 4 is in the set {56}
    #
    var value = newIntNode(c.kind, c.intVal)
    let max = lastOrd(nil, x.typ)
    # don't iterate too often:
    if max - getInt(value) < toInt128(1000):
      var i, pos, neg: int = 0
      while value.intVal <= max:
        if inSet(aSet, value): inc pos
        else: inc neg
        inc i; inc value.intVal
      if pos == i: result = impYes
      elif neg == i: result = impNo
      else: result = impUnknown
    else:
      result = impUnknown
  else:
    result = impUnknown

proc compareSets(a, b: PNode): TImplication =
  if equalSets(nil, a, b): result = impYes
  elif intersectSets(nil, a, b).len == 0: result = impNo
  else: result = impUnknown

proc impliesIn(fact, loc, aSet: PNode): TImplication =
  case fact[0].sym.magic
  of someEq:
    if sameTree(fact[1], loc):
      if inSet(aSet, fact[2]): result = impYes
      else: result = impNo
    elif sameTree(fact[2], loc):
      if inSet(aSet, fact[1]): result = impYes
      else: result = impNo
    else:
      result = impUnknown
  of mInSet:
    if sameTree(fact[2], loc):
      result = compareSets(fact[1], aSet)
    else:
      result = impUnknown
  of someLe:
    if sameTree(fact[1], loc):
      result = leImpliesIn(fact[1], fact[2], aSet)
    elif sameTree(fact[2], loc):
      result = geImpliesIn(fact[2], fact[1], aSet)
    else:
      result = impUnknown
  of someLt:
    if sameTree(fact[1], loc):
      result = leImpliesIn(fact[1], fact[2].pred, aSet)
    elif sameTree(fact[2], loc):
      # 4 < x  -->  3 <= x
      result = geImpliesIn(fact[2], fact[1].pred, aSet)
    else:
      result = impUnknown
  of mNot, mOr, mAnd:
    result = impUnknown
    assert(false, "impliesIn")
  else: result = impUnknown

proc valueIsNil(n: PNode): TImplication =
  if n.kind == nkNilLit: impYes
  elif n.kind in {nkStrLit..nkTripleStrLit, nkBracket, nkObjConstr}: impNo
  else: impUnknown

proc impliesIsNil(fact, eq: PNode): TImplication =
  case fact[0].sym.magic
  of mIsNil:
    if sameTree(fact[1], eq[1]):
      result = impYes
    else:
      result = impUnknown
  of someEq:
    if sameTree(fact[1], eq[1]):
      result = valueIsNil(fact[2].skipConv)
    elif sameTree(fact[2], eq[1]):
      result = valueIsNil(fact[1].skipConv)
    else:
      result = impUnknown
  of mNot, mOr, mAnd:
    result = impUnknown
    assert(false, "impliesIsNil")
  else: result = impUnknown

proc impliesGe(fact, x, c: PNode): TImplication =
  assert isLocation(x)
  case fact[0].sym.magic
  of someEq:
    if sameTree(fact[1], x):
      if isValue(fact[2]) and isValue(c):
        # fact:  x = 4;  question x >= 56? --> true iff 4 >= 56
        if leValue(c, fact[2]): result = impYes
        else: result = impNo
      else:
        result = impUnknown
    elif sameTree(fact[2], x):
      if isValue(fact[1]) and isValue(c):
        if leValue(c, fact[1]): result = impYes
        else: result = impNo
      else:
        result = impUnknown
    else:
      result = impUnknown
  of someLt:
    if sameTree(fact[1], x):
      if isValue(fact[2]) and isValue(c):
        # fact:  x < 4;  question N <= x? --> false iff N <= 4
        if leValue(fact[2], c): result = impNo
        else: result = impUnknown
        # fact:  x < 4;  question 2 <= x? --> we don't know
      else:
        result = impUnknown
    elif sameTree(fact[2], x):
      # fact: 3 < x; question: N-1 < x ?  --> true iff N-1 <= 3
      if isValue(fact[1]) and isValue(c):
        if leValue(c.pred, fact[1]): result = impYes
        else: result = impUnknown
      else:
        result = impUnknown
    else:
      result = impUnknown
  of someLe:
    if sameTree(fact[1], x):
      if isValue(fact[2]) and isValue(c):
        # fact:  x <= 4;  question x >= 56? --> false iff 4 <= 56
        if leValue(fact[2], c): result = impNo
        # fact:  x <= 4;  question x >= 2? --> we don't know
        else:
          result = impUnknown
      else:
        result = impUnknown
    elif sameTree(fact[2], x):
      # fact: 3 <= x; question: x >= 2 ?  --> true iff 2 <= 3
      if isValue(fact[1]) and isValue(c):
        if leValue(c, fact[1]): result = impYes
        else: result = impUnknown
      else:
        result = impUnknown
    else:
      result = impUnknown
  of mNot, mOr, mAnd:
    result = impUnknown
    assert(false, "impliesGe")
  else: result = impUnknown

proc impliesLe(fact, x, c: PNode): TImplication =
  if not isLocation(x):
    if c.isValue:
      if leValue(x, x): return impYes
      else: return impNo
    return impliesGe(fact, c, x)
  case fact[0].sym.magic
  of someEq:
    if sameTree(fact[1], x):
      if isValue(fact[2]) and isValue(c):
        # fact:  x = 4;  question x <= 56? --> true iff 4 <= 56
        if leValue(fact[2], c): result = impYes
        else: result = impNo
      else:
        result = impUnknown
    elif sameTree(fact[2], x):
      if isValue(fact[1]) and isValue(c):
        if leValue(fact[1], c): result = impYes
        else: result = impNo
      else:
        result = impUnknown
    else:
      result = impUnknown
  of someLt:
    if sameTree(fact[1], x):
      if isValue(fact[2]) and isValue(c):
        # fact:  x < 4;  question x <= N? --> true iff N-1 <= 4
        if leValue(fact[2], c.pred): result = impYes
        else:
          result = impUnknown
        # fact:  x < 4;  question x <= 2? --> we don't know
      else:
        result = impUnknown
    elif sameTree(fact[2], x):
      # fact: 3 < x; question: x <= 1 ?  --> false iff 1 <= 3
      if isValue(fact[1]) and isValue(c):
        if leValue(c, fact[1]): result = impNo
        else: result = impUnknown
      else:
        result = impUnknown
    else:
      result = impUnknown
  of someLe:
    if sameTree(fact[1], x):
      if isValue(fact[2]) and isValue(c):
        # fact:  x <= 4;  question x <= 56? --> true iff 4 <= 56
        if leValue(fact[2], c): result = impYes
        else: result = impUnknown
        # fact:  x <= 4;  question x <= 2? --> we don't know
      else:
        result = impUnknown

    elif sameTree(fact[2], x):
      # fact: 3 <= x; question: x <= 2 ?  --> false iff 2 < 3
      if isValue(fact[1]) and isValue(c):
        if leValue(c, fact[1].pred): result = impNo
        else:result = impUnknown
      else:
        result = impUnknown
    else:
      result = impUnknown

  of mNot, mOr, mAnd:
    result = impUnknown
    assert(false, "impliesLe")
  else: result = impUnknown

proc impliesLt(fact, x, c: PNode): TImplication =
  # x < 3  same as x <= 2:
  let p = c.pred
  if p != c:
    result = impliesLe(fact, x, p)
  else:
    # 4 < x  same as 3 <= x
    let q = x.pred
    if q != x:
      result = impliesLe(fact, q, c)
    else:
      result = impUnknown

proc `~`(x: TImplication): TImplication =
  case x
  of impUnknown: impUnknown
  of impNo: impYes
  of impYes: impNo

proc factImplies(fact, prop: PNode): TImplication =
  case fact.getMagic
  of mNot:
    # Consider:
    # enum nkBinary, nkTernary, nkStr
    # fact:      not (k <= nkBinary)
    # question:  k in {nkStr}
    # --> 'not' for facts is entirely different than 'not' for questions!
    # it's provably wrong if every value > 4 is in the set {56}
    # That's because we compute the implication and  'a -> not b' cannot
    # be treated the same as 'not a -> b'

    #  (not a) -> b  compute as  not (a -> b) ???
    #  == not a or not b == not (a and b)
    let arg = fact[1]
    case arg.getMagic
    of mIsNil, mEqRef:
      return ~factImplies(arg, prop)
    of mAnd:
      # not (a and b)  means  not a or not b:
      # a or b --> both need to imply 'prop'
      let a = factImplies(arg[1], prop)
      let b = factImplies(arg[2], prop)
      if a == b: return ~a
      return impUnknown
    else:
      return impUnknown
  of mAnd:
    result = factImplies(fact[1], prop)
    if result != impUnknown: return result
    return factImplies(fact[2], prop)
  else: discard

  case prop[0].sym.magic
  of mNot: result = ~fact.factImplies(prop[1])
  of mIsNil: result = impliesIsNil(fact, prop)
  of someEq: result = impliesEq(fact, prop)
  of someLe: result = impliesLe(fact, prop[1], prop[2])
  of someLt: result = impliesLt(fact, prop[1], prop[2])
  of mInSet: result = impliesIn(fact, prop[2], prop[1])
  else: result = impUnknown

proc doesImply*(facts: TModel, prop: PNode): TImplication =
  assert prop.kind in nkCallKinds
  result = impUnknown
  for f in facts.s:
    # facts can be invalidated, in which case they are 'nil':
    if not f.isNil:
      result = f.factImplies(prop)
      if result != impUnknown: return

proc impliesNotNil*(m: TModel, arg: PNode): TImplication =
  result = doesImply(m, m.g.operators.opIsNil.buildCall(arg).neg(m.g.operators))

proc simpleSlice*(a, b: PNode): BiggestInt =
  # returns 'c' if a..b matches (i+c)..(i+c), -1 otherwise. (i)..(i) is matched
  # as if it is (i+0)..(i+0).
  if guards.sameTree(a, b):
    if a.getMagic in someAdd and a[2].kind in {nkCharLit..nkUInt64Lit}:
      result = a[2].intVal
    else:
      result = 0
  else:
    result = -1


template isMul(x): untyped = x.getMagic in someMul
template isDiv(x): untyped = x.getMagic in someDiv
template isAdd(x): untyped = x.getMagic in someAdd
template isSub(x): untyped = x.getMagic in someSub
template isVal(x): untyped = x.kind in {nkCharLit..nkUInt64Lit}
template isIntVal(x, y): untyped = x.intVal == y

import std/macros

macro `=~`(x: PNode, pat: untyped): bool =
  proc m(x, pat, conds: NimNode) =
    case pat.kind
    of nnkInfix:
      case $pat[0]
      of "*": conds.add getAst(isMul(x))
      of "/": conds.add getAst(isDiv(x))
      of "+": conds.add getAst(isAdd(x))
      of "-": conds.add getAst(isSub(x))
      else:
        error("invalid pattern")
      m(newTree(nnkBracketExpr, x, newLit(1)), pat[1], conds)
      m(newTree(nnkBracketExpr, x, newLit(2)), pat[2], conds)
    of nnkPar:
      if pat.len == 1:
        m(x, pat[0], conds)
      else:
        error("invalid pattern")
    of nnkIdent:
      let c = newTree(nnkStmtListExpr, newLetStmt(pat, x))
      conds.add c
      # XXX why is this 'isVal(pat)' and not 'isVal(x)'?
      if ($pat)[^1] == 'c': c.add(getAst(isVal(x)))
      else: c.add bindSym"true"
    of nnkIntLit:
      conds.add(getAst(isIntVal(x, pat.intVal)))
    else:
      error("invalid pattern")

  var conds = newTree(nnkBracket)
  m(x, pat, conds)
  result = nestList(ident"and", conds)

proc isMinusOne(n: PNode): bool =
  n.kind in {nkCharLit..nkUInt64Lit} and n.intVal == -1

proc pleViaModel(model: TModel; aa, bb: PNode): TImplication

proc ple(m: TModel; a, b: PNode): TImplication =
  template `<=?`(a,b): untyped = ple(m,a,b) == impYes
  template `>=?`(a,b): untyped = ple(m, nkIntLit.newIntNode(b), a) == impYes

  #   0 <= 3
  if a.isValue and b.isValue:
    return if leValue(a, b): impYes else: impNo

  # use type information too:  x <= 4  iff  high(x) <= 4
  if b.isValue and a.typ != nil and a.typ.isOrdinalType:
    if lastOrd(nil, a.typ) <= b.intVal: return impYes
  # 3 <= x   iff  low(x) <= 3
  if a.isValue and b.typ != nil and b.typ.isOrdinalType:
    if a.intVal <= firstOrd(nil, b.typ): return impYes

  # x <= x
  if sameTree(a, b): return impYes

  # 0 <= x.len
  if b.getMagic in someLen and a.isValue:
    if a.intVal <= 0: return impYes

  #   x <= y+c  if 0 <= c and x <= y
  #   x <= y+(-c)  if c <= 0  and y >= x
  if b.getMagic in someAdd:
    if zero() <=? b[2] and a <=? b[1]: return impYes
    # x <= y-c  if x+c <= y
    if b[2] <=? zero() and (canon(m.g.operators.opSub.buildCall(a, b[2]), m.g.operators) <=? b[1]):
      return impYes

  #   x+c <= y  if c <= 0 and x <= y
  if a.getMagic in someAdd and a[2] <=? zero() and a[1] <=? b: return impYes

  #   x <= y*c  if  1 <= c and x <= y  and 0 <= y
  if b.getMagic in someMul:
    if a <=? b[1] and one() <=? b[2] and zero() <=? b[1]: return impYes


  if a.getMagic in someMul and a[2].isValue and a[1].getMagic in someDiv and
      a[1][2].isValue:
    # simplify   (x div 4) * 2 <= y   to  x div (c div d)  <= y
    if ple(m, buildCall(m.g.operators.opDiv, a[1][1], `|div|`(a[1][2], a[2])), b) == impYes:
      return impYes

  # x*3 + x == x*4. It follows that:
  # x*3 + y <= x*4  if  y <= x  and 3 <= 4
  if a =~ x*dc + y and b =~ x2*ec:
    if sameTree(x, x2):
      let ec1 = m.g.operators.opAdd.buildCall(ec, minusOne())
      if x >=? 1 and ec >=? 1 and dc >=? 1 and dc <=? ec1 and y <=? x:
        return impYes
  elif a =~ x*dc and b =~ x2*ec + y:
    #echo "BUG cam ehrer e ", a, " <=? ", b
    if sameTree(x, x2):
      let ec1 = m.g.operators.opAdd.buildCall(ec, minusOne())
      if x >=? 1 and ec >=? 1 and dc >=? 1 and dc <=? ec1 and y <=? zero():
        return impYes

  #  x+c <= x+d  if c <= d. Same for *, - etc.
  if a.getMagic in someBinaryOp and a.getMagic == b.getMagic:
    if sameTree(a[1], b[1]) and a[2] <=? b[2]: return impYes
    elif sameTree(a[2], b[2]) and a[1] <=? b[1]: return impYes

  #   x div c <= y   if   1 <= c  and  0 <= y  and x <= y:
  if a.getMagic in someDiv:
    if one() <=? a[2] and zero() <=? b and a[1] <=? b: return impYes

    #  x div c <= x div d  if d <= c
    if b.getMagic in someDiv:
      if sameTree(a[1], b[1]) and b[2] <=? a[2]: return impYes

    # x div z <= x - 1   if  z <= x
    if a[2].isValue and b.getMagic in someAdd and b[2].isMinusOne:
      if a[2] <=? a[1] and sameTree(a[1], b[1]): return impYes

  # slightly subtle:
  # x <= max(y, z)  iff x <= y or x <= z
  # note that 'x <= max(x, z)' is a special case of the above rule
  if b.getMagic in someMax:
    if a <=? b[1] or a <=? b[2]: return impYes

  # min(x, y) <= z  iff x <= z or y <= z
  if a.getMagic in someMin:
    if a[1] <=? b or a[2] <=? b: return impYes

  # use the knowledge base:
  return pleViaModel(m, a, b)
  #return doesImply(m, o.opLe.buildCall(a, b))

type TReplacements = seq[tuple[a, b: PNode]]

proc replaceSubTree(n, x, by: PNode): PNode =
  if sameTree(n, x):
    result = by
  elif hasSubTree(n, x):
    result = shallowCopy(n)
    for i in 0..n.safeLen-1:
      result[i] = replaceSubTree(n[i], x, by)
  else:
    result = n

proc applyReplacements(n: PNode; rep: TReplacements): PNode =
  result = n
  for x in rep: result = result.replaceSubTree(x.a, x.b)

proc pleViaModelRec(m: var TModel; a, b: PNode): TImplication =
  # now check for inferrable facts: a <= b and b <= c  implies a <= c
  result = impUnknown
  for i in 0..m.s.high:
    let fact = m.s[i]
    if fact != nil and fact.getMagic in someLe:
      # mark as used:
      m.s[i] = nil
      # i <= len-100
      # i <=? len-1
      # --> true  if  (len-100) <= (len-1)
      let x = fact[1]
      let y = fact[2]
      # x <= y.
      # Question: x <= b? True iff y <= b.
      if sameTree(x, a):
        if ple(m, y, b) == impYes: return impYes
        if y.getMagic in someAdd and b.getMagic in someAdd and sameTree(y[1], b[1]):
          if ple(m, b[2], y[2]) == impYes:
            return impYes

      # x <= y implies a <= b  if  a <= x and y <= b
      if ple(m, a, x) == impYes:
        if ple(m, y, b) == impYes:
          return impYes
        #if pleViaModelRec(m, y, b): return impYes
      # fact:  16 <= i
      #         x    y
      # question: i <= 15? no!
      result = impliesLe(fact, a, b)
      if result != impUnknown:
        return result
      when false:
        # given: x <= y;  y==a;  x <= a this means: a <= b  if  x <= b
        if sameTree(y, a):
          result = ple(m, b, x)
          if result != impUnknown:
            return result

proc pleViaModel(model: TModel; aa, bb: PNode): TImplication =
  # compute replacements:
  var replacements: TReplacements = @[]
  for fact in model.s:
    if fact != nil and fact.getMagic in someEq:
      let a = fact[1]
      let b = fact[2]
      if a.kind == nkSym: replacements.add((a,b))
      else: replacements.add((b,a))
  var m = TModel()
  var a = aa
  var b = bb
  if replacements.len > 0:
    m.s = @[]
    m.g = model.g
    # make the other facts consistent:
    for fact in model.s:
      if fact != nil and fact.getMagic notin someEq:
        # XXX 'canon' should not be necessary here, but it is
        m.s.add applyReplacements(fact, replacements).canon(m.g.operators)
    a = applyReplacements(aa, replacements)
    b = applyReplacements(bb, replacements)
  else:
    # we have to make a copy here, because the model will be modified:
    m = model
  result = pleViaModelRec(m, a, b)

proc proveLe*(m: TModel; a, b: PNode): TImplication =
  let x = canon(m.g.operators.opLe.buildCall(a, b), m.g.operators)
  #echo "ROOT ", renderTree(x[1]), " <=? ", renderTree(x[2])
  result = ple(m, x[1], x[2])
  if result == impUnknown:
    # try an alternative:  a <= b  iff  not (b < a)  iff  not (b+1 <= a):
    let y = canon(m.g.operators.opLe.buildCall(m.g.operators.opAdd.buildCall(b, one()), a), m.g.operators)
    result = ~ple(m, y[1], y[2])

proc addFactLe*(m: var TModel; a, b: PNode) =
  m.s.add canon(m.g.operators.opLe.buildCall(a, b), m.g.operators)

proc addFactLt*(m: var TModel; a, b: PNode) =
  let bb = m.g.operators.opAdd.buildCall(b, minusOne())
  addFactLe(m, a, bb)

proc settype(n: PNode): PType =
  var idgen = idGeneratorForPackage(-1'i32)
  result = newType(tySet, idgen, n.typ.owner)
  addSonSkipIntLit(result, n.typ, idgen)

proc buildOf(it, loc: PNode; o: Operators): PNode =
  var s = newNodeI(nkCurly, it.info, it.len-1)
  s.typ = settype(loc)
  for i in 0..<it.len-1: s[i] = it[i]
  result = newNodeI(nkCall, it.info, 3)
  result[0] = newSymNode(o.opContains)
  result[1] = s
  result[2] = loc

proc buildElse(n: PNode; o: Operators): PNode =
  var s = newNodeIT(nkCurly, n.info, settype(n[0]))
  for i in 1..<n.len-1:
    let branch = n[i]
    assert branch.kind != nkElse
    if branch.kind == nkOfBranch:
      for j in 0..<branch.len-1:
        s.add(branch[j])
  result = newNodeI(nkCall, n.info, 3)
  result[0] = newSymNode(o.opContains)
  result[1] = s
  result[2] = n[0]

proc addDiscriminantFact*(m: var TModel, n: PNode) =
  var fact = newNodeI(nkCall, n.info, 3)
  fact[0] = newSymNode(m.g.operators.opEq)
  fact[1] = n[0]
  fact[2] = n[1]
  m.s.add fact

proc addAsgnFact*(m: var TModel, key, value: PNode) =
  var fact = newNodeI(nkCall, key.info, 3)
  fact[0] = newSymNode(m.g.operators.opEq)
  fact[1] = key
  fact[2] = value
  m.s.add fact

proc sameSubexprs*(m: TModel; a, b: PNode): bool =
  # This should be used to check whether two *path expressions* refer to the
  # same memory location according to 'm'. This is tricky:
  # lock a[i].guard:
  #   ...
  #   access a[i].guarded
  #
  # Here a[i] is the same as a[i] iff 'i' and 'a' are not changed via '...'.
  # However, nil checking requires exactly the same mechanism! But for now
  # we simply use sameTree and live with the unsoundness of the analysis.
  var check = newNodeI(nkCall, a.info, 3)
  check[0] = newSymNode(m.g.operators.opEq)
  check[1] = a
  check[2] = b
  result = m.doesImply(check) == impYes

proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) =
  let branch = n[i]
  if branch.kind == nkOfBranch:
    m.s.add buildOf(branch, n[0], m.g.operators)
  else:
    m.s.add n.buildElse(m.g.operators).neg(m.g.operators)

proc buildProperFieldCheck(access, check: PNode; o: Operators): PNode =
  if check[1].kind == nkCurly:
    result = copyTree(check)
    if access.kind == nkDotExpr:
      var a = copyTree(access)
      a[1] = check[2]
      result[2] = a
      # 'access.kind != nkDotExpr' can happen for object constructors
      # which we don't check yet
  else:
    # it is some 'not'
    assert check.getMagic == mNot
    result = buildProperFieldCheck(access, check[1], o).neg(o)

proc checkFieldAccess*(m: TModel, n: PNode; conf: ConfigRef; produceError: bool) =
  for i in 1..<n.len:
    let check = buildProperFieldCheck(n[0], n[i], m.g.operators)
    if check != nil and m.doesImply(check) != impYes:
      if produceError:
        localError(conf, n.info, "field access outside of valid case branch: " & renderTree(n[0]))
      else:
        message(conf, n.info, warnProveField, renderTree(n[0]))
      break
generated by cgit-pink 1.4.1-2-gfad0 (git 2.36.2.497.gbbea4dcf42) at 2025-01-29 02:42:23 +0000