compiler: cleanup dfa.nim
This commit is contained in:
parent
dcc3ac74f4
commit
2fecf4f36a
1 changed files with 25 additions and 21 deletions
|
|
@ -7,18 +7,22 @@
|
||||||
# distribution, for details about the copyright.
|
# distribution, for details about the copyright.
|
||||||
#
|
#
|
||||||
|
|
||||||
## Data flow analysis for Nim. For now the task is to prove that every
|
## Data flow analysis for Nim.
|
||||||
## usage of a local variable 'v' is covered by an initialization to 'v'
|
|
||||||
## first.
|
|
||||||
## We transform the AST into a linear list of instructions first to
|
## We transform the AST into a linear list of instructions first to
|
||||||
## make this easier to handle: There are only 2 different branching
|
## make this easier to handle: There are only 2 different branching
|
||||||
## instructions: 'goto X' is an unconditional goto, 'fork X'
|
## instructions: 'goto X' is an unconditional goto, 'fork X'
|
||||||
## is a conditional goto (either the next instruction or 'X' can be
|
## is a conditional goto (either the next instruction or 'X' can be
|
||||||
## taken). Exhaustive case statements are translated
|
## taken). Exhaustive case statements could be translated
|
||||||
## so that the last branch is transformed into an 'else' branch.
|
## so that the last branch is transformed into an 'else' branch, but
|
||||||
|
## this is currently not done.
|
||||||
## ``return`` and ``break`` are all covered by 'goto'.
|
## ``return`` and ``break`` are all covered by 'goto'.
|
||||||
## The case to detect is ``use v`` that is not dominated by
|
##
|
||||||
## a ``def v``.
|
## Control flow through exception handling:
|
||||||
|
## Contrary to popular belief, exception handling doesn't cause
|
||||||
|
## many problems for this DFA representation, ``raise`` is a statement
|
||||||
|
## that ``goes to`` the outer ``finally`` or ``except`` if there is one,
|
||||||
|
## otherwise it is the same as ``return``.
|
||||||
|
##
|
||||||
## The data structures and algorithms used here are inspired by
|
## The data structures and algorithms used here are inspired by
|
||||||
## "A Graph–Free Approach to Data–Flow Analysis" by Markus Mohnen.
|
## "A Graph–Free Approach to Data–Flow Analysis" by Markus Mohnen.
|
||||||
## https://link.springer.com/content/pdf/10.1007/3-540-45937-5_6.pdf
|
## https://link.springer.com/content/pdf/10.1007/3-540-45937-5_6.pdf
|
||||||
|
|
@ -27,15 +31,11 @@ import ast, astalgo, types, intsets, tables, msgs, options, lineinfos
|
||||||
|
|
||||||
type
|
type
|
||||||
InstrKind* = enum
|
InstrKind* = enum
|
||||||
goto, fork, def, use,
|
goto, fork, def, use
|
||||||
useWithinCall # this strange special case is used to get more
|
|
||||||
# move optimizations out of regular code
|
|
||||||
# XXX This is still overly pessimistic in
|
|
||||||
# call(let x = foo; bar(x))
|
|
||||||
Instr* = object
|
Instr* = object
|
||||||
n*: PNode
|
n*: PNode
|
||||||
case kind*: InstrKind
|
case kind*: InstrKind
|
||||||
of def, use, useWithinCall: sym*: PSym
|
of def, use: sym*: PSym
|
||||||
of goto, fork: dest*: int
|
of goto, fork: dest*: int
|
||||||
|
|
||||||
ControlFlowGraph* = seq[Instr]
|
ControlFlowGraph* = seq[Instr]
|
||||||
|
|
@ -71,7 +71,7 @@ proc codeListing(c: ControlFlowGraph, result: var string, start=0; last = -1) =
|
||||||
result.add $c[i].kind
|
result.add $c[i].kind
|
||||||
result.add "\t"
|
result.add "\t"
|
||||||
case c[i].kind
|
case c[i].kind
|
||||||
of def, use, useWithinCall:
|
of def, use:
|
||||||
result.add c[i].sym.name.s
|
result.add c[i].sym.name.s
|
||||||
of goto, fork:
|
of goto, fork:
|
||||||
result.add "L"
|
result.add "L"
|
||||||
|
|
@ -199,6 +199,13 @@ proc genCase(c: var Con; n: PNode) =
|
||||||
# L2:
|
# L2:
|
||||||
# elsePart
|
# elsePart
|
||||||
# Lend:
|
# Lend:
|
||||||
|
when false:
|
||||||
|
# XXX Exhaustiveness is not yet mapped to the control flow graph as
|
||||||
|
# it seems to offer no benefits for the 'last read of' question.
|
||||||
|
let isExhaustive = skipTypes(n.sons[0].typ,
|
||||||
|
abstractVarRange-{tyTypeDesc}).kind in {tyFloat..tyFloat128, tyString} or
|
||||||
|
lastSon(n).kind == nkElse
|
||||||
|
|
||||||
var endings: seq[TPosition] = @[]
|
var endings: seq[TPosition] = @[]
|
||||||
c.gen(n.sons[0])
|
c.gen(n.sons[0])
|
||||||
for i in 1 ..< n.len:
|
for i in 1 ..< n.len:
|
||||||
|
|
@ -250,9 +257,6 @@ proc genUse(c: var Con; n: PNode) =
|
||||||
nkAddr, nkHiddenAddr}:
|
nkAddr, nkHiddenAddr}:
|
||||||
n = n[0]
|
n = n[0]
|
||||||
if n.kind == nkSym and n.sym.kind in InterestingSyms:
|
if n.kind == nkSym and n.sym.kind in InterestingSyms:
|
||||||
if c.inCall > 0:
|
|
||||||
c.code.add Instr(n: n, kind: useWithinCall, sym: n.sym)
|
|
||||||
else:
|
|
||||||
c.code.add Instr(n: n, kind: use, sym: n.sym)
|
c.code.add Instr(n: n, kind: use, sym: n.sym)
|
||||||
|
|
||||||
proc genDef(c: var Con; n: PNode) =
|
proc genDef(c: var Con; n: PNode) =
|
||||||
|
|
@ -345,7 +349,7 @@ proc dfa(code: seq[Instr]; conf: ConfigRef) =
|
||||||
d[i] = initIntSet()
|
d[i] = initIntSet()
|
||||||
c[i] = initIntSet()
|
c[i] = initIntSet()
|
||||||
case code[i].kind
|
case code[i].kind
|
||||||
of use, useWithinCall: u[i].incl(code[i].sym.id)
|
of use: u[i].incl(code[i].sym.id)
|
||||||
of def: d[i].incl(code[i].sym.id)
|
of def: d[i].incl(code[i].sym.id)
|
||||||
of fork, goto:
|
of fork, goto:
|
||||||
let d = i+code[i].dest
|
let d = i+code[i].dest
|
||||||
|
|
@ -407,7 +411,7 @@ proc dfa(code: seq[Instr]; conf: ConfigRef) =
|
||||||
#if someChange:
|
#if someChange:
|
||||||
w.add pc + code[pc].dest
|
w.add pc + code[pc].dest
|
||||||
inc pc
|
inc pc
|
||||||
of use, useWithinCall:
|
of use:
|
||||||
#if not d[prevPc].missingOrExcl():
|
#if not d[prevPc].missingOrExcl():
|
||||||
# someChange = true
|
# someChange = true
|
||||||
consuming = code[pc].sym.id
|
consuming = code[pc].sym.id
|
||||||
|
|
@ -424,7 +428,7 @@ proc dfa(code: seq[Instr]; conf: ConfigRef) =
|
||||||
# now check the condition we're interested in:
|
# now check the condition we're interested in:
|
||||||
for i in 0..<code.len:
|
for i in 0..<code.len:
|
||||||
case code[i].kind
|
case code[i].kind
|
||||||
of use, useWithinCall:
|
of use:
|
||||||
let s = code[i].sym
|
let s = code[i].sym
|
||||||
if s.id notin d[i]:
|
if s.id notin d[i]:
|
||||||
localError(conf, code[i].n.info, "usage of uninitialized variable: " & s.name.s)
|
localError(conf, code[i].n.info, "usage of uninitialized variable: " & s.name.s)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue