Definedness tracking
====================

[ old notes. something similar is partially implemented ]

Method 1: Track defined vars on output
--------------------------------------

    bool za = ...
    bool zb = ...

  bb1:                  [ x:-  y:- ]
    bool x
    bool y
    if za goto bb2      [ x:-  y:- ]
    x = true
    goto bb3            [ x:D  y:- ]

  bb2:                  [ x:-  y:- ]
    y = true
    if zb goto bb1      [ x:-  y:D ]
    goto bb3            [ x:-  y:D ]

  bb3:                  [ x:-  y:- ]
    return

Method 2: Track required vars
-----------------------------
Track all reads in each bblock, and writes in each transition.

For all bblocks:
    - Add all read variables as dependencies.
      (except for variables that are assigned first in the same bblock).
    - Add all writes in all jumps/transitions.

    xxx- Recursively add all dependencies of all jump sources.
    xxx  Detect and stop if there is a loop.

Then, starting from the first bblock, do a depth-first search and track
variable state.
- Report any errors
- Increase the read dependencies of the nodes closer to the root,
  until there is a matching write.
- At transitions, stop if the bblock has been seen already with an equal
  or strictly smaller set of defined variables
- Add all leaf nodes (e.g. return) and all points where there is a
  backwards loop, to a list.

Lastly, process the list and check for unmet dependencies.
(this step could perhaps be done immediately during the step above).

Possible simplification
-----------------------
Alternative 1:
* Give backward-jumps (backward-goto and loops) special treatment:
    - Require that backward-jumps do not have undefined (or maybe-none) values
      that are not expected to be undefined (or maybe-none) in the target.
    - Require that lifetime-tracked objects are expected to be in the
      same state in the target bblock.

Alternative 2:
* Completely forbid backward goto
    - but there is still continue! so it will probably not help.
    - unless continue is ONLY allowed at the "top" of loops,
      and the "top" is forbidden from changing definedness/none-ness
* Require that loops do not undefine anything (or set to none)
* Require that loops do not.

Extending this to none vs not-none tracking
===========================================
Have 3 states:
    - undefined
    - defined, maybe none
    - defined, not none