spec for view types (#15424)

* spec for view types
* spec additions
* refactoring; there are two different kinds of views
* refactorings and spec additions
* enforce that view types are initialized
* enforce borrowing from the first formal parameter
* enforce lifetimes for borrowing of locals
* typo in the manual
* clarify in the implementation what a borrow operation really is

doc/manual.rst

@@ -655,7 +655,7 @@ Precedence level    Operators                                              First
 ================  =======================================================  ==================  ===============
 
 
-Whether an operator is used a prefix operator is also affected by preceding
+Whether an operator is used as a prefix operator is also affected by preceding
 whitespace (this parsing change was introduced with version 0.13.0):
 
 .. code-block:: nim
@@ -3275,16 +3275,16 @@ programming and are inherently unsafe.
 
 .. code-block:: nim
   cast[int](x)
-  
+
 The target type of a cast must be a concrete type, for instance, a target type
 that is a type class (which is non-concrete) would be invalid:
 
 .. code-block:: nim
   type Foo = int or float
   var x = cast[Foo](1) # Error: cannot cast to a non concrete type: 'Foo'
-  
+
 Type casts should not be confused with *type conversions,* as mentioned in the
-prior section. Unlike type conversions, a type cast cannot change the underlying 
+prior section. Unlike type conversions, a type cast cannot change the underlying
 bit pattern of the data being casted (aside from that the size of the target type
 may differ from the source type). Casting resembles *type punning* in other
 languages or C++'s ``reinterpret_cast`` and ``bit_cast`` features.

doc/manual_experimental.rst

@@ -1814,18 +1814,49 @@ For example:
     # an object reachable from 'n' is potentially mutated
 
 
-The algorithm behind this analysis is currently not documented.
+The algorithm behind this analysis is described in
+the `view types section <#view-types-algorithm>`_.
 
 
 View types
 ==========
 
-A view type is a type that contains one of the following types:
+**Note**:  ``--experimental:views`` is more effective
+with ``--experimental:strictFuncs``.
+
+A view type is a type that is or contains one of the following types:
 
 - ``var T`` (mutable view into ``T``)
 - ``lent T`` (immutable view into ``T``)
 - ``openArray[T]`` (pair of (pointer to array of ``T``, size))
 
+For example:
+
+.. code-block:: nim
+
+  type
+    View1 = var int
+    View2 = openArray[byte]
+    View3 = lent string
+    View4 = Table[openArray[char], int]
+
+
+Exceptions to this rule are types constructed via ``ptr`` or ``proc``.
+For example, the following types are **not** view types:
+
+.. code-block:: nim
+
+  type
+    NotView1 = proc (x: openArray[int])
+    NotView2 = ptr openArray[char]
+    NotView3 = ptr array[4, var int]
+
+
+A *mutable* view type is a type that is or contains a ``var T`` type.
+An *immutable* view type is a view type that is not a mutable view type.
+
+A *view* is a symbol (a let, var, const, etc.) that has a view type.
+
 Since version 1.4 Nim allows view types to be used as local variables.
 This feature needs to be enabled via ``{.experimental: "views".}``.
 
@@ -1860,10 +1891,159 @@ For example:
   main(@[11, 22, 33])
 
 
+A local variable of a view type can borrow from a location
+derived from a parameter, another local variable, a global ``const`` or ``let``
+symbol or a thread-local ``var`` or ``let``.
 
-If a view type is used as a return type, the location must borrow from the
-first parameter that is passed to the proc.
+Let ``p`` the proc that is analysed for the correctness of the borrow operation.
+
+Let ``source`` be one of:
+
+- A formal parameter of ``p``. Note that this does not cover parameters of
+  inner procs.
+- The ``result`` symbol of ``p``.
+- A local ``var`` or ``let`` or ``const`` of ``p``. Note that this does
+  not cover locals of inner procs.
+- A thread-local ``var`` or ``let``.
+- A global ``let`` or ``const``.
+- A constant arraq/seq/object/tuple constructor.
+
+
+Path expressions
+----------------
+
+A location derived from ``source`` is then defined as a path expression that
+has ``source`` as the owner. A path expression ``e`` is defined recursively:
+
+- ``source`` itself is a path expression.
+- Container access like ``e[i]`` is a path expression.
+- Tuple access ``e[0]`` is a path expression.
+- Object field access ``e.field`` is a path expression.
+- ``system.toOpenArray(e, ...)`` is a path expression.
+- Pointer dereference ``e[]`` is a path expression.
+- An address ``addr e``, ``unsafeAddr e`` is a path expression.
+- A type conversion ``T(e)`` is a path expression.
+- A cast expression ``cast[T](e)`` is a path expression.
+- ``f(e, ...)`` is a path expression if ``f``'s return type is a view type.
+  Because the view can only have been borrowed from ``e``, we then know
+  that owner of ``f(e, ...)`` is ``e``.
+
+
+If a view type is used as a return type, the location must borrow from a location
+that is derived from the first parameter that is passed to the proc.
 See https://nim-lang.org/docs/manual.html#procedures-var-return-type for
 details about how this is done for ``var T``.
 
-The algorithm behind this analysis is currently not documented.
+A mutable view can borrow from a mutable location, an immutable view can borrow
+from both a mutable or an immutable location.
+
+The *duration* of a borrow is the span of commands beginning from the assignment
+to the view and ending with the last usage of the view.
+
+For the duration of the borrow operation, no mutations to the borrowed locations
+may be performed except via the potentially mutable view that borrowed from the
+location. The borrowed location is said to be *sealed* during the borrow.
+
+.. code-block:: nim
+
+  {.experimental: "views".}
+
+  type
+    Obj = object
+      field: string
+
+  proc dangerous(s: var seq[Obj]) =
+    let v: lent Obj = s[0] # seal 's'
+    s.setLen 0  # prevented at compile-time because 's' is sealed.
+    echo v.field
+
+
+The scope of the view does not matter:
+
+.. code-block:: nim
+
+  proc valid(s: var seq[Obj]) =
+    let v: lent Obj = s[0]  # begin of borrow
+    echo v.field            # end of borrow
+    s.setLen 0  # valid because 'v' isn't used afterwards
+
+
+The analysis requires as much precision about mutations as is reasonably obtainable,
+so it is more effective with the experimental `strict funcs <#strict-funcs>`_
+feature. In other words ``--experimental:views`` works better
+with ``--experimental:strictFuncs``.
+
+The analysis is currently control flow insensitive:
+
+.. code-block:: nim
+
+  proc invalid(s: var seq[Obj]) =
+    let v: lent Obj = s[0]
+    if false:
+      s.setLen 0
+    echo v.field
+
+In this example, the compiler assumes that ``s.setLen 0`` invalidates the
+borrow operation of ``v`` even though a human being can easily see that it
+will never do that at runtime.
+
+
+Reborrows
+---------
+
+A view ``v`` can borrow from multiple different locations. However, the borrow
+is always the full span of ``v``'s lifetime and every location that is borrowed
+from is sealed during ``v``'s lifetime.
+
+
+Algorithm
+---------
+
+The following section is an outline of the algorithm that the current implementation
+uses. The algorithm performs two traversals over the AST of the procedure or global
+section of code that uses a view variable. No fixpoint iterations are performed, the
+complexity of the analysis is O(N) where N is the number of nodes of the AST.
+
+The first pass over the AST computes the lifetime of each local variable based on
+a notion of an "abstract time", in the implementation it's a simple integer that is
+incremented for every visited node.
+
+In the second pass information about the underlying object "graphs" is computed.
+Let ``v`` be a parameter or a local variable. Let ``G(v)`` be the graph
+that ``v`` belongs to. A graph is defined by the set of variables that belong
+to the graph. Initially for all ``v``: ``G(v) = {v}``. Every variable can only
+be part of a single graph.
+
+Assignments like ``a = b`` "connect" two variables, both variables end up in the
+same graph ``{a, b} = G(a) = G(b)``. Unfortunately, the pattern to look for is
+much more complex than that and can involve multiple assignment targets
+and sources::
+
+  f(x, y) = g(a, b)
+
+connects ``x`` and ``y`` to ``a`` and ``b``: ``G(x) = G(y) = G(a) = G(b) = {x, y, a, b}``.
+A type based alias analysis rules out some of these combinations, for example
+a ``string`` value cannot possibly be connected to a ``seq[int]``.
+
+A pattern like ``v[] = value`` or ``v.field = value`` marks ``G(v)`` as mutated.
+After the second pass a set of disjoint graphs was computed.
+
+For strict functions it is then enforced that there is no graph that is both mutated
+and has an element that is an immutable parameter (that is a parameter that is not
+of type ``var T``).
+
+For borrow checking a different set of checks is performed. Let ``v`` be the view
+and ``b`` the location that is borrowed from.
+
+- The lifetime of ``v`` must not exceed ``b``'s lifetime. Note: The lifetime of
+  a parameter is the complete proc body.
+- If ``v`` is a mutable view and ``v`` is used to actually mutate the
+  borrowed location, then ``b`` has to be a mutable location.
+  Note: If it is not actually used for mutation, borrowing a mutable view from an
+  immutable location is allowed! This allows for many important idioms and will be
+  justified in an upcoming RFC.
+- During ``v``'s lifetime, ``G(b)`` can only be modified by ``v`` (and only if
+  ``v`` is a mutable view).
+- If ``v`` is ``result`` then ``b`` has to be a location derived from the first
+  formal parameter or from a constant location.
+- A view cannot be used for a read or a write access before it was assigned to.