`CheckSafetyRuleBodies` compiler stage fails to reorder unordered rule bodies with too many indirections

[johanfylling]

Consider the following policy:

package example

a := z if {
    y = f(x)
    z = f(y)
    x = 2
}

b := z if {
    y = f([v | v = x][0])
    z = f(y)
    x = 2
}

c := z if {
    x = 2
    y = f([v | v = x][0])
    z = f(y)
}

f(x) := x + 1 

Even though rules a and b have unordered bodies (x is assigned through unification after it is being used), the compiler should be able to reorder these rules to be safe for evaluation (via the CheckSafetyRuleBodies stage).

When evaluated however, we get an unexpected result:

$ opa eval -d policy.rego 'data.example' -fpretty
{
  "a": 4,
  "c": 4
}

The a and c rules successfully evaluated to a value, since a was successfully reordered and c didn't require reordering; whereas b failed to evaluate.

The CheckSafetyRuleBodies compiler stage output gives us:

package example

a := z if {
	x = 2                                    # x successfully reordered to precede all usage
	data.example.f(x, __local1__)
	y = __local1__
	data.example.f(y, __local2__)
	z = __local2__
}

b := z if {
	y = __local4__                           # __local4__ indirectly depends on x
	data.example.f(y, __local5__)
	z = __local5__
	x = 2                                    # x failed to be reordered to precede all (indirect) usage
	__local3__ = [v | v = x]
	data.example.f(__local3__[0], __local4__)
}

c := z if {
	x = 2
	__local6__ = [v | v = x]
	data.example.f(__local6__[0], __local7__)
	y = __local7__
	data.example.f(y, __local8__)
	z = __local8__
}

f(__local0__) := __local9__ if {
	true
	__local9__ = __local0__ + 1
}

We see above that the compiler fails to move the assignment of x to precede all indirect usage, which causes rule b to fail even though it should be semantically equivalent to c (save for body statement order).

Note: this is an old issue that may be unlikely to surface; but the introduction of template-strings might make it more frequent, as their reliance on set comprehensions make this kind of indirection more common even for trivial policies (however, an "unordered" rule body is a prerequisite).