Hi,

Please find a patch to fix part of the bug PR analyzer/94362. This bug is a
false positive for a null dereference found when compiling openssl. The cause
is the constraint_manager not knowing that i >= 0 within the for block:

for ( ; i-- > 0; )

The bug can be further reduced to the constraint manager not knowing that i >= 0
within the if block:

if (i-- > 0)

which is not replicated for other operators, such as prefix decrement. The
cause is that the constraint is applied to the initial_svalue of i, while it
is a binop_svalue of i that enters the block (with op PLUS and arg1 -1). The
constraint_manager does not have any constraints for this svalue and has no
handler. A handler has been added that essentially recurs on the remaining arg
if the other arg and other side of the condition are both constants and the op
is PLUS_EXPR or MINUS_EXPR.

This in essence fixed the problem, except an off by one error had been hiding
in range::eval_condition. This error is hard to notice, because, for example,
the code

if(idx > 0)
  __analyzer_eval(idx >= 1);

will compile as (check -fdump-ipa-analyzer to see)

void test (int idx)
{
  _Bool _1;
  int _2;

  <bb 2> :
  if (idx_4(D) > 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  _1 = idx_4(D) > 0;
  _2 = (int) _1;
  __analyzer_eval (_2);

  <bb 4> :
  return;

}

and will print "TRUE" to the screen, but as you can see, it is for the wrong
reason, because we are not really testing the condition we wanted to test.

You can force the failure (i.e. "UNKNOWN") for yourself with the following:

void test(int idx)
{
  int check = 1;
  if(idx > 0)
    __analyzer_eval(idx >= check);
}

which the compiler will not "fix" on us. An examination of range::eval_condition
should convince you that there is an off by one error. Incidentally, I might
recommend doing away with "open intervals of integers" entirely.

When running the initial bug (the for loop), you will find that the analyzer
prints "UNKNOWN" twice for the postfix operator, and "TRUE" "UNKNOWN" for other
operators. This patch reduces postfix to the same state as the other operators.
The second "UNKNOWN" seems to be due to a second "iterated" pass through the
loop with a widening_svalue. A full fix of the bug will need a handler for the
widening svalue, and much more critically, a correct merge of the constraints
at the loop entrance. That, unfortunately, looks to be a hard problem.

This patch fixes a few xfails as noted in the commit message. These were tests
that were evidently devised to test whether the analyzer would understand
arithmetic being done on constrained values. Addition and subtraction is now
working as expected, a handler for multiplication and division can be added.

As was noted in those test files, consideration at some point should be given to
overflow.


Thank you,
Brian

Sent with ProtonMail Secure Email.