Programmatic expression for the size of a CPROVER_bitvector

[Andreas Tiemeyer]

I am using CPROVER_bitvector for implementing operations on integers of arbitrary bounds, as found in e.g. the SystemC integer data types. 

For the implementation it would be useful to express the size of a CPROVER_bitvector programatically, for example with something like

CPROVER_bitvector[243] bv;

int size = CPROVER_size(bv);

where the value of size would be 243.

Is something like this supported, or if not can someone suggest a work-around?

Thank you in advance,

Andreas

[Martin Nyx Brain]

sizeof(bv) * CHAR_BITS should work but will give you it rounded up to
bytes. Alternatively:

#define BVSIZE 243
CPROVER_bitvector[BVSIZE] bv;

should work and has the option to set the size at analysis type from
the cbmc command-line:

cbmc -DBVSIZE=243 whatever.c

HTH

Cheers,
- Martin

[Andreas Tiemeyer]

What we are looking for is a version of sizeof() that counts bits rather than bytes. A possible solution would be to implement it as a built-in CPROVER function like CPROVER_array_copy. I was hoping that such a function already existed. I guess it was not needed before, because datatypes usually have a size that is a multiple of CHAR_BITS.

Andreas

[Martin Nyx Brain]

On Wed, 2021-06-09 at 22:52 -0700, Andreas Tiemeyer wrote:
> What we are looking for is a version of sizeof() that counts bits
> rather
> than bytes. A possible solution would be to implement it as a built-
> in
> CPROVER function like CPROVER_array_copy. I was hoping that such a
> function
> already existed. I guess it was not needed before, because datatypes
> usually have a size that is a multiple of CHAR_BITS.

Yes; the __CPROVER_bitvector types are not particularly widely used so
it might be that you are just the first person to ask. A built-in
function that works like sizeof() is probably the best way to do if you
want the solver to know, rather than just using a macro to define the
size of the bitvector.

Cheers,
- Martin