Support custom sized bitvectors

[mikhailramalho]

Request from the cseq team.

They're using frama-c to do some interval analysis and define custom bitvectors with arbitrary size. In a number of cases, the verification time is much smaller.

CBMC uses this weird semantic:
__CPROVER_bitvector[10] a;

Obviously, the clang frontend will not allow that, even if we define the __CPROVER_bitvector type.

The easiest solution I could come up is to use source annotations, which we already use for infinite sized arrays. I propose something like:

attribute((annotate("bv=10")))
int a;

This is parsed by clang, we can still compile the code and it will require little effort to implement.

The down side: it will only be supported by the new frontend.

[jmorse]

Hi,

On 09/02/17 19:53, Mikhail Ramalho wrote: The down side: it will only be supported by the new frontend.

Completely acceptable as far as I'm concerned, we should be comfortable with the old frontend dying.

They're using frama-c to do some interval analysis and define custom bitvectors with arbitrary size. In a number of cases, the verification time is much smaller.

Sweet,

The easiest solution I could come up is to use source annotations, which we already use for infinite sized arrays. I propose something like: *attribute*((annotate("bv=10"))) int a; This is parsed by clang, we can still compile the code and it will require little effort to implement.

I can't immediately think of any circumstance that would break as a result of this, other than if pointers came anywhere near these bitvectors. We still don't do bitfields {well,at all}, and this is a specialization of bitfields. If they're attacking this from the python-api or SSA level directly, obviously they can bypass any risk of pointer stuff.

…

-- Thanks, Jeremy

[thefischsun]

Hi - well, this specific application scenario should be safe. What happens is that we (well, Truc :-) run Frama-C over the sequentialized program to overapproximate the range of values that integer variables (only those) can take on any given run, and then replace those by bitvectors with the minimum number of bits required to represent that overapproximation. Big win if integers are used as booleans, or for all the indices into an array etc. The gains grow with the number of SSA representations of the original variable. (In fact, it might be even better to run this over the SSA representation, rather than the C-code, but it might get fiddlier...)

…

-- fisch On Thu, Feb 9, 2017 at 9:57 PM, Jeremy Morse <notifications@github.com> wrote:

Hi, On 09/02/17 19:53, Mikhail Ramalho wrote: > The down side: it will only be supported by the new frontend. Completely acceptable as far as I'm concerned, we should be comfortable with the old frontend dying. > They're using frama-c to do some interval analysis and define custom > bitvectors with arbitrary size. In a number of cases, the verification > time is much smaller. Sweet, > The easiest solution I could come up is to use source annotations, which > we already use for infinite sized arrays. I propose something like: > > *attribute*((annotate("bv=10"))) > int a; > > This is parsed by clang, we can still compile the code and it will > require little effort to implement. I can't immediately think of any circumstance that would break as a result of this, other than if pointers came anywhere near these bitvectors. We still don't do bitfields {well,at all}, and this is a specialization of bitfields. If they're attacking this from the python-api or SSA level directly, obviously they can bypass any risk of pointer stuff. -- Thanks, Jeremy — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <https://github.com/esbmc/esbmc-private/issues/165#issuecomment-278754411>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEF9N7k0MswYhF4jRzbhJuPFwerhPoe-ks5ra2-ugaJpZM4L8lxz> .

[github-actions]

Stale issue message

[github-actions]

Stale issue message

[lucasccordeiro]

This issue is obsolete. We already handle custom size bitvectors:

https://github.com/esbmc/esbmc/tree/master/regression/esbmc/bitvector_01
https://github.com/esbmc/esbmc/tree/master/regression/esbmc/bitvector_02
https://github.com/esbmc/esbmc/tree/master/regression/esbmc/bitvector_03
https://github.com/esbmc/esbmc/tree/master/regression/esbmc/bitvector_04