blob: bb809a06610c56d9e0232b25582628373e1d3f9e (
plain)
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
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
|
