Nil type check implementation (#15287)

* Nil checking
* Enable current older not nil checking again, run new checking only under flag, skip our test
* Enable tests, work on try/except and bugs, fix notnil tests

* Enable strictNotNil tests (currently with lowercase category) and add some expected output
* Work on try/except/finally: still some things unclear and a lot of code can raise out of try
* Fix the notnil build by going back to the old version of a test which I shouldn't have changed

* Fix test : use action compile
* Work on mutation and aliasing: not finished
* Render var parititions graph, try to understand it, fix a nilcheck if bug
* Rebase, progress on working with partitions
* Improve time logic
* Fix some bugs, use graph indices instead of symbol in nil map
* Fix bugs, test simpler ident aliasing for now, support two mutation levels
* Support ContentMutation and ReAssignment: for now just detect possible re assignment for var parameters of calls
* Enable several simple passing tests
* Cleanup a bit, fix condition/branch infix-related bug
* Remove some files, address some comments by Araq
* Use internalError and no quit for now
* Separate tests with expected warnings and with expected ok, fix a bug with if with a single branch related to copyMap
* Fix new data structures, bugs: make tests pass, disable some for now
* Work on fixing errors with non-sym nodes, aliasing: tests fail
* Work on alias support: simple set-based logic, todo more tests and ref sets?
* Use ref sets: TODO can we think of handle seq-s similar to varpartitions' Araq ones
* Handle defers in one place, stop raising in reverse to make an async test compile with strictNotNil, add a commented out test
* Dot expressions: call/reassignment. Other refactorings and distinct, SeqOfDistinct support. Checkout an older varpartitions
* Work on field tracking
* Backup : trying to fix bugs when running some stdlib stuff for running an async test
* Start a section about strict not nil checking in experimental manual
* Fix experimental strict not nil manual section and move it to another file based on Araq feedback
* Fix unstructured flow and double warning problems, fix manual, cleanup
* Fix if/elif/else : take in account structure according to Araq feedback
* Refactor a bit
* Work on bracket expr support, re-enable tests, clarify in manual/tests/implementation static index support for now
* Work on compiling stdlib and compiler with strictNotNil
* Small fixes to the manual for strictNotNil
* Fix idgen for strict check nil rebase
* Enable some simple tests, remove old stuff, comment out code/print
* Copy the original varpartitions source instead of my changes
* Remove some files

compiler/ast.nim

@@ -1004,7 +1004,7 @@ const
   ConstantDataTypes*: TTypeKinds = {tyArray, tySet,
                                     tyTuple, tySequence}
   NilableTypes*: TTypeKinds = {tyPointer, tyCString, tyRef, tyPtr,
-    tyProc, tyError}
+    tyProc, tyError} # TODO
   PtrLikeKinds*: TTypeKinds = {tyPointer, tyPtr} # for VM
   ExportableSymKinds* = {skVar, skConst, skProc, skFunc, skMethod, skType,
     skIterator,
@@ -1387,6 +1387,7 @@ proc newType*(kind: TTypeKind, id: ItemId; owner: PSym): PType =
       echo "KNID ", kind
       writeStackTrace()
 
+
 proc mergeLoc(a: var TLoc, b: TLoc) =
   if a.k == low(typeof(a.k)): a.k = b.k
   if a.storage == low(typeof(a.storage)): a.storage = b.storage
@@ -1952,9 +1953,13 @@ proc canRaise*(fn: PNode): bool =
   elif fn.kind == nkSym and fn.sym.magic == mEcho:
     result = true
   else:
-    result = fn.typ != nil and fn.typ.n != nil and ((fn.typ.n[0].len < effectListLen) or
-      (fn.typ.n[0][exceptionEffects] != nil and
-      fn.typ.n[0][exceptionEffects].safeLen > 0))
+    # TODO check for n having sons? or just return false for now if not
+    if fn.typ != nil and fn.typ.n != nil and fn.typ.n[0].kind == nkSym:
+      result = false
+    else:
+      result = fn.typ != nil and fn.typ.n != nil and ((fn.typ.n[0].len < effectListLen) or
+        (fn.typ.n[0][exceptionEffects] != nil and
+        fn.typ.n[0][exceptionEffects].safeLen > 0))
 
 proc toHumanStrImpl[T](kind: T, num: static int): string =
   result = $kind

compiler/lineinfos.nim

@@ -56,7 +56,7 @@ type
     warnLockLevel = "LockLevel", warnResultShadowed = "ResultShadowed",
     warnInconsistentSpacing = "Spacing",  warnCaseTransition = "CaseTransition",
     warnCycleCreated = "CycleCreated", warnObservableStores = "ObservableStores",
-    warnUser = "User",
+    warnUser = "User", warnStrictNotNil = "StrictNotNil",
 
     hintSuccess = "Success", hintSuccessX = "SuccessX", hintCC = "CC",
     hintLineTooLong = "LineTooLong", hintXDeclaredButNotUsed = "XDeclaredButNotUsed",
@@ -129,6 +129,7 @@ const
     warnCycleCreated: "$1",
     warnObservableStores: "observable stores to '$1'",
     warnUser: "$1",
+    warnStrictNotNil: "$1",
     hintSuccess: "operation successful: $#",
     # keep in sync with `testament.isSuccess`
     hintSuccessX: "${loc} lines; ${sec}s; $mem; $build build; proj: $project; out: $output",

compiler/options.nim

@@ -176,7 +176,8 @@ type
       ## Note: this feature can't be localized with {.push.}
     vmopsDanger,
     strictFuncs,
-    views
+    views,
+    strictNotNil
 
   LegacyFeature* = enum
     allowSemcheckedAstModification,

compiler/semobjconstr.nim

@@ -153,6 +153,7 @@ proc collectMissingFields(c: PContext, fieldsRecList: PNode,
       if assignment == nil:
         constrCtx.missingFields.add r.sym
 
+
 proc semConstructFields(c: PContext, n: PNode,
                         constrCtx: var ObjConstrContext,
                         flags: TExprFlags): InitStatus =

compiler/sempass2.nim

@@ -10,7 +10,7 @@
 import
   intsets, ast, astalgo, msgs, renderer, magicsys, types, idents, trees,
   wordrecg, strutils, options, guards, lineinfos, semfold, semdata,
-  modulegraphs, varpartitions, typeallowed
+  modulegraphs, varpartitions, typeallowed, nilcheck
 
 when defined(useDfa):
   import dfa
@@ -1344,7 +1344,10 @@ proc trackProc*(c: PContext; s: PSym, body: PNode) =
   when defined(useDfa):
     if s.name.s == "testp":
       dataflowAnalysis(s, body)
+                                                                                                                   
       when false: trackWrites(s, body)
+  if strictNotNil in c.features and s.kind == skProc:
+    checkNil(s, body, g.config, c.idgen)
 
 proc trackStmt*(c: PContext; module: PSym; n: PNode, isTopLevel: bool) =
   if n.kind in {nkPragma, nkMacroDef, nkTemplateDef, nkProcDef, nkFuncDef,

compiler/semtypes.nim

@@ -917,6 +917,7 @@ proc semAnyRef(c: PContext; n: PNode; kind: TTypeKind; prev: PType): PType =
     # check every except the last is an object:
     for i in isCall..<n.len-1:
       let ni = n[i]
+      # echo "semAnyRef ", "n: ", n, "i: ", i, "ni: ", ni
       if ni.kind == nkNilLit:
         isNilable = true
       else:
@@ -933,7 +934,7 @@ proc semAnyRef(c: PContext; n: PNode; kind: TTypeKind; prev: PType): PType =
     addSonSkipIntLit(result, t, c.idgen)
     if tfPartial in result.flags:
       if result.lastSon.kind == tyObject: incl(result.lastSon.flags, tfPartial)
-    #if not isNilable: result.flags.incl tfNotNil
+    # if not isNilable: result.flags.incl tfNotNil
     case wrapperKind
     of tyOwned:
       if optOwnedRefs in c.config.globalOptions:
@@ -1563,6 +1564,8 @@ proc semTypeClass(c: PContext, n: PNode, prev: PType): PType =
     if modifier != tyNone:
       dummyName = param[0]
       dummyType = c.makeTypeWithModifier(modifier, candidateTypeSlot)
+      # if modifier == tyRef:
+        # dummyType.flags.incl tfNotNil
       if modifier == tyTypeDesc:
         dummyType.flags.incl tfConceptMatchedTypeSym
         dummyType.flags.incl tfCheckedForDestructor
@@ -1747,9 +1750,11 @@ proc semTypeNode(c: PContext, n: PNode, prev: PType): PType =
           if n[2].kind != nkNilLit:
             localError(c.config, n.info,
               "Invalid syntax. When used with a type, 'not' can be followed only by 'nil'")
-          if notnil notin c.features:
+          if notnil notin c.features and strictNotNil notin c.features:
             localError(c.config, n.info,
-              "enable the 'not nil' annotation with {.experimental: \"notnil\".}")
+              "enable the 'not nil' annotation with {.experimental: \"notnil\".} or " &
+              "  the `strict not nil` annotation with {.experimental: \"strictNotNil\".} " &
+              "  the \"notnil\" one is going to be deprecated, so please use \"strictNotNil\"")
           let resolvedType = result.skipTypes({tyGenericInst, tyAlias, tySink, tyOwned})
           case resolvedType.kind
           of tyGenericParam, tyTypeDesc, tyFromExpr:

compiler/treetab.nim

@@ -12,8 +12,9 @@
 import
   hashes, ast, astalgo, types
 
-proc hashTree(n: PNode): Hash =
-  if n == nil: return
+proc hashTree*(n: PNode): Hash =
+  if n.isNil:
+    return
   result = ord(n.kind)
   case n.kind
   of nkEmpty, nkNilLit, nkType:
@@ -21,7 +22,7 @@ proc hashTree(n: PNode): Hash =
   of nkIdent:
     result = result !& n.ident.h
   of nkSym:
-    result = result !& n.sym.name.h
+    result = result !& n.sym.id
   of nkCharLit..nkUInt64Lit:
     if (n.intVal >= low(int)) and (n.intVal <= high(int)):
       result = result !& int(n.intVal)
@@ -33,6 +34,9 @@ proc hashTree(n: PNode): Hash =
   else:
     for i in 0..<n.len:
       result = result !& hashTree(n[i])
+  result = !$result
+  #echo "hashTree ", result
+  #echo n
 
 proc treesEquivalent(a, b: PNode): bool =
   if a == b:

compiler/varpartitions.nim

@@ -904,4 +904,4 @@ proc computeCursors*(s: PSym; n: PNode; config: ConfigRef) =
         discard "cannot cursor into a graph that is mutated"
       else:
         v.sym.flags.incl sfCursor
-        #echo "this is now a cursor ", v.sym, " ", par.s[rid].flags, " ", config $ v.sym.info
+        #echo "this is now a cursor ", v.sym, " ", par.s[rid].flags, " ", config $ v.sym.info

doc/manual_experimental.rst

@@ -465,6 +465,7 @@ The compiler ensures that every code path initializes variables which contain
 non-nilable pointers. The details of this analysis are still to be specified
 here.
 
+.. include:: manual_experimental_strictnotnil.rst
 
 Concepts
 ========

doc/manual_experimental_strictnotnil.rst

@@ -0,0 +1,235 @@
+
+Strict not nil checking
+=========================
+
+**Note:** This feature is experimental, you need to enable it with
+
+.. code-block:: nim
+  {.experimental: "strictNotNil".}
+
+or 
+
+.. code-block:: bash
+  nim c --experimental:strictNotNil <program>
+
+In the second case it would check builtin and imported modules as well.
+
+It checks the nilability of ref-like types and makes dereferencing safer based on flow typing and ``not nil`` annotations.
+
+Its implementation is different than the ``notnil`` one: defined under ``strictNotNil``. Keep in mind the difference in option names, be careful with distinguishing them.
+
+We check several kinds of types for nilability:
+
+- ref types
+- pointer types
+- proc types
+- cstrings
+
+nil
+-------
+
+The default kind of nilability types is the nilable kind: they can have the value ``nil``.
+If you have a non-nilable type ``T``, you can use ``T nil`` to get a nilable type for it.
+
+
+not nil
+--------
+
+You can annotate a type where nil isn't a valid value with ``not nil``.
+
+.. code-block:: nim
+    type
+      NilableObject = ref object
+        a: int
+      Object = NilableObject not nil
+
+      Proc = (proc (x, y: int))
+    
+    proc p(x: Object) =
+      echo x.a # ensured to dereference without an error
+    # compiler catches this:
+    p(nil)
+    # and also this:
+    var x: NilableObject
+    if x.isNil:
+      p(x)
+    else:
+      p(x) # ok
+
+
+
+If a type can include ``nil`` as a valid value, dereferencing values of the type
+is checked by the compiler: if a value which might be nil is derefenced, this produces a warning by default, you can turn this into an error using the compiler options ``--warningAsError:strictNotNil``
+
+If a type is nilable, you should dereference its values only after a ``isNil`` or equivalent check.
+
+local turn on/off
+---------------------
+
+You can still turn off nil checking on function/module level by using a ``{.strictNotNil: off}.`` pragma.
+Note: test that/TODO for code/manual.
+
+nilability state
+-----------------
+
+Currently a nilable value can be ``Safe``, ``MaybeNil`` or ``Nil`` : we use internally ``Parent`` and ``Unreachable`` but this is an implementation detail(a parent layer has the actual nilability).
+
+``Safe`` means it shouldn't be nil at that point: e.g. after assignment to a non-nil value or ``not a.isNil`` check
+``MaybeNil`` means it might be nil, but it might not be nil: e.g. an argument, a call argument or a value after an ``if`` and ``else``.
+``Nil`` means it should be nil at that point; e.g. after an assignment to ``nil`` or a ``.isNil`` check.
+
+``Unreachable`` means it shouldn't be possible to access this in this branch: so we do generate a warning as well.
+
+We show an error for each dereference (``[]``, ``.field``, ``[index]`` ``()`` etc) which is of a tracked expression which is
+in ``MaybeNil`` or ``Nil`` state.
+
+
+type nilability
+----------------
+
+Types are either nilable or non-nilable.
+When you pass a param or a default value, we use the type : for nilable types we return ``MaybeNil``
+and for non-nilable ``Safe``.
+
+TODO: fix the manual here. (This is not great, as default values for non-nilables and nilables are usually actually ``nil`` , so we should think a bit more about this section.)
+
+params rules
+------------
+
+Param's nilability is detected based on type nilability. We use the type of the argument to detect the nilability.
+
+
+assignment rules
+-----------------
+
+Let's say we have ``left = right``.
+
+When we assign, we pass the right's nilability to the left's expression. There should be special handling of aliasing and compound expressions which we specify in their sections. (Assignment is a possible alias ``move`` or ``move out``).
+
+call args rules
+-----------------
+
+When we call with arguments, we have two cases when we might change the nilability.
+
+.. code-block:: nim
+  callByVar(a)
+
+Here ``callByVar`` can re-assign ``a``, so this might change ``a``'s nilability, so we change it to ``MaybeNil``.
+This is also a possible aliasing ``move out`` (moving out of a current alias set).
+
+.. code-block:: nim
+  call(a)
+
+Here ``call`` can change a field or element of ``a``, so if we have a dependant expression of ``a`` : e.g. ``a.field``. Dependats become ``MaybeNil``.
+
+
+branches rules
+---------------
+
+Branches are the reason we do nil checking like this: with flow checking. 
+Sources of brancing are ``if``, ``while``, ``for``, ``and``, ``or``, ``case``, ``try`` and combinations with ``return``, ``break``, ``continue`` and ``raise``
+
+We create a new layer/"scope" for each branch where we map expressions to nilability. This happens when we "fork": usually on the beginning of a construct.
+When branches "join" we usually unify their expression maps or/and nilabilities.
+
+Merging usually merges maps and alias sets: nilabilities are merged like this:
+
+.. code-block:: nim
+  template union(l: Nilability, r: Nilability): Nilability =
+    ## unify two states
+    if l == r:
+      l
+    else:
+      MaybeNil
+
+Special handling is for ``.isNil`` and `` == nil``, also for ``not``, ``and`` and ``or``.
+
+``not`` reverses the nilability, ``and`` is similar to "forking" : the right expression is checked in the layer resulting from the left one and ``or`` is similar to "merging": the right and left expression should be both checked in the original layer.
+
+``isNil``, ``== nil`` make expressions ``Nil``. If there is a ``not`` or ``!= nil``, they make them ``Safe``.
+We also reverse the nilability in the opposite branch: e.g. ``else``.
+
+compound expressions: field, index expressions
+-----------------------------------------------
+
+We want to track also field(dot) and index(bracket) expressions.
+
+We track some of those compound expressions which might be nilable as dependants of their bases: ``a.field`` is changed if ``a`` is moved (re-assigned), 
+similarly ``a[index]`` is dependent on ``a`` and ``a.field.field`` on ``a.field``.
+
+When we move the base, we update dependants to ``MaybeNil``. Otherwise we usually start with type nilability.
+
+When we call args, we update the nilability of their dependants to ``MaybeNil`` as the calls usually can change them.
+We might need to check for ``strictFuncs`` pure funcs and not do that then.
+
+For field expressions ``a.field``, we calculate an integer value based on a hash of the tree and just accept equivalent trees as equivalent expressions.
+
+For item expression ``a[index]``, we also calculate an integer value based on a hash of the tree and accept equivalent trees as equivalent expressions: for static values only.
+For now we support only constant indices: we dont track expression with no-const indices. For those we just report a warning even if they are safe for now: one can use a local variable to workaround. For loops this might be annoying: so one should be able to turn off locally the warning using the ``{.warning[StrictCheckNotNil]:off}.``.
+
+For bracket expressions, in the future we might count ``a[<any>]`` as the same general expression.
+This means we should should the index but otherwise handle it the same for assign (maybe "aliasing" all the non-static elements) and differentiate only for static: e.g. ``a[0]`` and ``a[1]``.
+
+element tracking
+-----------------
+
+When we assign an object construction, we should track the fields as well: 
+
+
+.. code-block:: nim
+  var a = Nilable(field: Nilable()) # a : Safe, a.field: Safe
+
+Usually we just track the result of an expression: probably this should apply for elements in other cases as well.
+Also related to tracking initialization of expressions/fields.
+
+unstructured control flow rules
+-------------------------
+
+Unstructured control flow keywords as ``return``, ``break``, ``continue``, ``raise`` mean that we jump from a branch out.
+This means that if there is code after the finishing of the branch, it would be ran if one hasn't hit the direct parent branch of those: so it is similar to an ``else``. In those cases we should use the reverse nilabilities for the local to the condition expressions. E.g.
+
+.. code-block:: nim
+  for a in c:
+    if not a.isNil:
+      b()
+      break
+    code # here a: Nil , because if not, we would have breaked
+
+
+aliasing
+------------
+
+We support alias detection for local expressions.
+
+We track sets of aliased expressions. We start with all nilable local expressions in separate sets.
+Assignments and other changes to nilability can move / move out expressions of sets.
+
+``move``: Moving ``left`` to ``right`` means we remove ``left`` from its current set and unify it with the ``right``'s set.
+This means it stops being aliased with its previous aliases.
+
+.. code-block:: nim
+  var left = b
+  left = right # moving left to right
+
+``move out``: Moving out ``left`` might remove it from the current set and ensure that it's in its own set as a single element.
+e.g.
+
+
+.. code-block:: nim
+  var left = b
+  left = nil # moving out
+
+
+initialization of non nilable and nilable values
+-------------------------------------------------
+
+TODO
+
+warnings and errors
+---------------------
+
+We show an error for each dereference (`[]`, `.field`, `[index]` `()` etc) which is of a tracked expression which is
+in ``MaybeNil`` or ``Nil`` state.
+
+We might also show a history of the transitions and the reasons for them that might change the nilability of the expression.
+

tests/strictnotnil/tnilcheck.nim

@@ -0,0 +1,382 @@
+discard """
+cmd: "nim check $file"
+action: "reject"
+"""
+
+import tables
+
+{.experimental: "strictNotNil".}
+
+type
+  Nilable* = ref object
+    a*: int
+    field*: Nilable
+    
+  NonNilable* = Nilable not nil
+
+  Nilable2* = nil NonNilable
+
+
+# proc `[]`(a: Nilable, b: int): Nilable =
+#   nil
+
+
+# Nilable tests
+
+
+
+# test deref
+proc testDeref(a: Nilable) =
+  echo a.a > 0 #[tt.Warning
+       ^ can't deref a, it might be nil
+  ]#
+
+
+
+# # # test if else
+proc testIfElse(a: Nilable) =
+  if a.isNil:
+    echo a.a #[tt.Warning
+         ^ can't deref a, it is nil
+    ]#
+  else:
+    echo a.a # ok
+
+proc testIfNoElse(a: Nilable) =
+  if a.isNil:
+    echo a.a #[tt.Warning
+         ^ can't deref a, it is nil
+         ]#
+  echo a.a #[tt.Warning
+       ^ can't deref a, it might be nil
+   ]#
+
+proc testIfReturn(a: Nilable) =
+  if not a.isNil:
+    return
+  echo a.a #[tt.Warning
+       ^ can't deref a, it is nil
+  ]#
+
+proc testIfBreak(a: seq[Nilable]) =
+  for b in a:
+    if not b.isNil:
+      break
+    echo b.a #[tt.Warning
+         ^ can't deref b, it is nil
+    ]#
+
+proc testIfContinue(a: seq[Nilable]) =
+  for b in a:
+    if not b.isNil:
+      continue
+    echo b.a #[tt.Warning
+         ^ can't deref b, it is nil
+    ]#
+
+proc testIfRaise(a: Nilable) =
+  if not a.isNil:
+    raise newException(ValueError, "")
+  echo a.a #[tt.Warning
+       ^ can't deref a, it is nil
+  ]#
+
+proc testIfElif(a: Nilable) =
+  var c = 0
+  if c == 0:
+    echo a.a #[tt.Warning
+         ^ can't deref a, it might be nil
+      ]#
+  elif c == 1:
+    echo a.a #[tt.Warning
+         ^ can't deref a, it might be nil
+      ]#
+  elif not a.isNil:
+    echo a.a # ok
+  elif c == 2:
+    echo 0
+  else:
+    echo a.a #[tt.Warning
+         ^ can't deref a, it is nil
+    ]#
+
+proc testAssignUnify(a: Nilable, b: int) =
+  var a2 = a
+  if b == 0:
+    a2 = Nilable()
+  echo a2.a #[tt.Warning
+       ^ can't deref a2, it might be nil
+  ]#
+
+
+# # test assign in branch and unifiying that with the main block after end of branch
+proc testAssignUnifyNil(a: Nilable, b: int) =
+  var a2 = a
+  if b == 0:
+    a2 = nil
+  echo a2.a #[tt.Warning
+       ^ can't deref a2, it might be nil
+  ]#
+
+# test loop
+proc testForLoop(a: Nilable) =
+  var b = Nilable()
+  for i in 0 .. 5:
+    echo b.a #[tt.Warning
+         ^ can't deref b, it might be nil
+    ]#
+    if i == 2:
+      b = a
+  echo b.a #[tt.Warning
+       ^ can't deref b, it might be nil
+  ]#
+
+
+
+# # TODO implement this after discussion
+# # proc testResultCompoundNonNilableElement(a: Nilable): (NonNilable, NonNilable) = #[t t.Warning
+# #      ^ result might be not initialized, so it or an element might be nil
+# # ]#
+# #   if not a.isNil:
+# #     result[0] = a #[t t.Warning
+# #                 ^ can't assign nilable to non nilable: it might be nil
+# #     #]
+
+# # proc testNonNilDeref(a: NonNilable) =
+# #   echo a.a # ok
+
+
+
+# # # not only calls: we can use partitions for dependencies for field aliases
+# # # so we can detect on change what does this affect or was this mutated between us and the original field
+
+# # proc testRootAliasField(a: Nilable) =
+# #   var aliasA = a
+# #   if not a.isNil and not a.field.isNil:
+# #     aliasA.field = nil
+# #     # a.field = nil
+# #     # aliasA = nil 
+# #     echo a.field.a # [tt.Warning
+# #          ^ can't deref a.field, it might be nil
+# #     ]#
+
+
+proc testAliasChanging(a: Nilable) =
+  var b = a
+  var aliasA = b
+  b = Nilable()
+  if not b.isNil:
+    echo aliasA.a #[tt.Warning
+         ^ can't deref aliasA, it might be nil
+    ]#
+
+# # TODO
+# # proc testAliasUnion(a: Nilable) =
+# #   var a2 = a
+# #   var b = a2
+# #   if a.isNil:
+# #     b = Nilable()
+# #     a2 = nil
+# #   else:
+# #     a2 = Nilable()
+# #     b = a2
+# #   if not b.isNil:
+# #     echo a2.a #[ tt.Warning
+# #          ^ can't deref a2, it might be nil
+# #     ]#
+
+# # TODO after alias support
+# #proc callVar(a: var Nilable) =
+# #  a.field = nil
+
+
+# # TODO ptr support
+# # proc testPtrAlias(a: Nilable) =
+# #   # pointer to a: hm.
+# #   # alias to a?
+# #   var ptrA = a.unsafeAddr # {0, 1} 
+# #   if not a.isNil: # {0, 1}
+# #     ptrA[] = nil # {0, 1} 0: MaybeNil 1: MaybeNil
+# #     echo a.a #[ tt.Warning
+# #          ^ can't deref a, it might be nil
+# #     ]#
+
+# # TODO field stuff
+# # currently it just doesnt support dot, so accidentally it shows a warning but because that
+# # not alias i think
+# # proc testFieldAlias(a: Nilable) =
+# #   var b = a # {0, 1} {2} 
+# #   if not a.isNil and not a.field.isNil: # {0, 1} {2}
+# #     callVar(b) # {0, 1} {2} 0: Safe 1: Safe
+# #     echo a.field.a #[ tt.Warning
+# #           ^ can't deref a.field, it might be nil
+# #     ]#
+# #
+# # proc testUniqueHashTree(a: Nilable): Nilable =
+# #   # TODO what would be a clash
+# #   var field = 0
+# #   if not a.isNil and not a.field.isNil:
+# #     # echo a.field.a
+# #     echo a[field].a
+# #   result = Nilable()
+  
+# # proc testSeparateShadowingResult(a: Nilable): Nilable =
+# #   result = Nilable()
+# #   if not a.isNil:
+# #     var result: Nilable = nil
+# #   echo result.a
+
+
+proc testCStringDeref(a: cstring) =
+  echo a[0] #[tt.Warning
+       ^ can't deref a, it might be nil
+  ]#
+
+
+proc testNilablePtr(a: ptr int) =
+  if not a.isNil:
+    echo a[] # ok
+  echo a[] #[tt.Warning
+       ^ can't deref a, it might be nil
+  ]#
+
+# # proc testNonNilPtr(a: ptr int not nil) =
+# #   echo a[] # ok
+
+proc raiseCall: NonNilable = #[tt.Warning
+^ return value is nil
+]#
+  raise newException(ValueError, "raise for test") 
+
+# proc testTryCatch(a: Nilable) =
+#   var other = a
+#   try:
+#     other = raiseCall()
+#   except:
+#     discard
+#   echo other.a #[ tt.Warning
+#             ^ can't deref other, it might be nil
+#   ]#
+
+# # proc testTryCatchDetectNoRaise(a: Nilable) =
+# #   var other = Nilable()
+# #   try:
+# #     other = nil
+# #     other = a
+# #     other = Nilable()
+# #   except:
+# #     other = nil
+# #   echo other.a # ok
+
+# # proc testTryCatchDetectFinally =
+# #   var other = Nilable()
+# #   try:
+# #     other = nil
+# #     other = Nilable()
+# #   except:
+# #     other = Nilable()
+# #   finally:
+# #     other = nil
+# #   echo other.a # can't deref other: it is nil
+
+# # proc testTryCatchDetectNilableWithRaise(b: bool) =
+# #   var other = Nilable()
+# #   try:
+# #     if b:
+# #       other = nil
+# #     else:
+# #       other = Nilable()
+# #       var other2 = raiseCall()
+# #   except:
+# #     echo other.a # ok
+
+# #   echo other.a # can't deref a: it might be nil
+
+# # proc testRaise(a: Nilable) =
+# #   if a.isNil:
+# #     raise newException(ValueError, "a == nil")
+# #   echo a.a # ok
+
+
+# # proc testBlockScope(a: Nilable) =
+# #   var other = a
+# #   block:
+# #     var other = Nilable()
+# #     echo other.a # ok
+# #   echo other.a # can't deref other: it might be nil
+
+# # ok we can't really get the nil value from here, so should be ok
+# # proc testDirectRaiseCall: NonNilable =
+# #   var a = raiseCall()
+# #   result = NonNilable()
+
+# # proc testStmtList =
+# #   var a = Nilable()
+# #   block:
+# #     a = nil
+# #     a = Nilable()
+# #   echo a.a # ok
+
+proc callChange(a: Nilable) =
+  if not a.isNil:
+    a.field = nil
+
+proc testCallChangeField =
+  var a = Nilable()
+  a.field = Nilable()
+  callChange(a)
+  echo a.field.a #[ tt.Warning
+        ^ can't deref a.field, it might be nil
+       ]#
+
+proc testReassignVarWithField =
+  var a = Nilable()
+  a.field = Nilable()
+  echo a.field.a # ok
+  a = Nilable()
+  echo a.field.a #[ tt.Warning
+        ^ can't deref a.field, it might be nil
+        ]#
+
+
+proc testItemDeref(a: var seq[Nilable]) =
+  echo a[0].a #[tt.Warning
+        ^ can't deref a[0], it might be nil
+       ]#
+  a[0] = Nilable() # good: now .. if we dont track, how do we know 
+  echo a[0].a # ok
+  echo a[1].a #[tt.Warning
+        ^ can't deref a[1], it might be nil
+  ]#
+  var b = 1
+  if a[b].isNil:
+    echo a[1].a #[tt.Warning
+          ^ can't deref a[1], it might be nil
+    ]#
+    var c = 0
+    echo a[c].a #[tt.Warning
+          ^ can't deref a[c], it might be nil
+    ]#
+
+  # known false positive
+  if not a[b].isNil:
+    echo a[b].a #[tt.Warning
+          ^ can't deref a[b], it might be nil
+    ]#
+
+  const c = 0
+  if a[c].isNil:
+    echo a[0].a #[tt.Warning
+          ^ can't deref a[0], it is nil
+    ]#
+  a[c] = Nilable()
+  echo a[0].a # ok
+
+
+
+# # # proc test10(a: Nilable) =
+# # #   if not a.isNil and not a.b.isNil:
+# # #     c_memset(globalA.addr, 0, globalA.sizeOf.csize_t)
+# # #     globalA = nil
+# # #     echo a.a # can't deref a: it might be nil
+

