Add option removeBranchingOnConstants

[michael-schwarz]

This option can be used to disable the removal of the non-taken branches for branching over constants.

Enables analyzers to report such code as dead to the users. (c.f. goblint/analyzer#94)

[sim642]

Unfortunately this constant dead code logic is not as localized, but there are at least four more places where it's done:

cil/src/frontc/cabs2cil.ml

Lines 4768 to 4770 in 7f428b6

	CEExp (se1, e1') when isConstFalse e1' && canDrop se2 ->
	finishExp (se1 @@ se3) (snd (castTo t3 tresult e3')) tresult
	| CEExp (se1, e1') when isConstTrue e1' && canDrop se3 ->

cil/src/frontc/cabs2cil.ml

Lines 5084 to 5092 in 7f428b6

	CEExp (se1, ((Const _) as ci1)), _ ->
	if isConstTrue ci1 then
	addChunkBeforeCE se1 ce2
	else
	(* se2 might contain labels so we cannot always drop it *)
	if canDropCE ce2 then
	ce1
	else
	CEAnd (ce1, ce2)

cil/src/frontc/cabs2cil.ml

Lines 5103 to 5111 in 7f428b6

	CEExp (se1, (Const(CInt _) as ci1)), _ ->
	if isConstFalse ci1 then
	addChunkBeforeCE se1 ce2
	else
	(* se2 might contain labels so we cannot drop it *)
	if canDropCE ce2 then
	ce1
	else
	CEOr (ce1, ce2)

And I'm not sure if that even covers them all because there are so many different ways this is checked in different places: is_zero_cilint, isZero, isConstTrue, isConstFalse, etc.

[michael-schwarz]

Unfortunately this constant dead code logic is not as localized, but there are at least four more places where it's done

As far as I can see, these cases are within expressions(!), and there is no real reason to disallow it for those, or is there?

[jerhard]

Assuming we have code, such as

int truef(){
    return 1;
}

int main(){
    int x = 0 && truef();
    int y = 1 && truef();
    return x + y;
}

Goblint (on 924c219 with alldeadcode) will not warn that the call to truef in the first line of main will never happen. One might potentially be interested in such cases.

[sim642]

As far as I can see, these cases are within expressions(!), and there is no real reason to disallow it for those, or is there?

It would make things fully consistent though. a && b is also an expression and in Goblint we do produce warnings about branches over a or b being dead if they happen to be constant. It would be weird if we suddenly didn't in the even simpler case where they are constant by literal, not by propagation.

And at least one of the linked snippets is about ?: which is explicitly about branching and which Goblint in non-constant-literal cases may produce dead branch warnings about.

So it's about dead branches, rather than dead lines.

[michael-schwarz]

I have now modified CIL to also respect removeBranchingOnConstants for expressions.
However, we still perform this simplification of expressions when they are used in a constant context (e.g. inside of definitions of enums etc.). If we also did not do it there, CIL will generate statements that have nowhere to go, and CIL will fail. This occurs e.g. frequently in Linux headers.