NKI Dataflow

[JTurcotti]

Implements a NKIWalker to translate NKI ASTs into CFGs, then performs a dataflow analysis over the CFG to search for any variable reads that may be reached without a write. Examples are pretty printed when running NKIDataflow.lean, for example:

YES [SAFETY PROVEN]

NKIDataflow.lean:660:0
NO [SAFETY NOT PROVEN] BECAUSE: 
def test():
	x = 0
	c = 0
	p = 0
	if c:
		p(x)
	else:
		y = 0
		p(y)
	p(⦃!y⦄)
  
NKIDataflow.lean:664:0
NO [SAFETY NOT PROVEN] BECAUSE: 
def test():
	x = 0
	c = 0
	p = 0
	if c:
		p(x)
		for z in x:
			w = 0
			p(w)
			p(z)
		p(⦃!w⦄)
		p(⦃!z⦄)
	else:
		y = 0
		p(x)
		p(y)
	p(x)
	p(⦃!y⦄)
	p(⦃!z⦄)