tests/strictnotnil/tnilcheck_no_warnings.nim

@@ -0,0 +1,182 @@
+discard """
+cmd: "nim check --warningAsError:StrictNotNil $file"
+action: "compile"
+"""
+
+import tables
+
+{.experimental: "strictNotNil".}
+
+type
+  Nilable* = ref object
+    a*: int
+    field*: Nilable
+    
+  NonNilable* = Nilable not nil
+
+  Nilable2* = nil NonNilable
+
+
+# proc `[]`(a: Nilable, b: int): Nilable =
+#   nil
+
+
+# Nilable tests
+
+
+
+# # test and
+proc testAnd(a: Nilable) =
+  echo not a.isNil and a.a > 0 # ok
+
+
+# test else branch and inferring not isNil
+# proc testElse(a: Nilable, b: int) =
+#   if a.isNil:
+#     echo 0
+#   else:
+#     echo a.a
+
+# test that here we can infer that n can't be nil anymore
+proc testNotNilAfterAssign(a: Nilable, b: int) =
+  var n = a # a: MaybeNil n: MaybeNil
+  if n.isNil: # n: Safe a: MaybeNil
+    n = Nilable() # n: Safe a: MaybeNil
+  echo n.a # ok
+
+proc callVar(a: var Nilable) =
+   a = nil
+
+proc testVarAlias(a: Nilable) = # a: 0 aliasA: 1 {0} {1} 
+  var aliasA = a # {0, 1} 0 MaybeNil 1 MaybeNil
+  if not a.isNil: # {0, 1} 0 Safe 1 Safe
+    callVar(aliasA) # {0, 1} 0 MaybeNil 1 MaybeNil
+    # if aliasA stops being in alias: it might be nil, but then a is still not nil
+    # if not: it cant be nil as it still points here
+    echo a.a # ok 
+
+proc testAliasCheck(a: Nilable) =
+  var aliasA = a
+  if not a.isNil:
+    echo aliasA.a # ok
+
+proc testFieldCheck(a: Nilable) =
+  if not a.isNil and not a.field.isNil:
+    echo a.field.a # ok
+
+proc testTrackField =
+  var a = Nilable(field: Nilable())
+  echo a.field.a # ok
+
+proc testNonNilDeref(a: NonNilable) =
+  echo a.a # ok
+
+# # not only calls: we can use partitions for dependencies for field aliases
+# # so we can detect on change what does this affect or was this mutated between us and the original field
+
+
+# proc testUniqueHashTree(a: Nilable): Nilable =
+#   # TODO what would be a clash
+#   var field = 0
+#   if not a.isNil and not a.field.isNil:
+#     # echo a.field.a
+#     echo a[field].a
+#   result = Nilable()
+  
+proc testSeparateShadowingResult(a: Nilable): Nilable =
+  result = Nilable()
+  if not a.isNil:
+    var result: Nilable = nil
+  echo result.a
+
+
+proc testNonNilCString(a: cstring not nil) =
+  echo a[0] # ok
+
+proc testNonNilPtr(a: ptr int not nil) =
+  echo a[] # ok
+
+
+# proc testTryCatchDetectNoRaise(a: Nilable) =
+#   var other = Nilable()
+#   try:
+#     other = nil
+#     other = a
+#     other = Nilable()
+#   except:
+#     other = nil
+#   echo other.a # ok
+
+# proc testTryCatchDetectFinally =
+#   var other = Nilable()
+#   try:
+#     other = nil
+#     other = Nilable()
+#   except:
+#     other = Nilable()
+#   finally:
+#     other = nil
+#   echo other.a # can't deref other: it is nil
+
+# proc testTryCatchDetectNilableWithRaise(b: bool) =
+#   var other = Nilable()
+#   try:
+#     if b:
+#       other = nil
+#     else:
+#       other = Nilable()
+#       var other2 = raiseCall()
+#   except:
+#     echo other.a # ok
+
+#   echo other.a # can't deref a: it might be nil
+
+proc testRaise(a: Nilable) =
+  if a.isNil:
+    raise newException(ValueError, "a == nil")
+  echo a.a # ok
+
+# proc testBlockScope(a: Nilable) =
+#   var other = a
+#   block:
+#     var other = Nilable()
+#     echo other.a # ok
+#   echo other.a # can't deref other: it might be nil
+
+# # (ask Araq about this: not supported yet) ok we can't really get the nil value from here, so should be ok
+# proc testDirectRaiseCall: NonNilable =
+#   var a = raiseCall()
+#   result = NonNilable()
+
+proc testStmtList =
+  var a = Nilable()
+  block:
+    a = nil
+    a = Nilable()
+  echo a.a # ok
+
+proc testItemDerefNoWarning(a: var seq[Nilable]) =
+  a[0] = Nilable() # good: now .. if we dont track, how do we know 
+  echo a[0].a # ok
+  var b = 1
+
+  const c = 0
+  a[c] = Nilable()
+  echo a[0].a # ok
+
+# proc callChange(a: Nilable) =
+#   a.field = nil
+
+# proc testCallAlias =
+#   var a = Nilable(field: Nilable())
+#   callChange(a)
+#   echo a.field.a # can't deref a.field, it might be nil
+
+# # proc test10(a: Nilable) =
+# #   if not a.isNil and not a.b.isNil:
+# #     c_memset(globalA.addr, 0, globalA.sizeOf.csize_t)
+# #     globalA = nil
+# #     echo a.a # can't deref a: it might be nil
+
+var nilable: Nilable
+var withField = Nilable(a: 0, field: Nilable())