[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

[Manas Gupta via Phabricator via cfe-commits]

manas added a comment.

In D103440#2800710 <https://reviews.llvm.org/D103440#2800710>, @vsavchenko wrote:

> In D103440#2800122 <https://reviews.llvm.org/D103440#2800122>, @manas wrote:
>
>> In D103440#2799629 <https://reviews.llvm.org/D103440#2799629>, @xazax.hun wrote:
>>
>>> I was wondering, if we could try something new with the tests. To increase our confidence that the expected behavior is correct, how about including a Z3 proof with each of the test cases?
>>
>> We are looking forward to design a unit-test framework for the solver which can compact the test cases and make them much more manageable (unlike `constant-folding.c`). Perhaps, we can incorporate the Z3 proves in that framework, corresponding to test cases.
>
> Hmm, so you mean we can check if the analyzer was compiled with Z3 and if so, verify the same things by it?

Yeah in some sense. But I think that having proof for every test case may become redundant for certain cases.

For e.g., consider two test cases for addition operator:

1. c == [0, 10] and d == [-10, 0] will result in (c + d) == [-10, 10]
2. c == d ==  [0, 10] will result in (c + d) == [0, 20]

But the first test case can be modeled as `c - (- d)`or `c - D`, that is,

- usage of subtraction binary operator : (c **-** D), and
- symmetrical inversion of range around origin (**-** d) for symbol `d`. This will shift the range from `[-10, 0]` to `[0, 10]`.

Considering having proof for every test case will make the proof for test-case 1 kind of redundant.

So, I think we should go with @vsavchenko 's method of adding Z3 proof with the **implementation** (in code), instead of test cases themselves.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103440/new/

https://reviews.llvm.org/D103440