Bug with Automaton.Rewrite(int,int)

[DavePearce]

Issue by DavePearce
Wednesday May 15, 2013 at 00:57 GMT
Originally opened as Whiley/WhileyCompiler#273

---

There is currently a bug (or feature?) with the method Automaton.rewrite(int from,int to). The essential issue is that the method replaced all occurrences of from with to including those reachable from to.

This causes a problem with the following rule:

reduce Sum[real x, {|Mul... xs|}]:
    => let negs = {| y | y in xs, (*y)[0] < 0.0 |} 
       in Mul[-1.0,{|Sum[x,xs]|}], if x == 0.0 && (|xs| - |negs|) < |negs|

To understand, consider the outermost node as having index 8 and the new Mul has having index 23. Then applying the rule rewrites 8 => 23. Now, let's take a closer look at the automaton:

#20 [2,19], #21 {|8|}, #22 [4,21], #23 1(22) <18>

The key is that, as expected, state 8 is reachable from 23. This reflects the fact that the Mul does indeed contain a reference to the outermost Sum node. Unfortunately, this reference gets rewritten to 23 when applying rewrite, leading to a curious loop in the resulting automaton.

[DavePearce]

Comment by DavePearce
Wednesday May 15, 2013 at 00:59 GMT

---

The workaround is simply to ensure that Mul doesn't reference exactly the same node. That is, it must reference an equivalent but initially distinct node. That node can then be reduced down, and it'll all work out.

[DavePearce]

Comment by DavePearce
Wednesday May 15, 2013 at 01:10 GMT

---

For example, I can rewrite the above rule as follows:

reduce Sum[real x, {|Mul... xs|}]:
    => let negs = {| y | y in xs, (*y)[0] < 0.0 |},
           ys   = {| Mul[-(*y)[0],(*y)[1]] | y in xs |}
       in Sum[0,ys], if x == 0.0 && (|xs| - |negs|) < |negs|

This avoids the problem. But, sadly, the system doesn't tell me when I need to avoid the problem!!