Internal Invariants : How many operands should a binary expression have?

[martin-cs]

[ This is a question about what should be enforced / assumed about binary_exprts; it is not a bug report (yet!). See also https://github.com//issues/751. ]

https://github.com/diffblue/cbmc/blob/master/src/util/std_expr.h#L452
https://github.com/diffblue/cbmc/blob/master/src/util/std_expr.h#L487
https://github.com/diffblue/cbmc/blob/master/src/util/std_expr.h#L502

Rather imply the answer should be 2. However a plus_exprt is a binary_exprt

https://github.com/diffblue/cbmc/blob/master/src/util/std_expr.h#L608

and plus_exprt's can (and in the back-end) do have more than two operands, which is allowed by to_plus_expr:

https://github.com/diffblue/cbmc/blob/master/src/util/std_expr.h#L643

Possible fixes:

1. Weaken the invariant on binary_exprt; >= 2 is enough. Review code that uses it for possible issues where ==2 has been assumed. Less work but may hide bugs / misunderstandings.

2. Create associative_exprt with >=2 operands and move plus_exprt and mult_exprt to inherit from it. Deal with the breakage that this has caused but be happy that it will have found the possible issues. (I'm not quite sure what the >=2 operand version of minus_exprt means; I'd be tempted to keep it binary as it's a stretch to call is associative and enforce the binary-ness of it). More work but should help developers write more correct code.

I think the following code should demo the problem:

plus_exprt plus(a,b);
plus.operands().push_back(c);

binary_exprt bin(plus); // Works...
exprt exp(plus);
binary_exprt(to_binary_expr(exp)); // Doesn't

[kroening]

We need to introduce an explicit 'multi-ary' expression base class; plus_exprt would be one, but the shifts would not be.

[tautschnig]

Would a 'multi-ary' expression base class be any more specific than exprt? Maybe plus_exprt (and possibly others) simply shouldn't be inheriting from binary_exprt?

[martin-cs]

This is why I suggested an associative_exprt, whose invariants would be operands().size() >= 2 and flattening in expressions of the same id() would not change the value. Depending on what meets the criteria we might add symmetry as well so that the operands can be reordered.

[tautschnig]

Be aware that other than via RTTI we wouldn't have any way of knowing that an expression is an associative_exprt. Thus it would almost exclusively be information usable by humans, not necessarily by the compiler.

[martin-cs]

ID_and, ID_or, ID_bitor, ID_bitxor, ID_bitand would be other candidates, all of which are symmetric and associative. ID_concatinate is an example of an associative but not symmetric operation.

[tautschnig]

It may be worth mentioning that 3f1afed and 35eb739 have "happened".

[kroening]

It may be worth mentioning that multi_ary_exprt does have some semantic change over exprt -- this is not just 'human documentation'. In particular binary_exprt comes with two operands when constructed, a multi_ary_exprt does not.

[tautschnig]

@kroening Would you mind explaining what the difference between multi_ary_exprt and exprt is? (It's safe to say that I am very unhappy about the fact that 3f1afed and 35eb739 just "happened" without any chance for further discussion.)