[Analyzer] [WIP] Basic support for multiplication and division in the constraint manager
Needs RevisionPublic

Authored by baloghadamsoftware on Mon, Jul 9, 5:19 AM.

Details

Summary

Currently, the default (range-based) constrain manager supports symbolic expressions of the format "symbol + integer" or "symbol - integer" to compare them to another integer. However, multiplication and division is not supported yet.

An example where this lack of support causes false positives is the following:

unsigned size = 32;
int init(int *s);
void assert(int);
static void test(void)
{
  int val;
  if (size>10 && size<=100){
     for (unsigned j = 0; j<size/2; j++)
      init(&val);
     assert((int) (val == 1));  //False positive: val may be uninitialized
  }
}

In this example the loop executes at least 5 times, but the analyzer cannot deduce this so it assumes that it may be completely skipped, since it cannot reason about size/2 even if it knows that size has a range of (10..100] which is [11..100] among integers.

This patch solves this problem by introducing support for symbols such as "symbol * integer" or "symbol / integer". In this patch only positive integers are supported. On the long-term our goal is to extend this support to more generic first-degree symbolic expressions, e.g. "symbol * integer + another integer".

Diff Detail

All existing tests pass. I could not find the appropriate test file so I created a new one, but this is probably not the correct way.

@baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about instead using Z3 cross-check functionality recently added, to solve this and all other similar problems instead?

george.karpenkov requested changes to this revision.Mon, Jul 9, 10:57 AM

Let's discuss alternatives first.

This revision now requires changes to proceed.Mon, Jul 9, 10:57 AM
NoQ added inline comments.Mon, Jul 9, 3:36 PM
test/Analysis/constraint_manager_scale.c
78

If int is 32-bit and x equal to 2³¹ - 1, we have x * 2 equal to -2 which is less than 8, while x is greater than 4.

The overall point is that writing this kind of code is *extremely* error-prone.
We are actually considering going in a different direction and doing a rollback for the previous rearrangement patches due to some issues.
Could you see whether Z3 visitor would meet your needs?

baloghadamsoftware added a comment.EditedWed, Jul 11, 12:24 AM

@baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about instead using Z3 cross-check functionality recently added, to solve this and all other similar problems instead?

As far as I know the purpose of the cross-check functionality is to execute Z3 only on actual bug report paths. This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

As we discussed with @dcoughlin at the Euro LLVM 2018 the community should consider a new constraint manager, which is in between the range-based one and the Z3 both feature and performance wise. However, this is something long term, until then we should improve the existing one as far as reasonable. I am sure that multiplicative operations can be solved similarly to the additive ones.

test/Analysis/constraint_manager_scale.c
78

Thank you for pointing me out this! I uploaded this patch as WIP since I was sure I missed something because of modular arithmetic. I think this can be solved, even if not so easily. Maybe we should restrict the first version to division only?

The overall point is that writing this kind of code is *extremely* error-prone.

Every modifications on the core is extremely error-prone. That is why we must cross check it and only apply it if it is 100% mathematically correct. This patch is only WIP for now. Freezing the core in its current state helps us to not introduce new errors but also prevents improving the current functionality which is not yet sufficient for many of our customers. What I did is not hacking, multiplicative operations can be implemented a similar way to additive ones, they are just a bit more complex.

We are actually considering going in a different direction and doing a rollback for the previous rearrangement patches due to some issues.

What issues could it cause since it is guarded by an option? As for the rearrangement of the additive operations it was @NoQ's idea but I agree there. Actually I feel this rearrangement patch a bit of hacking, but I also agree with @NoQ that it may be useful for other checkers as well. That was the reason to put it into SValBuilder instead of the checker itself. As you may be aware of it I originally did the rearrangement inside the checker.

Could you see whether Z3 visitor would meet your needs?

We will look at it, but please read my previous answer.

This comment was removed by baloghadamsoftware.

What issues could it cause since it is guarded by an option?

I've meant the rearrangement. Actually, I would like to apologize for that point, I thought it was causing some issues, but it wasn't, we've just checked it yesterday.

As far as I know the purpose of the cross-check functionality is to execute Z3 only on actual bug report paths.

Yes.

This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.

This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.

This is not an example from the iterator checker (hopefully Adam will provide us with one example from there) but think of division by zero. The division by zero check will only warn if a value is constrained to be zero. The imprecision in the built in solver might result in failure to constrain a value to zero while the Z3 might be able to do that.

The imprecision in the built in solver might result in failure to constrain a value to zero while the Z3 might be able to do that.

Ah right, that's a good point, we only throw a null-pointer deref/division by zero when the pointer/value is definitely zero.

Do you have *motivating* examples though, like an actual code samples where you got a bug and the analyzer does not warn?
In my experience, we almost never warn about division by zero anyway,
and the null pointer dereference check is too noisy if anything.

MTC added a subscriber: MTC.Wed, Jul 11, 7:21 PM
NoQ added a comment.Thu, Jul 12, 1:54 PM

I'd also rather stick to integer arithmetic and avoid using floats even in intermediate calculations. It'd be hard to make sure that no rounding errors kick in if we use floats.

In D49074#1160793, @NoQ wrote:

I'd also rather stick to integer arithmetic and avoid using floats even in intermediate calculations. It'd be hard to make sure that no rounding errors kick in if we use floats.

Yes, I agree. I think an integer plus a flag (whether to take the reciprocal) is better since we only use n or 1/n for scaling.