Fix internal error when using an empty tuple with a ternary operator

[pgebal]

Closes #14929

The reason for this bug is that we forgot to handle an empty tuple in a code that translates instances our internal classes to z3 expressions.
I fixed it by adding the missing part of an if statement in Z3Interface::toZ3Expr.

[cameel]

Note that many things that are not supposed to return anything actually return an empty tuple. It would be best to add a few more tests to make sure they all work.

For example using a function with no return value causes this ICE too:

function f() {}
function g() {}

contract C {
    function test() public {
        true ? f() : g();
    }
}

Another case are events and errors (both instances and types), though I can't think of a way those could be used in a ternary expression.

An attempt to return an empty tuple from a function triggers the ICE too:

contract C {
    function test() public {
        return true ? () : ();
    }
}

[pgebal]

Thanks for test ideas. Those 2 cases no longer cause ICE after the fix.
Where can I learn more about what returns an empty tuple? Is istsomewhere in solidity docs?

[cameel]

I don't think it's explicitly documented unfortunately. The way to find out is to basically try things out and look at error messages. I know it from writing lots of test cases (and sometimes from implementation).

In any case, the ones I already listed probably cover most of it. Aside from errors and events most of the cases will just be various kinds of functions that don't return anything, including the built-in ones like require() or <address>.transfer(). Maybe some of the syntax elements and control structures that can be used inside expressions also technically return tuples, but you'd have to try them one by one. If you added the ones I listed, it's good enough.

[cameel]

The fix looks quite generic. Why were only empty tuples affected?

I checked a simple case like this and it seems to work fine, but is it possible that things were actually broken in more complex cases of non-empty tuples?

contract C {
    function test() public {
        true ? (1, 2) : (3, 4);
    }
}

[pgebal]

That's unlikely. The reason for this bug is that we forgot to handle an empty tuple in a code that translates our internal classes to z3 expression. Non-empty tuples are handled correctly.

[cameel]

So are empty tuples encoded differently than non-empty ones?

[blishko]

No, the representation is the same. The problem is that before we get to handling tuples (tuple_constructor) there is this check:

solidity/libsmtutil/Z3Interface.cpp

Line 160 in 37d4533

else if (arguments.empty())

So there is a special case for handling expressions with zero arguments, but it did not cover empty tuples before.

[blishko]

@pgebal: Related to @cameel 's comments, please add explanation what was causing the bug and how is the change fixing it.

[pgebal]

@pgebal: Related to @cameel 's comments, please add explanation what was causing the bug and how is the change fixing it.

done

[blishko]

LGTM!

There is a general code to handle tuple constructor, but this shortcut to handle expressions without arguments is taken for empty tuple before we get to the general handler. So the bug happens only for empty tuples and this is a good place to fix it.

[blishko]

@pgebal, can you rebase the PR? Then we can merge.

[pgebal]

@pgebal, can you rebase the PR? Then we can merge.

sure, done

[cameel]

Needs a rebase on develop now that we merged the fix for failing tests (#15035).