Skip to content

Rule in opt.gvn.expr.Expr restricting phi-node nesting is imprecise #4

@zGoldthorpe

Description

@zGoldthorpe

The expression class enforces a rule that disallows $\phi$-nodes to be an operand of another expression, which is in place to ensure that infinite nesting does not occur during any of the existing GVN passes. However, this is needlessly restrictive.

The rule should just enforce that nested $\phi$-nodes are disallowed. This would allow for finer reasoning with values, and can aid in finding loop invariants.

For example, consider code/gvn/flow/lift_to_max.ami, which in pseudocode is

x = read()
y = read()
if x > y:
    x, y = y, x
while x < y:
    x += 1
write(x)
write(y)

Below is equivalent, simplified ami code:

@enter:                                                               
    read %x.0                                                         
    read %y.0                                                         
    %flip = %y.0 < %x.0                                               
    branch %flip ? @flip : @loop                                      

@flip:                                                                
    %x.1 = %y.0                                                       
    %y.1 = %x.0
    goto @loop                                                        

@loop:                                                                
    %x.2 = phi [ %x.0, @enter ], [ %x.1, @flip ], [ %x.3, @iterate ]  
    %y.2 = phi [ %y.0, @enter ], [ %y.1, @flip ], [ %y.2, @iterate ]  
    %delta = %x.2 < %y.2                                              
    branch %delta ? @iterate : @done                                  

@iterate:                                                             
    %x.3 = %x.2 + 1                                                   
    goto @loop                                                        

@done:                                                                
    write %x.2                                                        
    write %y.2                                                        
    exit                                                              

The current implementation of Gargi's GVN algorithm assigns $x_2$ and $y_2$ to
$$x_2 \gets \phi(\overset{x_0\leq y_0}{x_0}, \overset{y_0 &lt; x_0}{y_0}, \overset{x_2 &lt; y_2}{x_2+1}) \qquad y_2 \gets \phi(\overset{x_0\leq y_0}{y_0}, \overset{y_0 &lt; x_0}{x_0}, \overset{x_2 &lt; y_2}{y_2})$$

We should be able to infer from this that $x_2 \leq y_2$ is a loop invariant (and thus when the @loop branch condition is false, conclude that $x_2 = y_2$).

Metadata

Metadata

Assignees

Labels

enhancementNew feature or request

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions