goto_check treats `ID_and` / `and_exprt` in a non-commutative way

[martin-cs]

While reviewing #6399 I wondered what is documented about it.

cbmc/src/util/simplify_utils.cpp

Line 51 in ce2680b

/// produce canonical ordering for associative and commutative binary operators

suggests that ID_and it is associative and commutative. However the handling of logical operations in goto_check is asymmetric:

cbmc/src/analyses/goto_check.cpp

Line 111 in ce2680b

/// Check a logical operation: check each operand in separation while

cbmc/src/analyses/goto_check.cpp

Line 1607 in ce2680b

void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)

These were refactoring made in https://github.com/diffblue/cbmc/pull/4611/files .

This seems a bit risky as a simplify in a pass before goto_check (for example in goto-analyzer --simplify) can alter / break the conditions that are generated.

[kroening]

Indeed; goto_check is very closely coupled with what comes out of the C front-end. The plan is to make goto_check part of the C front-end to remove this ambiguity.

[jimgrundy]

Would it make sense to have different ireps for logical ands and short-circuit ands?

[kroening]

sure, might help

[martin-cs]

Would it make sense to have different ireps for logical ands and short-circuit ands?

Maybe. IIRC && and || are split into multiple gotos during goto_convert so a && in the source code doesn't necessarily give an ID_and in the goto-program when it gets to goto_check. I am not sure about assumes and asserts though.

[jimgrundy]

I've gotten good performance improvements out of CBMC replacing "a && b" with "a & b" in my code when
1/ a and b are both expressions that return only 1 or 0
2/ b is an expression that cannot fail
Is there an optimization that does that automatically? Could there be one?

[tautschnig]

Closing for ef4dd67 actually moved analyses/goto_check to ansi-c/goto_check_c.