Data flow analysis establishes facts at program points, such as where a particular assignment may reach, whether a value is used later, or whether an expression has been computed on all paths. It compresses execution paths into computable abstract information and propagates it across the Control Flow Graph (CFG).
Results should be conservative relative to their use: proofs for code elimination cannot miss potential behaviors, while analyses reporting possible errors can tolerate some false positives. Conservative does not mean arbitrary guessing; it means explicitly defining the inclusion relationship between abstract results and actual execution.
Understanding may and must from branch merging
If asked which definition x may come from, merge the candidates from both paths; if asked whether expression a+b is must-computed, both paths must provide that fact. For classic set-based analysis, the former typically uses union, and the latter uses intersection.
However, may/must does not require all abstract domains to simply use set union and intersection. Lattice partial orders, top/bottom elements, and join/meet operators also vary by convention; define meanings first, then write formulas.
A unified framework requires five definitions
Item
What must be specified
Abstract domain
What facts are stored at a program point
Propagation direction
From predecessors forward, or successors backward
Merge operator
How information from multiple paths is combined
Transfer function
How a basic block transforms information
Boundary and initial values
How entry, exit, and other nodes start
Gen/Kill is a convenient form for many bit-vector analyses, not the unique form for all transfer functions. Even must analysis using intersection merge does not mean changing gen ∪ ... inside the transfer function to intersection.
Reaching Definitions: Forward may Analysis
Definition d reaches point p if there exists a path from d to p with no redefinition of the same variable in between. Assign independent IDs to each assignment rather than just recording variable names.
IN[B] = ∪ OUT[P], where P iterates over predecessors of B.
OUT[B] = GEN[B] ∪ (IN[B] − KILL[B]).
GEN contains definitions that survive to the block's exit; KILL contains other definitions of the same variable overwritten by assignments in this block. If a block sequentially executes d1: x=1; d2: x=2, d1 is not in the exit GEN, but d2 is.
Entry usually models definitions of parameters or external initial values; if the teaching model starts with an empty set, it should state that these are outside the analysis scope. In SSA, scalar uses directly associate with a unique static definition, but aliasing writes to memory still require separate analysis.
Live Variables: Backward may Analysis
A value is live at point p if there exists a subsequent path that uses the value before redefining it. Since the question looks to the future, propagation is backward from successors.
OUT[B] = ∪ IN[S], where S iterates over successors of B.
IN[B] = USE[B] ∪ (OUT[B] − DEF[B]).
USE is the set of variables used in the block before their first definition; DEF is the set of variables defined in the block, not requiring that the definition was never used before.
For example, in block x=x+1; y=x; return y, USE={x}, DEF={x,y}. When exit OUT=∅, entry IN={x}. It is perfectly reasonable for x to exist in both USE and DEF: the old x entering the block is needed for the first instruction, and a new x is produced within the block.
Loops cause live information to propagate across back edges. The live range of a value is the set of program points on relevant CFG paths, not simply connecting the definition line to the last use line in source code.
Available Expressions: Forward must Analysis
Expression e is available at p if every relevant path entering p has computed e, and its operands have not been modified since. In a pure scalar model:
IN[B] = ∩ OUT[P].
OUT[B] = GEN[B] ∪ (IN[B] − KILL[B]).
Note that x=x+y does not make x+y available at the exit based on the new x: the right-hand side calculation uses the old x, while the assignment changes x. When constructing GEN, consider subsequent assignments in the block and the definition of the statement itself.
Entry is usually empty; other reachable blocks can start from the universal set of expressions and shrink downwards. Unreachable blocks and nodes with no predecessors need explicit handling; do not arbitrarily take the intersection of empty sets and propagate false facts.
Worklist: Only recompute affected neighbors
Using forward analysis as an example, initialize boundaries and block states, enqueue blocks to be processed; pop B, re-merge predecessor outputs and apply the transfer function; if OUT changes, enqueue successors. For backward analysis, notify predecessors when IN changes.
On a lattice of finite height, monotonic iteration with correct initial values terminates. Merely having a maximum element does not imply finite height; interval domains of infinite height may require widening. The number of rounds is influenced by the CFG, loops, and domain, with no fixed guarantee of three to five rounds. Clang Data Flow Analysis Introduction
Reaching Definitions in Loops: First Pass at Header Has No Complete Answers
Analyze only two definitions of variable x: entry E executes d0: x=0, loop body B executes d1: x=x+1. Loop header H can enter B or go to exit X; B then returns to H. Conditions and other variables are not in the definition set of this model.
On the first pass from E to H, only d0 is known. Scanning B reveals d1; sending it along the back edge to H allows H to know that x may also come from d1 of the previous iteration. Here, d1 is the identity of a static assignment statement, not generating infinite definition IDs for each dynamic loop execution.
Below is the worklist implementation. State uses the inclusion order of definition sets, starting all blocks from an empty set; entry has no predecessors, so d0 is generated by GEN. All nodes are reachable, so unreachable inputs are not handled separately here.
fromcollectionsimportdequesucc={"E":["H"],"H":["B","X"],"B":["H"],"X":[]}pred={b:[pforpinsuccifbinsucc[p]]forbinsucc}gen={"E":{"d0"},"H":set(),"B":{"d1"},"X":set()}kill={"E":{"d1"},"H":set(),"B":{"d0"},"X":set()}defsolve(order):out={b:set()forbinsucc}work=deque(order)queued=set(order)history=[]whilework:b=work.popleft()queued.remove(b)incoming=set().union(*(out[p]forpinpred[b]))new=gen[b]|(incoming-kill[b])ifnew!=out[b]:out[b]=newhistory.append((b,tuple(sorted(new))))fornxtinsucc[b]:ifnxtnotinqueued:work.append(nxt)queued.add(nxt)returnout, historyexpected={"E":{"d0"},"H":{"d0","d1"},"B":{"d1"},"X":{"d0","d1"}}out, history=solve(["E","H","B","X"])assertout==expectedassert[vforb,vinhistoryifb=="H"]==[("d0",),("d0","d1")]assertsolve(["X","B","H","E"])[0]==expected# Check not only against expected but also that each block satisfies the original equation.
forbinsucc:incoming=set().union(*(out[p]forpinpred[b]))assertout[b]==gen[b]|(incoming-kill[b])
Node
Final IN
Final OUT
Explanation
E
∅
{d0}
Establish initial value
H
{d0,d1}
{d0,d1}
Initial entry and back-edge merge
B
{d0,d1}
{d1}
Current assignment overwrites previous x
X
{d0,d1}
{d0,d1}
Loop may execute zero or more times
Worklist order changes the intermediate process, but with the same finite, monotonic framework and boundary conditions, the final solution is identical. If traversing the CFG only once, H might never see the back edge; stopping if any node doesn't change might also miss new information from other nodes in the queue.
When do facts on back edges propagate back to the exit?
The buttons below are not prescribed course steps, but real analysis tasks in the pending set. You can process the exit first, letting it temporarily receive an empty set; when entry or back edges subsequently produce new facts, the exit will re-queue via successors. One invariance only indicates that this specific calculation added no new information; the global stop condition is an empty queue. d1 in the model remains a static assignment identity.
When do facts on back edges propagate back to the exit?
Processing a block with no change does not mean global termination. Only when all pending blocks are done has d1 from the back edge propagated to H and X; different processing orders yield the same final solution.
{"id":"reaching-definitions-worklist","title":"When do facts on back edges propagate back to the exit?","summary":"Processing a block with no change does not mean global termination. Only when all pending blocks are done has d1 from the back edge propagated to H and X; different processing orders yield the same final solution.","height":1000,"html":"<h2 data-i18n=\"heading\"></h2><p class=\"intro\" data-i18n=\"intro\"></p><label class=\"check\"><input type=\"checkbox\" id=\"loop\" checked><span data-i18n=\"loop\"></span></label><div class=\"actions\"><button id=\"E\" data-i18n=\"E\"></button><button id=\"H\" data-i18n=\"H\"></button><button id=\"B\" data-i18n=\"B\"></button><button id=\"X\" data-i18n=\"X\"></button><button id=\"solve\" data-i18n=\"solve\"></button><button id=\"reset\" data-i18n=\"reset\"></button></div><svg id=\"cfg\" class=\"diagram\" viewBox=\"0 0 360 180\" role=\"img\"></svg><div id=\"facts\" class=\"table\"></div><div class=\"metrics\"><div><span data-i18n=\"pending\"></span><strong id=\"pending\"></strong></div></div><p id=\"formula\" class=\"log\"></p><p class=\"hint\" data-i18n=\"hint\"></p><details class=\"scope\"><summary data-i18n=\"scopeLabel\"></summary><p data-i18n=\"scope\"></p></details>","css":".intro{margin:8px 0 18px;color:var(--muted);font-size:14px}.caption,.hint{font-size:12px;color:var(--muted);margin-top:12px}.control{display:grid;grid-template-columns:minmax(0,1fr) auto;gap:6px 12px;align-items:center;margin:14px 0;font-size:13px}.control label{font-size:13px}.control output{color:var(--accent);min-width:5em;text-align:right;font-variant-numeric:tabular-nums}.control input{grid-column:1/-1;width:100%;margin:0}.presets{display:flex;gap:4px;align-items:stretch}.presets button{flex:1 1 0;min-width:0;overflow-wrap:anywhere;font-size:13px}.actions{display:flex;gap:8px;flex-wrap:wrap;margin:14px 0}.actions button{flex:1;min-width:0;font-size:13px;min-height:42px}.copy{display:grid;font-size:14px;margin:16px 0}.copy>*{grid-area:1/1;margin:0}.reserve{visibility:hidden}.scope{margin-top:14px;color:var(--muted);font-size:12px}.scope summary{padding:8px 0;cursor:pointer}.scope p{margin-top:10px}.two{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:12px;margin:16px 0}.card{border:1px solid var(--rule);border-radius:9px;padding:14px;min-width:0}.card header{font-size:14px;font-weight:600;margin-bottom:10px}.card button{font-size:12px;width:100%;min-width:0}.card small{display:block;font-size:12px;color:var(--muted)}.card code{font-size:12px;overflow-wrap:anywhere}.metrics{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:12px;margin:16px 0}.metrics>div{border-left:2px solid var(--accent);padding-left:10px;min-width:0}.metrics span{display:block;min-height:3.2em;color:var(--muted);font-size:12px}.metrics strong{font-size:23px;display:block;font-weight:500;overflow-wrap:anywhere;font-variant-numeric:tabular-nums}.formula{border-top:1px solid var(--rule);padding-top:12px;margin-top:14px;font-size:13px;font-variant-numeric:tabular-nums;overflow-wrap:anywhere}.value{font:500 20px var(--viz-font-ui)}.legend{display:flex;flex-wrap:wrap;gap:6px 14px;font-size:12px;color:var(--muted);margin:12px 0}.legend span:before{content:'';display:inline-block;width:8px;height:8px;border-radius:2px;background:var(--accent);margin-right:6px}.legend .second:before{background:var(--second)}.check{display:flex;align-items:center;gap:8px;font-size:13px;margin:12px 0}.check input{width:16px;height:16px;flex-shrink:0;accent-color:var(--accent)}select,input[type=text],input[type=number]{background:var(--paper);color:var(--ink);font:inherit;font-size:13px;padding:10px;border:1px solid var(--rule);border-radius:7px;max-width:100%;min-width:0}select{width:100%;min-height:42px}.band{height:20px;display:flex;background:var(--surface);border-radius:4px;overflow:hidden}.band i{height:100%;display:block;background:var(--accent);transition:width .25s}.band i.second{background:var(--second)}button:disabled{cursor:default}.status{font-size:13px;min-height:4.8em}.mono{font-family:var(--viz-font-mono);font-variant-numeric:tabular-nums}.muted{color:var(--muted)}\n@media(max-width:480px){.two{gap:8px}.card{padding:12px 9px}.actions button,.presets button{font-size:12px}.metrics strong{font-size:20px}.metrics{gap:8px}}\n@media(prefers-reduced-motion:reduce){*,*::before,*::after{transition:none!important;animation:none!important}}\n.track-row{margin:16px 0}.track-row>span{display:block;font-size:12px;color:var(--muted);margin-bottom:7px}.track{display:flex;gap:5px;min-width:0}.cell{flex:1;min-width:0;min-height:48px;border:1px solid var(--rule);border-radius:5px;background:var(--surface);display:flex;align-items:center;justify-content:center;text-align:center;padding:5px 3px;font-size:12px;overflow-wrap:anywhere;font-variant-numeric:tabular-nums}.cell.on{background:var(--accent-soft);border-color:var(--accent)}.cell.gold{background:var(--second-soft);border-color:var(--second)}.cell.empty{border-style:dashed;color:var(--muted)}.cell.error{border-color:var(--second);text-decoration:line-through}.choices{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:6px;margin:14px 0}.choices button{min-width:0;padding:10px 4px;font-size:12px;overflow-wrap:anywhere}.choices button[aria-current=true]{border-color:var(--accent);background:var(--accent-soft)}.relation{display:grid;grid-template-columns:minmax(0,1fr) 28px minmax(0,1fr);align-items:center;gap:6px;margin:12px 0}.relation .cell{min-height:72px}.relation>i{text-align:center;font-style:normal;color:var(--accent)}.readout{font-size:13px;white-space:pre-line;min-height:6.4em;overflow-wrap:anywhere}.plot{position:relative;border-left:1px solid var(--rule);border-bottom:1px solid var(--rule);padding:8px 0;margin:18px 0}.plot-row{height:28px;position:relative;margin:4px 0;background:var(--surface)}.plot-row i{position:absolute;inset-block:5px;background:var(--accent);min-width:2px;transition:width .2s,left .2s}.plot-row b{position:relative;padding:4px 6px;font:11px/28px var(--viz-font-ui);background:var(--paper);border-radius:3px}.axis{display:flex;justify-content:space-between;font-size:11px;color:var(--muted)}\n\n/* Action labels must remain readable across locales and narrow embeds. */\n.actions{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:8px}\n.actions button{overflow-wrap:anywhere;white-space:normal;min-height:58px;padding:8px}\nbutton{overflow-wrap:anywhere}\n@media(min-width:640px){.actions{grid-template-columns:repeat(3,minmax(0,1fr))}}\n\n.metrics span{overflow-wrap:anywhere}\n.panel{border:1px solid var(--rule);border-radius:9px;padding:12px;margin:14px 0;min-width:0}.panel h3{font-size:13px;margin:0 0 10px;color:var(--muted)}.source{font:13px/1.8 var(--viz-font-mono);white-space:pre-wrap;overflow-wrap:anywhere;margin:12px 0}.source mark{background:var(--accent-soft);color:var(--ink);border-bottom:2px solid var(--accent)}.source .fault{background:var(--second-soft);border-color:var(--second)}.diagram{display:block;width:100%;height:auto;max-height:320px;margin:14px 0;overflow:visible}.diagram text{fill:var(--ink);font:12px var(--viz-font-ui)}.diagram .edge{stroke:var(--muted);stroke-width:1.5;fill:none}.diagram .edge.on{stroke:var(--accent);stroke-width:3}.diagram .node{fill:var(--surface);stroke:var(--rule);stroke-width:1.5}.diagram .node.on{fill:var(--accent-soft);stroke:var(--accent)}.diagram .node.gold{fill:var(--second-soft);stroke:var(--second)}.log{font:12px/1.8 var(--viz-font-mono);white-space:pre-line;overflow-wrap:anywhere;min-height:7.2em}.table{display:grid;gap:5px;margin:14px 0}.table .tr{display:grid;grid-template-columns:repeat(3,minmax(0,1fr));gap:5px}.table .tr>*{padding:8px 5px;background:var(--surface);border-radius:4px;min-width:0;overflow-wrap:anywhere;font-size:12px}.table .tr .on{background:var(--accent-soft)}.table .tr .gold{background:var(--second-soft)}.choices button{min-height:44px}.metrics strong{min-height:1.6em}.code-line{display:block}.code-line.on{background:var(--accent-soft);border-left:2px solid var(--accent);padding-left:6px}.status-badge{font-size:12px;color:var(--accent)}.tile-grid{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:6px}.tile-grid .cell{min-height:40px}.actions button{min-height:48px}.form-field{display:grid;gap:8px;margin:14px 0;font-size:13px}.form-field input{width:100%;font-family:var(--viz-font-ui)}.metrics.three{grid-template-columns:repeat(3,minmax(0,1fr))}.formula{min-height:3.2em}.presets{flex-wrap:wrap}.presets button{flex-basis:25%;min-height:44px}\n\n#facts .tr{grid-template-columns:40px 1fr 1fr}.metrics strong{font-size:18px}#formula{min-height:5.4em}","js":"const $=s=>document.querySelector(s);const set=(id,v)=>$('#'+id).textContent=v;const t=k=>viz.t(k);function cells(id,values){$('#'+id).replaceChildren(...values.map(v=>{const e=document.createElement('div');e.className='cell '+(v.cls||'');e.textContent=v.text;e.title=v.title||v.text;return e;}));}function pressed(mode){document.querySelectorAll('[data-mode]').forEach(e=>e.setAttribute('aria-pressed',String(e.dataset.mode===mode)));}const esc=s=>String(s).replace(/[&<>\"']/g,c=>({'&':'&','<':'<','>':'>','\"':'"',\"'\":'''}[c]));const fmt=s=>'{'+[...s].sort().join(', ')+'}';function graph(id,nodes,edges){const el=$('#'+id);el.setAttribute('viewBox','0 0 360 200');el.innerHTML='<defs><marker id=\"arrow-'+id+'\" viewBox=\"0 0 10 10\" refX=\"8\" refY=\"5\" markerWidth=\"5\" markerHeight=\"5\" orient=\"auto-start-reverse\"><path d=\"M 0 0 L 10 5 L 0 10 z\" fill=\"var(--muted)\"/></marker></defs>'+edges.map(e=>{const a=nodes[e[0]],b=nodes[e[1]],dx=b.x-a.x,dy=b.y-a.y,d=Math.hypot(dx,dy)||1;if(edges.some(r=>r[0]===e[1]&&r[1]===e[0])){const nx=-dy/d,ny=dx/d;return '<path class=\"edge '+(e[2]?'on':'')+'\" d=\"M '+(a.x+dx/d*22+nx*12)+' '+(a.y+dy/d*22+ny*12)+' Q '+((a.x+b.x)/2+nx*38)+' '+((a.y+b.y)/2+ny*38)+' '+(b.x-dx/d*25+nx*12)+' '+(b.y-dy/d*25+ny*12)+'\" marker-end=\"url(#arrow-'+id+')\"/>';}return '<line class=\"edge '+(e[2]?'on':'')+'\" x1=\"'+(a.x+dx/d*25)+'\" y1=\"'+(a.y+dy/d*25)+'\" x2=\"'+(b.x-dx/d*28)+'\" y2=\"'+(b.y-dy/d*28)+'\" marker-end=\"url(#arrow-'+id+')\"/>';}).join('')+nodes.map(n=>'<g><circle class=\"node '+(n.cls||'')+'\" cx=\"'+n.x+'\" cy=\"'+n.y+'\" r=\"25\"/><text x=\"'+n.x+'\" y=\"'+(n.y+4)+'\" text-anchor=\"middle\">'+esc(n.name)+'</text>'+(n.sub?'<text x=\"'+n.x+'\" y=\"'+(n.y+43)+'\" text-anchor=\"middle\">'+esc(n.sub)+'</text>':'')+'</g>').join('');}function table(id,rows){$('#'+id).replaceChildren(...rows.map(r=>{const row=document.createElement('div');row.className='tr';r.forEach(x=>{const c=document.createElement('div');if(typeof x==='object'){c.textContent=x.text;c.className=x.cls||'';}else c.textContent=x;row.append(c)});return row;}));}const names=['E','H','B','X'];let out,ins,pending,last='',formula='';function edges(){return [[0,1],[1,2],[1,3],...($('#loop').checked?[[2,1]]:[])]}function reset(){out=[0,0,0,0];ins=[0,0,0,0];pending=new Set([0,1,2,3]);last='';formula='∅';draw()}function f(mask){return fmt(['d0','d1'].filter((_,i)=>mask&(1<<i)))}function process(i){if(!pending.has(i))return;pending.delete(i);const input=edges().filter(e=>e[1]===i).reduce((a,[p])=>a|out[p],0),gen=i===0?1:i===2?2:0,kill=i===0?2:i===2?1:0,result=gen|(input&~kill),changed=out[i]!==result;ins[i]=input;out[i]=result;if(changed)edges().filter(e=>e[0]===i).forEach(e=>pending.add(e[1]));last=names[i];formula='IN['+last+'] = '+f(input)+'\\nOUT = '+f(gen)+' ∪ ('+f(input)+' − '+f(kill)+') = '+f(result);draw()}function draw(){const pos=[[45,80],[165,80],[290,35],[290,155]];graph('cfg',names.map((name,i)=>({name,x:pos[i][0],y:pos[i][1],cls:pending.has(i)?'gold':out[i]?'on':''})),edges());table('facts',[['block','IN','OUT'],...names.map((n,i)=>[n,f(ins[i]),f(out[i])])]);names.forEach((n,i)=>$('#'+n).disabled=!pending.has(i));$('#solve').disabled=pending.size===0;set('pending',fmt([...pending].map(i=>names[i])));set('formula',formula);$('#facts').dataset.out=out.join(',');$('#pending').dataset.count=pending.size;}names.forEach((n,i)=>$('#'+n).onclick=()=>process(i));$('#solve').onclick=()=>{let guard=0;while(pending.size&&guard++<100)process(pending.values().next().value);if(pending.size)throw Error('nonconvergence')};$('#reset').onclick=reset;$('#loop').onchange=reset;reset();","audio":false,"strings":{"B":"B","E":"E","H":"H","X":"X","formula":"Current transfer function","heading":"When do facts on back edges propagate back to the exit?","hint":"Buttons only process the corresponding block; successors are re-added to the pending set only when OUT changes.","intro":"Arbitrarily select pending blocks, or solve directly to a fixed point. Blue shows definition facts, gold marks blocks needing recomputation.","loop":"Keep B → H back edge","pending":"Pending blocks","reset":"Reset","scope":"Forward may reaching definitions, set domain {d0,d1}, starting from empty set. E defines d0, B defines d1; fix all reachable CFG, conditions and other variables are not in the model.","scopeLabel":"Model Scope and Conventions","solve":"Solve to fixed point"}}
Fixed Points and Path-by-Path Solving: Where Precision is Lost
MOP transforms along each CFG path first, then merges; iterative equations merge paths midway and continue transforming. Under conditions where transfer functions are distributive over merge, they are consistent; otherwise, premature merging may lose correlated information.
For example, two paths yield (x=1,y=2) and (x=2,y=1) respectively, followed by calculating z=x+y. Path-by-path calculation both yield 3; non-relational constant propagation merging first marks x and y as non-constant, potentially failing to derive z=3. Abstract domains preserving variable relationships can improve precision at higher cost.
MOP also typically traverses syntactic paths in the CFG, which may include paths where conditions cannot be simultaneously satisfied, so it cannot be directly called a perfect solution for actual program semantics. The magnitude direction of MFP vs MOP depends on the lattice order used; do not state an inequality without specifying the lattice-order convention.
After losing correlation, do not treat all combinations as real paths
Writing the previous two paths directly as sets, the precise path state is {(1,2),(2,1)}; after separately retaining possible values for x and y, both become {1,2}. Subsequently taking the Cartesian product introduces extra (1,1) and (2,2), yielding sums 2 and 4 that do not actually exist.
The non-relational result still contains the real result, so it is conservative to say "z may belong to {2,3,4}", but one cannot prove z is always 3. This precision loss comes from the abstract state not saving pairing relationships; adding more worklist rounds cannot recover discarded information. To improve, change the abstract domain, delay merging, or utilize path conditions, rather than just repeatedly running the same equation.
What is lost by remembering x and y separately?
Drawing specific paths as points in a 2D coordinate system accurately locates "correlation loss". Projecting separately onto x and y axes and then combining, the two real points may expand to four; the extra points are not newly discovered execution paths, but additional states allowed by the abstraction. Modifying the second path allows observing when extra combinations do not occur. Repeating the same iteration cannot recover lost pairing relationships.
R⊆πx(R)×πy(R)
Preparing the visual
What is lost by remembering x and y separately?
Independent sets only remember what x appeared and what y appeared, not how they paired. The gold grid represents states additionally allowed by abstraction, potentially making a previously constant x+y unprovable.
{"id":"lost-path-correlation","title":"What is lost by remembering x and y separately?","summary":"Independent sets only remember what x appeared and what y appeared, not how they paired. The gold grid represents states additionally allowed by abstraction, potentially making a previously constant x+y unprovable.","height":1000,"html":"<h2 data-i18n=\"heading\"></h2><p class=\"intro\" data-i18n=\"intro\"></p><div class=\"control\"><label for=\"x\" data-i18n=\"x\"></label><output for=\"x\" id=\"x-value\"></output><input id=\"x\" type=\"range\" min=\"0\" max=\"3\" value=\"2\" step=\"1\"></div><div class=\"control\"><label for=\"y\" data-i18n=\"y\"></label><output for=\"y\" id=\"y-value\"></output><input id=\"y\" type=\"range\" min=\"0\" max=\"3\" value=\"1\" step=\"1\"></div><div id=\"pairs\" class=\"tile-grid\"></div><div class=\"metrics\"><div><span data-i18n=\"exact\"></span><strong id=\"exact\"></strong></div><div><span data-i18n=\"abstract\"></span><strong id=\"abstract\"></strong></div></div><p id=\"equation\" class=\"formula\"></p><p class=\"hint\" data-i18n=\"hint\"></p><details class=\"scope\"><summary data-i18n=\"scopeLabel\"></summary><p data-i18n=\"scope\"></p></details>","css":".intro{margin:8px 0 18px;color:var(--muted);font-size:14px}.caption,.hint{font-size:12px;color:var(--muted);margin-top:12px}.control{display:grid;grid-template-columns:minmax(0,1fr) auto;gap:6px 12px;align-items:center;margin:14px 0;font-size:13px}.control label{font-size:13px}.control output{color:var(--accent);min-width:5em;text-align:right;font-variant-numeric:tabular-nums}.control input{grid-column:1/-1;width:100%;margin:0}.presets{display:flex;gap:4px;align-items:stretch}.presets button{flex:1 1 0;min-width:0;overflow-wrap:anywhere;font-size:13px}.actions{display:flex;gap:8px;flex-wrap:wrap;margin:14px 0}.actions button{flex:1;min-width:0;font-size:13px;min-height:42px}.copy{display:grid;font-size:14px;margin:16px 0}.copy>*{grid-area:1/1;margin:0}.reserve{visibility:hidden}.scope{margin-top:14px;color:var(--muted);font-size:12px}.scope summary{padding:8px 0;cursor:pointer}.scope p{margin-top:10px}.two{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:12px;margin:16px 0}.card{border:1px solid var(--rule);border-radius:9px;padding:14px;min-width:0}.card header{font-size:14px;font-weight:600;margin-bottom:10px}.card button{font-size:12px;width:100%;min-width:0}.card small{display:block;font-size:12px;color:var(--muted)}.card code{font-size:12px;overflow-wrap:anywhere}.metrics{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:12px;margin:16px 0}.metrics>div{border-left:2px solid var(--accent);padding-left:10px;min-width:0}.metrics span{display:block;min-height:3.2em;color:var(--muted);font-size:12px}.metrics strong{font-size:23px;display:block;font-weight:500;overflow-wrap:anywhere;font-variant-numeric:tabular-nums}.formula{border-top:1px solid var(--rule);padding-top:12px;margin-top:14px;font-size:13px;font-variant-numeric:tabular-nums;overflow-wrap:anywhere}.value{font:500 20px var(--viz-font-ui)}.legend{display:flex;flex-wrap:wrap;gap:6px 14px;font-size:12px;color:var(--muted);margin:12px 0}.legend span:before{content:'';display:inline-block;width:8px;height:8px;border-radius:2px;background:var(--accent);margin-right:6px}.legend .second:before{background:var(--second)}.check{display:flex;align-items:center;gap:8px;font-size:13px;margin:12px 0}.check input{width:16px;height:16px;flex-shrink:0;accent-color:var(--accent)}select,input[type=text],input[type=number]{background:var(--paper);color:var(--ink);font:inherit;font-size:13px;padding:10px;border:1px solid var(--rule);border-radius:7px;max-width:100%;min-width:0}select{width:100%;min-height:42px}.band{height:20px;display:flex;background:var(--surface);border-radius:4px;overflow:hidden}.band i{height:100%;display:block;background:var(--accent);transition:width .25s}.band i.second{background:var(--second)}button:disabled{cursor:default}.status{font-size:13px;min-height:4.8em}.mono{font-family:var(--viz-font-mono);font-variant-numeric:tabular-nums}.muted{color:var(--muted)}\n@media(max-width:480px){.two{gap:8px}.card{padding:12px 9px}.actions button,.presets button{font-size:12px}.metrics strong{font-size:20px}.metrics{gap:8px}}\n@media(prefers-reduced-motion:reduce){*,*::before,*::after{transition:none!important;animation:none!important}}\n.track-row{margin:16px 0}.track-row>span{display:block;font-size:12px;color:var(--muted);margin-bottom:7px}.track{display:flex;gap:5px;min-width:0}.cell{flex:1;min-width:0;min-height:48px;border:1px solid var(--rule);border-radius:5px;background:var(--surface);display:flex;align-items:center;justify-content:center;text-align:center;padding:5px 3px;font-size:12px;overflow-wrap:anywhere;font-variant-numeric:tabular-nums}.cell.on{background:var(--accent-soft);border-color:var(--accent)}.cell.gold{background:var(--second-soft);border-color:var(--second)}.cell.empty{border-style:dashed;color:var(--muted)}.cell.error{border-color:var(--second);text-decoration:line-through}.choices{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:6px;margin:14px 0}.choices button{min-width:0;padding:10px 4px;font-size:12px;overflow-wrap:anywhere}.choices button[aria-current=true]{border-color:var(--accent);background:var(--accent-soft)}.relation{display:grid;grid-template-columns:minmax(0,1fr) 28px minmax(0,1fr);align-items:center;gap:6px;margin:12px 0}.relation .cell{min-height:72px}.relation>i{text-align:center;font-style:normal;color:var(--accent)}.readout{font-size:13px;white-space:pre-line;min-height:6.4em;overflow-wrap:anywhere}.plot{position:relative;border-left:1px solid var(--rule);border-bottom:1px solid var(--rule);padding:8px 0;margin:18px 0}.plot-row{height:28px;position:relative;margin:4px 0;background:var(--surface)}.plot-row i{position:absolute;inset-block:5px;background:var(--accent);min-width:2px;transition:width .2s,left .2s}.plot-row b{position:relative;padding:4px 6px;font:11px/28px var(--viz-font-ui);background:var(--paper);border-radius:3px}.axis{display:flex;justify-content:space-between;font-size:11px;color:var(--muted)}\n\n/* Action labels must remain readable across locales and narrow embeds. */\n.actions{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:8px}\n.actions button{overflow-wrap:anywhere;white-space:normal;min-height:58px;padding:8px}\nbutton{overflow-wrap:anywhere}\n@media(min-width:640px){.actions{grid-template-columns:repeat(3,minmax(0,1fr))}}\n\n.metrics span{overflow-wrap:anywhere}\n.panel{border:1px solid var(--rule);border-radius:9px;padding:12px;margin:14px 0;min-width:0}.panel h3{font-size:13px;margin:0 0 10px;color:var(--muted)}.source{font:13px/1.8 var(--viz-font-mono);white-space:pre-wrap;overflow-wrap:anywhere;margin:12px 0}.source mark{background:var(--accent-soft);color:var(--ink);border-bottom:2px solid var(--accent)}.source .fault{background:var(--second-soft);border-color:var(--second)}.diagram{display:block;width:100%;height:auto;max-height:320px;margin:14px 0;overflow:visible}.diagram text{fill:var(--ink);font:12px var(--viz-font-ui)}.diagram .edge{stroke:var(--muted);stroke-width:1.5;fill:none}.diagram .edge.on{stroke:var(--accent);stroke-width:3}.diagram .node{fill:var(--surface);stroke:var(--rule);stroke-width:1.5}.diagram .node.on{fill:var(--accent-soft);stroke:var(--accent)}.diagram .node.gold{fill:var(--second-soft);stroke:var(--second)}.log{font:12px/1.8 var(--viz-font-mono);white-space:pre-line;overflow-wrap:anywhere;min-height:7.2em}.table{display:grid;gap:5px;margin:14px 0}.table .tr{display:grid;grid-template-columns:repeat(3,minmax(0,1fr));gap:5px}.table .tr>*{padding:8px 5px;background:var(--surface);border-radius:4px;min-width:0;overflow-wrap:anywhere;font-size:12px}.table .tr .on{background:var(--accent-soft)}.table .tr .gold{background:var(--second-soft)}.choices button{min-height:44px}.metrics strong{min-height:1.6em}.code-line{display:block}.code-line.on{background:var(--accent-soft);border-left:2px solid var(--accent);padding-left:6px}.status-badge{font-size:12px;color:var(--accent)}.tile-grid{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:6px}.tile-grid .cell{min-height:40px}.actions button{min-height:48px}.form-field{display:grid;gap:8px;margin:14px 0;font-size:13px}.form-field input{width:100%;font-family:var(--viz-font-ui)}.metrics.three{grid-template-columns:repeat(3,minmax(0,1fr))}.formula{min-height:3.2em}.presets{flex-wrap:wrap}.presets button{flex-basis:25%;min-height:44px}\n\n.metrics strong{font-size:18px}","js":"const $=s=>document.querySelector(s);const set=(id,v)=>$('#'+id).textContent=v;const t=k=>viz.t(k);function cells(id,values){$('#'+id).replaceChildren(...values.map(v=>{const e=document.createElement('div');e.className='cell '+(v.cls||'');e.textContent=v.text;e.title=v.title||v.text;return e;}));}function pressed(mode){document.querySelectorAll('[data-mode]').forEach(e=>e.setAttribute('aria-pressed',String(e.dataset.mode===mode)));}const esc=s=>String(s).replace(/[&<>\"']/g,c=>({'&':'&','<':'<','>':'>','\"':'"',\"'\":'''}[c]));const fmt=s=>'{'+[...s].sort().join(', ')+'}';function graph(id,nodes,edges){const el=$('#'+id);el.setAttribute('viewBox','0 0 360 200');el.innerHTML='<defs><marker id=\"arrow-'+id+'\" viewBox=\"0 0 10 10\" refX=\"8\" refY=\"5\" markerWidth=\"5\" markerHeight=\"5\" orient=\"auto-start-reverse\"><path d=\"M 0 0 L 10 5 L 0 10 z\" fill=\"var(--muted)\"/></marker></defs>'+edges.map(e=>{const a=nodes[e[0]],b=nodes[e[1]],dx=b.x-a.x,dy=b.y-a.y,d=Math.hypot(dx,dy)||1;if(edges.some(r=>r[0]===e[1]&&r[1]===e[0])){const nx=-dy/d,ny=dx/d;return '<path class=\"edge '+(e[2]?'on':'')+'\" d=\"M '+(a.x+dx/d*22+nx*12)+' '+(a.y+dy/d*22+ny*12)+' Q '+((a.x+b.x)/2+nx*38)+' '+((a.y+b.y)/2+ny*38)+' '+(b.x-dx/d*25+nx*12)+' '+(b.y-dy/d*25+ny*12)+'\" marker-end=\"url(#arrow-'+id+')\"/>';}return '<line class=\"edge '+(e[2]?'on':'')+'\" x1=\"'+(a.x+dx/d*25)+'\" y1=\"'+(a.y+dy/d*25)+'\" x2=\"'+(b.x-dx/d*28)+'\" y2=\"'+(b.y-dy/d*28)+'\" marker-end=\"url(#arrow-'+id+')\"/>';}).join('')+nodes.map(n=>'<g><circle class=\"node '+(n.cls||'')+'\" cx=\"'+n.x+'\" cy=\"'+n.y+'\" r=\"25\"/><text x=\"'+n.x+'\" y=\"'+(n.y+4)+'\" text-anchor=\"middle\">'+esc(n.name)+'</text>'+(n.sub?'<text x=\"'+n.x+'\" y=\"'+(n.y+43)+'\" text-anchor=\"middle\">'+esc(n.sub)+'</text>':'')+'</g>').join('');}function table(id,rows){$('#'+id).replaceChildren(...rows.map(r=>{const row=document.createElement('div');row.className='tr';r.forEach(x=>{const c=document.createElement('div');if(typeof x==='object'){c.textContent=x.text;c.className=x.cls||'';}else c.textContent=x;row.append(c)});return row;}));}function draw(){const x=+$('#x').value,y=+$('#y').value,pairs=[[1,2],[x,y]],xs=new Set([1,x]),ys=new Set([2,y]),exact=new Set(pairs.map(([a,b])=>a+b)),abstract=new Set;set('x-value',x);set('y-value',y);cells('pairs',Array.from({length:16},(_,i)=>{const a=i%4,b=Math.floor(i/4),real=pairs.some(p=>p[0]===a&&p[1]===b),possible=xs.has(a)&&ys.has(b);if(possible)abstract.add(a+b);return{text:a+','+b,cls:real?'on':possible?'gold':'empty'}}));set('exact',fmt(exact));set('abstract',fmt(abstract));set('equation',fmt(xs)+' × '+fmt(ys)+' → '+abstract.size+' sum(s)');$('#pairs').dataset.extra=xs.size*ys.size-new Set(pairs.map(p=>p.join(','))).size;$('#abstract').dataset.sums=[...abstract].sort((a,b)=>a-b).join(',');}$('#x').oninput=draw;$('#y').oninput=draw;draw();","audio":false,"strings":{"abstract":"Independent set x+y","exact":"Precise path x+y","heading":"What is lost by remembering x and y separately?","hint":"Path A is fixed at (1,2). Grid labels are (x,y), blue is real pairing, gold is generated only by independent combinations.","intro":"Two paths each produce an (x,y) pair. Modify the second path to observe which combinations are added to the precise pairing and Cartesian product.","reset":"Reset","scope":"Two feasible paths, integers 0..3, precise finite sets; this is not a complete constant propagation lattice, nor does it treat all CFG syntactic paths as truly feasible.","scopeLabel":"Model Scope and Conventions","x":"Path B's x","y":"Path B's y"}}
SSA and Sparse Analysis
SSA makes scalar def-use explicit, allowing many facts to propagate along relevant values, reducing work on irrelevant CFG edges. However, φ inputs depend on predecessor edges, loops may still require fixed points, and memory still has aliasing and side effects. SSA is not a guarantee that "all analyses degenerate to a single pass over the dominance tree."