summary refs log tree commit diff stats
path: root/doc/manual_experimental_strictnotnil.rst
diff options
context:
space:
mode:
authorAlexander Ivanov <alehander42@gmail.com>2020-12-29 11:31:11 +0200
committerGitHub <noreply@github.com>2020-12-29 10:31:11 +0100
commit672dc5cd87790dc7f44ad62ae66f07e96e665409 (patch)
tree31d101c8cd3dc6d71481812ab4ca74b98e0dcacf /doc/manual_experimental_strictnotnil.rst
parente70ac0f34c9f195f6e423b3ac7e54b912e62c71d (diff)
downloadNim-672dc5cd87790dc7f44ad62ae66f07e96e665409.tar.gz
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
Diffstat (limited to 'doc/manual_experimental_strictnotnil.rst')
-rw-r--r--doc/manual_experimental_strictnotnil.rst235
1 files changed, 235 insertions, 0 deletions
diff --git a/doc/manual_experimental_strictnotnil.rst b/doc/manual_experimental_strictnotnil.rst
new file mode 100644
index 000000000..d779162f4
--- /dev/null
+++ b/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.
+