Try to evaluate __builtin_choose_expr arguments as constants if possible

[jprotopopov-ut]

This feature is necessary for Linux kernel module analysis.

[sim642]

Isn't this already being done here?

cil/src/frontc/cabs2cil.ml

Lines 4709 to 4715 in e21285a

	else if fv.vname = "__builtin_choose_expr" then
	begin
	(* Constant-fold the argument and see if it is a constant *)
	(match !pargs with
	[ arg; e1; e2 ] -> begin
	match constFold true arg with
	| (Const _) as x ->

[jprotopopov-ut]

Isn't this already being done here?

cil/src/frontc/cabs2cil.ml

Lines 4709 to 4715 in e21285a

	else if fv.vname = "__builtin_choose_expr" then
	begin
	(* Constant-fold the argument and see if it is a constant *)
	(match !pargs with
	[ arg; e1; e2 ] -> begin
	match constFold true arg with
	| (Const _) as x ->

If I run the newly introduced test case on upstream Goblint, it results in Bug: newTempVar called outside a function error. My patch fixes the issue.

Whether or not this is the correct place to fix it, I am not sure, my primary concern was getting it to work with Linux kernel sources. I am not familiar enough with Goblint code base to make such judgements.

[sim642]

I think I see what the issue is: the constant expressions in the test contain short-circuiting logical operators, which doExp false converts to some if-based branching control flow which won't be allowed in a constant context. And it's too late for constFold to do anything about it.
Whereas doExp true forces the logical operators to be kept around as logical operators (LOr, LAnd) in a single branching-free expression. That expression can then be constFold-ed into a constant.

This seems like a broader oversight than __builtin_choose_expr though. Logical operators would probably bother constant folding in __builtin_constant_p and lots of other things.
If doExp is called with asconst = true, then it seems strange that doExp would recursively be called with false.
So my intuition is that instead of doExp isBuiltinConstArg it would be more general to doExp asconst. But maybe that causes something else strange to happen.

[jprotopopov-ut]

Changed to asconst and re-run CIL and Goblint tests. It seems to be working fine, so I pushed the change.