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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

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?
>
> For example:
>
>   (declare-const a ( _ BitVec 32 ))
>   (declare-const b ( _ BitVec 32 ))
>   
>   ; Assume 0 <= a, b, <= 5
>   (assert (bvsge a #x00000000))
>   (assert (bvsge b #x00000000))
>   (assert (bvsle a #x00000005))
>   (assert (bvsle b #x00000005))
>   
>   ; Check if 0 <= a + b  <= 10
>   (assert (not (and (bvsle (bvadd a b) #x0000000A) (bvsge (bvadd a b) #x00000000))))
>   
>   (check-sat)
>
> Of course, the example above is obvious, but with overflows and other corner cases it is great to have a tool doublecheck our assumptions, and share how to reproduce the results.

I usually add things like this not about the tests, but about the implementation. I think it provides a bit more generality.  But usually I do it as a comment to the patchset, maybe it is also good to put it in the code as well.

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?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103440