Implement gcc integer overflow builtins.

[danielsn]

Now that we have the overflow primitives, it would make sense to implement all the gcc builtins https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html

[danielsn]

@tautschnig may have solved this already; if so, feel free to close the ticket

[danielsn]

Note: the current overflow primitives lead to a significant performance cost when used in the naïve way, since they require the user to do a multiplication, keep the overflow bit but throw away the result, and do it again to get the result. Fixing this would help performance.

[martin-cs]

Maybe. In some cases the back-end will cache the two things back together. More importantly though, there are way better encodings of multiply overflow check than doing the full multiply.

[hannes-steffenhagen-diffblue]

@martin-cs What are the way better encodings for multiply overflow check?

[martin-cs]

@hannes-steffenhagen-diffblue Somewhere there is a Z3 paper from ... '09 or so with a more compact encoding but, as it's Friday, let's see what we can do in a comment.

First do the unsigned case as it's easier. Assume bit-vectors are length n. Consider the easy cases first:
*. If either x or y is 1 or 0 then it trivially it doesn't overflow.
*. If both are under sqrt(2^n - 1) then it trivially doesn't overflow. This is just a simple bit test and removes a number of bits from consideration outright.
*. Consider the ith and jth bits of x and y (apart from the ones above) with i + j >= n if they are both 1 then it overflows. This removes a maybe half of the partial product terms.
*. You can sum all of the remaining bits in the usual way but I think we can do better than that. I'd start building a tree (well, DAG, so cache) of ways that top bit can overflow. Either of it is a 1 and one of the lower log(n) bits carry a 1 up to it's position or it is a 0 and 2 or more of the lower log(n) bits carry up a 1 ... apply this recursively and you have a tree. This could probably be built stepwise as a refinement for the best encoding as I suspect it is rarely needed.

@danielsn / @hannes-steffenhagen-diffblue If either of you have interest and a set of real-world performance critical benchmarks that depend on this I can try to turn this into code and / or talk one of you through doing it.

[danpoe]

@danielsn The primitives have been implemented in PRs #5233, #5235, #5236, #5249 which have all been merged. What could still be done is implement some of the ideas for speeding up the checks. I would suggest we close this ticket here, and if the performance improvements are still required we can create a separate issue/ticket.

[danielsn]

Sounds good. Let’s open an issue for the checks, which are indeed the bottlenecks for some proofs.

…

On Wed, Jul 1, 2020 at 10:05 AM Daniel Poetzl ***@***.***> wrote: @danielsn <https://github.com/danielsn> The primitives have been implemented in PRs #5233 <#5233>, #5235 <#5235>, #5236 <#5236>, #5249 <#5249> which have all been merged. What could still be done is implement some of the ideas for speeding up the checks. I would suggest we close this ticket here, and if the performance improvements are still required we can create a separate issue/ticket. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#4701 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABBPVDXZL3CEQWGFXE7U4UDRZM7B3ANCNFSM4HPKCMNA> .

[danpoe]

Issue for the performance improvements: #5405