Base: Inconsistencies in eval_rv

[michael-schwarz]

While looking at #1696, I started wondering why for

//PARAM: --set sem.int.signed_overflow assume_none --enable ana.int.interval
int main(void)
{
   int h = 31;

   if (1 << h) {

   }
}

we produce a warning that both branches are dead, while we do not do so for

//PARAM: --set sem.int.signed_overflow assume_none --enable ana.int.interval
int main(void)
{
   int h = 31;

   if (1 << h != 0) {

   }
}

which is an equivalent program.

It turns out there is a (unrelated), but quite surprising difference where for one program eval_rv returns VD: Int (ID.top_of ik) vs. VD: Int (ID.bot ()) for the other:

analyzer/src/analyses/base.ml

Lines 1102 to 1109 in b90ee73

	let eval_rv ~man (st: store) (exp:exp): value =
	try
	let r = eval_rv ~man st exp in
	if M.tracing then M.tracel "eval" "eval_rv %a = %a" d_exp exp VD.pretty r;
	if VD.is_bot r then VD.top_value (Cilfacade.typeOf exp) else r
	with IntDomain.ArithmeticOnIntegerBot _ ->
	ValueDomain.Compound.top_value (Cilfacade.typeOf exp)

• For the first program, the evaluation produces Int (ID.bot ()), which does not trigger the check for VD.is_bot r and eval_rv returns Int (ID.bot ()).
• For the second program, eval_rv triggers an IntDomain.ArithmeticOnIntegerBot exception when evaluating the BinOp, which results in the value Int (ID.top_of ik)) for the appropriate ik.

In branch, neither of these values evaluate to a definite bool, so refine is called either way, but still this discrepancy is a little worrying.