@@ -97,15 +97,15 @@ const AbstractValue = Dict{Symbol,LatticeElement}
9797<= (X:: AbstractValue , Y:: AbstractValue ) = X⊓ Y == X
9898< (X:: AbstractValue , Y:: AbstractValue ) = X<= Y && X!= Y
9999
100- # Note: we solve an existential data-flow problem below, so:
100+ # Note: if we solve a " existential" data-flow problem, we need to
101101# - initialize states with `⊥` instead of `⊤`
102102# - use `!<=` instead of `!<=` to check whether or not the instruction makes a change
103103# - use `⊔` instead of `⊓` to update states
104- function max_fixed_point (P:: Program , a₁:: AbstractValue , eval) where {Program<: AbstractVector{Stmt} }
104+ function max_fixed_point (P:: Program , a₁:: AbstractValue , eval; existential :: Bool = false ) where {Program<: AbstractVector{Stmt} }
105105 n = length (P)
106- bot = AbstractValue ( v => ⊥ for v in keys (a₁) )
107- s = [ a₁; [ bot for i = 2 : n ] ]
108- W = BitSet (1 )
106+ init = AbstractValue ( v => (existential ? ⊥ : ⊤) for v in keys (a₁) )
107+ s = [ a₁; [ init for i = 2 : n ] ]
108+ W = BitSet (1 : n )
109109
110110 while ! isempty (W)
111111 pc = first (W)
@@ -118,20 +118,21 @@ function max_fixed_point(P::Program, a₁::AbstractValue, eval) where {Program<:
118118 new = copy (new)
119119 new[I. lhs. name] = eval (I. rhs, new)
120120 end
121+
121122 if isa (I, Goto)
122123 pc´ = I. label
123124 else
124125 pc´ = pc+ 1
125126 if isa (I, GotoIf)
126127 l = I. label
127- if ! (new <= s[l])
128+ if (existential ? ! (new <= s[l]) : ! (new >= s[l]) )
128129 push! (W, l)
129- s[l] = s[l] ⊔ new
130+ s[l] = (existential ? s[l] ⊔ new : s[l] ⊓ new)
130131 end
131132 end
132133 end
133- if pc´<= n && ! (new <= s[pc´])
134- s[pc´] = s[pc´] ⊔ new
134+ if pc´<= n && (existential ? ! (new <= s[pc´]) : ! (new >= s[pc´]) )
135+ s[pc´] = (existential ? s[pc´] ⊔ new : s[pc´] ⊓ new)
135136 pc = pc´
136137 else
137138 pc = n+ 1
@@ -141,8 +142,7 @@ function max_fixed_point(P::Program, a₁::AbstractValue, eval) where {Program<:
141142 s
142143end
143144
144-
145- # example problem - find uses of undefined variables
145+ # example problem 1. - find uses of undefined variables
146146
147147# flat lattice of variable definedness
148148
@@ -176,3 +176,47 @@ prog1 = [Assign(:x, 0), # 1
176176l = AbstractValue (:x => undef, :y => undef, :z => undef)
177177
178178max_fixed_point (prog1, l, abstract_eval)
179+
180+
181+ # example problem 2. - constant folding propagation (the paper example)
182+
183+ struct Const <: LatticeElement
184+ val:: Int
185+ end
186+
187+ abstract_eval (x:: Num , s:: AbstractValue ) = Const (x. val)
188+
189+ abstract_eval (x:: Sym , s:: AbstractValue ) = get (s, x. name, ⊥)
190+
191+ function abstract_eval (x:: Call , s:: AbstractValue )
192+ if any (a-> (abstract_eval (a,s) == ⊤), x. args)
193+ return ⊤
194+ end
195+ if any (a-> (abstract_eval (a,s) == ⊥), x. args)
196+ return ⊥
197+ end
198+
199+ to_val (x:: Num ) = x. val
200+ to_val (x:: Const ) = x. val
201+ to_val (x:: Sym ) = to_val (abstract_eval (x, s))
202+
203+ f = getfield (@__MODULE__ , x. head. name)
204+ args = to_val .(x. args)
205+ return Const (f (args... ))
206+ end
207+
208+ prog1 = [Assign (:x , 1 ), # 1
209+ Assign (:y , 2 ), # 2
210+ Assign (:z , 3 ), # 3
211+ Goto (9 ), # 4
212+ Assign (:r , Call (:(+ ), [:y , :z ])), # 5
213+ GotoIf (8 , Call (:(≤ ), [:x , :z ])), # 6
214+ Assign (:r , Call (:(+ ), [:z , :y ])), # 7
215+ Assign (:x , Call (:(+ ), [:x , 1 ])), # 8
216+ GotoIf (5 , Call (:(< ), [:x , 10 ])), # 9
217+ Ret ()]
218+
219+ # variables initially undefined
220+ a₁ = AbstractValue (:x => ⊤, :y => ⊤, :z => ⊤, :r => ⊤)
221+
222+ max_fixed_point (prog1, a₁, abstract_eval) # The solution contains the `:r => Const(5)`, which is not found in the program
0 commit comments