Seemingly incorrect definite assignedness after true/false

Issue #89 resolved
Jesper Öqvist created an issue

The equations for definite assignedness after true/false seem incorrect when comparing to the specification in JLSv3 16.1.7:

Actually, the definite assignedness after true/false checks look incorrect. Diff against what they probably should be:

-  eq Expr.isDAafterFalse(Variable v) = isTrue() || isDAbefore(v);
-  eq Expr.isDAafterTrue(Variable v) = isFalse() || isDAbefore(v);
+  eq Expr.isDAafterFalse(Variable v) = isTrue() || isDAafter(v);
+  eq Expr.isDAafterTrue(Variable v) = isFalse() || isDAafter(v);

This is difficult to find a test case to check, and applying the patch above causes lots of regressions.

Comments (4)

  1. Jesper Öqvist reporter

    There are equations for Binary which provide the correct value in most cases,

      syn lazy boolean Binary.isDAafterTrue(Variable v) = isFalse() || getRightOperand().isDAafter(v);
      syn lazy boolean Binary.isDAafterFalse(Variable v) = isTrue() || getRightOperand().isDAafter(v);

    however CastExpr is a subtype of Expr but not Binary so it is not covered by the correct expressions so I was able to create a test case using this info:

    // .result=COMPILE_PASS
    class Test {
                    int x;
                    int y = 3;
                    if (((boolean) (false || ((x=y)==2))) || true) ;
                    int z = x; // x is definitely assigned here

    This case finally exposes a bug in the equations. However, the question is why I get regressions when I apply the fix.

  2. Jesper Öqvist reporter

    Test errors caused by stack overflows. Some incorrect circular evaluation in the DAafterFalse attribute.

  3. Jesper Öqvist reporter

    The problem was an additional error in Expr.isDAafter:

    -  eq Expr.isDAafter(Variable v) = (isDAafterFalse(v) && isDAafterTrue(v)) || isDAbefore(v);
    +  eq Expr.isDAafter(Variable v) = isDAbefore(v);

    This caused for example integer literals to incite an infinite recursive call chain.

  4. Log in to comment