search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
839 stars 262 forks source link

Implement gcc integer overflow builtins. #4701

Closed danielsn closed 4 years ago

danielsn commented 5 years ago

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 commented 4 years ago

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

danielsn commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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

martin-cs commented 4 years ago

@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 commented 4 years ago

@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 commented 4 years ago

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 notifications@github.com wrote:

@danielsn https://github.com/danielsn The primitives have been implemented in PRs #5233 https://github.com/diffblue/cbmc/pull/5233,

5235 https://github.com/diffblue/cbmc/pull/5235, #5236

https://github.com/diffblue/cbmc/pull/5236, #5249 https://github.com/diffblue/cbmc/pull/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 https://github.com/diffblue/cbmc/issues/4701#issuecomment-652438855, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABBPVDXZL3CEQWGFXE7U4UDRZM7B3ANCNFSM4HPKCMNA .

danpoe commented 4 years ago

Issue for the performance improvements: #5405