C++: Add support for constant bound modulus operations

[jketema]

No description provided.

[MathiasVP]

This seems very sensible, but I'm wondering if it makes more sense to add this case in boundFlowStep (and call bounded recursively on the right-hand side)? I guess this would also handle a case such as:

int n = b ? 10 : 20;
range(unknown() % n)

?

[jketema]

This seems very sensible, but I'm wondering if it makes more sense to add this case in boundFlowStep (and call bounded recursively on the right-hand side)?

I'm not sure how to do this. How would this interact with a bound on the left-hand side? I'm not sure how to check whether that bound is missing or not. I started to run into non-monotonic recursion.

[jketema]

Or should I just completely ignore any bound coming from the left-hand side?

[MathiasVP]

Or should I just completely ignore any bound coming from the left-hand side?

I think so, yes. I think that's what SimpleRangeAnalysis is also doing.

[jketema]

Move to bounded as discussed. Also started a DCA experiment on top of the feature branch.

[MathiasVP]

I just noticed that boundFlowStep already has a case that handles SemRemExpr when the right-hand side is guaranteed to be positive. We might need to exclude that situation in our newly added case to prevent a duplication of computed bounds.

[jketema]

I just noticed that boundFlowStep already has a case that handles SemRemExpr when the right-hand side is guaranteed to be positive. We might need to exclude that situation in our newly added case to prevent a duplication of computed bounds.

I'm not sure how. I also having a hard time believing those bound by the way. It's not immediately clear to me why they would be correct.

[MathiasVP]

I'm not sure how.

Since one of the two boundFlowStep cases require that the right-hand side is always positive, you could exclude this case by requiring that not semPositive(rem.getRightOperand()), and the other case could similarly be exclude by requiring that not semPositive(rem.getLeftOperand()).

I also having a hard time believing those bound by the way. It's not immediately clear to me why they would be correct.

Hm, I don't see what's wrong with those bounds. If e = x % y then the first of the two cases in boundFlowStep says that if y <= B + k (for some SemBound B and constant k) then e <= B + (k - 1) (because it transfers the bound computed for y to the bound computed for e with a delta of -1). And the second bounds says that, if x <= B + k then e <= B + k (because it transfers the bound computed for x to the bound computed for e wit ha delta of 0). Aren't both of those bounds correct?

[jketema]

Ah. I don't think I was reading the code correctly. I'll have another look.

[jketema]

@MathiasVP Updated the PR and ran a new DCA experiment (which looks ok to me).

[MathiasVP]

LGTM!