Transformer short circuits logical Or correctly but not logical And

In the list.c0 example that I am working on we have both:

if (list == NULL || val <= list->val) { ... )

and

while (curr->next != NULL && curr->next->val < val) { ... )

Transformer turns the first code snippet into:

_ := list == NULL
_1 := !_
if (_1) {
  _2 := list.$struct_Node$val
  _ := val <= _2
}
if (_) { ... }

This is correct, because when list is not NULL in the logical Or we must evaluate the left hand side of the Or, val <= list->val to determine whether to take the true or false branch of the last if statement. Otherwise, when list == NULL, then the true branch of the last if statement is guaranteed to execute.

However, Transformer turns the second code snippet into:

_3 := curr.$struct_Node$next
_4 := _3 != null
_5 := !_4
if (_5) {
  _6 := curr.$struct_Node$next
  _7 := _6.$struct_Node$val
  _4 := _7 < val
}
while (_4) { ... }

This is incorrect, because we are dealing with logical And in this case. We want when curr->next != NULL is true to also check that curr->next->val < val, i.e. we want the true branch of the if statement to execute when curr->next != NULL. However, due to the negation in _5 := !_4, the true branch of the if will never execute when curr->next != NULL. To make this translation semantically correct, all we have to do is remove the negation from _5 := !_4. But, we need to preserve it for logical Or.

I've narrowed the problem down to this bit of Transformer code:

case logical: ResolvedLogical => {
        // Logical operators are short-circuiting, which introduces branching

        // Introduce a variable that represents the result of evaluating the LHS.
        // Immediately wrap it since we need a temporary variable that can be re-assigned without
        // modifying the original value.
        val (condition, lhsOps) = lowerExpression (logical.left, scope) match {
          case (expr, ops) => wrapExpr(expr, ops, scope)
        }

        val ops = ListBuffer[IR.Op](lhsOps:_*)

        // Negate the condition to check if the RHS needs evaluated
        val negated = scope.allocateTemp(IR.Type.Bool)
        ops += new IR.Op.AssignVar(negated, new IR.Expr.Not(condition))

        // Introduce an If that evaluates the RHS and assigns the result to the variable
        val (rhs, rhsOps) = lowerExpression(logical.right, scope)
        ops += new IR.Op.If(negated, new IR.Block(rhsOps :+ new IR.Op.AssignVar(condition, rhs)), new IR.Block(Nil))

        (condition, ops.toList)
}

In particular, this code always applies that negation, which is correct for logical Ors but incorrect for logical Ands.

Therefore, I propose the following code changes to fix the bug, which handles each Ors and Ands distinctly:

case logical: ResolvedLogical => {
        // Logical operators are short-circuiting, which introduces branching

        // Introduce a variable that represents the result of evaluating the LHS.
        // Immediately wrap it since we need a temporary variable that can be re-assigned without
        // modifying the original value.
        val (condition, lhsOps) = lowerExpression (logical.left, scope) match {
          case (expr, ops) => wrapExpr(expr, ops, scope)
        }

        val ops = ListBuffer[IR.Op](lhsOps:_*)

        val tmp = scope.allocateTemp(IR.Type.Bool)
        logical.operation match {
          case LogicalOperation.Or => ops += new IR.Op.AssignVar(tmp, new IR.Expr.Not(condition))
          case LogicalOperation.And => ops += new IR.Op.AssignVar(tmp, condition)
        }

        // Introduce an If that evaluates the RHS and assigns the result to the variable
        val (rhs, rhsOps) = lowerExpression(logical.right, scope)
        ops += new IR.Op.If(tmp, new IR.Block(rhsOps :+ new IR.Op.AssignVar(condition, rhs)), new IR.Block(Nil))

        (condition, ops.toList)
}

Please, review the proposed change. If it is correct, please make the change and commit the bug fix. Thanks!

Yeah, that looks good to me. I think what happened is that I implemented Or and was going to return and implement and but never got around to it.

I would suggest the following slight refactoring of your code, to factor out only the part that differs between && and ||:

ops += new IR.Op.AssignVar(tmp, logical.operation match {
      case LogicalOperation.Or => new IR.Expr.Not(condition)
      case LogicalOperation.And => condition
})

Also, this is something that should be tested, probably as an IR integration test, like the ones in src/test/resources/ir. The way I add tests for these is to create the .c0 file containing the element under test (see logical.c0 as an example test for ||). Create an empty file with the same name, but ending with .ir.c0 (see the logical.ir.c0 file for example), then run the tests. The tests will fail with a message containing the expected code. Copy this code, inspect it to make sure it matches what you expect, and then paste it into the .ir.c0 file and rerun to make sure it passes.

If you'd rather, feel free to commit your suggested changes and I could take care of adding the test.

gradual-verification / gvc0

Transformer short circuits logical Or correctly but not logical And #8