From d1009d0cfb4e367823e8d471667c39240cc1834b Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Sat, 17 Oct 2020 01:09:57 +0900
Subject: [PATCH] more memo:

- add a link to the paper
- explain the difference from the example in the paper
- better display of `IsDefined`
---
 dataflow.jl | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/dataflow.jl b/dataflow.jl
index ae72569..ac680a5 100644
--- a/dataflow.jl
+++ b/dataflow.jl
@@ -84,8 +84,7 @@ show(io::IO, ::BotElement) = print(io, "⊥")
 
 # Part 3: dataflow analysis
 
-# Note: the paper uses U+1D56E MATHEMATICAL BOLD FRAKTUR CAPITAL C for this
-typealias AbstractValue Dict{Symbol,LatticeElement}
+# Note: the paper (https://api.semanticscholar.org/CorpusID:28519618) uses U+1D56E MATHEMATICAL BOLD FRAKTUR CAPITAL C for this
 const AbstractValue = Dict{Symbol,LatticeElement}
 
 # Here we extend lattices of values to lattices of mappings of variables
@@ -98,6 +97,10 @@ const AbstractValue = Dict{Symbol,LatticeElement}
 <=(X::AbstractValue, Y::AbstractValue) = X⊓Y == X
 <(X::AbstractValue, Y::AbstractValue)  = X<=Y && X!=Y
 
+# Note: we solve an existential data-flow problem below, so:
+# - initialize states with `⊥` instead of `⊤`
+# - use `!<=` instead of `!<=` to check whether or not the instruction makes a change
+# - use `⊔` instead of `⊓` to update states
 function max_fixed_point(P::Program, a₁::AbstractValue, eval) where {Program<:AbstractVector{Stmt}}
     n = length(P)
     bot = AbstractValue( v => ⊥ for v in keys(a₁) )
@@ -146,6 +149,7 @@ end
 struct IsDefined <: LatticeElement
     is::Bool
 end
+show(io::IO, isdef::IsDefined) = print(io, isdef.is ? "defined" : "undefined")
 
 const undef = IsDefined(false)
 const def   = IsDefined(true)